Skip to content

Commit

Permalink
fixed carot parsing, added livelit projector, elaboration
Browse files Browse the repository at this point in the history
  • Loading branch information
gcrois committed Oct 30, 2024
1 parent 269c540 commit 20b6aef
Show file tree
Hide file tree
Showing 10 changed files with 151 additions and 39 deletions.
9 changes: 6 additions & 3 deletions src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
Expand Up @@ -115,8 +115,7 @@ let rec elaborate_pattern =
| Bool(_) => upat |> cast_from(Bool |> Typ.temp)
| Float(_) => upat |> cast_from(Float |> Typ.temp)
| String(_) => upat |> cast_from(String |> Typ.temp)
| LivelitInvocation(_) =>
upat |> cast_from(Unknown(Internal) |> Typ.temp)
| LivelitInvocation(_) => upat |> cast_from(String |> Typ.temp)
| ListLit(ps) =>
let (ps, tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip;
let inner_type =
Expand Down Expand Up @@ -251,7 +250,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
|> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
let ds' = List.map2((d, t) => fresh_cast(d, t, inner_type), ds, tys);
Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
| LivelitInvocation(_) => uexp |> cast_from(String |> Typ.temp)
| LivelitInvocation(livelit_name) =>
switch (Livelit.elaborate_livelit(livelit_name)) {
| Some(t) => uexp |> cast_from(t)
| None => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)))
}
| Constructor(c, _) =>
let mode =
switch (Id.Map.find_opt(Exp.rep_id(uexp), m)) {
Expand Down
13 changes: 1 addition & 12 deletions src/haz3lcore/lang/Form.re
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ let is_potential_operand = match(regexp("^[\\^a-zA-Z0-9_'\\.?]+$"));
* delimiters, string delimiters, or the instant expanding paired
* delimiters: ()[]| */
let potential_operator_regexp =
regexp("^[^a-zA-Z0-9_'?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
regexp("^[\\^a-zA-Z0-9_'?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
let is_potential_operator = match(potential_operator_regexp);
let is_potential_token = t =>
is_potential_operand(t)
Expand Down Expand Up @@ -153,8 +153,6 @@ let is_undefined = match(regexp("^" ++ undefined ++ "$"));
let is_livelit = str => {
let re = regexp("^(\\^)([a-z][A-Za-z0-9_]*)$");
let result = match(re, str);
print_endline("is_livelit: " ++ str ++ " " ++ string_of_bool(result));

result;
};
let parse_livelit = str =>
Expand Down Expand Up @@ -360,8 +358,6 @@ let delims: list(Token.t) =

let atomic_molds: Token.t => list(Mold.t) =
s => {
print_endline("atomic_molds");
print_endline(s);
List.fold_left(
(acc, (_, (test, molds))) => test(s) ? molds @ acc : acc,
[],
Expand All @@ -370,23 +366,16 @@ let atomic_molds: Token.t => list(Mold.t) =
};

let is_atomic = t => {
print_endline("is_atomic");
print_endline(t);
atomic_molds(t) != [];
};

let is_delim = t => List.mem(t, delims);

let is_valid_token = t => {
print_endline("is_valid_token");
print_endline(t);
is_atomic(t) || is_secondary(t) || is_delim(t);
};

let mk_atomic = (sort: Sort.t, t: Token.t) => {
print_endline("mk_atomic");
print_endline(t);

assert(is_atomic(t));
mk(ss, [t], Mold.(mk_op(sort, [])));
};
3 changes: 0 additions & 3 deletions src/haz3lcore/lang/Molds.re
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,6 @@ let forms_assoc: list((Label.t, list(Mold.t))) =
);

let get = (label: Label.t): list(Mold.t) => {
print_endline("Molds.get");
print_endline(String.concat(" ", label));

switch (label, List.assoc_opt(label, forms_assoc)) {
| ([t], Some(molds)) when Form.atomic_molds(t) != [] =>
Form.atomic_molds(t) @ molds
Expand Down
3 changes: 2 additions & 1 deletion src/haz3lcore/tiles/Base.re
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,8 @@ type kind =
| Checkbox
| Slider
| SliderF
| TextArea;
| TextArea
| Livelit;

[@deriving (show({with_path: false}), sexp, yojson, eq)]
type segment = list(piece)
Expand Down
31 changes: 12 additions & 19 deletions src/haz3lcore/tiles/Livelit.re
Original file line number Diff line number Diff line change
Expand Up @@ -5,46 +5,39 @@ type t = {
name: string,
width: int,
default: Pat.term,
expansion_type: Typ.cls,
expansion_type: Typ.t,
};

type state = Id.Map.t(DHExp.t);
let empty_state: state = Id.Map.empty;
type state = Id.Map.t(t);
let slider: t = {
name: "llslider\t",
name: "slider\t",
width: 10,
default: Int(30),
expansion_type: Int,
expansion_type: Typ.temp(Typ.Int),
};

let checkbox: t = {
name: "llcheckbox\t",
name: "checkbox\t",
width: 1,
default: Bool(false),
expansion_type: Bool,
expansion_type: Typ.temp(Typ.Bool),
};

let fslider: t = {
name: "llfslider\t",
name: "fslider\t",
width: 10,
default: Float(0.5),
expansion_type: Float,
expansion_type: Typ.temp(Typ.Float),
};

let livelits: list(t) = [checkbox, fslider, slider];

let find_livelit = (livelit_name: string): option(t) =>
List.find_opt(l => l.name == livelit_name, livelits);

let elaborate_livelit =
(livelit_name: string, uexp_id: Uuidm.t, livelits: state)
: option(Pat.term) => {
switch (Id.Map.find_opt(uexp_id, livelits)) {
// | Some(t) => Some(t)
| _ =>
switch (find_livelit(livelit_name)) {
| Some(l) => Some(l.default)
| None => None
}
let elaborate_livelit = (livelit_name: string): option(Typ.t) => {
switch (find_livelit(livelit_name)) {
| Some(l) => Some(l.expansion_type)
| None => None
};
};
1 change: 1 addition & 0 deletions src/haz3lcore/zipper/Projector.re
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ let to_module = (kind: Base.kind): (module Cooked) =>
| SliderF => (module Cook(SliderFProj.M))
| Checkbox => (module Cook(CheckboxProj.M))
| TextArea => (module Cook(TextAreaProj.M))
| Livelit => (module Cook(LivelitProj.M))
};

let shape = (p: Base.projector, info: info): shape => {
Expand Down
121 changes: 121 additions & 0 deletions src/haz3lcore/zipper/projectors/LivelitProj.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,121 @@
open Util;
open Virtual_dom.Vdom;
open ProjectorBase;

let of_id = (id: Id.t) =>
"id" ++ (id |> Id.to_string |> String.sub(_, 0, 8));

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 = (piece: Piece.t): string =>
switch (piece |> of_mono) {
| None => failwith("TextArea: not string 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 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)))
};
};
};
3 changes: 2 additions & 1 deletion src/haz3lcore/zipper/projectors/TextAreaProj.re
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,8 @@ let view = (_, ~info, ~local as _, ~parent) => {
[
Node.div(
~attrs=[Attr.classes(["cols", "code"])],
[Node.text("·")] @ [textarea(info.id, ~parent, text)],
[Node.text("I am a livelit projector")]
@ [textarea(info.id, ~parent, text)],
),
],
);
Expand Down
4 changes: 4 additions & 0 deletions src/haz3lweb/view/ProjectorView.re
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ let name = (p: kind): string =>
| Checkbox => "check"
| Slider => "slider"
| SliderF => "sliderf"
| Livelit => "livelit"
| TextArea => "text"
};

Expand All @@ -32,6 +33,7 @@ let of_name = (p: string): kind =>
| "check" => Checkbox
| "slider" => Slider
| "sliderf" => SliderF
| "livelit" => Livelit
| "text" => TextArea
| _ => failwith("Unknown projector kind")
};
Expand Down Expand Up @@ -215,6 +217,8 @@ module Panel = {
| Pat(Float) => [SliderF]
| Exp(String)
| Pat(String) => [TextArea]
| Exp(LivelitInvocation)
| Pat(LivelitInvocation) => [Livelit]
| _ => []
}
)
Expand Down
2 changes: 2 additions & 0 deletions src/util/Web.re
Original file line number Diff line number Diff line change
Expand Up @@ -134,3 +134,5 @@ module TextArea = {
textarea##.selectionEnd := content_length;
};
};

let span_text = (text: string) => span(~attrs=[], [Node.text(text)]);

0 comments on commit 20b6aef

Please sign in to comment.