test gha

.github/workflows/ci.yml

@@ -8,6 +8,7 @@ on:
   release:
     types:
       - published
+  workflow_dispatch:
 
 jobs:
   build-and-test:

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/eval.ml

@@ -59,7 +59,11 @@ let rec eval ?(debug=false) (env: (tyvar list * value) Environment.t) f =
     let xs, v = Environment.find x env in
     let us = List.map nu_to_fresh us in
     begin match v with
-      | FunV proc -> FunV (fun _ -> proc (xs, us))
+      | FunV proc -> FunV (
+          fun (xs', us') ->
+            let us = List.map (subst_type (Utils.List.zip xs' us')) us in
+            proc (xs, us)
+        )
       | _ -> v
     end
   | IConst (_, i) -> IntV i

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

@@ -240,13 +240,17 @@ module ITGL = struct
   let closure_tyvars1 u1 env v1 =
     TV.elements @@ TV.diff (ftv_ty u1) @@ TV.union (ftv_tyenv env) (ftv_exp v1)
 
-  let closure_tyvars_let_decl e u1 env =
+  let closure_tyvars_let_decl1 e u1 env =
     TV.elements @@ TV.diff (TV.union (tv_exp e) (ftv_ty u1)) (ftv_tyenv env)
 
   let closure_tyvars2 w1 env u1 v1 =
     let ftvs = TV.big_union [ftv_tyenv env; ftv_ty u1; ftv_exp v1] in
     TV.elements @@ TV.diff (Syntax.CC.ftv_exp w1) ftvs
 
+  let closure_tyvars_let_decl2 w1 env u1 v1 =
+    let ftvs = TV.big_union [ftv_tyenv env; ftv_ty u1; tv_exp v1] in
+    TV.elements @@ TV.diff (Syntax.CC.ftv_exp w1) ftvs
+
   let rec is_base_value env u =
     assert (u = TyInt || u = TyBool || u = TyUnit);
     function
@@ -387,12 +391,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 *)
 
@@ -511,12 +513,13 @@ module ITGL = struct
       env, CC.Exp f, u
     | LetDecl (x, e) when is_value env e ->
       let f, u = translate_exp env e in
-      let xs = closure_tyvars_let_decl e u env in
-      let ys = closure_tyvars2 f env u e in
+      let xs = closure_tyvars_let_decl1 e u env in
+      let ys = closure_tyvars_let_decl2 f env u e in
       let env = Environment.add x (TyScheme (xs @ ys, u)) env in
       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