Commits

relsa committed 5755cd5

Ex4.4

Comments (0)

Files changed (1)

Interpreter/typing.ml

         get_type_from_key k rest in
 
   match ty with
-  | TyInt -> TyInt
-  | TyBool -> TyBool
-  | TyVar t1 -> get_type_from_key t1 subst
-  | TyFun (t1, t2) -> TyFun (subst_type subst t1, subst_type subst t2)
+  | TyInt ->
+    TyInt
+  | TyBool ->
+    TyBool
+  | TyVar t1 ->
+    get_type_from_key t1 subst
+  | TyFun (t1, t2) ->
+    TyFun (subst_type subst t1, subst_type subst t2)
 ;; 
     
+
+let rec unify (l : (ty * ty) list) : subst = (* Ex4.4 *)
+  let rec rewrite tv t l =
+    match l with
+    | [] ->
+      []
+    | (t1, t2) :: rest ->
+      if t1 = TyVar tv && t2 = TyVar tv then
+        (t, t) :: rewrite tv t rest
+      else if t1 = TyVar tv then
+        (t, t2) :: rewrite tv t rest
+      else if t2 = TyVar tv then
+        (t1, t) :: rewrite tv t rest
+      else
+        (t1, t2) :: rewrite tv t rest in
+  match l with
+  | [] ->
+    []
+  | (t1, t2) :: rest ->
+    if t1 = t2 then
+      unify rest
+    else
+      begin
+        match t1, t2 with
+        | TyVar a, _ ->
+          (a, t2) :: unify (rewrite a t2 rest)
+        | _, TyVar a ->
+          (a, t1) :: unify (rewrite a t1 rest)
+        | TyFun (t11, t12), TyFun (t21, t22) ->
+          unify ((t11, t21) :: (t12, t22) :: rest)
+        | _, _ ->
+          err ("failed unification")
+      end
+;;