Fix function deferral for when there's a single remaining argument

hazelgrove · Oct 2, 2024 · b277846 · b277846
1 parent 4a8d817
commit b277846
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 6 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -351,11 +351,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
           List.combine(args, ty_fargs),
         );
       // TODO Should this be a product in the singleton case or not
-      // let remaining_arg_ty =
-      //   List.length(remaining_args) == 1
-      //     ? snd(List.hd(remaining_args))
-      //     : Prod(List.map(snd, remaining_args)) |> Typ.temp;
-      let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp;
+      let remaining_arg_ty =
+        List.length(remaining_args) == 1
+          ? snd(List.hd(remaining_args))
+          : Prod(List.map(snd, remaining_args)) |> Typ.temp;
       DeferredAp(f'', args'')
       |> rewrap
       |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp);

diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
@@ -180,6 +180,15 @@ let let_fun = () =>
 let deferral = () =>
   alco_check(
     "string_sub(\"hello\", 1, _)",
+    DeferredAp(
+      Var("string_sub") |> Exp.fresh,
+      [
+        String("hello") |> Exp.fresh,
+        Int(1) |> Exp.fresh,
+        Deferral(InAp) |> Exp.fresh,
+      ],
+    )
+    |> Exp.fresh,
     dhexp_of_uexp(
       DeferredAp(
         Var("string_sub") |> Exp.fresh,
@@ -191,7 +200,13 @@ let deferral = () =>
       )
       |> Exp.fresh,
     ),
-    dhexp_of_uexp(
+  );
+
+let ap_deferral_single_argument = () =>
+  alco_check(
+    "string_sub(\"hello\", 1, _)(2)",
+    Ap(
+      Forward,
       DeferredAp(
         Var("string_sub") |> Exp.fresh,
         [
@@ -201,6 +216,24 @@ let deferral = () =>
         ],
       )
       |> Exp.fresh,
+      Int(2) |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    dhexp_of_uexp(
+      Ap(
+        Forward,
+        DeferredAp(
+          Var("string_sub") |> Exp.fresh,
+          [
+            String("hello") |> Exp.fresh,
+            Int(1) |> Exp.fresh,
+            Deferral(InAp) |> Exp.fresh,
+          ],
+        )
+        |> Exp.fresh,
+        Int(2) |> Exp.fresh,
+      )
+      |> Exp.fresh,
     ),
   );
 
@@ -220,4 +253,9 @@ let elaboration_tests = [
     `Quick,
     deferral,
   ),
+  test_case(
+    "Function application with a single remaining argument after deferral",
+    `Quick,
+    ap_deferral_single_argument,
+  ),
 ];