open Absyn open Env open EoplPrint open List open Format exception TypeError of string exception TODO (* Type schemes, either monomorphic types or polymorphic types. *) type typ_scheme = Mono of typ | Poly of var list * typ (* Type environments map variables to type schemes. *) type tenv = typ_scheme Env.env (* A constraint set *) type constr = (typ * typ) list (* A substitution list *) type subst = (var * typ) list (* print out a constraint set, for debugging. *) let print_constr (c:constr) :unit = print_list c (fun (t1,t2) -> print_string (string_of_typ t1); print_string "="; print_string (string_of_typ t2)) print_comma (* print out a substitution, also for debugging. *) let print_subst (s:subst) : unit = print_list s (fun (x,t) -> print_string (x ^ "->"); print_string (string_of_typ t)) print_comma (* Create a new type (variable) *) let newvar = let ctr = ref 0 in fun () -> ctr := !ctr + 1; VarType ("ty$"^ (string_of_int !ctr)) (* Determine the free variables of a type expression *) let rec free_vars (t:typ) : var list = match t with IntType -> [] | BoolType -> [] | ProcType (ts,t) -> fold_left (fun a b -> rev_append (free_vars b) a) (free_vars t) ts | ListType t -> free_vars t | PairType (t1,t2) -> rev_append (free_vars t1) (free_vars t2) | VarType v -> [v] (* Determine if a variable appears free in a type, constraint set or environment *) let in_typ (v:var) (t:typ) : bool = List.mem v (free_vars t) let in_constr (v:var) (c:constr) : bool = List.exists (fun (t1,t2) -> in_typ v t1 || in_typ v t2) c let rec in_env (v:var) (env:tenv) : bool = match env with Empty -> false | Extend (vs,tarr,env) -> (Array.fold_left (fun b ts -> b || match ts with Mono t -> in_typ v t | Poly (vs,t) -> not (mem v vs) && in_typ v t) false tarr) || (in_env v env) (* Apply the substitution to a type expression *) let rec subst_typ (s:subst) (t:typ) :typ = match t with IntType -> t | BoolType -> t | ProcType (ts,t) -> ProcType (map (subst_typ s) ts, subst_typ s t) | ListType t -> ListType (subst_typ s t) | PairType (t1,t2) -> PairType (subst_typ s t1, subst_typ s t2) | VarType x -> (try List.assoc x s with Not_found -> VarType x) (* Apply the substitution to all types in the constraint *) let subst_constr (s:subst) (c:constr) :constr = map (fun (t1,t2) -> (subst_typ s t1, subst_typ s t2)) c (* convert a substitution into a constraint set *) let subst2constr (s:subst) : constr = map (fun (x,t) -> (VarType x,t)) s (* Create a substitution from a constraint set. * The expression is used to create an error * message showing where the problem occured. *) let rec unify (e:exp) (c:constr) : subst = match c with [] -> [] | (s,t)::c' when s = t -> unify e c' | (VarType x, t)::c' when not (in_typ x t) -> let s = unify e (subst_constr [x, t] c') in (x, subst_typ s t) :: s | (t, VarType x)::c' when not (in_typ x t) -> let s = unify e (subst_constr [x, t] c') in (x, subst_typ s t) :: s | (ProcType (args1,ret1), ProcType (args2,ret2))::c' -> unify e ((ret1,ret2)::rev_append (combine args1 args2) c') | (ListType t1, ListType t2)::c' -> unify e ((t1,t2)::c') | (PairType (s1,s2), PairType(t1,t2))::c' -> unify e ((s1,t1)::(s2,t2)::c') | (s,t)::c' -> print_string "Type error in "; print_exp e; print_string "\n"; raise (TypeError ("Cannot unify " ^ (string_of_typ s) ^ " and " ^ (string_of_typ t))) (* Given a type scheme, produce a type by creating new * unification variables for all of the variables bound * by the type scheme *) let rename (ts:typ_scheme) : typ = match ts with Mono t -> t | Poly (vs,t) -> let subst = map (fun v -> (v, newvar ())) vs in subst_typ subst t (* Determine which free variables of a type do not appear * in the environment or current constraint set. *) let generalize (env:tenv) (c:constr) (t:typ) : var list = filter (fun v -> not (in_env v env) || (not (in_constr v c)) ) (free_vars t) (* Given a typing annotation, if there is no type listed, create a new * type variable and set that annotation to be equal to that variable. *) let get_typ (tyopt:annot) : typ = match !tyopt with Some typ -> typ | None -> let t = newvar () in (tyopt := Some t; t) let is_value (e:exp) : bool = match e with LitInt _ -> true | LitBool _ -> true | Lambda _ -> true | LitNull -> true | _ -> false (* Type check a primitive, given a list of arguments. *) let rec check_prim (p:prim) (args:typ list) : typ * constr = match p,args with Plus, [t1;t2] -> IntType, [(t1,IntType);(t2,IntType)] | Times, [t1;t2] -> IntType, [(t1,IntType);(t2,IntType)] | Minus, [t1;t2] -> IntType, [(t1,IntType);(t2,IntType)] | And, [t1;t2] -> BoolType,[(t1,BoolType);(t2,BoolType)] | Or, [t1;t2] -> BoolType, [(t1,BoolType);(t2,BoolType)] | Not, [t] -> BoolType, [t,BoolType] | Add1, [t] -> IntType, [t,IntType] | Sub1, [t] -> IntType, [t,IntType] | Zero, [t] -> BoolType, [t,IntType] | LT, [t1;t2] -> BoolType,[(t1,IntType);(t2,IntType) ] | GT, [t1;t2] -> BoolType, [(t1,IntType);(t2,IntType)] | Equal, [t1;t2] -> BoolType,[(t1,IntType);(t2,IntType)] | Pair, [t1;t2] -> PairType (t1,t2),[] | Fst, [t] -> let t1 = newvar () in let t2 = newvar () in t1, [t,(PairType(t1,t2))] | Snd, [t] -> let t1 = newvar () in let t2 = newvar () in t2, [t,(PairType(t1,t2))] | Hd, [t] -> let t2 = newvar () in t2, [t,ListType t2] | Tl, [t] -> let t2 = newvar () in ListType t2, [t,ListType t2] | Cons, [t1; t] -> let t2 = newvar () in ListType t2, [t,ListType t2; t1,t2] | IsNull, [t] -> let t2 = newvar () in BoolType, [t,ListType t2] | _, _ -> raise (TypeError "Unimplemented primitive or invalid arguments") (* Extend the type environment for a letrec expression and check that all of the rhs's are well-typed. Returns the new environment and a constraint set for the expression. *) let rec extend_env_letrec (tys:annot list) (proc_names:var list) (arg_typs: annot list list) (idss: var list list) (bodies: exp list) (env: tenv) : tenv * constr = let tys = map get_typ tys in let arg_typs = map (map get_typ) arg_typs in (* Make a new environment containing all of the function names and their types *) let new_env = extend_env proc_names (List.map2 (fun a t -> Mono (ProcType (a,t))) arg_typs tys) env in (* Type check each function. This generates a constraint set. *) let rec loop l :constr = match l with (t::tys,a::arg_typs, i::ids, b::bodies) -> let actual_ret,c = type_exp b (extend_env i (map (fun x -> Mono x) a) new_env) in let c' = loop (tys, arg_typs, ids, bodies) in ((actual_ret,t)::(rev_append c c')) | [],[],[],[] -> [] | _ -> failwith "BUG: parser ensures lists are same length" in let c = loop (tys, arg_typs, idss, bodies) in let s = unify (LitInt 1) c in let poly_env = extend_env proc_names (List.map2 (fun a t -> let t1 = ProcType (a,t) in let t2 = subst_typ s t1 in let vs = generalize env c t2 in Poly (vs,t2)) arg_typs tys) env in poly_env, subst2constr s and type_exp_aux (exp:exp) (env:tenv) : typ * constr = match exp with LitInt i -> IntType, [] | LitBool b -> BoolType, [] | LitNull -> let t1 = newvar () in ListType(t1), [] | Var v -> rename (apply_env env v), [] | Prim (p, rands) -> let args,c1 = type_exp_rands rands env in let ret,c2 = check_prim p args in ret, rev_append c2 c1 | If (test_exp, true_exp, false_exp) -> let test_typ, test_constr = type_exp test_exp env in let true_typ, true_constr = type_exp true_exp env in let false_typ, false_constr = type_exp false_exp env in true_typ, (test_typ, BoolType)::(true_typ, false_typ):: rev_append test_constr (rev_append true_constr false_constr) | Let (vars,rands,body) -> let arg_typs,arg_constr = type_exp_rands rands env in let polys = map2 (fun t rand -> if is_value rand then let vs = generalize env arg_constr t in Poly (vs,t) else Mono t) arg_typs rands in let body_typ,body_constr = type_exp body (extend_env vars polys env) in body_typ, rev_append arg_constr body_constr | Lambda (tyopts,ids,body) -> let tys = map get_typ tyopts in let body_typ, constr = type_exp body (extend_env ids (map (fun t -> Mono t) tys) env) in ProcType (tys, body_typ), constr | App (rator,rands) -> let proc_typ,proc_constr = type_exp rator env in let arg_typs,arg_constr = type_exp_rands rands env in let ret_typ = newvar () in ret_typ, (proc_typ, (ProcType(arg_typs,ret_typ)))::(rev_append proc_constr arg_constr) | Letrec (tys, proc_names, arg_tys, idss, bodies, letrec_body) -> let new_env,constr1 = extend_env_letrec tys proc_names arg_tys idss bodies env in let body_typ,constr2 = type_exp letrec_body new_env in body_typ, (append constr1 constr2) | Varassign (id, rhs) -> let ts = apply_env env id in let t2,constr = type_exp rhs env in (match ts with Poly _ -> raise (TypeError "Cannot assign to polymorphic variables") | Mono t1 -> IntType, (t1,t2)::constr) | Begin(exp, exps) -> let v,constr = type_exp exp env in let rec loop l = match l with [] -> v,[] | [e] -> type_exp e env | (hd :: tl) -> let _, constr1 = type_exp hd env in let typ, constr2 = loop tl in typ, rev_append constr1 constr2 in loop exps and type_exp_rands (rands:exp list) (env:tenv): typ list * constr = match rands with [] -> [], [] | (rand::rands) -> let rt,ct = type_exp rand env in let rts,cts = type_exp_rands rands env in (rt::rts, rev_append ct cts) and type_exp (exp:exp) (env:tenv) : typ * constr = let typ,constr = type_exp_aux exp env in let subst = unify exp constr in subst_typ subst typ, subst2constr subst (* Apply a substitution to a typing annotation, setting that annotation to be the result of the substitution *) let subst_annot (s:subst) (tr:annot) : unit = match (!tr) with Some t -> (tr := Some (subst_typ s t)) | None -> failwith "Should be types everywhere." (* Apply a substitution to an expression, updating all of the typing annotations. *) let rec subst_type_exp (s:subst) (exp:exp) : unit = match exp with LitInt i -> () | LitBool b -> () | LitNull -> () | Var v -> () | Prim (p, rands) -> iter (subst_type_exp s) rands | If (test_exp, true_exp, false_exp) -> begin subst_type_exp s test_exp; subst_type_exp s true_exp; subst_type_exp s false_exp; end | Let (vars,rands,body) -> (iter (subst_type_exp s) rands; subst_type_exp s body) | Lambda (tyopts,ids,body) -> (iter (subst_annot s) tyopts; subst_type_exp s body) | App (rator,rands) -> (subst_type_exp s rator; iter (subst_type_exp s) rands) | Letrec (tys, proc_names, arg_tys, idss, bodies, letrec_body) -> iter (subst_annot s) tys; iter (iter (subst_annot s)) arg_tys; iter (subst_type_exp s) bodies; subst_type_exp s letrec_body | Varassign (id, rhs) -> subst_type_exp s rhs | Begin(exp, exps) -> (subst_type_exp s exp; iter (subst_type_exp s) exps) let type_program (e:exp) : typ = let typ,constr = type_exp e Empty in let s = unify e constr in subst_type_exp s e; typ