Implement Labeled Tuples

Makefile

@@ -64,7 +64,7 @@ test:
 	node $(TEST_DIR)/haz3ltest.bc.js
 
 watch-test:
-	dune build @fmt @runtest --auto-promote --watch
+	dune build @fmt @runtest @default --profile dev --auto-promote --watch
 
 clean:
 	dune clean

src/haz3lcore/LabeledTuple.re

@@ -0,0 +1,290 @@
+open Util;
+
+exception Exception;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type label = string;
+
+let equal: (option((label, 'a)), option((label, 'b))) => bool =
+  (left, right) => {
+    switch (left, right) {
+    | (Some((s1, _)), Some((s2, _))) => String.equal(s1, s2)
+    | (_, _) => false
+    };
+  };
+
+let length = String.length;
+
+let compare = String.compare;
+
+let find_opt: ('a => bool, list('a)) => option('a) = List.find_opt;
+
+// returns a pair containing a list of option(t) and a list of 'a
+// if 'a is a tuplabel, separates the label from the element held by it.
+let separate_labels:
+  ('a => option((label, 'a)), list('a)) =>
+  (list(option(label)), list('a)) =
+  (get_label, es) => {
+    let results =
+      List.fold_left(
+        ((ls, ns), e) =>
+          switch (get_label(e)) {
+          | Some((s1, e)) => (ls @ [Some(s1)], ns @ [e])
+          | None => (ls @ [None], ns @ [e])
+          },
+        ([], []),
+        es,
+      );
+    results;
+  };
+
+// returns a pair containing a list of option(t) and a list of 'a
+// if 'a is a tuplabel, extracts the label but keeps the tuplabel together
+let separate_and_keep_labels:
+  ('a => option((label, 'a)), 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;
+  };
+
+// 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))) => {
+  List.partition_map(
+    ((l, a)) =>
+      switch (l) {
+      | None => Right(a)
+      | Some(l) => Left((l, a))
+      },
+    xs,
+  );
+};
+
+// TODO Performance
+let intersect = (xs, ys) => {
+  List.filter_map(x => List.find_opt((==)(x), ys), xs);
+};
+
+// 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
+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
+      };
+    };
+  };
+
+// Basically another way to call rearrange_base using the raw lists, functions to extract labels from TupLabels, and constructor for new TupLabels.
+// Maintains the same ids if possible
+// TODO: clean up more
+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) => {
+    // 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) =>
+          // TODO: probably can keep the same ids in a cleaner way
+          switch (get_label2(b)) {
+          | Some(_) => b
+          | None => constructor(label, b)
+          }
+        | None => b
+        },
+      l2_reordered,
+    );
+  };
+
+// rearrange two other lists to match the first list of labels.
+// TODO: Ensure that the two lists match up with each other
+// TODO: This function currently exists only to make the elaborator code cleaner. Probably can make more efficient
+let rearrange2:
+  'a 'b.
+  (
+    list(option(label)),
+    'a => option((label, 'a)),
+    'b => option((label, 'b)),
+    list('a),
+    list('b),
+    (label, 'a) => 'a,
+    (label, 'b) => 'b
+  ) =>
+  (list('a), list('b))
+ =
+  (labels, get_label1, get_label2, l1, l2, constructor1, constructor2) => {
+    let (l1_labels, l1_vals) = separate_and_keep_labels(get_label1, l1);
+    let l1' = List.combine(l1_labels, l1_vals);
+    let l1_reordered = rearrange_base(labels, l1');
+    let l1_rearranged =
+      List.map(
+        ((optional_label, b)) =>
+          switch (optional_label) {
+          | Some(label) =>
+            // TODO: probably can keep the same ids in a cleaner way
+            switch (get_label1(b)) {
+            | Some(_) => b
+            | None => constructor1(label, b)
+            }
+          | None => b
+          },
+        l1_reordered,
+      );
+    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(labels, l2');
+    let l2_rearranged =
+      List.map(
+        ((optional_label, b)) =>
+          switch (optional_label) {
+          | Some(label) =>
+            // TODO: probably can keep the same ids in a cleaner way
+            switch (get_label2(b)) {
+            | Some(_) => b
+            | None => constructor2(label, b)
+            }
+          | None => b
+          },
+        l2_reordered,
+      );
+    (l1_rearranged, l2_rearranged);
+  };
+
+let find_label: ('a => option((label, 'a)), list('a), label) => option('a) =
+  (filt, es, label) => {
+    find_opt(
+      e => {
+        switch (filt(e)) {
+        | Some((s, _)) => compare(s, label) == 0
+        | None => false
+        }
+      },
+      es,
+    );
+  };

src/haz3lcore/dynamics/Casts.re

@@ -58,8 +58,10 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
+  | Label(_)
   | Var(_)
   | Rec(_)
+  | TupLabel(_, {term: Unknown(_), _})
   | Forall(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
@@ -81,6 +83,10 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Arrow(_, _) => grounded_Arrow
   | Forall(_) => grounded_Forall
   | List(_) => grounded_List
+  | TupLabel(label, _) =>
+    NotGroundOrHole(
+      TupLabel(label, Unknown(Internal) |> Typ.temp) |> Typ.temp,
+    )
   | Ap(_) => failwith("type application in dynamics")
   };
 };

src/haz3lcore/dynamics/Constraint.re

@@ -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 =>
@@ -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)),
@@ -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))
   };
 
@@ -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))
   };
 

src/haz3lcore/dynamics/DHExp.re

@@ -45,6 +45,8 @@ let rec strip_casts =
         switch (term_of(exp)) {
         /* Leave non-casts unchanged */
         | Tuple(_)
+        | TupLabel(_)
+        | Dot(_)
         | Cons(_)
         | ListConcat(_)
         | ListLit(_)
@@ -71,6 +73,7 @@ let rec strip_casts =
         | Int(_)
         | Float(_)
         | String(_)
+        | Label(_)
         | Constructor(_)
         | DynamicErrorHole(_)
         | Closure(_)
@@ -126,6 +129,8 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Cons(_)
           | ListConcat(_)
           | Tuple(_)
+          | TupLabel(_)
+          | Dot(_)
           | Match(_)
           | DynamicErrorHole(_)
           | Filter(_)
@@ -139,6 +144,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Int(_)
           | Float(_)
           | String(_)
+          | Label(_)
           | FailedCast(_, _, _)
           | MultiHole(_)
           | Deferral(_)