typing expression and toplevel

Some notes:
1. All type variables are identifier(Ident.ident) to get readable names
2. Definition `mod_type` is removed to "type cluster" of
3. In check.ml, indexes are synced between typed expression, type and unifier

lib/common/dune

@@ -4,7 +4,7 @@
  (inline_tests)
  (wrapped false)
  (preprocess
-  (pps ppx_sexp_conv ppx_inline_test ppx_jane)))
+  (pps ppx_sexp_conv ppx_deriving.eq ppx_inline_test ppx_jane)))
 
 (env
  (dev

lib/common/ident.ml

@@ -5,11 +5,23 @@ let compare_string = String.compare
 
 let compare_int = Int.compare
 
-type t = int * string [@@deriving compare]
+type ident = int * string [@@deriving sexp, compare]
 
-let sexp_of_t t = S.Atom (Printf.sprintf "%s/%d" (snd t) (fst t))
+type t = ident
 
-let t_of_sexp s =
+let compare (index0, name0) (index1, name1) =
+  let index_cmp = compare_int index0 index1 in
+  if index_cmp <> 0 then index_cmp else compare_string name0 name1
+
+let sexp_of_ident id = S.Atom (Printf.sprintf "%s/%d" (snd id) (fst id))
+
+let name_of_ident (_index, name) = name
+
+let index_of_ident (index, _name) = index
+
+let mk_ident index name = (index, name)
+
+let ident_of_sexp s =
   match s with
   | S.Atom s ->
       let splited = String.split_on_char '/' s in
@@ -29,3 +41,5 @@ let create ~(hint : string) =
 let rename (_, name) = create ~hint:name
 
 let to_string x = Printf.sprintf "%s/%d" (snd x) (fst x)
+
+let refresh () = index := 0

lib/common/ident.mli

@@ -1,11 +1,25 @@
-type t [@@deriving sexp, compare]
+val compare_string : String.t -> String.t -> int
 
-val same : t -> t -> bool
+val compare_int : int -> int -> int
 
-val from : string -> t
+type ident [@@deriving sexp]
 
-val create : hint:string -> t
+type t = ident [@@deriving compare]
 
-val rename : t -> t
+val name_of_ident : ident -> string
 
-val to_string : t -> string
+val index_of_ident : ident -> int
+
+val mk_ident : int -> string -> ident
+
+val same : ident -> ident -> bool
+
+val from : string -> ident
+
+val create : hint:string -> ident
+
+val rename : ident -> ident
+
+val to_string : ident -> string
+
+val refresh : unit -> unit

lib/syntax/dune

@@ -1,6 +1,6 @@
 (library
  (name syntax)
- (libraries sexplib menhirLib)
+ (libraries sexplib menhirLib common)
  (inline_tests)
  (preprocess
   (pps ppx_sexp_conv ppx_inline_test ppx_jane visitors.ppx)))

lib/syntax/parser.mly

@@ -95,7 +95,8 @@ functor_bind:
 
 type_def: 
     | TYPE LPAREN tvs=separated_list(COMMA, TYPEVAR) RPAREN n=IDENT 
-        EQ vs=separated_list(OR, variant) END { TDAdt (n, tvs, vs) }
+        EQ vs=separated_list(OR, variant) END 
+                { TDAdt (n, (List.map (fun x -> Ident.from x) tvs), vs) }
 
 pattern: 
     | n=IDENT { PVar n }

lib/syntax/parsetree.ml

@@ -47,7 +47,13 @@ and type_def =
   | TDAdt of string * type_paras * variant list
   | TDRecord of string * type_paras * (string * type_expr) list
 
-and type_paras = string list
+and type_paras = Ident.ident list
+
+and mod_type =
+  | MTName of string
+  | MTField of path * string
+  | MTSig of type_comp list
+  | MTFunctor of string * mod_type * mod_type
 
 and variant = string * type_expr option
 [@@deriving
@@ -89,7 +95,6 @@ and lambda = para * expr
 and mod_body = top_level list
 
 and mod_expr =
-  | MERoot
   | MEName of string (* M *)
   | MEStruct of mod_body (* struct ... end *)
   | MEFunctor of functor_expr (* functor (M: MT) -> ... *)
@@ -101,12 +106,6 @@ and functor_para = string * mod_type
 
 and functor_expr = functor_para * mod_expr
 
-and mod_type =
-  | MTName of string
-  | MTField of path * string
-  | MTSig of type_comp list
-  | MTFunctor of string * mod_type * mod_type
-
 and adt_def = string * type_paras * variant list
 [@@deriving
   sexp,

lib/test/dune

@@ -1,6 +1,6 @@
 (library
  (name test)
- (libraries sexplib syntax back typing)
+ (libraries sexplib syntax back typing common)
  (inline_tests)
  (wrapped false)
  (preprocess

lib/test/typing_test.ml

@@ -2,14 +2,200 @@ open Syntax.Parsing
 open Typing
 module T = Typedtree
 
+[@@@warning "-26"]
+
 let print_sexp s =
-  Sexplib.Sexp.to_string_hum ?indent:(Some 2) s |> print_string
+  Printf.printf "%s\n" (Sexplib.Sexp.to_string_hum ?indent:(Some 2) s)
 
 let%expect_test "Test: expression typing" =
   let print_typed str =
+    Ident.refresh ();
     let e = parse_string_expr str in
-    let typed, _ = Typing.Check.type_check e Typing.Env.empty in
+    let typed, _ = Typing.Check.tc_expr e Typing.Env.empty 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
+    typed |> T.get_ty |> Syntax.Parsetree.sexp_of_type_expr |> print_sexp
+  in
   print_typed "1";
-  [%expect {| (EConst (CInt 1) (TCons int ())) |}]
+  [%expect {| (EConst (CInt 1) (TCons int ())) |}];
+
+  print_type "1";
+  [%expect {| (TCons int ()) |}];
+
+  print_typed "let x = 1 in x";
+  [%expect
+    {|
+    (ELet x (EConst (CInt 1) (TCons int ())) (EVar x (TCons int ()))
+      (TCons int ())) |}];
+
+  print_type "let x = 1 in x";
+  [%expect {| (TCons int ()) |}];
+
+  print_typed "let f = (fun x -> x) in f";
+  [%expect
+    {|
+    (ELet f (ELam (x (EVar x (TVar '_t/1)) (TArrow (TVar '_t/1) (TVar '_t/1))))
+      (EVar f (TArrow (TVar '_t/2) (TVar '_t/2)))
+      (TArrow (TVar '_t/2) (TVar '_t/2))) |}];
+
+  print_typed "let f = (fun x -> x) in f 1";
+  [%expect
+    {|
+    (ELet f (ELam (x (EVar x (TVar '_t/1)) (TArrow (TVar '_t/1) (TVar '_t/1))))
+      (EApp (EVar f (TArrow (TCons int ()) (TCons int ())))
+        (EConst (CInt 1) (TCons int ())) (TCons int ()))
+      (TCons int ()))
+     |}];
+
+  print_type "let f = (fun x -> x) in f 1";
+  [%expect {|
+    (TCons int ()) |}];
+
+  print_typed "1, true";
+  [%expect
+    {|
+    (ETuple
+      ((EConst (CBool true) (TCons bool ())) (EConst (CInt 1) (TCons int ())))
+      (TTuple ((TCons bool ()) (TCons int ())))) |}];
+
+  print_typed "let f = (fun x -> x) in (f 1, f true)";
+  [%expect
+    {|
+    (ELet f (ELam (x (EVar x (TVar '_t/1)) (TArrow (TVar '_t/1) (TVar '_t/1))))
+      (ETuple
+        ((EApp (EVar f (TArrow (TCons bool ()) (TCons bool ())))
+           (EConst (CBool true) (TCons bool ())) (TCons bool ()))
+          (EApp (EVar f (TArrow (TCons int ()) (TCons int ())))
+            (EConst (CInt 1) (TCons int ())) (TCons int ())))
+        (TTuple ((TCons bool ()) (TCons int ()))))
+      (TTuple ((TCons bool ()) (TCons int ())))) |}];
+  print_typed
+    {|
+     let rec f = fun x -> g x
+     and 
+     g = fun x -> f x
+     in
+     1
+     |};
+  [%expect
+    {|
+    (ELetrec
+      ((f
+         (x
+           (EApp (EVar g (TArrow (TVar '_t/5) (TVar ret/6)))
+             (EVar x (TVar '_t/5)) (TVar ret/6))
+           (TArrow (TVar '_t/5) (TVar ret/6))))
+        (g
+          (x
+            (EApp (EVar f (TArrow (TVar '_t/5) (TVar ret/6)))
+              (EVar x (TVar '_t/5)) (TVar ret/6))
+            (TArrow (TVar '_t/5) (TVar ret/6)))))
+      (EConst (CInt 1) (TCons int ())) (TCons int ())) |}];
+
+  print_typed
+    {|
+     let rec f = fun x -> x
+     and 
+     g = fun x -> f 1
+     in
+     1
+     |};
+  [%expect
+    {|
+    (ELetrec
+      ((f (x (EVar x (TCons int ())) (TArrow (TCons int ()) (TCons int ()))))
+        (g
+          (x
+            (EApp (EVar f (TArrow (TCons int ()) (TCons int ())))
+              (EConst (CInt 1) (TCons int ())) (TCons int ()))
+            (TArrow (TVar '_t/4) (TCons int ())))))
+      (EConst (CInt 1) (TCons int ())) (TCons int ())) |}]
+(* todo: test pattern matching *)
+
+let%expect_test "Test: program toplevel typing" =
+  let print_typed str =
+    Ident.refresh ();
+    let prog = parse_string_program str in
+    let typed, _u, _env = Typing.Check.tc_program prog Typing.Env.empty in
+    typed |> T.sexp_of_program |> print_sexp
+  in
+  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
+    Printf.printf "%s\n" (Env.dbg env)
+  in
+  print_typed {|
+     let x = 1
+     |};
+  [%expect
+    {| ((TopLet x (EConst (CInt 1) (TCons int ())) (TCons int ()))) |}];
+  print_typed
+    {|
+     let rec f = fun x -> x
+     and 
+     g = fun x -> f 1
+     |};
+  [%expect
+    {|
+    ((TopLetRec
+       ((f (x (EVar x (TCons int ())) (TArrow (TCons int ()) (TCons int ()))))
+         (g
+           (x
+             (EApp (EVar f (TArrow (TCons int ()) (TCons int ())))
+               (EConst (CInt 1) (TCons int ())) (TCons int ()))
+             (TArrow (TVar '_t/4) (TCons int ()))))))) |}];
+  print_effect
+    {|
+     type () a 
+     = Cons of int
+     | Nil 
+     end
+     |};
+  [%expect {|
+    ------------------Envirment Debug Info Begin------------------------
+    Value Bindings:
+      Cons |-> forall  . (TArrow (TCons int ()) (TCons a ()));
+      Nil |-> forall  . (TCons a ())
+    Type Definitions:
+      a |-> (TDAdt a () ((Cons ((TCons int ()))) (Nil ())))
+    ------------------Envirment Debug Info End-------------------------- |}];
+  print_typed
+    {|
+     type () int_l 
+     = Cons of int
+     | Nil 
+     end
+     let c = Nil
+     let co = Cons 1
+     |};
+  [%expect {|
+    ((TopTypeDef (TDAdt int_l () ((Cons ((TCons int ()))) (Nil ()))))
+      (TopLet c (ECons Nil (TCons int_l ())) (TCons int_l ()))
+      (TopLet co
+        (EApp (ECons Cons (TArrow (TCons int ()) (TCons int_l ())))
+          (EConst (CInt 1) (TCons int ())) (TCons int_l ()))
+        (TCons int_l ()))) |}];
+  print_effect
+    {|
+     type () int_l 
+     = Cons of int
+     | Nil 
+     end
+     let c = Nil
+     let co = Cons 1
+     |};
+  [%expect {|
+    ------------------Envirment Debug Info Begin------------------------
+    Value Bindings:
+      co |-> forall  . (TCons int_l ());
+      c |-> forall  . (TCons int_l ());
+      Cons |-> forall  . (TArrow (TCons int ()) (TCons int_l ()));
+      Nil |-> forall  . (TCons int_l ())
+    Type Definitions:
+      int_l |-> (TDAdt int_l () ((Cons ((TCons int ()))) (Nil ())))
+    ------------------Envirment Debug Info End-------------------------- |}]