diff --git a/src/haz3lcore/LabeledTuple.re b/src/haz3lcore/LabeledTuple.re index fbbfdee19..a4ac9a667 100644 --- a/src/haz3lcore/LabeledTuple.re +++ b/src/haz3lcore/LabeledTuple.re @@ -57,45 +57,6 @@ let separate_and_keep_labels: results; }; -// returns ordered list of (Some(string), TupLabel) -// and another of (None, not-TupLabel) -// TODO: Actually validate uniqueness in statics -// TODO: Make more efficient -// let validate_uniqueness: -// 'a. -// ('a => option((t, 'a)), list('a)) => -// (bool, list((option(t), 'a)), list('a)) -// = -// (get_label, es) => { -// let results = -// List.fold_left( -// ((b, ls, ns), e) => -// switch (get_label(e)) { -// | Some((s1, _)) -// when -// b -// && List.fold_left( -// (v, l) => -// switch (l) { -// | (Some(s2), _) when v => compare(s1, s2) != 0 -// | _ => false -// }, -// true, -// ls, -// ) => ( -// b, -// ls @ [(Some(s1), e)], -// ns, -// ) -// | None => (b, ls, ns @ [e]) -// | _ => (false, ls, ns) -// }, -// (true, [], []), -// es, -// ); -// results; -// }; - // TODO consider adding a t = (option(label), 'a) let separate_labeled = (xs: list((option(label), 'a))) => { @@ -114,6 +75,66 @@ let intersect = (xs, ys) => { List.filter_map(x => List.find_opt((==)(x), ys), xs); }; +// TODO: can just use get_duplicate_labels and check if empty. +// Takes a list of strings and returns true if there are no duplicates. +let rec is_uniquely_labeled_base: list(label) => bool = + labels => { + let contains_duplicates = + switch (labels) { + | [] => false + | [hd, ...tl] => + List.exists(l => hd == l, tl) || is_uniquely_labeled_base(tl) + }; + !contains_duplicates; + }; + +// TODO: Performance +// Takes a list of strings and returns a list of duplicates and list of uniques. +// Can also be modified to get unique labels. +let get_duplicate_and_unique_labels_base: + list(label) => (list(label), list(label)) = + labels => { + let (duplicates, uniques) = + List.fold_left( + (acc, label) => { + let (dupes, uniqs) = acc; + List.exists(l => label == l, uniqs) + ? List.exists(l => label == l, dupes) + ? (dupes, uniqs) : (dupes @ [label], uniqs) + : (dupes, uniqs @ [label]); + }, + ([], []), + labels, + ); + (duplicates, uniques); + }; + +// Takes in a get_label function and a list of elements and applys is_uniquely_labeled_base +let is_uniquely_labeled: 'a. ('a => option((label, 'a)), list('a)) => bool = + (get_label, es) => { + let labels = fst(separate_and_keep_labels(get_label, es)); + let labels = + labels + |> List.filter(x => Option.is_some(x)) + |> OptUtil.sequence + |> OptUtil.get(() => []); + is_uniquely_labeled_base(labels); + }; + +let get_duplicate_and_unique_labels: + 'a. + ('a => option((label, 'a)), list('a)) => (list(label), list(label)) + = + (get_label, es) => { + let labels = fst(separate_and_keep_labels(get_label, es)); + let labels = + labels + |> List.filter(x => Option.is_some(x)) + |> OptUtil.sequence + |> OptUtil.get(() => []); + get_duplicate_and_unique_labels_base(labels); + }; + // Assumes all labels are unique // Rearranges all the labels in l2 to match the order of the labels in l1. Labels are optional and should me reordered for all present labels first and then unlabled fields matched up pairwise. So labeled fields can be reordered and unlabeled ones can't. Also add labels to the unlabeled. // TODO Handle the unequal length case and extra labels case diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 6202d262f..e9580b476 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -59,7 +59,11 @@ type error_common = /* Underdetermined: No type can be assigned */ | NoType(error_no_type) /* Overdetermined: Conflicting type expectations */ - | Inconsistent(error_inconsistent); + | Inconsistent(error_inconsistent) + /* Duplicate labels in labeled tuple */ + | DuplicateLabels(Typ.t) + /* Duplicate item, used for duplicated labels*/ + | Duplicate(Typ.t); [@deriving (show({with_path: false}), sexp, yojson)] type error_exp = @@ -132,7 +136,8 @@ type status_variant = [@deriving (show({with_path: false}), sexp, yojson)] type typ_expects = | TypeExpected - | TupleExpected + | TupleExpected(status_variant) + | LabelExpected(status_variant, list(string)) // list of duplicate labels expected to NOT be | ConstructorExpected(status_variant, Typ.t) | VariantExpected(status_variant, Typ.t); @@ -145,8 +150,11 @@ type error_typ = | BadToken(Token.t) /* Invalid token, treated as type hole */ | FreeTypeVariable(string) /* Free type variable */ | DuplicateConstructor(Constructor.t) /* Duplicate ctr in same sum */ + | DuplicateLabels(Typ.t) + | Duplicate(Typ.t) | WantTypeFoundAp | WantTuple + | WantLabel | WantConstructorFoundType(Typ.t) | WantConstructorFoundAp; @@ -373,6 +381,11 @@ let rec status_common = } | (BadToken(name), _) => InHole(NoType(BadToken(name))) | (BadTrivAp(ty), _) => InHole(NoType(BadTrivAp(ty))) + | (Duplicate_Labels(Just(ty)), _) => InHole(DuplicateLabels(ty)) + | (Duplicate(Just(ty)), _) => InHole(Duplicate(ty)) + | (Duplicate_Labels(_), _) => + InHole(DuplicateLabels(Unknown(Internal) |> Typ.temp)) + | (Duplicate(_), _) => InHole(Duplicate(Unknown(Internal) |> Typ.temp)) | (IsMulti, _) => NotInHole(Syn(Unknown(Internal) |> Typ.temp)) | (NoJoin(wrap, tys), Ana(ana)) => let syn: Typ.t = Self.join_of(wrap, Unknown(Internal) |> Typ.temp); @@ -395,6 +408,8 @@ let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => | InHole(Common(Inconsistent(Internal(_) | Expectation(_))) as err) | InHole(Common(NoType(_)) as err) => Some(err) | NotInHole(_) => None + | InHole(Common(DuplicateLabels(_))) // Is this right? + | InHole(Common(Duplicate(_))) | InHole(Common(Inconsistent(WithArrow(_)))) | InHole(ExpectedConstructor | Redundant(_)) => // ExpectedConstructor cannot be a reason to hole-wrap the entire pattern @@ -431,6 +446,8 @@ let rec status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp => | NotInHole(_) | InHole(Common(Inconsistent(Expectation(_) | WithArrow(_)))) => None /* Type checking should fail and these errors would be nullified */ | InHole(Common(NoType(_))) + | InHole(Common(DuplicateLabels(_))) // Is this right? + | InHole(Common(Duplicate(_))) | InHole( FreeVariable(_) | InexhaustiveMatch(_) | UnusedDeferral | BadPartialAp(_), @@ -467,12 +484,18 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ => | VariantExpected(Duplicate, _) | ConstructorExpected(Duplicate, _) => InHole(DuplicateConstructor(name)) - | TupleExpected => + | TupleExpected(_) => switch (Ctx.lookup_alias(ctx, name)) { | Some({term: Prod(_), _}) => NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty))) | _ => InHole(WantTuple) } + | LabelExpected(_) => + switch (Ctx.lookup_alias(ctx, name)) { + | Some({term: Label(_), _}) => + NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty))) + | _ => InHole(WantLabel) + } | TypeExpected => switch (Ctx.is_alias(ctx, name)) { | false => @@ -493,7 +516,8 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ => NotInHole(VariantIncomplete(Arrow(ty_in, ty_variant) |> Typ.temp)) } | ConstructorExpected(_) => InHole(WantConstructorFoundAp) - | TupleExpected => InHole(WantTuple) + | TupleExpected(_) => InHole(WantTuple) + | LabelExpected(_) => InHole(WantLabel) | TypeExpected => InHole(WantTypeFoundAp) } // | Dot(t1, _) => @@ -505,10 +529,33 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ => // } // | _ => NotInHole(Type(ty)) // } + | Label(name) => + switch (expects) { + | TypeExpected => NotInHole(Type(ty)) + | TupleExpected(_) => InHole(WantTuple) + | LabelExpected(_, dupes) => + List.exists(l => name == l, dupes) + ? InHole(Duplicate(ty)) : InHole(WantLabel) + | ConstructorExpected(_) + | VariantExpected(_) => InHole(WantConstructorFoundType(ty)) + } + | Prod(_) => + switch (expects) { + | TypeExpected => NotInHole(Type(ty)) + | TupleExpected(status) => + switch (status) { + | Duplicate => InHole(DuplicateLabels(ty)) + | _ => InHole(WantTuple) // shouldn't happen + } + | LabelExpected(_) => InHole(WantLabel) + | ConstructorExpected(_) + | VariantExpected(_) => InHole(WantConstructorFoundType(ty)) + } | _ => switch (expects) { | TypeExpected => NotInHole(Type(ty)) - | TupleExpected => InHole(WantTuple) + | TupleExpected(_) => InHole(WantTuple) + | LabelExpected(_) => InHole(WantLabel) | ConstructorExpected(_) | VariantExpected(_) => InHole(WantConstructorFoundType(ty)) } @@ -571,6 +618,8 @@ let fixed_typ_ok: ok_pat => Typ.t = let fixed_typ_err_common: error_common => Typ.t = fun | NoType(_) => Unknown(Internal) |> Typ.temp + | DuplicateLabels(typ) => typ + | Duplicate(typ) => typ | Inconsistent(Expectation({ana, _})) => ana | Inconsistent(Internal(_)) => Unknown(Internal) |> Typ.temp // Should this be some sort of meet? | Inconsistent(WithArrow(_)) => diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index cece7d2b0..87d699e55 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -29,7 +29,9 @@ type join_type = type t = | Just(Typ.t) /* Just a regular type */ | NoJoin(join_type, list(Typ.source)) /* Inconsistent types for e.g match, listlits */ - | BadToken(Token.t) /* Invalid expression token, treated as hole */ + | Duplicate_Labels(t) /* Duplicate labels in a labeled tuple, treated as regular type (?) */ + | Duplicate(t) /* Duplicatee label, marked as duplicate */ + | BadToken(Token.t) /* Invalid expression token, continues with undefined behavior */ | BadTrivAp(Typ.t) /* Trivial (nullary) ap on function that doesn't take triv */ | IsMulti /* Multihole, treated as hole */ | IsConstructor({ @@ -71,11 +73,15 @@ let join_of = (j: join_type, ty: Typ.t): Typ.t => let typ_of: (Ctx.t, t) => option(Typ.t) = _ctx => fun - | Just(typ) => Some(typ) + | Just(typ) + | Duplicate_Labels(Just(typ)) + | Duplicate(Just(typ)) => Some(typ) | IsConstructor({syn_ty, _}) => syn_ty | BadToken(_) | BadTrivAp(_) | IsMulti + | Duplicate_Labels(_) + | Duplicate(_) | NoJoin(_) => None; let typ_of_exp: (Ctx.t, exp) => option(Typ.t) = diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index dc7b8b809..fd13ac892 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -131,7 +131,7 @@ let rec any_to_info_map = switch (any) { | Exp(e) => let ({co_ctx, _}: Info.exp, m) = - uexp_to_info_map(~ctx, ~ancestors, e, m); + uexp_to_info_map(~ctx, ~ancestors, ~duplicates=[], e, m); (co_ctx, m); | Pat(p) => let m = @@ -139,6 +139,7 @@ let rec any_to_info_map = ~is_synswitch=false, ~co_ctx=CoCtx.empty, ~ancestors, + ~duplicates=[], ~ctx, p, m, @@ -172,6 +173,7 @@ and uexp_to_info_map = ~mode=Mode.Syn, ~is_in_filter=false, ~ancestors, + ~duplicates: list(string), {ids, copied: _, term} as uexp: UExp.t, m: Map.t, ) @@ -219,20 +221,30 @@ and uexp_to_info_map = ~mode=Mode.Syn, ~is_in_filter=is_in_filter, ~ancestors=ancestors, + ~duplicates=[], uexp: UExp.t, m: Map.t, ) => { - uexp_to_info_map(~ctx, ~mode, ~is_in_filter, ~ancestors, uexp, m); + uexp_to_info_map( + ~ctx, + ~mode, + ~is_in_filter, + ~ancestors, + ~duplicates, + uexp, + m, + ); }; let go' = uexp_to_info_map(~ancestors); let go = go'(~ctx); - let map_m_go = m => + let map_m_go = (m, ~duplicates=[]) => List.fold_left2( ((es, m), mode, e) => - go(~mode, e, m) |> (((e, m)) => (es @ [e], m)), + go(~mode, ~duplicates, e, m) |> (((e, m)) => (es @ [e], m)), ([], m), ); - let go_pat = upat_to_info_map(~ctx, ~ancestors); + // TODO: Confirm if duplicates should or not be default [] + let go_pat = upat_to_info_map(~ctx, ~ancestors, ~duplicates); let elaborate_singleton_tuple = (uexp: Exp.t, inner_ty, l, m) => { print_endline("Elaborating singleton tuple"); let (term, rewrap) = UExp.unwrap(uexp); @@ -291,7 +303,10 @@ and uexp_to_info_map = | Int(_) => atomic(Just(Int |> Typ.temp)) | Float(_) => atomic(Just(Float |> Typ.temp)) | String(_) => atomic(Just(String |> Typ.temp)) - | Label(name) => atomic(Just(Label(name) |> Typ.temp)) + | Label(name) => + let self = Self.Just(Label(name) |> Typ.temp); + List.exists(l => name == l, duplicates) + ? atomic(Duplicate(self)) : atomic(self); | ListLit(es) => let ids = List.map(UExp.rep_id, es); let modes = Mode.of_list_lit(ctx, List.length(es), mode); @@ -361,7 +376,7 @@ and uexp_to_info_map = ); | TupLabel(label, e) => let (labmode, mode) = Mode.of_label(ctx, mode); - let (lab, m) = go(~mode=labmode, label, m); + let (lab, m) = go(~mode=labmode, ~duplicates, label, m); let (e, m) = go(~mode, e, m); add( ~self=Just(TupLabel(lab.ty, e.ty) |> Typ.temp), @@ -379,12 +394,14 @@ and uexp_to_info_map = Mode.of_prod(ctx, mode, es, UExp.get_label, (name, b) => TupLabel(Label(name) |> Exp.fresh, b) |> Exp.fresh ); - let (es', m) = map_m_go(m, modes, es); - add( - ~self=Just(Prod(List.map(Info.exp_ty, es')) |> Typ.temp), - ~co_ctx=CoCtx.union(List.map(Info.exp_co_ctx, es')), - m, - ); + let (duplicate_labels, _) = + LabeledTuple.get_duplicate_and_unique_labels(Exp.get_label, es); + let (es', m) = map_m_go(~duplicates=duplicate_labels, m, modes, es); + let ty_list = List.map(Info.exp_ty, es'); + let self = Self.Just(Prod(ty_list) |> Typ.temp); + let self = + List.is_empty(duplicate_labels) ? self : Self.Duplicate_Labels(self); + add(~self, ~co_ctx=CoCtx.union(List.map(Info.exp_co_ctx, es')), m); | Dot(e1, e2) => let (info_e1, m) = go(~mode=Syn, e1, m); let (ty, m) = { @@ -877,6 +894,7 @@ and upat_to_info_map = ~ctx, ~co_ctx, ~ancestors: Info.ancestors, + ~duplicates: list(string), ~mode: Mode.t=Mode.Syn, {ids, term, _} as upat: UPat.t, m: Map.t, @@ -909,6 +927,7 @@ and upat_to_info_map = ~ctx, ~co_ctx, ~ancestors, + ~duplicates=[], ~mode, upat: UPat.t, m: Map.t, @@ -918,6 +937,7 @@ and upat_to_info_map = ~ctx, ~co_ctx, ~ancestors, + ~duplicates, ~mode, upat, m: Map.t, @@ -927,10 +947,10 @@ and upat_to_info_map = let ancestors = [UPat.rep_id(upat)] @ ancestors; let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx); let unknown = Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp; - let ctx_fold = (ctx: Ctx.t, m) => + let ctx_fold = (ctx: Ctx.t, m, ~duplicates=[]) => List.fold_left2( ((ctx, tys, cons, m), e, mode) => - go(~ctx, ~mode, e, m) + go(~ctx, ~mode, ~duplicates, e, m) |> ( ((info, m)) => ( info.ctx, @@ -961,7 +981,12 @@ and upat_to_info_map = ) | String(string) => atomic(Just(String |> Typ.temp), Constraint.String(string)) - | Label(name) => atomic(Just(Label(name) |> Typ.temp), Constraint.Truth) + | Label(name) => + // TODO: Constraint? + let self = Self.Just(Label(name) |> Typ.temp); + List.exists(l => name == l, duplicates) + ? atomic(Duplicate(self), Constraint.Truth) + : atomic(self, Constraint.Truth); | ListLit(ps) => let ids = List.map(UPat.rep_id, ps); let modes = Mode.of_list_lit(ctx, List.length(ps), mode); @@ -1009,7 +1034,7 @@ and upat_to_info_map = ); | TupLabel(label, p) => let (labmode, mode) = Mode.of_label(ctx, mode); - let (lab, m) = go(~ctx, ~mode=labmode, label, m); + let (lab, m) = go(~ctx, ~mode=labmode, ~duplicates, label, m); let (p, m) = go(~ctx, ~mode, p, m); add( ~self=Just(TupLabel(lab.ty, p.ty) |> Typ.temp), @@ -1022,19 +1047,20 @@ and upat_to_info_map = Mode.of_prod(ctx, mode, ps, UPat.get_label, (name, b) => TupLabel(Label(name) |> UPat.fresh, b) |> UPat.fresh ); - let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); let rec cons_fold_tuple = cs => switch (cs) { | [] => Constraint.Truth | [elt] => elt | [hd, ...tl] => Constraint.Pair(hd, cons_fold_tuple(tl)) }; - add( - ~self=Just(Prod(tys) |> Typ.temp), - ~ctx, - ~constraint_=cons_fold_tuple(cons), - m, - ); + let (duplicate_labels, _) = + LabeledTuple.get_duplicate_and_unique_labels(Pat.get_label, ps); + let (ctx, tys, cons, m) = + ctx_fold(ctx, m, ~duplicates=duplicate_labels, ps, modes); + let self = Self.Just(Prod(tys) |> Typ.temp); + let self = + List.is_empty(duplicate_labels) ? self : Self.Duplicate_Labels(self); + add(~self, ~ctx, ~constraint_=cons_fold_tuple(cons), m); | Parens(p) => let (p, m) = go(~ctx, ~mode, p, m); add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); @@ -1069,10 +1095,11 @@ and utyp_to_info_map = m: Map.t, ) : (Info.typ, Map.t) => { - let add = (~utyp=utyp, m) => { + let add' = (~expects=expects, ~utyp=utyp, m) => { let info = Info.derived_typ(~utyp, ~ctx, ~ancestors, ~expects); (info, add_info(ids, InfoTyp(info), m)); }; + let add = (~utyp=utyp, m) => add'(~utyp, m); let ancestors = [UTyp.rep_id(utyp)] @ ancestors; let go' = utyp_to_info_map(~ctx, ~ancestors); let go = go'(~expects=TypeExpected); @@ -1096,12 +1123,33 @@ and utyp_to_info_map = let m = go(t2, m) |> snd; add(m); | TupLabel(label, t) => - let m = go(label, m) |> snd; + let expects = + switch (expects) { + | LabelExpected(_) => expects + | _ => TypeExpected + }; + let m = go'(~expects, label, m) |> snd; let m = go(t, m) |> snd; - add(m); + add'(~expects=TypeExpected, m); | Prod(ts) => - let m = map_m(go, ts, m) |> snd; - add(m); + // let m = map_m(go, ts, m) |> snd; + // add(m); + let (duplicate_labels, _) = + LabeledTuple.get_duplicate_and_unique_labels(Typ.get_label, ts); + let (expects, m) = + List.is_empty(duplicate_labels) + ? (expects, map_m(go, ts, m) |> snd) + : ( + TupleExpected(Duplicate), + map_m( + go'(~expects=LabelExpected(Duplicate, duplicate_labels)), + ts, + m, + ) + |> snd, + ); + let info = Info.derived_typ(~utyp, ~ctx, ~ancestors, ~expects); + (info, add_info(ids, InfoTyp(info), m)); | Ap(t1, t2) => let t1_mode: Info.typ_expects = switch (expects) { @@ -1224,7 +1272,8 @@ and variant_to_info_map = let mk = Core.Memo.general(~cache_size_bound=1000, (ctx, e) => { - uexp_to_info_map(~ctx, ~ancestors=[], e, Id.Map.empty) |> snd + uexp_to_info_map(~ctx, ~ancestors=[], ~duplicates=[], e, Id.Map.empty) + |> snd }); let mk = (core: CoreSettings.t, ctx, exp) => diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 17e36c948..6e05fcd76 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -81,6 +81,8 @@ let common_err_view = Type.view(Prod([]) |> Typ.fresh), ] | NoType(FreeConstructor(name)) => [code_err(name), text("not found")] + | DuplicateLabels(_) => [text("Duplicate labels within a tuple")] + | Duplicate(_) => [text("Duplicated Label")] | Inconsistent(WithArrow(typ)) => [ text(":"), Type.view(typ), @@ -188,6 +190,9 @@ let typ_err_view = (ok: Info.error_typ) => | WantConstructorFoundType(_) => [text("Expected a constructor")] | WantTypeFoundAp => [text("Must be part of a sum type")] | WantTuple => [text("Expect a valid tuple")] + | WantLabel => [text("Expect a valid label")] + | DuplicateLabels(_) => [text("Duplicate labels within a tuple")] + | Duplicate(_) => [text("Duplicated Label")] | DuplicateConstructor(name) => [ Type.view(Var(name) |> Typ.fresh), text("already used in this sum"),