syntax.ml

   1: (** Abstract syntax *)
   2: 
   3: (** The type of variable names. *)
   4: type name = string
   5: 
   6: (** Types in Poly. *)
   7: type htype =
   8:   | TInt                     (** integers [int] *)
   9:   | TBool                    (** booleans [bool] *)
  10:   | TParam of int            (** parameter *)
  11:   | TTimes of htype * htype  (** Product [s * t] *)
  12:   | TArrow of htype * htype  (** Function type [s -> t] *)
  13:   | TList of htype           (** Lists *)
  14: 
  15: (** Poly expressions. *)
  16: type expr =
  17:   | Var of name          (* variable *)
  18:   | Int of int           (* integer constant *)
  19:   | Bool of bool         (* boolean value *)
  20:   | Times of expr * expr (* product [e1 * e2] *)
  21:   | Divide of expr * expr(* quotient [e1 / e2] *)
  22:   | Mod of expr * expr   (* remainder [e1 % e2] *)
  23:   | Plus of expr * expr  (* sum [e1 + e2] *)
  24:   | Minus of expr * expr (* difference [e1 - e2] *)
  25:   | Equal of expr * expr (* integer equality [e1 = e2] *)
  26:   | Less of expr * expr  (* integer comparison [e1 < e2] *)
  27:   | If of expr * expr * expr (* conditional [if e1 then e2 else e3] *)
  28:   | Fun of name * expr   (* function [fun x -> e] *)
  29:   | Apply of expr * expr (* application [e1 e2] *)
  30:   | Pair of expr * expr  (* ordered pair [(e1, e2)] *)
  31:   | Fst of expr          (* first projection [fst e] *)
  32:   | Snd of expr          (* second projection [snd e] *)
  33:   | Rec of name * expr   (* recursion [rec x is e] *)
  34:   | Nil                  (* empty list *)
  35:   | Cons of expr * expr  (* cons list *)
  36:   | Match of expr * expr * name * name * expr
  37:       (* list decomposition [match e with [] -> e1 | x::y -> e2] *)
  38: 
  39: (** Toplevel commands *)
  40: type toplevel_cmd =
  41:   | Expr of expr       (* an expression to be evaluated *)
  42:   | Def of name * expr (* toplevel definition [let x = e] *)
  43:   | Use of string      (* load a file [$use "<filename"] *)
  44:   | Quit               (* exit toplevel [$quit] *)
  45: 
  46: (** [rename t] renames parameters in type [t] so that they count from
  47:     [0] up. This is useful for pretty printing. *)
  48: let rename ty =
  49:   let rec ren ((j,s) as c) = function
  50:     | TInt -> TInt, c
  51:     | TBool -> TBool, c
  52:     | TParam k ->
  53:         (try
  54:            TParam (List.assoc k s), c
  55:          with 
  56:              Not_found -> TParam j, (j+1, (k, j)::s))
  57:     | TArrow (t1, t2) ->
  58:         let u1, c'  = ren c t1 in
  59:         let u2, c'' = ren c' t2 in
  60:           TArrow (u1,u2), c''
  61:     | TTimes (t1, t2) ->
  62:         let u1, c'  = ren c t1 in
  63:         let u2, c'' = ren c' t2 in
  64:           TTimes (u1,u2), c''
  65:     | TList t ->
  66:         let u, c' = ren c t in TList u, c'
  67:   in
  68:     fst (ren (0,[]) ty)
  69: 
  70: (** [rename t1 t2] simultaneously renames types [t1] and [t2] so that
  71:     parameters appearing in them are numbered from [0] on. *)
  72: let rename2 t1 t2 =
  73:   match rename (TTimes (t1,t2)) with
  74:       TTimes (u1, u2) -> u1, u2
  75:     | _ -> assert false
  76: 
  77: (** [string_of_type] converts a Poly type to string. *)
  78: let string_of_type ty =
  79:   let a = [|"a";"b";"c";"d";"e";"f";"g";"h";"i";
  80:             "j";"k";"l";"m";"n";"o";"p";"q";"r";
  81:             "s";"t";"u";"v";"w";"x";"y";"z"|]
  82:   in
  83:   let rec to_str n ty =
  84:     let (m, str) =
  85:       match ty with
  86:         | TInt -> (4, "int")
  87:         | TBool -> (4, "bool")
  88:         | TParam k -> (4, (if k < Array.length a then "'" ^ a.(k) else "'ty" ^ string_of_int k))
  89:         | TList ty -> (3, to_str 3 ty ^ " list")
  90:         | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2))
  91:         | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2))
  92:     in
  93:       if m > n then str else "(" ^ str ^ ")"
  94:   in
  95:     to_str (-1) ty
  96: 
  97: (** [string_of_expr e] converts expression [e] to string. *)
  98: let string_of_expr e =
  99:   let rec to_str n e =
 100:     let (m, str) =
 101:       match e with
 102:           Int n ->          (10, string_of_int n)
 103:         | Bool b ->         (10, string_of_bool b)
 104:         | Var x ->          (10, x)
 105:         | Pair (e1, e2) ->  (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")")
 106:         | Nil ->            (10, "[]")
 107:         | Fst e ->           (9, "fst " ^ (to_str 9 e))
 108:         | Snd e ->           (9, "snd " ^ (to_str 9 e))
 109:         | Apply (e1, e2) ->  (10, "<app>")
 110:             (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *)
 111:         | Times (e1, e2) ->  (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2))
 112:         | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2))
 113:         | Mod (e1, e2) ->    (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2))
 114:         | Plus (e1, e2) ->   (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2))
 115:         | Minus (e1, e2) ->  (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2))
 116:         | Cons (e1, e2) ->   (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2))
 117:         | Equal (e1, e2) ->  (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2))
 118:         | Less (e1, e2) ->   (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2))
 119:         | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^
 120:                                 (to_str 4 e2) ^ " else " ^ (to_str 4 e3))
 121:         | Match (e1, e2, x, y, e3) ->
 122:             (3, "match " ^ (to_str 3 e1) ^ " with " ^
 123:                "[] -> " ^ (to_str 3 e2) ^ " | " ^
 124:                x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3))
 125:         | Fun (x, e) -> (10, "<fun>")
 126:             (* (2, "fun " ^ x ^  " -> " ^ (to_str 0 e)) *)
 127:         | Rec (x, e) -> (10, "<rec>")
 128:             (* (1, "rec " ^ x ^ " is " ^ (to_str 0 e)) *)
 129:                
 130:     in
 131:       if m > n then str else "(" ^ str ^ ")"
 132:   in
 133:     to_str (-1) e
 134: 
 135: (** [subst [(x1,e1);...;(xn;en)] e] replaces in [e] free occurrences
 136:     of variables [x1], ..., [xn] with expressions [e1], ..., [en]. *)
 137: let rec subst s = function
 138:   | (Var x) as e -> (try List.assoc x s with Not_found -> e)
 139:   | (Int _ | Bool _ | Nil) as e -> e
 140:   | Times (e1, e2) -> Times (subst s e1, subst s e2)
 141:   | Divide (e1, e2) -> Divide (subst s e1, subst s e2)
 142:   | Mod (e1, e2) -> Mod (subst s e1, subst s e2)
 143:   | Plus (e1, e2) -> Plus (subst s e1, subst s e2)
 144:   | Minus (e1, e2) -> Minus (subst s e1, subst s e2)
 145:   | Equal (e1, e2) -> Equal (subst s e1, subst s e2)
 146:   | Cons (e1, e2) -> Cons  (subst s e1, subst s e2)
 147:   | Less (e1, e2) -> Less (subst s e1, subst s e2)
 148:   | If (e1, e2, e3) -> If (subst s e1, subst s e2, subst s e3)
 149:   | Fun (x, e) -> let s' = List.remove_assoc x s in Fun (x, subst s' e)
 150:   | Rec (x, e) -> let s' = List.remove_assoc x s in Rec (x, subst s' e)
 151:   | Match (e1, e2, x, y, e3) ->
 152:       let s' = List.remove_assoc y (List.remove_assoc x s) in
 153:         Match (subst s e1, subst s e2, x, y, subst s' e3)
 154:   | Apply (e1, e2) -> Apply (subst s e1, subst s e2)
 155:   | Pair (e1, e2) -> Pair (subst s e1, subst s e2)
 156:   | Fst e -> Fst (subst s e)
 157:   | Snd e -> Snd (subst s e)
 158: 
 159: (** [tsubst [(k1,t1); ...; (kn,tn)] t] replaces in type [t] parameters
 160:     [TParam ki] with types [ti]. *)
 161: let rec tsubst s = function
 162:   | (TInt | TBool) as t -> t
 163:   | TParam k -> (try List.assoc k s with Not_found -> TParam k)
 164:   | TTimes (t1, t2) -> TTimes (tsubst s t1, tsubst s t2)
 165:   | TArrow (t1, t2) -> TArrow (tsubst s t1, tsubst s t2)
 166:   | TList t -> TList (tsubst s t)

type_infer.ml

   1: (* Type inference *)
   2: 
   3: open Syntax
   4: 
   5: exception Type_error of string
   6: 
   7: (** [ty_error msg] reports a type error by raising [Type_error msg]. *)
   8: let type_error msg = raise (Type_error msg)
   9: 
  10: (** [fresh ()] returns an unused type parameter. *)
  11: let fresh =
  12:   let k = ref 0 in
  13:     fun () -> incr k; TParam !k
  14: 
  15: (** [refresh t] replaces all parameters appearing in [t] with unused ones. *)
  16: let refresh ty =
  17:   let rec refresh s = function
  18:     | TInt -> TInt, s
  19:     | TBool -> TBool, s
  20:     | TParam k ->
  21:         (try
  22:            List.assoc k s, s
  23:          with Not_found -> let t = fresh () in t, (k,t)::s)
  24:     | TArrow (t1, t2) ->
  25:         let u1, s'  = refresh s t1 in
  26:         let u2, s'' = refresh s' t2 in
  27:           TArrow (u1, u2), s''
  28:     | TTimes (t1, t2) ->
  29:         let u1, s'  = refresh s t1 in
  30:         let u2, s'' = refresh s' t2 in
  31:           TTimes (u1, u2), s''
  32:     | TList t ->
  33:         let u, s' = refresh s t in
  34:           TList u, s'
  35:   in
  36:     fst (refresh [] ty)
  37: 
  38: (** [occurs k t] returns [true] if parameter [TParam k] appears in type [t]. *)
  39: let rec occurs k = function
  40:   | TInt -> false
  41:   | TBool -> false
  42:   | TParam j -> k = j
  43:   | TArrow (t1, t2) -> occurs k t1 || occurs k t2
  44:   | TTimes (t1, t2) -> occurs k t1 || occurs k t2
  45:   | TList t -> occurs k t
  46: 
  47: (** [solve [(t1,u1); ...; (tn,un)] solves the system of equations
  48:     [t1=u1], ..., [tn=un]. The solution is represented by a list of
  49:     pairs [(k,t)], meaning that [TParam k] equals [t]. A type error is
  50:     raised if there is no solution. The solution found is the most general
  51:     one.
  52: *)
  53: let solve eq =
  54:   let rec solve eq sbst =
  55:     match eq with
  56:       | [] -> sbst
  57:           
  58:       | (t1, t2) :: eq when t1 = t2 -> solve eq sbst
  59:           
  60:       | ((TParam k, t) :: eq | (t, TParam k) :: eq) when (not (occurs k t)) ->
  61:           let ts = tsubst [(k,t)] in
  62:             solve
  63:               (List.map (fun (ty1,ty2) -> (ts ty1, ts ty2)) eq)
  64:               ((k,t)::(List.map (fun (n, u) -> (n, ts u)) sbst))
  65:               
  66:       | (TTimes (u1,v1), TTimes (u2,v2)) :: eq
  67:       | (TArrow (u1,v1), TArrow (u2,v2)) :: eq ->
  68:           solve ((u1,u2)::(v1,v2)::eq) sbst
  69:             
  70:       | (TList t1, TList t2) :: eq -> solve ((t1,t2) :: eq) sbst
  71:           
  72:       | (t1,t2)::_ ->
  73:           let u1, u2 = rename2 t1 t2 in
  74:             type_error ("The types " ^ string_of_type u1 ^ " and " ^
  75:                           string_of_type u2 ^ " are incompatible")
  76:   in
  77:     solve eq []
  78: 
  79: (** [constraints_of gctx e] infers the type of expression [e] and a set
  80:     of constraints, where [gctx] is global context of values that [e]
  81:     may refer to. *)
  82: let rec constraints_of gctx = 
  83:   let rec cnstr ctx = function
  84:     | Var x ->  
  85:         (try
  86:            List.assoc x ctx, []
  87:          with Not_found ->
  88:            (try
  89:               (* we call [refresh] here to get let-polymorphism *)
  90:               refresh (List.assoc x gctx), []
  91:             with Not_found -> type_error ("Unknown variable " ^ x)))
  92:           
  93:     | Int _ ->  TInt, []
  94: 
  95:     | Bool _ -> TBool, []
  96: 
  97:     | Nil -> TList (fresh ()), []
  98: 
  99:     | Times (e1, e2)
 100:     | Divide (e1, e2)
 101:     | Mod (e1, e2)
 102:     | Plus (e1, e2)
 103:     | Minus (e1, e2) ->
 104:         let ty1, eq1 = cnstr ctx e1 in
 105:         let ty2, eq2 = cnstr ctx e2 in
 106:           TInt, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2
 107: 
 108:     | Equal (e1, e2)
 109:     | Less (e1, e2) ->
 110:         let ty1, eq1 = cnstr ctx e1 in
 111:         let ty2, eq2 = cnstr ctx e2 in
 112:           TBool, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2
 113: 
 114:     | Cons (e1, e2) ->
 115:         let ty1, eq1 = cnstr ctx e1 in
 116:         let ty2, eq2 = cnstr ctx e2 in
 117:         let ty = TList ty1 in
 118:           ty, (ty2, ty) :: eq1 @ eq2
 119: 
 120:     | If (e1, e2, e3) ->
 121:         let ty1, eq1 = cnstr ctx e1 in
 122:         let ty2, eq2 = cnstr ctx e2 in
 123:         let ty3, eq3 = cnstr ctx e3 in
 124:           ty2, (ty1, TBool) :: (ty2, ty3) :: eq1 @ eq2 @ eq3
 125: 
 126:     | Fun (x, e) ->
 127:         let ty1 = fresh () in
 128:         let ty2, eq = cnstr ((x,ty1)::ctx) e in
 129:           TArrow (ty1, ty2), eq
 130: 
 131:     | Rec (x, e) ->
 132:         let ty1 = fresh () in
 133:         let ty2, eq = cnstr ((x,ty1)::ctx) e in
 134:           ty1, (ty1, ty2) :: eq
 135: 
 136:     | Match (e1, e2, x, y, e3) ->
 137:         let ty = fresh () in
 138:         let ty1, eq1 = cnstr ctx e1 in
 139:         let ty2, eq2 = cnstr ctx e2 in
 140:         let ty3, eq3 = cnstr ((x,ty)::(y, TList ty)::ctx) e3 in
 141:           ty2, (ty1, TList ty) :: (ty2, ty3) :: eq1 @ eq2 @ eq3
 142: 
 143:     | Apply (e1, e2) ->
 144:         let ty1, eq1 = cnstr ctx e1 in
 145:         let ty2, eq2 = cnstr ctx e2 in
 146:         let ty = fresh () in
 147:           ty, (ty1, TArrow (ty2,ty)) :: eq1 @ eq2
 148: 
 149:     | Pair (e1, e2) ->
 150:         let ty1, eq1 = cnstr ctx e1 in
 151:         let ty2, eq2 = cnstr ctx e2 in
 152:           TTimes (ty1, ty2), eq1 @ eq2
 153: 
 154:     | Fst e ->
 155:         let ty, eq = cnstr ctx e in
 156:         let ty1 = fresh () in
 157:         let ty2 = fresh () in
 158:           ty1, (ty, TTimes (ty1, ty2)) :: eq
 159: 
 160:     | Snd e ->
 161:         let ty, eq = cnstr ctx e in
 162:         let ty1 = fresh () in
 163:         let ty2 = fresh () in
 164:           ty2, (ty, TTimes (ty1, ty2)) :: eq
 165:   in
 166:     cnstr []
 167: 
 168: (** [type_of ctx e] computes the principal type of expression [e] in
 169:     context [ctx]. *)
 170: let type_of ctx e =
 171:   let ty, eq = constraints_of ctx e in
 172:     tsubst (solve eq) ty

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
  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 -> VNil
  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: (** [print_result n v] prints at most [n] nodes of the value [v]. *)
  92: let rec print_result n v =
  93:   (if n = 0 then
  94:      print_string "..."
  95:    else
  96:      match v with
  97:        | VInt k -> print_int k
  98:        | VBool b -> print_string (string_of_bool b)
  99:        | VNil -> print_string "[]"
 100:        | VClosure (env, Pair (e1, e2)) ->
 101:            print_char '(' ;
 102:            print_result (n/2) (interp env e1) ;
 103:            print_string ", " ;
 104:            print_result (n/2) (interp env e2) ;
 105:            print_char ')'
 106:        | VClosure (env, Cons (e1, e2)) ->
 107:            let v1 = interp env e1 in
 108:              (match v1 with
 109:                   VClosure (_, Cons _) ->
 110:                     print_char '(' ; print_result (n/2) v1 ; print_char ')'
 111:                 | _ -> print_result (n/2) v1) ;
 112:              print_string " :: " ;
 113:              print_result (n-1) (interp env e2)
 114:        | VClosure (_, Fun _) -> print_string "<fun>"
 115:        | _ -> print_string "?"
 116:   ) ;
 117:   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:   | '('             { LPAREN }
  45:   | ')'             { RPAREN }
  46:   | '*'             { TIMES }
  47:   | '+'             { PLUS }
  48:   | ','             { COMMA }
  49:   | '-'             { MINUS }
  50:   | '/'             { DIVIDE }
  51:   | ':'             { COLON }
  52:   | '<'             { LESS }
  53:   | '='             { EQUAL }
  54:   | '['             { LBRACK }
  55:   | ']'             { RBRACK }
  56:   | '|'             { ALTERNATIVE }
  57:   | var             { VAR (lexeme lexbuf) }
  58:   | eof             { EOF }
  59: 
  60: {
  61: }

parser.mly

   1: %{
   2:   open Syntax
   3: %}
   4: 
   5: %token TINT
   6: %token TBOOL
   7: %token TTIMES
   8: %token TARROW
   9: %token TLIST
  10: %token <Syntax.name> VAR
  11: %token <int> INT
  12: %token TRUE FALSE
  13: %token PLUS
  14: %token MINUS
  15: %token TIMES
  16: %token DIVIDE
  17: %token MOD
  18: %token EQUAL LESS
  19: %token IF THEN ELSE
  20: %token FUN ARROW
  21: %token COLON
  22: %token LPAREN RPAREN
  23: %token LET
  24: %token SEMICOLON2
  25: %token COMMA
  26: %token FST
  27: %token SND
  28: %token LBRACK RBRACK
  29: %token CONS
  30: %token MATCH WITH ALTERNATIVE
  31: %token REC IS
  32: %token QUIT
  33: %token USE
  34: %token <string>STRING
  35: %token EOF
  36: 
  37: %start toplevel
  38: %type <Syntax.toplevel_cmd list> toplevel
  39: 
  40: %nonassoc REC IS
  41: %right FUN ARROW
  42: %nonassoc MATCH WITH
  43: %nonassoc IF THEN ELSE
  44: %nonassoc EQUAL LESS
  45: %left PLUS MINUS
  46: %left TIMES DIVIDE MOD
  47: %right CONS
  48: %right TARROW
  49: %left TTIMES
  50: %nonassoc TLIST
  51: 
  52: %%
  53: 
  54: toplevel:
  55:   | EOF                      { [] }
  56:   | lettop                   { $1 }
  57:   | exprtop                  { $1 }
  58:   | cmdtop                   { $1 }
  59: 
  60: lettop:
  61:   | def EOF                  { [$1] }
  62:   | def lettop               { $1 :: $2 }
  63:   | def SEMICOLON2 toplevel  { $1 :: $3 }
  64: 
  65: exprtop:
  66:   | expr EOF                 { [Expr $1] }
  67:   | expr SEMICOLON2 toplevel { Expr $1 :: $3 }
  68: 
  69: cmdtop:
  70:   | cmd EOF                  { [$1] }
  71:   | cmd SEMICOLON2 toplevel  { $1 :: $3 }
  72: 
  73: cmd:
  74:   | USE STRING { Use $2 }
  75:   | QUIT       { Quit }
  76: 
  77: def: LET VAR EQUAL expr { Def ($2, $4) }
  78: 
  79: expr:
  80:   | non_app             { $1 }
  81:   | app                 { $1 }
  82:   | arith               { $1 }
  83:   | boolean             { $1 }
  84:   | expr CONS expr      { Cons ($1, $3) }
  85:   | IF expr THEN expr ELSE expr        { If ($2, $4, $6) }
  86:   | FUN VAR ARROW expr  { Fun ($2, $4) }
  87:   | REC VAR IS expr     { Rec ($2, $4) }
  88:   | MATCH expr WITH nil ARROW expr ALTERNATIVE VAR CONS VAR ARROW expr
  89:       { Match ($2, $6, $8, $10, $12) }
  90: 
  91: app:
  92:     app non_app         { Apply ($1, $2) }
  93:   | FST non_app         { Fst $2 }
  94:   | SND non_app         { Snd $2 }
  95:   | non_app non_app     { Apply ($1, $2) }
  96: 
  97: non_app:
  98:     VAR                                  { Var $1 }
  99:   | TRUE                          { Bool true }
 100:   | FALSE                         { Bool false }
 101:   | INT                                  { Int $1 }
 102:   | nil                           { Nil }
 103:   | LPAREN expr RPAREN                  { $2 }    
 104:   | LPAREN expr COMMA expr RPAREN { Pair ($2, $4) }
 105: 
 106: arith:
 107:   | MINUS INT           { Int (-$2) }
 108:   | expr PLUS expr        { Plus ($1, $3) }
 109:   | expr MINUS expr        { Minus ($1, $3) }
 110:   | expr TIMES expr        { Times ($1, $3) }
 111:   | expr DIVIDE expr        { Divide ($1, $3) }
 112:   | expr MOD expr        { Mod ($1, $3) }
 113: 
 114: nil: LBRACK RBRACK      { () }
 115: 
 116: boolean:
 117:   | expr EQUAL expr { Equal ($1, $3) }
 118:   | expr LESS expr  { Less ($1, $3) }
 119: 
 120: ty:
 121:     TBOOL                      { TBool }
 122:   | TINT                      { TInt }
 123:   | ty TIMES ty { TTimes ($1, $3) }
 124:   | ty ARROW ty { TArrow ($1, $3) }
 125:   | ty TLIST                 { TList $1 }
 126:   | LPAREN ty RPAREN         { $2 }
 127: 
 128: %%

poly.ml

   1: (** Poly tolevel. *)
   2: 
   3: open Message
   4: open Syntax
   5: 
   6: (**
   7:    The toplevel accepts global value definitions [let x = e] and expressions,
   8:    separated by double semicolons [;;] when contained in a file.
   9:  
  10:    Usage:
  11:  
  12:      [poly] runs the interactive loop
  13:  
  14:      [poly dat1 ... datN] evaluates the contents of files
  15:      [dat1], ..., [datN] then runs the interactive loop.
  16:  
  17:      [poly -n dat1 ..., datN] evaluates the contents of files
  18:      [dat1],...,[datN] and exits.
  19: *)
  20: 
  21: exception Fatal_error of string
  22: 
  23: let fatal_error msg = raise (Fatal_error msg)
  24: 
  25: (** [exec_cmd (ctx, env) n cmd] executes the toplevel command [cmd] in
  26:     the given context [ctx] and environment [env]. It forces
  27:     evaluation of up to [n] nodes of pairs and lists. It returns the
  28:     new context and environment. *)
  29: let rec exec_cmd n (ctx, env) = function
  30:     Expr e ->
  31:       (* type check [e], evaluate, and print result *)
  32:       let ty = rename (Type_infer.type_of ctx e) in
  33:       let v = Interpret.interp env e in
  34:         print_string ("- : " ^ string_of_type ty ^ " = ") ;
  35:         Interpret.print_result n v ;
  36:         print_newline () ;
  37:         (ctx, env)
  38:   | Def (x, e) ->
  39:       (* type check [e], and store it unevaluated! *)
  40:       let ty = rename (Type_infer.type_of ctx e) in
  41:         print_endline ("val " ^ x ^ " : " ^ string_of_type ty) ;
  42:         ((x,ty)::ctx, (x, ref (Interpret.VClosure (env,e)))::env)
  43:   | Quit -> raise End_of_file
  44:   | Use fn -> exec_file n (ctx, env) fn
  45: 
  46: (** [exec_file (ctx, env) n fn] executes the contents of file [fn] in
  47:     the given context [ctx] and environment [env]. It forces
  48:     evaluation of up to [n] levels of nesting of pairs and lists. It
  49:     returns the new context and environment. *)
  50: and exec_file n ce fn =
  51:   let fh = open_in fn in
  52:   let lex = Message.lexer_from_channel fn fh in
  53:     try
  54:       let cmds = Parser.toplevel Lexer.token lex in
  55:         close_in fh ;
  56:         exec_cmds n ce cmds
  57:     with
  58:         Type_infer.Type_error msg -> fatal_error (fn ^ ":\n" ^ msg)
  59:       | Interpret.Runtime_error msg -> fatal_error msg
  60:       | Sys.Break -> fatal_error "Interrupted."
  61:       | Parsing.Parse_error | Failure("lexing: empty token") ->
  62:           fatal_error (Message.syntax_error lex)
  63: 
  64: (** [exec_cmds (ctx, env) n cmds] executes the list of toplevel
  65:     commands [cmd] in the given context [ctx] and environment
  66:     [env]. It forces evaluation of up to [n] levels of nesting of
  67:     pairs and lists. It returns the new context and environment. *)
  68: and exec_cmds n ce cmds =
  69:   List.fold_left (exec_cmd n) ce cmds
  70: ;;
  71: 
  72: (** [shell ctx env] is the interactive shell. Here [ctx] and [env] are
  73:     the context and environment of global definitions. *)
  74: let shell n ctx env =
  75:   print_string ("Poly. Press ") ;
  76:   print_string (match Sys.os_type with
  77:                     "Unix" | "Cygwin" -> "Ctrl-D"
  78:                   | "Win32" -> "Ctrl-Z"
  79:                   | _ -> "EOF") ;
  80:   print_endline " to exit." ;
  81:   let global_ctx = ref ctx in
  82:   let global_env = ref env in
  83:     try
  84:       while true do
  85:         try
  86:           (* read a line, parse it and exectute it *)
  87:           print_string "Poly> ";
  88:           let str = read_line () in
  89:           let lex = Message.lexer_from_string str in
  90:           let cmds =
  91:             try
  92:               Parser.toplevel Lexer.token lex
  93:             with
  94:               | Failure("lexing: empty token")
  95:               | Parsing.Parse_error -> fatal_error (Message.syntax_error lex)
  96:           in
  97:           let (ctx, env) = exec_cmds n (!global_ctx, !global_env) cmds in
  98:             (* set the new values of the global context and environment *)
  99:             global_ctx := ctx ;
 100:             global_env := env
 101:         with
 102:             Fatal_error msg -> Message.report msg
 103:           | Interpret.Runtime_error msg -> Message.report msg
 104:           | Type_infer.Type_error msg -> Message.report msg
 105:           | Sys.Break -> Message.report ("Interrupted.")
 106:       done 
 107:     with
 108:         End_of_file -> print_endline "\nGood bye."
 109: 
 110: (** The main program. *)
 111: let main =
 112:   Sys.catch_break true ;
 113:   let print_depth = ref 100 in
 114:   let noninteractive = ref false in
 115:   let files = ref [] in
 116:     Arg.parse
 117:       [("-n", Arg.Set noninteractive, "do not run the interactive shell");
 118:        ("-p", Arg.Int (fun n -> print_depth := n), "set print depth")]
 119:       (fun f -> files := f :: !files)
 120:       "Usage: poly [-p <int>] [-n] [file] ..." ;
 121:     files := List.rev !files ;
 122:     let ctx, env =
 123:       try
 124:         List.fold_left (exec_file !print_depth) ([],[]) !files
 125:       with
 126:           Fatal_error msg -> Message.report msg ; exit 1
 127:     in    
 128:       if not !noninteractive then shell !print_depth ctx env