Labeled Tuples

src/haz3lcore/LabeledTuple.re

@@ -0,0 +1,97 @@
+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);
+
+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, 'd) => 'a,
+    'a,
+    'a,
+    list((option('b), 'c)),
+    list((option('b), 'd))
+  ) =>
+  '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);
+    // 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;
+    };
+  };

src/haz3lcore/assistant/AssistantCtx.re

@@ -146,6 +146,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
       List.map(restrategize(" )::"), exp_aps(ty))
       @ List.map(restrategize("::"), exp_refs(ty))
     | Prod([ty, ...tys]) =>
+      let (_, ty) = ty; // TODO: Fix this
       let commas =
         List.init(List.length(tys), _ => ",") |> String.concat(" ");
       List.map(restrategize(" )" ++ commas), exp_aps(ty))
@@ -170,6 +171,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
       List.map(restrategize(" )::"), pat_aps(ty))
       @ List.map(restrategize("::"), pat_refs(ty))
     | Prod([ty, ...tys]) =>
+      let (_, ty) = ty; // TODO: Fix this
       let commas =
         List.init(List.length(tys), _ => ",") |> String.concat(" ");
       List.map(restrategize(" )" ++ commas), pat_aps(ty))

src/haz3lcore/assistant/AssistantForms.re

@@ -33,7 +33,7 @@ module Typ = {
 
   let of_infix_delim: list((Token.t, Typ.t)) = [
     ("|>", unk), /* */
-    (",", Prod([unk, unk])), /* NOTE: Current approach doesn't work for this, but irrelevant as 1-char */
+    (",", Prod([(None, unk), (None, unk)])), /* NOTE: Current approach doesn't work for this, but irrelevant as 1-char */
     ("::", List(unk)),
     ("@", List(unk)),
     (";", unk),

src/haz3lcore/dynamics/Builtins.re

@@ -145,7 +145,7 @@ module Pervasives = {
 
     let int_mod = (name, d1) =>
       switch (d1) {
-      | Tuple([IntLit(n), IntLit(m)]) =>
+      | Tuple([(_, IntLit(n)), (_, IntLit(m))]) =>
         switch (m) {
         | 0 => InvalidOperation(ApBuiltin(name, [d1]), DivideByZero)
         | _ => IntLit(n mod m)
@@ -163,7 +163,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)),
       );
@@ -183,7 +183,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)))
@@ -194,7 +194,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(StringLit(String.sub(s, idx, len)))) {
           | _ =>
             let d' = DHExp.ApBuiltin(name, [d]);
@@ -251,22 +251,26 @@ 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("mod"))
+    |> fn(
+         "mod",
+         Arrow(Prod([(None, Int), (None, Int)]), Int),
+         int_mod("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),
+         Arrow(Prod([(None, String), (None, Int), (None, Int)]), String),
          string_sub("string_sub"),
        );
 };

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,17 @@ 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)) =>
+      // 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(fast_equal, 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)
@@ -256,6 +268,7 @@ module rec DHExp: {
     | (Cons(_), _)
     | (ListConcat(_), _)
     | (ListLit(_), _)
+    | (TupLabel(_), _)
     | (Tuple(_), _)
     | (Prj(_), _)
     | (BinBoolOp(_), _)

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);

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 Tuple
       | 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 Tuple stuff
+    | 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) =>

src/haz3lcore/dynamics/Evaluator.re

@@ -71,6 +71,16 @@ module Evaluator: {
         (r1 && r2, [x', ...xs']);
       };
 
+  let rec req_all_final_tuple = (f, i, dsp, dst) =>
+    switch (dsp, dst) {
+    | ([], []) => (BoxedReady, [])
+    | ([p, ...ps], [x, ...xs]) =>
+      let (r1, x') = req_final(f, i, x);
+      let (r2, pxs') = req_all_final_tuple(f, i + 1, ps, xs);
+      (r1 && r2, [(p, x'), ...pxs']);
+    | (_, _) => (BoxedReady, []) //TODO: Handle this error, though should never occur.
+    };
+
   let otherwise = c => (BoxedReady, (), c);
 
   let (and.) = ((r1, x1, c1), (r2, x2)) => (r1 && r2, (x1, x2), c1(x2));