Skip to content

Commit

Permalink
Add support for lifting single values into a singleton labeled tuple …
Browse files Browse the repository at this point in the history
…when the label is not present
  • Loading branch information
7h3kk1d committed Oct 14, 2024
1 parent 7688a2b commit c86e5f0
Showing 1 changed file with 23 additions and 0 deletions.
23 changes: 23 additions & 0 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,29 @@ and uexp_to_info_map =
);
let go_pat = upat_to_info_map(~ctx, ~ancestors);
let atomic = self => add(~self, ~co_ctx=CoCtx.empty, m);

// This is to allow lifting single values into a singleton labeled tuple when the label is not present
// TODO Think about this real hard
let uexp =
switch (mode) {
| Ana(ty) =>
let ty = Typ.weak_head_normalize(ctx, ty).term;
switch (ty) {
| Prod([{term: TupLabel({term: Label(l1), _}, ty), _}]) =>
let (e, m) = go(~mode=Mode.Syn, uexp, m);
switch (Typ.weak_head_normalize(e.ctx, e.ty).term) {
| Prod([{term: TupLabel({term: Label(l2), _}, ty), _}])
when l1 == l2 => uexp
| _ =>

Tuple([uexp]) |> Exp.fresh;
};
| _ => uexp
};
| _ => uexp
};
let term = uexp.term;

switch (term) {
| Closure(_) =>
failwith(
Expand Down

0 comments on commit c86e5f0

Please sign in to comment.