Live Projectors

licenses/Icons.md

@@ -0,0 +1 @@
+The icons used in Hazel, including the Hazel icon, are from The Noun Project (https://thenounproject.com/) under the Icon Pro license (https://thenounproject.com/legal/terms-of-use/#icon-licenses).

src/haz3lcore/ClipboardCache.re

@@ -0,0 +1,33 @@
+/* In order to retain projectors on cut/copy/paste, and to speed
+ * up pasting after in-editor copy/cut, we maintain a cached of
+ * the last copied selection segment and do segment insertion
+ * instead of reparsing if the clipboard text contents are the
+ * same as text serialization of the cached segment */
+
+let cache: ref(option((string, Segment.t))) = ref(None);
+
+let set = (seg: option(Segment.t), str: string): unit =>
+  switch (seg) {
+  | Some(seg) when Segment.deep_tile_complete(seg) =>
+    /* This check makes sure we won't create backpack orphans */
+    cache := Some((str, seg))
+  | _ => ()
+  };
+
+let intersection = (ids1: list(Id.t), ids2: list(Id.t)): list(Id.t) =>
+  List.filter(id => List.mem(id, ids2), ids1);
+
+let get = (pasted: string): Action.t => {
+  /* Note the trimming of leading whitespace on each line */
+  let trim = Util.StringUtil.trim_leading;
+  let trimmed_pasted = trim(pasted);
+  switch (cache^) {
+  | None => Paste(String(trimmed_pasted))
+  | Some((cached, segment)) =>
+    /* Note that we must replace unique ids here if we want to
+     * support copying and/or multiples pastes for a copy */
+    trim(cached) == trimmed_pasted
+      ? Paste(Segment(Segment.IDs.replace(segment)))
+      : Paste(String(trimmed_pasted))
+  };
+};

src/haz3lcore/Measured.re

@@ -56,7 +56,6 @@ type t = {
   secondary: Id.Map.t(measurement),
   projectors: Id.Map.t(measurement),
   rows: Rows.t,
-  linebreaks: Id.Map.t(rel_indent),
 };
 
 let empty = {
@@ -65,7 +64,6 @@ let empty = {
   secondary: Id.Map.empty,
   projectors: Id.Map.empty,
   rows: Rows.empty,
-  linebreaks: Id.Map.empty,
 };
 
 let add_s = (id: Id.t, i: int, m, map) => {
@@ -131,11 +129,6 @@ let rec add_n_rows = (origin: Point.t, row_indent, n: abs_indent, map: t): t =>
     |> add_row(origin.row + n - 1, {indent: row_indent, max_col: origin.col})
   };
 
-let add_lb = (id, indent, map) => {
-  ...map,
-  linebreaks: Id.Map.add(id, indent, map.linebreaks),
-};
-
 let singleton_w = (w, m) => empty |> add_w(w, m);
 let singleton_g = (g, m) => empty |> add_g(g, m);
 let singleton_s = (id, shard, m) => empty |> add_s(id, shard, m);
@@ -147,8 +140,6 @@ let find_shards = (~msg="", t: Tile.t, map) =>
   | _ => failwith("find_shards: " ++ msg)
   };
 
-let find_opt_lb = (id, map) => Id.Map.find_opt(id, map.linebreaks);
-
 let find_shards' = (id: Id.t, map) =>
   switch (Id.Map.find_opt(id, map.tiles)) {
   | None => []
@@ -282,7 +273,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, shape_map: Id.Map.t(ProjectorCore.Shape.t)): t => {
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -340,7 +332,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
                    origin.row,
                    {indent: row_indent, max_col: origin.col},
                  )
-              |> add_lb(w.id, indent);
+              |> add_n_rows(origin, row_indent, 1);
             (indent, last, map);
           | Secondary(w) =>
             let wspace_length =
@@ -353,11 +345,25 @@ 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 last = last_of_token(token, origin);
-            let map = extra_rows(token, origin, map);
-            let map = add_pr(p, {origin, last}, map);
+            let row_indent = container_indent + contained_indent;
+            let shape = ProjectorCore.Shape.Map.lookup(p.id, shape_map);
+            let num_extra_rows =
+              switch (shape.vertical) {
+              | Inline => 0
+              | Block(num_lbs) => num_lbs
+              };
+            let last = {
+              col: origin.col + shape.horizontal,
+              row:
+                switch (shape.vertical) {
+                | Inline => origin.row
+                | Block(num_lb) => origin.row + num_lb
+                },
+            };
+            let map =
+              map
+              |> add_n_rows(origin, row_indent, num_extra_rows)
+              |> add_pr(p, {origin, last});
             (contained_indent, last, map);
           | Tile(t) =>
             let add_shard = (origin, shard, map) => {
@@ -392,6 +398,9 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
   snd(go_nested(~map=empty, seg));
 };
 
+/* Memoized for perf */
+let of_segment = Core.Memo.general(of_segment);
+
 let length = (seg: Segment.t, map: t): int =>
   switch (seg) {
   | [] => 0
@@ -403,3 +412,10 @@ let length = (seg: Segment.t, map: t): int =>
     let last = find_p(ListUtil.last(tl), map);
     last.last.col - first.origin.col;
   };
+
+/* Width in characters of row at measurement.origin */
+let start_row_width = (measurement: measurement, measured: t): int =>
+  switch (IntMap.find_opt(measurement.origin.row, measured.rows)) {
+  | None => 0
+  | Some(row) => row.max_col
+  };

src/haz3lcore/assistant/AssistantForms.re

@@ -38,7 +38,7 @@ module Typ = {
   let of_infix_delim: list((Token.t, Typ.term)) = [
     //("|>", Unknown(Internal)), /* annoying during case rules */
     (",", Prod([unk, unk])), /* NOTE: Current approach doesn't work for this, but irrelevant as 1-char */
-    ("::", List(unk)), /* annoying in patterns */
+    //("::", List(unk)), /* annoying in patterns. TODO: add codepath to show only if Ana(List(_)) */
     ("@", List(unk)),
     (";", Unknown(Internal)),
     ("&&", Bool),

src/haz3lcore/assistant/TyDi.re

@@ -49,10 +49,8 @@ let token_to_left = (z: Zipper.t): option(string) =>
 /* The selection buffer used by TyDi is currently unstructured; it simply
  * holds an unparsed string, which is parsed via the same mechanism as
  * Paste only when a suggestion is accepted. */
-let mk_unparsed_buffer =
-    (~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t => {
-  let mold = Siblings.mold_fitting_between(sort, Precedence.max, sibs);
-  [Tile({id: Id.mk(), label: [t], shards: [0], children: [], mold})];
+let mk_unparsed_buffer = (t: Token.t): Segment.t => {
+  [Secondary({id: Id.mk(), content: Comment(t)})];
 };
 
 /* If 'current' is a proper prefix of 'candidate', return the
@@ -70,7 +68,7 @@ let suffix_of = (candidate: Token.t, current: Token.t): option(Token.t) => {
 /* Returns the text content of the suggestion buffer */
 let get_buffer = (z: Zipper.t): option(Token.t) =>
   switch (z.selection.mode, z.selection.content) {
-  | (Buffer(Unparsed), [Tile({label: [completion], _})]) =>
+  | (Buffer(Unparsed), [Secondary({content: Comment(completion), _})]) =>
     Some(completion)
   | _ => None
   };
@@ -96,12 +94,7 @@ let set_buffer = (~info_map: Statics.Map.t, z: Zipper.t): option(Zipper.t) => {
        );
   let* top_suggestion = suggestions |> Util.ListUtil.hd_opt;
   let* suggestion_suffix = suffix_of(top_suggestion.content, tok_to_left);
-  let content =
-    mk_unparsed_buffer(
-      ~sort=Info.sort_of(ci),
-      z.relatives.siblings,
-      suggestion_suffix,
-    );
+  let content = mk_unparsed_buffer(suggestion_suffix);
   let z = Zipper.set_buffer(z, ~content, ~mode=Unparsed);
   Some(z);
 };

src/haz3lcore/dynamics/DHExp.re

@@ -80,6 +80,7 @@ let rec strip_casts =
         | BinOp(_)
         | Match(_)
         | Parens(_)
+        | Probe(_)
         | EmptyHole
         | Invalid(_)
         | Var(_)
@@ -162,6 +163,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | TyAlias(_)
           | DeferredAp(_)
           | Parens(_)
+          | Probe(_)
           | UnOp(_) => continue(exp)
           },
       exp,

src/haz3lcore/dynamics/EvalCtx.re

@@ -23,6 +23,8 @@ type term =
   | BinOp2(Operators.op_bin, DHExp.t, t)
   | Tuple(t, (list(DHExp.t), list(DHExp.t)))
   | Test(t)
+  | Parens(t)
+  | Probe(t, Probe.t)
   | ListLit(t, (list(DHExp.t), list(DHExp.t)))
   | MultiHole(t, (list(Any.t), list(Any.t)))
   | Cons1(t, DHExp.t)
@@ -88,6 +90,12 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
     | Test(ctx) =>
       let d1 = compose(ctx, d);
       Test(d1) |> wrap;
+    | Parens(ctx) =>
+      let d1 = compose(ctx, d);
+      Parens(d1) |> wrap;
+    | Probe(ctx, p) =>
+      let d1 = compose(ctx, d);
+      Probe(d1, p) |> wrap;
     | UnOp(op, ctx) =>
       let d1 = compose(ctx, d);
       UnOp(op, d1) |> wrap;

src/haz3lcore/dynamics/Evaluator.re

@@ -61,6 +61,9 @@ module EvaluatorEVMode: {
   let update_test = (state, id, v) =>
     state := EvaluatorState.add_test(state^, id, v);
 
+  let update_probe = (state, closure: Dynamics.Probe.Closure.t) =>
+    state := EvaluatorState.add_closure(state^, closure);
+
   let req_final = (f, _, x) => {
     let.trampoline x' = Next(() => f(x));
     Trampoline.return(x' |> snd);

src/haz3lcore/dynamics/EvaluatorState.re

@@ -2,9 +2,14 @@
 type t = {
   stats: EvaluatorStats.t,
   tests: TestMap.t,
+  probes: Dynamics.Probe.Map.t,
 };
 
-let init = {stats: EvaluatorStats.initial, tests: TestMap.empty};
+let init = {
+  stats: EvaluatorStats.initial,
+  tests: TestMap.empty,
+  probes: Dynamics.Probe.Map.empty,
+};
 
 let take_step = ({stats, _} as es) => {
   ...es,
@@ -22,4 +27,9 @@ let add_test = ({tests, _} as es, id, report) => {
 
 let get_tests = ({tests, _}) => tests;
 
-let put_tests = (tests, es) => {...es, tests};
+let add_closure = ({probes, _} as es, closure: Dynamics.Probe.Closure.t) => {
+  ...es,
+  probes: Dynamics.Probe.Map.extend(closure.syntax_id, closure, probes),
+};
+
+let get_probes = ({probes, _}) => probes;

src/haz3lcore/dynamics/EvaluatorState.rei

@@ -32,4 +32,6 @@ let add_test: (t, Id.t, TestMap.instance_report) => t;
 
 let get_tests: t => TestMap.t;
 
-let put_tests: (TestMap.t, t) => t;
+let add_closure: (t, Dynamics.Probe.Closure.t) => t;
+
+let get_probes: t => Dynamics.Probe.Map.t;

src/haz3lcore/dynamics/EvaluatorStep.re

@@ -140,6 +140,12 @@ let rec matches =
       | Test(ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Test(ctx) |> rewrap;
+      | Parens(ctx) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Parens(ctx) |> rewrap;
+      | Probe(ctx, pr) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Probe(ctx, pr) |> rewrap;
       | ListLit(ctx, ds) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         ListLit(ctx, ds) |> rewrap;
@@ -298,6 +304,8 @@ module Decompose = {
     let otherwise = (env, o) => (o, Result.BoxedValue, env, ());
     let update_test = (state, id, v) =>
       state := EvaluatorState.add_test(state^, id, v);
+    let update_probe = (state, closure: Dynamics.Probe.Closure.t) =>
+      state := EvaluatorState.add_closure(state^, closure);
   };
 
   module Decomp = Transition(DecomposeEVMode);
@@ -339,6 +347,9 @@ module TakeStep = {
 
     let update_test = (state, id, v) =>
       state := EvaluatorState.add_test(state^, id, v);
+
+    let update_probe = (state, closure: Dynamics.Probe.Closure.t) =>
+      state := EvaluatorState.add_closure(state^, closure);
   };
 
   module TakeStepEV = Transition(TakeStepEVMode);

src/haz3lcore/dynamics/FilterMatcher.re

@@ -1,11 +1,4 @@
-let evaluate_extend_env =
-    (new_bindings: Environment.t, to_extend: ClosureEnvironment.t)
-    : ClosureEnvironment.t => {
-  to_extend
-  |> ClosureEnvironment.map_of
-  |> Environment.union(new_bindings)
-  |> ClosureEnvironment.of_environment;
-};
+let evaluate_extend_env = ClosureEnvironment.extend_eval(~call_stack=[]);
 
 let evaluate_extend_env_with_pat =
     (
@@ -104,8 +97,8 @@ let rec matches_exp =
     true;
   } else {
     switch (d |> DHExp.term_of, f |> DHExp.term_of) {
-    | (Parens(d), _) => matches_exp(d, f)
-    | (_, Parens(f)) => matches_exp(d, f)
+    | (Parens(d) | Probe(d, _), _) => matches_exp(d, f)
+    | (_, Parens(f) | Probe(f, _)) => matches_exp(d, f)
 
     | (Constructor("$e", _), _) => failwith("$e in matched expression")
     | (Constructor("$v", _), _) => failwith("$v in matched expression")

src/haz3lcore/dynamics/PatternMatch.re

@@ -11,7 +11,8 @@ let combine_result = (r1: match_result, r2: match_result): match_result =>
     Matches(Environment.union(env1, env2))
   };
 
-let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
+let rec matches = (capture, dp: Pat.t, d: DHExp.t): match_result => {
+  let matches = matches(capture);
   switch (DHPat.term_of(dp)) {
   | Invalid(_)
   | EmptyHole
@@ -56,6 +57,38 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
     List.map2(matches, ps, ds)
     |> List.fold_left(combine_result, Matches(Environment.empty));
   | Parens(p) => matches(p, d)
+  | Probe(p, pr) =>
+    let inner_match = matches(p, d);
+    capture(pr, dp, d, inner_match);
+    inner_match;
   | Cast(p, t1, t2) =>
     matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple)
   };
+};
+
+type closure_closures = list(Probe.call_stack => Dynamics.Probe.Closure.t);
+
+type matches_and_closures = {
+  matches: match_result,
+  closures: closure_closures,
+};
+
+let matches = (dp: Pat.t, d: DHExp.t): matches_and_closures => {
+  /* Closure capture for Probe instrumentation */
+  let closure_closures: ref(closure_closures) = ref([]);
+  let capture =
+      (pr: Probe.t, dp: Term.Pat.t, d: DHExp.t, inner_match: match_result)
+      : unit =>
+    switch (inner_match) {
+    | DoesNotMatch => ()
+    | IndetMatch => ()
+    | Matches(env) =>
+      closure_closures :=
+        List.cons(
+          Dynamics.Probe.Closure.mk(Term.Pat.rep_id(dp), d, env, _, pr),
+          closure_closures^,
+        )
+    };
+  let res = matches(capture, dp, d);
+  {matches: res, closures: closure_closures^};
+};

src/haz3lcore/dynamics/Probe.re

@@ -0,0 +1,21 @@
+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 intermediate
+ * dynamic data such as environment variables and
+ * callstack state. Probes are created during maketerm
+ * and can be intercepted duting elaboration to add
+ * static information to inform dynamic information
+ * capture (such as as restricting environment variable
+ * capture to variables actually referenced. */
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {refs: Binding.s};
+
+/* A call at stack represented by function ap ids */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type call_stack = list(Id.t);
+
+let empty: t = {refs: []};