(* TODO: Write a good set of tests for infer. *)
let infer_tests = [
(* An example test case.
Note that you are *only* required to write tests for Rec, Fn, and Apply!
Copyright By PowCoder代写 加微信 powcoder
(([(“x”, Int)], Var “x”), Int)
(* TODO: Implement the missing cases of infer. *)
let rec infer ctx e =
match e with
| Var x ->
try lookup x ctx
with Not_found -> raise (TypeError (Free_variable x))
| I _ -> Int
| B _ -> Bool
| Primop (po, exps) ->
let (domain, range) = primopType po in
check ctx exps domain range
| If (e, e1, e2) ->
match infer ctx e with
let t1 = infer ctx e1 in
let t2 = infer ctx e2 in
if t1 = t2 then t1
else type_mismatch t1 t2
| t -> type_mismatch Bool t
| Let (x, e1, e2) ->
let t1 = infer ctx e1 in
infer (extend ctx (x, t1)) e2
| Rec (f, t, e) -> raise NotImplemented
| Fn (xs, e) -> raise NotImplemented
| Apply (e, es) -> raise NotImplemented
and check ctx exps tps result =
match exps, tps with
| [], [] -> result
| e :: es, t :: ts ->
let t’ = infer ctx e in
if t = t’ then check ctx es ts result
else type_mismatch t t’
| _ -> raise (TypeError Arity_mismatch)
(* TODO: Implement type unification. *)
let unify : utp -> utp -> utp UTVarMap.t =
let rec unify (substitution : utp UTVarMap.t) (t1 : utp) (t2 : utp) : utp UTVarMap.t =
match t1, t2 with
(* Unifying identical concrete types does nothing *)
| UInt, UInt
| UBool, UBool -> substitution
| UTVar a, UTVar a’ when a = a’ -> substitution
(* For type constructors, recursively unify the parts *)
| UArrow (t1, t1′), UArrow (t2, t2′) ->
raise NotImplemented
| UTVar a, _ -> unifyVar substitution a t2
| _, UTVar b -> unifyVar substitution b t1
(* All other cases are mismatched types. *)
| _, _ -> unif_error @@ UnifMismatch (t1, t2)
(* Unify a variable with a type *)
and unifyVar (substitution : utp UTVarMap.t) (a : string) (t : utp) : utp UTVarMap.t =
let rec occurs : utp -> bool = function
| UInt | UBool -> false
| UArrow (t1, t2) -> occurs t1 || occurs t2
| UTVar b ->
match UTVarMap.find_opt b substitution with
| None -> false
| Some t’ -> occurs t’
raise NotImplemented
in fun t1 t2 -> unify UTVarMap.empty t1 t2
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com