add tests

src/Juvix/Compiler/Internal/Language.hs

@@ -669,7 +669,7 @@ instance HasLoc CaseBranch where
   getLoc c = getLoc (c ^. caseBranchPattern) <> getLoc (c ^. caseBranchRhs)
 
 instance HasLoc Case where
-  getLoc c = getLoc (c ^. caseExpression) <> getLocSpan (c ^. caseBranches)
+  getLoc c = getLocSpan (c ^. caseBranches)
 
 instance HasLoc Expression where
   getLoc = \case

test/Compilation/Negative.hs

@@ -53,5 +53,9 @@ tests =
     NegTest
       "Test006: Ill scoped term (This is a bug. It should be positive)"
       $(mkRelDir ".")
-      $(mkRelFile "test006.juvix")
+      $(mkRelFile "test006.juvix"),
+    NegTest
+      "Test007: Pattern matching coverage with side conditions"
+      $(mkRelDir ".")
+      $(mkRelFile "test007.juvix")
   ]

tests/Compilation/negative/test007.juvix

@@ -0,0 +1,10 @@
+module test007;
+
+import Stdlib.Prelude open;
+
+f (x : List Nat) : Nat :=
+  case x of
+    | nil := 0
+    | x :: _ if true := x;
+
+main : Nat := f (1 :: 2 :: nil);

tests/Compilation/positive/out/test035.out

@@ -7,3 +7,8 @@
 13536
 1
 0
+1
+0
+4
+9
+0

tests/Compilation/positive/test035.juvix

@@ -40,6 +40,14 @@ h : Nat -> Nat
   | (suc (suc (suc (suc n)))) := n
   | _ := 0;
 
+hh (x : Nat) : Nat :=
+  case x of
+  | zero := 1
+  | (suc n) if h n == 0 := n
+  | (suc zero) := 17
+  | (suc (suc (suc (suc (suc (suc zero)))))) := 9
+  | _ := 0;
+
 printListNatLn : List Nat → IO
   | nil := printStringLn "nil"
   | (x :: xs) :=
@@ -54,4 +62,9 @@ main : IO :=
     >>> printNatLn (f (gen 18))
     >>> printNatLn (f (gen 20))
     >>> printNatLn (h 5)
-    >>> printNatLn (h 3);
+    >>> printNatLn (h 3)
+    >>> printNatLn (hh 0)
+    >>> printNatLn (hh 1)
+    >>> printNatLn (hh 5)
+    >>> printNatLn (hh 6)
+    >>> printNatLn (hh 7);