eval test for match side-conditions

anoma · Jan 30, 2025 · 7cfa465 · 7cfa465
1 parent 9a37076
commit 7cfa465
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 6 deletions.
diff --git a/test/Core/Eval/Negative.hs b/test/Core/Eval/Negative.hs
@@ -65,9 +65,5 @@ tests =
     NegTest
       "Erroneous Church numerals"
       $(mkRelDir ".")
-      $(mkRelFile "test009.jvc"),
-    NegTest
-      "Empty letrec"
-      $(mkRelDir ".")
-      $(mkRelFile "test010.jvc")
+      $(mkRelFile "test009.jvc")
   ]
diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
@@ -367,5 +367,10 @@ tests =
       "Test065: Let / LetRec type inference"
       $(mkRelDir ".")
       $(mkRelFile "test065.jvc")
-      $(mkRelFile "out/test065.out")
+      $(mkRelFile "out/test065.out"),
+    PosTest
+      "Test066: Match side-conditions"
+      $(mkRelDir ".")
+      $(mkRelFile "test066.jvc")
+      $(mkRelFile "out/test066.out")
   ]
diff --git a/tests/Core/positive/out/test066.out b/tests/Core/positive/out/test066.out
@@ -0,0 +1 @@
+8
diff --git a/tests/Core/positive/test066.jvc b/tests/Core/positive/test066.jvc
@@ -0,0 +1,17 @@
+type Unit {
+  unit : Unit;
+};
+
+type Box {
+  box : Any -> Box;
+};
+
+def f := \x
+  match box 9, x, unit with {
+    box z, box y, unit if y < z := 1;
+    box z, box y, unit if y = z + 1 := 0;
+    box z, box y, unit if y > z := 10;
+    _, _, _ := 11;
+  };
+
+3 * f (box 11) * f (box 7) - f (box 10) - 2 * f (box 9)