Skip to content

Commit

Permalink
removed function implicit labelling and rearranging in type consisten…
Browse files Browse the repository at this point in the history 
…cy join
  • Loading branch information
@WondAli
WondAli committed Oct 4, 2024
1 parent f4d778e commit 32173ea
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 124 deletions.
102 changes: 1 addition & 101 deletions src/haz3lcore/dynamics/Elaborator.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -329,75 +329,9 @@ let rec elaborate =
| Fun(p, e, env, n) =>
let (p', typ) = elaborate_pattern(m, p, false);
let (e', tye) = elaborate(m, e);
// ensure that p is a labeled tuple, make it so if needed
let elaborated_typ =
//TODO: better way to get typ'
switch (elaborated_type.term) {
| Arrow(typ', _) => typ'
| Unknown(_) => elaborated_type
| _ => typ
};
let expected_labels = Typ.get_labels(ctx, elaborated_typ);
// TODO: Factor out code
// TODO: Error handling
let rec get_labels_pat = pat => {
switch (DHPat.term_of(pat)) {
| Parens(pat) => get_labels_pat(pat)
| Tuple(ps) => ps
| _ => [pat]
};
};
let rec get_labels_typ = typ => {
switch (Typ.term_of(typ)) {
| Parens(typ) => get_labels_typ(typ)
| Prod(ts) => ts
| _ => [typ]
};
};
let p_list = get_labels_pat(p');
let typ_list = get_labels_typ(typ);
// let reordered_ps =
// LabeledTuple.rearrange_base(expected_labels, p_list);
// let ps: list(DHPat.t) =
// List.map(
// ((optional_label, pat: DHPat.t)) => {
// switch (optional_label) {
// | Some(label) =>
// DHPat.TupLabel(Label(label) |> DHPat.fresh, pat) |> DHPat.fresh
// | None => pat
// }
// },
// reordered_ps,
// );
// let reordered_ts =
// LabeledTuple.rearrange_base(expected_labels, typ_list);
// let ts: list(Typ.t) =
// List.map(
// ((optional_label, typ: Typ.t)) => {
// switch (optional_label) {
// | Some(label) =>
// Typ.TupLabel(Label(label) |> Typ.temp, typ) |> Typ.temp
// | None => typ
// }
// },
// reordered_ts,
// );
let (ps, ts) =
LabeledTuple.rearrange2(
expected_labels,
DHPat.get_label,
Typ.get_label,
p_list,
typ_list,
(name, p) =>
DHPat.TupLabel(Label(name) |> DHPat.fresh, p) |> DHPat.fresh,
(name, t) => Typ.TupLabel(Label(name) |> Typ.temp, t) |> Typ.temp,
);
let p' = Tuple(ps) |> DHPat.fresh;
let typ' = Typ.Prod(ts) |> Typ.temp;
Exp.Fun(p', e', env, n)
|> rewrap
|> cast_from(Arrow(typ', tye) |> Typ.temp);
|> cast_from(Arrow(typ, tye) |> Typ.temp);
| TypFun(tpat, e, name) =>
let (e', tye) = elaborate(m, e);
Exp.TypFun(tpat, e', name)
Expand Down Expand Up @@ -548,40 +482,6 @@ let rec elaborate =
let (a', tya) = elaborate(m, a);
let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp);
// In case of singleton tuple for fun ty_in, implicitly convert arg if necessary
// TODO: Is needed for other Aps?
// let rec get_args = (a: Exp.t, tya, tyf1) =>
// switch (
// a.term,
// Typ.weak_head_normalize(ctx, tya).term,
// Typ.weak_head_normalize(ctx, tyf1).term,
// ) {
// | (Parens(a), _, _) =>
// //TODO: make sure weak_head_normalize doesn't unalign a and tya.
// get_args(a, tya, tyf1)
// | (Cast(a, cty1, cty2), _, _) =>
// let (a, tya) = get_args(a, tya, tyf1);
// (Cast(a, cty1, cty2) |> Exp.fresh, tya);
// | (Tuple(es), Prod(tyas), Prod(tyf1s)) =>
// //rearrange es and tyas to match tyf1s
// let es' =
// LabeledTuple.rearrange(
// Typ.get_label, Exp.get_label, tyf1s, es, (name, e) =>
// TupLabel(Label(name) |> Exp.fresh, e) |> Exp.fresh
// );
// let tyas' =
// LabeledTuple.rearrange(
// Typ.get_label, Typ.get_label, tyf1s, tyas, (name, t) =>
// TupLabel(Label(name) |> Typ.temp, t) |> Typ.temp
// );
// (Tuple(es') |> Exp.fresh, Prod(tyas') |> Typ.temp);
// | (_, _, Prod([{term: TupLabel(_), _}])) => (
// Tuple([a']) |> Exp.fresh,
// Prod([tya]) |> Typ.temp,
// )
// | (_, _, _) => (a, tya)
// };
// let (a', tya) = get_args(a', tya, tyf1);
let a'' = fresh_cast(a', tya, tyf1);
Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
| DeferredAp(f, args) =>
Expand Down
7 changes: 1 addition & 6 deletions src/haz3lcore/lang/term/Typ.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -253,8 +253,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
} else {
None;
}
| (TupLabel(_, ty1), _) => join'(ty1, ty2)
| (_, TupLabel(_, ty2)) => join'(ty1, ty2)
| (TupLabel(_), _) => None
| (Rec(tp1, ty1), Rec(tp2, ty2)) =>
let ctx = Ctx.extend_dummy_tvar(ctx, tp1);
let ty1' =
Expand Down Expand Up @@ -306,10 +305,6 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
if (!l1_valid || !l2_valid || List.length(tys1) != List.length(tys2)) {
None;
} else {
let tys2 =
LabeledTuple.rearrange(get_label, get_label, tys1, tys2, (t, b) =>
TupLabel(Label(t) |> temp, b) |> temp
);
let* tys = ListUtil.map2_opt(join', tys1, tys2);
let+ tys = OptUtil.sequence(tys);
Prod(tys) |> temp;
Expand Down
18 changes: 1 addition & 17 deletions src/haz3lcore/statics/Statics.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -499,25 +499,9 @@ and uexp_to_info_map =
/* add co_ctx to pattern */
let (p'', m) =
go_pat(~is_synswitch=false, ~co_ctx=e.co_ctx, ~mode=mode_pat, p, m);
// convert variables into labeled types if needed
let rec get_var = (p1: UPat.t, p2: Typ.t) =>
switch (p1.term) {
| UPat.Var(s) => Typ.TupLabel(Label(s) |> Typ.temp, p2) |> Typ.temp
| Cast(s, _, _) => get_var(s, p2)
| _ => p2
};
let rec get_typ = (p: UPat.t, t: Typ.t): Typ.t =>
switch (p.term, t.term) {
| (Tuple(l1), Prod(l2)) =>
let pt: list(Typ.t) = List.map2(get_var, l1, l2);
Prod(pt) |> Typ.temp;
| (Cast(s, _, _), t) => get_typ(s, t |> Typ.temp)
| _ => Prod([get_var(p, t)]) |> Typ.temp
};
let pty = get_typ(p, p''.ty);
// TODO: factor out code
let unwrapped_self: Self.exp =
Common(Just(Arrow(pty, e.ty) |> Typ.temp));
Common(Just(Arrow(p''.ty, e.ty) |> Typ.temp));
let is_exhaustive = p'' |> Info.pat_constraint |> Incon.is_exhaustive;
let self =
is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self);
Expand Down

0 comments on commit 32173ea

Please sign in to comment.