Skip to content

Commit

Permalink
clarify live projector statics
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Nov 20, 2024
1 parent 881a086 commit 1d07174
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 5 deletions.
11 changes: 7 additions & 4 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,9 @@ let return = (wrap, ids, tm) => {
/* Map to collect projector ids */
let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty);

let mk_probe = (e: list(Piece.t)) =>
Piece.mk_tile(
let mk_probe = (id, e: list(Piece.t)) =>
Piece.mk_tile_id(
id,
Form.mk(Form.ii, ["@@", "@@"], Mold.mk_op(Exp, [Exp])),
[e],
);
Expand All @@ -124,7 +125,7 @@ let rm_and_log_projectors = (seg: Segment.t): Segment.t =>
fun
| Piece.Projector(pr) => {
projectors := Id.Map.add(pr.id, pr, projectors^);
mk_probe([pr.syntax]);
mk_probe(pr.id, [pr.syntax]);
}
| x => x,
seg,
Expand Down Expand Up @@ -198,7 +199,9 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
| ([t], []) when Form.is_ctr(t) =>
ret(Constructor(t, Unknown(Internal) |> Typ.temp))
| (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren))
| (["@@", "@@"], [Exp(body)]) => ret(Parens(body, Probe))
| (["@@", "@@"], [Exp(body)]) =>
// TODO(andrew): apologize for this
ret(Parens(body, Probe))
| (["[", "]"], [Exp(body)]) =>
switch (body) {
| {ids, copied: false, term: Tuple(es)} => (ListLit(es), ids)
Expand Down
8 changes: 7 additions & 1 deletion src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -269,9 +269,15 @@ and uexp_to_info_map =
m,
)
| DynamicErrorHole(e, _)
| Parens(e, _) =>
| Parens(e, Paren) =>
let (e, m) = go(~mode, e, m);
add(~self=Just(e.ty), ~co_ctx=e.co_ctx, m);
| Parens(e, Probe) =>
/* Currently doing this as otherwise it clobbers the statics
* for the contained expression as i'm just reusing the same id
* in order to associate it through dynamics */
go(~mode, e, m)
//TODO(andrew): ponder this
| UnOp(Meta(Unquote), e) when is_in_filter =>
let e: UExp.t = {
ids: e.ids,
Expand Down
10 changes: 10 additions & 0 deletions src/haz3lcore/tiles/Piece.re
Original file line number Diff line number Diff line change
Expand Up @@ -186,3 +186,13 @@ let is_term = (p: t) =>
| Secondary(_) => false // debatable
| _ => false
};

let mk_tile_id: (Id.t, Form.t, list(list(t))) => t =
(id, form, children) =>
Tile({
id,
label: form.label,
mold: form.mold,
shards: List.mapi((i, _) => i, form.label),
children,
});

0 comments on commit 1d07174

Please sign in to comment.