Add elavorator and evaluator tests for deferral applied to a hole

hazelgrove · Oct 3, 2024 · 8d4ead1 · 8d4ead1
1 parent ab9f981
commit 8d4ead1
Show file tree

Hide file tree

Showing 2 changed files with 198 additions and 0 deletions.
diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
@@ -237,6 +237,88 @@ let ap_deferral_single_argument = () =>
     ),
   );
 
+let ap_of_deferral_of_hole = () =>
+  alco_check(
+    "?(_, _, 3)(1., true)",
+    Ap(
+      Forward,
+      DeferredAp(
+        Cast(
+          Cast(
+            EmptyHole |> Exp.fresh,
+            Unknown(Internal) |> Typ.fresh,
+            Arrow(
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            )
+            |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Arrow(
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+          Arrow(
+            Prod([
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            ])
+            |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        [
+          Deferral(InAp) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+          Cast(
+            Int(3) |> Exp.fresh,
+            Int |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+      Tuple([
+        Cast(
+          Float(1.) |> Exp.fresh,
+          Float |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Bool(true) |> Exp.fresh,
+          Bool |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    dhexp_of_uexp(
+      Ap(
+        Forward,
+        DeferredAp(
+          EmptyHole |> Exp.fresh,
+          [
+            Deferral(InAp) |> Exp.fresh,
+            Deferral(InAp) |> Exp.fresh,
+            Int(3) |> Exp.fresh,
+          ],
+        )
+        |> Exp.fresh,
+        Tuple([Float(1.) |> Exp.fresh, Bool(true) |> Exp.fresh])
+        |> Exp.fresh,
+      )
+      |> Exp.fresh,
+    ),
+  );
+
 let elaboration_tests = [
   test_case("Single integer", `Quick, single_integer),
   test_case("Empty hole", `Quick, empty_hole),
@@ -258,4 +340,9 @@ let elaboration_tests = [
     `Quick,
     ap_deferral_single_argument,
   ),
+  test_case(
+    "Function application with a deferral of a hole",
+    `Quick,
+    ap_of_deferral_of_hole,
+  ),
 ];
diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re
@@ -50,9 +50,120 @@ let test_function_deferral = () =>
     |> Exp.fresh,
   );
 
+let tet_ap_of_hole_deferral = () =>
+  evaluation_test(
+    "?(_, _, 3)(1., true)",
+    Ap(
+      Forward,
+      Cast(
+        EmptyHole |> Exp.fresh,
+        Unknown(Internal) |> Typ.fresh,
+        Arrow(
+          Unknown(Internal) |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Typ.fresh,
+      )
+      |> Exp.fresh,
+      Cast(
+        Tuple([
+          Cast(
+            Float(1.) |> Exp.fresh,
+            Float |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Cast(
+            Bool(true) |> Exp.fresh,
+            Bool |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Cast(
+            Int(3) |> Exp.fresh,
+            Int |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+        ])
+        |> Exp.fresh,
+        Prod([
+          Unknown(Internal) |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        ])
+        |> Typ.fresh,
+        Unknown(Internal) |> Typ.fresh,
+      )
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+    Ap(
+      Forward,
+      DeferredAp(
+        Cast(
+          Cast(
+            EmptyHole |> Exp.fresh,
+            Unknown(Internal) |> Typ.fresh,
+            Arrow(
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            )
+            |> Typ.fresh,
+          )
+          |> Exp.fresh,
+          Arrow(
+            Unknown(Internal) |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+          Arrow(
+            Prod([
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+              Unknown(Internal) |> Typ.fresh,
+            ])
+            |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        [
+          Deferral(InAp) |> Exp.fresh,
+          Deferral(InAp) |> Exp.fresh,
+          Cast(
+            Int(3) |> Exp.fresh,
+            Int |> Typ.fresh,
+            Unknown(Internal) |> Typ.fresh,
+          )
+          |> Exp.fresh,
+        ],
+      )
+      |> Exp.fresh,
+      Tuple([
+        Cast(
+          Float(1.) |> Exp.fresh,
+          Float |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+        Cast(
+          Bool(true) |> Exp.fresh,
+          Bool |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Exp.fresh,
+      ])
+      |> Exp.fresh,
+    )
+    |> Exp.fresh,
+  );
+
 let tests = [
   test_case("Integer literal", `Quick, test_int),
   test_case("Integer sum", `Quick, test_sum),
   test_case("Function application", `Quick, test_function_application),
   test_case("Function deferral", `Quick, test_function_deferral),
+  test_case("Deferral applied to hole", `Quick, tet_ap_of_hole_deferral),
 ];