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/FontMetrics.re

@@ -0,0 +1,25 @@
+open Util;
+open Js_of_ocaml;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  row_height: float,
+  col_width: float,
+};
+
+let init = {row_height: 10., col_width: 10.};
+
+let get_goal =
+    (
+      ~font_metrics: t,
+      text_box: Js.t(Dom_html.element),
+      e: Js.t(Dom_html.mouseEvent),
+    )
+    : Point.t => {
+  open Float;
+  let x_rel = of_int(e##.clientX) -. text_box##getBoundingClientRect##.left;
+  let y_rel = of_int(e##.clientY) -. text_box##getBoundingClientRect##.top;
+  let row = to_int(y_rel /. font_metrics.row_height);
+  let col = to_int(round(x_rel /. font_metrics.col_width));
+  {row, col};
+};

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_of_proj: Base.projector => ProjectorShape.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 = shape_of_proj(p);
+            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) => {
@@ -403,3 +409,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/dynamics/Casts.re

@@ -63,7 +63,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Forall(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
-  | Parens(ty) => ground_cases_of(ty)
+  | Wrap(ty) => ground_cases_of(ty)
   | Prod(tys) =>
     if (List.for_all(
           fun

src/haz3lcore/dynamics/DHExp.re

@@ -79,7 +79,7 @@ let rec strip_casts =
         | UnOp(_)
         | BinOp(_)
         | Match(_)
-        | Parens(_)
+        | Wrap(_)
         | EmptyHole
         | Invalid(_)
         | Var(_)
@@ -161,7 +161,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Deferral(_)
           | TyAlias(_)
           | DeferredAp(_)
-          | Parens(_)
+          | Wrap(_)
           | UnOp(_) => continue(exp)
           },
       exp,

src/haz3lcore/dynamics/EvalCtx.re

@@ -23,6 +23,7 @@ type term =
   | BinOp2(Operators.op_bin, DHExp.t, t)
   | Tuple(t, (list(DHExp.t), list(DHExp.t)))
   | Test(t)
+  | Wrap(t, Probe.tag)
   | ListLit(t, (list(DHExp.t), list(DHExp.t)))
   | MultiHole(t, (list(Any.t), list(Any.t)))
   | Cons1(t, DHExp.t)
@@ -88,6 +89,9 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
     | Test(ctx) =>
       let d1 = compose(ctx, d);
       Test(d1) |> wrap;
+    | Wrap(ctx, tag) =>
+      let d1 = compose(ctx, d);
+      Wrap(d1, tag) |> 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, id, v) =>
+    state := EvaluatorState.add_closure(state^, id, v);
+
   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, id: Id.t, v: Dynamics.Probe.Closure.t) => {
+  ...es,
+  probes: Dynamics.Probe.Map.extend(id, v, 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, Id.t, Dynamics.Probe.Closure.t) => t;
+
+let get_probes: t => Dynamics.Probe.Map.t;

src/haz3lcore/dynamics/EvaluatorStep.re

@@ -140,6 +140,9 @@ let rec matches =
       | Test(ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Test(ctx) |> rewrap;
+      | Wrap(ctx, tag) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Wrap(ctx, tag) |> rewrap;
       | ListLit(ctx, ds) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         ListLit(ctx, ds) |> rewrap;
@@ -298,6 +301,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, id, info) =>
+      state := EvaluatorState.add_closure(state^, id, info);
   };
 
   module Decomp = Transition(DecomposeEVMode);
@@ -339,6 +344,9 @@ module TakeStep = {
 
     let update_test = (state, id, v) =>
       state := EvaluatorState.add_test(state^, id, v);
+
+    let update_probe = (state, id, info) =>
+      state := EvaluatorState.add_closure(state^, id, info);
   };
 
   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;
 
 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)
+    | (Wrap(d, _), _) => matches_exp(d, f)
+    | (_, Wrap(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,6 +11,26 @@ let combine_result = (r1: match_result, r2: match_result): match_result =>
     Matches(Environment.union(env1, env2))
   };
 
+type closure_closures =
+  list((Probe.stack, Probe.stack) => (Id.t, Dynamics.Probe.Closure.t));
+let closure_closures: ref(closure_closures) = ref([]);
+
+let capture_closure = (pr, id: Id.t, d, inner_match: match_result): unit =>
+  switch (inner_match) {
+  | DoesNotMatch => ()
+  | IndetMatch => ()
+  | Matches(env) =>
+    closure_closures :=
+      List.cons(
+        (stack, dyn_stack) =>
+          (
+            id,
+            Dynamics.Probe.Closure.mk(d, {env, stack, dyn_stack, id}, pr),
+          ),
+        closure_closures^,
+      )
+  };
+
 let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
   switch (DHPat.term_of(dp)) {
   | Invalid(_)
@@ -55,7 +75,23 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
     let* ds = Unboxing.unbox(Tuple(List.length(ps)), d);
     List.map2(matches, ps, ds)
     |> List.fold_left(combine_result, Matches(Environment.empty));
-  | Parens(p) => matches(p, d)
+  | Wrap(p, Paren) => matches(p, d)
+  | Wrap(p, Probe(pr)) =>
+    let inner_match = matches(p, d);
+    capture_closure(pr, Term.Pat.rep_id(dp), d, inner_match);
+    inner_match;
   | Cast(p, t1, t2) =>
     matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple)
   };
+
+type matches_and_closures = {
+  matches: match_result,
+  closures: closure_closures,
+};
+
+// wrap matches but do stateful thing (closure capture)
+let matches = (dp: Pat.t, d: DHExp.t): matches_and_closures => {
+  closure_closures := [];
+  let res = matches(dp, d);
+  {matches: res, closures: closure_closures^};
+};

src/haz3lcore/dynamics/Probe.re

@@ -0,0 +1,38 @@
+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,
+  stem: Binding.stem,
+};
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type tag =
+  | Paren
+  | Probe(t);
+
+/* Information about the evaluation of an ap */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type frame = {
+  ap_id: Id.t, /* Syntax ID of the ap */
+  env_id: Id.t /* ID of env in which ap was applied */
+};
+
+/* List of applications prior to some evaluation */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type stack = list(frame);
+
+let empty: t = {refs: [], stem: []};
+
+let env_stack: list(frame) => list(Id.t) =
+  List.map((en: frame) => en.env_id);
+
+let mk_frame = (~env_id: Id.t, ~ap_id: Id.t): frame => {env_id, ap_id};