Skip to content

Commit

Permalink
removed projector guts from piece. much re-routing necessary. project…
Browse files Browse the repository at this point in the history
… and setsyntax work, but not projector statics, dynamics, or unproject
  • Loading branch information
disconcision committed Feb 8, 2025
1 parent 44797c9 commit 6f0b9e7
Show file tree
Hide file tree
Showing 20 changed files with 279 additions and 153 deletions.
12 changes: 10 additions & 2 deletions src/haz3lcore/projectors/ProjectorBase.re
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,15 @@ open Virtual_dom.Vdom;
[@deriving (show({with_path: false}), sexp, yojson)]
type syntax = Base.piece;

//TODO(andrew)
[@deriving (show({with_path: false}), sexp, yojson)]
type trad = {
id: Id.t,
kind: ProjectorCore.Kind.t,
syntax: Base.piece,
model: string,
};

/* Global actions available to handlers in all projectors */
type external_action =
| Remove /* Remove projector entirely */
Expand Down Expand Up @@ -190,5 +199,4 @@ module Cook = (C: Projector) : Cooked => {
};

/* Projectors currently are all convex */
let shapes = (_: ProjectorCore.t(syntax)): Nibs.shapes =>
Nib.Shape.(Convex, Convex);
let shapes = _: Nibs.shapes => Nib.Shape.(Convex, Convex);
9 changes: 5 additions & 4 deletions src/haz3lcore/projectors/ProjectorCore.re
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,13 @@ module Kind = {
[@deriving (show({with_path: false}), sexp, yojson)]
type t('syntax) = {
id: Id.t,
kind: Kind.t,
syntax: 'syntax,
model: string,
// kind: Kind.t,
// syntax: 'syntax,
// model: string,
};

let mk = (id, kind, syntax, model) => {id, kind, syntax, model};
//let mk = (id, kind, syntax, model) => {id, kind, syntax, model};
let mk = (id: Id.t): t('a) => {id: id};

module Shape = {
/* A projector shape determines the space left for
Expand Down
8 changes: 6 additions & 2 deletions src/haz3lcore/projectors/ProjectorInfo.re
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,19 @@ let mk_info =

module ShapeMapSemantics = {
let from_semantics =
(statics: Statics.Map.t, dynamics: Dynamics.Map.t, p: Base.projector)
(
statics: Statics.Map.t,
dynamics: Dynamics.Map.t,
p: ProjectorBase.trad,
)
: ProjectorCore.Shape.t => {
let (module P) = ProjectorInit.to_module(p.kind);
P.placeholder(p.model, mk_info(p.id, p.syntax, ~statics, ~dynamics));
};

let mk =
(
proj_map: Id.Map.t(Base.projector),
proj_map: Id.Map.t(ProjectorBase.trad),
statics: Statics.Map.t,
dynamics: Dynamics.Map.t,
)
Expand Down
38 changes: 18 additions & 20 deletions src/haz3lcore/projectors/ProjectorInit.re
Original file line number Diff line number Diff line change
Expand Up @@ -15,35 +15,33 @@ let to_module = (kind: ProjectorCore.Kind.t): (module Cooked) =>
| TextArea => (module Cook(TextAreaProj.M))
};

let init =
(kind: ProjectorCore.Kind.t, id, syntax: syntax, any: Term.Any.t)
: option(syntax) => {
let init = (kind: ProjectorCore.Kind.t, id, any: Term.Any.t): option(syntax) => {
let (module P) = to_module(kind);
switch (P.can_project(any)) {
| false => None
| true => Some(Projector(ProjectorCore.mk(id, kind, syntax, P.init)))
| true => Some(Projector(ProjectorCore.mk(id)))
};
};

let init_or_noop =
(kind: ProjectorCore.Kind.t, id, syntax: syntax, any: Term.Any.t): syntax =>
switch (init(kind, id, syntax, any)) {
switch (init(kind, id, any)) {
| Some(pr) => pr
| None => syntax
};

let init_or_noop_from_str =
(
kind: ProjectorCore.Kind.t,
syntax: syntax,
any: Term.Any.t,
model_str: string,
id: Id.t,
)
: syntax => {
let (module P) = to_module(kind);
switch (P.can_project(any)) {
| false => syntax
| true => Projector(ProjectorCore.mk(id, kind, syntax, model_str))
};
};
// let init_or_noop_from_str =
// (
// kind: ProjectorCore.Kind.t,
// syntax: syntax,
// any: Term.Any.t,
// model_str: string,
// id: Id.t,
// )
// : syntax => {
// let (module P) = to_module(kind);
// switch (P.can_project(any)) {
// | false => syntax
// | true => Projector(ProjectorCore.mk(id, kind, syntax, model_str))
// };
// };
91 changes: 54 additions & 37 deletions src/haz3lcore/projectors/ProjectorPerform.re
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,7 @@ let init =
* of those parentheses are passed to the projector implementations */
switch (MakeTerm.for_projection(seg)) {
| None => None
| Some(any) =>
ProjectorInit.init(kind, projector_id, Segment.parenthesize(seg), any)
| Some(any) => ProjectorInit.init(kind, projector_id, any)
};

let replace_selection_and_unselect =
Expand Down Expand Up @@ -64,9 +63,10 @@ let update =

let go =
(
jump_to_id_indicated,
_jump_to_id_indicated, //TODO:
jump_to_side_of_id,
select_term: Zipper.t => option(Zipper.t),
projectors: Id.Map.t(ProjectorBase.trad),
a: Action.project,
z: Zipper.t,
)
Expand All @@ -80,16 +80,23 @@ let go =
: Some((z.selection.focus, z));

let set_indicated =
(z: Zipper.t, projector_id, kind: ProjectorCore.Kind.t)
(z: Zipper.t, projector_id: Id.t, kind: ProjectorCore.Kind.t)
: option(Zipper.t) => {
/* If not projected, project. If already same kind, remove. If other kind, change */
let* (focus, z) = setup_selection(z);
switch (z.selection.content) {
| [Projector(pr)] when pr.kind == kind =>
Some(remove(pr.syntax, focus, z))
| [Projector(pr)] =>
let+ piece = init(kind, projector_id, Piece.unparenthesize(pr.syntax));
replace_selection_and_unselect(piece, focus, z);
let pr = Id.Map.find_opt(pr.id, projectors);
switch (pr) {
| Some(pr) when pr.kind == kind => Some(remove(pr.syntax, focus, z))
| Some(pr) =>
let+ piece =
init(kind, projector_id, Piece.unparenthesize(pr.syntax));
replace_selection_and_unselect(piece, focus, z);
| None =>
prerr_endline("Projector not found");
None;
};
| seg =>
let+ piece = init(kind, projector_id, seg);
replace_selection_and_unselect(piece, focus, z);
Expand All @@ -99,7 +106,12 @@ let go =
let remove_indicated = (z: Zipper.t): option(Zipper.t) => {
let* (focus, z) = setup_selection(z);
switch (z.selection.content) {
| [Projector(pr)] => Some(remove(pr.syntax, focus, z))
| [Projector(pr)] =>
let pr = Id.Map.find_opt(pr.id, projectors);
switch (pr) {
| Some(pr) => Some(remove(pr.syntax, focus, z))
| None => None
};
| _ => None
};
};
Expand All @@ -125,34 +137,39 @@ let go =
| Some(z) => Ok(z)
| None => Error(Cant_project)
}
| SetSyntax(id, seg) =>
Ok(update(p => {...p, syntax: Segment.parenthesize(seg)}, id, z))
| SetModel(id, model) => Ok(update(pr => {...pr, model}, id, z))
| Focus(id, d) =>
switch (d) {
| None =>
/* Focus by mouse click */
/* Currently not calling focus method as projectors get focus here naturally */
Ok(Option.value(~default=z, jump_to_id_indicated(z, id)))
| Some(Right) =>
/* Focus by arrow key hand-off */
switch (Siblings.left_neighbor(z.relatives.siblings)) {
| Some(Projector({id, kind, _})) =>
let (module P) = ProjectorInit.to_module(kind);
P.focus((id, Some(Right)));
| _ => ()
};
Ok(z);
| Some(Left) =>
/* Focus by arrow key hand-off */
switch (Siblings.right_neighbor(z.relatives.siblings)) {
| Some(Projector({id, kind, _})) =>
let (module P) = ProjectorInit.to_module(kind);
P.focus((id, Some(Left)));
| _ => ()
};
Ok(z);
}
| SetSyntax(_id, _seg) =>
failwith("TODO: projectorperform update: wire or remove")

//Ok(update(p => {...p, syntax: Segment.parenthesize(seg)}, id, z))
| SetModel(_id, _model) =>
failwith("TODO: projectorperform setmodel: wire or remove")
//Ok(update(pr => {...pr, model}, id, z))
| Focus(_id, _d) =>
failwith("TODO: projectorperform focus: wire or remove")
// switch (d) {
// | None =>
// /* Focus by mouse click */
// /* Currently not calling focus method as projectors get focus here naturally */
// Ok(Option.value(~default=z, jump_to_id_indicated(z, id)))
// | Some(Right) =>
// /* Focus by arrow key hand-off */
// switch (Siblings.left_neighbor(z.relatives.siblings)) {
// | Some(Projector({id, kind, _})) =>
// let (module P) = ProjectorInit.to_module(kind);
// P.focus((id, Some(Right)));
// | _ => ()
// };
// Ok(z);
// | Some(Left) =>
// /* Focus by arrow key hand-off */
// switch (Siblings.right_neighbor(z.relatives.siblings)) {
// | Some(Projector({id, kind, _})) =>
// let (module P) = ProjectorInit.to_module(kind);
// P.focus((id, Some(Left)));
// | _ => ()
// };
// Ok(z);
// }
| Escape(id, d) => Ok(jump_to_side_of_id(d, z, id))
};
};
39 changes: 21 additions & 18 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,8 @@ let tokens =
* which are retained through maketerm so as to be used in
* dynamics. These are inserted and removed entirely internal
* to maketerm. */
probe_wrap,
//probe_wrap,
["PROBE_WRAP"],
);

[@deriving (show({with_path: false}), sexp, yojson)]
Expand Down Expand Up @@ -130,13 +131,13 @@ let log_projector = (pr: Base.projector): unit => {
/* Check if a term should be instrumented with a probe.
* Precondition: The relevant projector must have been
* logged before this is called */
let should_instrument = (id: Id.t): bool =>
switch (Id.Map.find_opt(id, projectors^)) {
| Some(pr) =>
let (module P) = ProjectorInit.to_module(pr.kind);
P.dynamics;
| None => failwith("MakeTerm.exp: projector not found")
};
// let should_instrument = (id: Id.t): bool =>
// switch (Id.Map.find_opt(id, projectors^)) {
// | Some(pr) =>
// let (module P) = ProjectorInit.to_module(pr.kind);
// P.dynamics;
// | None => failwith("MakeTerm.exp: projector not found")
// };

let parse_sum_term: Typ.t => ConstructorMap.variant(Typ.t) =
fun
Expand Down Expand Up @@ -190,7 +191,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
| Op(tiles) as tm =>
switch (tiles) {
// single-tile case
| ([(id, t)], []) =>
| ([(_id, t)], []) =>
switch (t) {
| ([t], []) when Form.is_empty_tuple(t) => ret(Tuple([]))
| ([t], []) when Form.is_wild(t) => ret(Deferral(OutsideAp))
Expand All @@ -207,7 +208,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
| (["(", ")"], [Exp(body)]) => ret(Parens(body))
| (label, [Exp(body)]) when is_probe_wrap(label) =>
// Temporary wrapping form to persist projector probes
ret(should_instrument(id) ? Probe(body, Probe.empty) : body.term)
ret(Probe(body, Probe.empty))
| (["[", "]"], [Exp(body)]) =>
switch (body) {
| {ids, copied: false, term: Tuple(es)} => (ListLit(es), ids)
Expand Down Expand Up @@ -354,7 +355,7 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
fun
| Op(tiles) as tm =>
switch (tiles) {
| ([(id, tile)], []) =>
| ([(_id, tile)], []) =>
ret(
switch (tile) {
| ([t], []) when Form.is_empty_tuple(t) => Tuple([])
Expand All @@ -371,7 +372,7 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
Invalid(t)
| (["(", ")"], [Pat(body)]) => Parens(body)
| (label, [Pat(body)]) when is_probe_wrap(label) =>
should_instrument(id) ? Probe(body, Probe.empty) : body.term
Probe(body, Probe.empty)
| (["[", "]"], [Pat(body)]) =>
switch (body) {
| {term: Tuple(ps), _} => ListLit(ps)
Expand Down Expand Up @@ -547,12 +548,14 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
switch (p) {
| Secondary(_)
| Grout(_) => []
| Projector({syntax, _} as pr) =>
let _ = log_projector(pr);
let sort = Piece.sort(syntax) |> fst;
//TODO(andrew): be more selective about unparening
let seg = Piece.unparenthesize(syntax);
[go_s(sort, Segment.skel(seg), seg)];
| Projector(_) => []
//TODO(andrew): allowing this as want the cachedsyntax call to go through
// failwith("TODO: MakeTerm unsorted projector")
// let _ = log_projector(pr);
// let sort = Piece.sort(syntax) |> fst;
// //TODO(andrew): be more selective about unparening
// let seg = Piece.unparenthesize(syntax);
// [go_s(sort, Segment.skel(seg), seg)];
| Tile({mold, shards, children, _}) =>
Aba.aba_triples(Aba.mk(shards, children))
|> List.map(((l, kid, r)) => {
Expand Down
13 changes: 7 additions & 6 deletions src/haz3lcore/tiles/Segment.re
Original file line number Diff line number Diff line change
Expand Up @@ -801,11 +801,11 @@ module IDs = {
| Tile(t) => Tile({...t, children: List.map(replace, t.children), id})
| Grout(grout) => Grout({...grout, id})
| Secondary(w) => Secondary({...w, id})
| Projector(p) =>
/* Need to keep projector and contained piece id in-sync */
let id = Id.mk();
let syntax = replace_piece(~id, p.syntax);
Projector({...p, syntax, id});
| Projector(p) => failwith("Segment: IDs.all: Projectors not supported")
/* Need to keep projector and contained piece id in-sync */
// let id = Id.mk();
// let syntax = replace_piece(~id, p.syntax);
// Projector({...p, syntax, id});
};
};

Expand All @@ -817,7 +817,8 @@ module IDs = {
| Tile(t) => [id, ...List.concat_map(all, t.children)]
| Grout(_)
| Secondary(_) => [id]
| Projector(p) => [id, ...all_piece(p.syntax)]
| Projector(_) => failwith("Segment: IDs.all: Projectors not supported")
// [id, ...all_piece(p.syntax)]
};
};
};
Loading

0 comments on commit 6f0b9e7

Please sign in to comment.