refactor: use debug .. in for filter expression

src/haz3lcore/dynamics/Builtins.re

@@ -371,6 +371,25 @@ let ctx_init: Ctx.t = {
   |> Ctx.add_ctrs(_, "$Meta", Id.invalid, meta_cons_map);
 };
 
+let filter_keyword_ctx_init: Ctx.t = {
+  let impl = _ => failwith("evaluating filter keyword");
+  Pervasives.builtins
+  |> fn("eval", Unknown(Internal), Filter, impl)
+  |> fn("hide", Unknown(Internal), Filter, impl)
+  |> fn("stop", Unknown(Internal), Filter, impl)
+  |> fn("step", Unknown(Internal), Filter, impl)
+  |> List.map(
+       fun
+       | (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid})
+       | (name, Fn(t1, t2, _)) =>
+         Ctx.VarEntry({
+           name,
+           typ: Arrow(t1, t2) |> Typ.fresh,
+           id: Id.invalid,
+         }),
+     );
+};
+
 let forms_init: forms =
   List.filter_map(
     fun

src/haz3lcore/dynamics/Casts.re

@@ -58,6 +58,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
+  | Filter
   | Var(_)
   | Rec(_)
   | Forall(_, {term: Unknown(_), _})

src/haz3lcore/dynamics/DHExp.re

@@ -51,6 +51,7 @@ let rec strip_casts =
         | MultiHole(_)
         | Seq(_)
         | Filter(_)
+        | Residue(_)
         | Let(_)
         | FixF(_)
         | TyAlias(_)
@@ -129,6 +130,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Match(_)
           | DynamicErrorHole(_)
           | Filter(_)
+          | Residue(_)
           | If(_)
           | EmptyHole
           | Invalid(_)

src/haz3lcore/dynamics/Elaborator.re

@@ -385,14 +385,27 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       Test(fresh_cast(e', t, Bool |> Typ.temp))
       |> rewrap
       |> cast_from(Prod([]) |> Typ.temp);
-    | Filter(kind, e) =>
+    | Filter(_, p, e) =>
+      switch (p.term) {
+      | Ap(_, {term: Var(name), _}, arg) =>
+        switch (FilterAction.t_of_string(name)) {
+        | Some(act) =>
+          let (e', t) = elaborate(m, e);
+          let (p', _) = elaborate(m, arg);
+          Filter(Some(act), p', e') |> rewrap |> cast_from(t);
+        | None =>
+          let (e', t) = elaborate(m, e);
+          let (p', _) = elaborate(m, p);
+          Filter(None, p', e') |> rewrap |> cast_from(t);
+        }
+      | _ =>
+        let (e', t) = elaborate(m, e);
+        let (p', _) = elaborate(m, p);
+        Filter(None, p', e') |> rewrap |> cast_from(t);
+      }
+    | Residue(i, a, e) =>
       let (e', t) = elaborate(m, e);
-      let kind' =
-        switch (kind) {
-        | Residue(_) => kind
-        | Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst})
-        };
-      Filter(kind', e') |> rewrap |> cast_from(t);
+      Residue(i, a, e') |> rewrap |> cast_from(t);
     | Closure(env, e) =>
       // Should we be elaborating the contents of the environment?
       let (e', t) = elaborate(m, e);

src/haz3lcore/dynamics/EvalCtx.re

@@ -3,7 +3,8 @@ open Util;
 [@deriving (show({with_path: false}), sexp, yojson)]
 type term =
   | Closure([@show.opaque] ClosureEnvironment.t, t)
-  | Filter(TermBase.StepperFilterKind.t, t)
+  | Filter(option(FilterAction.t), DHExp.t, t)
+  | Residue(int, FilterAction.t, t)
   | Seq1(t, DHExp.t)
   | Seq2(DHExp.t, t)
   | Let1(Pat.t, t, DHExp.t)
@@ -56,9 +57,12 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
       | Closure(env, ctx) =>
         let d = compose(ctx, d);
         Closure(env, d) |> wrap;
-      | Filter(flt, ctx) =>
+      | Filter(act, pat, ctx) =>
         let d = compose(ctx, d);
-        Filter(flt, d) |> wrap;
+        Filter(act, pat, d) |> wrap;
+      | Residue(idx, act, ctx) =>
+        let d = compose(ctx, d);
+        Residue(idx, act, d) |> wrap;
       | Seq1(ctx, d2) =>
         let d1 = compose(ctx, d);
         Seq(d1, d2) |> wrap;

src/haz3lcore/dynamics/EvaluatorStep.re

@@ -227,7 +227,7 @@ let rec matches =
   let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt);
   let (act, idx) =
     switch (ctx) {
-    | Term({term: Filter(_, _), _}) => (pact, pidx)
+    | Term({term: Filter(_, _, _), _}) => (pact, pidx)
     | _ => midx > pidx ? (mact, midx) : (pact, pidx)
     };
   let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => {
@@ -243,11 +243,14 @@ let rec matches =
       | Closure(env, ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Closure(env, ctx) |> wrap_ids(ids);
-      | Filter(Filter(flt'), ctx) =>
-        let flt = flt |> FilterEnvironment.extends(flt');
+      | Filter(Some(fact), pat, ctx) =>
+        let flt = flt |> FilterEnvironment.extends({act: fact, pat});
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
-        Filter(Filter(flt'), ctx) |> wrap_ids(ids);
-      | Filter(Residue(idx', act'), ctx) =>
+        Filter(Some(fact), pat, ctx) |> wrap_ids(ids);
+      | Filter(fact, pat, ctx) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Filter(fact, pat, ctx) |> wrap_ids(ids);
+      | Residue(idx', act', ctx) =>
         let (ract, ridx, rctx) =
           if (idx > idx') {
             matches(env, flt, ctx, exp, act, idx);
@@ -258,10 +261,7 @@ let rec matches =
           (
             ract,
             ridx,
-            Term({
-              term: Filter(Residue(idx', act'), rctx),
-              ids: [Id.mk()],
-            }),
+            Term({term: Residue(idx', act', rctx), ids: [Id.mk()]}),
           );
         } else {
           (ract, ridx, rctx);
@@ -380,7 +380,7 @@ let rec matches =
   | _ when midx > pidx && mact |> snd == All => (
       ract,
       ridx,
-      Term({term: Filter(Residue(midx, mact), rctx), ids: [Id.mk()]}),
+      Term({term: Residue(midx, mact, rctx), ids: [Id.mk()]}),
     )
   | _ => (ract, ridx, rctx)
   };
@@ -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/FilterAction.re

@@ -11,10 +11,20 @@ type count =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = (action, count);
 
+let t_of_string = s => {
+  switch (s) {
+  | "stop" => Some((Step, One))
+  | "step" => Some((Step, All))
+  | "hide" => Some((Eval, One))
+  | "eval" => Some((Eval, All))
+  | _ => None
+  };
+};
+
 let string_of_t = v => {
   switch (v) {
-  | (Step, One) => "pause"
-  | (Step, All) => "debug"
+  | (Step, One) => "stop"
+  | (Step, All) => "step"
   | (Eval, One) => "hide"
   | (Eval, All) => "eval"
   };

src/haz3lcore/dynamics/FilterEnvironment.re

@@ -1,2 +1,9 @@
-type t = list(TermBase.StepperFilterKind.filter);
-let extends = (flt, env) => [flt, ...env];
+type filter = {
+  act: FilterAction.t,
+  pat: Exp.t,
+};
+type t = list(filter);
+let extends = (flt: filter, env: list(filter)): list(filter) => [
+  flt,
+  ...env,
+];

src/haz3lcore/dynamics/FilterMatcher.re

@@ -154,7 +154,12 @@ let rec matches_exp =
     | (_, EmptyHole)
     | (_, Constructor("$e", _)) => true
 
-    | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f)
+    | (Cast(d, dty1, dty2), Cast(f, fty1, fty2)) =>
+      matches_exp(d, f)
+      && matches_typ(dty1, fty1)
+      && matches_typ(dty2, fty2)
+    | (Cast(_), _) => false
+
     | (Closure(denv, d), Closure(fenv, f)) =>
       matches_exp(~denv, d, ~fenv, f)
 
@@ -163,9 +168,8 @@ let rec matches_exp =
     | (_, 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)
+    | (Residue(_, _, d), _) => matches_exp(d, f)
 
     | (Var(dx), Var(fx)) =>
       if (String.starts_with(~prefix=alpha_magic, dx)
@@ -198,8 +202,8 @@ let rec matches_exp =
     | (Deferral(x), Deferral(y)) => x == y
     | (Deferral(_), _) => false
 
-    | (Filter(df, dd), Filter(ff, fd)) =>
-      TermBase.StepperFilterKind.fast_equal(df, ff) && matches_exp(dd, fd)
+    | (Filter(da, dp, dd), Filter(fa, fp, fd)) =>
+      da == fa && matches_exp(dp, fp) && matches_exp(dd, fd)
     | (Filter(_), _) => false
 
     | (Bool(dv), Bool(fv)) => dv == fv
@@ -225,8 +229,15 @@ let rec matches_exp =
     | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn
     | (BuiltinFun(_), _) => false
 
-    | (TypFun(pat1, d1, s1), TypFun(pat2, d2, s2)) =>
-      s1 == s2 && matches_utpat(pat1, pat2) && matches_exp(d1, d2)
+    | (TypFun(dpat, d, _), TypFun(fpat, f, _)) =>
+      switch (dpat |> IdTagged.term_of, fpat |> IdTagged.term_of) {
+      | (_, EmptyHole) => matches_exp(d, f)
+      | _ =>
+        let id = alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4));
+        let d' = DHExp.ty_subst(Typ.Var(id) |> IdTagged.fresh, dpat, d);
+        let f' = DHExp.ty_subst(Typ.Var(id) |> IdTagged.fresh, fpat, f);
+        matches_exp(d', f');
+      }
     | (TypFun(_), _) => false
 
     | (Fun(dp1, d1, Some(denv), _), Fun(fp1, f1, Some(fenv), _)) =>
@@ -390,7 +401,7 @@ let matches =
     (
       ~env: ClosureEnvironment.t,
       ~exp: DHExp.t,
-      ~flt: TermBase.StepperFilterKind.filter,
+      ~flt: FilterEnvironment.filter,
     )
     : option(FilterAction.t) =>
   if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) {