Assistant Plus

src/haz3lcore/Hyper.re

@@ -0,0 +1,5 @@
+let export_id =
+  "10000137-0000-0000-0000-000000000000" |> Uuidm.of_string |> Option.get;
+
+let export_str = "EXPORT";
+let is_export = (==)(export_str);

src/haz3lcore/Measured.re

@@ -407,27 +407,44 @@ let length = (seg: Segment.t, map: t): int =>
     last.last.col - first.origin.col;
   };
 
-let segment_origin = (seg: Segment.t): option(Point.t) =>
-  Option.map(
-    first => find_p(first, of_segment(seg)).origin,
-    ListUtil.hd_opt(seg),
-  );
-
-let segment_last = (seg: Segment.t): option(Point.t) =>
-  Option.map(
-    last => find_p(last, of_segment(seg)).last,
-    ListUtil.last_opt(seg),
-  );
-
-let segment_height = (seg: Segment.t) =>
-  switch (segment_last(seg), segment_origin(seg)) {
-  | (Some(last), Some(first)) => 1 + last.row - first.row
-  | _ => 0
-  };
+let height = (m: t): int => IntMap.cardinal(m.rows);
+
+let width = (m: t): int =>
+  IntMap.fold((_, {max_col, _}: Rows.shape) => max(max_col), m.rows, 0);
+
+let segment_height = (seg: Segment.t) => seg |> of_segment |> height;
+
+let segment_width = (seg: Segment.t): int => seg |> of_segment |> width;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type piece_path = list(int);
+
+let fold_lefti = (f, acc, seg) =>
+  List.fold_left2(f, acc, seg, List.init(List.length(seg), Fun.id));
 
-let segment_width = (seg: Segment.t): int =>
-  IntMap.fold(
-    (_, {max_col, _}: Rows.shape, acc) => max(max_col, acc),
-    of_segment(seg).rows,
-    0,
-  );
+[@deriving (show({with_path: false}), sexp, yojson)]
+let path_map = (seg: Segment.t): Id.Map.t(piece_path) => {
+  //NOTE: paths will be in reverse order
+  let rec go = (path: piece_path, map: Id.Map.t(piece_path), seg: Segment.t) =>
+    fold_lefti(
+      (map, p: Piece.t, idx: int) => {
+        let path = [idx, ...path];
+        let map = Id.Map.add(Piece.id(p), path, map);
+        let map =
+          switch (p) {
+          | Secondary(_)
+          | Grout(_) => map
+          | Tile(t) =>
+            fold_lefti(
+              (map, child, idx) => go([idx, ...path], map, child),
+              map,
+              t.children,
+            )
+          };
+        map;
+      },
+      map,
+      seg,
+    );
+  go([], Id.Map.empty, seg);
+};

src/haz3lcore/assistant/TyDi.re

@@ -91,6 +91,12 @@ let set_buffer = (~settings, ~ctx: Ctx.t, z: Zipper.t): option(Zipper.t) => {
   let* tok_to_left = token_to_left(z);
   let* ci = z_to_ci(~settings, ~ctx, z);
   let suggestions = suggest(ci, z);
+  /*print_endline("suggestions:");
+    print_endline(
+      suggestions
+      |> List.map((s: Suggestion.t) => s.content)
+      |> String.concat(", "),
+    );*/
   let suggestions =
     suggestions
     |> List.filter(({content, _}: Suggestion.t) =>

src/haz3lcore/dynamics/Builtins.re

@@ -276,12 +276,52 @@ module Pervasives = {
     |> fn("string_sub", Arrow(Prod([String, Int, Int]), String), string_sub);
 };
 
+let styles: Typ.sum_map =
+  [
+    ("AlignItems", Some(Typ.String)),
+    ("BackgroundColor", Some(String)),
+    ("Border", Some(String)),
+    ("BorderRadius", Some(String)),
+    ("BoxShadow", Some(String)),
+    ("Color", Some(String)),
+    ("Cursor", Some(String)),
+    ("Display", Some(String)),
+    ("FlexDirection", Some(String)),
+    ("FontFamily", Some(String)),
+    ("FontSize", Some(String)),
+    ("FontStyle", Some(String)),
+    ("Gap", Some(String)),
+    ("Height", Some(String)),
+    ("JustifyContent", Some(String)),
+    ("Margin", Some(String)),
+    ("Opacity", Some(String)),
+    ("Outline", Some(String)),
+    ("Overflow", Some(String)),
+    ("Padding", Some(String)),
+    ("Position", Some(String)),
+    ("Width", Some(String)),
+    ("S", Some(Prod([String, String]))),
+  ]
+  |> ConstructorMap.of_list;
+
+let add_alias = (name, ty, ctx: Ctx.t) =>
+  Ctx.extend_alias(ctx, name, Id.invalid, ty);
+
+let add_constructors = (name, sum_map: Typ.sum_map, ctx: Ctx.t) =>
+  Ctx.add_ctrs(ctx, name, Id.invalid, sum_map);
+
+let add_sum_alias = (name: string, sum_map: Typ.sum_map, ctx: Ctx.t) =>
+  ctx |> add_alias(name, Sum(sum_map)) |> add_constructors(name, sum_map);
+
+let mvu_builtins: Ctx.t = add_sum_alias("StyleAttr", styles, []);
+
 let ctx_init: Ctx.t =
-  List.map(
-    ((name, Builtin.{typ, _})) =>
-      Ctx.VarEntry({name, typ, id: Id.invalid}),
-    Pervasives.builtins,
-  );
+  mvu_builtins
+  @ List.map(
+      ((name, Builtin.{typ, _})) =>
+        Ctx.VarEntry({name, typ, id: Id.invalid}),
+      Pervasives.builtins,
+    );
 
 let forms_init: forms =
   List.map(

src/haz3lcore/dynamics/DH.re

@@ -1,6 +1,11 @@
 open Sexplib.Std;
 
 module rec DHExp: {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type monitor =
+    | Test
+    | Probe;
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | EmptyHole(MetaVar.t, HoleInstanceId.t)
@@ -17,7 +22,7 @@ module rec DHExp: {
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
     | ApBuiltin(string, list(t))
-    | TestLit(KeywordID.t)
+    | Monitor(monitor, Id.t)
     | BoolLit(bool)
     | IntLit(int)
     | FloatLit(float)
@@ -52,6 +57,11 @@ module rec DHExp: {
 
   let fast_equal: (t, t) => bool;
 } = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type monitor =
+    | Test
+    | Probe;
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     /* Hole types */
@@ -71,7 +81,7 @@ module rec DHExp: {
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
     | ApBuiltin(string, list(t))
-    | TestLit(KeywordID.t)
+    | Monitor(monitor, Id.t)
     | BoolLit(bool)
     | IntLit(int)
     | FloatLit(float)
@@ -110,7 +120,8 @@ module rec DHExp: {
     | Closure(_, _) => "Closure"
     | Ap(_, _) => "Ap"
     | ApBuiltin(_, _) => "ApBuiltin"
-    | TestLit(_) => "TestLit"
+    | Monitor(Test, _) => "TestLit"
+    | Monitor(Probe, _) => "Probe"
     | BoolLit(_) => "BoolLit"
     | IntLit(_) => "IntLit"
     | FloatLit(_) => "FloatLit"
@@ -185,7 +196,7 @@ module rec DHExp: {
     | FreeVar(_) as d
     | InvalidText(_) as d
     | BoundVar(_) as d
-    | TestLit(_) as d
+    | Monitor(_) as d
     | BoolLit(_) as d
     | IntLit(_) as d
     | FloatLit(_) as d
@@ -199,7 +210,7 @@ module rec DHExp: {
     /* Primitive forms: regular structural equality */
     | (BoundVar(_), _)
     /* TODO: Not sure if this is right... */
-    | (TestLit(_), _)
+    | (Monitor(_), _)
     | (BoolLit(_), _)
     | (IntLit(_), _)
     | (FloatLit(_), _)

src/haz3lcore/dynamics/Elaborator.re

@@ -97,7 +97,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | BinIntOp(_)
     | BinFloatOp(_)
     | BinStringOp(_)
-    | TestLit(_) => DHExp.cast(d, self_ty, ana_ty)
+    | Monitor(_) => DHExp.cast(d, self_ty, ana_ty)
     };
   };
 
@@ -116,20 +116,31 @@ let wrap = (ctx: Ctx.t, u: Id.t, mode: Mode.t, self, d: DHExp.t): DHExp.t =>
   };
 
 let rec dhexp_of_uexp =
-        (m: Statics.Map.t, uexp: Term.UExp.t): option(DHExp.t) => {
+        (~probe_ids, m: Statics.Map.t, uexp: Term.UExp.t): option(DHExp.t) => {
+  let dhexp_of_uexp = dhexp_of_uexp(~probe_ids);
   switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) {
-  | Some(InfoExp({mode, self, ctx, _})) =>
+  | Some(InfoExp({mode, self, ctx, ancestors, _})) =>
     let err_status = Info.status_exp(ctx, mode, self);
     let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */
     let+ d: DHExp.t =
       switch (uexp.term) {
       | Invalid(t) => Some(DHExp.InvalidText(id, 0, t))
       | EmptyHole => Some(DHExp.EmptyHole(id, 0))
       | MultiHole(_tms) =>
+        let+ ds =
+          _tms
+          |> List.map(
+               fun
+               | Term.Exp(t) => dhexp_of_uexp(m, t)
+               | _ => Some(EmptyHole(id, 0)),
+             )
+          |> OptUtil.sequence;
+        //TODO(andrew): turning this into tuples for now; yolo
         /* TODO: add a dhexp case and eval logic for multiholes.
            Make sure new dhexp form is properly considered Indet
            to avoid casting issues. */
-        Some(EmptyHole(id, 0))
+        //Some(EmptyHole(id, 0))
+        DHExp.Tuple(ds);
       | Triv => Some(Tuple([]))
       | Bool(b) => Some(BoolLit(b))
       | Int(n) => Some(IntLit(n))
@@ -184,14 +195,16 @@ let rec dhexp_of_uexp =
         DHExp.Sequence(d1, d2);
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
-        DHExp.Ap(TestLit(id), dtest);
+        DHExp.Ap(Monitor(Test, id), dtest);
       | Var(name) =>
         switch (err_status) {
         | InHole(FreeVariable(_)) => Some(FreeVar(id, 0, name))
         | _ => Some(BoundVar(name))
         }
       | Constructor(name) =>
         switch (err_status) {
+        | _ when Hyper.is_export(name) =>
+          Some(DHExp.Ap(Monitor(Test, Hyper.export_id), Tuple([])))
         | InHole(Common(NoType(FreeConstructor(_)))) =>
           Some(FreeVar(id, 0, name))
         | _ => Some(Constructor(name))
@@ -237,6 +250,50 @@ let rec dhexp_of_uexp =
                );
           Let(dp, FixF(self_id, ty_body, substituted_def), dbody);
         };
+      | Ap(
+          {term: Constructor("Stage"), _},
+          {term: Tuple([update, model]), _},
+        ) =>
+        let id_str = Term.UExp.rep_id(uexp) |> Id.to_string;
+        let body: Term.UExp.t = {
+          term:
+            Ap(
+              {term: Constructor("Inject"), ids: [Id.mk()]},
+              {
+                term:
+                  Tuple([
+                    {term: String(id_str), ids: [Id.mk()]},
+                    update,
+                    {term: Var("action"), ids: [Id.mk()]},
+                  ]),
+                ids: [Id.mk()],
+              },
+            ),
+          ids: [Id.mk()],
+        };
+        let inject: Term.UExp.t = {
+          term: Fun({term: Var("action"), ids: [Id.mk()]}, body),
+          ids: [Id.mk()],
+        };
+        //TODO(andrew): include actual stage ids / ana type somewhere?
+        let ret: Term.UExp.t = {
+          term: Tuple([model, inject]),
+          ids: [Id.mk()],
+        };
+        //(<init_model>, fun (action:Action) -> Inject(Int(<init_model>.uuid), <update>, action)
+        /*let* update = dhexp_of_uexp(m, update);
+          let+ model = dhexp_of_uexp(m, model);
+          let body =
+            DHExp.Ap(
+              Constructor("Inject"),
+              Tuple([StringLit(id_str), update, BoundVar("action")]),
+            );
+          let inject =
+            DHExp.Fun(Var("action"), Unknown(Internal), body, None);
+          DHExp.Tuple([model, inject]);*/
+        let (_, m_new) =
+          Statics.uexp_to_info_map(~ctx, ~mode, ~ancestors, ret, m);
+        dhexp_of_uexp(m_new, ret);
       | Ap(fn, arg) =>
         let* c_fn = dhexp_of_uexp(m, fn);
         let+ c_arg = dhexp_of_uexp(m, arg);
@@ -273,9 +330,21 @@ let rec dhexp_of_uexp =
         };
       | TyAlias(_, _, e) => dhexp_of_uexp(m, e)
       };
-    wrap(ctx, id, mode, self, d);
-  | Some(InfoPat(_) | InfoTyp(_) | InfoTPat(_))
-  | None => None
+    let d = wrap(ctx, id, mode, self, d);
+    /* Wrap with probe if indicated by id */
+    List.mem(id, probe_ids) ? DHExp.Ap(Monitor(Probe, id), d) : d;
+  | Some((InfoPat(_) | InfoTyp(_) | InfoTPat(_)) as ci) =>
+    Printf.printf(
+      "Elaborate: Exp: Infomap returned wrong sort: %s\n",
+      Info.show(ci),
+    );
+    None;
+  | None =>
+    Printf.printf(
+      "Elaborate: Exp: Infomap lookup failed for: %s\n",
+      Id.to_string(Term.UExp.rep_id(uexp)),
+    );
+    None;
   };
 }
 and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
@@ -332,22 +401,35 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
       let* dp = dhpat_of_upat(m, p);
       wrap(dp);
     };
-  | Some(InfoExp(_) | InfoTyp(_) | InfoTPat(_))
-  | None => None
+  | Some((InfoExp(_) | InfoTyp(_) | InfoTPat(_)) as ci) =>
+    Printf.printf(
+      "Elaborate: Pat: Infomap returned wrong sort: %s\n",
+      Info.show(ci),
+    );
+    None;
+  | None =>
+    Printf.printf(
+      "Elaborate: Pat: Infomap lookup failed for: %s\n",
+      Id.to_string(Term.UPat.rep_id(upat)),
+    );
+    None;
   };
 };
 
-//let dhexp_of_uexp = Core.Memo.general(~cache_size_bound=1000, dhexp_of_uexp);
-
-let uexp_elab = (m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
-  switch (dhexp_of_uexp(m, uexp)) {
+let uexp_elab =
+    (~probe_ids=[], m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
+  switch (dhexp_of_uexp(~probe_ids, m, uexp)) {
   | None => DoesNotElaborate
   | Some(d) =>
-    //let d = uexp_elab_wrap_builtins(d);
     let ty =
       switch (fixed_exp_typ(m, uexp)) {
       | Some(ty) => ty
       | None => Typ.Unknown(Internal)
       };
     Elaborates(d, ty, Delta.empty);
   };
+
+//TODO(andrew): cleanup
+let uexp_elab' =
+    (probe_ids, m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
+  uexp_elab(~probe_ids, m, uexp);