From f56a27865f7e880f5bba78ee2f2cfda3d061c5e1 Mon Sep 17 00:00:00 2001 From: WondAli Date: Sun, 4 Feb 2024 20:04:56 -0500 Subject: [PATCH] finished label rearrangements, though need cleanup --- src/haz3lcore/dynamics/PatternMatch.re | 74 +++++++++++++-------- src/haz3lcore/statics/TypBase.re | 92 +++++++++++++++++++++----- 2 files changed, 121 insertions(+), 45 deletions(-) diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re index cf133d7dcc..aec09fa869 100644 --- a/src/haz3lcore/dynamics/PatternMatch.re +++ b/src/haz3lcore/dynamics/PatternMatch.re @@ -304,35 +304,55 @@ and matches_cast_Tuple = DoesNotMatch; } else { assert(List.length(List.combine(dps, ds)) == List.length(elt_casts)); - List.fold_right( - ((((pp, dp), (p, d)), casts), result) => { - switch (result) { - | DoesNotMatch - | IndetMatch => result - | Matches(env) => - switch (pp, p) { - | (Some(sp), Some(s)) => - if (LabeledTuple.compare(sp, s) == 0) { - switch (matches(dp, DHExp.apply_casts(d, casts))) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) - }; - } else { - DoesNotMatch; - } - | (None, None) => - switch (matches(dp, DHExp.apply_casts(d, casts))) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) - } - | (_, _) => DoesNotMatch - } + // List.fold_right( + // ((((pp, dp), (p, d)), casts), result) => { + // switch (result) { + // | DoesNotMatch + // | IndetMatch => result + // | Matches(env) => + // switch (pp, p) { + // | (Some(sp), Some(s)) => + // if (LabeledTuple.compare(sp, s) == 0) { + // switch (matches(dp, DHExp.apply_casts(d, casts))) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env') => Matches(Environment.union(env, env')) + // }; + // } else { + // DoesNotMatch; + // } + // | (None, None) => + // switch (matches(dp, DHExp.apply_casts(d, casts))) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env') => Matches(Environment.union(env, env')) + // } + // | (_, _) => DoesNotMatch + // } + // } + // }, + // List.combine(List.combine(dps, ds), elt_casts), + // Matches(Environment.empty), + // ); + let f = (result, dp, (d, casts)) => { + switch (result) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env) => + switch (matches(dp, DHExp.apply_casts(d, casts))) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env') => Matches(Environment.union(env, env')) } - }, - List.combine(List.combine(dps, ds), elt_casts), + }; + }; + let (dlabs, dvals) = List.split(ds); + LabeledTuple.ana_tuple( + f, Matches(Environment.empty), + DoesNotMatch, + dps, + List.combine(dlabs, List.combine(dvals, elt_casts)), ); }; | Cast(d', Prod(tys), Prod(tys')) => diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 61f9136db3..c903ed0678 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -280,25 +280,81 @@ module rec Typ: { Arrow(ty1, ty2); | (Arrow(_), _) => None | (Prod(tys1), Prod(tys2)) => - let (tysp, _) = List.split(tys1); - let* tys = - ListUtil.map2_opt( - ((p1, t1), (p2, t2)) => - switch (p1, p2) { - | (Some(ap), Some(bp)) => - if (LabeledTuple.compare(ap, bp) == 0) { - join'(t1, t2); - } else { - None; + let (tysp, _) = List.split(tys1); // assuming tys1 is the proper order. + let f = (b, tys1_val, tys2_val) => { + switch (b) { + | false => false + | true => eq(tys1_val, tys2_val) + }; + }; + let valid = LabeledTuple.ana_tuple(f, true, false, tys1, tys2); + valid + ? { + let l2_lab = List.filter(((p, _)) => p != None, tys2); + let l2_none = List.filter(((p, _)) => p == None, tys1); + // is this custom function necessary? + let rec f = + (l1: list('a), l2_lab: list('a), l2_none: list('a)) + : list(option(t)) => + switch (l1) { + | [hd, ...tl] => + switch (hd) { + | (Some(_), l1_val) => + let l2_item = + List.find_opt( + l2_item => { + switch (hd, l2_item) { + | ((Some(s1), _), (Some(s2), _)) => + compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + l2_lab, + ); + switch (l2_item) { + | Some((_, l2_val)) => + [join'(l1_val, l2_val)] @ f(tl, l2_lab, l2_none) + | None => [None] @ f(tl, l2_lab, l2_none) + }; + | (None, l1_val) => + switch (l2_none) { + | [(_, t2), ...tl2] => + [join'(l1_val, t2)] @ f(tl, l2_lab, tl2) + | [] => [None] @ f(tl, l2_lab, l2_none) + } } - | (None, None) => join'(t1, t2) - | (_, _) => None - }, - tys1, - tys2, - ); - let+ tys = OptUtil.sequence(tys); - Prod(List.combine(tysp, tys)); //TODO: Fix this + | [] => [] + }; + let* tys = Some(f(tys1, l2_lab, l2_none)); + // let fail_val = List.init(List.length(tys1), _ => None); + // let f = (l, tys1_val, tys2_val) => { + // l @ [join'(tys1_val, tys2_val)] + // }; + // let* tys = Some(LabeledTuple.ana_tuple(f, [], fail_val, tys1, tys2)); + // ListUtil.map2_opt( + // ((p1, t1), (p2, t2)) => + // switch (p1, p2) { + // | (Some(ap), Some(bp)) => + // if (LabeledTuple.compare(ap, bp) == 0) { + // join'(t1, t2); + // } else { + // None; + // } + // | (None, None) => join'(t1, t2) + // | (_, _) => None + // }, + // tys1, + // tys2, + // ); + let+ tys = OptUtil.sequence(tys); + Prod(List.combine(tysp, tys)); + } //TODO: Fix this + : { + let* tys = Some(List.init(List.length(tys1), _ => None)); + let+ tys = OptUtil.sequence(tys); + Prod(List.combine(tysp, tys)); + }; | (Prod(_), _) => None | (Sum(sm1), Sum(sm2)) => let (sorted1, sorted2) =