From 239cf23961de7eecb65795061aeedc7667233f4a Mon Sep 17 00:00:00 2001 From: WondAli Date: Sun, 19 Nov 2023 17:27:13 -0500 Subject: [PATCH 1/6] moved all labeled_tuple progress to a new branch --- src/haz3lcore/LabeledTuple.re | 12 ++ src/haz3lcore/dynamics/Builtins.re | 20 ++-- src/haz3lcore/dynamics/DH.re | 28 ++++- src/haz3lcore/dynamics/DHPat.re | 6 +- src/haz3lcore/dynamics/Elaborator.re | 49 +++++++- src/haz3lcore/dynamics/Evaluator.re | 120 +++++++++++++++---- src/haz3lcore/dynamics/EvaluatorPost.re | 19 ++- src/haz3lcore/dynamics/Substitution.re | 4 +- src/haz3lcore/lang/Form.re | 3 + src/haz3lcore/statics/MakeTerm.re | 98 ++++++++++++++- src/haz3lcore/statics/Mode.re | 7 +- src/haz3lcore/statics/Statics.re | 40 ++++++- src/haz3lcore/statics/Term.re | 30 ++++- src/haz3lcore/statics/TermBase.re | 18 ++- src/haz3lcore/statics/TypBase.re | 81 ++++++++++--- src/haz3lcore/zipper/EditorUtil.re | 1 + src/haz3lschool/SyntaxTest.re | 34 ++++-- src/haz3lweb/view/LangDoc.re | 97 +++++++++++++++ src/haz3lweb/view/Type.re | 4 +- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 4 +- src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re | 3 +- src/haz3lweb/view/dhcode/layout/HTypDoc.re | 2 + 22 files changed, 575 insertions(+), 105 deletions(-) create mode 100644 src/haz3lcore/LabeledTuple.re diff --git a/src/haz3lcore/LabeledTuple.re b/src/haz3lcore/LabeledTuple.re new file mode 100644 index 0000000000..bf1e6fb963 --- /dev/null +++ b/src/haz3lcore/LabeledTuple.re @@ -0,0 +1,12 @@ +open Sexplib.Std; + +[@deriving (show({with_path: false}), sexp, yojson)] +type t = string; + +let eq = String.equal; + +let length = String.length; + +let valid_regex = + Re.Str.regexp("^\\([a-zA-Z]\\|_[_a-zA-Z0-9]\\)[_a-zA-Z0-9']*$"); +let is_valid = s => Re.Str.string_match(valid_regex, s, 0); diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 85bda5dbe1..cff7fc3775 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -161,7 +161,7 @@ module Pervasives = { let int_mod = (name, r) => switch (r) { - | BoxedValue(Tuple([IntLit(n), IntLit(m)]) as d1) => + | BoxedValue(Tuple([(_, IntLit(n)), (_, IntLit(m))]) as d1) => switch (m) { | 0 => Indet(InvalidOperation(ApBuiltin(name, [d1]), DivideByZero)) @@ -183,7 +183,7 @@ module Pervasives = { let string_compare = unary( fun - | Tuple([StringLit(s1), StringLit(s2)]) => + | Tuple([(_, StringLit(s1)), (_, StringLit(s2))]) => Ok(IntLit(String.compare(s1, s2))) | d => Error(InvalidBoxedTuple(d)), ); @@ -203,7 +203,7 @@ module Pervasives = { let string_concat = unary( fun - | Tuple([StringLit(s1), ListLit(_, _, _, xs)]) => + | Tuple([(_, StringLit(s1)), (_, ListLit(_, _, _, xs))]) => switch (xs |> List.map(string_of) |> Util.OptUtil.sequence) { | None => Error(InvalidBoxedStringLit(List.hd(xs))) | Some(xs) => Ok(StringLit(String.concat(s1, xs))) @@ -214,7 +214,7 @@ module Pervasives = { let string_sub = name => unary'( fun - | Tuple([StringLit(s), IntLit(idx), IntLit(len)]) as d => + | Tuple([(_, StringLit(s)), (_, IntLit(idx)), (_, IntLit(len))]) as d => try(Ok(BoxedValue(StringLit(String.sub(s, idx, len))))) { | _ => let d' = DHExp.ApBuiltin(name, [d]); @@ -260,20 +260,24 @@ module Pervasives = { |> fn("asin", Arrow(Float, Float), asin) |> fn("acos", Arrow(Float, Float), acos) |> fn("atan", Arrow(Float, Float), atan) - |> fn("mod", Arrow(Prod([Int, Int]), Int), int_mod) + |> fn("mod", Arrow(Prod([(None, Int), (None, Int)]), Int), int_mod) |> fn("string_length", Arrow(String, Int), string_length) |> fn( "string_compare", - Arrow(Prod([String, String]), Int), + Arrow(Prod([(None, String), (None, String)]), Int), string_compare, ) |> fn("string_trim", Arrow(String, String), string_trim) |> fn( "string_concat", - Arrow(Prod([String, List(String)]), String), + Arrow(Prod([(None, String), (None, List(String))]), String), string_concat, ) - |> fn("string_sub", Arrow(Prod([String, Int, Int]), String), string_sub); + |> fn( + "string_sub", + Arrow(Prod([(None, String), (None, Int), (None, Int)]), String), + string_sub, + ); }; let ctx_init: Ctx.t = diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re index b2d0a2bd17..874b64c4ec 100644 --- a/src/haz3lcore/dynamics/DH.re +++ b/src/haz3lcore/dynamics/DH.re @@ -29,7 +29,8 @@ module rec DHExp: { | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t)) | Cons(t, t) | ListConcat(t, t) - | Tuple(list(t)) + | TupLabel(DHPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Prj(t, int) | Constructor(string) | ConsistentCase(case) @@ -43,7 +44,7 @@ module rec DHExp: { let constructor_string: t => string; - let mk_tuple: list(t) => t; + let mk_tuple: list((option(LabeledTuple.t), t)) => t; let cast: (t, Typ.t, Typ.t) => t; @@ -83,7 +84,8 @@ module rec DHExp: { | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t)) | Cons(t, t) | ListConcat(t, t) - | Tuple(list(t)) + | TupLabel(DHPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Prj(t, int) | Constructor(string) | ConsistentCase(case) @@ -122,6 +124,7 @@ module rec DHExp: { | ListLit(_) => "ListLit" | Cons(_, _) => "Cons" | ListConcat(_, _) => "ListConcat" + | TupLabel(_) => "Tuple Item Label" | Tuple(_) => "Tuple" | Prj(_) => "Prj" | Constructor(_) => "Constructor" @@ -132,7 +135,7 @@ module rec DHExp: { | InvalidOperation(_) => "InvalidOperation" }; - let mk_tuple: list(t) => t = + let mk_tuple: list((option(LabeledTuple.t), t)) => t = fun | [] | [_] => failwith("mk_tuple: expected at least 2 elements") @@ -153,7 +156,8 @@ module rec DHExp: { | Closure(ei, d) => Closure(ei, strip_casts(d)) | Cast(d, _, _) => strip_casts(d) | FailedCast(d, _, _) => strip_casts(d) - | Tuple(ds) => Tuple(ds |> List.map(strip_casts)) + | TupLabel(p, t) => TupLabel(p, strip_casts(t)) + | Tuple(ds) => Tuple(ds |> List.map(((p, e)) => (p, strip_casts(e)))) | Prj(d, n) => Prj(strip_casts(d), n) | Cons(d1, d2) => Cons(strip_casts(d1), strip_casts(d2)) | ListConcat(d1, d2) => ListConcat(strip_casts(d1), strip_casts(d2)) @@ -221,9 +225,20 @@ module rec DHExp: { fast_equal(d11, d12) && fast_equal(d21, d22) | (ListConcat(d11, d21), ListConcat(d12, d22)) => fast_equal(d11, d12) && fast_equal(d21, d22) + | (TupLabel(_, e1), TupLabel(_, e2)) => fast_equal(e1, e2) // TODO: Not right? | (Tuple(ds1), Tuple(ds2)) => List.length(ds1) == List.length(ds2) - && List.for_all2(fast_equal, ds1, ds2) + && List.for_all2( + ((ap, ad), (bp, bd)) => + switch (ap, bp) { + | (Some(ap), Some(bp)) => + compare(ap, bp) == 0 && fast_equal(ad, bd) + | (None, None) => fast_equal(ad, bd) + | (_, _) => false + }, + ds1, + ds2, + ) | (Prj(d1, n), Prj(d2, m)) => n == m && fast_equal(d1, d2) | (ApBuiltin(f1, args1), ApBuiltin(f2, args2)) => f1 == f2 && List.for_all2(fast_equal, args1, args2) @@ -255,6 +270,7 @@ module rec DHExp: { | (Cons(_), _) | (ListConcat(_), _) | (ListLit(_), _) + | (TupLabel(_), _) | (Tuple(_), _) | (Prj(_), _) | (BinBoolOp(_), _) diff --git a/src/haz3lcore/dynamics/DHPat.re b/src/haz3lcore/dynamics/DHPat.re index 0cac9b9814..e1ede68cbc 100644 --- a/src/haz3lcore/dynamics/DHPat.re +++ b/src/haz3lcore/dynamics/DHPat.re @@ -15,11 +15,11 @@ type t = | StringLit(string) | ListLit(Typ.t, list(t)) | Cons(t, t) - | Tuple(list(t)) + | Tuple(list((option(LabeledTuple.t), t))) | Constructor(string) | Ap(t, t); -let mk_tuple: list(t) => t = +let mk_tuple: list((option(LabeledTuple.t), t)) => t = fun | [] | [_] => failwith("mk_tuple: expected at least 2 elements") @@ -42,7 +42,7 @@ let rec binds_var = (x: Var.t, dp: t): bool => | Constructor(_) | ExpandingKeyword(_, _, _) => false | Var(y) => Var.eq(x, y) - | Tuple(dps) => dps |> List.exists(binds_var(x)) + | Tuple(dps) => dps |> List.exists(((_, e)) => binds_var(x, e)) | Cons(dp1, dp2) => binds_var(x, dp1) || binds_var(x, dp2) | ListLit(_, d_list) => let new_list = List.map(binds_var(x), d_list); diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index ba13bd069c..1ef8da1c78 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -53,10 +53,16 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => let (_, ana_out) = Typ.matched_arrow(ctx, ana_ty); let (self_in, _) = Typ.matched_arrow(ctx, self_ty); DHExp.cast(d, Arrow(self_in, ana_out), ana_ty); + | TupLabel(_) => + //TODO check this + switch (ana_ty) { + | Unknown(prov) => DHExp.cast(d, self_ty, Unknown(prov)) + | _ => d + } | Tuple(ds) => switch (ana_ty) { | Unknown(prov) => - let us = List.init(List.length(ds), _ => Typ.Unknown(prov)); + let us = ds |> List.map(((p, _)) => (p, Typ.Unknown(prov))); DHExp.cast(d, Prod(us), Unknown(prov)); | _ => d } @@ -145,9 +151,25 @@ let rec dhexp_of_uexp = let* d1 = dhexp_of_uexp(m, body); let+ ty = fixed_pat_typ(m, p); DHExp.Fun(dp, ty, d1, None); + | TupLabel(_, e) => + //let* dp = dhpat_of_upat(m, p); + let+ de = dhexp_of_uexp(m, e); + //DHExp.TupLabel(dp, de); // TODO check this. Remove from dh.re? + de; | Tuple(es) => - let+ ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence; - DHExp.Tuple(ds); + /*let tempfuncname = p => + switch (p) { + | Some(d) => dhpat_of_upat(m, d) + | None => None + }; + let dsp = es |> List.map(((p, _)) => tempfuncname(p));*/ + let (dsp, _) = List.split(es); + let+ ds = + es + |> List.map(((_, d)) => dhexp_of_uexp(m, d)) + |> OptUtil.sequence; + DHExp.Tuple(List.combine(dsp, ds)); + //TODO: Fix this | Cons(e1, e2) => let* dc1 = dhexp_of_uexp(m, e1); let+ dc2 = dhexp_of_uexp(m, e2); @@ -219,7 +241,10 @@ let rec dhexp_of_uexp = let ddef = switch (ddef) { | Tuple(a) => - DHExp.Tuple(List.map2(s => add_name(Some(s)), fs, a)) + let (ap, a) = List.split(a); + DHExp.Tuple( + List.combine(ap, List.map2(s => add_name(Some(s)), fs, a)), + ); | _ => ddef }; let uniq_id = List.nth(def.ids, 0); @@ -320,9 +345,21 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => { let* d_hd = dhpat_of_upat(m, hd); let* d_tl = dhpat_of_upat(m, tl); wrap(Cons(d_hd, d_tl)); + // TODO: Fix this + | TupLabel(_, p2) => + let* dp2 = dhpat_of_upat(m, p2); + wrap(dp2); | Tuple(ps) => - let* ds = ps |> List.map(dhpat_of_upat(m)) |> OptUtil.sequence; - wrap(DHPat.Tuple(ds)); + /*let tempfuncname = p => + switch (p) { + | Some(d) => dhpat_of_upat(m, d) + | None => None + }; + let dsp = ps |> List.map(((p, _)) => tempfuncname(p));*/ + let (dsp, _) = List.split(ps); + let* ds = + ps |> List.map(((_, d)) => dhpat_of_upat(m, d)) |> OptUtil.sequence; + wrap(DHPat.Tuple(List.combine(dsp, ds))); | Var(name) => Some(Var(name)) | Parens(p) => dhpat_of_upat(m, p) | Ap(p1, p2) => diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index cc9d2525df..4d53fa0209 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -24,7 +24,9 @@ let const_unknown: 'a => Typ.t = _ => Unknown(Internal); let grounded_Arrow = NotGroundOrHole(Arrow(Unknown(Internal), Unknown(Internal))); let grounded_Prod = length => - NotGroundOrHole(Prod(ListUtil.replicate(length, Typ.Unknown(Internal)))); + NotGroundOrHole( + Prod(ListUtil.replicate(length, (None, Typ.Unknown(Internal)))), + ); let grounded_Sum = (sm: Typ.sum_map): ground_cases => { let sm' = sm |> ConstructorMap.map(Option.map(const_unknown)); NotGroundOrHole(Sum(sm')); @@ -52,7 +54,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { fun | Typ.Unknown(_) => true | _ => false, - tys, + tys |> List.map(((_, b)) => b), )) { Ground; } else { @@ -203,15 +205,31 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => DoesNotMatch; } else { List.fold_left2( - (result, dp, d) => + (result, (pp, dp), (p, d)) => switch (result) { | DoesNotMatch => DoesNotMatch | IndetMatch => IndetMatch | Matches(env) => - switch (matches(dp, d)) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) + // TODO: Need a function to reorganize lists to match up vars + // TODO: check if this logic is right + switch (pp, p) { + | (Some(sp), Some(s)) => + if (compare(sp, s) == 0) { + switch (matches(dp, d)) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env') => Matches(Environment.union(env, env')) + }; + } else { + DoesNotMatch; + } + | (None, None) => + switch (matches(dp, d)) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env') => Matches(Environment.union(env, env')) + } + | (_, _) => DoesNotMatch } }, Matches(Environment.empty), @@ -224,7 +242,13 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => matches_cast_Tuple( dps, d, - List.map(p => [p], List.combine(tys, tys')), + List.map( + p => [p], + List.combine( + tys, + List.init(List.length(tys), t => (None, const_unknown(t))), + ), + ), ); | (Tuple(dps), Cast(d, Prod(tys), Unknown(_))) => matches_cast_Tuple( @@ -232,7 +256,10 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => d, List.map( p => [p], - List.combine(tys, List.init(List.length(tys), const_unknown)), + List.combine( + List.init(List.length(tys), t => (None, const_unknown(t))), + tys, + ), ), ) | (Tuple(dps), Cast(d, Unknown(_), Prod(tys'))) => @@ -241,7 +268,10 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => d, List.map( p => [p], - List.combine(List.init(List.length(tys'), const_unknown), tys'), + List.combine( + List.init(List.length(tys'), t => (None, const_unknown(t))), + tys', + ), ), ) | (Tuple(_), Cast(_)) => DoesNotMatch @@ -317,6 +347,7 @@ and matches_cast_Sum = | FloatLit(_) | StringLit(_) | ListLit(_) + | TupLabel(_) | Tuple(_) | Prj(_) | ConsistentCase(_) @@ -328,34 +359,61 @@ and matches_cast_Sum = } and matches_cast_Tuple = ( - dps: list(DHPat.t), + dps: list((option(LabeledTuple.t), DHPat.t)), d: DHExp.t, - elt_casts: list(list((Typ.t, Typ.t))), + elt_casts: + list( + list( + ( + (option(LabeledTuple.t), Typ.t), + (option(LabeledTuple.t), Typ.t), + ), + ), + ), ) : match_result => + // TODO: Fix this whole thing switch (d) { + | TupLabel(_) => DoesNotMatch | Tuple(ds) => + let elt_casts = + elt_casts + |> List.map(l => l |> List.map((((_, e1), (_, e2))) => (e1, e2))); if (List.length(dps) != List.length(ds)) { DoesNotMatch; } else { assert(List.length(List.combine(dps, ds)) == List.length(elt_casts)); List.fold_right( - (((dp, d), casts), result) => { + ((((pp, dp), (p, d)), casts), result) => { switch (result) { | DoesNotMatch | IndetMatch => result | Matches(env) => - switch (matches(dp, DHExp.apply_casts(d, casts))) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) + switch (pp, p) { + | (Some(sp), Some(s)) => + if (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), ); - } + }; | Cast(d', Prod(tys), Prod(tys')) => if (List.length(dps) != List.length(tys)) { DoesNotMatch; @@ -368,14 +426,14 @@ and matches_cast_Tuple = ); } | Cast(d', Prod(tys), Unknown(_)) => - let tys' = List.init(List.length(tys), const_unknown); + let tys' = List.init(List.length(tys), t => (None, const_unknown(t))); matches_cast_Tuple( dps, d', List.map2(List.cons, List.combine(tys, tys'), elt_casts), ); | Cast(d', Unknown(_), Prod(tys')) => - let tys = List.init(List.length(tys'), const_unknown); + let tys = List.init(List.length(tys'), t => (None, const_unknown(t))); matches_cast_Tuple( dps, d', @@ -540,6 +598,7 @@ and matches_cast_Cons = | TestLit(_) => DoesNotMatch | FloatLit(_) => DoesNotMatch | StringLit(_) => DoesNotMatch + | TupLabel(_) => DoesNotMatch | Tuple(_) => DoesNotMatch | Prj(_) => DoesNotMatch | Constructor(_) => DoesNotMatch @@ -843,8 +902,12 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = }; }; + | TupLabel(_) => BoxedValue(d) |> return //TODO: Fix this? + | Tuple(ds) => - let+ lst = ds |> List.map(evaluate(env)) |> sequence; + //TODO: Fix this + let lstp = ds |> List.map(((p, _)) => p); + let+ lst = ds |> List.map(((_, d)) => evaluate(env, d)) |> sequence; let (ds', indet) = List.fold_right( (el, (lst, indet)) => @@ -856,7 +919,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = ([], false), ); - let d = DHExp.Tuple(ds'); + let d = DHExp.Tuple(List.combine(lstp, ds')); if (indet) { Indet(d); } else { @@ -881,6 +944,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = ), ); } else { + let ds = ds |> List.map(((_, e)) => e); return(BoxedValue(List.nth(ds, n))); } | Indet(Tuple(ds) as rv) => @@ -891,6 +955,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = ), ); } else { + let ds = ds |> List.map(((_, e)) => e); return(Indet(List.nth(ds, n))); } | BoxedValue(Cast(targ', Prod(tys), Prod(tys')) as rv) @@ -902,6 +967,8 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = ), ); } else { + let (_, tys) = List.split(tys); + let (_, tys') = List.split(tys'); let ty = List.nth(tys, n); let ty' = List.nth(tys', n); evaluate(env, Cast(Prj(targ', n), ty, ty')); @@ -1211,9 +1278,14 @@ and evaluate_test = | Ap(fn, Tuple(args)) => let* args_d: list(EvaluatorResult.t) = - args |> List.map(evaluate(env)) |> sequence; + args |> List.map(((_, e)) => evaluate(env, e)) |> sequence; let arg_show = - DHExp.Ap(fn, Tuple(List.map(EvaluatorResult.unbox, args_d))); + DHExp.Ap( + fn, + Tuple( + List.map(arg => (None, EvaluatorResult.unbox(arg)), args_d), + ), + ); let* arg_result = evaluate(env, arg_show); (arg_show, arg_result) |> return; diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re index 01aef79d29..832f4e76f5 100644 --- a/src/haz3lcore/dynamics/EvaluatorPost.re +++ b/src/haz3lcore/dynamics/EvaluatorPost.re @@ -109,10 +109,10 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) => let+ ds = ds |> List.fold_left( - (ds, d) => { + (ds, (p, d)) => { let* ds = ds; let+ d = pp_eval(d); - ds @ [d]; + ds @ [(p, d)]; }, return([]), ); @@ -137,6 +137,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) => /* These expression forms should not exist outside closure in evaluated result */ | BoundVar(_) | Let(_) + | TupLabel(_) | ConsistentCase(_) | Fun(_) | EmptyHole(_) @@ -331,14 +332,18 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) => ); ListLit(a, b, c, ds); + | TupLabel(dp, d1) => + let* d1' = pp_uneval(env, d1); + TupLabel(dp, d1') |> return; + | Tuple(ds) => let+ ds = ds |> List.fold_left( - (ds, d) => { + (ds, (p, d)) => { let* ds = ds; - let+ d = pp_uneval(env, d); - ds @ [d]; + let+ d = pp_eval(d); + ds @ [(p, d)]; }, return([]), ); @@ -462,9 +467,11 @@ let rec track_children_of_hole = hii, ) + | TupLabel(_, d) => track_children_of_hole(hii, parent, d) + | Tuple(ds) => List.fold_right( - (d, hii) => track_children_of_hole(hii, parent, d), + ((_, d), hii) => track_children_of_hole(hii, parent, d), ds, hii, ) diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index 92f8cff0fe..d66799f8ae 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -67,7 +67,9 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => let d3 = subst_var(d1, x, d3); let d4 = subst_var(d1, x, d4); ListConcat(d3, d4); - | Tuple(ds) => Tuple(List.map(subst_var(d1, x), ds)) + | TupLabel(p, d3) => TupLabel(p, subst_var(d1, x, d3)) + | Tuple(ds) => + Tuple(List.map(((p, d)) => (p, subst_var(d1, x, d)), ds)) | Prj(d, n) => Prj(subst_var(d1, x, d), n) | BinBoolOp(op, d3, d4) => let d3 = subst_var(d1, x, d3); diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 5409a3be17..46c50253a3 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -265,6 +265,9 @@ let forms: list((string, t)) = [ mk(ds, ["type", "=", "in"], mk_pre(P.let_, Exp, [TPat, Typ])), ), ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))), + ("tuple_label_exp", mk(ss, ["="], mk_bin'(P.ann, Exp, Pat, [], Exp))), // TODO: Rename + ("tuple_label_pat", mk(ss, ["="], mk_bin'(P.ann, Pat, Pat, [], Pat))), // TODO: Rename + ("tuple_label_typ", mk(ss, ["="], mk_bin'(P.ann, Typ, Pat, [], Typ))), // TODO: Rename ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))), ( "rule", diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 7d7a159d29..5be0d212b7 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -48,6 +48,76 @@ let is_tuple_pat = is_nary(TermBase.Any.is_pat, ","); let is_tuple_typ = is_nary(TermBase.Any.is_typ, ","); let is_typ_bsum = is_nary(TermBase.Any.is_typ, "+"); +// TODO: Clean this up +// Tuplabel util functions +// TODO: filter patternss so that result (option(Var.t), UExp.t) + +let return_tuplabel = (p: UPat.t, t: 'a): (option(LabeledTuple.t), 'a) => + switch (p.term) { + | Var(s) => (Some(s), t) + | _ => raise(EvaluatorError.Exception(BadBuiltinAp("", []))) // TOOD: put the real error + }; + +let return_tuplabel_exp = + (p: UPat.t, t: UExp.t): (option(LabeledTuple.t), UExp.t) => + switch (p.term) { + | Var(s) => (Some(s), t) + | _ => + let t: UExp.t = {ids: t.ids, term: Invalid("")}; + (None, t); + }; + +let return_tuplabel_pat = + (p: UPat.t, t: UPat.t): (option(LabeledTuple.t), UPat.t) => + switch (p.term) { + | Var(s) => (Some(s), t) + | _ => + let t: UPat.t = {ids: t.ids, term: Invalid("")}; + (None, t); + }; + +let return_tuplabel_typ = + (p: UPat.t, t: UTyp.t): (option(LabeledTuple.t), UTyp.t) => + switch (p.term) { + | Var(s) => (Some(s), t) + | _ => + let t: UTyp.t = {ids: t.ids, term: Invalid("")}; + (None, t); + }; + +let make_labeled_tuple_exp_helper = + (exp: UExp.t): (option(LabeledTuple.t), UExp.t) => + switch (exp.term) { + | TupLabel(p, e) => return_tuplabel_exp(p, e) + | _ => (None, exp) + }; + +let make_labeled_tuple_exp = (es: list(UExp.t)) => { + es |> List.map(make_labeled_tuple_exp_helper); +}; + +let make_labeled_tuple_pat_helper = + (pat: UPat.t): (option(LabeledTuple.t), UPat.t) => + switch (pat.term) { + | TupLabel(p, pt) => return_tuplabel_pat(p, pt) + | _ => (None, pat) + }; + +let make_labeled_tuple_pat = (ps: list(UPat.t)) => { + ps |> List.map(make_labeled_tuple_pat_helper); +}; + +let make_labeled_tuple_typ_helper = + (typ: UTyp.t): (option(LabeledTuple.t), UTyp.t) => + switch (typ.term) { + | TupLabel(p, t) => return_tuplabel_typ(p, t) + | _ => (None, typ) + }; + +let make_labeled_tuple_typ = (ts: list('a)) => { + ts |> List.map(make_labeled_tuple_typ_helper); +}; + let is_grout = tiles => Aba.get_as(tiles) |> List.map(snd) |> List.for_all((==)(([" "], []))); @@ -161,7 +231,9 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["(", ")"], [Exp(body)]) => ret(Parens(body)) | (["[", "]"], [Exp(body)]) => switch (body) { - | {ids, term: Tuple(es)} => (ListLit(es), ids) + | {ids, term: Tuple(es)} => + let (_, es) = List.split(es); + (ListLit(es), ids); | term => ret(ListLit([term])) } | (["test", "end"], [Exp(test)]) => ret(Test(test)) @@ -202,9 +274,15 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { } | _ => ret(hole(tm)) } + | Bin(Pat(p), tiles, Exp(e)) as tm => + switch (tiles) { + | ([(_id, (["="], []))], []) => ret(TupLabel(p, e)) + | _ => ret(hole(tm)) + } | Bin(Exp(l), tiles, Exp(r)) as tm => switch (is_tuple_exp(tiles)) { - | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r])) + | Some(between_kids) => + ret(Tuple(make_labeled_tuple_exp([l] @ between_kids @ [r]))) | None => switch (tiles) { | ([(_id, t)], []) => @@ -279,7 +357,9 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | (["(", ")"], [Pat(body)]) => Parens(body) | (["[", "]"], [Pat(body)]) => switch (body) { - | {term: Tuple(ps), _} => ListLit(ps) + | {term: Tuple(ps), _} => + let (_, ps) = List.split(ps); + ListLit(ps); | term => ListLit([term]) } | _ => hole(tm) @@ -306,9 +386,11 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { } | Bin(Pat(l), tiles, Pat(r)) as tm => switch (is_tuple_pat(tiles)) { - | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r])) + | Some(between_kids) => + ret(Tuple(make_labeled_tuple_pat([l] @ between_kids @ [r]))) | None => switch (tiles) { + | ([(_id, (["="], []))], []) => ret(TupLabel(l, r)) | ([(_id, (["::"], []))], []) => ret(Cons(l, r)) | _ => ret(hole(tm)) } @@ -365,9 +447,15 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { ret(Sum(List.map(parse_sum_term, [t1] @ between_kids @ [t2]))) | None => ret(hole(tm)) } + | Bin(Pat(p), tiles, Typ(t)) as tm => + switch (tiles) { + | ([(_id, (["="], []))], []) => ret(TupLabel(p, t)) + | _ => ret(hole(tm)) + } | Bin(Typ(l), tiles, Typ(r)) as tm => switch (is_tuple_typ(tiles)) { - | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r])) + | Some(between_kids) => + ret(Tuple(make_labeled_tuple_typ([l] @ between_kids @ [r]))) | None => switch (tiles) { | ([(_id, (["->"], []))], []) => ret(Arrow(l, r)) diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index f8dc127b9f..0f96e117c1 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -39,11 +39,12 @@ let of_arrow = (ctx: Ctx.t, mode: t): (t, t) => | Ana(ty) => ty |> Typ.matched_arrow(ctx) |> TupleUtil.map2(ana) }; -let of_prod = (ctx: Ctx.t, mode: t, length): list(t) => +let of_prod = + (ctx: Ctx.t, mode: t, es: list((option(LabeledTuple.t), 'a))): list(t) => switch (mode) { | Syn - | SynFun => List.init(length, _ => Syn) - | Ana(ty) => ty |> Typ.matched_prod(ctx, length) |> List.map(ana) + | SynFun => List.init(List.length(es), _ => Syn) + | Ana(ty) => Typ.matched_prod(ctx, es, ty) |> List.map(ty => Ana(ty)) }; let of_cons_hd = (ctx: Ctx.t, mode: t): t => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index df41335cc8..108d199f21 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -210,11 +210,27 @@ and uexp_to_info_map = let (e1, m) = go(~mode=Ana(ty1), e1, m); let (e2, m) = go(~mode=Ana(ty2), e2, m); add(~self=Just(ty_out), ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]), m); + // TODO: Fix this + | TupLabel(p, e) => + let (e, m) = go(~mode=Syn, e, m); + // probably no need for p + let (p, m) = + upat_to_info_map( + ~is_synswitch=true, + ~ctx, + ~ancestors, + ~mode=Mode.Ana(e.ty), + p, + m, + ); + add(~self=Just(e.ty), ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m); | Tuple(es) => - let modes = Mode.of_prod(ctx, mode, List.length(es)); - let (es, m) = map_m_go(m, modes, es); + let (esp, ese) = List.split(es); + // TODO: check labels within this of_prod + let modes = Mode.of_prod(ctx, mode, es); + let (es, m) = map_m_go(m, modes, ese); add( - ~self=Just(Prod(List.map(Info.exp_ty, es))), + ~self=Just(Prod(List.combine(esp, List.map(Info.exp_ty, es)))), ~co_ctx=CoCtx.union(List.map(Info.exp_co_ctx, es)), m, ); @@ -397,10 +413,16 @@ and upat_to_info_map = Info.fixed_typ_pat(ctx, mode, Common(Just(Unknown(Internal)))); let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); add(~self=Just(unknown), ~ctx=Ctx.extend(ctx, entry), m); + // TODO: Fix this + | TupLabel(p1, p2) => + let (p2, m) = go(~ctx, ~mode, p2, m); + let (_, m) = go(~ctx, ~mode, p1, m); + add(~self=Just(p2.ty), ~ctx=p2.ctx, m); | Tuple(ps) => - let modes = Mode.of_prod(ctx, mode, List.length(ps)); - let (ctx, tys, m) = ctx_fold(ctx, m, ps, modes); - add(~self=Just(Prod(tys)), ~ctx, m); + let (psp, pse) = List.split(ps); + let modes = Mode.of_prod(ctx, mode, ps); + let (ctx, tys, m) = ctx_fold(ctx, m, pse, modes); + add(~self=Just(Prod(List.combine(psp, tys))), ~ctx, m); | Parens(p) => let (p, m) = go(~ctx, ~mode, p, m); add(~self=Just(p.ty), ~ctx=p.ctx, m); @@ -454,7 +476,13 @@ and utyp_to_info_map = let m = go(t1, m) |> snd; let m = go(t2, m) |> snd; add(m); + | TupLabel(p, t) => + let m = go(t, m) |> snd; + let (_, m) = + upat_to_info_map(~is_synswitch=true, ~ctx, ~ancestors, ~mode=Syn, p, m); + add(m); | Tuple(ts) => + let ts = ts |> List.map(((_, t)) => t); let m = map_m(go, ts, m) |> snd; add(m); | Ap(t1, t2) => diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 1ca34e57eb..c191a9e93f 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -30,6 +30,7 @@ module UTyp = { | Bool | String | Arrow + | TupLabel | Tuple | Sum | List @@ -64,6 +65,7 @@ module UTyp = { | Arrow(_) => Arrow | Var(_) => Var | Constructor(_) => Constructor + | TupLabel(_) => TupLabel | Tuple(_) => Tuple | Parens(_) => Parens | Ap(_) => Ap @@ -82,6 +84,7 @@ module UTyp = { | Constructor => "Sum constructor" | List => "List type" | Arrow => "Function type" + | TupLabel => "Tuple Lable" | Tuple => "Product type" | Sum => "Sum type" | Parens => "Parenthesized type" @@ -99,6 +102,7 @@ module UTyp = { | Bool | String | List(_) + | TupLabel(_) | Tuple(_) | Var(_) | Constructor(_) @@ -124,7 +128,8 @@ module UTyp = { | None => Unknown(Free(name)) } | Arrow(u1, u2) => Arrow(to_typ(ctx, u1), to_typ(ctx, u2)) - | Tuple(us) => Prod(List.map(to_typ(ctx), us)) + | TupLabel(_, ty) => to_typ(ctx, ty) // TODO: this. Lookup in ctx and reorgnize + | Tuple(us) => Prod(us |> List.map(((p, e)) => (p, to_typ(ctx, e)))) | Sum(uts) => Sum(to_ctr_map(ctx, uts)) | List(u) => List(to_typ(ctx, u)) | Parens(u) => to_typ(ctx, u) @@ -201,6 +206,7 @@ module UPat = { | Constructor | Cons | Var + | TupLabel | Tuple | Parens | Ap @@ -234,6 +240,7 @@ module UPat = { | Constructor(_) => Constructor | Cons(_) => Cons | Var(_) => Var + | TupLabel(_) => TupLabel | Tuple(_) => Tuple | Parens(_) => Parens | Ap(_) => Ap @@ -254,6 +261,7 @@ module UPat = { | Constructor => "Constructor" | Cons => "Cons" | Var => "Variable binding" + | TupLabel => "Tuple Label" | Tuple => "Tuple" | Parens => "Parenthesized pattern" | Ap => "Constructor application" @@ -275,6 +283,7 @@ module UPat = { | Triv | ListLit(_) | Cons(_, _) + | TupLabel(_, _) | Tuple(_) | Constructor(_) | Ap(_) => false @@ -297,6 +306,7 @@ module UPat = { | ListLit(_) | Cons(_, _) | Var(_) + | TupLabel(_, _) | Tuple(_) | Constructor(_) | Ap(_) => false @@ -308,7 +318,9 @@ module UPat = { || ( switch (pat.term) { | Parens(pat) => is_tuple_of_arrows(pat) - | Tuple(pats) => pats |> List.for_all(is_fun_var) + | Tuple(pats) => + let pats = pats |> List.map(((_, u)) => u); + pats |> List.for_all(is_fun_var); | Invalid(_) | EmptyHole | MultiHole(_) @@ -322,6 +334,7 @@ module UPat = { | Cons(_, _) | Var(_) | TypeAnn(_) + | TupLabel(_) | Constructor(_) | Ap(_) => false } @@ -343,6 +356,7 @@ module UPat = { | Triv | ListLit(_) | Cons(_, _) + | TupLabel(_, _) | Tuple(_) | Constructor(_) | Ap(_) => None @@ -370,6 +384,7 @@ module UPat = { | ListLit(_) | Cons(_, _) | Var(_) + | TupLabel(_, _) | Tuple(_) | Constructor(_) | Ap(_) => None @@ -383,6 +398,7 @@ module UPat = { switch (pat.term) { | Parens(pat) => get_recursive_bindings(pat) | Tuple(pats) => + let pats = pats |> List.map(((_, p)) => p); let fun_vars = pats |> List.map(get_fun_var); if (List.exists(Option.is_none, fun_vars)) { None; @@ -402,6 +418,7 @@ module UPat = { | Cons(_, _) | Var(_) | TypeAnn(_) + | TupLabel(_, _) | Constructor(_) | Ap(_) => None } @@ -431,6 +448,7 @@ module UExp = { | ListLit | Constructor | Fun + | TupLabel | Tuple | Var | Let @@ -471,6 +489,7 @@ module UExp = { | ListLit(_) => ListLit | Constructor(_) => Constructor | Fun(_) => Fun + | TupLabel(_) => TupLabel | Tuple(_) => Tuple | Var(_) => Var | Let(_) => Let @@ -558,6 +577,7 @@ module UExp = { | ListLit => "List literal" | Constructor => "Constructor" | Fun => "Function literal" + | TupLabel => "Tuple Label Exp" | Tuple => "Tuple literal" | Var => "Variable reference" | Let => "Let expression" @@ -587,6 +607,7 @@ module UExp = { | Float(_) | String(_) | ListLit(_) + | TupLabel(_) | Tuple(_) | Var(_) | Let(_) @@ -610,7 +631,9 @@ module UExp = { || ( switch (e.term) { | Parens(e) => is_tuple_of_functions(e) - | Tuple(es) => es |> List.for_all(is_fun) + | Tuple(es) => + let es = es |> List.map(((_, e)) => e); + es |> List.for_all(is_fun); | Invalid(_) | EmptyHole | MultiHole(_) @@ -634,6 +657,7 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) + | TupLabel(_) | Constructor(_) => false } ); diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index a6297a3061..8fa7771744 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -110,7 +110,8 @@ and UExp: { | ListLit(list(t)) | Constructor(string) | Fun(UPat.t, t) - | Tuple(list(t)) + | TupLabel(UPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Var(Var.t) | Let(UPat.t, t, t) | TyAlias(UTPat.t, UTyp.t, t) @@ -207,7 +208,8 @@ and UExp: { | ListLit(list(t)) | Constructor(string) | Fun(UPat.t, t) - | Tuple(list(t)) + | TupLabel(UPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Var(Var.t) | Let(UPat.t, t, t) | TyAlias(UTPat.t, UTyp.t, t) @@ -290,7 +292,8 @@ and UPat: { | Constructor(string) | Cons(t, t) | Var(Var.t) - | Tuple(list(t)) + | TupLabel(t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Parens(t) | Ap(t, t) | TypeAnn(t, UTyp.t) @@ -314,7 +317,8 @@ and UPat: { | Constructor(string) | Cons(t, t) | Var(Var.t) - | Tuple(list(t)) + | TupLabel(t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Parens(t) | Ap(t, t) | TypeAnn(t, UTyp.t) @@ -337,7 +341,8 @@ and UTyp: { | Var(string) | Constructor(string) | Arrow(t, t) - | Tuple(list(t)) + | TupLabel(UPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Parens(t) | Ap(t, t) | Sum(list(variant)) @@ -362,7 +367,8 @@ and UTyp: { | Var(string) | Constructor(string) | Arrow(t, t) - | Tuple(list(t)) + | TupLabel(UPat.t, t) + | Tuple(list((option(LabeledTuple.t), t))) | Parens(t) | Ap(t, t) | Sum(list(variant)) diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 3f614145ab..8ec9fa66d6 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -31,7 +31,7 @@ module rec Typ: { | List(t) | Arrow(t, t) | Sum(sum_map) - | Prod(list(t)) + | Prod(list((option(LabeledTuple.t), t))) | Rec(TypVar.t, t) and sum_map = ConstructorMap.t(option(t)); @@ -52,7 +52,8 @@ module rec Typ: { let join_type_provenance: (type_provenance, type_provenance) => type_provenance; let matched_arrow: (Ctx.t, t) => (t, t); - let matched_prod: (Ctx.t, int, t) => list(t); + let matched_prod: + (Ctx.t, list((option(LabeledTuple.t), 'a)), t) => list(t); let matched_list: (Ctx.t, t) => t; let precedence: t => int; let subst: (t, TypVar.t, t) => t; @@ -88,7 +89,7 @@ module rec Typ: { | List(t) | Arrow(t, t) | Sum(sum_map) - | Prod(list(t)) + | Prod(list((option(LabeledTuple.t), t))) | Rec(TypVar.t, t) and sum_map = ConstructorMap.t(option(t)); @@ -144,7 +145,7 @@ module rec Typ: { | String => String | Unknown(prov) => Unknown(prov) | Arrow(ty1, ty2) => Arrow(subst(s, x, ty1), subst(s, x, ty2)) - | Prod(tys) => Prod(List.map(subst(s, x), tys)) + | Prod(tys) => Prod(tys |> List.map(((p, e)) => (p, subst(s, x, e)))) | Sum(sm) => Sum(ConstructorMap.map(Option.map(subst(s, x)), sm)) | Rec(y, ty) when TypVar.eq(x, y) => Rec(y, ty) | Rec(y, ty) => Rec(y, subst(s, x, ty)) @@ -177,7 +178,17 @@ module rec Typ: { | (Unknown(_), _) => false | (Arrow(t1, t2), Arrow(t1', t2')) => eq(t1, t1') && eq(t2, t2') | (Arrow(_), _) => false - | (Prod(tys1), Prod(tys2)) => List.equal(eq, tys1, tys2) + | (Prod(tys1), Prod(tys2)) => + List.equal( + ((p1, t1), (p2, t2)) => + switch (p1, p2) { + | (Some(ap), Some(bp)) => compare(ap, bp) == 0 && eq(t1, t2) + | (None, None) => eq(t1, t2) + | (_, _) => false + }, + tys1, + tys2, + ) | (Prod(_), _) => false | (List(t1), List(t2)) => eq(t1, t2) | (List(_), _) => false @@ -206,7 +217,8 @@ module rec Typ: { | Some(typ) => free_vars(~bound, typ), List.map(snd, sm), ) - | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) + | Prod(tys) => + ListUtil.flat_map(free_vars(~bound), tys |> List.map(((_, b)) => b)) | Rec(x, ty) => free_vars(~bound=[x, ...bound], ty) }; @@ -270,9 +282,25 @@ module rec Typ: { Arrow(ty1, ty2); | (Arrow(_), _) => None | (Prod(tys1), Prod(tys2)) => - let* tys = ListUtil.map2_opt(join', tys1, tys2); + let (tysp, _) = List.split(tys1); + let* tys = + ListUtil.map2_opt( + ((p1, t1), (p2, t2)) => + switch (p1, p2) { + | (Some(ap), Some(bp)) => + if (compare(ap, bp) == 0) { + join'(t1, t2); + } else { + None; + } + | (None, None) => join'(t1, t2) + | (_, _) => None + }, + tys1, + tys2, + ); let+ tys = OptUtil.sequence(tys); - Prod(tys); + Prod(List.combine(tysp, tys)); //TODO: Fix this | (Prod(_), _) => None | (Sum(sm1), Sum(sm2)) => let (sorted1, sorted2) = @@ -348,7 +376,7 @@ module rec Typ: { | String => ty | List(t) => List(normalize(ctx, t)) | Arrow(t1, t2) => Arrow(normalize(ctx, t1), normalize(ctx, t2)) - | Prod(ts) => Prod(List.map(normalize(ctx), ts)) + | Prod(ts) => Prod(ts |> List.map(((p, e)) => (p, normalize(ctx, e)))) | Sum(ts) => Sum(ConstructorMap.map(Option.map(normalize(ctx)), ts)) | Rec(name, ty) => /* NOTE: Dummy tvar added has fake id but shouldn't matter @@ -365,11 +393,36 @@ module rec Typ: { | _ => (Unknown(Internal), Unknown(Internal)) }; - let matched_prod = (ctx, length, ty) => - switch (weak_head_normalize(ctx, ty)) { - | Prod(tys) when List.length(tys) == length => tys - | Unknown(SynSwitch) => List.init(length, _ => Unknown(SynSwitch)) - | _ => List.init(length, _ => Unknown(Internal)) + let matched_prod: + (Ctx.t, list((option(LabeledTuple.t), 'a)), t) => list(t) = + (ctx, es, ty) => { + switch (weak_head_normalize(ctx, ty)) { + | Prod(tys) + when + List.length(tys) == List.length(es) + && List.fold_right( + ((ty, e), b) => { + b + ? switch (ty, e) { + | (Some(tstr), Some(estr)) => tstr == estr + | (None, None) => true + | (_, _) => false + } + : { + false; + } + }, + List.combine( + tys |> List.map(((a, _)) => a), + es |> List.map(((a, _)) => a), + ), + true, + ) => + tys |> List.map(((_, b)) => b) + | Unknown(SynSwitch) => + List.init(List.length(es), _ => Unknown(SynSwitch)) + | _ => List.init(List.length(es), _ => Unknown(Internal)) + }; }; let matched_list = (ctx, ty) => diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index 1a62565b35..59899c6dca 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -65,6 +65,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => { | ListLit(_) | Constructor(_) | Fun(_) + | TupLabel(_) | Tuple(_) | Var(_) | Ap(_) diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re index 52eba25966..3fd5a6fb90 100644 --- a/src/haz3lschool/SyntaxTest.re +++ b/src/haz3lschool/SyntaxTest.re @@ -11,9 +11,11 @@ let rec find_var_upat = (name: string, upat: Term.UPat.t): bool => { switch (upat.term) { | Var(x) => x == name | Cons(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2) - | ListLit(l) - | Tuple(l) => + | ListLit(l) => List.fold_left((acc, up) => {acc || find_var_upat(name, up)}, false, l) + | Tuple(l) => + let (_, l) = List.split(l); + List.fold_left((acc, up) => {acc || find_var_upat(name, up)}, false, l); | Parens(up) => find_var_upat(name, up) | Ap(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2) | TypeAnn(up, _) => find_var_upat(name, up) @@ -26,9 +28,11 @@ let rec var_mention = (name: string, uexp: Term.UExp.t): bool => { | Var(x) => x == name | Fun(args, body) => find_var_upat(name, args) ? false : var_mention(name, body) - | ListLit(l) - | Tuple(l) => + | ListLit(l) => List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l) + | Tuple(l) => + let (_, l) = List.split(l); + List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l); | Let(p, def, body) => find_var_upat(name, p) ? false : var_mention(name, def) || var_mention(name, body) @@ -61,9 +65,11 @@ let rec var_applied = (name: string, uexp: Term.UExp.t): bool => { switch (uexp.term) { | Fun(args, body) => find_var_upat(name, args) ? false : var_applied(name, body) - | ListLit(l) - | Tuple(l) => + | ListLit(l) => List.fold_left((acc, ue) => {acc || var_applied(name, ue)}, false, l) + | Tuple(l) => + let (_, l) = List.split(l); + List.fold_left((acc, ue) => {acc || var_applied(name, ue)}, false, l); | Let(p, def, body) => find_var_upat(name, p) ? false : var_applied(name, def) || var_applied(name, body) @@ -117,6 +123,8 @@ let rec find_in_let = l; } | (Tuple(pl), Tuple(ul)) => + let (_, pl) = List.split(pl); + let (_, ul) = List.split(ul); if (List.length(pl) != List.length(ul)) { l; } else { @@ -126,7 +134,7 @@ let rec find_in_let = pl, ul, ); - } + }; | _ => l }; }; @@ -137,9 +145,11 @@ let rec find_fn = switch (uexp.term) { | Let(up, def, body) => l |> find_in_let(name, up, def) |> find_fn(name, body) - | ListLit(ul) - | Tuple(ul) => + | ListLit(ul) => List.fold_left((acc, u1) => {find_fn(name, u1, acc)}, l, ul) + | Tuple(ul) => + let (_, ul) = List.split(ul); + List.fold_left((acc, u1) => {find_fn(name, u1, acc)}, l, ul); | Fun(_, body) => l |> find_fn(name, body) | Parens(u1) | UnOp(_, u1) @@ -181,10 +191,12 @@ let rec tail_check = (name: string, uexp: Term.UExp.t): bool => { | Let(p, def, body) => find_var_upat(name, p) || var_mention(name, def) ? false : tail_check(name, body) - | ListLit(l) + | ListLit(l) => + !List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l) | Tuple(l) => //If l has no recursive calls then true - !List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l) + let (_, l) = List.split(l); + !List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l); | Test(_) => false | TyAlias(_, _, u) | Parens(u) => tail_check(name, u) diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index 3e663ea093..f32ccdeb88 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -1020,7 +1020,37 @@ let get_doc = } else { basic(doc, LangDocMessages.function_var_group, options); }; + | TupLabel(_) => + // TODO: Fix this + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.function_triv_group, + docs, + ); + if (LangDocMessages.function_triv_exp.id == doc.id) { + let pat_id = List.nth(pat.ids, 0); + let body_id = List.nth(body.ids, 0); + get_message( + doc, + options, + LangDocMessages.function_triv_group, + Printf.sprintf( + Scanf.format_from_string(doc.explanation.message, "%s%s%s"), + pat_id |> Id.to_string, + pat_id |> Id.to_string, + body_id |> Id.to_string, + ), + LangDocMessages.function_triv_exp_coloring_ids( + ~pat_id, + ~body_id, + ), + ); + } else { + basic(doc, LangDocMessages.function_triv_group, options); + }; | Tuple(elements) => + // TODO: Fix this + let elements = elements |> List.map(((_, e)) => e); let pat_id = List.nth(pat.ids, 0); let body_id = List.nth(body.ids, 0); let basic_tuple = (doc: LangDocMessages.form, group_id, options) => { @@ -1190,7 +1220,9 @@ let get_doc = | Parens(_) => default // Shouldn't get hit? | TypeAnn(_) => default // Shouldn't get hit? }; + | TupLabel(_) => basic_info(LangDocMessages.empty_hole_exp_group) | Tuple(terms) => + let terms = terms |> List.map(((_, e)) => e); let basic = (doc, group_id, options) => get_message( doc, @@ -1688,7 +1720,44 @@ let get_doc = } else { basic(doc, LangDocMessages.let_var_exp_group, options); }; + | TupLabel(_) => + // TODO: Fix this + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.let_triv_exp_group, + docs, + ); + if (LangDocMessages.let_triv_exp.id == doc.id) { + let pat_id = List.nth(pat.ids, 0); + let def_id = List.nth(def.ids, 0); + let body_id = List.nth(body.ids, 0); + get_message( + doc, + options, + LangDocMessages.let_triv_exp_group, + Printf.sprintf( + Scanf.format_from_string(doc.explanation.message, "%s%s%s%s"), + def_id |> Id.to_string, + pat_id |> Id.to_string, + def_id |> Id.to_string, + body_id |> Id.to_string, + ), + LangDocMessages.let_triv_exp_coloring_ids( + ~pat_id, + ~def_id, + ~body_id, + ), + ); + } else { + /* TODO The coloring for the syntactic form is sometimes wrong here and other places when switching syntactic specificities... seems like might be Safari issue... */ + basic( + doc, + LangDocMessages.let_triv_exp_group, + options, + ); + }; | Tuple(elements) => + let elements = elements |> List.map(((_, e)) => e); let pat_id = List.nth(pat.ids, 0); let def_id = List.nth(def.ids, 0); let basic_tuple = (doc: LangDocMessages.form, group_id, options) => { @@ -2438,7 +2507,21 @@ let get_doc = ), [], ); + | TupLabel(_) => + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.triv_pat_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.triv_pat_group, + doc.explanation.message, + [], + ); | Tuple(elements) => + let elements = elements |> List.map(((_, e)) => e); let basic = (doc, group, options) => get_message( doc, @@ -2722,7 +2805,21 @@ let get_doc = ); basic(doc, LangDocMessages.arrow_typ_group, options); }; + | TupLabel(_) => + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.bool_typ_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.bool_typ_group, + doc.explanation.message, + [], + ); | Tuple(elements) => + let elements = elements |> List.map(((_, e)) => e); let basic = (doc, group, options) => get_message( doc, diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index ae88419f0e..20d2ad2bb6 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -53,6 +53,8 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => | Prod([_]) => div(~attr=clss(["typ-view", "Prod"]), [text("Singleton Product")]) | Prod([t0, ...ts]) => + let (_, t0) = t0; + let ts = ts |> List.map(((_, t)) => t); div( ~attr=clss(["typ-view", "atom", "Prod"]), [ @@ -64,7 +66,7 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => ), text(")"), ], - ) + ); | Sum(ts) => div( ~attr=clss(["typ-view", "Sum"]), diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 2dc53757b5..7998e189a5 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -75,6 +75,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => { | ApBuiltin(_) => DHDoc_common.precedence_Ap | Cons(_) => DHDoc_common.precedence_Cons | ListConcat(_) => DHDoc_common.precedence_Plus + | TupLabel(_) => DHDoc_common.precedence_Comma | Tuple(_) => DHDoc_common.precedence_Comma | NonEmptyHole(_, _, _, d) => precedence'(d) @@ -233,9 +234,10 @@ let rec mk = let (doc1, doc2) = mk_right_associative_operands(precedence_bin_bool_op(op), d1, d2); hseps([mk_cast(doc1), mk_bin_bool_op(op), mk_cast(doc2)]); + | TupLabel(_, e) => fdoc(~enforce_inline, ~d=e) | Tuple([]) => DHDoc_common.Delim.triv | Tuple(ds) => - DHDoc_common.mk_Tuple(ds |> List.map(d => mk_cast(go'(d)))) + DHDoc_common.mk_Tuple(ds |> List.map(((_, d)) => mk_cast(go'(d)))) | Prj(d, n) => DHDoc_common.mk_Prj(mk_cast(go'(d)), n) | ConsistentCase(Case(dscrut, drs, _)) => go_case(dscrut, drs) | Cast(d, _, _) => diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re index c27aa21b07..415dff64df 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re @@ -56,7 +56,8 @@ let rec mk = mk_right_associative_operands(DHDoc_common.precedence_Cons, dp1, dp2); DHDoc_common.mk_Cons(doc1, doc2); | Tuple([]) => DHDoc_common.Delim.triv - | Tuple(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds)) + | Tuple(ds) => + DHDoc_common.mk_Tuple(List.map(mk', ds |> List.map(((_, d)) => d))) | Ap(dp1, dp2) => let (doc1, doc2) = mk_left_associative_operands(DHDoc_common.precedence_Ap, dp1, dp2); diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 8acbc0455f..486e2ba132 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -79,6 +79,8 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { ); | Prod([]) => (text("()"), parenthesize) | Prod([head, ...tail]) => + let (_, head) = head; + let tail = tail |> List.map(((_, e)) => e); let center = [ annot( From a7775adbfe2ad40a7fe1fc22aa9bb1dd15ea9757 Mon Sep 17 00:00:00 2001 From: WondAli Date: Wed, 6 Dec 2023 14:58:30 -0500 Subject: [PATCH 2/6] some maketerm cleanup --- src/haz3lcore/statics/MakeTerm.re | 136 ++++++++++++++++++++---------- 1 file changed, 92 insertions(+), 44 deletions(-) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 5be0d212b7..6bc6c8bb5f 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -52,70 +52,118 @@ let is_typ_bsum = is_nary(TermBase.Any.is_typ, "+"); // Tuplabel util functions // TODO: filter patternss so that result (option(Var.t), UExp.t) -let return_tuplabel = (p: UPat.t, t: 'a): (option(LabeledTuple.t), 'a) => - switch (p.term) { - | Var(s) => (Some(s), t) - | _ => raise(EvaluatorError.Exception(BadBuiltinAp("", []))) // TOOD: put the real error - }; - -let return_tuplabel_exp = - (p: UPat.t, t: UExp.t): (option(LabeledTuple.t), UExp.t) => - switch (p.term) { - | Var(s) => (Some(s), t) - | _ => - let t: UExp.t = {ids: t.ids, term: Invalid("")}; - (None, t); - }; - -let return_tuplabel_pat = - (p: UPat.t, t: UPat.t): (option(LabeledTuple.t), UPat.t) => - switch (p.term) { - | Var(s) => (Some(s), t) - | _ => - let t: UPat.t = {ids: t.ids, term: Invalid("")}; - (None, t); - }; - -let return_tuplabel_typ = - (p: UPat.t, t: UTyp.t): (option(LabeledTuple.t), UTyp.t) => - switch (p.term) { - | Var(s) => (Some(s), t) - | _ => - let t: UTyp.t = {ids: t.ids, term: Invalid("")}; - (None, t); - }; +// let return_tuplabel = (p: UPat.t, t: 'a): (option(LabeledTuple.t), 'a) => +// switch (p.term) { +// | Var(s) => (Some(s), t) +// | _ => raise(EvaluatorError.Exception(BadBuiltinAp("", []))) // TOOD: put the real error +// }; let make_labeled_tuple_exp_helper = - (exp: UExp.t): (option(LabeledTuple.t), UExp.t) => + (exp: UExp.t, result: list((option(LabeledTuple.t), UExp.t))) + : (option(LabeledTuple.t), UExp.t) => switch (exp.term) { - | TupLabel(p, e) => return_tuplabel_exp(p, e) + | TupLabel(p, e) => + switch (p.term) { + | Var(s) + when + List.fold_left( + (b, opt) => + switch (opt) { + | (Some(st), _) when b => compare(st, s) != 0 + | _ => b + }, + true, + result, + ) => ( + Some(s), + e, + ) + | _ => + let t: UExp.t = {ids: e.ids, term: Invalid("")}; + (None, t); + } | _ => (None, exp) }; -let make_labeled_tuple_exp = (es: list(UExp.t)) => { - es |> List.map(make_labeled_tuple_exp_helper); +let make_labeled_tuple_exp = + (es: list(UExp.t)): list((option(LabeledTuple.t), UExp.t)) => { + es + |> List.fold_left( + (result, e) => {result @ [make_labeled_tuple_exp_helper(e, result)]}, + [], + ); }; let make_labeled_tuple_pat_helper = - (pat: UPat.t): (option(LabeledTuple.t), UPat.t) => + (pat: UPat.t, result: list((option(LabeledTuple.t), UPat.t))) + : (option(LabeledTuple.t), UPat.t) => switch (pat.term) { - | TupLabel(p, pt) => return_tuplabel_pat(p, pt) + | TupLabel(p, pt) => + switch (p.term) { + | Var(s) + when + List.fold_left( + (b, opt) => + switch (opt) { + | (Some(st), _) when b => compare(st, s) != 0 + | _ => b + }, + true, + result, + ) => ( + Some(s), + pt, + ) + | _ => + let t: UPat.t = {ids: pt.ids, term: Invalid("")}; + (None, t); + } | _ => (None, pat) }; -let make_labeled_tuple_pat = (ps: list(UPat.t)) => { - ps |> List.map(make_labeled_tuple_pat_helper); +let make_labeled_tuple_pat = + (ps: list(UPat.t)): list((option(LabeledTuple.t), UPat.t)) => { + ps + |> List.fold_left( + (result, p) => {result @ [make_labeled_tuple_pat_helper(p, result)]}, + [], + ); }; let make_labeled_tuple_typ_helper = - (typ: UTyp.t): (option(LabeledTuple.t), UTyp.t) => + (typ: UTyp.t, result: list((option(LabeledTuple.t), UTyp.t))) + : (option(LabeledTuple.t), UTyp.t) => switch (typ.term) { - | TupLabel(p, t) => return_tuplabel_typ(p, t) + | TupLabel(p, t) => + switch (p.term) { + | Var(s) + when + List.fold_left( + (b, opt) => + switch (opt) { + | (Some(st), _) when b => compare(st, s) != 0 + | _ => b + }, + true, + result, + ) => ( + Some(s), + t, + ) + | _ => + let t: UTyp.t = {ids: t.ids, term: Invalid("")}; + (None, t); + } | _ => (None, typ) }; -let make_labeled_tuple_typ = (ts: list('a)) => { - ts |> List.map(make_labeled_tuple_typ_helper); +let make_labeled_tuple_typ = + (ts: list(UTyp.t)): list((option(LabeledTuple.t), UTyp.t)) => { + ts + |> List.fold_left( + (result, t) => {result @ [make_labeled_tuple_typ_helper(t, result)]}, + [], + ); }; let is_grout = tiles => From 508b369e78c877a7e1824b8965483b47b96b9c4c Mon Sep 17 00:00:00 2001 From: WondAli Date: Mon, 18 Dec 2023 18:56:25 -0500 Subject: [PATCH 3/6] committing progress before refactor --- src/haz3lcore/LabeledTuple.re | 80 ++++++++++++++++++ src/haz3lcore/dynamics/DH.re | 2 +- src/haz3lcore/dynamics/Evaluator.re | 124 ++++++++++++++++++++++------ src/haz3lcore/statics/MakeTerm.re | 6 +- src/haz3lcore/statics/TypBase.re | 102 ++++++++++++++++++----- 5 files changed, 263 insertions(+), 51 deletions(-) diff --git a/src/haz3lcore/LabeledTuple.re b/src/haz3lcore/LabeledTuple.re index bf1e6fb963..2cf760f8ac 100644 --- a/src/haz3lcore/LabeledTuple.re +++ b/src/haz3lcore/LabeledTuple.re @@ -10,3 +10,83 @@ let length = String.length; let valid_regex = Re.Str.regexp("^\\([a-zA-Z]\\|_[_a-zA-Z0-9]\\)[_a-zA-Z0-9']*$"); let is_valid = s => Re.Str.string_match(valid_regex, s, 0); + +let compare = String.compare; + +let find_opt: ('a => bool, list('a)) => option('a) = List.find_opt; + +// Rename and clean this +// Assumes all labels are unique +// In order of operations: +// Checks all labeled pairs in l2 are in l1 and performs f on each pair +// Checks all labeled pairs in l1 are in l2 and performs f on each pair +// Checks remaining None pairs in order and performs f on each pair +let ana_tuple: + ( + ('a, 'c, 'c) => 'a, + 'a, + 'a, + list((option('b), 'c)), + list((option('b), 'c)) + ) => + 'a = + (f, accu, accu_fail, l1, l2) => { + let l1_lab = List.filter(((p, _)) => p != None, l1); + let l1_none = List.filter(((p, _)) => p == None, l1); + let l2_lab = List.filter(((p, _)) => p != None, l2); + let l2_none = List.filter(((p, _)) => p == None, l2); + let accu = + List.fold_left( + (accu, l2_item) => { + let l1_item = + List.find_opt( + l1_item => { + switch (l1_item, l2_item) { + | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + l1_lab, + ); + switch (l1_item, l2_item) { + | (Some((_, l1_val)), (_, l2_val)) => f(accu, l1_val, l2_val) + | (None, _) => accu_fail + }; + }, + accu, + l2_lab, + ); + // TODO: Currently duplicating checks + let accu = + List.fold_left( + (accu, l1_item) => { + let l2_item = + List.find_opt( + l2_item => { + switch (l1_item, l2_item) { + | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + l2_lab, + ); + switch (l1_item, l2_item) { + | ((_, l1_val), Some((_, l2_val))) => f(accu, l1_val, l2_val) + | (_, None) => accu_fail + }; + }, + accu, + l1_lab, + ); + // None checks + let accu = + List.fold_left2( + (accu, (_, l1_val), (_, l2_val)) => f(accu, l1_val, l2_val), + accu, + l1_none, + l2_none, + ); + accu; + }; diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re index 874b64c4ec..16fbe2a7f6 100644 --- a/src/haz3lcore/dynamics/DH.re +++ b/src/haz3lcore/dynamics/DH.re @@ -232,7 +232,7 @@ module rec DHExp: { ((ap, ad), (bp, bd)) => switch (ap, bp) { | (Some(ap), Some(bp)) => - compare(ap, bp) == 0 && fast_equal(ad, bd) + LabeledTuple.compare(ap, bp) == 0 && fast_equal(ad, bd) | (None, None) => fast_equal(ad, bd) | (_, _) => false }, diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 4d53fa0209..a046b06016 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -204,38 +204,112 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => if (List.length(dps) != List.length(ds)) { DoesNotMatch; } else { + // List.fold_left2( + // (result, (pp, dp), (p, d)) => + // switch (result) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env) => + // // TODO: Need a function to reorganize lists to match up vars + // // TODO: check if this logic is right + // switch (pp, p) { + // | (Some(sp), Some(s)) => + // if (LabeledTuple.compare(sp, s) == 0) { + // switch (matches(dp, d)) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env') => Matches(Environment.union(env, env')) + // }; + // } else { + // DoesNotMatch; + // } + // | (None, None) => + // switch (matches(dp, d)) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env') => Matches(Environment.union(env, env')) + // } + // | (_, _) => DoesNotMatch + // } + // }, + // Matches(Environment.empty), + // dps, + // ds, + // ); + // Check labels + // let f = (result, dp, d) => { + // switch (result) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env) => + // switch (matches(dp, d)) { + // | DoesNotMatch => DoesNotMatch + // | IndetMatch => IndetMatch + // | Matches(env') => Matches(Environment.union(env, env')) + // } + // } + // } + let (_, result) = + List.fold_left( + ((dps, result), (p, d)) => + switch (result) { + | DoesNotMatch => (dps, DoesNotMatch) + | IndetMatch => (dps, IndetMatch) + | Matches(env) => + // TODO: Need a function to reorganize lists to match up vars + // TODO: check if this logic is right + switch (p) { + | None => (dps, result) + | _ => + let dp_opt = + List.find_opt( + dp => { + switch (dp, (p, d)) { + | ((Some(sp), _), (Some(s), _)) => + LabeledTuple.compare(sp, s) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + dps, + ); + switch (dp_opt) { + | Some((_, dp)) => + switch (matches(dp, d)) { + | DoesNotMatch => (dps, DoesNotMatch) + | IndetMatch => (dps, IndetMatch) + | Matches(env') => ( + dps, + Matches(Environment.union(env, env')), + ) + } + | None => (dps, DoesNotMatch) + }; + } + }, + (dps, Matches(Environment.empty)), + ds, + ); + // Now check Nones + let dps_nones = List.filter(((p, _)) => p == None, dps); + let ds_nones = List.filter(((p, _)) => p == None, ds); List.fold_left2( - (result, (pp, dp), (p, d)) => + (result, (_, dp), (_, d)) => switch (result) { | DoesNotMatch => DoesNotMatch | IndetMatch => IndetMatch | Matches(env) => - // TODO: Need a function to reorganize lists to match up vars - // TODO: check if this logic is right - switch (pp, p) { - | (Some(sp), Some(s)) => - if (compare(sp, s) == 0) { - switch (matches(dp, d)) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) - }; - } else { - DoesNotMatch; - } - | (None, None) => - switch (matches(dp, d)) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) - } - | (_, _) => DoesNotMatch + switch (matches(dp, d)) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env') => Matches(Environment.union(env, env')) } }, - Matches(Environment.empty), - dps, - ds, + result, + dps_nones, + ds_nones, ); + //LabeledTuple.ana_tuple(f, Matches(Environment.empty), DoesNotMatch, dps, ds) } | (Tuple(dps), Cast(d, Prod(tys), Prod(tys'))) => assert(List.length(tys) == List.length(tys')); @@ -391,7 +465,7 @@ and matches_cast_Tuple = | Matches(env) => switch (pp, p) { | (Some(sp), Some(s)) => - if (compare(sp, s) == 0) { + if (LabeledTuple.compare(sp, s) == 0) { switch (matches(dp, DHExp.apply_casts(d, casts))) { | DoesNotMatch => DoesNotMatch | IndetMatch => IndetMatch diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 6bc6c8bb5f..464cd3e218 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -69,7 +69,7 @@ let make_labeled_tuple_exp_helper = List.fold_left( (b, opt) => switch (opt) { - | (Some(st), _) when b => compare(st, s) != 0 + | (Some(st), _) when b => LabeledTuple.compare(st, s) != 0 | _ => b }, true, @@ -105,7 +105,7 @@ let make_labeled_tuple_pat_helper = List.fold_left( (b, opt) => switch (opt) { - | (Some(st), _) when b => compare(st, s) != 0 + | (Some(st), _) when b => LabeledTuple.compare(st, s) != 0 | _ => b }, true, @@ -141,7 +141,7 @@ let make_labeled_tuple_typ_helper = List.fold_left( (b, opt) => switch (opt) { - | (Some(st), _) when b => compare(st, s) != 0 + | (Some(st), _) when b => LabeledTuple.compare(st, s) != 0 | _ => b }, true, diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 8ec9fa66d6..212a0e9c9c 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -179,16 +179,64 @@ module rec Typ: { | (Arrow(t1, t2), Arrow(t1', t2')) => eq(t1, t1') && eq(t2, t2') | (Arrow(_), _) => false | (Prod(tys1), Prod(tys2)) => - List.equal( - ((p1, t1), (p2, t2)) => - switch (p1, p2) { - | (Some(ap), Some(bp)) => compare(ap, bp) == 0 && eq(t1, t2) - | (None, None) => eq(t1, t2) - | (_, _) => false - }, - tys1, - tys2, - ) + // List.equal( + // ((p1, t1), (p2, t2)) => + // switch (p1, p2) { + // | (Some(ap), Some(bp)) => + // LabeledTuple.compare(ap, bp) == 0 && eq(t1, t2) + // | (None, None) => eq(t1, t2) + // | (_, _) => false + // }, + // tys1, + // tys2, + // ) + let (_, b) = + List.fold_left( + ((tys1, b), ty2) => + if (b) { + switch (ty2) { + | (None, _) => (tys1, b) + | _ => + let ty1_opt = + List.find_opt( + ty1 => { + switch (ty1, ty2) { + | ((Some(s1), _), (Some(s2), _)) => + LabeledTuple.compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + tys1, + ); + switch (ty1_opt, ty2) { + | (Some((_, t1)), (_, t2)) => (tys1, eq(t1, t2)) + | (None, _) => (tys1, false) + }; + }; + } else { + (tys1, false); + }, + (tys1, true), + tys2, + ); + if (b) { + // check Nones + let tys1_nones = List.filter(((p, _)) => p == None, tys1); + let tys2_nones = List.filter(((p, _)) => p == None, tys2); + List.fold_left2( + (b, (_, t1), (_, t2)) => + switch (b) { + | false => false + | true => eq(t1, t2) + }, + b, + tys1_nones, + tys2_nones, + ); + } else { + b; + }; | (Prod(_), _) => false | (List(t1), List(t2)) => eq(t1, t2) | (List(_), _) => false @@ -288,7 +336,7 @@ module rec Typ: { ((p1, t1), (p2, t2)) => switch (p1, p2) { | (Some(ap), Some(bp)) => - if (compare(ap, bp) == 0) { + if (LabeledTuple.compare(ap, bp) == 0) { join'(t1, t2); } else { None; @@ -401,24 +449,34 @@ module rec Typ: { when List.length(tys) == List.length(es) && List.fold_right( - ((ty, e), b) => { + (ty, b) => { b - ? switch (ty, e) { - | (Some(tstr), Some(estr)) => tstr == estr - | (None, None) => true - | (_, _) => false - } + ? { + let e_opt = + List.find_opt( + e => { + switch (e, ty) { + | ((Some(sp), _), (Some(s), _)) => + LabeledTuple.compare(sp, s) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + es, + ); + switch (e_opt) { + | None => false + | _ => true + }; + } : { false; } }, - List.combine( - tys |> List.map(((a, _)) => a), - es |> List.map(((a, _)) => a), - ), + tys, true, ) => - tys |> List.map(((_, b)) => b) + tys |> List.map(((_, ty)) => ty) | Unknown(SynSwitch) => List.init(List.length(es), _ => Unknown(SynSwitch)) | _ => List.init(List.length(es), _ => Unknown(Internal)) From f8e643c85c9d40161b491f86ebec92fa0ec3a322 Mon Sep 17 00:00:00 2001 From: WondAli Date: Mon, 18 Dec 2023 19:19:59 -0500 Subject: [PATCH 4/6] saving commit before merging with dev evaluator rewrite --- src/haz3lcore/LabeledTuple.re | 4 +- src/haz3lcore/dynamics/DH.re | 19 ++--- src/haz3lcore/dynamics/Evaluator.re | 119 ++++------------------------ src/haz3lcore/statics/TypBase.re | 93 ++-------------------- 4 files changed, 34 insertions(+), 201 deletions(-) diff --git a/src/haz3lcore/LabeledTuple.re b/src/haz3lcore/LabeledTuple.re index 2cf760f8ac..80c4ec171b 100644 --- a/src/haz3lcore/LabeledTuple.re +++ b/src/haz3lcore/LabeledTuple.re @@ -23,11 +23,11 @@ let find_opt: ('a => bool, list('a)) => option('a) = List.find_opt; // Checks remaining None pairs in order and performs f on each pair let ana_tuple: ( - ('a, 'c, 'c) => 'a, + ('a, 'c, 'd) => 'a, 'a, 'a, list((option('b), 'c)), - list((option('b), 'c)) + list((option('b), 'd)) ) => 'a = (f, accu, accu_fail, l1, l2) => { diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re index 16fbe2a7f6..657c7576c2 100644 --- a/src/haz3lcore/dynamics/DH.re +++ b/src/haz3lcore/dynamics/DH.re @@ -227,18 +227,15 @@ module rec DHExp: { fast_equal(d11, d12) && fast_equal(d21, d22) | (TupLabel(_, e1), TupLabel(_, e2)) => fast_equal(e1, e2) // TODO: Not right? | (Tuple(ds1), Tuple(ds2)) => + // is the full comparison necessary for fast_equal? + let f = (b, ds1_val, ds2_val) => { + switch (b) { + | false => false + | true => fast_equal(ds1_val, ds2_val) + }; + }; List.length(ds1) == List.length(ds2) - && List.for_all2( - ((ap, ad), (bp, bd)) => - switch (ap, bp) { - | (Some(ap), Some(bp)) => - LabeledTuple.compare(ap, bp) == 0 && fast_equal(ad, bd) - | (None, None) => fast_equal(ad, bd) - | (_, _) => false - }, - ds1, - ds2, - ) + && LabeledTuple.ana_tuple(f, true, false, ds1, ds2); | (Prj(d1, n), Prj(d2, m)) => n == m && fast_equal(d1, d2) | (ApBuiltin(f1, args1), ApBuiltin(f2, args2)) => f1 == f2 && List.for_all2(fast_equal, args1, args2) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index a046b06016..a8000f1fb8 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -204,112 +204,25 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => if (List.length(dps) != List.length(ds)) { DoesNotMatch; } else { - // List.fold_left2( - // (result, (pp, dp), (p, d)) => - // switch (result) { - // | DoesNotMatch => DoesNotMatch - // | IndetMatch => IndetMatch - // | Matches(env) => - // // TODO: Need a function to reorganize lists to match up vars - // // TODO: check if this logic is right - // switch (pp, p) { - // | (Some(sp), Some(s)) => - // if (LabeledTuple.compare(sp, s) == 0) { - // switch (matches(dp, d)) { - // | DoesNotMatch => DoesNotMatch - // | IndetMatch => IndetMatch - // | Matches(env') => Matches(Environment.union(env, env')) - // }; - // } else { - // DoesNotMatch; - // } - // | (None, None) => - // switch (matches(dp, d)) { - // | DoesNotMatch => DoesNotMatch - // | IndetMatch => IndetMatch - // | Matches(env') => Matches(Environment.union(env, env')) - // } - // | (_, _) => DoesNotMatch - // } - // }, - // Matches(Environment.empty), - // dps, - // ds, - // ); - // Check labels - // let f = (result, dp, d) => { - // switch (result) { - // | DoesNotMatch => DoesNotMatch - // | IndetMatch => IndetMatch - // | Matches(env) => - // switch (matches(dp, d)) { - // | DoesNotMatch => DoesNotMatch - // | IndetMatch => IndetMatch - // | Matches(env') => Matches(Environment.union(env, env')) - // } - // } - // } - let (_, result) = - List.fold_left( - ((dps, result), (p, d)) => - switch (result) { - | DoesNotMatch => (dps, DoesNotMatch) - | IndetMatch => (dps, IndetMatch) - | Matches(env) => - // TODO: Need a function to reorganize lists to match up vars - // TODO: check if this logic is right - switch (p) { - | None => (dps, result) - | _ => - let dp_opt = - List.find_opt( - dp => { - switch (dp, (p, d)) { - | ((Some(sp), _), (Some(s), _)) => - LabeledTuple.compare(sp, s) == 0 - | ((None, _), (None, _)) => true - | (_, _) => false - } - }, - dps, - ); - switch (dp_opt) { - | Some((_, dp)) => - switch (matches(dp, d)) { - | DoesNotMatch => (dps, DoesNotMatch) - | IndetMatch => (dps, IndetMatch) - | Matches(env') => ( - dps, - Matches(Environment.union(env, env')), - ) - } - | None => (dps, DoesNotMatch) - }; - } - }, - (dps, Matches(Environment.empty)), - ds, - ); - // Now check Nones - let dps_nones = List.filter(((p, _)) => p == None, dps); - let ds_nones = List.filter(((p, _)) => p == None, ds); - List.fold_left2( - (result, (_, dp), (_, d)) => - switch (result) { + let f = (result, dp, d) => { + switch (result) { + | DoesNotMatch => DoesNotMatch + | IndetMatch => IndetMatch + | Matches(env) => + switch (matches(dp, d)) { | DoesNotMatch => DoesNotMatch | IndetMatch => IndetMatch - | Matches(env) => - switch (matches(dp, d)) { - | DoesNotMatch => DoesNotMatch - | IndetMatch => IndetMatch - | Matches(env') => Matches(Environment.union(env, env')) - } - }, - result, - dps_nones, - ds_nones, + | Matches(env') => Matches(Environment.union(env, env')) + } + }; + }; + LabeledTuple.ana_tuple( + f, + Matches(Environment.empty), + DoesNotMatch, + dps, + ds, ); - //LabeledTuple.ana_tuple(f, Matches(Environment.empty), DoesNotMatch, dps, ds) } | (Tuple(dps), Cast(d, Prod(tys), Prod(tys'))) => assert(List.length(tys) == List.length(tys')); diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 212a0e9c9c..61f9136db3 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -179,64 +179,14 @@ module rec Typ: { | (Arrow(t1, t2), Arrow(t1', t2')) => eq(t1, t1') && eq(t2, t2') | (Arrow(_), _) => false | (Prod(tys1), Prod(tys2)) => - // List.equal( - // ((p1, t1), (p2, t2)) => - // switch (p1, p2) { - // | (Some(ap), Some(bp)) => - // LabeledTuple.compare(ap, bp) == 0 && eq(t1, t2) - // | (None, None) => eq(t1, t2) - // | (_, _) => false - // }, - // tys1, - // tys2, - // ) - let (_, b) = - List.fold_left( - ((tys1, b), ty2) => - if (b) { - switch (ty2) { - | (None, _) => (tys1, b) - | _ => - let ty1_opt = - List.find_opt( - ty1 => { - switch (ty1, ty2) { - | ((Some(s1), _), (Some(s2), _)) => - LabeledTuple.compare(s1, s2) == 0 - | ((None, _), (None, _)) => true - | (_, _) => false - } - }, - tys1, - ); - switch (ty1_opt, ty2) { - | (Some((_, t1)), (_, t2)) => (tys1, eq(t1, t2)) - | (None, _) => (tys1, false) - }; - }; - } else { - (tys1, false); - }, - (tys1, true), - tys2, - ); - if (b) { - // check Nones - let tys1_nones = List.filter(((p, _)) => p == None, tys1); - let tys2_nones = List.filter(((p, _)) => p == None, tys2); - List.fold_left2( - (b, (_, t1), (_, t2)) => - switch (b) { - | false => false - | true => eq(t1, t2) - }, - b, - tys1_nones, - tys2_nones, - ); - } else { - b; + let f = (b, tys1_val, tys2_val) => { + switch (b) { + | false => false + | true => eq(tys1_val, tys2_val) + }; }; + List.length(tys1) == List.length(tys2) + && LabeledTuple.ana_tuple(f, true, false, tys1, tys2); | (Prod(_), _) => false | (List(t1), List(t2)) => eq(t1, t2) | (List(_), _) => false @@ -448,34 +398,7 @@ module rec Typ: { | Prod(tys) when List.length(tys) == List.length(es) - && List.fold_right( - (ty, b) => { - b - ? { - let e_opt = - List.find_opt( - e => { - switch (e, ty) { - | ((Some(sp), _), (Some(s), _)) => - LabeledTuple.compare(sp, s) == 0 - | ((None, _), (None, _)) => true - | (_, _) => false - } - }, - es, - ); - switch (e_opt) { - | None => false - | _ => true - }; - } - : { - false; - } - }, - tys, - true, - ) => + && LabeledTuple.ana_tuple((a, _, _) => a, true, false, es, tys) => tys |> List.map(((_, ty)) => ty) | Unknown(SynSwitch) => List.init(List.length(es), _ => Unknown(SynSwitch)) From 60604930a612fc6551ca230d64fac8d3bfbc5965 Mon Sep 17 00:00:00 2001 From: WondAli Date: Sun, 7 Jan 2024 16:48:48 -0500 Subject: [PATCH 5/6] error fixes --- src/haz3lcore/LabeledTuple.re | 113 +++++++++++++------------ src/haz3lcore/dynamics/PatternMatch.re | 2 +- src/haz3lcore/statics/MakeTerm.re | 34 +++++--- 3 files changed, 84 insertions(+), 65 deletions(-) diff --git a/src/haz3lcore/LabeledTuple.re b/src/haz3lcore/LabeledTuple.re index 1a3e07d802..cf0502f0e9 100644 --- a/src/haz3lcore/LabeledTuple.re +++ b/src/haz3lcore/LabeledTuple.re @@ -35,58 +35,63 @@ let ana_tuple: let l1_none = List.filter(((p, _)) => p == None, l1); let l2_lab = List.filter(((p, _)) => p != None, l2); let l2_none = List.filter(((p, _)) => p == None, l2); - let accu = - List.fold_left( - (accu, l2_item) => { - let l1_item = - List.find_opt( - l1_item => { - switch (l1_item, l2_item) { - | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 - | ((None, _), (None, _)) => true - | (_, _) => false - } - }, - l1_lab, - ); - switch (l1_item, l2_item) { - | (Some((_, l1_val)), (_, l2_val)) => f(accu, l1_val, l2_val) - | (None, _) => accu_fail - }; - }, - accu, - l2_lab, - ); - // TODO: Currently duplicating checks, for both directions - let accu = - List.fold_left( - (accu, l1_item) => { - let l2_item = - List.find_opt( - l2_item => { - switch (l1_item, l2_item) { - | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 - | ((None, _), (None, _)) => true - | (_, _) => false - } - }, - l2_lab, - ); - switch (l1_item, l2_item) { - | ((_, l1_val), Some((_, l2_val))) => f(accu, l1_val, l2_val) - | (_, None) => accu_fail - }; - }, - accu, - l1_lab, - ); - // None checks - let accu = - List.fold_left2( - (accu, (_, l1_val), (_, l2_val)) => f(accu, l1_val, l2_val), - accu, - l1_none, - l2_none, - ); - accu; + // temporary solution if mess up earlier in tuple, such as make_term + if (List.length(l1_none) != List.length(l2_none)) { + accu_fail; + } else { + let accu = + List.fold_left( + (accu, l2_item) => { + let l1_item = + List.find_opt( + l1_item => { + switch (l1_item, l2_item) { + | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + l1_lab, + ); + switch (l1_item, l2_item) { + | (Some((_, l1_val)), (_, l2_val)) => f(accu, l1_val, l2_val) + | (None, _) => accu_fail + }; + }, + accu, + l2_lab, + ); + // TODO: Currently duplicating checks, for both directions + let accu = + List.fold_left( + (accu, l1_item) => { + let l2_item = + List.find_opt( + l2_item => { + switch (l1_item, l2_item) { + | ((Some(s1), _), (Some(s2), _)) => compare(s1, s2) == 0 + | ((None, _), (None, _)) => true + | (_, _) => false + } + }, + l2_lab, + ); + switch (l1_item, l2_item) { + | ((_, l1_val), Some((_, l2_val))) => f(accu, l1_val, l2_val) + | (_, None) => accu_fail + }; + }, + accu, + l1_lab, + ); + // None checks + let accu = + List.fold_left2( + (accu, (_, l1_val), (_, l2_val)) => f(accu, l1_val, l2_val), + accu, + l1_none, + l2_none, + ); + accu; + }; }; diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re index 89e98423f3..cf133d7dcc 100644 --- a/src/haz3lcore/dynamics/PatternMatch.re +++ b/src/haz3lcore/dynamics/PatternMatch.re @@ -293,7 +293,7 @@ and matches_cast_Tuple = ), ) : match_result => - // TODO: Fix this whole thing + // TODO: Fix this whole thing tuples switch (d) { | TupLabel(_) => DoesNotMatch | Tuple(ds) => diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index fd8ddf2bf4..b13601c6bb 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -79,9 +79,9 @@ let make_labeled_tuple_exp_helper = e, ) | _ => - // after fixing this, can turn all three into one function wwith 'a - let t: UExp.t = {ids: e.ids, term: Invalid("")}; - (None, t); + // Should not ever occur + // let t: UExp.t = {ids: e.ids, term: Invalid("")}; + (None, e) } | _ => (None, exp) }; @@ -116,8 +116,9 @@ let make_labeled_tuple_pat_helper = pt, ) | _ => - let t: UPat.t = {ids: pt.ids, term: Invalid("")}; - (None, t); + // Should not ever occur + // let t: UPat.t = {ids: pt.ids, term: Invalid("")}; + (None, pt) } | _ => (None, pat) }; @@ -152,8 +153,9 @@ let make_labeled_tuple_typ_helper = t, ) | _ => - let t: UTyp.t = {ids: t.ids, term: Invalid("")}; - (None, t); + // Should not ever occur + // let t: UTyp.t = {ids: t.ids, term: Invalid("")}; + (None, t) } | _ => (None, typ) }; @@ -327,7 +329,11 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { } | Bin(Pat(p), tiles, Exp(e)) as tm => switch (tiles) { - | ([(_id, (["="], []))], []) => ret(TupLabel(p, e)) + | ([(_id, (["="], []))], []) => + switch (p.term) { + | Var(_) => ret(TupLabel(p, e)) + | _ => ret(hole(tm)) + } | _ => ret(hole(tm)) } | Bin(Exp(l), tiles, Exp(r)) as tm => @@ -442,7 +448,11 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { ret(Tuple(make_labeled_tuple_pat([l] @ between_kids @ [r]))) | None => switch (tiles) { - | ([(_id, (["="], []))], []) => ret(TupLabel(l, r)) + | ([(_id, (["="], []))], []) => + switch (l.term) { + | Var(_) => ret(TupLabel(l, r)) + | _ => ret(hole(tm)) + } | ([(_id, (["::"], []))], []) => ret(Cons(l, r)) | _ => ret(hole(tm)) } @@ -502,7 +512,11 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { } | Bin(Pat(p), tiles, Typ(t)) as tm => switch (tiles) { - | ([(_id, (["="], []))], []) => ret(TupLabel(p, t)) + | ([(_id, (["="], []))], []) => + switch (p.term) { + | Var(_) => ret(TupLabel(p, t)) + | _ => ret(hole(tm)) + } | _ => ret(hole(tm)) } | Bin(Typ(l), tiles, Typ(r)) as tm => From f56a27865f7e880f5bba78ee2f2cfda3d061c5e1 Mon Sep 17 00:00:00 2001 From: WondAli Date: Sun, 4 Feb 2024 20:04:56 -0500 Subject: [PATCH 6/6] 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) =