Skip to content

Commit

Permalink
Make plus signs in types escape sort
Browse files Browse the repository at this point in the history
  • Loading branch information
@Negabinary
Negabinary committed Sep 4, 2024
1 parent ec8305f commit 2f6b06d
Show file tree
Hide file tree
Showing 2 changed files with 72 additions and 34 deletions.
10 changes: 5 additions & 5 deletions src/haz3lcore/lang/Precedence.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,16 @@ let right_associative = (level: t) => {
let max: t = 0;

// ========== TYPES ==========
let type_sum_ap = 22;
let type_sum_ap = 11;
// _____ (Int)
// + T1 + _____
let type_plus = 25;
let type_plus = 12 |> right_associative;
// _____ -> Int
let type_arrow = 28 |> right_associative;
let type_arrow = 13 |> right_associative;
// Int -> _____
// String , _____ , String
let type_prod = 45;
let type_binder = 38;
let type_prod = 14;
let type_binder = 15;
// forall t -> _____
// rec t -> _____

Expand Down
96 changes: 67 additions & 29 deletions src/haz3lcore/tiles/Segment.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,19 +128,23 @@ and remold_typ = (shape, seg: t): t =>
| Tile(t) =>
switch (remold_tile(Typ, shape, t)) {
| None => [Tile(t), ...remold_typ(snd(Tile.shapes(t)), tl)]
| Some(t) when !Tile.has_end(Right, t) =>
let (_, r) = Tile.nibs(t);
let remolded = remold(~shape=r.shape, tl, r.sort);
[Tile(t), ...remolded];
| Some(t) => [Tile(t), ...remold_typ(snd(Tile.shapes(t)), tl)]
}
}
}
and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
and remold_typ_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
switch (seg) {
| [] => ([], shape, [])
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
let (remolded, shape, rest) = remold_typ_uni(shape, tl);
let (remolded, shape, rest) = remold_typ_uni(shape, tl, parent_sorts);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Typ, shape, t)) {
Expand All @@ -150,27 +154,31 @@ and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
let remolded = remold(~shape=r.shape, tl, r.sort);
let (_, shape, _) = shape_affix(Left, remolded, r.shape);
([Tile(t), ...remolded], shape, []);
| Some(t) when t.label == Form.get("comma_typ").label => (
| Some(t)
when
t.label == Form.get("comma_typ").label
|| t.label == Form.get("typ_plus").label
&& List.exists((==)(Sort.Exp), parent_sorts) => (
[],
shape,
seg,
)
| Some(t) =>
let (remolded, shape, rest) =
remold_typ_uni(snd(Tile.shapes(t)), tl);
remold_typ_uni(snd(Tile.shapes(t)), tl, parent_sorts);
([Tile(t), ...remolded], shape, rest);
}
}
}
and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
and remold_pat_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
switch (seg) {
| [] => ([], shape, [])
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
let (remolded, shape, rest) = remold_pat_uni(shape, tl);
let (remolded, shape, rest) = remold_pat_uni(shape, tl, parent_sorts);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Pat, shape, t)) {
Expand All @@ -183,12 +191,14 @@ and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: Typ}) =>
let (remolded_typ, shape, rest) = remold_typ_uni(shape, tl);
let (remolded_pat, shape, rest) = remold_pat_uni(shape, rest);
let (remolded_typ, shape, rest) =
remold_typ_uni(shape, tl, [Sort.Pat, ...parent_sorts]);
let (remolded_pat, shape, rest) =
remold_pat_uni(shape, rest, parent_sorts);
([Piece.Tile(t), ...remolded_typ] @ remolded_pat, shape, rest);
| _ =>
let (remolded, shape, rest) =
remold_pat_uni(snd(Tile.shapes(t)), tl);
remold_pat_uni(snd(Tile.shapes(t)), tl, parent_sorts);
([Tile(t), ...remolded], shape, rest);
}
}
Expand All @@ -205,25 +215,30 @@ and remold_pat = (shape, seg: t): t =>
| Tile(t) =>
switch (remold_tile(Pat, shape, t)) {
| None => [Tile(t), ...remold_pat(snd(Tile.shapes(t)), tl)]
| Some(t) when !Tile.has_end(Right, t) =>
let (_, r) = Tile.nibs(t);
let remolded = remold(~shape=r.shape, tl, r.sort);
[Tile(t), ...remolded];
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: Typ}) =>
let (remolded, shape, rest) = remold_typ_uni(shape, tl);
let (remolded, shape, rest) =
remold_typ_uni(shape, tl, [Sort.Pat]);
[Piece.Tile(t), ...remolded] @ remold_pat(shape, rest);
| _ => [Tile(t), ...remold_pat(snd(Tile.shapes(t)), tl)]
}
}
}
}
and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
and remold_tpat_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
switch (seg) {
| [] => ([], shape, [])
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
let (remolded, shape, rest) = remold_tpat_uni(shape, tl);
let (remolded, shape, rest) = remold_tpat_uni(shape, tl, parent_sorts);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(TPat, shape, t)) {
Expand All @@ -237,7 +252,7 @@ and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
switch (Tile.nibs(t)) {
| _ =>
let (remolded, shape, rest) =
remold_tpat_uni(snd(Tile.shapes(t)), tl);
remold_tpat_uni(snd(Tile.shapes(t)), tl, parent_sorts);
([Tile(t), ...remolded], shape, rest);
}
}
Expand All @@ -254,25 +269,30 @@ and remold_tpat = (shape, seg: t): t =>
| Tile(t) =>
switch (remold_tile(TPat, shape, t)) {
| None => [Tile(t), ...remold_tpat(snd(Tile.shapes(t)), tl)]
| Some(t) when !Tile.has_end(Right, t) =>
let (_, r) = Tile.nibs(t);
let remolded = remold(~shape=r.shape, tl, r.sort);
[Tile(t), ...remolded];
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: Typ}) =>
let (remolded, shape, rest) = remold_typ_uni(shape, tl);
let (remolded, shape, rest) =
remold_typ_uni(shape, tl, [Sort.TPat]);
[Piece.Tile(t), ...remolded] @ remold_tpat(shape, rest);
| _ => [Tile(t), ...remold_tpat(snd(Tile.shapes(t)), tl)]
}
}
}
}
and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
and remold_exp_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
switch (seg) {
| [] => ([], shape, [])
| [hd, ...tl] =>
switch (hd) {
| Secondary(_)
| Grout(_)
| Projector(_) =>
let (remolded, shape, rest) = remold_exp_uni(shape, tl);
let (remolded, shape, rest) = remold_exp_uni(shape, tl, parent_sorts);
([hd, ...remolded], shape, rest);
| Tile(t) =>
switch (remold_tile(Exp, shape, t)) {
Expand All @@ -285,23 +305,29 @@ and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: TPat}) =>
let (remolded_tpat, shape, rest) = remold_tpat_uni(shape, tl);
let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
let (remolded_tpat, shape, rest) =
remold_tpat_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
let (remolded_exp, shape, rest) =
remold_exp_uni(shape, rest, parent_sorts);
([Piece.Tile(t), ...remolded_tpat] @ remolded_exp, shape, rest);
| (_, {shape, sort: Pat}) =>
let (remolded_pat, shape, rest) = remold_pat_uni(shape, tl);
let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
let (remolded_pat, shape, rest) =
remold_pat_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
let (remolded_exp, shape, rest) =
remold_exp_uni(shape, rest, parent_sorts);
([Piece.Tile(t), ...remolded_pat] @ remolded_exp, shape, rest);
| (_, {shape, sort: Typ}) =>
let (remolded_typ, shape, rest) = remold_typ_uni(shape, tl);
let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
let (remolded_typ, shape, rest) =
remold_typ_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
let (remolded_exp, shape, rest) =
remold_exp_uni(shape, rest, parent_sorts);
([Piece.Tile(t), ...remolded_typ] @ remolded_exp, shape, rest);
| (_, {shape, sort: Rul}) =>
// TODO review short circuit
([Tile(t)], shape, tl)
| _ =>
let (remolded, shape, rest) =
remold_exp_uni(snd(Tile.shapes(t)), tl);
remold_exp_uni(snd(Tile.shapes(t)), tl, parent_sorts);
([Tile(t), ...remolded], shape, rest);
}
}
Expand All @@ -317,19 +343,27 @@ and remold_rul = (shape, seg: t): t =>
| Projector(_) => [hd, ...remold_rul(shape, tl)]
| Tile(t) =>
switch (remold_tile(Rul, shape, t)) {
| Some(t) when !Tile.has_end(Right, t) =>
let (_, r) = Tile.nibs(t);
let remolded = remold(~shape=r.shape, tl, r.sort);
[Tile(t), ...remolded];
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: Exp}) =>
let (remolded, shape, rest) = remold_exp_uni(shape, tl);
let (remolded, shape, rest) =
remold_exp_uni(shape, tl, [Sort.Rul]);
[Piece.Tile(t), ...remolded] @ remold_rul(shape, rest);
| (_, {shape, sort: Pat}) =>
let (remolded, shape, rest) = remold_pat_uni(shape, tl);
let (remolded, shape, rest) =
remold_pat_uni(shape, tl, [Sort.Rul]);
// TODO(d) continuing onto rule might not be right right...
[Piece.Tile(t), ...remolded] @ remold_rul(shape, rest);
| _ => failwith("remold_rul unexpected")
}
| None =>
let (remolded, shape, rest) = remold_exp_uni(shape, [hd, ...tl]);
// TODO: not sure whether we should add Rul to parent_sorts here
let (remolded, shape, rest) =
remold_exp_uni(shape, [hd, ...tl], []);
switch (remolded) {
| [] => [Piece.Tile(t), ...remold_rul(shape, tl)]
| [_, ..._] => remolded @ remold_rul(shape, rest)
Expand All @@ -348,16 +382,20 @@ and remold_exp = (shape, seg: t): t =>
| Tile(t) =>
switch (remold_tile(Exp, shape, t)) {
| None => [Tile(t), ...remold_exp(snd(Tile.shapes(t)), tl)]
| Some(t) when !Tile.has_end(Right, t) =>
let (_, r) = Tile.nibs(t);
let remolded = remold(~shape=r.shape, tl, r.sort);
[Tile(t), ...remolded];
| Some(t) =>
switch (Tile.nibs(t)) {
| (_, {shape, sort: Pat}) =>
let (remolded, shape, rest) = remold_pat_uni(shape, tl);
let (remolded, shape, rest) = remold_pat_uni(shape, tl, [Exp]);
[Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
| (_, {shape, sort: TPat}) =>
let (remolded, shape, rest) = remold_tpat_uni(shape, tl);
let (remolded, shape, rest) = remold_tpat_uni(shape, tl, [Exp]);
[Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
| (_, {shape, sort: Typ}) =>
let (remolded, shape, rest) = remold_typ_uni(shape, tl);
let (remolded, shape, rest) = remold_typ_uni(shape, tl, [Exp]);
[Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
| (_, {shape, sort: Rul}) => [Tile(t), ...remold_rul(shape, tl)]
| _ => [Tile(t), ...remold_exp(snd(Tile.shapes(t)), tl)]
Expand Down

0 comments on commit 2f6b06d

Please sign in to comment.