projector API flag for dynamics collection

src/haz3lcore/prog/Dynamics.re

@@ -103,7 +103,7 @@ module Probe = {
 
   /* Intercepts a probe form and adds in static semantic information
    * to guide dynamic information gathering  */
-  let instrument =
+  let instrument_exp =
       (m: Statics.Map.t, id: Id.t, probe_tag: Probe.tag): Probe.tag =>
     switch (probe_tag) {
     | Paren => Paren

src/haz3lcore/statics/Elaborator.re

@@ -243,7 +243,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       e' |> cast_from(ty);
     | Parens(e, probe) =>
       let (e', ty) = elaborate(m, e);
-      let probe = Dynamics.Probe.instrument(m, Exp.rep_id(uexp), probe);
+      let probe = Dynamics.Probe.instrument_exp(m, Exp.rep_id(uexp), probe);
       Parens(e' |> cast_from(ty), probe) |> rewrap;
     | Deferral(_) => uexp
     | Int(_) => uexp |> cast_from(Int |> Typ.temp)

src/haz3lcore/statics/MakeTerm.re

@@ -127,6 +127,17 @@ let log_projector = (pr: Base.projector): unit => {
   projectors := Id.Map.add(pr.id, pr, projectors^);
 };
 
+/* Check if a term should be instrumented with a probe.
+ * Precondition: The relevant projector must have been
+ * logged before this is called */
+let should_instrument = (id: Id.t): bool =>
+  switch (Id.Map.find_opt(id, projectors^)) {
+  | Some(pr) =>
+    let (module P) = Projector.to_module(pr.kind);
+    P.dynamics;
+  | None => failwith("MakeTerm.exp: projector not found")
+  };
+
 let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) =
   fun
   | {term: Var(ctr), ids, _} => Variant(ctr, ids, None)
@@ -197,7 +208,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
       | (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren))
       | (label, [Exp(body)]) when is_probe_wrap(label) =>
         // Temporary wrapping form to persist projector probes
-        ret(Parens(body, Probe(Probe.empty)))
+        ret(
+          should_instrument(Exp.rep_id(body))
+            ? Parens(body, Probe(Probe.empty)) : body.term,
+        )
       | (["[", "]"], [Exp(body)]) =>
         switch (body) {
         | {ids, copied: false, term: Tuple(es)} => (ListLit(es), ids)
@@ -361,7 +375,8 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
           Invalid(t)
         | (["(", ")"], [Pat(body)]) => Parens(body, Paren)
         | (label, [Pat(body)]) when is_probe_wrap(label) =>
-          Parens(body, Probe(Probe.empty))
+          should_instrument(Pat.rep_id(body))
+            ? Parens(body, Probe(Probe.empty)) : body.term
         | (["[", "]"], [Pat(body)]) =>
           switch (body) {
           | {term: Tuple(ps), _} => ListLit(ps)
@@ -536,7 +551,7 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
     switch (p) {
     | Secondary(_)
     | Grout(_) => []
-    | Projector({syntax, id: _, _} as pr) =>
+    | Projector({syntax, _} as pr) =>
       let _ = log_projector(pr);
       let sort = Piece.sort(syntax) |> fst;
       [go_s(sort, Segment.skel([syntax]), [syntax])];

src/haz3lcore/zipper/ProjectorBase.re

@@ -100,6 +100,10 @@ module type Projector = {
    * and has two callbacks: ~parent for parent editor
    * actions(see external_action type above), and ~local
    * for this projector's local update function. */
+  let dynamics: bool;
+  /* If dynamics is true, this projector will be
+   * instrumented with a probe to collect dynamic
+   * information during evaluation */
   let view:
     (
       model,
@@ -146,6 +150,7 @@ module Cook = (C: Projector) : Cooked => {
   let init = C.init |> serialize_m;
   let can_project = C.can_project;
   let can_focus = C.can_focus;
+  let dynamics = C.dynamics;
   let view = (m, ~info, ~local, ~parent, ~utility) =>
     C.view(
       deserialize_m(m),

src/haz3lcore/zipper/projectors/CheckboxProj.re

@@ -52,6 +52,7 @@ module M: Projector = {
   let init = ();
   let can_project = p => state_of(p) != None;
   let can_focus = false;
+  let dynamics = false;
   let placeholder = (_, _) => Inline(2);
   let update = (model, _) => model;
   let view = view;

src/haz3lcore/zipper/projectors/FoldProj.re

@@ -17,6 +17,7 @@ module M: Projector = {
   let init = {text: "⋱"};
   let can_project = _ => true;
   let can_focus = false;
+  let dynamics = false;
   let placeholder = (m, _) =>
     Inline(m.text == "⋱" ? 2 : m.text |> String.length);
   let update = (m, _) => m;

src/haz3lcore/zipper/projectors/InfoProj.re

@@ -49,6 +49,7 @@ module M: Projector = {
   };
 
   let can_focus = false;
+  let dynamics = false;
 
   let display_ty = (model, info) =>
     switch (model) {

src/haz3lcore/zipper/projectors/ProbeProj.re

@@ -198,8 +198,8 @@ let rm_opaques:
 
 /* Is the underlying syntax a variable reference? */
 let is_var_ref = (info: info): bool =>
-  switch (MakeTerm.go([info.syntax]).term.term) {
-  | Var(_) => true
+  switch (info.statics) {
+  | Some(InfoExp({term: {term: Var(_), _}, _})) => true
   | _ => false
   };
 
@@ -372,6 +372,7 @@ module M: Projector = {
   let init = init;
   let can_project = _ => true;
   let can_focus = false;
+  let dynamics = true;
   let placeholder = placeholder;
   let update = update;
   let view = view;

src/haz3lcore/zipper/projectors/SliderFProj.re

@@ -24,6 +24,7 @@ module M: Projector = {
   let init = ();
   let can_project = p => get_opt(p) != None;
   let can_focus = false;
+  let dynamics = false;
   let placeholder = (_, _) => Inline(10);
   let update = (model, _) => model;
   let view =

src/haz3lcore/zipper/projectors/SliderProj.re

@@ -21,6 +21,7 @@ module M: Projector = {
   let init = ();
   let can_project = p => get_opt(p) != None;
   let can_focus = false;
+  let dynamics = false;
   let placeholder = (_, _) => Inline(10);
   let update = (model, _) => model;
   let view =

src/haz3lcore/zipper/projectors/TextAreaProj.re

@@ -98,6 +98,7 @@ module M: Projector = {
   let init = ();
   let can_project = _ => true; //TODO(andrew): restrict somehow
   let can_focus = true;
+  let dynamics = false;
   let placeholder = (_, info) => {
     let str = Form.strip_quotes(get(info.syntax));
     Block({