From 32173eac5cbb958f64729fbb882875e5e5c723bd Mon Sep 17 00:00:00 2001 From: WondAli Date: Fri, 4 Oct 2024 15:45:44 -0400 Subject: [PATCH] removed function implicit labelling and rearranging in type consistency join --- src/haz3lcore/dynamics/Elaborator.re | 102 +-------------------------- src/haz3lcore/lang/term/Typ.re | 7 +- src/haz3lcore/statics/Statics.re | 18 +---- 3 files changed, 3 insertions(+), 124 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 8210cd7c57..50b3d535d0 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -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) @@ -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) => diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index 6a6df7346e..9a2b757997 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -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' = @@ -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; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 2d4af4d5f6..d8792fc221 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -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);