clean up live projectors maketerm

src/haz3lcore/dynamics/Probe.re

@@ -1,5 +1,13 @@
 open Util;
 
+/* A syntax probe is inserted into syntax to capture
+ * information during evaluation. The tag type below,
+ * for the probe case, is used to collect binding ids
+ * which are used to faciltate capturing the values
+ * of certain variables in the environment. This captured
+ * information is, for a given closure, encoded in
+ * the `frame` type. */
+
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = {
   refs: Binding.s,
@@ -11,15 +19,25 @@ type tag =
   | Paren
   | Probe(t);
 
+/* Information about the evaluation of an ap */
 [@deriving (show({with_path: false}), sexp, yojson)]
 type frame = {
-  env_id: Id.t,
-  frame_id: Id.t,
+  closure_id: Id.t, /* Primary ID (Unique) */
+  ap_id: Id.t, /* Syntax ID of the ap */
+  env_id: Id.t /* ID of ClosureEnv created by ap  */
 };
 
+/* List of applications prior to some evaluation */
 [@deriving (show({with_path: false}), sexp, yojson)]
 type stack = list(frame);
 
-let empty = {refs: [], stem: []};
+let empty: t = {refs: [], stem: []};
+
+let env_stack: list(frame) => list(Id.t) =
+  List.map((en: frame) => en.env_id);
 
-let env_stack = List.map((en: frame) => en.env_id);
+let mk_frame = (~env_id: Id.t, ~ap_id: Id.t): frame => {
+  closure_id: Id.mk(),
+  env_id,
+  ap_id,
+};

src/haz3lcore/statics/MakeTerm.re

@@ -13,13 +13,23 @@
 open Util;
 open Any;
 
+/* Hack: Temporary construct internal to maketerm
+ * to handle probe parsing; see `tokens` below */
+let probe_wrap = ["@@@@@", "@@@@@"];
+let is_probe_wrap = (==)(probe_wrap);
+
 // TODO make less hacky
 let tokens =
   Piece.get(
     _ => [],
     _ => [" "],
     (t: Tile.t) => t.shards |> List.map(List.nth(t.label)),
-    _ => [],
+    _ =>
+      /* Hack: These act as temporary wrappers for projectors,
+       * which are retained through maketerm so as to be used in
+       * dynamics. These are inserted and removed entirely internal
+       * to maketerm. */
+      probe_wrap,
   );
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -112,21 +122,13 @@ let return = (wrap, ids, tm) => {
 /* Map to collect projector ids */
 let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty);
 
-/* Temporary form to persist projector dynamics probe to segments */
-let mk_probe = (id, e: list(Piece.t)) =>
-  Piece.mk_tile_id(
-    id,
-    Form.mk(Form.ii, ["@@", "@@"], Mold.mk_op(Exp, [Exp])),
-    [e],
-  );
-
 /* Strip a projector from a segment and log it in the map */
-let rm_and_log_projectors = (seg: Segment.t): Segment.t =>
+let log_projectors = (seg: Segment.t): Segment.t =>
   List.map(
     fun
     | Piece.Projector(pr) => {
         projectors := Id.Map.add(pr.id, pr, projectors^);
-        mk_probe(pr.id, [pr.syntax]);
+        Piece.Projector(pr);
       }
     | x => x,
     seg,
@@ -200,7 +202,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
       | ([t], []) when Form.is_ctr(t) =>
         ret(Constructor(t, Unknown(Internal) |> Typ.temp))
       | (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren))
-      | (["@@", "@@"], [Exp(body)]) =>
+      | (label, [Exp(body)]) when is_probe_wrap(label) =>
         // Temporary wrapping form to persist projector probes
         ret(Parens(body, Probe(Probe.empty)))
       | (["[", "]"], [Exp(body)]) =>
@@ -365,6 +367,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Invalid(t)
         | (["(", ")"], [Pat(body)]) => Parens(body)
+        | (label, [Pat(body)]) when is_probe_wrap(label) => Parens(body)
         | (["[", "]"], [Pat(body)]) =>
           switch (body) {
           | {term: Tuple(ps), _} => ListLit(ps)
@@ -425,6 +428,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | (["String"], []) => String
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
+        | (label, [Typ(body)]) when is_probe_wrap(label) => Parens(body)
         | (["[", "]"], [Typ(body)]) => List(body)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Unknown(Hole(Invalid(t)))
@@ -534,12 +538,17 @@ and rul = (unsorted: unsorted): Rul.t => {
 and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
   /* Remove projectors. We do this here as opposed to removing
    * them in an external call to save a whole-syntax pass. */
-  let seg = rm_and_log_projectors(seg);
+  let _ = log_projectors(seg);
   let tile_kids = (p: Piece.t): list(Term.Any.t) =>
     switch (p) {
     | Secondary(_)
     | Grout(_) => []
-    | Projector(_) => []
+    | Projector({syntax, id: _, _}) =>
+      let sort = Piece.sort(syntax) |> fst;
+      let seg = [syntax];
+      //let seg = [mk_probe(id, seg)];
+      //print_endline("unsorted projector case");
+      [go_s(sort, Segment.skel(seg), seg)];
     | Tile({mold, shards, children, _}) =>
       Aba.aba_triples(Aba.mk(shards, children))
       |> List.map(((l, kid, r)) => {

src/haz3lcore/statics/TermBase.re

@@ -976,12 +976,12 @@ and ClosureEnvironment: {
 
   let without_keys = keys => update_env(Environment.without_keys(keys));
 
-  let update_stack = (frame: option(Id.t), env) => {
+  let update_stack = (ap_id: option(Id.t), env) => {
     let stack =
-      switch (frame) {
+      switch (ap_id) {
       | None => stack_of(env)
-      | Some(frame) => [
-          {env_id: id_of(env), frame_id: frame},
+      | Some(ap_id) => [
+          Probe.mk_frame(~env_id=id_of(env), ~ap_id),
           ...stack_of(env),
         ]
       };

src/haz3lcore/zipper/projectors/ProbeProj.re

@@ -39,11 +39,13 @@ type a =
 let stack = stack =>
   stack
   |> List.rev
-  |> List.map(({env_id, frame_id}: Probe.frame) =>
+  |> List.map(({env_id, ap_id, closure_id}: Probe.frame) =>
        ""
+       ++ String.sub(Id.to_string(closure_id), 0, 2)
+       ++ "\n"
        ++ String.sub(Id.to_string(env_id), 0, 2)
        ++ "\n"
-       ++ String.sub(Id.to_string(frame_id), 0, 2)
+       ++ String.sub(Id.to_string(ap_id), 0, 2)
      )
   |> String.concat("\n");