add a index to indicate current typing module

butterunderflow · May 18, 2024 · c50862b · c50862b
1 parent 27722ae
commit c50862b
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 11 deletions.
diff --git a/lib/test/typing_test.ml b/lib/test/typing_test.ml
@@ -11,13 +11,13 @@ let%expect_test "Test: expression typing" =
   let print_typed str =
     Ident.refresh ();
     let e = parse_string_expr str in
-    let typed, _ = Typing.Check.tc_expr e Typing.Env.empty in
+    let typed, _ = Typing.Check.tc_expr e Typing.Env.init in
     typed |> T.sexp_of_expr |> print_sexp
   in
   let print_type str =
     Ident.refresh ();
     let e = parse_string_expr str in
-    let typed, _ = Typing.Check.tc_expr e Typing.Env.empty in
+    let typed, _ = Typing.Check.tc_expr e Typing.Env.init in
     typed |> T.get_ty |> Syntax.Parsetree.sexp_of_type_expr |> print_sexp
   in
   print_typed "1";
@@ -121,7 +121,7 @@ let%expect_test "Test: program toplevel typing" =
     Ident.refresh ();
     let prog = parse_string_program str in
     try
-      let typed, _u, _env = Typing.Check.tc_program prog Typing.Env.empty in
+      let typed, _u, _env = Typing.Check.tc_program prog Typing.Env.init in
       typed |> T.sexp_of_program |> print_sexp
     with
     | Unify.UnificationError (t0, t1) ->
@@ -130,7 +130,7 @@ let%expect_test "Test: program toplevel typing" =
   let print_effect str =
     Ident.refresh ();
     let prog = parse_string_program str in
-    let _typed, _u, env = Typing.Check.tc_program prog Typing.Env.empty in
+    let _typed, _u, env = Typing.Check.tc_program prog Typing.Env.init in
     Printf.printf "%s\n" (Env.dbg env)
   in
   print_typed {|
@@ -168,6 +168,8 @@ let%expect_test "Test: program toplevel typing" =
       Nil |-> forall  . (TCons a ())
     Type Definitions:
       a |-> (TDAdt a () ((Cons ((TCons int ()))) (Nil ())))
+    Current Module Index:
+      0
     ------------------Envirment Debug Info End-------------------------- |}];
   print_typed
     {|
@@ -205,6 +207,8 @@ let%expect_test "Test: program toplevel typing" =
       Nil |-> forall  . (TCons int_l ())
     Type Definitions:
       int_l |-> (TDAdt int_l () ((Cons ((TCons int ()))) (Nil ())))
+    Current Module Index:
+      0
     ------------------Envirment Debug Info End-------------------------- |}];
   print_typed
     {|
@@ -274,6 +278,8 @@ let%expect_test "Test: program toplevel typing" =
     Type Definitions:
       int_l |-> (TDAdt int_l ('a/0 'b/0)
       ((Cons ((TTuple ((TVar 'a/0) (TVar 'b/0))))) (Nil ())))
+    Current Module Index:
+      0
     ------------------Envirment Debug Info End-------------------------- |}]
 
 
@@ -283,7 +289,7 @@ let%expect_test "Test: type check pattern" =
     Ident.refresh ();
     let prog = parse_string_program str in
     try
-      let typed, _u, _env = Typing.Check.tc_program prog Typing.Env.empty in
+      let typed, _u, _env = Typing.Check.tc_program prog Typing.Env.init in
       typed |> T.sexp_of_program |> print_sexp
     with
     | Unify.UnificationError (t0, t1) ->

diff --git a/lib/typing/env.ml b/lib/typing/env.ml
@@ -4,6 +4,7 @@ type t = {
   values : (string * bind_ty) list;
   types : ty_def list;
   modules : (string * mod_ty) list;
+  curr : int
 }
 
 let add_value x ty env = { env with values = (x, ty) :: env.values }
@@ -24,7 +25,7 @@ let get_type_def tn env =
           x = tn)
     env.types
 
-let empty = { values = []; types = []; modules = [] }
+let init = { values = []; types = []; modules = [] ; curr = 0}
 
 let dbg env =
   let values =
@@ -58,6 +59,8 @@ Value Bindings:
   %s
 Type Definitions:
   %s
+Current Module Index:
+  %d 
 ------------------Envirment Debug Info End--------------------------
 |}
-values ty_defs
+values ty_defs env.curr
diff --git a/lib/typing/unify.ml b/lib/typing/unify.ml
@@ -73,10 +73,9 @@ let apply_lst (u : t) lst : ty list = List.map (apply u) lst
 
 let apply_env (u : t) (env : Env.t) : Env.t =
   {
+    env with
     values = List.map (fun (x, (qvs, te)) -> (x, (qvs, u <$> te))) env.values;
     (* types and modules have no space for inference *)
-    types = env.types;
-    modules = env.modules;
   }
 
 exception UnificationError of (string * string)
@@ -114,8 +113,7 @@ let rec unify (t0 : ty) (t1 : ty) : t =
         unify_lst tes0 tes1
     | TArrow (op0, arg0), TArrow (op1, arg1) ->
         unify_lst [ op0; arg0 ] [ op1; arg1 ]
-    | TTuple tes0, TTuple tes1 ->
-       unify_lst tes0 tes1
+    | TTuple tes0, TTuple tes1 -> unify_lst tes0 tes1
     (* by default raise an exception *)
     | _ ->
         let t0_str =