Probectors

src/haz3lcore/ProbePerform.re

@@ -316,13 +316,29 @@ let add_ids_from_auto_term =
     (~syntax: CachedSyntax.t, ~info_map: Statics.Map.t, z: Zipper.t): Zipper.t => {
   let auto_ids = Id.Map.bindings(z.refractors.autos.ids) |> List.map(fst);
   let ids = List.concat_map(ids_from_term(~syntax, ~info_map), auto_ids);
+  /* Build a set for O(log n) membership checks */
+  let new_ids_set =
+    List.fold_left((map, id) => Id.Map.add(id, (), map), Id.Map.empty, ids);
   Zipper.update_ephemerals(
-    _ =>
+    old_ephemerals => {
+      /* Keep existing entries that are still valid (preserves models) */
+      let kept =
+        Id.Map.filter(
+          (id, _) => Id.Map.mem(id, new_ids_set),
+          old_ephemerals,
+        );
+      /* Add new entries only for IDs not already present */
       List.fold_left(
-        (map, id) => Id.Map.add(id, Refractors.mk_entry(Probe), map),
-        Id.Map.empty,
+        (map, id) =>
+          if (Id.Map.mem(id, map)) {
+            map; /* Already exists with model, keep it */
+          } else {
+            Id.Map.add(id, Refractors.mk_entry(Probe), map);
+          },
+        kept,
         ids,
-      ),
+      );
+    },
     z,
   );
 };

src/haz3lcore/projectors/ProjectorBase.re

@@ -31,13 +31,14 @@ type utility = {
   /* Convert a segment to a term */
   seg_to_term: Base.segment => option(Any.t),
   /* Convert a term to a segment */
-  term_to_seg: Any.t => Base.segment,
+  term_to_seg: (~inline: bool, Any.t) => Base.segment,
   seg_to_string: Base.segment => string,
   /* Lifts term->term functions to syntax->syntax. This will
    * proactively attempt to parenthesize resulting non-single
    * piece terms. As such, sorts that do not have parentheses
    * (currently all degenerate cases) will throw an error */
-  lift_syntax: (Any.t => Any.t, Base.segment) => option(Base.segment),
+  lift_syntax:
+    (~inline: bool, Any.t => Any.t, Base.segment) => option(Base.segment),
 };
 
 module Focusable = {
@@ -223,6 +224,6 @@ module Cook = (C: Projector) : Cooked => {
     });
   let placeholder = m =>
     m |> Sexplib.Sexp.of_string |> C.model_of_sexp |> C.placeholder;
-  let update = (m, i, a) =>
+  let update = (m: model, i: info, a: action): model =>
     C.update(m |> deserialize_m, i, a |> deserialize_a) |> serialize_m;
 };

src/haz3lcore/projectors/ProjectorInfo.re

@@ -7,27 +7,29 @@ open Language;
  * See ProjectorBase.utility definition for more information */
 let utility: ProjectorBase.utility = {
   let seg_to_term = MakeTerm.for_projection;
-  let term_to_seg =
+  let term_to_seg = (inline, any) =>
     ExpToSegment.any_to_segment(
       ~settings={
-        ...ExpToSegment.Settings.of_core(~inline=true, CoreSettings.off),
+        ...ExpToSegment.Settings.of_core(~inline, CoreSettings.off),
         show_unknown_as_hole: false,
         fold_fn_bodies: `NoFold,
       },
+      any,
     );
   let lift_syntax =
-      (fn: Any.t => Any.t, seg: Base.segment): option(Base.segment) =>
+      (inline, fn: Any.t => Any.t, seg: Base.segment): option(Base.segment) => {
     switch (seg |> seg_to_term) {
     | None => None
-    | Some(s) => Some(s |> fn |> term_to_seg)
+    | Some(s) => Some(s |> fn |> term_to_seg(inline))
     };
+  };
   /* NOTE: Setting indent to anything other than "" has serious
    * perf implications when there are lots of probes on the screen */
   let seg_to_string = Printer.of_segment(~holes="?", ~indent="");
   {
-    term_to_seg,
+    term_to_seg: (~inline, any) => term_to_seg(inline, any),
     seg_to_term,
-    lift_syntax,
+    lift_syntax: (~inline) => lift_syntax(inline),
     seg_to_string,
   };
 };

src/haz3lcore/projectors/ProjectorPerform.re

@@ -184,37 +184,90 @@ let go =
     | Some(z) => Ok(z)
     | None => Error(Cant_project)
     }
-  | SetSyntax(idx, seg) =>
-    Ok(
-      update(
-        p =>
-          {
-            ...p,
-            syntax: Segment.parenthesize(seg),
-          },
-        projector_idx_to_id(idx),
-        z,
-      ),
-    )
+  | SetSyntax(idx, kind, seg) =>
+    let id = idx_to_id(kind, idx);
+    // Ensure seg is parenthesized unless it already is
+    let parenthesized_piece =
+      Segment.unparenthesize(seg) |> Segment.parenthesize;
+    if (ProjectorCore.Kind.is_refractor(kind)) {
+      let parenthesized_seg = [parenthesized_piece];
+      // Check for existing refractors (automatic ephemeral or manual) that control this projector
+      let original_id = id;
+      let ephemeral_model =
+        Id.Map.find_opt(original_id, z.refractors.autos.ephemerals)
+        |> Option.map((pr: Refractors.entry) => pr.model);
+      let manual_refractor_model =
+        List.assoc_opt(original_id, z.refractors.manuals)
+        |> Option.map((pr: Refractors.entry) => pr.model);
+      switch (manual_refractor_model, ephemeral_model) {
+      | (Some(refractor_model), _) =>
+        // Manual refractor exists: update the selection to this projector's term range,
+        // replace with new syntax, and create a new refractor probe monitoring the updated term
+        let new_id =
+          MakeTerm.from_zip_for_sem(
+            Zipper.unzip(~direction=Right, parenthesized_seg),
+          ).
+            term
+          |> Language.Exp.rep_id;
+
+        let new_z = {
+          open OptUtil.Syntax;
+          let* (l, r) = TermData.extremes_shards(id, term_data);
+          let+ z = Select.shard_range(l, r, z);
+          let z = Zipper.replace_selection(Right, parenthesized_seg, z);
+          ZipperBase.add_manual(~model=refractor_model, new_id, kind, z);
+        };
+
+        switch (new_z) {
+        | Some(z) => Ok(z)
+        | None => Error(Cant_project)
+        };
+      | (_, Some(_)) =>
+        // Ephemeral refractor exists: update selection and replace syntax,
+        // but don't create new refractor as this is handled automatically
+
+        let new_z = {
+          open OptUtil.Syntax;
+          let* (l, r) = TermData.extremes_shards(id, term_data);
+          let+ z = Select.shard_range(l, r, z);
+          let z = Zipper.replace_selection(Right, parenthesized_seg, z);
+          z;
+        };
+
+        switch (new_z) {
+        | Some(z) => Ok(z)
+        | None => Error(Cant_project)
+        };
+      | (None, None) => assert(false)
+      };
+    } else {
+      Ok(
+        update(
+          pr =>
+            {
+              ...pr,
+              syntax: parenthesized_piece,
+            },
+          id,
+          z,
+        ),
+      );
+    };
   | SetModel(idx, kind, new_model) =>
     let id = idx_to_id(kind, idx);
     Ok(
       if (ProjectorCore.Kind.is_refractor(kind)) {
-        Zipper.update_manuals(
-          map =>
-            ListUtil.assoc_update(
-              id,
-              fun
-              | Some(entry: Refractors.entry) =>
-                Some(
-                  Refractors.{
-                    kind: entry.kind,
-                    model: new_model,
-                  },
-                )
-              | None => None,
-              map,
-            ),
+        Zipper.update_refractor(
+          id,
+          fun
+          | Some(entry: Refractors.entry) =>
+            Some(
+              Refractors.{
+                kind: entry.kind,
+                model: new_model,
+              },
+            )
+          | None => None,
           z,
         );
       } else {

src/haz3lcore/projectors/implementations/CSVProjector.re

@@ -74,6 +74,7 @@ module M: Projector = {
 
     switch (
       info.utility.lift_syntax(
+        ~inline=true,
         fun
         | Exp(any) =>
           Exp({