Fixed singleton labeled tuple in function application

hazelgrove · Nov 4, 2024 · 12eef70 · 12eef70
1 parent 8d3d3e6
commit 12eef70
Show file tree

Hide file tree

Showing 3 changed files with 67 additions and 56 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -18,59 +18,18 @@ module ElaborationResult = {
     | DoesNotElaborate;
 };
 
-let rec fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => {
-  switch (t1.term) {
-  | Label(_) =>
-    // TODO Remove duplication in cases
-    Typ.eq(t1, t2)
-      ? d
-      : {
-        let d' =
-          DHExp.Cast(d, t1, Typ.temp(Unknown(Internal)))
-          |> DHExp.fresh
-          |> Casts.transition_multiple;
-        DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2)
+let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => {
+  Typ.eq(t1, t2)
+    ? d
+    : {
+      let d' =
+        DHExp.Cast(d, t1, Typ.temp(Unknown(Internal)))
         |> DHExp.fresh
         |> Casts.transition_multiple;
-      } // These should be a different sort. I don't think we should be casting them.
-  | _ =>
-    switch (t2.term) {
-    | Prod([{term: TupLabel({term: Label(l), _}, t), _}]) =>
-      switch (t1.term) {
-      | Prod([{term: TupLabel({term: Label(l'), _}, _), _}]) when l == l' =>
-        Typ.eq(t1, t2)
-          ? d
-          : {
-            let d' =
-              DHExp.Cast(d, t1, Typ.temp(Unknown(Internal)))
-              |> DHExp.fresh
-              |> Casts.transition_multiple;
-            DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2)
-            |> DHExp.fresh
-            |> Casts.transition_multiple;
-          }
-      | _ =>
-        Tuple([
-          TupLabel(Label(l) |> DHExp.fresh, fresh_cast(d, t1, t))
-          |> DHExp.fresh,
-        ])
-        |> DHExp.fresh
-      }
-    | _ =>
-      // TODO Remove duplication in cases
-      Typ.eq(t1, t2)
-        ? d
-        : {
-          let d' =
-            DHExp.Cast(d, t1, Typ.temp(Unknown(Internal)))
-            |> DHExp.fresh
-            |> Casts.transition_multiple;
-          DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2)
-          |> DHExp.fresh
-          |> Casts.transition_multiple;
-        }
-    }
-  };
+      DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2)
+      |> DHExp.fresh
+      |> Casts.transition_multiple;
+    };
 };
 
 let fresh_pat_cast = (p: DHPat.t, t1: Typ.t, t2: Typ.t): DHPat.t => {

diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -226,6 +226,7 @@ and uexp_to_info_map =
     );
   let go_pat = upat_to_info_map(~ctx, ~ancestors);
   let elaborate_singleton_tuple = (uexp: Exp.t, inner_ty, l, m) => {
+    print_endline("Elaborating singleton tuple");
     let (term, rewrap) = UExp.unwrap(uexp);
     let original_expression = Exp.fresh(term);
     let (original_info, m) =
@@ -484,11 +485,12 @@ and uexp_to_info_map =
             copied: arg.copied,
           };
           arg;
-        | (TupLabel(_), Prod([{term: TupLabel(_), _}])) =>
-          Tuple([arg]) |> Exp.fresh
-        | (_, Prod([{term: TupLabel({term: Label(name), _}, _), _}])) =>
-          Tuple([TupLabel(Label(name) |> Exp.fresh, arg) |> Exp.fresh])
-          |> Exp.fresh
+        // Now doing the singleton label elaboration below. I'll discuss with Anthony before removing these
+        // | (TupLabel(_), Prod([{term: TupLabel(_), _}])) =>
+        //   Tuple([arg]) |> Exp.fresh
+        // | (_, Prod([{term: TupLabel({term: Label(name), _}, _), _}])) =>
+        //   Tuple([TupLabel(Label(name) |> Exp.fresh, arg) |> Exp.fresh])
+        //   |> Exp.fresh
         | (_, _) => arg
         };
       let (arg, m) = go(~mode=Ana(ty_in), arg, m);

diff --git a/test/Test_Statics.re b/test/Test_Statics.re
@@ -627,4 +627,54 @@ let tests =
       ),
       parse_exp({|let x : (a=b=c=?) = b=? in x|}),
     ),
+    fully_consistent_typecheck(
+      "Singleton labeled argument function application with unknown type",
+      {|(fun a=x->x)(a=1)|},
+      Some(unknown(Internal)),
+      Ap(
+        Forward,
+        Fun(
+          Tuple([
+            TupLabel(Label("a") |> Pat.fresh, Var("x") |> Pat.fresh)
+            |> Pat.fresh,
+          ])
+          |> Pat.fresh,
+          Var("x") |> Exp.fresh,
+          None,
+          None,
+        )
+        |> Exp.fresh,
+        Tuple([
+          TupLabel(Label("a") |> Exp.fresh, Int(1) |> Exp.fresh)
+          |> Exp.fresh,
+        ])
+        |> Exp.fresh,
+      )
+      |> Exp.fresh,
+    ),
+    fully_consistent_typecheck(
+      "Singleton labeled argument function application with no labeled param",
+      {|(fun a=x->x)(1)|},
+      Some(int),
+      Ap(
+        Forward,
+        Fun(
+          Tuple([
+            TupLabel(Label("a") |> Pat.fresh, Var("x") |> Pat.fresh)
+            |> Pat.fresh,
+          ])
+          |> Pat.fresh,
+          Var("x") |> Exp.fresh,
+          None,
+          None,
+        )
+        |> Exp.fresh,
+        Tuple([
+          TupLabel(Label("a") |> Exp.fresh, Int(1) |> Exp.fresh)
+          |> Exp.fresh,
+        ])
+        |> Exp.fresh,
+      )
+      |> Exp.fresh,
+    ),
   ];