From 983266159441baab240f36d33459bc9327865356 Mon Sep 17 00:00:00 2001 From: Yuki Oshima Date: Fri, 15 Nov 2024 20:41:54 +0900 Subject: [PATCH 1/2] 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/2] 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 _