fixed static typing, dynamic projector

hazelgrove · Nov 5, 2024 · 2dd93b0 · 2dd93b0
1 parent e195409
commit 2dd93b0
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 105 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -252,8 +252,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
     | LivelitInvocation(livelit_name) =>
       switch (Livelit.elaborate_livelit(livelit_name)) {
-      | Some((_t, uexp_f)) => uexp_f(uexp)
-      | None => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)))
+      | Some((t, uexp_f)) => uexp_f(uexp) |> cast_from(t)
+      | None =>
+        print_endline("Livelit not found");
+        uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)));
       }
     | Constructor(c, _) =>
       let mode =

diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -231,7 +231,7 @@ and uexp_to_info_map =
   | Int(_) => atomic(Just(Int |> Typ.temp))
   | Float(_) => atomic(Just(Float |> Typ.temp))
   | String(_) => atomic(Just(String |> Typ.temp))
-  | LivelitInvocation(_) => atomic(Just(String |> Typ.temp))
+  | LivelitInvocation(name) => atomic(Just(Livelit.get_livelit_type(name)))
   | ListLit(es) =>
     let ids = List.map(UExp.rep_id, es);
     let modes = Mode.of_list_lit(ctx, List.length(es), mode);

diff --git a/src/haz3lcore/zipper/projectors/LivelitProj.re b/src/haz3lcore/zipper/projectors/LivelitProj.re
@@ -2,120 +2,35 @@ open Util;
 open Virtual_dom.Vdom;
 open ProjectorBase;
 
-let of_id = (id: Id.t) =>
-  "id" ++ (id |> Id.to_string |> String.sub(_, 0, 8));
+let put: string => Piece.t = Piece.mk_mono(Exp);
 
-let of_mono = (syntax: Piece.t): option(string) =>
-  switch (syntax) {
-  | Tile({label: [l], _}) => Some(StringUtil.unescape_linebreaks(l))
-  | _ => None
-  };
-
-let mk_mono = (sort: Sort.t, string: string): Piece.t =>
-  string
-  |> StringUtil.escape_linebreaks
-  |> Form.mk_atomic(sort)
-  |> Piece.mk_tile(_, []);
+let get_opt = (piece: Piece.t): option(string) =>
+  piece |> Piece.of_mono |> Option.map(Form.parse_livelit);
 
 let get = (piece: Piece.t): string =>
-  switch (piece |> of_mono) {
-  | None => failwith("TextArea: not string literal")
+  switch (get_opt(piece)) {
+  | None => failwith("ERROR: Slider: not integer literal")
   | Some(s) => s
   };
 
-let put = (s: string): Piece.t => s |> mk_mono(Exp);
-
-let put = (str: string): external_action =>
-  SetSyntax(str |> Form.string_quote |> put);
-
-let is_last_pos = id =>
-  Web.TextArea.caret_at_end(Web.TextArea.get(of_id(id)));
-let is_first_pos = id =>
-  Web.TextArea.caret_at_start(Web.TextArea.get(of_id(id)));
-
-let key_handler = (id, ~parent, evt) => {
-  open Effect;
-  let key = Key.mk(KeyDown, evt);
-
-  switch (key.key) {
-  | D("ArrowRight" | "ArrowDown") when is_last_pos(id) =>
-    JsUtil.get_elem_by_id(of_id(id))##blur;
-    Many([parent(Escape(Right)), Stop_propagation]);
-  | D("ArrowLeft" | "ArrowUp") when is_first_pos(id) =>
-    JsUtil.get_elem_by_id(of_id(id))##blur;
-    Many([parent(Escape(Left)), Stop_propagation]);
-  /* Defer to parent editor undo for now */
-  | D("z" | "Z" | "y" | "Y") when Key.ctrl_held(evt) || Key.meta_held(evt) =>
-    Many([Prevent_default])
-  | D("z" | "Z")
-      when Key.shift_held(evt) && (Key.ctrl_held(evt) || Key.meta_held(evt)) =>
-    Many([Prevent_default])
-  | D("\"") =>
-    /* Hide quotes from both the textarea and parent editor */
-    Many([Prevent_default, Stop_propagation])
-  | _ => Stop_propagation
-  };
-};
-
-let textarea =
-    (id, ~parent: external_action => Ui_effect.t(unit), text: string) =>
-  Node.textarea(
-    ~attrs=[
-      Attr.id(of_id(id)),
-      Attr.on_keydown(key_handler(id, ~parent)),
-      Attr.on_input((_, new_text) =>
-        Effect.(Many([parent(put(new_text))]))
-      ),
-      /* Note: adding these handlers below because
-       * currently these are handled on page level.
-       * unnecesary maybe if we move handling down */
-      Attr.on_copy(_ => Effect.Stop_propagation),
-      Attr.on_cut(_ => Effect.Stop_propagation),
-      Attr.on_paste(_ => Effect.Stop_propagation),
-      Attr.string_property("value", text),
-    ],
-    [],
-  );
-
-let view = (_, ~info, ~local as _, ~parent) => {
-  let text = info.syntax |> get |> Form.strip_quotes;
-  Node.div(
-    ~attrs=[Attr.classes(["wrapper"])],
-    [
-      Node.div(
-        ~attrs=[Attr.classes(["cols", "code"])],
-        [Node.text("I am a livelit projector")],
-      ),
-    ],
-  );
-};
-
 module M: Projector = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model = unit;
   [@deriving (show({with_path: false}), sexp, yojson)]
   type action = unit;
   let init = ();
-  let can_project = _ => true; //TODO(andrew): restrict somehow
-  let can_focus = true;
-  let placeholder = (_, info) => {
-    let str = Form.strip_quotes(get(info.syntax));
-    Block({
-      row: StringUtil.num_lines(str),
-      /* +2 for left and right padding */
-      col: 2 + StringUtil.max_line_width(str),
-    });
-  };
+  let can_project = p => get_opt(p) != None;
+  let can_focus = false;
+  let placeholder = (_, _) => Inline(10);
   let update = (model, _) => model;
-  let view = view;
-  let focus = ((id: Id.t, d: option(Direction.t))) => {
-    JsUtil.get_elem_by_id(of_id(id))##focus;
-    switch (d) {
-    | None => ()
-    | Some(Left) =>
-      Web.TextArea.set_caret_to_start(Web.TextArea.get(of_id(id)))
-    | Some(Right) =>
-      Web.TextArea.set_caret_to_end(Web.TextArea.get(of_id(id)))
-    };
+  let view =
+      (_, ~info, ~local as _, ~parent: external_action => Ui_effect.t(unit)) => {
+    let llname = get(info.syntax);
+    print_endline("Livelit: " ++ llname);
+    Node.div(
+      ~attrs=[Attr.class_("livelit")],
+      [Node.text("Livelit: " ++ llname)],
+    );
   };
+  let focus = _ => ();
 };