From b28c2603456633445268f941d3543313ebc13b33 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 4 Oct 2024 16:29:02 +0800 Subject: [PATCH] fix: typing error for $e and $v --- src/haz3lcore/dynamics/EvaluatorStep.re | 16 -- src/haz3lcore/dynamics/EvaluatorStep.rei | 59 +++++++ src/haz3lcore/dynamics/FilterMatcher.re | 2 - src/haz3lcore/dynamics/Stepper.re | 178 --------------------- src/haz3lcore/statics/Statics.re | 10 +- src/haz3lweb/explainthis/data/FilterExp.re | 19 ++- src/haz3lweb/view/ExplainThis.re | 32 ++++ 7 files changed, 107 insertions(+), 209 deletions(-) create mode 100644 src/haz3lcore/dynamics/EvaluatorStep.rei diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index caff2caf63..d86417ec42 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -413,19 +413,3 @@ let should_hide_step = (~settings, x: step): (FilterAction.action, step) => let decompose = (~settings, d, st) => decompose(d, st) |> List.map(should_hide_eval_obj(~settings)); - -let evaluate_with_history = (~settings, d) => { - let state = ref(EvaluatorState.init); - let rec go = d => - switch (decompose(~settings, d, state^)) { - | [] => [] - | [(_, x), ..._] => - switch (take_step(state, x.env, x.d_loc)) { - | None => [] - | Some(d) => - let next = EvalCtx.compose(x.ctx, d); - [next, ...go(next)]; - } - }; - go(d); -}; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.rei b/src/haz3lcore/dynamics/EvaluatorStep.rei new file mode 100644 index 0000000000..71b1db2792 --- /dev/null +++ b/src/haz3lcore/dynamics/EvaluatorStep.rei @@ -0,0 +1,59 @@ +[@deriving (show({with_path: false}), sexp, yojson)] +type step = { + d: DHExp.t, // technically can be calculated from d_loc and ctx + state: EvaluatorState.t, + d_loc: DHExp.t, // the expression at the location given by ctx + d_loc': DHExp.t, + ctx: EvalCtx.t, + knd: Transition.step_kind, +}; + +module EvalObj: { + [@deriving (show({with_path: false}), sexp, yojson)] + type t = { + env: ClosureEnvironment.t, // technically can be calculated from ctx + d_loc: DHExp.t, + ctx: EvalCtx.t, + knd: Transition.step_kind, + }; + + let mk: + (EvalCtx.t, ClosureEnvironment.t, DHExp.t, Transition.step_kind) => t; + let get_ctx: t => EvalCtx.t; + let get_kind: t => Transition.step_kind; + let wrap: (EvalCtx.t => EvalCtx.t, t) => t; +}; + +let decompose: + (~settings: CoreSettings.Evaluation.t, DHExp.t, EvaluatorState.t) => + list((FilterAction.action, EvalObj.t)); + +module TakeStep: { + module TakeStepEVMode: { + include + Transition.EV_MODE with + type result = option(DHExp.t) and type state = ref(EvaluatorState.t); + }; +}; + +let take_step: + (TakeStep.TakeStepEVMode.state, ClosureEnvironment.t, DHExp.t) => + TakeStep.TakeStepEVMode.result; + +let matches: + ( + ClosureEnvironment.t, + FilterEnvironment.t, + EvalCtx.t, + DHExp.t, + FilterAction.t, + int + ) => + (FilterAction.t, int, EvalCtx.t); + +let should_hide_eval_obj: + (~settings: CoreSettings.Evaluation.t, EvalObj.t) => + (FilterAction.action, EvalObj.t); + +let should_hide_step: + (~settings: CoreSettings.Evaluation.t, step) => (FilterAction.action, step); diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 4e65071dc3..f5f69aac85 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -100,8 +100,6 @@ let rec matches_exp = : bool => { let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); - Printf.printf("d: %s\n", DHExp.show(d)); - Printf.printf("f: %s\n", DHExp.show(f)); if (d == f) { true; } else { diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index f1341493c3..6bed91b06e 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -21,184 +21,6 @@ type t = { stepper_state, }; -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 = EvalCtx.compose(ctx, exp); - let (pact, pidx) = (act, idx); - let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt); - let (act, idx) = - switch (ctx) { - | Term({term: Filter(_, _, _), _}) => (pact, pidx) - | _ => midx > pidx ? (mact, midx) : (pact, pidx) - }; - let map = ((a, i, c), f) => { - (a, i, f(c)); - }; - let (let+) = map; - let (ract, ridx, rctx) = - switch (ctx) { - | Mark => (act, idx, EvalCtx.Mark) - | Term({term, ids}) => - let rewrap = term => EvalCtx.Term({term, ids}); - switch ((term: EvalCtx.term)) { - | Closure(env, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Closure(env, ctx) |> rewrap; - | Filter(Some(fact), fpat, ctx) => - let flt = flt |> FilterEnvironment.extends({act: fact, pat: fpat}); - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Some(fact), fpat, ctx) |> rewrap; - | Filter(None, _, _) => failwith("Invalid filter expression") - | 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, Residue(idx', act', rctx) |> rewrap); - } else { - (ract, ridx, rctx); - }; - | Seq1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Seq1(ctx, d2) |> rewrap; - | Seq2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Seq2(d1, ctx) |> rewrap; - | Let1(d1, ctx, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Let1(d1, ctx, d3) |> rewrap; - | Let2(d1, d2, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Let2(d1, d2, ctx) |> rewrap; - | Fun(dp, ctx, env', name) => - let+ ctx = - matches(Option.value(~default=env, env'), flt, ctx, exp, act, idx); - Fun(dp, ctx, env', name) |> rewrap; - | FixF(name, ctx, env') => - let+ ctx = - matches(Option.value(~default=env, env'), flt, ctx, exp, act, idx); - FixF(name, ctx, env') |> rewrap; - | Ap1(dir, ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Ap1(dir, ctx, d2) |> rewrap; - | Ap2(dir, d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Ap2(dir, d1, ctx) |> rewrap; - | TypAp(ctx, ty) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - TypAp(ctx, ty) |> rewrap; - | DeferredAp1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DeferredAp1(ctx, d2) |> rewrap; - | DeferredAp2(d1, ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DeferredAp2(d1, ctx, ds) |> rewrap; - | If1(ctx, d2, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If1(ctx, d2, d3) |> rewrap; - | If2(d1, ctx, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If2(d1, ctx, d3) |> rewrap; - | If3(d1, d2, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If3(d1, d2, ctx) |> rewrap; - | UnOp(op, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - UnOp(op, ctx) |> rewrap; - | BinOp1(op, ctx, d1) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - BinOp1(op, ctx, d1) |> rewrap; - | BinOp2(op, d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - BinOp2(op, d1, ctx) |> rewrap; - | Tuple(ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Tuple(ctx, ds) |> rewrap; - | Test(ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Test(ctx) |> rewrap; - | ListLit(ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListLit(ctx, ds) |> rewrap; - | Cons1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cons1(ctx, d2) |> rewrap; - | Cons2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cons2(d1, ctx) |> rewrap; - | ListConcat1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListConcat1(ctx, d2) |> rewrap; - | ListConcat2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListConcat2(d1, ctx) |> rewrap; - | MultiHole(ctx, (dl, dr)) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MultiHole(ctx, (dl, dr)) |> rewrap; - | Cast(ctx, ty, ty') => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cast(ctx, ty, ty') |> rewrap; - | FailedCast(ctx, ty, ty') => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - FailedCast(ctx, ty, ty') |> rewrap; - | DynamicErrorHole(ctx, error) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DynamicErrorHole(ctx, error) |> rewrap; - | MatchScrut(ctx, rs) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MatchScrut(ctx, rs) |> rewrap; - | MatchRule(scr, p, ctx, rs) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MatchRule(scr, p, ctx, rs) |> rewrap; - }; - }; - switch (ctx) { - | Term({term: Filter(_), _}) => (ract, ridx, rctx) - | _ when midx > pidx && mact |> snd == All => ( - ract, - ridx, - Term({term: Residue(midx, mact, rctx), ids: [Id.mk()]}), - ) - | _ => (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 get_elab = ({history, _}: t): Elaborator.Elaboration.t => { let (d, _) = Aba.last_a(history); {d: d}; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index e8af1667fd..ffd2a5f377 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -281,7 +281,7 @@ and uexp_to_info_map = | _ => e.term }, }; - let ty_in = Typ.Var("$Meta") |> Typ.temp; + let ty_in = Typ.Unknown(Internal) |> Typ.temp; let ty_out = Typ.Unknown(Internal) |> Typ.temp; let (e, m) = go(~mode=Ana(ty_in), e, m); add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m); @@ -342,7 +342,7 @@ and uexp_to_info_map = let (fn, m) = go'(~ctx=Builtins.filter_keyword_ctx_init, ~mode=fn_mode, fn, m); let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); - let (arg, m) = go(~mode=Ana(ty_in), arg, m); + let (arg, m) = go(~mode=Ana(ty_in), arg, m, ~is_in_filter=true); let self: Self.t = Id.is_nullary_ap_flag(arg.term.ids) && !Typ.is_consistent(ctx, ty_in, Prod([]) |> Typ.temp) @@ -375,12 +375,6 @@ and uexp_to_info_map = let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn)); let (fn, m) = go(~mode=fn_mode, fn, m); let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); - Printf.printf("uexp_to_info_map: Ap: uexp = %s\n", UExp.show(uexp)); - Printf.printf( - "uexp_to_info_map: Ap: ty_in = %s, ty_out = %s\n", - Typ.show(ty_in), - Typ.show(ty_out), - ); let (arg, m) = go(~mode=Ana(ty_in), arg, m); let self: Self.t = Id.is_nullary_ap_flag(arg.term.ids) diff --git a/src/haz3lweb/explainthis/data/FilterExp.re b/src/haz3lweb/explainthis/data/FilterExp.re index 9e66a0b7fd..98dc073e4c 100644 --- a/src/haz3lweb/explainthis/data/FilterExp.re +++ b/src/haz3lweb/explainthis/data/FilterExp.re @@ -18,8 +18,9 @@ let filter_pause = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { examples: [ { sub_id: FilterStep, - term: mk_example("eval $e + $e in\n(1 + 2) * (3 + 4)"), - message: "The expression (1 * 2) + (3 * 4) is guarded by a pause filter expression pause $v + $v, which instruct the evaluator to pause the evaluation when it sees a value is added to another value. After evaluating subterms (1 * 2) and (3 * 4), the expression turns into 2 + 12. 2 matches the first $v pattern, and 12 matches the second $v pattern. Therefore, the evaluator stops when the expression steps to 2 + 12", + term: mk_example({|debug stop($v + $v) in +(1 + 2) * (3 + 4)|}), + message: "The expression (1 * 2) + (3 * 4) is guarded by a pause filter expression debug pause($v + $v), which instruct the evaluator to pause the evaluation when it sees a value is added to another value. After evaluating subterms (1 * 2) and (3 * 4), the expression turns into 2 + 12. 2 matches the first $v pattern, and 12 matches the second $v pattern. Therefore, the evaluator stops when the expression steps to 2 + 12", }, ], }; @@ -42,9 +43,13 @@ let filter_eval = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { sub_id: FilterEval, term: mk_example( - "pause $e in\nhide let = in in\nlet x = 1 in\nlet y = 2 in\nx + y", + {|debug stop($e) in +debug eval(let = in) in +let x = 1 in +let x = y in +x + y|}, ), - message: "pause $e in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression instructs the evaluator to skip over all evaluator steps that destructs perform substitution on a let-expression. Here, the substitution of variable x and y is skipped over and we directly got 1 + 2 in the result area.", + message: "debug stop($e) in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression debug eval(let = in) instructs the evaluator to evaluate all let-expressions. Here, the evaluation of the two let-expressions are skipped over, and we get the final answer 2 immediately.", }, ], }; @@ -67,7 +72,11 @@ let filter_hide = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { sub_id: FilterHide, term: mk_example( - "pause $e in\nhide let = in in\nlet x = 1 in\nlet y = 2 in\nx + y", + {|debug stop($e) in +debug hide(let = in) in +let x = 1 in +let y = 2 in +x + y|}, ), message: "pause $e in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression instructs the evaluator to skip over all evaluator steps that destructs perform substitution on a let-expression. Here, the substitution of variable x and y is skipped over and we directly got 1 + 2 in the result area.", }, diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index f6902276a0..5b9907c63a 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -1738,6 +1738,38 @@ let get_doc = ~body_id=UExp.rep_id(body), ), ) + | Filter(None, {term: Ap(_, {term: Var(var), _}, _), _} as pat, body) => + switch (var) { + | "stop" => + message_single( + FilterExp.filter_pause( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "step" => + message_single( + FilterExp.filter_debug( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "hide" => + message_single( + FilterExp.filter_hide( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "eval" => + message_single( + FilterExp.filter_eval( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | _ => simple("Internal expression") + } | Filter(None, _, _) | Residue(_) => simple("Internal expression") | Test(body) =>