live projectors view layer. minimal poc complete

src/haz3lcore/Measured.re

@@ -282,7 +282,8 @@ let last_of_token = (token: string, origin: Point.t): Point.t =>
     row: origin.row + StringUtil.num_linebreaks(token),
   };
 
-let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
+let of_segment =
+    (seg: Segment.t, info_map: Statics.Map.t, dyn_map: TestMap.t): t => {
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -353,8 +354,9 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
             let map = map |> add_g(g, {origin, last});
             (contained_indent, last, map);
           | Projector(p) =>
-            let token =
-              Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
+            let ci = Id.Map.find_opt(p.id, info_map);
+            let dyn = TestMap.lookup(p.id, dyn_map);
+            let token = Projector.placeholder(p, ci, dyn);
             let last = last_of_token(token, origin);
             let map = extra_rows(token, origin, map);
             let map = add_pr(p, {origin, last}, map);

src/haz3lcore/zipper/Editor.re

@@ -33,7 +33,7 @@ module CachedSyntax = {
   let yojson_of_t = _ => failwith("Editor.Meta.yojson_of_t");
   let t_of_yojson = _ => failwith("Editor.Meta.t_of_yojson");
 
-  let init = (z, info_map): t => {
+  let init = (z, info_map, dyn_map): t => {
     let segment = Zipper.unselect_and_zip(z);
     let MakeTerm.{term, terms, projectors} = MakeTerm.go(segment);
     {
@@ -42,7 +42,7 @@ module CachedSyntax = {
       term_ranges: TermRanges.mk(segment),
       tiles: TileMap.mk(segment),
       holes: Segment.holes(segment),
-      measured: Measured.of_segment(segment, info_map),
+      measured: Measured.of_segment(segment, info_map, dyn_map),
       selection_ids: Selection.selection_ids(z.selection),
       term,
       terms,
@@ -52,9 +52,9 @@ module CachedSyntax = {
 
   let mark_old: t => t = old => {...old, old: true};
 
-  let calculate = (z: Zipper.t, info_map, old: t) =>
+  let calculate = (z: Zipper.t, info_map, dyn_map, old: t) =>
     old.old
-      ? init(z, info_map)
+      ? init(z, info_map, dyn_map)
       : {...old, selection_ids: Selection.selection_ids(z.selection)};
 };
 
@@ -97,7 +97,7 @@ module Model = {
       col_target: None,
     },
     history: History.empty,
-    syntax: CachedSyntax.init(zipper, Id.Map.empty),
+    syntax: CachedSyntax.init(zipper, Id.Map.empty, TestMap.empty),
   };
 
   type persistent = PersistentZipper.t;
@@ -241,6 +241,7 @@ module Update = {
         ~settings: CoreSettings.t,
         ~is_edited,
         new_statics,
+        dyn_map,
         {syntax, state, history}: Model.t,
       ) => {
     // 1. Recalculate the autocomplete buffer if necessary
@@ -264,7 +265,8 @@ module Update = {
     // 2. Recalculate syntax cache
     let syntax = is_edited ? CachedSyntax.mark_old(syntax) : syntax;
 
-    let syntax = CachedSyntax.calculate(zipper, new_statics.info_map, syntax);
+    let syntax =
+      CachedSyntax.calculate(zipper, new_statics.info_map, dyn_map, syntax);
 
     // Recombine
     Model.{

src/haz3lcore/zipper/Printer.re

@@ -58,7 +58,7 @@ let measured = z =>
   z
   |> ProjectorPerform.Update.remove_all
   |> Zipper.seg_without_buffer
-  |> Measured.of_segment(_, Id.Map.empty);
+  |> Measured.of_segment(_, Id.Map.empty, TestMap.empty);
 
 let pretty_print = (~holes: option(string)=Some(""), z: Zipper.t): string =>
   to_rows(

src/haz3lcore/zipper/Projector.re

@@ -25,8 +25,8 @@ let shape = (p: Base.projector, info: info): shape => {
  * in the zipper; a tile consisting of any number of whitespaces
  * is considered a placeholder. This could be made more principled.
  * Note that a placeholder retains the UUID of the underlying. */
-let placeholder = (p: Base.projector, ci: option(Info.t)): string =>
-  switch (shape(p, {id: p.id, syntax: p.syntax, ci})) {
+let placeholder = (p: Base.projector, ci: option(Info.t), dyn): string =>
+  switch (shape(p, {id: p.id, syntax: p.syntax, ci, dyn})) {
   | Inline(width) => String.make(width, ' ')
   | Block({row, col}) => String.make(row - 1, '\n') ++ String.make(col, ' ')
   };

src/haz3lcore/zipper/ProjectorBase.re

@@ -33,6 +33,7 @@ type info = {
   id: Id.t,
   syntax,
   ci: option(Info.t),
+  dyn: option(list(TestMap.instance_report)),
 };
 
 /* To add a new projector:

src/haz3lcore/zipper/projectors/FoldProj.re

@@ -9,6 +9,17 @@ type t = {
   text: string,
 };
 
+/* Proof of concept value exposure. This isn't getting set right
+   after actions, only initially */
+let get_first_val = (rs: option(list(TestMap.instance_report))) => {
+  switch (rs) {
+  | Some(rs) =>
+    List.map(((d: DHExp.t, _)) => d.term |> TermBase.Exp.show_term, rs)
+    |> String.concat(", ")
+  | _ => "Nein"
+  };
+};
+
 module M: Projector = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model = t;
@@ -20,9 +31,12 @@ module M: Projector = {
   let placeholder = (m, _) =>
     Inline(m.text == "⋱" ? 2 : m.text |> String.length);
   let update = (m, _) => m;
-  let view = (m: model, ~info as _, ~local as _, ~parent) =>
+  let view = (m: model, ~info, ~local as _, ~parent) =>
     div(
-      ~attrs=[Attr.on_double_click(_ => parent(Remove))],
+      ~attrs=[
+        Attr.on_double_click(_ => parent(Remove)),
+        Attr.title(get_first_val(info.dyn)),
+      ],
       [text(m.text)],
     );
   let focus = _ => ();

src/haz3lweb/app/common/ProjectorView.re

@@ -118,6 +118,7 @@ let setup_view =
       id: Id.t,
       ~cached_statics: CachedStatics.t,
       ~cached_syntax: Editor.CachedSyntax.t,
+      ~dyn_map,
       ~inject: Action.t => Ui_effect.t(unit),
       ~font_metrics,
       ~indication: option(Direction.t),
@@ -126,7 +127,8 @@ let setup_view =
   let* p = Id.Map.find_opt(id, cached_syntax.projectors);
   let* syntax = Some(p.syntax);
   let ci = Id.Map.find_opt(id, cached_statics.info_map);
-  let info = {id, ci, syntax};
+  let dyn = TestMap.lookup(id, dyn_map);
+  let info = {id, ci, dyn, syntax};
   let+ measurement = Measured.find_pr_opt(p, cached_syntax.measured);
   let (module P) = to_module(p.kind);
   let parent = a => inject(Project(handle(id, a)));
@@ -156,6 +158,7 @@ let all =
       z,
       ~cached_statics: CachedStatics.t,
       ~cached_syntax: Editor.CachedSyntax.t,
+      ~dyn_map,
       ~inject,
       ~font_metrics,
     ) => {
@@ -172,6 +175,7 @@ let all =
           id,
           ~cached_statics,
           ~cached_syntax,
+          ~dyn_map,
           ~inject,
           ~font_metrics,
           ~indication,

src/haz3lweb/app/editors/cell/CellEditor.re

@@ -56,7 +56,13 @@ module Update = {
       )
       : Model.t => {
     let editor =
-      CodeEditable.Update.calculate(~settings, ~is_edited, ~stitch, editor);
+      CodeEditable.Update.calculate(
+        ~settings,
+        ~is_edited,
+        ~stitch,
+        ~dyn_map=TestMap.empty, //TODO(andrew): see below
+        editor,
+      );
     let result =
       EvalResult.Update.calculate(
         ~settings,
@@ -65,6 +71,20 @@ module Update = {
         editor |> CodeEditable.Model.get_statics,
         result,
       );
+    //TODO(andrew): double-calcing editor...
+    let dyn_map =
+      switch (EvalResult.Model.make_test_report(result)) {
+      | Some(res) => res.test_map
+      | None => TestMap.empty
+      };
+    let editor =
+      CodeEditable.Update.calculate(
+        ~settings,
+        ~is_edited,
+        ~stitch,
+        ~dyn_map,
+        editor,
+      );
     {editor, result};
   };
 };
@@ -149,6 +169,11 @@ module View = {
         ~locked,
         model.result,
       );
+    let dyn_map =
+      switch (EvalResult.Model.make_test_report(model.result)) {
+      | Some(res) => res.test_map
+      | None => TestMap.empty
+      };
     div(
       ~attrs=[Attr.classes(["cell", locked ? "locked" : "unlocked"])],
       Option.to_list(caption)
@@ -166,6 +191,7 @@ module View = {
               : (action => inject(MainEditor(action))),
           ~selected=selected == Some(MainEditor),
           ~overlays=overlays(model.editor.editor),
+          ~dyn_map,
           ~sort?,
           model.editor,
         ),

src/haz3lweb/app/editors/code/Code.re

@@ -71,9 +71,15 @@ let of_secondary =
     }
   );
 
-let of_projector = (p, expected_sort, indent, info_map) =>
+let of_projector = (p, expected_sort, indent, info_map, dyn_map) =>
   of_delim'((
-    [Projector.placeholder(p, Id.Map.find_opt(p.id, info_map))],
+    [
+      Projector.placeholder(
+        p,
+        Id.Map.find_opt(p.id, info_map),
+        TestMap.lookup(p.id, dyn_map),
+      ),
+    ],
     false,
     expected_sort,
     true,
@@ -88,6 +94,7 @@ module Text =
            let map: Measured.t;
            let settings: Settings.Model.t;
            let info_map: Statics.Map.t;
+           let dyn_map: TestMap.t;
          },
        ) => {
   let m = p => Measured.find_p(~msg="Text", p, M.map);
@@ -118,7 +125,13 @@ module Text =
     | Secondary({content, _}) =>
       of_secondary((content, M.settings.secondary_icons, m(p).last.col))
     | Projector(p) =>
-      of_projector(p, expected_sort, m(Projector(p)).origin.col, M.info_map)
+      of_projector(
+        p,
+        expected_sort,
+        m(Projector(p)).origin.col,
+        M.info_map,
+        M.dyn_map,
+      )
     };
   }
   and of_tile = (buffer_ids, expected_sort: Sort.t, t: Tile.t): list(Node.t) => {
@@ -160,12 +173,13 @@ let rec holes =
      );
 
 let simple_view = (~font_metrics, ~segment, ~settings: Settings.t): Node.t => {
-  let map = Measured.of_segment(segment, Id.Map.empty);
+  let map = Measured.of_segment(segment, Id.Map.empty, TestMap.empty);
   module Text =
     Text({
       let map = map;
       let settings = settings;
       let info_map = Id.Map.empty; /* Assume this doesn't contain projectors */
+      let dyn_map = TestMap.empty; /* Assume this doesn't contain projectors */
     });
   let holes = holes(~map, ~font_metrics, segment);
   div(

src/haz3lweb/app/editors/code/CodeEditable.re

@@ -242,6 +242,7 @@ module View = {
         ~selected: bool,
         ~overlays: list(Node.t)=[],
         ~sort=?,
+        ~dyn_map,
         model: Model.t,
       ) => {
     let edit_decos = {
@@ -250,6 +251,7 @@ module View = {
           let editor = model.editor;
           let globals = globals;
           let statics = model.statics;
+          let dynamics = dyn_map;
         });
       Deco.editor(model.editor.state.zipper, selected);
     };
@@ -260,10 +262,11 @@ module View = {
         ~cached_syntax=model.editor.syntax,
         ~inject=x => inject(Perform(x)),
         ~font_metrics=globals.font_metrics,
+        ~dyn_map,
       );
     let overlays = edit_decos @ overlays @ [projectors];
     let code_view =
-      CodeWithStatics.View.view(~globals, ~overlays, ~sort?, model);
+      CodeWithStatics.View.view(~globals, ~overlays, ~dyn_map, ~sort?, model);
     let mousedown_overlay =
       selected && globals.mousedown
         ? [mousedown_overlay(~globals, ~inject=x => inject(Perform(x)))]

src/haz3lweb/app/editors/code/CodeViewable.re

@@ -13,13 +13,15 @@ let view =
       ~segment,
       ~holes,
       ~info_map,
+      ~dyn_map,
     )
     : Node.t => {
   module Text =
     Code.Text({
       let map = measured;
       let settings = globals.settings;
       let info_map = info_map;
+      let dyn_map = dyn_map;
     });
   let code = Text.of_segment(buffer_ids, false, sort, segment);
   let holes = List.map(Code.of_hole(~measured, ~globals), holes);
@@ -51,21 +53,36 @@ let view =
 // };
 
 let view_segment =
-    (~globals: Globals.t, ~sort: Sort.t, ~info_map, segment: Segment.t) => {
-  let measured = Measured.of_segment(segment, info_map);
+    (
+      ~globals: Globals.t,
+      ~sort: Sort.t,
+      ~info_map,
+      ~dyn_map,
+      segment: Segment.t,
+    ) => {
+  let measured = Measured.of_segment(segment, info_map, dyn_map);
   let buffer_ids = [];
   let holes = Segment.holes(segment);
-  view(~globals, ~sort, ~measured, ~buffer_ids, ~holes, ~segment, ~info_map);
+  view(
+    ~globals,
+    ~sort,
+    ~measured,
+    ~buffer_ids,
+    ~holes,
+    ~segment,
+    ~dyn_map,
+    ~info_map,
+  );
 };
 
-let view_exp = (~globals: Globals.t, ~settings, exp: Exp.t) => {
+let view_exp = (~dyn_map, ~globals: Globals.t, ~settings, exp: Exp.t) => {
   exp
   |> ExpToSegment.exp_to_segment(~settings)
-  |> view_segment(~globals, ~sort=Exp);
+  |> view_segment(~dyn_map, ~globals, ~sort=Exp);
 };
 
 let view_typ = (~globals: Globals.t, ~settings, typ: Typ.t) => {
   typ
   |> ExpToSegment.typ_to_segment(~settings)
-  |> view_segment(~globals, ~sort=Typ);
+  |> view_segment(~dyn_map=TestMap.empty, ~globals, ~sort=Typ);
 };