Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Shaped Projectors #1387

Draft
wants to merge 19 commits into
base: dev
Choose a base branch
from
Draft
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 42 additions & 7 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ let tokens =
_ => [],
_ => [" "],
(t: Tile.t) => t.shards |> List.map(List.nth(t.label)),
_ => [],
_ => [" "] //TODO(andrew): ??? necessary to avoid throwing aba exn
);

[@deriving (show({with_path: false}), sexp, yojson)]
@@ -114,13 +114,13 @@ 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 rm_and_log_projectors = (seg: Segment.t): Segment.t =>
List.map(
List.concat_map(
fun
| Piece.Projector(pr) => {
projectors := Id.Map.add(pr.id, pr, projectors^);
pr.syntax;
}
| x => x,
| x => [x],
seg,
);

@@ -517,7 +517,8 @@ 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 seg = rm_and_log_projectors(seg);
//TODO(andrew): check this one call is actually necessary
//let seg = rm_and_log_projectors(seg);
let tile_kids = (p: Piece.t): list(Term.Any.t) =>
switch (p) {
| Secondary(_)
@@ -527,6 +528,9 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
Aba.aba_triples(Aba.mk(shards, children))
|> List.map(((l, kid, r)) => {
let s = l + 1 == r ? List.nth(mold.in_, l) : Sort.Any;
/* Remove projectors. We do this here as opposed to removing
* them in an external call to save a whole-syntax pass. */
let kid = rm_and_log_projectors(kid);
go_s(s, Segment.skel(kid), kid);
})
};
@@ -544,9 +548,24 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
let s = s_l == s_r ? s_l : Sort.Any;
go_s(s, kid, seg);
})
|> Aba.map_a(p
// TODO throw proper exception
=> (Piece.id(p), Aba.mk(tokens(p), tile_kids(p))));
|> Aba.map_a(p => {
(
// TODO throw proper exception
//TODO(andrew): cleanup
// print_endline("aba: ");
// print_endline("p: " ++ Piece.show(p));
// print_endline(
// "tokens(p)"
// ++ (List.map(Token.show, tokens(p)) |> String.concat(" ")),
// );
// print_endline(
// "tile_kids(p): "
// ++ (tile_kids(p) |> List.map(Any.show) |> String.concat(" ")),
// );
Piece.id(p),
Aba.mk(tokens(p), tile_kids(p)),
)
});

let (l_sort, r_sort) = {
let p_l = Aba.first_a(root);
@@ -571,6 +590,22 @@ let go =
seg => {
map := TermMap.empty;
projectors := Id.Map.empty;
//TODO(andrew): cleanup
//need to remove holistically now or skel calc gets fucked up
// let remove_projector_always = (piece: Piece.t): Segment.t =>
// switch (piece) {
// | Projector(pr) =>
// projectors := Id.Map.add(pr.id, pr, projectors^);
// pr.syntax;
// | x => [x]
// };
// let ff = (seg: Segment.t) => {
// List.concat(List.map(p => remove_projector_always(p), seg));
// };
// let seg = ZipperBase.MapSegment.of_segment(ff, seg);
let seg = rm_and_log_projectors(seg);
//TODO(andrew): remove whole pass if possible
//let seg = ZipperBase.MapSegment.of_segment(rm_and_log_projectors, seg);
let term = exp(unsorted(Segment.skel(seg), seg));
{term, terms: map^, projectors: projectors^};
},
2 changes: 1 addition & 1 deletion src/haz3lcore/tiles/Base.re
Original file line number Diff line number Diff line change
@@ -34,7 +34,7 @@ and tile = {
and projector = {
id: Id.t,
kind,
syntax: piece,
syntax: list(piece),
model: string,
};

15 changes: 7 additions & 8 deletions src/haz3lcore/tiles/Piece.re
Original file line number Diff line number Diff line change
@@ -35,7 +35,7 @@ let nibs =
},
t => Some(Tile.nibs(t)),
p => {
let (l, r) = ProjectorBase.shapes(p);
let (l, r) = ProjectorBase.shapes_p(p);
Some(Nib.({shape: l, sort: Any}, {shape: r, sort: Any}));
},
);
@@ -76,13 +76,7 @@ let disassemble = (p: t): segment =>
| Tile(t) => Tile.disassemble(t)
};

let shapes =
get(
_ => None,
g => Some(Grout.shapes(g)),
t => Some(Tile.shapes(t)),
p => Some(ProjectorBase.shapes(p)),
);
let shapes = ProjectorBase.shapes;

let is_convex = (p: t): bool =>
switch (shapes(p)) {
@@ -167,6 +161,11 @@ let is_not_case_or_rule_or_space = (p: t) =>
| Secondary(_) => false
| _ => true
};
let not_space = (p: t) =>
switch (p) {
| Secondary(s) => !Secondary.is_space(s)
| _ => true
};
let not_comment_or_space = (p: t) =>
switch (p) {
| Secondary(s) => Secondary.is_linebreak(s)
116 changes: 96 additions & 20 deletions src/haz3lcore/tiles/Segment.re
Original file line number Diff line number Diff line change
@@ -66,7 +66,7 @@ let shape_affix =
| Grout(g) => (Aba.cons([], g, wgw), s, tl)
| Projector(p) =>
let (l, _) =
ProjectorBase.shapes(p) |> (d == Left ? TupleUtil.swap : Fun.id);
ProjectorBase.shapes_p(p) |> (d == Left ? TupleUtil.swap : Fun.id);
(empty_wgw, l, tl);
| Tile(t) =>
let (l, _) = Tile.shapes(t) |> (d == Left ? TupleUtil.swap : Fun.id);
@@ -123,8 +123,11 @@ and remold_typ = (shape, seg: t): t =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) => [hd, ...remold_typ(shape, tl)]
| Grout(_) => [hd, ...remold_typ(shape, tl)]
| Projector(p) => [
hd,
...remold_typ(snd(ProjectorBase.shapes_p(p)), tl),
]
| Tile(t) =>
switch (remold_tile(Typ, shape, t)) {
| None => [Tile(t), ...remold_typ(snd(Tile.shapes(t)), tl)]
@@ -138,10 +141,13 @@ and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
| Grout(_) =>
let (remolded, shape, rest) = remold_typ_uni(shape, tl);
([hd, ...remolded], shape, rest);
| Projector(p) =>
let (remolded, shape, rest) =
remold_typ_uni(snd(ProjectorBase.shapes_p(p)), tl);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Typ, shape, t)) {
| None => ([], shape, seg)
@@ -155,6 +161,7 @@ and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
shape,
seg,
)

| Some(t) =>
let (remolded, shape, rest) =
remold_typ_uni(snd(Tile.shapes(t)), tl);
@@ -168,10 +175,13 @@ and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
| Grout(_) =>
let (remolded, shape, rest) = remold_pat_uni(shape, tl);
([hd, ...remolded], shape, rest);
| Projector(p) =>
let (remolded, shape, rest) =
remold_pat_uni(snd(ProjectorBase.shapes_p(p)), tl);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Pat, shape, t)) {
| None => ([], shape, seg)
@@ -200,8 +210,11 @@ and remold_pat = (shape, seg: t): t =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) => [hd, ...remold_pat(shape, tl)]
| Grout(_) => [hd, ...remold_pat(shape, tl)]
| Projector(p) => [
hd,
...remold_pat(snd(ProjectorBase.shapes_p(p)), tl),
]
| Tile(t) =>
switch (remold_tile(Pat, shape, t)) {
| None => [Tile(t), ...remold_pat(snd(Tile.shapes(t)), tl)]
@@ -221,10 +234,13 @@ and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
| Grout(_) =>
let (remolded, shape, rest) = remold_tpat_uni(shape, tl);
([hd, ...remolded], shape, rest);
| Projector(p) =>
let (remolded, shape, rest) =
remold_tpat_uni(snd(ProjectorBase.shapes_p(p)), tl);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(TPat, shape, t)) {
| None => ([], shape, seg)
@@ -249,8 +265,11 @@ and remold_tpat = (shape, seg: t): t =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) => [hd, ...remold_tpat(shape, tl)]
| Grout(_) => [hd, ...remold_tpat(shape, tl)]
| Projector(p) => [
hd,
...remold_tpat(snd(ProjectorBase.shapes_p(p)), tl),
]
| Tile(t) =>
switch (remold_tile(TPat, shape, t)) {
| None => [Tile(t), ...remold_tpat(snd(Tile.shapes(t)), tl)]
@@ -270,10 +289,13 @@ and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
| Grout(_) =>
let (remolded, shape, rest) = remold_exp_uni(shape, tl);
([hd, ...remolded], shape, rest);
| Projector(p) =>
let (remolded, shape, rest) =
remold_exp_uni(snd(ProjectorBase.shapes_p(p)), tl);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Exp, shape, t)) {
| None => ([], shape, seg)
@@ -313,8 +335,11 @@ and remold_rul = (shape, seg: t): t =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) => [hd, ...remold_rul(shape, tl)]
| Grout(_) => [hd, ...remold_rul(shape, tl)]
| Projector(p) => [
hd,
...remold_rul(snd(ProjectorBase.shapes_p(p)), tl),
]
| Tile(t) =>
switch (remold_tile(Rul, shape, t)) {
| Some(t) =>
@@ -343,8 +368,11 @@ and remold_exp = (shape, seg: t): t =>
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) => [hd, ...remold_exp(shape, tl)]
| Grout(_) => [hd, ...remold_exp(shape, tl)]
| Projector(p) => [
hd,
...remold_exp(snd(ProjectorBase.shapes_p(p)), tl),
]
| Tile(t) =>
switch (remold_tile(Exp, shape, t)) {
| None => [Tile(t), ...remold_exp(snd(Tile.shapes(t)), tl)]
@@ -374,6 +402,9 @@ let skel =
|> Skel.mk
);

let root_rep_id = (seg: t): Id.t =>
Piece.id(List.nth(seg, Util.Aba.first_a(Skel.root(skel(seg)))));

let sorted_children = List.concat_map(Piece.sorted_children);
let children = seg => List.map(snd, sorted_children(seg));

@@ -504,7 +535,8 @@ and regrout_affix =
| Projector(pr) =>
let p = Piece.Projector(pr);
let (l', r') =
ProjectorBase.shapes(pr) |> (d == Left ? TupleUtil.swap : Fun.id);
ProjectorBase.shapes_p(pr)
|> (d == Left ? TupleUtil.swap : Fun.id);
let trim = Trim.regrout(d, (r', r), trim);
(Trim.empty, l', [p, ...Trim.to_seg(trim)] @ tl);
| Tile(t) =>
@@ -674,3 +706,47 @@ and ids_of_piece = (p: Piece.t): list(Id.t) =>
| Secondary(_)
| Projector(_) => [Piece.id(p)]
};

let term_bounds = (skel, seg: t, id: Id.t): option((int, int)) => {
let is_root_id = (root: Aba.t(int, Skel.t)): bool => {
let index = Aba.first_a(root); // TODO(andrew): this assumes singleton maybe?
let piece = List.nth(seg, index);
Piece.id(piece) == id;
};
let rec go = (seg: t, skel: Skel.t): option((int, int)) => {
switch (skel) {
| Op(root) => is_root_id(root) ? Some(Skel.bounds(skel)) : None
| Pre(root, skel_r) =>
is_root_id(root) ? Some(Skel.bounds(skel)) : go(seg, skel_r)
| Post(skel_l, r) =>
is_root_id(r) ? Some(Skel.bounds(skel)) : go(seg, skel_l)
| Bin(skel_l, root, skel_r) =>
if (is_root_id(root)) {
Some(Skel.bounds(skel));
} else {
switch (go(seg, skel_l)) {
| Some(bounds) => Some(bounds)
| None => go(seg, skel_r)
};
}
};
};
go(seg, skel);
};

let term_partitions = (seg: t, id: Id.t): option((t, t, t)) => {
open OptUtil.Syntax;
// eliminate segs that have no term and hence will crash skel
let* _ = trim_secondary(Left, seg) == [] ? None : Some();
//print_endline("term_partitions:");
//print_endline(show(seg));
print_endline("CCC");
let* skel =
try(Some(skel(seg))) {
| _ => None
};
print_endline("DDD");
let* (l, r) = term_bounds(skel, seg, id);
print_endline("EEE");
ListUtil.split_sublist_opt(l, r + 1, seg);
};
15 changes: 15 additions & 0 deletions src/haz3lcore/tiles/Skel.re
Original file line number Diff line number Diff line change
@@ -183,3 +183,18 @@ let mk = (seg: list(ip)): t => {
|> Stacks.finish;
ListUtil.hd_opt(stacks.output) |> OptUtil.get_or_raise(Nonconvex_segment);
};

let rec bounds = (skel: t): (int, int) =>
switch (skel) {
| Op(root) => (Aba.first_a(root), Aba.last_a(root))
| Pre(root, skel_r) =>
let (_, last) = bounds(skel_r);
(Aba.first_a(root), last);
| Post(skel_l, root) =>
let (first, _) = bounds(skel_l);
(first, Aba.last_a(root));
| Bin(skel_l, _, skel_r) =>
let (first, _) = bounds(skel_l);
let (_, last) = bounds(skel_r);
(first, last);
};
2 changes: 1 addition & 1 deletion src/haz3lcore/zipper/Printer.re
Original file line number Diff line number Diff line change
@@ -13,7 +13,7 @@ and of_piece = (~holes, p: Piece.t): string =>
| Grout({shape: Convex, _}) => " "
| Secondary(w) =>
Secondary.is_linebreak(w) ? "\n" : Secondary.get_string(w.content)
| Projector(p) => of_piece(~holes, p.syntax)
| Projector(p) => of_segment(~holes, p.syntax)
}
and of_tile = (~holes, t: Tile.t): string =>
Aba.mk(t.shards, t.children)
Loading