From 983266159441baab240f36d33459bc9327865356 Mon Sep 17 00:00:00 2001 From: Yuki Oshima Date: Fri, 15 Nov 2024 20:41:54 +0900 Subject: [PATCH 1/5] tyenv_bug fixed --- bin/main.ml | 6 +++--- lib/stdlib.ml | 6 +++--- lib/typing.ml | 7 +++---- lib/typing.mli | 2 +- test/test_examples.ml | 12 +++++++++--- test/test_typing.ml | 2 +- 6 files changed, 20 insertions(+), 15 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index e6c9939..95f4320 100644 --- a/bin/main.ml +++ b/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; diff --git a/lib/stdlib.ml b/lib/stdlib.ml index 57b5f49..0a18fd7 100644 --- a/lib/stdlib.ml +++ b/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 diff --git a/lib/typing.ml b/lib/typing.ml index 8c8aa54..b3e3709 100644 --- a/lib/typing.ml +++ b/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 diff --git a/lib/typing.mli b/lib/typing.mli index 4fb3a65..89b9c05 100644 --- a/lib/typing.mli +++ b/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 diff --git a/test/test_examples.ml b/test/test_examples.ml index a199313..ec13368 100644 --- a/test/test_examples.ml +++ b/test/test_examples.ml @@ -156,6 +156,12 @@ let test_cases = [ "let dyn x = ((fun (y: 'b) -> y): ? -> ?) x", "'a -> ?", ""; "f (dyn 2) (dyn true)", "int", "0"; ]; + [ + "let f = fun x -> x", "'a -> 'a", ""; + "let f = fun x -> x f", "(('a -> 'a) -> 'b) -> 'b", ""; + "f (fun x -> x) 4", "int", "4"; + "f", "(('a -> 'a) -> 'b) -> 'b", ""; + ]; (* 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-" diff --git a/test/test_typing.ml b/test/test_typing.ml index e99d104..eb4d301 100644 --- a/test/test_typing.ml +++ b/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 From e0bee77771a693addf85954b9ac8bb9ce9ebe41d Mon Sep 17 00:00:00 2001 From: Yuki Oshima Date: Mon, 18 Nov 2024 12:52:22 +0900 Subject: [PATCH 2/5] is_value bug fixed --- lib/syntax.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/syntax.ml b/lib/syntax.ml index 4b459cd..e2a3c4d 100644 --- a/lib/syntax.ml +++ b/lib/syntax.ml @@ -169,6 +169,7 @@ module CC = struct | LetExp (r, _, _, _, _) -> r let rec is_value = function + | Var _ | IConst _ | BConst _ | UConst _ From 23d40e40cf1a4bb3ba624dd353617256470101d2 Mon Sep 17 00:00:00 2001 From: Yuki Oshima Date: Sat, 30 Nov 2024 15:03:38 +0900 Subject: [PATCH 3/5] eval_Var_bug fixed --- lib/eval.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/lib/eval.ml b/lib/eval.ml index 6ab129b..3f58701 100644 --- a/lib/eval.ml +++ b/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 From d74f665bdc37812b049043657d5e70f66dad7d92 Mon Sep 17 00:00:00 2001 From: oshimayuki1124 Date: Fri, 30 May 2025 15:14:09 +0900 Subject: [PATCH 4/5] modify closure_tyvar --- lib/typing.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/lib/typing.ml b/lib/typing.ml index b3e3709..91c1b15 100644 --- a/lib/typing.ml +++ b/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 @@ -509,8 +513,8 @@ 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) -> From afb755ec1f439d1152b740d26cd7310e99715e5f Mon Sep 17 00:00:00 2001 From: oshimayuki1124 Date: Fri, 30 May 2025 16:48:47 +0900 Subject: [PATCH 5/5] ci: Add workflow_dispatch --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92cdaf2..54eabac 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,6 +8,7 @@ on: release: types: - published + workflow_dispatch: jobs: build-and-test: