probe projectors on patterns

src/haz3lcore/dynamics/DHPat.re

@@ -22,7 +22,7 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool =>
     | String(_)
     | Constructor(_) => false
     | Cast(y, _, _)
-    | Parens(y) => binds_var(m, x, y)
+    | Parens(y, _) => binds_var(m, x, y)
     | Var(y) => Var.eq(x, y)
     | Tuple(dps) => dps |> List.exists(binds_var(m, x))
     | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)

src/haz3lcore/dynamics/PatternMatch.re

@@ -11,6 +11,23 @@ let combine_result = (r1: match_result, r2: match_result): match_result =>
     Matches(Environment.union(env1, env2))
   };
 
+let closure_closures:
+  ref(list(Probe.stack => (Id.t, Dynamics.Probe.Closure.t))) =
+  ref([]);
+
+let capture_closure = (pr, id: Id.t, d, inner_match: match_result): unit =>
+  switch (inner_match) {
+  | DoesNotMatch => ()
+  | IndetMatch => ()
+  | Matches(env) =>
+    print_endline("Pattern Match: capturing a closure");
+    closure_closures :=
+      List.cons(
+        stack => (id, Dynamics.Probe.Closure.mk(d, {env, stack, id}, pr)),
+        closure_closures^,
+      );
+  };
+
 let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
   switch (DHPat.term_of(dp)) {
   | Invalid(_)
@@ -49,12 +66,36 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
     let* d2 = Unboxing.unbox(SumWithArg(ctr), d);
     matches(p2, d2);
   | Ap(_, _) => IndetMatch // TODO: should this fail?
-  | Var(x) => Matches(Environment.singleton((x, d)))
+  | Var(x) =>
+    print_endline(
+      "id of pat var "
+      ++ x
+      ++ " being bound to d:"
+      ++ Id.to_string(IdTagged.rep_id(dp)),
+    );
+    Matches(Environment.singleton((x, d)));
   | Tuple(ps) =>
     let* ds = Unboxing.unbox(Tuple(List.length(ps)), d);
     List.map2(matches, ps, ds)
     |> List.fold_left(combine_result, Matches(Environment.empty));
-  | Parens(p) => matches(p, d)
+  | Parens(p, Paren) => matches(p, d)
+  | Parens(p, Probe(pr)) =>
+    print_endline("Pattern Match: found pattern probe");
+    let inner_match = matches(p, d);
+    capture_closure(pr, Term.Pat.rep_id(dp), d, inner_match);
+    inner_match;
   | Cast(p, t1, t2) =>
     matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple)
   };
+
+type matches_and_closures = {
+  matches: match_result,
+  closures: list(Probe.stack => (Id.t, Dynamics.Probe.Closure.t)),
+};
+
+// wrap matches but do stateful thing (closure capture)
+let matches = (dp: Pat.t, d: DHExp.t): matches_and_closures => {
+  closure_closures := [];
+  let res = matches(dp, d);
+  {matches: res, closures: closure_closures^};
+};

src/haz3lcore/dynamics/Transition.re

@@ -149,6 +149,16 @@ module Transition = (EV: EV_MODE) => {
     | Matches(env') => r(evaluate_extend_env(env', env))
     };
 
+  let capture_closures =
+      (env: ClosureEnvironment.t, state: state, closures, ()): unit =>
+    List.iter(
+      closure => {
+        let (id, closure: Dynamics.Probe.Closure.t) = closure(env.stack);
+        update_probe(state, id, closure);
+      },
+      closures,
+    );
+
   /* Note[Matt]: For IDs, I'm currently using a fresh id
      if anything about the current node changes, if only its
      children change, we use rewrap */
@@ -181,10 +191,11 @@ module Transition = (EV: EV_MODE) => {
       let. _ = otherwise(env, d1 => Let(dp, d1, d2) |> rewrap)
       and. d1' =
         req_final(req(state, env), d1 => Let1(dp, d1, d2) |> wrap_ctx, d1);
-      let.match env' = (env, matches(dp, d1'));
+      let {matches, closures} = matches(dp, d1');
+      let.match env' = (env, matches);
       Step({
         expr: Closure(env', d2) |> fresh,
-        state_update,
+        state_update: capture_closures(env, state, closures),
         kind: LetBind,
         is_value: false,
       });
@@ -341,7 +352,9 @@ module Transition = (EV: EV_MODE) => {
       switch (DHExp.term_of(d1')) {
       | Constructor(_) => Constructor
       | Fun(dp, d3, Some(env'), _) =>
-        switch (matches(dp, d2')) {
+        let matches = matches(dp, d2');
+
+        switch (matches.matches) {
         | IndetMatch
         | DoesNotMatch => Indet
         | Matches(env'') =>
@@ -353,11 +366,11 @@ module Transition = (EV: EV_MODE) => {
             );
           Step({
             expr: Closure(env'', d3) |> fresh,
-            state_update,
+            state_update: capture_closures(env, state, matches.closures),
             kind: FunAp,
             is_value: false,
           });
-        }
+        };
       | Cast(
           d3',
           {term: Arrow(ty1, ty2), _},
@@ -719,18 +732,20 @@ module Transition = (EV: EV_MODE) => {
       let rec next_rule = (
         fun
         | [] => None
-        | [(dp, d2), ...rules] =>
-          switch (matches(dp, d1)) {
-          | Matches(env') => Some((env', d2))
-          | DoesNotMatch => next_rule(rules)
-          | IndetMatch => None
+        | [(dp, d2), ...rules] => {
+            let matches = matches(dp, d1);
+            switch (matches.matches) {
+            | Matches(env') => Some((env', d2, matches.closures))
+            | DoesNotMatch => next_rule(rules)
+            | IndetMatch => None
+            };
           }
       );
       switch (next_rule(rules)) {
-      | Some((env', d2)) =>
+      | Some((env', d2, closures)) =>
         Step({
           expr: Closure(evaluate_extend_env(env', env), d2) |> fresh,
-          state_update,
+          state_update: capture_closures(env, state, closures),
           kind: CaseApply,
           is_value: false,
         })

src/haz3lcore/dynamics/TypeAssignment.re

@@ -64,7 +64,7 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
     | Wild
     | Invalid(_)
     | MultiHole(_) => Some([])
-    | Parens(dhp) => dhpat_var_entry(dhp, ty)
+    | Parens(dhp, _) => dhpat_var_entry(dhp, ty)
     | Int(_) => Typ.eq(ty, Int |> Typ.temp) ? Some([]) : None
     | Float(_) => Typ.eq(ty, Float |> Typ.temp) ? Some([]) : None
     | Bool(_) => Typ.eq(ty, Bool |> Typ.temp) ? Some([]) : None
@@ -98,7 +98,7 @@ let rec dhpat_synthesize = (dhpat: DHPat.t, ctx: Ctx.t): option(Typ.t) => {
   | Wild => Some(Unknown(Internal) |> Typ.temp)
   | Invalid(_)
   | MultiHole(_) => Some(Unknown(Internal) |> Typ.temp)
-  | Parens(dhp) => dhpat_synthesize(dhp, ctx)
+  | Parens(dhp, _) => dhpat_synthesize(dhp, ctx)
   | Int(_) => Some(Int |> Typ.temp)
   | Float(_) => Some(Float |> Typ.temp)
   | Bool(_) => Some(Bool |> Typ.temp)

src/haz3lcore/pretty/ExpToSegment.re

@@ -518,7 +518,7 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
     @ List.flatten(
         List.map2((id, x) => [mk_form("comma_pat", id, [])] @ x, ids, xs),
       );
-  | Parens(p) =>
+  | Parens(p, _) =>
     let id = pat |> Pat.rep_id;
     let+ p = go(p);
     [mk_form("parens_pat", id, [p])];
@@ -778,12 +778,12 @@ let paren_assoc_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
 
 let paren_pat_at = (internal_precedence: Precedence.t, pat: Pat.t): Pat.t =>
   external_precedence_pat(pat) >= internal_precedence
-    ? Pat.fresh(Parens(pat)) : pat;
+    ? Pat.fresh(Parens(pat, Paren)) : pat;
 
 let paren_pat_assoc_at =
     (internal_precedence: Precedence.t, pat: Pat.t): Pat.t =>
   external_precedence_pat(pat) > internal_precedence
-    ? Pat.fresh(Parens(pat)) : pat;
+    ? Pat.fresh(Parens(pat, Paren)) : pat;
 
 let paren_typ_at = (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
   external_precedence_typ(typ) >= internal_precedence
@@ -979,8 +979,9 @@ and parenthesize_pat = (pat: Pat.t): Pat.t => {
 
   // Other forms
   | Wild => pat
-  | Parens(p) =>
-    Parens(parenthesize_pat(p) |> paren_pat_at(Precedence.min)) |> rewrap
+  | Parens(p, tag) =>
+    Parens(parenthesize_pat(p) |> paren_pat_at(Precedence.min), tag)
+    |> rewrap
   | Cons(p1, p2) =>
     Cons(
       parenthesize_pat(p1) |> paren_pat_at(Precedence.cons),

src/haz3lcore/prog/Dynamics.re

@@ -32,32 +32,29 @@ module Probe = {
     /* Selectively elide dynamic information not currently
      * being used in the live probe UI, for (putative, unbenchmarked)
      * performance purposes for worker de/serialization */
-    let elide = (env: ClosureEnvironment.t, d: DHExp.t) =>
+    let elide = (env: Environment.t, d: DHExp.t) =>
       switch (d.term) {
       | Fun(_)
       | FixF(_) => Opaque
-      | _ =>
-        Val(
-          d
-          |> DHExp.strip_casts
-          |> Exp.substitute_closures(ClosureEnvironment.map_of(env)),
-        )
+      | _ => Val(d |> DHExp.strip_casts |> Exp.substitute_closures(env))
       };
 
-    let mk_entry = (env: ClosureEnvironment.t, {name, id, _}: Binding.t) =>
-      switch (ClosureEnvironment.lookup(env, name)) {
+    let mk_entry = (env: Environment.t, {name, id, _}: Binding.t) =>
+      switch (Environment.lookup(env, name)) {
       | Some(d) => {
           binding: {
             name,
             id,
           },
           value: elide(env, d),
         }
-      | None => failwith("Probe: variable not found in environment")
+      | None =>
+        print_endline("binding:" ++ name);
+        failwith("Probe: variable not found in environment");
       };
 
-    let mk = (env: ClosureEnvironment.t, refs: Binding.s) =>
-      List.map(mk_entry(env), refs);
+    let mk = (env: Environment.t, bound_in: Binding.s) =>
+      List.map(mk_entry(env), bound_in);
   };
 
   /* A probe closure records an elided value and environment,
@@ -77,7 +74,7 @@ module Probe = {
       closure_id: Id.mk(),
       value,
       stack: ClosureEnvironment.stack_of(env),
-      env: Env.mk(env, pr.refs),
+      env: Env.mk(ClosureEnvironment.map_of(env), pr.refs),
     };
   };
 
@@ -114,6 +111,17 @@ module Probe = {
         stem: Statics.Map.enclosing_abstractions(m, id),
       })
     };
+
+  let instrument_pat =
+      (m: Statics.Map.t, id: Id.t, probe_tag: Probe.tag): Probe.tag =>
+    switch (probe_tag) {
+    | Paren => Paren
+    | Probe(_) =>
+      Probe({
+        refs: Statics.Map.bound_in(m, id),
+        stem: Statics.Map.enclosing_abstractions(m, id),
+      })
+    };
 };
 
 module Info = {

src/haz3lcore/statics/Elaborator.re

@@ -160,11 +160,15 @@ let rec elaborate_pattern =
               )
            |> Option.value(~default=Typ.temp(Unknown(Internal))),
          )
-    // Type annotations should already appear
-    | Parens(p)
+    // Type annotations should already appeard
+    | Parens(p, Paren)
     | Cast(p, _, _) =>
       let (p', ty) = elaborate_pattern(m, p);
       p' |> cast_from(ty |> Typ.normalize(ctx) |> Typ.all_ids_temp);
+    | Parens(p, probe) =>
+      let (e', ty) = elaborate_pattern(m, p);
+      let probe = Dynamics.Probe.instrument_pat(m, Pat.rep_id(upat), probe);
+      Parens(e' |> cast_from(ty), probe) |> rewrap;
     | Constructor(c, _) =>
       let mode =
         switch (Id.Map.find_opt(Pat.rep_id(upat), m)) {

src/haz3lcore/statics/MakeTerm.re

@@ -359,8 +359,9 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
           Constructor(t, Unknown(Internal) |> Typ.fresh)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Invalid(t)
-        | (["(", ")"], [Pat(body)]) => Parens(body)
-        | (label, [Pat(body)]) when is_probe_wrap(label) => body.term
+        | (["(", ")"], [Pat(body)]) => Parens(body, Paren)
+        | (label, [Pat(body)]) when is_probe_wrap(label) =>
+          Parens(body, Probe(Probe.empty))
         | (["[", "]"], [Pat(body)]) =>
           switch (body) {
           | {term: Tuple(ps), _} => ListLit(ps)

src/haz3lcore/statics/Statics.re

@@ -79,6 +79,12 @@ module Map = {
       |> List.map(((n, _)) => Ctx.binding_of(ctx, n))
     | _ => []
     };
+
+  let bound_in = (m: t, id: Id.t): Binding.s =>
+    switch (lookup(id, m)) {
+    | Some(InfoPat({term, _})) => Term.Pat.bindings(term)
+    | _ => []
+    };
 };
 
 let map_m = (f, xs, m: Map.t) =>
@@ -834,7 +840,12 @@ and upat_to_info_map =
       ~constraint_=cons_fold_tuple(cons),
       m,
     );
-  | Parens(p) =>
+  | Parens(p, Probe(_)) =>
+    /* Currently doing this as otherwise it clobbers the statics
+     * for the contained expression as i'm just reusing the same id
+     * in order to associate it through dynamics */
+    go(~ctx, ~mode, p, m)
+  | Parens(p, Paren) =>
     let (p, m) = go(~ctx, ~mode, p, m);
     add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
   | Constructor(ctr, _) =>