Skip to content

Commit

Permalink
label uniqueness checking
Browse files Browse the repository at this point in the history
  • Loading branch information
@WondAli
WondAli committed Nov 10, 2024
1 parent d1cd408 commit ece70b4
Show file tree
Hide file tree
Showing 5 changed files with 206 additions and 76 deletions.
99 changes: 60 additions & 39 deletions src/haz3lcore/LabeledTuple.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))) => {
Expand All @@ -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
Expand Down
59 changes: 54 additions & 5 deletions src/haz3lcore/statics/Info.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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);

Expand All @@ -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;

Expand Down Expand Up @@ -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);
Expand All @@ -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
Expand Down Expand Up @@ -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(_),
Expand Down Expand Up @@ -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 =>
Expand All @@ -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, _) =>
Expand All @@ -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))
}
Expand Down Expand Up @@ -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(_)) =>
Expand Down
10 changes: 8 additions & 2 deletions src/haz3lcore/statics/Self.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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({
Expand Down Expand Up @@ -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) =
Expand Down
Loading

0 comments on commit ece70b4

Please sign in to comment.