refactor: use debug .. in for filter expression

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

src/haz3lcore/dynamics/FilterAction.re

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

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

@@ -100,6 +100,8 @@ 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 {
@@ -154,7 +156,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 +170,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 +204,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 +231,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 +403,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)) {

src/haz3lcore/dynamics/Stepper.re

@@ -36,7 +36,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) => {
@@ -52,19 +52,20 @@ let rec matches =
       | Closure(env, ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Closure(env, ctx) |> rewrap;
-      | Filter(Filter(flt'), ctx) =>
-        let flt = flt |> FilterEnvironment.extends(flt');
+      | Filter(Some(fact), fpat, ctx) =>
+        let flt = flt |> FilterEnvironment.extends({act: fact, pat: fpat});
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
-        Filter(Filter(flt'), ctx) |> rewrap;
-      | Filter(Residue(idx', act'), ctx) =>
+        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, Filter(Residue(idx', act'), rctx) |> rewrap);
+          (ract, ridx, Residue(idx', act', rctx) |> rewrap);
         } else {
           (ract, ridx, rctx);
         };
@@ -167,7 +168,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)
   };

src/haz3lcore/dynamics/Substitution.re

@@ -14,10 +14,23 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     let d3 = subst_var(m, d1, x, d3);
     let d4 = subst_var(m, d1, x, d4);
     Seq(d3, d4) |> rewrap;
-  | Filter(filter, dbody) =>
+  | Filter(None, pat, dbody) =>
+    let pat =
+      switch (pat.term) {
+      | Ap(direction, fn, arg) =>
+        let arg = subst_var(m, d1, x, arg);
+        {...pat, term: TermBase.Exp.Ap(direction, fn, arg)};
+      | _ => pat
+      };
+    let dbody = subst_var(m, d1, x, dbody);
+    Filter(None, pat, dbody) |> rewrap;
+  | Filter(Some(act), pat, dbody) =>
+    let pat = subst_var(m, d1, x, pat);
+    let dbody = subst_var(m, d1, x, dbody);
+    Filter(Some(act), pat, dbody) |> rewrap;
+  | Residue(idx, act, dbody) =>
     let dbody = subst_var(m, d1, x, dbody);
-    let filter = subst_var_filter(m, d1, x, filter);
-    Filter(filter, dbody) |> rewrap;
+    Residue(idx, act, dbody) |> rewrap;
   | Let(dp, d3, d4) =>
     let d3 = subst_var(m, d1, x, d3);
     let d4 =
@@ -159,12 +172,6 @@ and subst_var_env =
        );
 
   ClosureEnvironment.wrap(id, map);
-}
-
-and subst_var_filter =
-    (m, d1: DHExp.t, x: Var.t, flt: TermBase.StepperFilterKind.t)
-    : TermBase.StepperFilterKind.t => {
-  flt |> TermBase.StepperFilterKind.map(subst_var(m, d1, x));
 };
 
 let subst = (m, env: Environment.t, d: DHExp.t): DHExp.t =>

src/haz3lcore/dynamics/Transition.re

@@ -768,10 +768,23 @@ module Transition = (EV: EV_MODE) => {
     | TyAlias(_, _, d) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveTypeAlias, is_value: false});
-    | Filter(f1, d1) =>
-      let. _ = otherwise(env, d1 => Filter(f1, d1) |> rewrap)
+    | Filter(a1, p1, d1) =>
+      let. _ = otherwise(env, d1 => Filter(a1, p1, d1) |> rewrap)
       and. d1 =
-        req_final(req(state, env), d1 => Filter(f1, d1) |> wrap_ctx, d1);
+        req_final(
+          req(state, env),
+          d1 => Filter(a1, p1, d1) |> wrap_ctx,
+          d1,
+        );
+      Step({expr: d1, state_update, kind: CompleteFilter, is_value: true});
+    | Residue(a1, p1, d1) =>
+      let. _ = otherwise(env, d1 => Residue(a1, p1, d1) |> rewrap)
+      and. d1 =
+        req_final(
+          req(state, env),
+          d1 => Residue(a1, p1, d1) |> wrap_ctx,
+          d1,
+        );
       Step({expr: d1, state_update, kind: CompleteFilter, is_value: true});
     };
   };

src/haz3lcore/dynamics/TypeAssignment.re

@@ -132,7 +132,8 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
   | Closure(env, d) =>
     let* ctx' = env_extend_ctx(env, m, ctx);
     typ_of_dhexp(ctx', m, d);
-  | Filter(_, d) => typ_of_dhexp(ctx, m, d)
+  | Filter(_, _, d) => typ_of_dhexp(ctx, m, d)
+  | Residue(_, _, d) => typ_of_dhexp(ctx, m, d)
   | Var(name) =>
     let* var = Ctx.lookup_var(ctx, name);
     Some(var.typ);

src/haz3lcore/dynamics/Unboxing.re

@@ -185,6 +185,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         Seq(_) |
         Test(_) |
         Filter(_) |
+        Residue(_) |
         Closure(_) |
         Parens(_) |
         Cons(_) |

src/haz3lcore/lang/Form.re

@@ -318,11 +318,7 @@ let forms: list((string, t)) = [
     mk(ds, ["|", "=>"], mk_bin'(P.rule_sep, Rul, Exp, [Pat], Exp)),
   ),
   ("pipeline", mk_infix("|>", Exp, P.eqs)), // in OCaml, pipeline precedence is in same class as '=', '<', etc.
-  // DOUBLE DELIMITERS
-  ("filter_hide", mk(ds, ["hide", "in"], mk_pre(P.let_, Exp, [Exp]))),
-  ("filter_eval", mk(ds, ["eval", "in"], mk_pre(P.let_, Exp, [Exp]))),
-  ("filter_pause", mk(ds, ["pause", "in"], mk_pre(P.let_, Exp, [Exp]))),
-  ("filter_debug", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))),
+  ("filter", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))),
   // TRIPLE DELIMITERS
   ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))),
   (
@@ -332,8 +328,12 @@ let forms: list((string, t)) = [
   ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))),
 ];
 
-let get: String.t => t =
-  name => Util.ListUtil.assoc_err(name, forms, "Forms.get");
+let get: String.t => t = {
+  name => {
+    print_endline("Forms.get: name = " ++ name);
+    Util.ListUtil.assoc_err(name, forms, "Forms.get");
+  };
+};
 
 let delims: list(Token.t) =
   forms