syntax.ml

   1: (** Abstract syntax *)
   2: 
   3: (** The type of variable names. *)
   4: type name = string
   5: 
   6: (** MiniHaskell types. *)
   7: type htype =
   8:     TInt (** integer [int] *)
   9:   | TBool (** booleans [bool] *)
  10:   | TTimes of htype * htype  (** Product [s * t] *)
  11:   | TArrow of htype * htype  (** Function type *)
  12:   | TList of htype (** Lists [t list] *)
  13: 
  14: (** MiniHaskell expressions *)
  15: type expr =
  16:     Var of name          (** variable *)
  17:   | Int of int           (** integer constant *)
  18:   | Bool of bool         (** boolean constant *)
  19:   | Times of expr * expr (** product [e1 * e2] *)
  20:   | Divide of expr * expr(** quotient [e1 / e2] *)
  21:   | Mod of expr * expr   (** remainder [e1 % e2] *)
  22:   | Plus of expr * expr  (** sum [e1 + e2] *)
  23:   | Minus of expr * expr (** difference [e1 - e2] *)
  24:   | Equal of expr * expr (** integer equality [e1 = e2] *)
  25:   | Less of expr * expr  (** integer comparison [e1 < e2] *)
  26:   | If of expr * expr * expr (** conditional [if e1 then e2 else e3] *)
  27:   | Fun of name * htype * expr (** function [fun x:t -> e] *)
  28:   | Apply of expr * expr (** application [e1 e2] *)
  29:   | Pair of expr * expr  (** pair [(e1, e2)] *)
  30:   | Fst of expr          (** first projection [fst e] *)
  31:   | Snd of expr          (** second projection [snd e] *)
  32:   | Rec of name * htype * expr (** recursion [rec x:t is e] *)
  33:   | Nil of htype         (** empty list *)
  34:   | Cons of expr * expr  (** cons list [e1 :: e2] *)
  35:   | Match of expr * htype * expr * name * name * expr (** list decomposition [match e with [t] -> e1 | x::y -> e2] *)
  36: 
  37: (** Toplevel commands *)
  38: type toplevel_cmd =
  39:     Expr of expr       (** an expression to be evaluated *)
  40:   | Def of name * expr (** toplevel definition [let x = e] *)
  41:   | Use of string      (** load a file [$use "<filename>"] *)
  42:   | Quit               (** exit toplevel [$quit] *)
  43: 
  44: (** Conversion from a type to a string *)
  45: let string_of_type ty =
  46:   let rec to_str n ty =
  47:     let (m, str) =
  48:       match ty with
  49:           TInt -> (4, "int")
  50:         | TBool -> (4, "bool")
  51:         | TList ty -> (3, to_str 3 ty ^ " list")
  52:         | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2))
  53:         | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2))
  54:     in
  55:       if m > n then str else "(" ^ str ^ ")"
  56:   in
  57:     to_str (-1) ty
  58: 
  59: (** Conversion from an expression to a string *)
  60: let string_of_expr e =
  61:   let rec to_str n e =
  62:     let (m, str) =
  63:       match e with
  64:           Int n ->          (10, string_of_int n)
  65:         | Bool b ->         (10, string_of_bool b)
  66:         | Var x ->          (10, x)
  67:         | Pair (e1, e2) ->  (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")")
  68:         | Nil ty ->         (10, "[" ^ (string_of_type ty) ^ "]")
  69:         | Fst e ->           (9, "fst " ^ (to_str 9 e))
  70:         | Snd e ->           (9, "snd " ^ (to_str 9 e))
  71:         | Apply (e1, e2) ->  (10, "<app>")
  72:             (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *)
  73:         | Times (e1, e2) ->  (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2))
  74:         | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2))
  75:         | Mod (e1, e2) ->    (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2))
  76:         | Plus (e1, e2) ->   (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2))
  77:         | Minus (e1, e2) ->  (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2))
  78:         | Cons (e1, e2) ->   (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2))
  79:         | Equal (e1, e2) ->  (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2))
  80:         | Less (e1, e2) ->   (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2))
  81:         | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^
  82:                                 (to_str 4 e2) ^ " else " ^ (to_str 4 e3))
  83:         | Match (e1, ty, e2, x, y, e3) ->
  84:             (3, "match " ^ (to_str 3 e1) ^ " with " ^
  85:                "[" ^ (string_of_type ty) ^ "] -> " ^ (to_str 3 e2) ^ " | " ^
  86:                x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3))
  87:         | Fun (x, ty, e) -> (10, "<fun>")
  88:             (* (2, "fun " ^ x ^ " : " ^ (string_of_type ty) ^ " -> " ^ (to_str 0 e)) *)
  89:         | Rec (x, ty, e) -> (10, "<rec>")
  90:             (* (1, "rec " ^ x ^ " : " ^ (string_of_type ty) ^ " is " ^ (to_str 0 e)) *)
  91:                
  92:     in
  93:       if m > n then str else "(" ^ str ^ ")"
  94:   in
  95:     to_str (-1) e
  96: 
  97: (** [subst [(x1,e1);...;(xn;en)] e] replaces in [e] free occurrences
  98:     of variables [x1], ..., [xn] with expressions [e1], ..., [en]. *)
  99: let rec subst s = function
 100:   |  (Var x) as e -> (try List.assoc x s with Not_found -> e)
 101:   | (Int _ | Bool _ | Nil _) as e -> e
 102:   | Times (e1, e2) -> Times (subst s e1, subst s e2)
 103:   | Divide (e1, e2) -> Divide (subst s e1, subst s e2)
 104:   | Mod (e1, e2) -> Mod (subst s e1, subst s e2)
 105:   | Plus (e1, e2) -> Plus (subst s e1, subst s e2)
 106:   | Minus (e1, e2) -> Minus (subst s e1, subst s e2)
 107:   | Equal (e1, e2) -> Equal (subst s e1, subst s e2)
 108:   | Cons (e1, e2) -> Cons  (subst s e1, subst s e2)
 109:   | Less (e1, e2) -> Less (subst s e1, subst s e2)
 110:   | If (e1, e2, e3) -> If (subst s e1, subst s e2, subst s e3)
 111:   | Fun (x, ty, e) -> let s' = List.remove_assoc x s in Fun (x, ty, subst s' e)
 112:   | Rec (x, ty, e) -> let s' = List.remove_assoc x s in Rec (x, ty, subst s' e)
 113:   | Match (e1, ty, e2, x, y, e3) ->
 114:       let s' = List.remove_assoc y (List.remove_assoc x s) in
 115:         Match (subst s e1, ty, subst s e2, x, y, subst s' e3)
 116:   | Apply (e1, e2) -> Apply (subst s e1, subst s e2)
 117:   | Pair (e1, e2) -> Pair (subst s e1, subst s e2)
 118:   | Fst e -> Fst (subst s e)
 119:   | Snd e -> Snd (subst s e)

type_check.ml

   1: (** Type checking. *)
   2: 
   3: open Syntax
   4: 
   5: (** Exception indicating a type-checking error. *)
   6: exception Type_error of string
   7: 
   8: (** [ty_error msg] raises exception [Type_error msg]. *)
   9: let type_error msg = raise (Type_error msg)
  10: 
  11: (** [check ctx ty e] checks that expression [e] has type [ty] in context [ctx].
  12:     It raises [Type_error] if it does not. *)
  13: let rec check ctx ty e =
  14:   let ty' = type_of ctx e in
  15:     if ty' <> ty then
  16:       type_error
  17:         (string_of_expr e ^ " has type " ^ string_of_type ty' ^
  18:          " but is used as if it had type " ^ string_of_type ty)
  19: 
  20: (** [type-of ctx e] computes the type of expression [e] in context [ctx].
  21:     It raises [Type_error] if [e] does not have a type. *)
  22: and type_of ctx = function
  23:   | Var x ->
  24:       (try List.assoc x ctx with
  25:            Not_found -> type_error ("unknown identifier " ^ x))
  26:   | Int _ -> TInt
  27:   | Bool _ -> TBool
  28:   | Nil ty -> TList ty
  29:   | Times (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt
  30:   | Divide (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt
  31:   | Mod (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt
  32:   | Plus (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt
  33:   | Cons (e1, e2) -> let ty = type_of ctx e1 in check ctx (TList ty) e2; TList ty
  34:   | Minus (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt
  35:   | Equal (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TBool
  36:   | Less (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TBool
  37:   | If (e1, e2, e3) ->
  38:       check ctx TBool e1 ;
  39:       let ty = type_of ctx e2 in
  40:         check ctx ty e3 ; ty
  41:   | Fun (x, ty, e) -> TArrow (ty, type_of ((x,ty)::ctx) e)
  42:   | Rec (x, ty, e) -> check ((x,ty)::ctx) ty e; ty
  43:   | Match (e1, ty, e2, x, y, e3) ->
  44:       (match type_of ctx e1 with
  45:            TList ty1 ->
  46:              check ctx (TList ty) e1;
  47:              let ty2 = type_of ctx e2 in
  48:                check ((x,ty)::(y, TList ty)::ctx) ty2 e3 ; ty2
  49:          | ty -> type_error (string_of_expr e1 ^
  50:                             " is used as a list but its type is " ^
  51:                             string_of_type ty))
  52:   | Apply (e1, e2) ->
  53:       (match type_of ctx e1 with
  54:            TArrow (ty1, ty2) -> check ctx ty1 e2 ; ty2
  55:          | ty ->
  56:              type_error (string_of_expr e1 ^
  57:                          " is used as a function but its type is " ^
  58:                          string_of_type ty))
  59:         | Pair (e1, e2) -> TTimes (type_of ctx e1, type_of ctx e2)
  60:   | Fst e ->
  61:       (match type_of ctx e with
  62:            TTimes (ty1, _) -> ty1
  63:          | ty ->
  64:              type_error (string_of_expr e ^
  65:                          " is used as a pair but its type is " ^
  66:                          string_of_type ty))
  67:   | Snd e ->
  68:       (match type_of ctx e with
  69:            TTimes (_, ty2) -> ty2
  70:          | ty ->
  71:              type_error (string_of_expr e ^
  72:                          " is used as a pair but its type is " ^
  73:                          string_of_type ty))
  74: 

eval.ml

   1: (** Small step semantics, for demonstration purposes only. *)
   2: 
   3: open Syntax
   4: 
   5: (** [is_value e] returns [true], if [e] is a value. *)
   6: let rec is_value = function
   7:     Int _ | Bool _ | Fun _ | Nil _ | Cons _ | Pair _ -> true
   8:   | Var _ | Times _ | Divide _ | Mod _ | Plus _ | Minus _
   9:   | Equal _ | Less _ | If _ | Apply _
  10:   | Match _ | Rec _ | Fst _ | Snd _ -> false
  11: 
  12: (** Expression [Eval_error] indicates a runtime error. *)
  13: exception Eval_error
  14: 
  15: (** [eval1 e] izvede en korak v evaluaciji zaprtega izraz [e]. Èe
  16: naslednjega koraka ni, se spro¾i izjema [Eval_error], ki lahko pomeni
  17: bodisi, da je [e] konèna vrednost, bodisi da je [e] blokiral. *)
  18: 
  19: (** [eval1 e] performs one evaluation step of program [e]. If there is
  20:     no next step, it raises [Eval_error], which happens if [e] is a value
  21:     or if [e] gets stuck. *)
  22: let rec eval1 = function
  23:   | Var _ | Int _ | Bool _ | Fun _ | Nil _ | Pair _ | Cons _ -> raise Eval_error
  24:   | Times (Int k1, Int k2) -> Int (k1 * k2)
  25:   | Times (Int k1, e2)     -> Times (Int k1, eval1 e2)
  26:   | Times (e1, e2)         -> Times (eval1 e1, e2)
  27:   | Divide (Int k1, Int k2)-> Int (k1 / k2)
  28:   | Divide (Int k1, e2)    -> Divide (Int k1, eval1 e2)
  29:   | Divide (e1, e2)        -> Divide (eval1 e1, e2)
  30:   | Mod (Int k1, Int k2)   -> Int (k1 mod k2)
  31:   | Mod (Int k1, e2)       -> Mod (Int k1, eval1 e2)
  32:   | Mod (e1, e2)           -> Mod (eval1 e1, e2)
  33:   | Plus (Int k1, Int k2)  -> Int (k1 + k2)
  34:   | Plus (Int k1, e2)      -> Plus (Int k1, eval1 e2)
  35:   | Plus (e1, e2)          -> Plus (eval1 e1, e2)
  36:   | Minus (Int k1, Int k2) -> Int (k1 - k2)
  37:   | Minus (Int k1, e2)     -> Minus (Int k1, eval1 e2)
  38:   | Minus (e1, e2)         -> Minus (eval1 e1, e2)
  39:   | Equal (Int k1, Int k2) -> Bool (k1 = k2)
  40:   | Equal (Int k1, e2)     -> Equal (Int k1, eval1 e2)
  41:   | Equal (e1, e2)         -> Equal (eval1 e1, e2)
  42:   | Less (Int k1, Int k2)  -> Bool (k1 < k2)
  43:   | Less (Int k1, e2)      -> Less (Int k1, eval1 e2)
  44:   | Less (e1, e2)          -> Less (eval1 e1, e2)
  45:   | If (Bool true, e2, e3) -> e2
  46:   | If (Bool false, e2, e3)-> e3
  47:   | If (e1, e2, e3)        -> If (eval1 e1, e2, e3)
  48:   | Apply (Fun (x, _, e), e2) -> subst [(x, e2)] e
  49:   | Apply (e1, e2) -> Apply (eval1 e1, e2)
  50:   | Rec (x, _, e') as e -> subst [(x,e)] e'
  51:   | Match (Nil _, _, e, _, _, _) -> e
  52:   | Match (Cons (e1, e2), _, _, x, y, e) -> subst [(x,e1);(y,e2)] e
  53:   | Match (e1, ty, e2, x, y, e3) -> Match (eval1 e1, ty, e2, x, y, e3)
  54:   | Fst (Pair (e1, _)) -> e1
  55:   | Fst e -> Fst (eval1 e)
  56:   | Snd (Pair (_, e2)) -> e2
  57:   | Snd e -> Snd (eval1 e)
  58: 
  59: (** [eval n e] evaluates program [e]. It raises [Eval_error] if [e] gets stuck.
  60:     It forces up to [n] levels of evaluation in pairs and lists. This function
  61:     is inefficient and is here for demostration purposes only. See module [Interpret]
  62:     for a more efficient version.
  63: *)
  64: let rec eval n e =
  65:   let rec loop = function
  66:       Pair (e1, e2) -> Pair (eval (n-1) e1, eval (n-1) e2)
  67:     | Cons (e1, e2) -> Cons (eval n e1, if n <= 0 then e2 else eval (n-1) e2)
  68:     | e when is_value e -> e
  69:     | e -> loop (eval1 e)
  70:   in
  71:     loop e

interpret.ml

   1: (** An efficient interpreter. *)
   2: 
   3: open Syntax
   4: 
   5: type environment = (name * value ref) list
   6: 
   7: and value =
   8:   | VInt of int
   9:   | VBool of bool
  10:   | VNil of htype
  11:   | VClosure of environment * expr
  12: 
  13: exception Runtime_error of string
  14: 
  15: let runtime_error msg = raise (Runtime_error msg)
  16: 
  17: let rec interp env = function
  18:     Var x ->
  19:       (try
  20:          let r = List.assoc x env in
  21:            match !r with
  22:                VClosure (env', e) -> let v = interp env' e in r := v ; v
  23:              | v -> v
  24:        with
  25:            Not_found -> runtime_error ("Unknown variable " ^ x))
  26:   | Int k -> VInt k
  27:   | Bool b -> VBool b
  28:   | Times (e1, e2) ->
  29:       (match (interp env e1), (interp env e2) with
  30:            VInt k1, VInt k2 -> VInt (k1 * k2)
  31:          | _ -> runtime_error "Integers expected in multiplication")
  32:   | Divide (e1, e2) ->
  33:       (match (interp env e1), (interp env e2) with
  34:            VInt k1, VInt 0  -> runtime_error ("Division by 0")
  35:          | VInt k1, VInt k2 -> VInt (k1 / k2)
  36:          | _ -> runtime_error "Integers expected in division")
  37:   | Mod (e1, e2) ->
  38:       (match (interp env e1), (interp env e2) with
  39:            VInt k1, VInt 0  -> runtime_error ("Division by 0")
  40:          | VInt k1, VInt k2 -> VInt (k1 mod k2)
  41:          | _ -> runtime_error "Integers expected in remainder")
  42:   | Plus (e1, e2) ->
  43:       (match (interp env e1), (interp env e2) with
  44:            VInt k1, VInt k2 -> VInt (k1 + k2)
  45:          | _ -> runtime_error "Integers expected in addition")
  46:   | Minus (e1, e2) ->
  47:       (match (interp env e1), (interp env e2) with
  48:            VInt k1, VInt k2 -> VInt (k1 - k2)
  49:          | _ -> runtime_error "Integers expected in subtraction")
  50:   | Equal (e1, e2) ->
  51:       (match (interp env e1), (interp env e2) with
  52:            VInt k1, VInt k2 -> VBool (k1 = k2)
  53:          | _ -> runtime_error "Integers expected in =")
  54:   | Less (e1, e2) ->
  55:       (match (interp env e1), (interp env e2) with
  56:            VInt k1, VInt k2 -> VBool (k1 < k2)
  57:          | _ -> runtime_error "Integers expected in <")
  58:   | If (e1, e2, e3) ->
  59:       (match interp env e1 with
  60:            VBool true -> interp env e2
  61:          | VBool false -> interp env e3
  62:          | _ -> runtime_error "Boolean expected in if")
  63:   | Fun _ as e -> VClosure (env, e)
  64:   | Apply (e1, e2) ->
  65:       (match interp env e1 with
  66:            VClosure (env', Fun (x, _, e)) ->
  67:              interp ((x, ref (VClosure (env, e2)))::env') e
  68:          | _ -> runtime_error "Function expected in application")
  69:   | Pair _ as e ->  VClosure (env, e)
  70:   | Fst e ->
  71:       (match interp env e with
  72:            VClosure (env', Pair (e1, e2)) -> interp env' e1
  73:          | _ -> runtime_error "Pair expected in fst")
  74:   | Snd e ->
  75:       (match interp env e with
  76:            VClosure (env', Pair (e1, e2)) -> interp env' e2
  77:          | _ -> runtime_error "Pair expected in snd")
  78:   | Rec (x, _, e) -> 
  79:       let rec env' = (x,ref (VClosure (env',e))) :: env in
  80:         interp env' e
  81:   | Nil ty -> VNil ty
  82:   | Cons _ as e -> VClosure (env, e)
  83:   | Match (e1, _, e2, x, y, e3) ->
  84:       (match interp env e1 with
  85:            VNil _ -> interp env e2
  86:          | VClosure (env', Cons (d1, d2)) ->
  87:              interp ((x,ref (VClosure(env',d1)))::(y,ref (VClosure(env',d2)))::env) e3
  88:          | _ -> runtime_error "List expected in match")
  89: 
  90: 
  91: let rec print_result n v =
  92:   (if n = 0 then
  93:      print_string "..."
  94:    else
  95:      match v with
  96:          VInt k -> print_int k
  97:        | VBool b -> print_string (string_of_bool b)
  98:        | VNil ty -> print_string ("[" ^ string_of_type ty ^ "]")
  99:        | VClosure (env, Pair (e1, e2)) ->
 100:           print_char '(' ;
 101:           print_result (n/2) (interp env e1) ;
 102:           print_string ", " ;
 103:           print_result (n/2) (interp env e2) ;
 104:           print_char ')'
 105:       | VClosure (env, Cons (e1, e2)) ->
 106:           let v1 = interp env e1 in
 107:             (match v1 with
 108:                  VClosure (_, Cons _) ->
 109:                    print_char '(' ; print_result (n/2) v1 ; print_char ')'
 110:                | _ -> print_result (n/2) v1) ;
 111:           print_string " :: " ;
 112:           print_result (n-1) (interp env e2)
 113:       | VClosure (_, Fun _) -> print_string "<fun>"
 114:       | _ -> print_string "?"
 115:   ) ;
 116:   flush stdout

lexer.mll

   1: {
   2:   open Parser
   3:   open Lexing
   4: 
   5:   let incr_linenum lexbuf =
   6:     let pos = lexbuf.lex_curr_p in
   7:     lexbuf.lex_curr_p <- { pos with
   8:       pos_lnum = pos.pos_lnum + 1;
   9:       pos_bol = pos.pos_cnum;
  10:     }
  11: }
  12: 
  13: let var = ['_' 'a'-'z' 'A'-'Z'] ['_' 'a'-'z' 'A'-'Z' '0'-'9']*
  14: 
  15: rule token = parse
  16:     '#' [^'\n']* '\n' { incr_linenum lexbuf; token lexbuf }
  17:   | '\n'            { incr_linenum lexbuf; token lexbuf }
  18:   | [' ' '\t']      { token lexbuf }
  19:   | ['0'-'9']+      { INT (int_of_string(lexeme lexbuf)) }
  20:   | "bool"          { TBOOL }
  21:   | "else"          { ELSE }
  22:   | "false"         { FALSE }
  23:   | "fst"           { FST }
  24:   | "fun"           { FUN }
  25:   | "if"            { IF }
  26:   | "int"           { TINT }
  27:   | "is"            { IS }
  28:   | "let"           { LET }  
  29:   | "list"          { TLIST }
  30:   | "match"         { MATCH }
  31:   | "rec"           { REC }
  32:   | "snd"           { SND }
  33:   | "then"          { THEN }
  34:   | "true"          { TRUE }
  35:   | "$use"           { USE }
  36:   | "$quit"          { QUIT }
  37:   | "with"          { WITH }
  38:   | "->"            { ARROW }
  39:   | "::"            { CONS }
  40:   | ";;"            { SEMICOLON2 }
  41:   | '\"' [^'\"']* '\"' { let str = lexeme lexbuf in
  42:                         STRING (String.sub str 1 (String.length str - 2)) }
  43:   | '%'             { MOD }
  44: