fix: typing error for $e and $v

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);
-};

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);

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 {

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};

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)

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.",
     },

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) =>