From e09511d50fa168436d7bd2921cd142897db796ff Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 5 Sep 2024 14:21:36 +0200
Subject: [PATCH] add tests

---
 src/Juvix/Compiler/Internal/Language.hs    |  2 +-
 test/Compilation/Negative.hs               |  6 +++++-
 tests/Compilation/negative/test007.juvix   | 10 ++++++++++
 tests/Compilation/positive/out/test035.out |  5 +++++
 tests/Compilation/positive/test035.juvix   | 15 ++++++++++++++-
 5 files changed, 35 insertions(+), 3 deletions(-)
 create mode 100644 tests/Compilation/negative/test007.juvix

diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index ce43ab97c7..662c691513 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/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
diff --git a/test/Compilation/Negative.hs b/test/Compilation/Negative.hs
index c6fbf1f57a..afbc4b2c63 100644
--- a/test/Compilation/Negative.hs
+++ b/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")
   ]
diff --git a/tests/Compilation/negative/test007.juvix b/tests/Compilation/negative/test007.juvix
new file mode 100644
index 0000000000..7235242512
--- /dev/null
+++ b/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);
diff --git a/tests/Compilation/positive/out/test035.out b/tests/Compilation/positive/out/test035.out
index 80257c93d2..a420b9e14c 100644
--- a/tests/Compilation/positive/out/test035.out
+++ b/tests/Compilation/positive/out/test035.out
@@ -7,3 +7,8 @@
 13536
 1
 0
+1
+0
+4
+9
+0
diff --git a/tests/Compilation/positive/test035.juvix b/tests/Compilation/positive/test035.juvix
index 463330ce92..30bd483f0d 100644
--- a/tests/Compilation/positive/test035.juvix
+++ b/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);