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

Try making all of the ids type parameters #1371

Draft
wants to merge 8 commits into
base: dev
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
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
53 changes: 27 additions & 26 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -85,12 +85,12 @@ let add_s = (id: Id.t, i: int, m, map) => {
};

// assumes tile is single shard
let add_t = (t: Tile.t, m, map) => {
let add_t = (t: Tile.t(Id.t), m, map) => {
...map,
tiles:
map.tiles
|> Id.Map.update(
t.id,
t.extra,
fun
| None => Some([(Tile.l_shard(t), m)])
| Some(ms) => Some([(Tile.l_shard(t), m), ...ms]),
Expand All @@ -104,11 +104,11 @@ let add_w = (w: Secondary.t, m, map) => {
...map,
secondary: map.secondary |> Id.Map.add(w.id, m),
};
let add_pr = (p: Base.projector, m, map) => {
let add_pr = (p: Base.projector(Id.t), m, map) => {
...map,
projectors: map.projectors |> Id.Map.add(p.id, m),
projectors: map.projectors |> Id.Map.add(p.extra, m),
};
let add_p = (p: Piece.t, m, map) =>
let add_p = (p: Piece.t(Id.t), m, map) =>
p
|> Piece.get(
w => add_w(w, m, map),
Expand Down Expand Up @@ -141,9 +141,10 @@ let singleton_g = (g, m) => empty |> add_g(g, m);
let singleton_s = (id, shard, m) => empty |> add_s(id, shard, m);

// TODO(d) rename
let find_opt_shards = (t: Tile.t, map) => Id.Map.find_opt(t.id, map.tiles);
let find_shards = (~msg="", t: Tile.t, map) =>
try(Id.Map.find(t.id, map.tiles)) {
let find_opt_shards = (t: Tile.t(Id.t), map) =>
Id.Map.find_opt(t.extra, map.tiles);
let find_shards = (~msg="", t: Tile.t(Id.t), map) =>
try(Id.Map.find(t.extra, map.tiles)) {
| _ => failwith("find_shards: " ++ msg)
};

Expand All @@ -163,15 +164,15 @@ let find_g = (~msg="", g: Grout.t, map): measurement =>
try(Id.Map.find(g.id, map.grout)) {
| _ => failwith("find_g: " ++ msg)
};
let find_pr = (~msg="", p: Base.projector, map): measurement =>
try(Id.Map.find(p.id, map.projectors)) {
let find_pr = (~msg="", p: Base.projector(Id.t), map): measurement =>
try(Id.Map.find(p.extra, map.projectors)) {
| _ => failwith("find_g: " ++ msg)
};
let find_pr_opt = (p: Base.projector, map): option(measurement) =>
Id.Map.find_opt(p.id, map.projectors);
let find_pr_opt = (p: Base.projector(Id.t), map): option(measurement) =>
Id.Map.find_opt(p.extra, map.projectors);
// returns the measurement spanning the whole tile
let find_t = (t: Tile.t, map): measurement => {
let shards = Id.Map.find(t.id, map.tiles);
let find_t = (t: Tile.t(Id.t), map): measurement => {
let shards = Id.Map.find(t.extra, map.tiles);
let (first, last) =
try({
let first = ListUtil.assoc_err(Tile.l_shard(t), shards, "find_t");
Expand All @@ -182,7 +183,7 @@ let find_t = (t: Tile.t, map): measurement => {
};
{origin: first.origin, last: last.last};
};
let find_p = (~msg="", p: Piece.t, map): measurement =>
let find_p = (~msg="", p: Piece.t(Id.t), map): measurement =>
try(
p
|> Piece.get(
Expand Down Expand Up @@ -228,7 +229,7 @@ let find_by_id = (id: Id.t, map: t): option(measurement) => {
};
};

let post_tile_indent = (t: Tile.t) => {
let post_tile_indent = (t: Tile.t(Id.t)) => {
// hack for indent following fun/if tiles.
// proper fix involves updating mold datatype
// to specify whether a right-facing concave
Expand All @@ -244,13 +245,13 @@ let post_tile_indent = (t: Tile.t) => {
complete_fun || missing_right_extreme;
};

let missing_left_extreme = (t: Tile.t) => Tile.l_shard(t) > 0;
let missing_left_extreme = (t: Tile.t(Id.t)) => Tile.l_shard(t) > 0;

let is_indented_map = (seg: Segment.t) => {
let rec go = (~is_indented=false, ~map=Id.Map.empty, seg: Segment.t) =>
let is_indented_map = (seg: Segment.t(Id.t)) => {
let rec go = (~is_indented=false, ~map=Id.Map.empty, seg: Segment.t(Id.t)) =>
seg
|> List.fold_left(
((is_indented, map), p: Piece.t) =>
((is_indented, map), p: Piece.t(Id.t)) =>
switch (p) {
| Secondary(w) when Secondary.is_linebreak(w) => (
false,
Expand Down Expand Up @@ -282,7 +283,7 @@ let last_of_token = (token: string, origin: Point.t): Point.t =>
row: origin.row + StringUtil.num_linebreaks(token),
};

let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
let of_segment = (seg: Segment.t(Id.t), info_map: Statics.Map.t): t => {
let is_indented = is_indented_map(seg);

// recursive across seg's bidelimited containers
Expand All @@ -291,7 +292,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
~map,
~container_indent: abs_indent=0,
~origin=Point.zero,
seg: Segment.t,
seg: Segment.t(Id.t),
)
: (Point.t, t) => {
// recursive across seg's list structure
Expand All @@ -300,7 +301,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
~map,
~contained_indent: rel_indent=0,
~origin: Point.t,
seg: Segment.t,
seg: Segment.t(Id.t),
)
: (Point.t, t) =>
switch (seg) {
Expand Down Expand Up @@ -354,7 +355,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
(contained_indent, last, map);
| Projector(p) =>
let token =
Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
Projector.placeholder(p, Id.Map.find_opt(p.extra, info_map));
let last = last_of_token(token, origin);
let map = extra_rows(token, origin, map);
let map = add_pr(p, {origin, last}, map);
Expand All @@ -364,7 +365,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
let token = List.nth(t.label, shard);
let map = extra_rows(token, origin, map);
let last = last_of_token(token, origin);
let map = add_s(t.id, shard, {origin, last}, map);
let map = add_s(t.extra, shard, {origin, last}, map);
(last, map);
};
let (last, map) =
Expand Down Expand Up @@ -392,7 +393,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
snd(go_nested(~map=empty, seg));
};

let length = (seg: Segment.t, map: t): int =>
let length = (seg: Segment.t(Id.t), map: t): int =>
switch (seg) {
| [] => 0
| [p] =>
Expand Down
6 changes: 3 additions & 3 deletions src/haz3lcore/TermRanges.re
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
open Util;

include Id.Map;
type range = (Piece.t, Piece.t);
type range = (Piece.t(Id.t), Piece.t(Id.t));
type nonrec t = t(range);

let union = union((_, range, _) => Some(range));
Expand All @@ -11,7 +11,7 @@ let union = union((_, range, _) => Some(range));
* unmemoized traversal building a hashtbl avoiding unioning.

TODO(andrew): Consider setting a limit for the hashtbl size */
let range_hash: Hashtbl.t(Tile.segment, Id.Map.t(range)) =
let range_hash: Hashtbl.t(Tile.segment(Id.t), Id.Map.t(range)) =
Hashtbl.create(1000);

// NOTE: this calculation is out of sync with
Expand All @@ -23,7 +23,7 @@ let range_hash: Hashtbl.t(Tile.segment, Id.Map.t(range)) =
// TODO(d) fix or derive from other info
//
// tail-recursive in outer recursion
let rec mk' = (seg: Segment.t) => {
let rec mk' = (seg: Segment.t(Id.t)) => {
let rec go = (skel: Skel.t): (range, t) => {
let root = Skel.root(skel) |> Aba.map_a(List.nth(seg));
let root_l = Aba.first_a(root);
Expand Down
11 changes: 7 additions & 4 deletions src/haz3lcore/TileMap.re
Original file line number Diff line number Diff line change
@@ -1,13 +1,16 @@
include Id.Map;
type t = Id.Map.t(Tile.t);
type t = Id.Map.t(Tile.t(Id.t));

// tail-recursive
let rec mk = (~map=empty, seg: Segment.t): t =>
let rec mk = (~map=empty, seg: Segment.t(Id.t)): t =>
Segment.tiles(seg)
|> List.fold_left(
(map, t: Tile.t) => {
(map, t: Tile.t(Id.t)) => {
t.children
|> List.fold_left((map, kid) => mk(~map, kid), add(t.id, t, map))
|> List.fold_left(
(map, kid) => mk(~map, kid),
add(t.extra, t, map),
)
},
map,
);
4 changes: 2 additions & 2 deletions src/haz3lcore/assistant/TyDi.re
Original file line number Diff line number Diff line change
Expand Up @@ -50,9 +50,9 @@ let token_to_left = (z: Zipper.t): option(string) =>
* holds an unparsed string, which is parsed via the same mechanism as
* Paste only when a suggestion is accepted. */
let mk_unparsed_buffer =
(~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t => {
(~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t(Id.t) => {
let mold = Siblings.mold_fitting_between(sort, Precedence.max, sibs);
[Tile({id: Id.mk(), label: [t], shards: [0], children: [], mold})];
[Tile({extra: Id.mk(), label: [t], shards: [0], children: [], mold})];
};

/* If 'current' is a proper prefix of 'candidate', return the
Expand Down
18 changes: 9 additions & 9 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ let tokens =
Piece.get(
_ => [],
_ => [" "],
(t: Tile.t) => t.shards |> List.map(List.nth(t.label)),
(t: Tile.t('a)) => t.shards |> List.map(List.nth(t.label)),
_ => [],
);

Expand All @@ -38,7 +38,7 @@ type unsorted =
type t = {
term: UExp.t,
terms: TermMap.t,
projectors: Id.Map.t(Piece.projector),
projectors: Id.Map.t(Piece.projector(Id.t)),
};

let is_nary =
Expand Down Expand Up @@ -110,14 +110,14 @@ let return = (wrap, ids, tm) => {
};

/* Map to collect projector ids */
let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty);
let projectors: ref(Id.Map.t(Piece.projector(Id.t))) = 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 =>
let rm_and_log_projectors = (seg: Segment.t(Id.t)): Segment.t(Id.t) =>
List.map(
fun
| Piece.Projector(pr) => {
projectors := Id.Map.add(pr.id, pr, projectors^);
projectors := Id.Map.add(pr.extra, pr, projectors^);
pr.syntax;
}
| x => x,
Expand All @@ -139,7 +139,7 @@ let mk_bad = (ctr, ids, value) => {
};
};

let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t =>
let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t(Id.t)): Term.Any.t =>
switch (s) {
| Pat => Pat(pat(unsorted(skel, seg)))
| TPat => TPat(tpat(unsorted(skel, seg)))
Expand Down Expand Up @@ -514,11 +514,11 @@ and rul = (unsorted: unsorted): Rul.t => {
};
}

and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
and unsorted = (skel: Skel.t, seg: Segment.t(Id.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);
let tile_kids = (p: Piece.t): list(Term.Any.t) =>
let tile_kids = (p: Piece.t(Id.t)): list(Term.Any.t) =>
switch (p) {
| Secondary(_)
| Grout(_) => []
Expand All @@ -531,7 +531,7 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
})
};

let root: Aba.t(Piece.t, Skel.t) =
let root: Aba.t(Piece.t(Id.t), Skel.t) =
Skel.root(skel) |> Aba.map_a(List.nth(seg));

// maintaining this alternating ordered structure
Expand Down
20 changes: 10 additions & 10 deletions src/haz3lcore/tiles/Base.re
Original file line number Diff line number Diff line change
Expand Up @@ -13,28 +13,28 @@ type kind =
| TextArea;

[@deriving (show({with_path: false}), sexp, yojson)]
type segment = list(piece)
and piece =
| Tile(tile)
type segment('a) = list(piece('a))
and piece('a) =
| Tile(tile('a))
| Grout(Grout.t)
| Secondary(Secondary.t)
| Projector(projector)
and tile = {
| Projector(projector('a))
and tile('a) = {
Comment on lines +16 to +22
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the main idea for tiles.

// invariants:
// - length(mold.in_) + 1 == length(label)
// - length(shards) <= length(label)
// - length(shards) == length(children) + 1
// - sort(shards) == shards
id: Id.t,
extra: 'a,
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rename this to something more relevant and have the inhabitants use a {id: Id.t} type rather than directly embed Id.t

label: Label.t,
mold: Mold.t,
shards: list(int),
children: list(segment),
children: list(segment('a)),
}
and projector = {
id: Id.t,
and projector('a) = {
kind,
syntax: piece,
extra: 'a,
syntax: piece('a),
model: string,
};

Expand Down
Loading
Loading