Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/dev' into setup-ocaml-action
Browse files Browse the repository at this point in the history
  • Loading branch information
@7h3kk1d
7h3kk1d committed Aug 8, 2024
2 parents 3f1842d + 5cb2cf2 commit 6df5431
Show file tree
Hide file tree
Showing 91 changed files with 12,629 additions and 9,722 deletions.
213 changes: 91 additions & 122 deletions src/haz3lcore/Measured.re
View file
Original file line number Diff line number Diff line change
@@ -1,44 +1,7 @@
open Util;
open Point;

[@deriving (show({with_path: false}), sexp, yojson)]
type row = int;
[@deriving (show({with_path: false}), sexp, yojson)]
type col = int;

module Point = {
[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
row,
col,
};
let zero = {row: 0, col: 0};

let equals: (t, t) => bool = (p, q) => p.row == q.row && p.col == q.col;

type comparison =
| Exact
| Under
| Over;

let comp = (current, target): comparison =>
switch () {
| _ when current == target => Exact
| _ when current < target => Under
| _ => Over
};
let compare = (p1, p2) =>
switch (comp(p1, p2)) {
| Exact => 0
| Under => (-1)
| Over => 1
};

let dcomp = (direction: Direction.t, a, b) =>
switch (direction) {
| Right => comp(a, b)
| Left => comp(b, a)
};
};
module Point = Point;

[@deriving (show({with_path: false}), sexp, yojson)]
type measurement = {
Expand Down Expand Up @@ -85,17 +48,13 @@ module Shards = {
snd(List.hd(row)).origin.row == snd(hd).origin.row
? [[hd, ...row], ...rows] : [[hd], row, ...rows]
};
// let last = (shards: t) =>
// shards
// |> List.sort(((i, _), (j, _)) => Int.compare(i, j))
// |> ListUtil.last_opt
// |> Option.map(snd);
};

type t = {
tiles: Id.Map.t(Shards.t),
grout: Id.Map.t(measurement),
secondary: Id.Map.t(measurement),
projectors: Id.Map.t(measurement),
rows: Rows.t,
linebreaks: Id.Map.t(rel_indent),
};
Expand All @@ -104,6 +63,7 @@ let empty = {
tiles: Id.Map.empty,
grout: Id.Map.empty,
secondary: Id.Map.empty,
projectors: Id.Map.empty,
rows: Rows.empty,
linebreaks: Id.Map.empty,
};
Expand Down Expand Up @@ -144,19 +104,33 @@ 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) => {
...map,
projectors: map.projectors |> Id.Map.add(p.id, m),
};
let add_p = (p: Piece.t, m, map) =>
p
|> Piece.get(
w => add_w(w, m, map),
g => add_g(g, m, map),
t => add_t(t, m, map),
pr => add_pr(pr, m, map),
);

let add_row = (row: int, shape: Rows.shape, map) => {
...map,
rows: Rows.add(row, shape, map.rows),
};

let rec add_n_rows = (origin: Point.t, row_indent, n: abs_indent, map: t): t =>
switch (n) {
| 0 => map
| _ =>
map
|> add_n_rows(origin, row_indent, n - 1)
|> add_row(origin.row + n - 1, {indent: row_indent, max_col: origin.col})
};

let add_lb = (id, indent, map) => {
...map,
linebreaks: Id.Map.add(id, indent, map.linebreaks),
Expand All @@ -168,7 +142,10 @@ 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 = (t: Tile.t, map) => Id.Map.find(t.id, map.tiles);
let find_shards = (~msg="", t: Tile.t, map) =>
try(Id.Map.find(t.id, map.tiles)) {
| _ => failwith("find_shards: " ++ msg)
};

let find_opt_lb = (id, map) => Id.Map.find_opt(id, map.linebreaks);

Expand All @@ -178,25 +155,45 @@ let find_shards' = (id: Id.t, map) =>
| Some(ss) => ss
};

let find_w = (w: Secondary.t, map): measurement =>
Id.Map.find(w.id, map.secondary);
let find_g = (g: Grout.t, map): measurement => Id.Map.find(g.id, map.grout);
let find_w = (~msg="", w: Secondary.t, map): measurement =>
try(Id.Map.find(w.id, map.secondary)) {
| _ => failwith("find_w: " ++ msg)
};
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)) {
| _ => failwith("find_g: " ++ msg)
};
let find_pr_opt = (p: Base.projector, map): option(measurement) =>
Id.Map.find_opt(p.id, 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 first = ListUtil.assoc_err(Tile.l_shard(t), shards, "find_t");
let last = ListUtil.assoc_err(Tile.r_shard(t), shards, "find_t");
let (first, last) =
try({
let first = ListUtil.assoc_err(Tile.l_shard(t), shards, "find_t");
let last = ListUtil.assoc_err(Tile.r_shard(t), shards, "find_t");
(first, last);
}) {
| _ => failwith("find_t: inconsistent shard infor between tile and map")
};
{origin: first.origin, last: last.last};
};
// let find_a = ({shards: (l, r), _} as a: Ancestor.t, map) =>
// List.assoc(l @ r, Id.Map.find(a.id, map.tiles));
let find_p = (p: Piece.t, map): measurement =>
p
|> Piece.get(
w => find_w(w, map),
g => find_g(g, map),
t => find_t(t, map),
);
let find_p = (~msg="", p: Piece.t, map): measurement =>
try(
p
|> Piece.get(
w => find_w(w, map),
g => find_g(g, map),
t => find_t(t, map),
p => find_pr(p, map),
)
) {
| _ => failwith("find_p: " ++ msg ++ "id: " ++ Id.to_string(p |> Piece.id))
};

let find_by_id = (id: Id.t, map: t): option(measurement) => {
switch (Id.Map.find_opt(id, map.secondary)) {
Expand All @@ -217,8 +214,15 @@ let find_by_id = (id: Id.t, map: t): option(measurement) => {
);
Some({origin: first.origin, last: last.last});
| None =>
Printf.printf("Measured.WARNING: id %s not found", Id.to_string(id));
None;
switch (Id.Map.find_opt(id, map.projectors)) {
| Some(m) => Some(m)
| None =>
Printf.printf(
"Measured.WARNING: id %s not found",
Id.to_string(id),
);
None;
}
}
}
};
Expand Down Expand Up @@ -254,6 +258,7 @@ let is_indented_map = (seg: Segment.t) => {
)
| Secondary(_)
| Grout(_) => (is_indented, map)
| Projector(_) => (is_indented, map)
| Tile(t) =>
let is_indented = is_indented || post_tile_indent(t);
let map =
Expand All @@ -270,7 +275,14 @@ let is_indented_map = (seg: Segment.t) => {
go(seg);
};

let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
let last_of_token = (token: string, origin: Point.t): Point.t =>
/* Supports multi-line tokens e.g. projector placeholders */
Point.{
col: origin.col + StringUtil.max_line_width(token),
row: origin.row + StringUtil.num_linebreaks(token),
};

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

// recursive across seg's bidelimited containers
Expand All @@ -282,24 +294,6 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
seg: Segment.t,
)
: (Point.t, t) => {
let first_touched_incomplete =
switch (Segment.incomplete_tiles(seg)) {
| [] => None
| ts =>
ts
|> List.map((t: Tile.t) => Touched.find_opt(t.id, touched))
|> List.fold_left(
(acc, touched) =>
switch (acc, touched) {
| (Some(time), Some(time')) => Some(Time.min(time, time'))
| (Some(time), _)
| (_, Some(time)) => Some(time)
| _ => None
},
None,
)
};

// recursive across seg's list structure
let rec go_seq =
(
Expand All @@ -322,6 +316,11 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
);
(origin, map);
| [hd, ...tl] =>
let extra_rows = (token, origin, map) => {
let row_indent = container_indent + contained_indent;
let num_extra_rows = StringUtil.num_linebreaks(token);
add_n_rows(origin, row_indent, num_extra_rows, map);
};
let (contained_indent, origin, map) =
switch (hd) {
| Secondary(w) when Secondary.is_linebreak(w) =>
Expand All @@ -330,16 +329,7 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
if (Segment.sameline_secondary(tl)) {
0;
} else {
switch (
Touched.find_opt(w.id, touched),
first_touched_incomplete,
find_opt_lb(w.id, old),
) {
| (Some(touched), Some(touched'), Some(indent))
when Time.lt(touched, touched') => indent
| _ =>
contained_indent + (Id.Map.find(w.id, is_indented) ? 2 : 0)
};
contained_indent + (Id.Map.find(w.id, is_indented) ? 2 : 0);
};
let last =
Point.{row: origin.row + 1, col: container_indent + indent};
Expand All @@ -362,15 +352,19 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
let last = {...origin, col: origin.col + 1};
let map = map |> add_g(g, {origin, last});
(contained_indent, last, map);
| Projector(p) =>
let token =
Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
let last = last_of_token(token, origin);
let map = extra_rows(token, origin, map);
let map = add_pr(p, {origin, last}, map);
(contained_indent, last, map);
| Tile(t) =>
let token = List.nth(t.label);
let add_shard = (origin, shard, map) => {
let last =
Point.{
...origin,
col: origin.col + String.length(token(shard)),
};
let map = map |> add_s(t.id, shard, {origin, last});
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);
(last, map);
};
let (last, map) =
Expand Down Expand Up @@ -409,28 +403,3 @@ let length = (seg: Segment.t, map: t): int =>
let last = find_p(ListUtil.last(tl), map);
last.last.col - first.origin.col;
};

let segment_origin = (seg: Segment.t): option(Point.t) =>
Option.map(
first => find_p(first, of_segment(seg)).origin,
ListUtil.hd_opt(seg),
);

let segment_last = (seg: Segment.t): option(Point.t) =>
Option.map(
last => find_p(last, of_segment(seg)).last,
ListUtil.last_opt(seg),
);

let segment_height = (seg: Segment.t) =>
switch (segment_last(seg), segment_origin(seg)) {
| (Some(last), Some(first)) => 1 + last.row - first.row
| _ => 0
};

let segment_width = (seg: Segment.t): int =>
IntMap.fold(
(_, {max_col, _}: Rows.shape, acc) => max(max_col, acc),
of_segment(seg).rows,
0,
);
9 changes: 2 additions & 7 deletions src/haz3lcore/assistant/AssistantCtx.re
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
open Suggestion;

let expander = AssistantExpander.c;

/* For suggestions in patterns, suggest variables which
* occur free in that pattern's scope. */
let free_variables =
Expand Down Expand Up @@ -55,7 +53,7 @@ let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
Typ.is_consistent(ctx, ty_expect, ty_out)
&& !Typ.is_consistent(ctx, ty_expect, ty_arr) => {
Some({
content: name ++ "(" ++ expander,
content: name ++ "(",
strategy: Exp(Common(FromCtxAp(ty_out))),
});
}
Expand All @@ -74,10 +72,7 @@ let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
when
Typ.is_consistent(ctx, ty, ty_out)
&& !Typ.is_consistent(ctx, ty, ty_arr) =>
Some({
content: name ++ "(" ++ expander,
strategy: wrap(FromCtxAp(ty_out)),
})
Some({content: name ++ "(", strategy: wrap(FromCtxAp(ty_out))})
| _ => None,
ctx,
);
Expand Down
24 changes: 8 additions & 16 deletions src/haz3lcore/assistant/AssistantExpander.re
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,16 @@
/* Bit of a hack. We want to decorate suggestions which will trigger
an expansion to telegraph that expansion. Easiest way metrics wise
is to keep that deco in the syntax. Want to decorate with ellipses
character, but OCaml string functions don't support unicode, so
we use $, then swap it out for the unicode character in Code.
Eventually replace this by extending the suggestion data structure */
let c = "$";
/* We decorate buffers whose content will result in an
* expansion with a trailing "...". Note that this ...
* (at least in the current implementation) is not literally
* inserted into the syntax so will not be reflected
* in the decoration metrics */

let is_expander_tok = (t: Token.t) =>
String.sub(t, String.length(t) - 1, 1) == c;

let trim_last = (t: Token.t) => String.sub(t, 0, String.length(t) - 1);
let last = t => String.sub(t, String.length(t) - 1, 1);

let is_expander = (label: Label.t) =>
switch (label) {
| [t] => is_expander_tok(t)
| [t] => last(t) == " " || last(t) == "("
| _ => false
};

let mark = (label: Label.t): Label.t =>
is_expander(label) ? List.map(t => trim_last(t) ++ "…", label) : label;

let trim = (completion: Token.t): Token.t =>
is_expander_tok(completion) ? trim_last(completion) : completion;
is_expander(label) ? List.map(t => t ++ "…", label) : label;
Loading

0 comments on commit 6df5431

Please sign in to comment.