Skip to content

Commit

Permalink
Implement Labeled Tuples (#1235)
Browse files Browse the repository at this point in the history
  • Loading branch information
cyrus- authored Feb 11, 2025
2 parents 61b5c0b + f9a8381 commit 119284e
Show file tree
Hide file tree
Showing 58 changed files with 16,130 additions and 9,591 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ test:
node $(TEST_DIR)/haz3ltest.bc.js

watch-test:
dune build @ocaml-index @fmt @runtest --auto-promote --watch
dune build @ocaml-index @fmt @runtest @default --profile dev --auto-promote --watch

coverage:
dune build @src/fmt @test/fmt --auto-promote src test --profile dev
Expand Down
213 changes: 213 additions & 0 deletions src/haz3lcore/LabeledTuple.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,213 @@
open Util;

exception Exception;

[@deriving (show({with_path: false}), sexp, yojson)]
type label = string;

let equal_label = String.equal;

let has_same_labels: (option((label, 'a)), option((label, 'b))) => bool =
(left, right) => {
switch (left, right) {
| (Some((s1, _)), Some((s2, _))) => equal_label(s1, s2)
| (_, _) => false
};
};

// This function should only be used for type checking labels
let match_labels: (label, label) => bool =
(label1, label2) => {
switch (label1, label2) {
// Empty label is a placeholder for checking any label
| ("", _)
| (_, "") => true
| (_, _) => label1 == label2
};
};

// returns a pair containing a list of option(label) and a list of 'a
// if 'a is a tuplabel, extracts the label but keeps the tuplabel together
let separate_and_keep_labels:
'a 'b.
('a => option((label, 'b)), list('a)) =>
(list(option(label)), list('a))
=
(get_label, es) => {
let results =
List.fold_left(
((ls, ns), e) =>
switch (get_label(e)) {
| Some((s1, _)) => (ls @ [Some(s1)], ns @ [e])
| None => (ls @ [None], ns @ [e])
},
([], []),
es,
);
results;
};

// Keeps the labels in x that exist in y. Maintains the order from x.
let intersect = (xs: list(label), ys: list(label)) => {
List.filter_map(x => List.find_opt(equal_label(x), ys), xs);
};

// Takes a list of strings and returns a list of duplicates
// Can also be modified to get unique labels.
let get_duplicate_labels_base: list(label) => list(label) =
labels => {
let (duplicates, _seen) =
List.fold_left(
((dupes, seen), label) =>
if (List.exists(l => label == l, seen)) {
List.exists(l => label == l, dupes)
? (dupes, seen) : (dupes @ [label], seen);
} else {
(dupes, seen @ [label]);
},
([], []),
labels,
);
duplicates;
};

let get_duplicate_labels:
'a 'b.
('a => option((label, 'b)), list('a)) => list(label)
=
(get_label, es) => {
separate_and_keep_labels(get_label, es)
|> fst
|> List.filter_map(Fun.id)
|> get_duplicate_labels_base;
};

/**
* 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 be reordered for all present labels first and then unlabeled fields matched up pairwise.
* So labeled fields can be reordered and unlabeled ones can't. Also, add labels to the unlabeled.
*/
let rec rearrange_base:
'b.
(
~show_b: 'b => string=?,
list(option(label)),
list((option(label), 'b))
) =>
list((option(label), 'b))
=
(~show_b=?, l1: list(option(label)), l2: list((option(label), 'b))) => {
let l1_labels = List.filter_map(Fun.id, l1);
let l2_labels = List.filter_map(fst, l2);
let common_labels = intersect(l1_labels, l2_labels);

switch (l1, l2) {
| ([], _) => l2
| (_, []) => []
| ([Some(expected_label), ...remaining_expectations], remaining) =>
let maybe_found = List.assoc_opt(Some(expected_label), remaining);

switch (maybe_found) {
| Some(found) =>
[(Some(expected_label), found)]
@ rearrange_base(
~show_b?,
remaining_expectations,
List.remove_assoc(Some(expected_label), remaining),
)
| None =>
let (
pre: list((option(label), 'b)),
current: option((option(label), 'b)),
post: list((option(label), 'b)),
) =
ListUtil.split(remaining, ((label: option(label), _)) => {
switch (label) {
| Some(label) => !List.mem(label, common_labels)
| None => true
}
});

switch (current) {
| Some((_existing_label, b)) =>
[(Some(expected_label), b)]
@ rearrange_base(~show_b?, remaining_expectations, pre @ post)
| None => remaining
};
};
| ([None, ...remaining_expectations], remaining) =>
// Pick the first one that's not in common labels and then keep the rest in remaining
let (
pre: list((option(label), 'b)),
current: option((option(label), 'b)),
post: list((option(label), 'b)),
) =
ListUtil.split(remaining, ((label: option(label), _)) => {
switch (label) {
| Some(label) => !List.mem(label, common_labels)
| None => true
}
});
switch (current) {
| Some((_existing_label, b)) =>
[(None, b)]
@ rearrange_base(~show_b?, remaining_expectations, pre @ post)
| None => remaining
};
};
};

/**
* Rearranges the elements of the list to match up the labels and adds missing labels.
* This function is essentially another way to call `rearrange_base` using raw lists.
* It utilizes functions to extract labels from `TupLabels` and a constructor for new `TupLabels`.
* The function maintains the same ids if possible, ensuring that the rearranged list
* preserves the original structure as closely as possible while accommodating any new labels.
*/
let rearrange:
'a 'b.
(
'a => option((label, 'a)),
'b => option((label, 'b)),
list('a),
list('b),
(label, 'b) => 'b
) =>
list('b)
=
(get_label1, get_label2, l1, l2, constructor) =>
if (List.length(l1) != List.length(l2)) {
l2;
} else {
// TODO: Error handling in case of bad arguments
let l1' = fst(separate_and_keep_labels(get_label1, l1));
let (l2_labels, l2_vals) = separate_and_keep_labels(get_label2, l2);
let l2' = List.combine(l2_labels, l2_vals);
let l2_reordered = rearrange_base(l1', l2');
List.map(
((optional_label, b)) =>
switch (optional_label) {
| Some(label) =>
switch (get_label2(b)) {
| Some(_) => b
| None => constructor(label, b)
}
| None => b
},
l2_reordered,
);
};

let find_label: ('a => option((label, 'a)), list('a), label) => option('a) =
(filt, es, label) => {
List.find_opt(
e => {
switch (filt(e)) {
| Some((s, _)) => s == label
| None => false
}
},
es,
);
};
20 changes: 16 additions & 4 deletions src/haz3lcore/assistant/AssistantForms.re
Original file line number Diff line number Diff line change
Expand Up @@ -197,10 +197,22 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
};

let suggest_operator: Info.t => list(Suggestion.t) =
suggest_form(
List.map(((a, b)) => (a, IdTagged.fresh(b)), Typ.of_infix_delim),
Delims.infix,
);
info => {
switch (info) {
| InfoExp({
term:
{term: Tuple([{term: TupLabel({term: Label(_), _}, _), _}]), _},
_,
}) =>
[] // Stop completing (a= to (a==
| _ =>
suggest_form(
List.map(((a, b)) => (a, IdTagged.fresh(b)), Typ.of_infix_delim),
Delims.infix,
info,
)
};
};

let suggest_operand: Info.t => list(Suggestion.t) =
suggest_form(Typ.of_const_mono_delim, Delims.const_mono);
Expand Down
27 changes: 18 additions & 9 deletions src/haz3lcore/assistant/TyDi.re
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,24 @@ let suggest = (ci: Info.t, z: Zipper.t): list(Suggestion.t) => {
* may not be desirable in other ways, for example maybe we want
* recency bias in ctx. Revisit this later. I'm sorting before
* combination because we want backpack candidates to show up first */
suggest_backpack(z)
@ (
AssistantForms.suggest_operand(ci)
@ AssistantForms.suggest_leading(ci)
@ AssistantCtx.suggest_variable(ci)
@ AssistantCtx.suggest_lookahead_variable(ci)
|> List.sort(Suggestion.compare)
)
@ (AssistantForms.suggest_operator(ci) |> List.sort(Suggestion.compare));
switch (ci) {
| InfoExp({cls: Exp(Label), _})
| InfoPat({cls: Pat(Label), _})
| InfoTyp({cls: Typ(Label), _})
| InfoExp({cls: Exp(TupLabel), _})
| InfoPat({cls: Pat(TupLabel), _})
| InfoTyp({cls: Typ(TupLabel), _}) => [] // TODO: Autocomplete for labels
| _ =>
suggest_backpack(z)
@ (
AssistantForms.suggest_operand(ci)
@ AssistantForms.suggest_leading(ci)
@ AssistantCtx.suggest_variable(ci)
@ AssistantCtx.suggest_lookahead_variable(ci)
|> List.sort(Suggestion.compare)
)
@ (AssistantForms.suggest_operator(ci) |> List.sort(Suggestion.compare))
};
};

/* If there is a monotile to the left of the caret, return it. We
Expand Down
6 changes: 6 additions & 0 deletions src/haz3lcore/dynamics/Casts.re
Original file line number Diff line number Diff line change
Expand Up @@ -58,12 +58,18 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
| Int
| Float
| String
| Label(_)
| TupLabel(_, {term: Unknown(_), _})
| Var(_)
| Rec(_)
| Forall(_, {term: Unknown(_), _})
| Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
| List({term: Unknown(_), _}) => Ground
| Parens(ty) => ground_cases_of(ty)
| TupLabel(label, _) =>
NotGroundOrHole(
TupLabel(label, Unknown(Internal) |> Typ.temp) |> Typ.temp,
)
| Prod(tys) =>
if (List.for_all(
fun
Expand Down
4 changes: 4 additions & 0 deletions src/haz3lcore/dynamics/Constraint.re
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ type t =
| Or(t, t)
| InjL(t)
| InjR(t)
| TupLabel(t, t)
| Pair(t, t);

let rec dual = (c: t): t =>
Expand All @@ -32,6 +33,7 @@ let rec dual = (c: t): t =>
| Or(c1, c2) => And(dual(c1), dual(c2))
| InjL(c1) => Or(InjL(dual(c1)), InjR(Truth))
| InjR(c2) => Or(InjR(dual(c2)), InjL(Truth))
| TupLabel(c1, c2) => TupLabel(dual(c1), dual(c2))
| Pair(c1, c2) =>
Or(
Pair(c1, dual(c2)),
Expand All @@ -55,6 +57,7 @@ let rec truify = (c: t): t =>
| Or(c1, c2) => Or(truify(c1), truify(c2))
| InjL(c) => InjL(truify(c))
| InjR(c) => InjR(truify(c))
| TupLabel(c1, c2) => TupLabel(truify(c1), truify(c2))
| Pair(c1, c2) => Pair(truify(c1), truify(c2))
};

Expand All @@ -74,6 +77,7 @@ let rec falsify = (c: t): t =>
| Or(c1, c2) => Or(falsify(c1), falsify(c2))
| InjL(c) => InjL(falsify(c))
| InjR(c) => InjR(falsify(c))
| TupLabel(c1, c2) => TupLabel(falsify(c1), falsify(c2))
| Pair(c1, c2) => Pair(falsify(c1), falsify(c2))
};

Expand Down
Loading

0 comments on commit 119284e

Please sign in to comment.