Live Projectors

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

@@ -282,7 +282,7 @@ 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, token_of_proj: Base.projector => string): t => {
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -353,8 +353,7 @@ 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 token = token_of_proj(p);
             let last = last_of_token(token, origin);
             let map = extra_rows(token, origin, map);
             let map = add_pr(p, {origin, last}, map);
@@ -403,3 +402,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/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)
+  | Parens(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;
+    | Parens(ctx, tag) =>
+      let d1 = compose(ctx, d);
+      Parens(d1, tag) |> wrap;
     | UnOp(op, ctx) =>
       let d1 = compose(ctx, d);
       UnOp(op, d1) |> wrap;

src/haz3lcore/dynamics/Evaluator.re

@@ -41,6 +41,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_value = (f, _, x) =>
     switch (f(x)) {
     | (BoxedValue, x) => (BoxedReady, x)

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;
+      | Parens(ctx, tag) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Parens(ctx, tag) |> rewrap;
       | ListLit(ctx, ds) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         ListLit(ctx, ds) |> rewrap;
@@ -332,6 +335,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);
@@ -377,6 +382,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)
+    | (Parens(d, _), _) => matches_exp(d, f)
+    | (_, Parens(f, _)) => matches_exp(d, f)
 
     | (Constructor("$e", _), _) => failwith("$e in matched expression")
     | (Constructor("$v", _), _) => failwith("$v in matched expression")

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 ClosureEnv created by ap  */
+};
+
+/* 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};

src/haz3lcore/dynamics/Substitution.re

@@ -115,9 +115,9 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
   | TyAlias(tp, ut, d4) =>
     let d4' = subst_var(m, d1, x, d4);
     TyAlias(tp, ut, d4') |> rewrap;
-  | Parens(d4) =>
+  | Parens(d4, tag) =>
     let d4' = subst_var(m, d1, x, d4);
-    Parens(d4') |> rewrap;
+    Parens(d4', tag) |> rewrap;
   | Deferral(_) => d2
   | DeferredAp(d3, d4s) =>
     let d3 = subst_var(m, d1, x, d3);
@@ -132,33 +132,28 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
 and subst_var_env =
     (m, d1: DHExp.t, x: Var.t, env: ClosureEnvironment.t)
     : ClosureEnvironment.t => {
-  let id = env |> ClosureEnvironment.id_of;
-  let map =
-    env
-    |> ClosureEnvironment.map_of
-    |> Environment.foldo(
-         ((x', d': DHExp.t), map) => {
-           let d' =
-             switch (DHExp.term_of(d')) {
-             /* Substitute each previously substituted binding into the
-              * fixpoint. */
-             | FixF(_) =>
-               map
-               |> Environment.foldo(
-                    ((x'', d''), d) => subst_var(m, d'', x'', d),
-                    d',
-                  )
-             | _ => d'
-             };
+  Environment.foldo(
+    ((x', d': DHExp.t), map) => {
+      let d' =
+        switch (DHExp.term_of(d')) {
+        /* Substitute each previously substituted binding into the
+         * fixpoint. */
+        | FixF(_) =>
+          map
+          |> Environment.foldo(
+               ((x'', d''), d) => subst_var(m, d'', x'', d),
+               d',
+             )
+        | _ => d'
+        };
 
-           /* Substitute. */
-           let d' = subst_var(m, d1, x, d');
-           Environment.extend(map, (x', d'));
-         },
-         Environment.empty,
-       );
-
-  ClosureEnvironment.wrap(id, map);
+      /* Substitute. */
+      let d' = subst_var(m, d1, x, d');
+      Environment.extend(map, (x', d'));
+    },
+    Environment.empty,
+  )
+  |> ClosureEnvironment.update_env(_, env);
 }
 
 and subst_var_filter =

src/haz3lcore/dynamics/Transition.re

@@ -74,14 +74,7 @@ type step_kind =
   | Cast
   | RemoveTypeAlias
   | RemoveParens;
-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;
 
 type rule =
   | Step({
@@ -138,6 +131,8 @@ module type EV_MODE = {
   let otherwise: (ClosureEnvironment.t, 'a) => requirements(unit, 'a);
 
   let update_test: (state, Id.t, TestMap.instance_report) => unit;
+
+  let update_probe: (state, Id.t, Dynamics.Probe.Closure.t) => unit;
 };
 
 module Transition = (EV: EV_MODE) => {
@@ -346,13 +341,23 @@ module Transition = (EV: EV_MODE) => {
       switch (DHExp.term_of(d1')) {
       | Constructor(_) => Constructor
       | Fun(dp, d3, Some(env'), _) =>
-        let.match env'' = (env', matches(dp, d2'));
-        Step({
-          expr: Closure(env'', d3) |> fresh,
-          state_update,
-          kind: FunAp,
-          is_value: false,
-        });
+        switch (matches(dp, d2')) {
+        | IndetMatch
+        | DoesNotMatch => Indet
+        | Matches(env'') =>
+          let env'' =
+            evaluate_extend_env(
+              ~frame=Some(Term.Exp.rep_id(d)),
+              env'',
+              env',
+            );
+          Step({
+            expr: Closure(env'', d3) |> fresh,
+            state_update,
+            kind: FunAp,
+            is_value: false,
+          });
+        }
       | Cast(
           d3',
           {term: Arrow(ty1, ty2), _},
@@ -770,7 +775,26 @@ module Transition = (EV: EV_MODE) => {
     | Undefined =>
       let. _ = otherwise(env, d);
       Indet;
-    | Parens(d) =>
+    | Parens(d'', Probe(pr)) =>
+      /* When evaluated, a probe adds a dynamics info entry
+       * reflecting the evaluation of the contained expression */
+      let. _ = otherwise(env, ((d, _)) => Parens(d, Probe(pr)) |> rewrap)
+      and. (d', _) =
+        req_final_or_value(
+          req(state, env),
+          d => Parens(d, Probe(pr)) |> wrap_ctx,
+          d'',
+        );
+      Step({
+        expr: d',
+        state_update: () => {
+          let closure = Dynamics.Probe.Closure.mk(d', env, pr);
+          update_probe(state, DHExp.rep_id(d), closure);
+        },
+        kind: RemoveParens,
+        is_value: true,
+      });
+    | Parens(d, Paren) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveParens, is_value: false});
     | TyAlias(_, _, d) =>

src/haz3lcore/dynamics/TypeAssignment.re

@@ -344,7 +344,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
       None;
     };
   | TyAlias(_, _, d) => typ_of_dhexp(ctx, m, d)
-  | Parens(d) => typ_of_dhexp(ctx, m, d)
+  | Parens(d, _) => typ_of_dhexp(ctx, m, d)
   };
 };
 

src/haz3lcore/dynamics/ValueChecker.re

@@ -78,6 +78,7 @@ module ValueCheckerEVMode: {
   };
 
   let update_test = (_, _, _) => ();
+  let update_probe = (_, _, _) => ();
 };
 
 module CV = Transition(ValueCheckerEVMode);