From 2c5f1f0e2b893e7020d5670b2587489927f48225 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 22:38:05 +0100 Subject: [PATCH 1/4] Bugfix in printer --- src/stages/5-ast_typed/PP_generic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stages/5-ast_typed/PP_generic.ml b/src/stages/5-ast_typed/PP_generic.ml index 1e503ace6..c29a31b30 100644 --- a/src/stages/5-ast_typed/PP_generic.ml +++ b/src/stages/5-ast_typed/PP_generic.ml @@ -89,7 +89,7 @@ module M = struct option = (fun _visitor continue NoState o -> match o with | None -> fprintf ppf "None" - | Some v -> fprintf ppf "%a" (fun _ppf -> continue NoState) v) ; + | Some v -> fprintf ppf "Some %a" (fun _ppf -> continue NoState) v) ; poly_unionfind = (fun _visitor continue NoState p -> let lst = (UnionFind.Poly2.partitions p) in let aux1 l = fprintf ppf "[@,@[ (*%a*) %a @]@,]" From 424a0b0ba748cc859cef8bfff06d6267081f7510 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 3 Jun 2020 01:31:33 +0100 Subject: [PATCH 2/4] Bugfix: equality --- src/stages/typesystem/misc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 389f93e89..070a502ff 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -230,7 +230,7 @@ module Substitution = struct | P_forall p -> ( let aux c = constraint_ ~c ~substs in let constraints = List.map aux p.constraints in - if (p.binder = v) then ( + if (Var.equal p.binder v) then ( { tsrc = "?TODO3?" ; t = P_forall { p with constraints } } ) else ( let body = self p.body in From 19f02a4b36329efe758fa85483296e5a00f8023e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 23:27:00 +0100 Subject: [PATCH 3/4] bugfix: forgot to explicitly discard new typer state --- src/test/test_helpers.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index 12ea7cc9c..9ed64a53c 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -99,7 +99,8 @@ let typed_program_with_imperative_input_to_michelson let%bind sugar = Compile.Of_imperative.compile_expression input in let%bind core = Compile.Of_sugar.compile_expression sugar in let%bind app = Compile.Of_core.apply entry_point core in - let%bind (typed_app,_) = Compile.Of_core.compile_expression ~env ~state app in + let%bind (typed_app,new_state) = Compile.Of_core.compile_expression ~env ~state app in + let () = Typer.Solver.discard_state new_state in let%bind compiled_applied = Compile.Of_typed.compile_expression typed_app in let%bind mini_c_prg = Compile.Of_typed.compile program in Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied From 64c6b8896d063b5375397806ad3d1e5f8c3e5a71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 3 Jun 2020 12:54:40 +0100 Subject: [PATCH 4/4] comment --- src/stages/typesystem/misc.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 070a502ff..da0bcdd50 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -231,8 +231,14 @@ module Substitution = struct let aux c = constraint_ ~c ~substs in let constraints = List.map aux p.constraints in if (Var.equal p.binder v) then ( + (* The variable v is shadowed by the forall's binder, so + we don't substitute inside the body. This should be + handled in a more elegant manner once we have a proper + environment and scopes. *) { tsrc = "?TODO3?" ; t = P_forall { p with constraints } } ) else ( + (* The variable v is still visible within the forall, so + substitute also within the body *) let body = self p.body in { tsrc = "?TODO4?" ; t = P_forall { p with constraints ; body } } )