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);