From 829fa975c78b598607183e828531fcbfecd0959d Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 8 Feb 2024 11:04:34 -0500 Subject: [PATCH 1/7] Fix fixpoint semantics --- src/haz3lcore/dynamics/Stepper.re | 5 +++-- src/haz3lcore/dynamics/Transition.re | 14 ++++++++------ src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 1 + 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 0f481a341e..4b185e13a1 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -419,8 +419,9 @@ let get_justification: step_kind => string = | VarLookup => "variable lookup" | CastAp | Cast => "cast calculus" - | CompleteFilter => "unidentified step" - | CompleteClosure => "unidentified step" + | FixClosure + | CompleteFilter + | CompleteClosure | FunClosure => "unidentified step" | Skip => "skipped steps"; diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index dfe896ca06..a401d4a4ae 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -52,6 +52,7 @@ type step_kind = | LetBind | FunClosure | FixUnwrap + | FixClosure | UpdateTest | FunAp | CastAp @@ -222,15 +223,15 @@ module Transition = (EV: EV_MODE) => { kind: FunClosure, value: true, }); + | FixF(f, _, Closure(env, d1)) => + let. _ = otherwise(env, d); + let env' = evaluate_extend_env(Environment.singleton((f, d)), env); + Step({apply: () => Closure(env', d1), kind: FixUnwrap, value: false}); | FixF(f, t, d1) => let. _ = otherwise(env, FixF(f, t, d1)); Step({ - apply: () => - Closure( - evaluate_extend_env(Environment.singleton((f, d1)), env), - d1, - ), - kind: FixUnwrap, + apply: () => FixF(f, t, Closure(env, d1)), + kind: FixClosure, value: false, }); | Test(id, d) => @@ -668,6 +669,7 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) => | CaseNext | CompleteClosure | CompleteFilter + | FixClosure | FixUnwrap | BuiltinWrap | FunClosure => true; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 310ce39e2c..9722d9138b 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -141,6 +141,7 @@ let mk = | (VarLookup, _) | (Sequence, _) | (FunClosure, _) + | (FixClosure, _) | (UpdateTest, _) | (CastAp, _) | (BuiltinWrap, _) From 2ad6918b73e45c1d3b81c80987934dbc09b10b94 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 22 Feb 2024 17:06:23 -0500 Subject: [PATCH 2/7] Fix fixpoint printing issues --- src/haz3lcore/dynamics/Transition.re | 6 +-- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 52 ++++++++++---------- 2 files changed, 30 insertions(+), 28 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a401d4a4ae..1320349508 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -666,10 +666,10 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) => | VarLookup => !settings.show_lookup_steps | CastAp | Cast => !settings.show_casts + | FixUnwrap => !settings.show_fixpoints | CaseNext | CompleteClosure | CompleteFilter - | FixClosure - | FixUnwrap | BuiltinWrap - | FunClosure => true; + | FunClosure + | FixClosure => true; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 30928b9a5c..1291579388 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -124,7 +124,6 @@ let mk = chosen_step: option(step), next_steps: list((EvalCtx.t, int)), recent_subst: list(Var.t), - recursive_calls: list(Var.t), ) : DHDoc.t => { open Doc; @@ -136,7 +135,8 @@ let mk = | (FunAp, _) => [] | (LetBind, Let(p, _, _)) => DHPat.bound_vars(p) | (LetBind, _) => [] - | (FixUnwrap, _) // TODO[Matt]: Could do something here? + | (FixUnwrap, FixF(f, _, _)) => [f] + | (FixUnwrap, _) => [] | (InvalidStep, _) | (VarLookup, _) | (Sequence, _) @@ -163,12 +163,24 @@ let mk = } | _ => recent_subst }; + let substitution = + hidden_steps + |> List.find_opt(step => + step.knd == VarLookup + // HACK[Matt]: to prevent substitutions hiding inside casts + && EvalCtx.fuzzy_mark(step.ctx) + ); + let next_recent_subst = + switch (substitution) { + | Some({d_loc: BoundVar(v), _}) => + List.filter(u => u != v, recent_subst) + | _ => recent_subst + }; let go' = ( ~env=env, ~enforce_inline=enforce_inline, - ~recent_subst=recent_subst, - ~recursive_calls=recursive_calls, + ~recent_subst=next_recent_subst, d, ctx, ) => { @@ -192,7 +204,6 @@ let mk = next_steps, ), recent_subst, - recursive_calls, ); }; let parenthesize = (b, doc) => @@ -319,7 +330,6 @@ let mk = | InconsistentBranches(u, i, Case(dscrut, drs, _)) => go_case(dscrut, drs, false) |> annot(DHAnnot.InconsistentBranches((u, i))) - | BoundVar(x) when List.mem(x, recursive_calls) => text(x) | BoundVar(x) when settings.show_lookup_steps => text(x) | BoundVar(x) => switch (ClosureEnvironment.lookup(env, x)) { @@ -329,7 +339,12 @@ let mk = hcats([ go'(~env=ClosureEnvironment.empty, BoundVar(x), BoundVar) |> annot(DHAnnot.Substituted), - go'(~env=ClosureEnvironment.empty, d', BoundVar), + go'( + ~env=ClosureEnvironment.empty, + ~recent_subst=List.filter(u => u != x, next_recent_subst), + d', + BoundVar, + ), ]); } else { go'(~env=ClosureEnvironment.empty, d', BoundVar); @@ -458,7 +473,7 @@ let mk = ~enforce_inline=false, ~env=ClosureEnvironment.without_keys(bindings, env), ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), + List.filter(x => !List.mem(x, bindings), next_recent_subst), dbody, Let2, ), @@ -518,17 +533,14 @@ let mk = let bindings = DHPat.bound_vars(dp); let body_doc = go_formattable( - Closure( - ClosureEnvironment.without_keys(Option.to_list(s), env'), - d, - ), + Closure(env', d), ~env= ClosureEnvironment.without_keys( DHPat.bound_vars(dp) @ Option.to_list(s), env, ), ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), + List.filter(x => !List.mem(x, bindings), next_recent_subst), Fun, ); hcats( @@ -570,8 +582,7 @@ let mk = dbody, ~env=ClosureEnvironment.without_keys(bindings, env), ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), - ~recursive_calls=Option.to_list(s) @ recursive_calls, + List.filter(x => !List.mem(x, bindings), next_recent_subst), Fun, ); hcats( @@ -630,8 +641,7 @@ let mk = doc_body |> DHDoc_common.pad_child(~enforce_inline), ], ); - | FixF(x, _, d) => - go'(~env=ClosureEnvironment.without_keys([x], env), d, FixF) + | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ ">")) }; }; let steppable = @@ -640,13 +650,6 @@ let mk = chosen_step |> Option.map(x => x.ctx == Mark) |> Option.value(~default=false); - let substitution = - hidden_steps - |> List.find_opt(step => - step.knd == VarLookup - // HACK[Matt]: to prevent substitutions hiding inside casts - && EvalCtx.fuzzy_mark(step.ctx) - ); let doc = switch (substitution) { | Some({d_loc: BoundVar(v), _}) when List.mem(v, recent_subst) => @@ -674,6 +677,5 @@ let mk = chosen_step, List.mapi((idx, x: EvalObj.t) => (x.ctx, idx), next_steps), [], - [], ); }; From 169c9e07b68d423ca2f383a734c9ab2e69262d7c Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Thu, 29 Feb 2024 11:57:55 -0500 Subject: [PATCH 3/7] Update DHDoc_Exp.re --- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 1291579388..80ece39503 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -636,12 +636,13 @@ let mk = : [] ) @ [ + space(), DHDoc_common.Delim.arrow_FixF, space(), doc_body |> DHDoc_common.pad_child(~enforce_inline), ], ); - | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ ">")) + | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ "*>")) }; }; let steppable = From 8db9ad977c1343d1767a1eec62f0ddc99efd7ee6 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 8 Mar 2024 13:23:03 -0500 Subject: [PATCH 4/7] Change fixpoint printing --- src/haz3lcore/dynamics/Elaborator.re | 4 +- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 117 ++++++++----------- 2 files changed, 48 insertions(+), 73 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 68d352c67f..783d84e4f7 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -231,13 +231,13 @@ let rec dhexp_of_uexp = DHExp.Let(dp, add_name(Term.UPat.get_var(p), ddef), dbody) | Some([f]) => /* simple recursion */ - Let(dp, FixF(f, ty, add_name(Some(f), ddef)), dbody) + Let(dp, FixF(f, ty, add_name(Some(f ++ "+"), ddef)), dbody) | Some(fs) => /* mutual recursion */ let ddef = switch (ddef) { | Tuple(a) => - DHExp.Tuple(List.map2(s => add_name(Some(s)), fs, a)) + DHExp.Tuple(List.map2(s => add_name(Some(s ++ "+")), fs, a)) | _ => ddef }; let uniq_id = List.nth(def.ids, 0); diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 80ece39503..1a45fe2146 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -528,12 +528,13 @@ let mk = ), DHDoc_common.Delim.mk(")"), ]); - | Fun(dp, ty, Closure(env', d), s) => - if (settings.show_fn_bodies) { - let bindings = DHPat.bound_vars(dp); - let body_doc = + | Fun(dp, ty, dbody, s) when settings.show_fn_bodies => + let bindings = DHPat.bound_vars(dp); + let body_doc = + switch (dbody) { + | Closure(env', dbody) => go_formattable( - Closure(env', d), + Closure(env', dbody), ~env= ClosureEnvironment.without_keys( DHPat.bound_vars(dp) @ Option.to_list(s), @@ -542,81 +543,55 @@ let mk = ~recent_subst= List.filter(x => !List.mem(x, bindings), next_recent_subst), Fun, - ); - hcats( - [ - DHDoc_common.Delim.sym_Fun, - DHDoc_Pat.mk(dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline, - ), - ] - @ ( - settings.show_casts - ? [ - DHDoc_common.Delim.colon_Fun, - space(), - DHDoc_Typ.mk(~enforce_inline=true, ty), - space(), - ] - : [] ) - @ [ - DHDoc_common.Delim.arrow_Fun, - space(), - body_doc |> DHDoc_common.pad_child(~enforce_inline=false), - ], - ); - } else { - switch (s) { - | None => annot(DHAnnot.Collapsed, text("")) - | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")) - }; - } - | Fun(dp, ty, dbody, s) => - if (settings.show_fn_bodies) { - let bindings = DHPat.bound_vars(dp); - let body_doc = + | _ => go_formattable( dbody, ~env=ClosureEnvironment.without_keys(bindings, env), ~recent_subst= List.filter(x => !List.mem(x, bindings), next_recent_subst), Fun, - ); - hcats( - [ - DHDoc_common.Delim.sym_Fun, - DHDoc_Pat.mk(dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline, - ), - ] - @ ( - settings.show_casts - ? [ - DHDoc_common.Delim.colon_Fun, - space(), - DHDoc_Typ.mk(~enforce_inline=true, ty), - space(), - ] - : [] ) - @ [ - DHDoc_common.Delim.arrow_Fun, - space(), - body_doc |> DHDoc_common.pad_child(~enforce_inline), - ], - ); - } else { + }; + hcats( + [ + DHDoc_common.Delim.sym_Fun, + DHDoc_Pat.mk(dp) + |> DHDoc_common.pad_child( + ~inline_padding=(space(), space()), + ~enforce_inline, + ), + ] + @ ( + settings.show_casts + ? [ + DHDoc_common.Delim.colon_Fun, + space(), + DHDoc_Typ.mk(~enforce_inline=true, ty), + space(), + ] + : [] + ) + @ [ + DHDoc_common.Delim.arrow_Fun, + space(), + body_doc |> DHDoc_common.pad_child(~enforce_inline=false), + ], + ); + | Fun(_, _, _, s) => + let name = switch (s) { - | None => annot(DHAnnot.Collapsed, text("")) - | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")) + | None => "anon fn" + | Some(name) + when + !settings.show_fixpoints + && String.ends_with(~suffix="+", name) => + String.sub(name, 0, String.length(name) - 1) + | Some(name) => name }; - } - | FixF(x, ty, dbody) when settings.show_fixpoints => + annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")); + | FixF(x, ty, dbody) + when settings.show_fn_bodies && settings.show_fixpoints => let doc_body = go_formattable( dbody, @@ -642,7 +617,7 @@ let mk = doc_body |> DHDoc_common.pad_child(~enforce_inline), ], ); - | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ "*>")) + | FixF(x, _, _) => annot(DHAnnot.Collapsed, text("<" ++ x ++ ">")) }; }; let steppable = From bd8d0698ac31997d8bfaf0f65bf7305973aac2f6 Mon Sep 17 00:00:00 2001 From: disconcision Date: Mon, 11 Mar 2024 14:22:44 -0400 Subject: [PATCH 5/7] fix unchecked exception due to explainthis listlit string template mismatch --- src/haz3lweb/explainthis/data/FunctionExp.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lweb/explainthis/data/FunctionExp.re b/src/haz3lweb/explainthis/data/FunctionExp.re index c83993f45a..895f9d7db6 100644 --- a/src/haz3lweb/explainthis/data/FunctionExp.re +++ b/src/haz3lweb/explainthis/data/FunctionExp.re @@ -254,7 +254,7 @@ let _exp = exp("e"); let function_listlit_exp_coloring_ids = _pat_body_function_exp_coloring_ids(Piece.id(_pat), Piece.id(_exp)); let function_listlit_exp: form = { - let explanation = "The only values that match the [*argument pattern*](%s) are lists with %n-elements, each matching the corresponding element pattern. When applied to an argument which matches the [*argument pattern*](%s), evaluates to the function [*body*](%s)."; + let explanation = "The only values that match the [*argument pattern*](%s) are lists with %s-elements, each matching the corresponding element pattern. When applied to an argument which matches the [*argument pattern*](%s), evaluates to the function [*body*](%s)."; let form = [mk_fun([[space(), _pat, space()]]), space(), _exp]; { id: FunctionExp(ListLit), From d4007ea17a81b78269b8ec7d4fdf01011dd8f292 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Wed, 13 Mar 2024 10:47:21 -0400 Subject: [PATCH 6/7] Update tests --- src/test/Test_Elaboration.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/Test_Elaboration.re b/src/test/Test_Elaboration.re index 2e20c1e869..98d1db0fdd 100644 --- a/src/test/Test_Elaboration.re +++ b/src/test/Test_Elaboration.re @@ -265,7 +265,7 @@ let d9: DHExp.t = Var("x"), Int, BinIntOp(Plus, IntLit(1), BoundVar("x")), - Some("f"), + Some("f+"), ), ), IntLit(55), From 88a23ab1fe22fc559538d978bcf1401fdf1eb8f0 Mon Sep 17 00:00:00 2001 From: disconcision Date: Thu, 14 Mar 2024 19:07:54 -0400 Subject: [PATCH 7/7] fix for issue #1244 --- src/haz3lcore/statics/TypBase.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 15620b1ac9..99a5e9cf33 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -227,7 +227,7 @@ module rec Typ: { | (Unknown(p1), Unknown(p2)) => Some(Unknown(join_type_provenance(p1, p2))) | (Unknown(_), ty) - | (ty, Unknown(Internal | SynSwitch)) => Some(ty) + | (ty, Unknown(_)) => Some(ty) | (Var(n1), Var(n2)) => if (n1 == n2) { Some(Var(n1));