Skip to content

Commit

Permalink
projectors live cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Dec 16, 2024
1 parent dc8ebfe commit d64e739
Show file tree
Hide file tree
Showing 12 changed files with 60 additions and 478 deletions.
21 changes: 7 additions & 14 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
Expand Up @@ -123,16 +123,9 @@ let return = (wrap, ids, tm) => {
let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty);

/* Strip a projector from a segment and log it in the map */
let log_projectors = (seg: Segment.t): Segment.t =>
List.map(
fun
| Piece.Projector(pr) => {
projectors := Id.Map.add(pr.id, pr, projectors^);
Piece.Projector(pr);
}
| x => x,
seg,
);
let log_projector = (pr: Base.projector): unit => {
projectors := Id.Map.add(pr.id, pr, projectors^);
};

let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) =
fun
Expand Down Expand Up @@ -367,7 +360,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
| ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
Invalid(t)
| (["(", ")"], [Pat(body)]) => Parens(body)
| (label, [Pat(body)]) when is_probe_wrap(label) => Parens(body)
| (label, [Pat(body)]) when is_probe_wrap(label) => body.term
| (["[", "]"], [Pat(body)]) =>
switch (body) {
| {term: Tuple(ps), _} => ListLit(ps)
Expand Down Expand Up @@ -428,7 +421,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
| (["String"], []) => String
| ([t], []) when Form.is_typ_var(t) => Var(t)
| (["(", ")"], [Typ(body)]) => Parens(body)
| (label, [Typ(body)]) when is_probe_wrap(label) => Parens(body)
| (label, [Typ(body)]) when is_probe_wrap(label) => body.term
| (["[", "]"], [Typ(body)]) => List(body)
| ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
Unknown(Hole(Invalid(t)))
Expand Down Expand Up @@ -538,12 +531,12 @@ and rul = (unsorted: unsorted): Rul.t => {
and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
/* Remove projectors. We do this here as opposed to removing
* them in an external call to save a whole-syntax pass. */
let _ = log_projectors(seg);
let tile_kids = (p: Piece.t): list(Term.Any.t) =>
switch (p) {
| Secondary(_)
| Grout(_) => []
| Projector({syntax, id: _, _}) =>
| Projector({syntax, id: _, _} as pr) =>
let _ = log_projector(pr);
let sort = Piece.sort(syntax) |> fst;
[go_s(sort, Segment.skel([syntax]), [syntax])];
| Tile({mold, shards, children, _}) =>
Expand Down
2 changes: 1 addition & 1 deletion src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
itself is dedicated to the piping necessary to (A) introduce and
(B) propagate the necessary information through the syntax tree.
*/
*/

module Info = Info;

Expand Down
10 changes: 0 additions & 10 deletions src/haz3lcore/tiles/Piece.re
Original file line number Diff line number Diff line change
Expand Up @@ -186,13 +186,3 @@ let is_term = (p: t) =>
| Secondary(_) => false // debatable
| _ => false
};

let mk_tile_id: (Id.t, Form.t, list(list(t))) => t =
(id, form, children) =>
Tile({
id,
label: form.label,
mold: form.mold,
shards: List.mapi((i, _) => i, form.label),
children,
});
36 changes: 2 additions & 34 deletions src/haz3lcore/zipper/projectors/ProbeProj.re
Original file line number Diff line number Diff line change
Expand Up @@ -4,25 +4,6 @@ open Virtual_dom.Vdom;
open Node;
open Js_of_ocaml;

//let _ = Zipper.base_point; //not cyclical
//let _ = Editor.show; //cyclical

/* Plan for extended dynamics:
in principle we could track:
- prev 'stack frame': id of prev expr that began execution?
- env (or just the part of the env that's relevant to the current expr)
aka the co-ctx
*/

/* Plan for selectable (editable as well maybe):
selectable:
create own mini version of editor, use it as model
update fn updates model after applying mini editor action
hopefully can use same actions
*/

[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
[@default "⋱"]
Expand Down Expand Up @@ -96,22 +77,15 @@ let get_goal = (utility: utility, e: Js.t(Dom_html.mouseEvent)) =>
let resizable_val =
(~resizable=false, model, utility, local, pi: Dynamics.Probe.Info.t) => {
let val_pointerdown = (e: Js.t(Dom_html.pointerEvent)) => {
// print_endline("pointerdown");
let target = e##.target |> Js.Opt.get(_, _ => failwith("no target"));
JsUtil.setPointerCapture(target, e##.pointerId) |> ignore;
mousedown := Some(target);
// if (last_target^ == [target] && !Js.to_bool(e##.shiftKey)) {
// env_cursor := [];
// last_target := [];
// } else {
env_cursor := Probe.env_stack(pi.stack);
last_target := [target];
// };
Effect.Ignore;
};

let val_pointerup = (e: Js.t(Dom_html.pointerEvent)) => {
// print_endline("pointerup");
switch (mousedown^) {
| Some(target) =>
JsUtil.releasePointerCapture(target, e##.pointerId) |> ignore
Expand All @@ -128,10 +102,7 @@ let resizable_val =
/* Ideally we could just use hasPointerCapture... */
let goal = get_goal(utility, e);
local(ChangeLength(goal.col));
// print_endline("mousemove: resizing");
| _ =>
// print_endline("mousemove: not resizing");
Effect.Ignore
| _ => Effect.Ignore
};

div(
Expand All @@ -145,10 +116,7 @@ let resizable_val =
Attr.on_pointerup(val_pointerup),
Attr.on_mousemove(val_mousemove),
],
[
seg_view(utility, model.len, pi.value),
//, text(stack(pi.stack))
],
[seg_view(utility, model.len, pi.value)],
);
};

Expand Down
2 changes: 0 additions & 2 deletions src/haz3lweb/app/explainthis/Example.re
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,6 @@ let int = n => mk_monotile(Form.mk_atomic(Exp, n));
let exp = v => mk_monotile(Form.mk_atomic(Exp, v));
let pat = v => mk_monotile(Form.mk_atomic(Pat, v));
let mk_parens_exp = mk_tile(Form.get("parens_exp"));
let mk_probe = (e: list(Piece.t)) =>
mk_tile(Form.mk(Form.ii, ["@@", "@@"], Mold.mk_op(Exp, [Exp])), [e]);
let mk_fun = mk_tile(Form.get("fun_"));
let mk_fun_ancestor = mk_ancestor(Form.get("fun_"));
let mk_parens_ancestor = mk_ancestor(Form.get("parens_exp"));
Expand Down
111 changes: 44 additions & 67 deletions src/haz3lweb/app/inspector/ProjectorPanel.re
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,7 @@ open Projector;
open Util.OptUtil.Syntax;
open Util.Web;

/* The projector selection panel on the right of the bottom bar */
let option_view = (_name, n) =>
option([
//~attrs=n == name ? [Attr.create("selected", "selected")] : [],
text(n),
]);
// The projector selection panel on the right of the bottom bar

/* Decide which projectors are applicable based on the cursor info.
* This is slightly inside-out as elsewhere it depends on the underlying
Expand Down Expand Up @@ -100,74 +95,56 @@ let might_project: Cursor.cursor(Editors.Update.t) => bool =
}
};

let currently_selected = editor =>
option_view(
switch (kind(editor)) {
| None => "fold"
| Some(k) => ProjectorView.name(k)
},
);

let currently_selected_str = (editor, _): string =>
switch (kind(editor)) {
| None => "fold"
| Some(k) => ProjectorView.name(k)
};
let lift = (str, strs) => List.cons(str, List.filter((!=)(str), strs));

let currently_selected_str_opt = (editor, _): option(string) =>
switch (kind(editor)) {
| None => None
| Some(k) => Some(ProjectorView.name(k))
/* The string names of all projectors applicable to the currently
* indicated syntax, with the currently applied projection (if any)
* lifted to the top of the list */
let applicable_projector_strings = (cursor: Cursor.cursor(Editors.Update.t)) => {
let strs =
applicable_projectors(cursor.info) |> List.map(ProjectorView.name);
switch (kind(cursor.editor)) {
| None => strs
| Some(k) => lift(ProjectorView.name(k), strs)
};
};

let view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => {
let applicable_projectors = applicable_projectors(cursor.info);
let should_show = might_project(cursor) && applicable_projectors != [];
//TODO(andrew): cleanup
// print_endline("currentrly: " ++ currently_selected_str(cursor.editor, ()));
let applicable_projector_strings =
(might_project(cursor) ? applicable_projectors : [Fold])
|> List.map(ProjectorView.name);
/* A selection input for contetually applicable projectors */
let select_view =
(
~inject: Action.project => Ui_effect.t(unit),
cursor: Cursor.cursor(Editors.Update.t),
) => {
let applicable_projector_strings =
switch (currently_selected_str_opt(cursor.editor, ())) {
| None => applicable_projector_strings
| Some(guy) =>
List.cons(
guy,
List.filter(x => x != guy, applicable_projector_strings),
)
};
might_project(cursor) ? applicable_projector_strings(cursor) : [];
let value =
switch (kind(cursor.editor)) {
| Some(k) => ProjectorView.name(k)
| None =>
applicable_projector_strings
//|> List.map(currently_selected_str(cursor.editor))
|> List.hd
switch (applicable_projector_strings) {
| [] => ""
| [hd, ..._] => hd
};
// print_endline("value: " ++ value);
let select_view =
Node.select(
~attrs=[
Attr.on_change((_, name) =>
inject(Action.SetIndicated(ProjectorView.of_name(name)))
),
Attr.string_property("value", value),
],
applicable_projector_strings
|> List.map(option_view("garbageTODO(andrew)")),
//|> List.map(currently_selected(cursor.editor)),
);
let toggle_view =
toggle_view(
~inject,
cursor.info,
id(cursor.editor),
kind(cursor.editor) != None,
might_project(cursor),
);
Node.select(
~attrs=[
Attr.on_change((_, name) =>
inject(SetIndicated(ProjectorView.of_name(name)))
),
Attr.string_property("value", value),
],
applicable_projector_strings |> List.map(n => option([text(n)])),
);
};

let toggle_view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) =>
toggle_view(
~inject,
cursor.info,
id(cursor.editor),
kind(cursor.editor) != None,
might_project(cursor),
);

let view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => {
div(
~attrs=[Attr.id("projectors")],
(should_show ? [select_view] : []) @ [toggle_view],
[select_view(~inject, cursor)] @ [toggle_view(~inject, cursor)],
);
};
3 changes: 1 addition & 2 deletions src/haz3lweb/www/style.css
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,10 @@
@import "style/animations.css";
@import "style/loading.css";
@import "style/editor.css";
@import "style/projectors.css";
@import "style/projectors/base.css";
@import "style/nut-menu.css";
@import "style/cursor-inspector.css";
@import "style/type-display.css";
@import "style/projectors-panel.css";
@import "style/explainthis.css";
@import "style/exercise-mode.css";
@import "style/cell.css";
Expand Down
4 changes: 3 additions & 1 deletion src/haz3lweb/www/style/editor.css
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,9 @@
/* This is a hack to compensating for default linebreak handling
* preventing a trailing linebreak in code editors from leaving a
* trailing blank line, as per https://stackoverflow.com/questions/43492826/.
* The mysterious chracter below is a zero-width space */
* The mysterious chracter below is a zero-width space, used here
* to avoid inserting an extraneous whitespace context for inline
* syntax views, e.g. type views in the cursor inspector */
.code-text:after {
content: "​";
}
Expand Down
29 changes: 0 additions & 29 deletions src/haz3lweb/www/style/projectors-panel.css

This file was deleted.

Loading

0 comments on commit d64e739

Please sign in to comment.