open Absyn open Env open EoplPrint exception TypeError of string exception TODO type tenv = typ Env.env let rec check_equal (tenv:tenv) (t1:typ)(t2:typ) : unit = if (t1 = t2) then () else raise (TypeError ((string_of_typ t1) ^ " does not equal " ^ (string_of_typ t2))) (* Apply the function f to all pairs of elements in f1 f2 and return true if all results are true *) let all2 f l1 l2 : bool = List.fold_left2 (fun x y z -> x && f y z) true l1 l2 (* Type check a primitive, given a list of arguments. *) let rec check_prim (p:prim) (args:typ list) : typ = match p,args with Plus, [IntType;IntType] -> IntType | Times, [IntType;IntType] -> IntType | Minus, [IntType;IntType] -> IntType | And, [BoolType; BoolType] -> BoolType | Or, [BoolType; BoolType] -> BoolType | Not, [BoolType] -> BoolType | Add1, [IntType] -> IntType | Sub1, [IntType] -> IntType | Zero, [IntType] -> BoolType | LT, [IntType; IntType] -> BoolType | GT, [IntType; IntType] -> BoolType | Equal, [IntType;IntType] -> BoolType (* For II.2 *) | Pair, [t1;t2] -> PairType (t1,t2) | Fst, [PairType (t1,t2)] -> t1 | Snd, [PairType (t1,t2)] -> t2 (* For II.3 *) | Hd, [ListType t2] -> t2 | Tl, [ListType t2] -> ListType t2 | Cons, [t1; ListType t2] when t1 = t2 -> ListType t2 | IsNull, [ListType v] -> BoolType | _, _ -> 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. *) let rec extend_env_letrec (tys:typ list) (proc_names:var list) (arg_typs: typ list list) (idss: var list list) (bodies: exp list) (env: tenv) : tenv = (* 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 -> ProcType (a,t)) arg_typs tys) env in (* Type check each function. This is a side-effect operation only. *) let rec loop l = match l with (t::tys,a::arg_typs, i::ids, b::bodies) -> let actual_ret = type_exp b (extend_env i a new_env) in check_equal env actual_ret t; loop (tys, arg_typs, ids, bodies) | [],[],[],[] -> () | _ -> failwith "BUG: parser ensures lists are same length" in loop (tys, arg_typs, idss, bodies); new_env and type_exp (exp:exp) (env:tenv) : typ = match exp with LitInt i -> IntType | LitBool b -> BoolType | LitNull t -> (match t with ListType (t1) -> t | _ -> raise (TypeError ("Null must be a list type"))) | Var v -> apply_env env v | Prim (p, rands) -> let args = type_exp_rands rands env in check_prim p args | If (test_exp, true_exp, false_exp) -> begin check_equal env BoolType (type_exp test_exp env); let t1 = (type_exp true_exp env) in check_equal env t1 (type_exp false_exp env); t1 end | Let (vars,rands,body) -> let args = type_exp_rands rands env in type_exp body (extend_env vars args env) | Lambda (tys,ids,body) -> ProcType (tys, type_exp body (extend_env ids tys env)) | App (rator,rands) -> let proc = type_exp rator env in let args = type_exp_rands rands env in (match proc with ProcType (arg_typs, ret) -> (try if all2 (fun t1 t2 -> check_equal env t1 t2; true) args arg_typs then ret else raise (TypeError "Invalid argument to function") with Invalid_argument _ -> raise (TypeError "Wrong number of args to function")) | _ -> raise (TypeError "Attempt to apply non-function")) | Letrec (tys, proc_names, arg_tys, idss, bodies, letrec_body) -> type_exp letrec_body (extend_env_letrec tys proc_names arg_tys idss bodies env) | Varassign (id, rhs) -> let t1 = apply_env env id in let t2 = type_exp rhs env in (check_equal env t1 t2; IntType) | Begin(exp, exps) -> let v = type_exp exp env in let rec loop l = match l with [] -> v | [e] -> type_exp e env | (hd :: tl) -> ignore (type_exp hd env) ; loop tl in loop exps and type_exp_rands (rands:exp list) (env:tenv): typ list = List.map (fun x -> type_exp x env) rands let type_program (e:exp) : typ = type_exp e Empty