From 118281a1b3bc82989c2cfee46a5f737af3a9c725 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 16 Feb 2024 18:42:35 +0800 Subject: [PATCH 01/12] Fix missing nested instrumentation --- src/haz3lcore/dynamics/Stepper.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 7b7e9cbfcd..d4e5316ab7 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -176,7 +176,7 @@ let rec matches = }; switch (ctx) { | Filter(_) => (ract, ridx, rctx) - | _ when midx == ridx && midx > pidx && mact |> snd == All => ( + | _ when mact |> snd == All => ( ract, ridx, Filter(Residue(midx, mact), rctx), From fc7aaf2badd5f57767364de623496e73976d9f72 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 16 Feb 2024 18:42:35 +0800 Subject: [PATCH 02/12] Fix missing nested instrumentation --- src/haz3lcore/dynamics/FilterMatcher.re | 1 + src/haz3lcore/dynamics/Stepper.re | 17 +++++++++++------ 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index dd501b3563..d76fdc3d0d 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -41,6 +41,7 @@ let rec matches_exp = | (Closure(env, d), _) => matches_exp(env, d, f) | (Cast(d, _, _), _) => matches_exp(env, d, f) | (FailedCast(d, _, _), _) => matches_exp(env, d, f) + | (Filter(Residue(_), d), _) => matches_exp(env, d, f) | (BoundVar(dx), BoundVar(fx)) => dx == fx | (BoundVar(dx), _) => diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index d4e5316ab7..9644341ad0 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -42,7 +42,7 @@ let rec matches = let (act, idx) = switch (ctx) { | Filter(_, _) => (pact, pidx) - | _ => midx > idx ? (mact, midx) : (pact, pidx) + | _ => midx > pidx ? (mact, midx) : (pact, pidx) }; let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => { (a, i, f(c)); @@ -58,10 +58,15 @@ let rec matches = let flt = flt |> FilterEnvironment.extends(flt'); let+ ctx = matches(env, flt, ctx, exp, act, idx); Filter(Filter(flt'), ctx); - | Filter(Residue(idx, act), ctx) => - let (ract, ridx, rctx) = matches(env, flt, ctx, exp, act, idx); - if (ridx == idx && ract |> snd == All) { - (ract, ridx, Filter(Residue(idx, act), rctx)); + | Filter(Residue(idx', act'), ctx) => + let (ract, ridx, rctx) = + if (idx > idx') { + matches(env, flt, ctx, exp, act, idx); + } else { + matches(env, flt, ctx, exp, act', idx'); + }; + if (act' |> snd == All) { + (ract, ridx, Filter(Residue(idx', act'), rctx)); } else { (ract, ridx, rctx); }; @@ -176,7 +181,7 @@ let rec matches = }; switch (ctx) { | Filter(_) => (ract, ridx, rctx) - | _ when mact |> snd == All => ( + | _ when midx > pidx && mact |> snd == All => ( ract, ridx, Filter(Residue(midx, mact), rctx), From 81f669dad811b4e5cc0fe19616b102998985c96d Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Tue, 20 Feb 2024 11:47:46 -0500 Subject: [PATCH 03/12] Make decompose more consistent across undo, step_forward, init --- src/haz3lcore/dynamics/EvaluatorStep.re | 193 +++++++++++++++++++++++- src/haz3lcore/dynamics/Stepper.re | 50 ++---- src/haz3lcore/dynamics/Transition.re | 2 +- src/haz3lcore/prog/ModelResult.re | 12 +- src/haz3lcore/prog/ModelResults.re | 4 +- src/haz3lweb/Export.re | 8 +- src/haz3lweb/Model.re | 14 +- src/haz3lweb/Store.re | 40 ++--- src/haz3lweb/Update.re | 19 ++- src/haz3lweb/view/StepperView.re | 2 +- 10 files changed, 263 insertions(+), 81 deletions(-) diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index b6fad324f2..0e9e9f366d 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -347,12 +347,199 @@ let decompose = (d: DHExp.t) => { Decompose.Result.unbox(rs); }; -let evaluate_with_history = d => { +let rec matches = + ( + env: ClosureEnvironment.t, + flt: FilterEnvironment.t, + ctx: EvalCtx.t, + exp: DHExp.t, + act: FilterAction.t, + idx: int, + ) + : (FilterAction.t, int, EvalCtx.t) => { + let composed = compose(ctx, exp); + let (pact, pidx) = (act, idx); + let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt); + let (act, idx) = + switch (ctx) { + | Filter(_, _) => (pact, pidx) + | _ => midx > idx ? (mact, midx) : (pact, pidx) + }; + let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => { + (a, i, f(c)); + }; + let (let+) = map; + let (ract, ridx, rctx) = + switch (ctx) { + | Mark => (act, idx, EvalCtx.Mark) + | Closure(env, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Closure(env, ctx); + | Filter(Filter(flt'), ctx) => + let flt = flt |> FilterEnvironment.extends(flt'); + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Filter(Filter(flt'), ctx); + | Filter(Residue(idx, act), ctx) => + let (ract, ridx, rctx) = matches(env, flt, ctx, exp, act, idx); + if (ridx == idx && ract |> snd == All) { + (ract, ridx, Filter(Residue(idx, act), rctx)); + } else { + (ract, ridx, rctx); + }; + | Sequence1(ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Sequence1(ctx, d2); + | Sequence2(d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Sequence2(d1, ctx); + | Let1(d1, ctx, d3) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Let1(d1, ctx, d3); + | Let2(d1, d2, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Let2(d1, d2, ctx); + | Fun(dp, ty, ctx, name) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Fun(dp, ty, ctx, name); + | FixF(name, ty, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + FixF(name, ty, ctx); + | Ap1(ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Ap1(ctx, d2); + | Ap2(d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Ap2(d1, ctx); + | IfThenElse1(c, ctx, d2, d3) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + IfThenElse1(c, ctx, d2, d3); + | IfThenElse2(c, d1, ctx, d3) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + IfThenElse2(c, d1, ctx, d3); + | IfThenElse3(c, d1, d2, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + IfThenElse3(c, d1, d2, ctx); + | BinBoolOp1(op, ctx, d1) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinBoolOp1(op, ctx, d1); + | BinBoolOp2(op, d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinBoolOp2(op, d1, ctx); + | BinIntOp1(op, ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinIntOp1(op, ctx, d2); + | BinIntOp2(op, d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinIntOp2(op, d1, ctx); + | BinFloatOp1(op, ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinFloatOp1(op, ctx, d2); + | BinFloatOp2(op, d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinFloatOp2(op, d1, ctx); + | BinStringOp1(op, ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinStringOp1(op, ctx, d2); + | BinStringOp2(op, d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + BinStringOp2(op, d1, ctx); + | Tuple(ctx, ds) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Tuple(ctx, ds); + | ApBuiltin(name, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ApBuiltin(name, ctx); + | Test(id, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Test(id, ctx); + | ListLit(u, i, ty, ctx, ds) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ListLit(u, i, ty, ctx, ds); + | Cons1(ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Cons1(ctx, d2); + | Cons2(d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Cons2(d1, ctx); + | ListConcat1(ctx, d2) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ListConcat1(ctx, d2); + | ListConcat2(d1, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ListConcat2(d1, ctx); + | Prj(ctx, n) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Prj(ctx, n); + | NonEmptyHole(e, u, i, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + NonEmptyHole(e, u, i, ctx); + | Cast(ctx, ty, ty') => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Cast(ctx, ty, ty'); + | FailedCast(ctx, ty, ty') => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + FailedCast(ctx, ty, ty'); + | InvalidOperation(ctx, error) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + InvalidOperation(ctx, error); + | ConsistentCase(Case(ctx, rs, i)) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ConsistentCase(Case(ctx, rs, i)); + | ConsistentCaseRule(dexp, dpat, ctx, rs, i) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + ConsistentCaseRule(dexp, dpat, ctx, rs, i); + | InconsistentBranches(u, i, Case(ctx, rs, ri)) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + InconsistentBranches(u, i, Case(ctx, rs, ri)); + | InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri); + }; + switch (ctx) { + | Filter(_) => (ract, ridx, rctx) + | _ when mact |> snd == All => ( + ract, + ridx, + Filter(Residue(midx, mact), rctx), + ) + | _ => (ract, ridx, rctx) + }; +}; + +let should_hide_eval_obj = + (~settings, x: EvalObj.t): (FilterAction.action, EvalObj.t) => + if (should_hide_step_kind(~settings, x.knd)) { + (Eval, x); + } else { + let (act, _, ctx) = + matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0); + switch (act) { + | (Eval, _) => (Eval, {...x, ctx}) + | (Step, _) => (Step, {...x, ctx}) + }; + }; + +let should_hide_step = (~settings, x: step): (FilterAction.action, step) => + if (should_hide_step_kind(~settings, x.knd)) { + (Eval, x); + } else { + let (act, _, ctx) = + matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0); + switch (act) { + | (Eval, _) => (Eval, {...x, ctx}) + | (Step, _) => (Step, {...x, ctx}) + }; + }; + +let decompose = (~settings, d) => + d |> decompose |> List.map(should_hide_eval_obj(~settings)); + +let evaluate_with_history = (~settings, d) => { let state = ref(EvaluatorState.init); let rec go = d => - switch (decompose(d)) { + switch (decompose(~settings, d)) { | [] => [] - | [x, ..._] => + | [(_, x), ..._] => switch (take_step(state, x.env, x.d_loc)) { | None => [] | Some(d) => diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 9644341ad0..6d84e9e973 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -23,7 +23,7 @@ type t = { elab: DHExp.t, previous: list(step), current, - next: list(EvalObj.t), + next: list((FilterAction.action, EvalObj.t)), }; let rec matches = @@ -192,7 +192,7 @@ let rec matches = let should_hide_eval_obj = (~settings, x: EvalObj.t): (FilterAction.action, EvalObj.t) => - if (should_hide_step(~settings, x.knd)) { + if (should_hide_step_kind(~settings, x.knd)) { (Eval, x); } else { let (act, _, ctx) = @@ -204,7 +204,7 @@ let should_hide_eval_obj = }; let should_hide_step = (~settings, x: step): (FilterAction.action, step) => - if (should_hide_step(~settings, x.knd)) { + if (should_hide_step_kind(~settings, x.knd)) { (Eval, x); } else { let (act, _, ctx) = @@ -229,7 +229,7 @@ let current_expr = (s: t) => let step_pending = (idx: int, {elab, previous, current, next}: t) => { // TODO[Matt]: change to nth_opt after refactor - let eo = List.nth(next, idx); + let eo = List.nth(next, idx) |> snd; switch (current) { | StepperOK(d, s) => { elab, @@ -257,31 +257,15 @@ let step_pending = (idx: int, {elab, previous, current, next}: t) => { }; }; -let init = (elab: DHExp.t) => { +let init = (~settings, elab: DHExp.t) => { { elab, previous: [], current: StepPending(elab, EvaluatorState.init, None), - next: decompose(elab), + next: decompose(~settings, elab), }; }; -let update_result = - ( - ( - d: DHExp.t, - state: EvaluatorState.t, - next_eval_objs: list(EvalObj.t), - skipped_steps: list(step), - ), - s: t, - ) => { - previous: skipped_steps @ s.previous, - current: StepperOK(d, state), - next: next_eval_objs, - elab: s.elab, -}; - let rec evaluate_pending = (~settings, s: t) => { switch (s.current) { | StepperOK(_) @@ -301,27 +285,26 @@ let rec evaluate_pending = (~settings, s: t) => { ...s.previous, ], current: StepPending(d', state_ref^, None), - next: decompose(d'), + next: decompose(~settings, d'), } |> evaluate_pending(~settings); | StepPending(d, state, None) => - let next' = s.next |> List.map(should_hide_eval_obj(~settings)); - switch (List.find_opt(((act, _)) => act == FilterAction.Eval, next')) { + switch (List.find_opt(((act, _)) => act == FilterAction.Eval, s.next)) { | Some((_, eo)) => { elab: s.elab, previous: s.previous, current: StepPending(d, state, Some(eo)), - next: next' |> List.map(snd), + next: s.next, } |> evaluate_pending(~settings) | None => { elab: s.elab, previous: s.previous, current: StepperOK(d, state), - next: next' |> List.map(snd), + next: s.next, } - }; + } }; }; @@ -384,7 +367,7 @@ let step_backward = (~settings, s: t) => | None => failwith("cannot step backwards") | Some((x, xs)) => { current: StepperOK(x.d, x.state), - next: decompose(x.d), + next: decompose(~settings, x.d), previous: xs, elab: s.elab, } @@ -475,8 +458,7 @@ let to_persistent: t => persistent = } | {elab, previous, current, _} => {elab, previous, current}; -let from_persistent: persistent => t = - ({elab, previous, current}) => { - let s = {elab, previous, current, next: []}; - {elab, previous, current, next: decompose(current_expr(s))}; - }; +let from_persistent = (~settings, {elab, previous, current}) => { + let s = {elab, previous, current, next: []}; + {elab, previous, current, next: decompose(~settings, current_expr(s))}; +}; diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index dfe896ca06..96fae9315d 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -644,7 +644,7 @@ module Transition = (EV: EV_MODE) => { }; }; -let should_hide_step = (~settings: CoreSettings.Evaluation.t) => +let should_hide_step_kind = (~settings: CoreSettings.Evaluation.t) => fun | LetBind | Sequence diff --git a/src/haz3lcore/prog/ModelResult.re b/src/haz3lcore/prog/ModelResult.re index fe1e40d281..5965cd1c52 100644 --- a/src/haz3lcore/prog/ModelResult.re +++ b/src/haz3lcore/prog/ModelResult.re @@ -14,14 +14,14 @@ type t = let init_eval = elab => Evaluation({elab, evaluation: ResultPending, previous: ResultPending}); -let update_elab = elab => +let update_elab = (~settings, elab) => fun | NoElab => Evaluation({elab, evaluation: ResultPending, previous: ResultPending}) | Evaluation({evaluation, _}) => Evaluation({elab, evaluation: ResultPending, previous: evaluation}) | Stepper({elab: elab2, _}) as s when DHExp.fast_equal(elab, elab2) => s - | Stepper(_) => Stepper(Stepper.init(elab)); + | Stepper(_) => Stepper(Stepper.init(~settings, elab)); let update_stepper = f => fun @@ -55,10 +55,10 @@ let timeout: t => t = Evaluation({...e, evaluation: ResultFail(Timeout), previous: evaluation}) | Stepper(s) => Stepper(Stepper.timeout(s)); -let toggle_stepper = +let toggle_stepper = (~settings) => fun | NoElab => NoElab - | Evaluation({elab, _}) => Stepper(Stepper.init(elab)) + | Evaluation({elab, _}) => Stepper(Stepper.init(~settings, elab)) | Stepper({elab, _}) => Evaluation({elab, evaluation: ResultPending, previous: ResultPending}); @@ -91,7 +91,7 @@ let to_persistent: t => persistent = | Evaluation(_) => Evaluation | Stepper(s) => Stepper(Stepper.to_persistent(s)); -let of_persistent: persistent => t = +let of_persistent = (~settings) => fun | Evaluation => NoElab - | Stepper(s) => Stepper(Stepper.from_persistent(s)); + | Stepper(s) => Stepper(Stepper.from_persistent(~settings, s)); diff --git a/src/haz3lcore/prog/ModelResults.re b/src/haz3lcore/prog/ModelResults.re index a1814f14ba..cceeb3153d 100644 --- a/src/haz3lcore/prog/ModelResults.re +++ b/src/haz3lcore/prog/ModelResults.re @@ -22,7 +22,7 @@ type t = M.t(ModelResult.t); let init_eval = (ds: list((Key.t, DHExp.t))): t => ds |> List.to_seq |> of_seq |> map(ModelResult.init_eval); -let update_elabs = +let update_elabs = (~settings) => List.fold_right(((k, elab), acc) => update( k, @@ -30,7 +30,7 @@ let update_elabs = Some( v |> Option.value(~default=ModelResult.NoElab) - |> ModelResult.update_elab(elab), + |> ModelResult.update_elab(~settings, elab), ), acc, ) diff --git a/src/haz3lweb/Export.re b/src/haz3lweb/Export.re index 7bc711cc34..0aa22384e2 100644 --- a/src/haz3lweb/Export.re +++ b/src/haz3lweb/Export.re @@ -22,8 +22,10 @@ type all_f22 = { let mk_all = (~instructor_mode, ~log) => { let settings = Store.Settings.export(); let explainThisModel = Store.ExplainThisModel.export(); - let scratch = Store.Scratch.export(); - let documentation = Store.Documentation.export(); + let settings_obj = Store.Settings.load(); + let scratch = Store.Scratch.export(~settings=settings_obj.core.evaluation); + let documentation = + Store.Documentation.export(~settings=settings_obj.core.evaluation); let exercise = Store.Exercise.export( ~specs=ExerciseSettings.exercises, @@ -53,7 +55,7 @@ let import_all = (data, ~specs) => { let settings = Store.Settings.import(all.settings); Store.ExplainThisModel.import(all.explainThisModel); let instructor_mode = settings.instructor_mode; - Store.Scratch.import(all.scratch); + Store.Scratch.import(~settings=settings.core.evaluation, all.scratch); Store.Exercise.import(all.exercise, ~specs, ~instructor_mode); Log.import(all.log); }; diff --git a/src/haz3lweb/Model.re b/src/haz3lweb/Model.re index 75ac22a0e4..65c5d519c0 100644 --- a/src/haz3lweb/Model.re +++ b/src/haz3lweb/Model.re @@ -56,14 +56,14 @@ let blank = mk(Editors.Scratch(0, []), ModelResults.empty, CachedStatics.empty); let load_editors = - (~mode: Settings.mode, ~instructor_mode: bool) + (~settings, ~mode: Settings.mode, ~instructor_mode: bool) : (Editors.t, ModelResults.t) => switch (mode) { | Scratch => - let (idx, slides, results) = Store.Scratch.load(); + let (idx, slides, results) = Store.Scratch.load(~settings); (Scratch(idx, slides), results); | Documentation => - let (name, slides, results) = Store.Documentation.load(); + let (name, slides, results) = Store.Documentation.load(~settings); (Documentation(name, slides), results); | Exercises => let (n, specs, exercise) = @@ -90,6 +90,7 @@ let load = (init_model: t): t => { let explainThisModel = Store.ExplainThisModel.load(); let (editors, results) = load_editors( + ~settings=settings.core.evaluation, ~mode=settings.mode, ~instructor_mode=settings.instructor_mode, ); @@ -112,10 +113,11 @@ let reset = (model: t): t => { /* Reset model to default, including in localstorage, but don't otherwise erase localstorage, allowing e.g. api keys to persist */ - ignore(Store.Settings.init()); + let settings = Store.Settings.init(); + ignore(settings); ignore(Store.ExplainThisModel.init()); - ignore(Store.Scratch.init()); - ignore(Store.Documentation.init()); + ignore(Store.Scratch.init(~settings=settings.core.evaluation)); + ignore(Store.Documentation.init(~settings=settings.core.evaluation)); ignore(Store.Exercise.init(~instructor_mode=true)); let new_model = load(blank); { diff --git a/src/haz3lweb/Store.re b/src/haz3lweb/Store.re index 8156dd975d..0c4ac3fe23 100644 --- a/src/haz3lweb/Store.re +++ b/src/haz3lweb/Store.re @@ -121,14 +121,14 @@ module Scratch = { |> ModelResults.bindings, ); - let of_persistent = ((idx, slides, results): persistent) => { + let of_persistent = (~settings, (idx, slides, results): persistent) => { ( idx, List.map(ScratchSlide.unpersist, slides), results |> List.to_seq |> ModelResults.of_seq - |> ModelResults.map(ModelResult.of_persistent), + |> ModelResults.map(ModelResult.of_persistent(~settings)), ); }; @@ -144,23 +144,23 @@ module Scratch = { JsUtil.set_localstore(save_scratch_key, serialize(scratch)); }; - let init = () => { - let scratch = of_persistent(Init.startup.scratch); + let init = (~settings) => { + let scratch = of_persistent(~settings, Init.startup.scratch); save(scratch); scratch; }; - let load = () => + let load = (~settings) => switch (JsUtil.get_localstore(save_scratch_key)) { - | None => init() + | None => init(~settings) | Some(data) => - try(deserialize(data)) { - | _ => init() + try(deserialize(~settings, data)) { + | _ => init(~settings) } }; - let export = () => serialize(load()); - let import = data => save(deserialize(data)); + let export = (~settings) => serialize(load(~settings)); + let import = (~settings, data) => save(deserialize(~settings, data)); }; module Documentation = { @@ -186,14 +186,14 @@ module Documentation = { |> ModelResults.bindings, ); - let of_persistent = ((string, slides, results): persistent) => { + let of_persistent = (~settings, (string, slides, results): persistent) => { ( string, List.map(unpersist, slides), results |> List.to_seq |> ModelResults.of_seq - |> ModelResults.map(ModelResult.of_persistent), + |> ModelResults.map(ModelResult.of_persistent(~settings)), ); }; @@ -209,23 +209,23 @@ module Documentation = { JsUtil.set_localstore(save_documentation_key, serialize(slides)); }; - let init = () => { - let documentation = of_persistent(Init.startup.documentation); + let init = (~settings) => { + let documentation = of_persistent(~settings, Init.startup.documentation); save(documentation); documentation; }; - let load = () => + let load = (~settings) => switch (JsUtil.get_localstore(save_documentation_key)) { - | None => init() + | None => init(~settings) | Some(data) => - try(deserialize(data)) { - | _ => init() + try(deserialize(~settings, data)) { + | _ => init(~settings) } }; - let export = () => serialize(load()); - let import = data => save(deserialize(data)); + let export = (~settings) => serialize(load(~settings)); + let import = (~settings, data) => save(deserialize(~settings, data)); }; module Exercise = { diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 260aa6a151..e9d4f46068 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -207,7 +207,10 @@ let schedule_evaluation = (~schedule_action, model: Model.t): unit => if (!ModelResults.is_empty(step_rs)) { let new_rs = step_rs - |> ModelResults.update_elabs(elabs) + |> ModelResults.update_elabs( + ~settings=model.settings.core.evaluation, + elabs, + ) |> ModelResults.run_pending(~settings=model.settings.core); schedule_action(UpdateResult(new_rs)); }; @@ -279,11 +282,15 @@ let switch_exercise_editor = this between users. The former is a TODO, currently difficult due to the more complex architecture of Exercises. */ let export_persistent_data = () => { + let settings = Store.Settings.load(); let data: PersistentData.t = { documentation: - Store.Documentation.load() |> Store.Documentation.to_persistent, - scratch: Store.Scratch.load() |> Store.Scratch.to_persistent, - settings: Store.Settings.load(), + Store.Documentation.load(~settings=settings.core.evaluation) + |> Store.Documentation.to_persistent, + scratch: + Store.Scratch.load(~settings=settings.core.evaluation) + |> Store.Scratch.to_persistent, + settings, }; let contents = "let startup : PersistentData.t = " ++ PersistentData.show(data); @@ -491,7 +498,9 @@ let rec apply = Some( v |> Option.value(~default=NoElab: ModelResult.t) - |> ModelResult.toggle_stepper, + |> ModelResult.toggle_stepper( + ~settings=model.settings.core.evaluation, + ), ) ), }) diff --git a/src/haz3lweb/view/StepperView.re b/src/haz3lweb/view/StepperView.re index 83813b4f0b..2a31bf9f0d 100644 --- a/src/haz3lweb/view/StepperView.re +++ b/src/haz3lweb/view/StepperView.re @@ -187,7 +187,7 @@ let stepper_view = previous |> List.nth_opt(_, 0) |> Option.map((x: Stepper.step_with_previous) => x.step), - ~next_steps=Stepper.get_next_steps(stepper), + ~next_steps=Stepper.get_next_steps(stepper) |> List.map(snd), ~hidden_steps=hidden, ~result_key, d, From f585f9cc072c4b268bb002eda016baf831b3c57b Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Wed, 28 Feb 2024 14:22:44 -0500 Subject: [PATCH 04/12] Fix merge issues --- src/haz3lcore/dynamics/EvaluatorStep.re | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index 0e9e9f366d..5e0ed14db9 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -363,7 +363,7 @@ let rec matches = let (act, idx) = switch (ctx) { | Filter(_, _) => (pact, pidx) - | _ => midx > idx ? (mact, midx) : (pact, pidx) + | _ => midx > pidx ? (mact, midx) : (pact, pidx) }; let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => { (a, i, f(c)); @@ -379,10 +379,15 @@ let rec matches = let flt = flt |> FilterEnvironment.extends(flt'); let+ ctx = matches(env, flt, ctx, exp, act, idx); Filter(Filter(flt'), ctx); - | Filter(Residue(idx, act), ctx) => - let (ract, ridx, rctx) = matches(env, flt, ctx, exp, act, idx); - if (ridx == idx && ract |> snd == All) { - (ract, ridx, Filter(Residue(idx, act), rctx)); + | Filter(Residue(idx', act'), ctx) => + let (ract, ridx, rctx) = + if (idx > idx') { + matches(env, flt, ctx, exp, act, idx); + } else { + matches(env, flt, ctx, exp, act', idx'); + }; + if (act' |> snd == All) { + (ract, ridx, Filter(Residue(idx', act'), rctx)); } else { (ract, ridx, rctx); }; @@ -497,7 +502,7 @@ let rec matches = }; switch (ctx) { | Filter(_) => (ract, ridx, rctx) - | _ when mact |> snd == All => ( + | _ when midx > pidx && mact |> snd == All => ( ract, ridx, Filter(Residue(midx, mact), rctx), From dd5348644def7fd378512652852d8a70ff56d680 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 1 Mar 2024 00:22:18 +0800 Subject: [PATCH 05/12] Use separate envs for d and f during matching --- src/haz3lcore/dynamics/EvaluatorStep.re | 9 -- src/haz3lcore/dynamics/FilterMatcher.re | 147 ++++++++++++------------ src/haz3lcore/dynamics/Transition.re | 10 +- 3 files changed, 81 insertions(+), 85 deletions(-) diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index 5e0ed14db9..9fc7e0b839 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -150,15 +150,6 @@ module Decompose = { module Decomp = Transition(DecomposeEVMode); let rec decompose = (state, env, exp) => { switch (exp) { - | DHExp.Filter(flt, d1) => - DecomposeEVMode.( - { - let. _ = otherwise(env, (d1) => (Filter(flt, d1): DHExp.t)) - and. d1 = - req_final(decompose(state, env), d1 => Filter(flt, d1), d1); - Step({apply: () => d1, kind: CompleteFilter, value: true}); - } - ) | _ => Decomp.transition(decompose, state, env, exp) }; }; diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d76fdc3d0d..e92debafd8 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -1,5 +1,13 @@ let rec matches_exp = - (env: ClosureEnvironment.t, d: DHExp.t, f: DHExp.t): bool => { + ( + ~denv: ClosureEnvironment.t, + d: DHExp.t, + ~fenv: ClosureEnvironment.t, + f: DHExp.t, + ) + : bool => { + let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => + matches_exp(~denv, d, ~fenv, f); switch (d, f) { | (Constructor("$e"), _) => failwith("$e in matched expression") | (Constructor("$v"), _) => failwith("$v in matched expression") @@ -7,25 +15,27 @@ let rec matches_exp = // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps | (FixF(dp, _, dc), f) => matches_exp( - env, - Closure( - Transition.evaluate_extend_env(Environment.singleton((dp, dc)), env), - dc, - ), + ~denv= + Transition.evaluate_extend_env( + Environment.singleton((dp, dc)), + denv, + ), + dc, f, ) - | (d, FixF(fp, _, fc)) => + | (dexp, FixF(fp, _, fc)) => matches_exp( - env, - d, - Closure( - Transition.evaluate_extend_env(Environment.singleton((fp, fc)), env), - fc, - ), + dexp, + ~fenv= + Transition.evaluate_extend_env( + Environment.singleton((fp, fc)), + fenv, + ), + f, ) | (_, Constructor("$v")) => - switch (ValueChecker.check_value(env, d)) { + switch (ValueChecker.check_value(denv, d)) { | Indet | Value => true | Expr => false @@ -34,34 +44,40 @@ let rec matches_exp = | (_, EmptyHole(_)) | (_, Constructor("$e")) => true - | (_, Closure(env, f)) => matches_exp(env, d, f) - | (_, Cast(f, _, _)) => matches_exp(env, d, f) - | (_, FailedCast(f, _, _)) => matches_exp(env, d, f) + | (_, Closure(fenv, f)) => matches_exp(~fenv, d, f) + | (_, Cast(f, _, _)) => matches_exp(d, f) + | (_, FailedCast(f, _, _)) => matches_exp(d, f) - | (Closure(env, d), _) => matches_exp(env, d, f) - | (Cast(d, _, _), _) => matches_exp(env, d, f) - | (FailedCast(d, _, _), _) => matches_exp(env, d, f) - | (Filter(Residue(_), d), _) => matches_exp(env, d, f) + | (Closure(denv, d), _) => matches_exp(~denv, d, f) + | (Cast(d, _, _), _) => matches_exp(d, f) + | (FailedCast(d, _, _), _) => matches_exp(d, f) + | (Filter(Residue(_), d), _) => matches_exp(d, f) - | (BoundVar(dx), BoundVar(fx)) => dx == fx + | (BoundVar(dx), BoundVar(fx)) => + switch ( + ClosureEnvironment.lookup(denv, dx), + ClosureEnvironment.lookup(fenv, fx), + ) { + | (Some(d), Some(f)) => matches_exp(d, f) + | (Some(_), None) => false + | (None, Some(_)) => false + | (None, None) => true + } | (BoundVar(dx), _) => - let d = - ClosureEnvironment.lookup(env, dx) - |> Util.OptUtil.get(() => { - print_endline("FreeInvalidVar:" ++ dx); - raise(EvaluatorError.Exception(FreeInvalidVar(dx))); - }); - matches_exp(env, d, f); + switch (ClosureEnvironment.lookup(denv, dx)) { + | Some(d) => matches_exp(d, f) + | None => false + } | (_, BoundVar(fx)) => - switch (ClosureEnvironment.lookup(env, fx)) { - | Some(f) => matches_exp(env, d, f) + switch (ClosureEnvironment.lookup(fenv, fx)) { + | Some(f) => matches_exp(d, f) | None => false } | (EmptyHole(_), _) => false | (Filter(df, dd), Filter(ff, fd)) => - DH.DHFilter.fast_equal(df, ff) && matches_exp(env, dd, fd) + DH.DHFilter.fast_equal(df, ff) && matches_exp(dd, fd) | (Filter(_), _) => false | (BoolLit(dv), BoolLit(fv)) => dv == fv @@ -83,11 +99,8 @@ let rec matches_exp = | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn | (BuiltinFun(_), _) => false - | (Fun(dp1, dty1, d1, dname1), Fun(fp1, fty1, f1, fname1)) => - matches_pat(dp1, fp1) - && dty1 == fty1 - && matches_exp(env, d1, f1) - && dname1 == fname1 + | (Fun(dp1, dty1, d1, _), Fun(fp1, fty1, f1, _)) => + matches_pat(dp1, fp1) && dty1 == fty1 && matches_exp(d1, f1) | (Fun(_), _) => false | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) => @@ -95,38 +108,34 @@ let rec matches_exp = | (FreeVar(_), _) => false | (Let(dp, d1, d2), Let(fp, f1, f2)) => - matches_pat(dp, fp) - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) + matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2) | (Let(_), _) => false - | (Ap(d1, d2), Ap(f1, f2)) => - matches_exp(env, d1, f1) && matches_exp(env, d2, f2) + | (Ap(d1, d2), Ap(f1, f2)) => matches_exp(d1, f1) && matches_exp(d2, f2) | (Ap(_), _) => false | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) => dc == fc - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) - && matches_exp(env, d3, f3) + && matches_exp(d1, f1) + && matches_exp(d2, f2) + && matches_exp(d3, f3) | (IfThenElse(_), _) => false | (Sequence(d1, d2), Sequence(f1, f2)) => - matches_exp(env, d1, f1) && matches_exp(env, d2, f2) + matches_exp(d1, f1) && matches_exp(d2, f2) | (Sequence(_), _) => false - | (Test(id1, d2), Test(id2, f2)) => - id1 == id2 && matches_exp(env, d2, f2) + | (Test(id1, d2), Test(id2, f2)) => id1 == id2 && matches_exp(d2, f2) | (Test(_), _) => false | (Cons(d1, d2), Cons(f1, f2)) => - matches_exp(env, d1, f1) && matches_exp(env, d2, f2) + matches_exp(d1, f1) && matches_exp(d2, f2) | (Cons(_), _) => false | (ListLit(_, _, dt, dv), ListLit(_, _, ft, fv)) => dt == ft && List.fold_left2( - (acc, d, f) => acc && matches_exp(env, d, f), + (acc, d, f) => acc && matches_exp(d, f), true, dv, fv, @@ -134,37 +143,24 @@ let rec matches_exp = | (ListLit(_), _) => false | (Tuple(dv), Tuple(fv)) => - List.fold_left2( - (acc, d, f) => acc && matches_exp(env, d, f), - true, - dv, - fv, - ) + List.fold_left2((acc, d, f) => acc && matches_exp(d, f), true, dv, fv) | (Tuple(_), _) => false | (BinBoolOp(d_op_bin, d1, d2), BinBoolOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) | (BinBoolOp(_), _) => false | (BinIntOp(d_op_bin, d1, d2), BinIntOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) | (BinIntOp(_), _) => false | (BinFloatOp(d_op_bin, d1, d2), BinFloatOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) | (BinFloatOp(_), _) => false | (BinStringOp(d_op_bin, d1, d2), BinStringOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin - && matches_exp(env, d1, f1) - && matches_exp(env, d2, f2) + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) | (BinStringOp(_), _) => false | (ListConcat(_), _) => false @@ -177,11 +173,12 @@ let rec matches_exp = InconsistentBranches(_, _, Case(dscrut, drule, _)), InconsistentBranches(_, _, Case(fscrut, frule, _)), ) => - matches_exp(env, dscrut, fscrut) + matches_exp(dscrut, fscrut) && ( switch ( List.fold_left2( - (res, drule, frule) => res && matches_rul(env, drule, frule), + (res, drule, frule) => + res && matches_rul(~denv, drule, ~fenv, frule), true, drule, frule, @@ -200,10 +197,10 @@ let rec matches_exp = | (InvalidOperation(_), _) => false | (ApBuiltin(dname, darg), ApBuiltin(fname, farg)) => - dname == fname && matches_exp(env, darg, farg) + dname == fname && matches_exp(darg, farg) | (ApBuiltin(_), _) => false - | (Prj(dv, di), Prj(fv, fi)) => matches_exp(env, dv, fv) && di == fi + | (Prj(dv, di), Prj(fv, fi)) => matches_exp(dv, fv) && di == fi | (Prj(_), _) => false }; } @@ -256,17 +253,17 @@ and matches_pat = (d: DHPat.t, f: DHPat.t): bool => { and matches_typ = (d: Typ.t, f: Typ.t) => { Typ.eq(d, f); } -and matches_rul = (env, d: DHExp.rule, f: DHExp.rule) => { +and matches_rul = (~denv, d: DHExp.rule, ~fenv, f: DHExp.rule) => { switch (d, f) { | (Rule(dp, d), Rule(fp, f)) => - matches_pat(dp, fp) && matches_exp(env, d, f) + matches_pat(dp, fp) && matches_exp(~denv, d, ~fenv, f) }; }; let matches = (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: Filter.t) : option(FilterAction.t) => - if (matches_exp(env, exp, flt.pat)) { + if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) { Some(flt.act); } else { None; diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 96fae9315d..91dbbadc03 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -637,10 +637,18 @@ module Transition = (EV: EV_MODE) => { let. _ = otherwise(env, d1 => FailedCast(d1, t1, t2)) and. _ = req_final(req(state, env), d1 => FailedCast(d1, t1, t2), d1); Indet; - | Filter(f1, d1) => + | Filter(Filter({pat: Closure(_), _}) as f1, d1) + | Filter(Residue(_) as f1, d1) => let. _ = otherwise(env, d1 => Filter(f1, d1)) and. d1 = req_final(req(state, env), d1 => Filter(f1, d1), d1); Step({apply: () => d1, kind: CompleteFilter, value: true}); + | Filter(Filter({pat, act}) as f1, d1) => + let. _ = otherwise(env, Filter(f1, d1)); + Step({ + apply: () => Filter(Filter({pat: Closure(env, pat), act}), d1), + kind: CompleteFilter, + value: false, + }); }; }; From 3287b316528dc4cee0d6c9c3a4a1cbaeb770355c Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 1 Mar 2024 21:38:44 +0800 Subject: [PATCH 06/12] test for structural equality first --- src/haz3lcore/dynamics/FilterMatcher.re | 376 ++++++++++++------------ 1 file changed, 192 insertions(+), 184 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index e92debafd8..0c54a2dc68 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -8,200 +8,208 @@ let rec matches_exp = : bool => { let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); - switch (d, f) { - | (Constructor("$e"), _) => failwith("$e in matched expression") - | (Constructor("$v"), _) => failwith("$v in matched expression") - - // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps - | (FixF(dp, _, dc), f) => - matches_exp( - ~denv= - Transition.evaluate_extend_env( - Environment.singleton((dp, dc)), - denv, - ), - dc, - f, - ) - | (dexp, FixF(fp, _, fc)) => - matches_exp( - dexp, - ~fenv= - Transition.evaluate_extend_env( - Environment.singleton((fp, fc)), - fenv, - ), - f, - ) - - | (_, Constructor("$v")) => - switch (ValueChecker.check_value(denv, d)) { - | Indet - | Value => true - | Expr => false - } - - | (_, EmptyHole(_)) - | (_, Constructor("$e")) => true - - | (_, Closure(fenv, f)) => matches_exp(~fenv, d, f) - | (_, Cast(f, _, _)) => matches_exp(d, f) - | (_, FailedCast(f, _, _)) => matches_exp(d, f) - - | (Closure(denv, d), _) => matches_exp(~denv, d, f) - | (Cast(d, _, _), _) => matches_exp(d, f) - | (FailedCast(d, _, _), _) => matches_exp(d, f) - | (Filter(Residue(_), d), _) => matches_exp(d, f) - - | (BoundVar(dx), BoundVar(fx)) => - switch ( - ClosureEnvironment.lookup(denv, dx), - ClosureEnvironment.lookup(fenv, fx), - ) { - | (Some(d), Some(f)) => matches_exp(d, f) - | (Some(_), None) => false - | (None, Some(_)) => false - | (None, None) => true - } - | (BoundVar(dx), _) => - switch (ClosureEnvironment.lookup(denv, dx)) { - | Some(d) => matches_exp(d, f) - | None => false - } - | (_, BoundVar(fx)) => - switch (ClosureEnvironment.lookup(fenv, fx)) { - | Some(f) => matches_exp(d, f) - | None => false - } - - | (EmptyHole(_), _) => false - - | (Filter(df, dd), Filter(ff, fd)) => - DH.DHFilter.fast_equal(df, ff) && matches_exp(dd, fd) - | (Filter(_), _) => false - - | (BoolLit(dv), BoolLit(fv)) => dv == fv - | (BoolLit(_), _) => false - - | (IntLit(dv), IntLit(fv)) => dv == fv - | (IntLit(_), _) => false - - | (FloatLit(dv), FloatLit(fv)) => dv == fv - | (FloatLit(_), _) => false - - | (StringLit(dv), StringLit(fv)) => dv == fv - | (StringLit(_), _) => false - - | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true - | (Constructor(dt), Constructor(ft)) => dt == ft - | (Constructor(_), _) => false - - | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn - | (BuiltinFun(_), _) => false - - | (Fun(dp1, dty1, d1, _), Fun(fp1, fty1, f1, _)) => - matches_pat(dp1, fp1) && dty1 == fty1 && matches_exp(d1, f1) - | (Fun(_), _) => false - - | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) => - du == fu && di == fi && dx == fx - | (FreeVar(_), _) => false - - | (Let(dp, d1, d2), Let(fp, f1, f2)) => - matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2) - | (Let(_), _) => false - - | (Ap(d1, d2), Ap(f1, f2)) => matches_exp(d1, f1) && matches_exp(d2, f2) - | (Ap(_), _) => false - - | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) => - dc == fc - && matches_exp(d1, f1) - && matches_exp(d2, f2) - && matches_exp(d3, f3) - | (IfThenElse(_), _) => false - - | (Sequence(d1, d2), Sequence(f1, f2)) => - matches_exp(d1, f1) && matches_exp(d2, f2) - | (Sequence(_), _) => false - - | (Test(id1, d2), Test(id2, f2)) => id1 == id2 && matches_exp(d2, f2) - | (Test(_), _) => false - - | (Cons(d1, d2), Cons(f1, f2)) => - matches_exp(d1, f1) && matches_exp(d2, f2) - | (Cons(_), _) => false - - | (ListLit(_, _, dt, dv), ListLit(_, _, ft, fv)) => - dt == ft - && List.fold_left2( - (acc, d, f) => acc && matches_exp(d, f), - true, - dv, - fv, - ) - | (ListLit(_), _) => false - - | (Tuple(dv), Tuple(fv)) => - List.fold_left2((acc, d, f) => acc && matches_exp(d, f), true, dv, fv) - | (Tuple(_), _) => false - - | (BinBoolOp(d_op_bin, d1, d2), BinBoolOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) - - | (BinBoolOp(_), _) => false + if (d == f) { + true; + } else { + switch (d, f) { + | (Constructor("$e"), _) => failwith("$e in matched expression") + | (Constructor("$v"), _) => failwith("$v in matched expression") + + // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps + | (FixF(dp, dt, dc), FixF(fp, ft, fc)) => + dp == fp + && dt == ft + && matches_exp( + ~denv=denv |> ClosureEnvironment.without_keys([dp]), + dc, + ~fenv=fenv |> ClosureEnvironment.without_keys([fp]), + fc, + ) + | (FixF(dp, _, dc), f) => + matches_exp(~denv=denv |> ClosureEnvironment.without_keys([dp]), dc, f) + | (d, FixF(fp, _, fc)) => + matches_exp(d, ~fenv=fenv |> ClosureEnvironment.without_keys([fp]), fc) + + | (_, Constructor("$v")) => + switch (ValueChecker.check_value(denv, d)) { + | Indet + | Value => true + | Expr => false + } - | (BinIntOp(d_op_bin, d1, d2), BinIntOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) - | (BinIntOp(_), _) => false + | (_, EmptyHole(_)) + | (_, Constructor("$e")) => true - | (BinFloatOp(d_op_bin, d1, d2), BinFloatOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) - | (BinFloatOp(_), _) => false + | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f) - | (BinStringOp(d_op_bin, d1, d2), BinStringOp(f_op_bin, f1, f2)) => - d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) - | (BinStringOp(_), _) => false + | (_, Closure(fenv, f)) => matches_exp(~fenv, d, f) + | (_, Cast(f, _, _)) => matches_exp(d, f) + | (_, FailedCast(f, _, _)) => matches_exp(d, f) - | (ListConcat(_), _) => false + | (Closure(denv, d), _) => matches_exp(~denv, d, f) + | (Cast(d, _, _), _) => matches_exp(d, f) + | (FailedCast(d, _, _), _) => matches_exp(d, f) + | (Filter(Residue(_), d), _) => matches_exp(d, f) - | ( - ConsistentCase(Case(dscrut, drule, _)), - ConsistentCase(Case(fscrut, frule, _)), - ) - | ( - InconsistentBranches(_, _, Case(dscrut, drule, _)), - InconsistentBranches(_, _, Case(fscrut, frule, _)), - ) => - matches_exp(dscrut, fscrut) - && ( + | (BoundVar(dx), BoundVar(fx)) => switch ( - List.fold_left2( - (res, drule, frule) => - res && matches_rul(~denv, drule, ~fenv, frule), - true, - drule, - frule, - ) + ClosureEnvironment.lookup(denv, dx), + ClosureEnvironment.lookup(fenv, fx), ) { - | exception (Invalid_argument(_)) => false - | res => res + | (Some(d), Some(f)) => matches_exp(d, f) + | (Some(_), None) => false + | (None, Some(_)) => false + | (None, None) => true + } + | (BoundVar(dx), _) => + switch (ClosureEnvironment.lookup(denv, dx)) { + | Some(d) => matches_exp(d, f) + | None => false + } + | (_, BoundVar(fx)) => + switch (ClosureEnvironment.lookup(fenv, fx)) { + | Some(f) => matches_exp(d, f) + | None => false } - ) - | (ConsistentCase(_), _) - | (InconsistentBranches(_), _) => false - - | (NonEmptyHole(_), _) => false - | (ExpandingKeyword(_), _) => false - | (InvalidText(_), _) => false - | (InvalidOperation(_), _) => false - | (ApBuiltin(dname, darg), ApBuiltin(fname, farg)) => - dname == fname && matches_exp(darg, farg) - | (ApBuiltin(_), _) => false + | (EmptyHole(_), _) => false - | (Prj(dv, di), Prj(fv, fi)) => matches_exp(dv, fv) && di == fi - | (Prj(_), _) => false + | (Filter(df, dd), Filter(ff, fd)) => + DH.DHFilter.fast_equal(df, ff) && matches_exp(dd, fd) + | (Filter(_), _) => false + + | (BoolLit(dv), BoolLit(fv)) => dv == fv + | (BoolLit(_), _) => false + + | (IntLit(dv), IntLit(fv)) => dv == fv + | (IntLit(_), _) => false + + | (FloatLit(dv), FloatLit(fv)) => dv == fv + | (FloatLit(_), _) => false + + | (StringLit(dv), StringLit(fv)) => dv == fv + | (StringLit(_), _) => false + + | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true + | (Constructor(dt), Constructor(ft)) => dt == ft + | (Constructor(_), _) => false + + | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn + | (BuiltinFun(_), _) => false + + | (Fun(dp1, dty1, d1, _), Fun(fp1, fty1, f1, _)) => + matches_pat(dp1, fp1) + && dty1 == fty1 + && ( + if (d1 == f1) { + true; + } else { + matches_exp(d1, f1); + } + ) + | (Fun(_), _) => false + + | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) => + du == fu && di == fi && dx == fx + | (FreeVar(_), _) => false + + | (Let(dp, d1, d2), Let(fp, f1, f2)) => + matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2) + | (Let(_), _) => false + + | (Ap(d1, d2), Ap(f1, f2)) => + matches_exp(d1, f1) && matches_exp(d2, f2) + | (Ap(_), _) => false + + | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) => + dc == fc + && matches_exp(d1, f1) + && matches_exp(d2, f2) + && matches_exp(d3, f3) + | (IfThenElse(_), _) => false + + | (Sequence(d1, d2), Sequence(f1, f2)) => + matches_exp(d1, f1) && matches_exp(d2, f2) + | (Sequence(_), _) => false + + | (Test(id1, d2), Test(id2, f2)) => id1 == id2 && matches_exp(d2, f2) + | (Test(_), _) => false + + | (Cons(d1, d2), Cons(f1, f2)) => + matches_exp(d1, f1) && matches_exp(d2, f2) + | (Cons(_), _) => false + + | (ListLit(_, _, dt, dv), ListLit(_, _, ft, fv)) => + dt == ft + && List.fold_left2( + (acc, d, f) => acc && matches_exp(d, f), + true, + dv, + fv, + ) + | (ListLit(_), _) => false + + | (Tuple(dv), Tuple(fv)) => + List.fold_left2((acc, d, f) => acc && matches_exp(d, f), true, dv, fv) + | (Tuple(_), _) => false + + | (BinBoolOp(d_op_bin, d1, d2), BinBoolOp(f_op_bin, f1, f2)) => + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) + + | (BinBoolOp(_), _) => false + + | (BinIntOp(d_op_bin, d1, d2), BinIntOp(f_op_bin, f1, f2)) => + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) + | (BinIntOp(_), _) => false + + | (BinFloatOp(d_op_bin, d1, d2), BinFloatOp(f_op_bin, f1, f2)) => + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) + | (BinFloatOp(_), _) => false + + | (BinStringOp(d_op_bin, d1, d2), BinStringOp(f_op_bin, f1, f2)) => + d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2) + | (BinStringOp(_), _) => false + + | (ListConcat(_), _) => false + + | ( + ConsistentCase(Case(dscrut, drule, _)), + ConsistentCase(Case(fscrut, frule, _)), + ) + | ( + InconsistentBranches(_, _, Case(dscrut, drule, _)), + InconsistentBranches(_, _, Case(fscrut, frule, _)), + ) => + matches_exp(dscrut, fscrut) + && ( + switch ( + List.fold_left2( + (res, drule, frule) => + res && matches_rul(~denv, drule, ~fenv, frule), + true, + drule, + frule, + ) + ) { + | exception (Invalid_argument(_)) => false + | res => res + } + ) + | (ConsistentCase(_), _) + | (InconsistentBranches(_), _) => false + + | (NonEmptyHole(_), _) => false + | (ExpandingKeyword(_), _) => false + | (InvalidText(_), _) => false + | (InvalidOperation(_), _) => false + + | (ApBuiltin(dname, darg), ApBuiltin(fname, farg)) => + dname == fname && matches_exp(darg, farg) + | (ApBuiltin(_), _) => false + + | (Prj(dv, di), Prj(fv, fi)) => matches_exp(dv, fv) && di == fi + | (Prj(_), _) => false + }; }; } and matches_pat = (d: DHPat.t, f: DHPat.t): bool => { From 752e45d221b612603202bbfcc67717a6828f379f Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sat, 2 Mar 2024 16:01:02 +0800 Subject: [PATCH 07/12] test for structural equality for fixpoints --- src/haz3lcore/dynamics/FilterMatcher.re | 48 +++++++++++++++++++++++-- 1 file changed, 46 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 0c54a2dc68..52a3e355d0 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -1,3 +1,24 @@ +let rec find_keys = (dp: DHPat.t): list(string) => { + switch (dp) { + | DHPat.EmptyHole(_, _) + | DHPat.NonEmptyHole(_, _, _, _) + | DHPat.Wild + | DHPat.ExpandingKeyword(_, _, _) + | DHPat.InvalidText(_, _, _) + | DHPat.BadConstructor(_, _, _) => [] + | DHPat.Var(x) => [x] + | DHPat.IntLit(_) + | DHPat.FloatLit(_) + | DHPat.BoolLit(_) + | DHPat.StringLit(_) + | DHPat.Constructor(_) => [] + | DHPat.ListLit(_, dps) + | DHPat.Tuple(dps) => List.concat_map(find_keys, dps) + | DHPat.Cons(dp1, dp2) + | DHPat.Ap(dp1, dp2) => find_keys(dp1) @ find_keys(dp2) + }; +}; + let rec matches_exp = ( ~denv: ClosureEnvironment.t, @@ -6,6 +27,8 @@ let rec matches_exp = f: DHExp.t, ) : bool => { + print_endline("d = " ++ DHExp.show(d)); + print_endline("f = " ++ DHExp.show(f)); let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); if (d == f) { @@ -41,6 +64,8 @@ let rec matches_exp = | (_, Constructor("$e")) => true | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f) + | (Closure(denv, d), Closure(fenv, f)) => + matches_exp(~denv, d, ~fenv, f) | (_, Closure(fenv, f)) => matches_exp(~fenv, d, f) | (_, Cast(f, _, _)) => matches_exp(d, f) @@ -51,15 +76,29 @@ let rec matches_exp = | (FailedCast(d, _, _), _) => matches_exp(d, f) | (Filter(Residue(_), d), _) => matches_exp(d, f) + | (BoundVar(dx), BoundVar(fx)) + when String.starts_with(dx, ~prefix="__mutual__") => + String.starts_with(fx, ~prefix="__mutual__") && dx == fx | (BoundVar(dx), BoundVar(fx)) => switch ( ClosureEnvironment.lookup(denv, dx), ClosureEnvironment.lookup(fenv, fx), ) { + | ( + Some(Fun(_, _, d, Some(dname))), + Some(Fun(_, _, f, Some(fname))), + ) + when dx == dname && fx == fname => + matches_exp( + ~denv=ClosureEnvironment.without_keys([dname], denv), + d, + ~fenv=ClosureEnvironment.without_keys([fname], denv), + f, + ) | (Some(d), Some(f)) => matches_exp(d, f) | (Some(_), None) => false | (None, Some(_)) => false - | (None, None) => true + | (None, None) => dx == fx } | (BoundVar(dx), _) => switch (ClosureEnvironment.lookup(denv, dx)) { @@ -104,7 +143,12 @@ let rec matches_exp = if (d1 == f1) { true; } else { - matches_exp(d1, f1); + matches_exp( + ~denv=ClosureEnvironment.without_keys(find_keys(dp1), denv), + d1, + ~fenv=ClosureEnvironment.without_keys(find_keys(fp1), fenv), + f1, + ); } ) | (Fun(_), _) => false From 2f00fc66d2dde14ade03a621f46578e6e54c849e Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sun, 10 Mar 2024 16:37:10 +0800 Subject: [PATCH 08/12] proper alpha equivalence --- src/haz3lcore/dynamics/FilterMatcher.re | 49 +++++++++++++++---------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 52a3e355d0..8ab149defe 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -27,8 +27,6 @@ let rec matches_exp = f: DHExp.t, ) : bool => { - print_endline("d = " ++ DHExp.show(d)); - print_endline("f = " ++ DHExp.show(f)); let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); if (d == f) { @@ -98,7 +96,7 @@ let rec matches_exp = | (Some(d), Some(f)) => matches_exp(d, f) | (Some(_), None) => false | (None, Some(_)) => false - | (None, None) => dx == fx + | (None, None) => true } | (BoundVar(dx), _) => switch (ClosureEnvironment.lookup(denv, dx)) { @@ -136,21 +134,17 @@ let rec matches_exp = | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn | (BuiltinFun(_), _) => false - | (Fun(dp1, dty1, d1, _), Fun(fp1, fty1, f1, _)) => - matches_pat(dp1, fp1) - && dty1 == fty1 - && ( - if (d1 == f1) { - true; - } else { - matches_exp( - ~denv=ClosureEnvironment.without_keys(find_keys(dp1), denv), - d1, - ~fenv=ClosureEnvironment.without_keys(find_keys(fp1), fenv), - f1, - ); - } - ) + | ( + Fun(dp1, _, Closure(denv, d1), _), + Fun(fp1, _, Closure(fenv, f1), _), + ) => + matches_fun(~denv, dp1, d1, ~fenv, fp1, f1) + | (Fun(dp1, _, Closure(denv, d1), _), Fun(fp1, _, f1, _)) => + matches_fun(~denv, dp1, d1, ~fenv, fp1, f1) + | (Fun(dp1, _, d1, _), Fun(fp1, _, Closure(fenv, f1), _)) => + matches_fun(~denv, dp1, d1, ~fenv, fp1, f1) + | (Fun(dp1, _, d1, _), Fun(fp1, _, f1, _)) => + matches_fun(~denv, dp1, d1, ~fenv, fp1, f1) | (Fun(_), _) => false | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) => @@ -256,6 +250,23 @@ let rec matches_exp = }; }; } +and matches_fun = + ( + ~denv: ClosureEnvironment.t, + dp: DHPat.t, + d: DHExp.t, + ~fenv: ClosureEnvironment.t, + fp: DHPat.t, + f: DHExp.t, + ) => { + matches_pat(dp, fp) + && matches_exp( + ~denv=ClosureEnvironment.without_keys(find_keys(dp), denv), + d, + ~fenv=ClosureEnvironment.without_keys(find_keys(fp), fenv), + f, + ); +} and matches_pat = (d: DHPat.t, f: DHPat.t): bool => { switch (d, f) { | (_, EmptyHole(_)) => true @@ -279,7 +290,7 @@ and matches_pat = (d: DHPat.t, f: DHPat.t): bool => { | (ListLit(_), _) => false | (Constructor(dt), Constructor(ft)) => dt == ft | (Constructor(_), _) => false - | (Var(dx), Var(fx)) => dx == fx + | (Var(_), Var(_)) => true | (Var(_), _) => false | (Tuple(dl), Tuple(fl)) => switch ( From 57c83cf469b48e1ed050b2b8d059084e0fdc41b6 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sun, 10 Mar 2024 17:07:27 +0800 Subject: [PATCH 09/12] proper fix-point test --- src/haz3lcore/dynamics/FilterMatcher.re | 47 +++++++++++++++++++++++-- 1 file changed, 44 insertions(+), 3 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 8ab149defe..d4dd46ecc3 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -83,10 +83,51 @@ let rec matches_exp = ClosureEnvironment.lookup(fenv, fx), ) { | ( - Some(Fun(_, _, d, Some(dname))), - Some(Fun(_, _, f, Some(fname))), + Some(Fun(_, _, Closure(denv, _), Some(dname)) as d), + Some(Fun(_, _, Closure(fenv, _), Some(fname)) as f), ) - when dx == dname && fx == fname => + when + ClosureEnvironment.lookup(denv, dname) == Some(d) + && ClosureEnvironment.lookup(fenv, fname) == Some(f) => + matches_exp( + ~denv=ClosureEnvironment.without_keys([dname], denv), + d, + ~fenv=ClosureEnvironment.without_keys([fname], fenv), + f, + ) + | ( + Some(Fun(_, _, Closure(denv, _), Some(dname)) as d), + Some(Fun(_, _, _, Some(fname)) as f), + ) + when + ClosureEnvironment.lookup(denv, dname) == Some(d) + && ClosureEnvironment.lookup(fenv, fname) == Some(f) => + matches_exp( + ~denv=ClosureEnvironment.without_keys([dname], denv), + d, + ~fenv=ClosureEnvironment.without_keys([fname], fenv), + f, + ) + | ( + Some(Fun(_, _, _, Some(dname)) as d), + Some(Fun(_, _, _, Some(fname)) as f), + ) + when + ClosureEnvironment.lookup(denv, dname) == Some(d) + && ClosureEnvironment.lookup(fenv, fname) == Some(f) => + matches_exp( + ~denv=ClosureEnvironment.without_keys([dname], denv), + d, + ~fenv=ClosureEnvironment.without_keys([fname], fenv), + f, + ) + | ( + Some(Fun(_, _, _, Some(dname)) as d), + Some(Fun(_, _, _, Some(fname)) as f), + ) + when + ClosureEnvironment.lookup(denv, dname) == Some(d) + && ClosureEnvironment.lookup(fenv, fname) == Some(f) => matches_exp( ~denv=ClosureEnvironment.without_keys([dname], denv), d, From c418f38ddf064eca071898a5a6d671958529f010 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 22 Mar 2024 21:31:01 +0800 Subject: [PATCH 10/12] fix filter static --- src/haz3lcore/statics/Statics.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 1d1beb302b..5c73d96639 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -275,7 +275,7 @@ and uexp_to_info_map = let (e, m) = go(~mode=Ana(Bool), e, m); add(~self=Just(Prod([])), ~co_ctx=e.co_ctx, m); | Filter(_, cond, body) => - let (cond, m) = go(~mode, cond, m, ~is_in_filter=true); + let (cond, m) = go(~mode=Syn, cond, m, ~is_in_filter=true); let (body, m) = go(~mode, body, m); add( ~self=Just(body.ty), From 9388861968768eb2106a10ddf24d35e5d27b2c6a Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Thu, 18 Apr 2024 18:32:10 -0400 Subject: [PATCH 11/12] Update Elaborator.re --- src/haz3lcore/dynamics/Elaborator.re | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index e8c902f2e1..0d4894f962 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -126,7 +126,7 @@ let rec dhexp_of_uexp = dhexp_of_uexp(m, uexp, in_filter); }; switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { - | Some(InfoExp({mode, self, ctx, ancestors, _})) => + | Some(InfoExp({mode, self, ctx, ancestors, co_ctx, _})) => let err_status = Info.status_exp(ctx, mode, self); let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */ let+ d: DHExp.t = @@ -226,7 +226,12 @@ let rec dhexp_of_uexp = let* ddef = dhexp_of_uexp(m, def); let* dbody = dhexp_of_uexp(m, body); let+ ty = fixed_pat_typ(m, p); - if (!Statics.is_recursive(ctx, p, def, ty)) { + let is_recursive = + Statics.is_recursive(ctx, p, def, ty) + && Term.UPat.get_bindings(p) + |> Option.get + |> List.exists(f => VarMap.lookup(co_ctx, f) != None); + if (!is_recursive) { /* not recursive */ DHExp.Let( dp, From 41adb5104d7e4f18af360f425fb63a6108a2868c Mon Sep 17 00:00:00 2001 From: Cyrus Omar Date: Tue, 28 May 2024 13:34:48 -0400 Subject: [PATCH 12/12] fix test --- test/Test_Elaboration.re | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 98d1db0fdd..d584492091 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -258,15 +258,11 @@ let u9: Term.UExp.t = { let d9: DHExp.t = Let( Var("f"), - FixF( - "f", - Arrow(Int, Int), - Fun( - Var("x"), - Int, - BinIntOp(Plus, IntLit(1), BoundVar("x")), - Some("f+"), - ), + Fun( + Var("x"), + Int, + BinIntOp(Plus, IntLit(1), BoundVar("x")), + Some("f"), ), IntLit(55), );