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

hazelgrove · Oct 3, 2024 · 50440ea · 50440ea
1 parent 9e5570a
commit 50440ea
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 9 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -350,12 +350,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
           ((arg, _)) => Exp.is_deferral(arg),
           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/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
@@ -333,7 +333,6 @@ module Transition = (EV: EV_MODE) => {
         );
       Constructor;
     | Ap(dir, d1, d2) =>
-      // TODO I don't know why this needs to be final
       let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap)
       and. d1' =
         req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1)
@@ -433,7 +432,11 @@ module Transition = (EV: EV_MODE) => {
         });
       | Cast(_)
       | FailedCast(_) => Indet
-      | FixF(_) => failwith("FixF in Ap")
+      | FixF(_) =>
+        print_endline(Exp.show(d1));
+        print_endline(Exp.show(d1'));
+        print_endline("FIXF");
+        failwith("FixF in Ap");
       | _ =>
         Step({
           expr: {

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,
+  ),
 ];