Merge pull request #42 from SoftwareFoundationGroupAtKyotoU/ldti_orig…

…inal

tyenv_bug

bin/main.ml

@@ -19,7 +19,7 @@ let rec read_eval_print lexbuf env tyenv =
 
       (* Type inference *)
       print_debug "***** Typing *****\n";
-      let tyenv, e, u = Typing.ITGL.type_of_program tyenv e in
+      let e, u = Typing.ITGL.type_of_program tyenv e in
       print_debug "e: %a\n" Pp.ITGL.pp_program e;
       print_debug "U: %a\n" Pp.pp_ty u;
 
@@ -29,7 +29,7 @@ let rec read_eval_print lexbuf env tyenv =
 
       (* Translation *)
       print_debug "***** Cast-insertion *****\n";
-      let tyenv, f, u' = Typing.ITGL.translate tyenv e in
+      let new_tyenv, f, u' = Typing.ITGL.translate tyenv e in
       print_debug "f: %a\n" Pp.CC.pp_program f;
       print_debug "U: %a\n" Pp.pp_ty u';
       assert (Typing.is_equal u u');
@@ -43,7 +43,7 @@ let rec read_eval_print lexbuf env tyenv =
         pp_print_string x
         Pp.pp_ty2 u
         Pp.CC.pp_value v;
-      read_eval_print lexbuf env tyenv
+      read_eval_print lexbuf env new_tyenv
     with
     | Failure message ->
       print "Failure: %s\n" message;

lib/stdlib.ml

@@ -67,12 +67,12 @@ let env, tyenv =
  List.fold_left
     (fun (env, tyenv) str ->
       let e = Parser.toplevel Lexer.main @@ Lexing.from_string str in
-      let tyenv, e, u = Typing.ITGL.type_of_program tyenv e in
+      let e, u = Typing.ITGL.type_of_program tyenv e in
       let tyenv, e, _ = Typing.ITGL.normalize tyenv e u in
-      let tyenv, f, _ = Typing.ITGL.translate tyenv e in
+      let new_tyenv, f, _ = Typing.ITGL.translate tyenv e in
       let _ = Typing.CC.type_of_program tyenv f in
       let env, _, _ = Eval.eval_program env f in
-      env, tyenv)
+      env, new_tyenv)
     (env, tyenv)
     implementations
 

lib/syntax.ml

@@ -169,6 +169,7 @@ module CC = struct
     | LetExp (r, _, _, _, _) -> r
 
   let rec is_value = function
+    | Var _
     | IConst _
     | BConst _
     | UConst _

lib/typing.ml

@@ -387,12 +387,10 @@ module ITGL = struct
 
   let type_of_program env = function
     | Exp e ->
-      env, Exp e, type_of_exp env e
+      Exp e, type_of_exp env e
     | LetDecl (x, e) ->
       let u = type_of_exp env e in
-      let xs = if is_value env e then closure_tyvars_let_decl e u env else [] in
-      let env = Environment.add x (TyScheme (xs, u)) env in
-      env, LetDecl (x, e), u
+      LetDecl (x, e), u
 
   (* Normalize type variables *)
 
@@ -517,6 +515,7 @@ module ITGL = struct
       env, CC.LetDecl (x, xs @ ys, f), u
     | LetDecl (x, e) ->
       let f, u = translate_exp env e in
+      let env = Environment.add x (tysc_of_ty u) env in
       env, CC.LetDecl (x, [], f), u
 end
 

lib/typing.mli

@@ -19,7 +19,7 @@ val tyarg_to_ty : Syntax.CC.tyarg -> ty
 module ITGL : sig
   open Syntax.ITGL
 
-  val type_of_program : tysc Environment.t -> program -> (tysc Environment.t * program * ty)
+  val type_of_program : tysc Environment.t -> program -> (program * ty)
 
   val normalize : tysc Environment.t -> program -> ty -> (tysc Environment.t * program * ty)
   val normalize_type : ty -> ty

test/test_examples.ml

@@ -156,6 +156,12 @@ let test_cases = [
     "let dyn x = ((fun (y: 'b) -> y): ? -> ?) x", "'a -> ?", "<fun>";
     "f (dyn 2) (dyn true)", "int", "0";
   ];
+  [
+    "let f = fun x -> x", "'a -> 'a", "<fun>";
+    "let f = fun x -> x f", "(('a -> 'a) -> 'b) -> 'b", "<fun>";
+    "f (fun x -> x) 4", "int", "4";
+    "f", "(('a -> 'a) -> 'b) -> 'b", "<fun>";
+  ];
   (* let-poly & recursion *)
   ["let rec fact n = if n <= 1 then 1 else n * fact (n - 1) in fact 5", "int", "120"];
   ["let rec fact (n:?) = if n <= 1 then 1 else n * fact (n - 1) in fact 5", "int", "120"];
@@ -176,15 +182,15 @@ let id x = x
 let run env tyenv program =
   let parse str = Parser.toplevel Lexer.main @@ Lexing.from_string str in
   let e = parse @@ program ^ ";;" in
-  let tyenv, e, u = Typing.ITGL.type_of_program tyenv e in
+  let e, u = Typing.ITGL.type_of_program tyenv e in
   let tyenv, e, u = Typing.ITGL.normalize tyenv e u in
-  let tyenv, f, u' = Typing.ITGL.translate tyenv e in
+  let new_tyenv, f, u' = Typing.ITGL.translate tyenv e in
   assert (Typing.is_equal u u');
   let u'' = Typing.CC.type_of_program tyenv f in
   assert (Typing.is_equal u u'');
   try
     let env, _, v = Eval.eval_program env f in
-    env, tyenv, asprintf "%a" Pp.pp_ty2 u, asprintf "%a" Pp.CC.pp_value v
+    env, new_tyenv, asprintf "%a" Pp.pp_ty2 u, asprintf "%a" Pp.CC.pp_value v
   with
   | Eval.Blame (_, CC.Pos) -> env, tyenv, asprintf "%a" Pp.pp_ty2 u, "blame+"
   | Eval.Blame (_, CC.Neg) -> env, tyenv, asprintf "%a" Pp.pp_ty2 u, "blame-"

test/test_typing.ml

@@ -19,7 +19,7 @@ module ITGL = struct
     let test (program, expected) =
       program >:: fun ctxt ->
         let e = parse @@ program ^ ";;" in
-        let _, _, u = Typing.ITGL.type_of_program tyenv e in
+        let _, u = Typing.ITGL.type_of_program tyenv e in
         let u = Typing.ITGL.normalize_type u in
         assert_equal ~ctxt:ctxt ~printer:id expected @@ asprintf "%a" Pp.pp_ty2 u
     in