add negative test

test/Compilation.hs

@@ -1,7 +1,8 @@
 module Compilation where
 
 import Base
+import Compilation.Negative qualified as N
 import Compilation.Positive qualified as P
 
 allTests :: TestTree
-allTests = testGroup "Juvix compilation pipeline tests" [P.allTests]
+allTests = testGroup "Juvix compilation pipeline tests" [P.allTests, N.allTests]

test/Compilation/Base.hs

@@ -36,3 +36,16 @@ compileAssertion mode mainFile expectedFile step = do
         EvalOnly -> evalAssertion
         CompileOnly stdinText -> compileAssertion' stdinText
         EvalAndCompile -> evalAssertion >> compileAssertion' ""
+
+compileErrorAssertion ::
+  Path Abs File ->
+  (String -> IO ()) ->
+  Assertion
+compileErrorAssertion mainFile step = do
+  step "Translate to JuvixCore"
+  cwd <- getCurrentDir
+  let entryPoint = defaultEntryPoint cwd mainFile
+  tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toEval' tab of
+    Left _ -> assertBool "" True
+    Right _ -> assertFailure "no error"

test/Compilation/Negative.hs

@@ -0,0 +1,37 @@
+module Compilation.Negative where
+
+import Base
+import Compilation.Base
+
+data NegTest = NegTest
+  { _name :: String,
+    _relDir :: Path Rel Dir,
+    _file :: Path Rel File
+  }
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Compilation/negative")
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} =
+  let tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ compileErrorAssertion file'
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Juvix compilation pipeline negative tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [NegTest]
+tests =
+  [ NegTest
+      "Pattern matching coverage"
+      $(mkRelDir ".")
+      $(mkRelFile "test001.juvix")
+  ]

tests/Compilation/negative/test001.juvix

@@ -0,0 +1,14 @@
+-- pattern matching coverage
+module test001;
+
+open import Stdlib.Prelude;
+
+f : List Nat -> List Nat -> Nat;
+f (x :: xs) (y :: ys) := x + y;
+f _ (_ :: (z :: zs)) := z;
+f _ nil := 0;
+
+main : Nat;
+main := f (1 :: nil) (2 :: nil);
+
+end;