adapt arity tests

anoma · Nov 28, 2023 · 361503b · 361503b
1 parent ff8e7c3
commit 361503b
Show file tree

Hide file tree

Showing 6 changed files with 101 additions and 9 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -955,7 +955,7 @@ viewInductiveApp ty = do
       case r of
         Just h' -> viewInductiveApp h'
         Nothing -> return (Left h)
-    _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty))
+    _ -> throw (ErrInvalidPatternMatching (InvalidPatternMatching ty))
   where
     viewTypeApp :: Expression -> (Expression, [Expression])
     viewTypeApp tyapp = case tyapp of

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -1369,7 +1369,7 @@ viewInductiveApp ty = do
       case r of
         Just h' -> viewInductiveApp h'
         Nothing -> return (Left h)
-    _ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty))
+    _ -> throw (ErrInvalidPatternMatching (InvalidPatternMatching ty))
   where
     viewTypeApp :: Expression -> (Expression, [Expression])
     viewTypeApp tyapp = case tyapp of

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
@@ -20,7 +20,7 @@ data TypeCheckerError
   | ErrExpectedFunctionType ExpectedFunctionType
   | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
   | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
-  | ErrImpracticalPatternMatching ImpracticalPatternMatching
+  | ErrInvalidPatternMatching InvalidPatternMatching
   | ErrNoPositivity NoPositivity
   | ErrUnsupportedTypeFunction UnsupportedTypeFunction
   | ErrInvalidInstanceType InvalidInstanceType
@@ -48,7 +48,7 @@ instance ToGenericError TypeCheckerError where
     ErrExpectedFunctionType e -> genericError e
     ErrTooManyArgumentsIndType e -> genericError e
     ErrTooFewArgumentsIndType e -> genericError e
-    ErrImpracticalPatternMatching e -> genericError e
+    ErrInvalidPatternMatching e -> genericError e
     ErrNoPositivity e -> genericError e
     ErrUnsupportedTypeFunction e -> genericError e
     ErrInvalidInstanceType e -> genericError e

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -281,13 +281,13 @@ instance ToGenericError WrongNumberArgumentsIndType where
                   )
               <+> "given"
 
-newtype ImpracticalPatternMatching = ImpracticalPatternMatching
+newtype InvalidPatternMatching = InvalidPatternMatching
   { _impracticalPatternMatchingType :: Expression
   }
 
-makeLenses ''ImpracticalPatternMatching
+makeLenses ''InvalidPatternMatching
 
-instance ToGenericError ImpracticalPatternMatching where
+instance ToGenericError InvalidPatternMatching where
   genericError e = ask >>= generr
     where
       generr opts =

diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs
@@ -1,4 +1,4 @@
-module Arity.Negative (allTests) where
+module Arity.Negative where
 
 import Base
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error

diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
@@ -46,7 +46,10 @@ allTests =
         (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)),
       testGroup
         "Non-strictly positive data types"
-        (map (mkTest . testDescr) Old.negPositivityTests)
+        (map (mkTest . testDescr) Old.negPositivityTests),
+      testGroup
+        "Arity tests"
+        (map (mkTest . testDescr) arityTests)
     ]
 
 isIgnored :: Old.NegTest -> Bool
@@ -56,3 +59,92 @@ ignored :: HashSet String
 ignored =
   HashSet.fromList
     []
+
+wrongError :: Maybe FailMsg
+wrongError = Just "Incorrect error"
+
+negArityTest :: String -> Path Rel Dir -> Path Rel File -> (ArityCheckerError -> Maybe FailMsg) -> Old.NegTest
+negArityTest _name rdir rfile ariErr =
+  let _dir = root <//> rdir
+   in Old.NegTest
+        { _file = _dir <//> rfile,
+          _checkErr = \case
+            ErrArityCheckerError e -> ariErr e
+            _ -> wrongError,
+          _name,
+          _dir
+        }
+
+arityTests :: [Old.NegTest]
+arityTests =
+  [ negTest
+      "Too many arguments in expression"
+      $(mkRelDir "Internal")
+      $(mkRelFile "TooManyArguments.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Pattern match a function type"
+      $(mkRelDir "Internal")
+      $(mkRelFile "FunctionPattern.juvix")
+      $ \case
+        ErrInvalidPatternMatching {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Function type (* → *) application"
+      $(mkRelDir "Internal")
+      $(mkRelFile "FunctionApplied.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Expected explicit pattern"
+      $(mkRelDir "Internal")
+      $(mkRelFile "ExpectedExplicitPattern.juvix")
+      $ \case
+        ErrWrongPatternIsImplicit {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Expected explicit argument"
+      $(mkRelDir "Internal")
+      $(mkRelFile "ExpectedExplicitArgument.juvix")
+      $ \case
+        ErrExpectedExplicitArgument {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Function clause with two many patterns in the lhs"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LhsTooManyPatterns.juvix")
+      $ \case
+        ErrLhsTooManyPatterns {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Too many arguments for the return type of a constructor"
+      $(mkRelDir "Internal")
+      $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Lazy builtin not fully applied"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LazyBuiltin.juvix")
+      $ \case
+        ErrBuiltinNotFullyApplied {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "issue 2293: Non-terminating function with arity error"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue2293.juvix")
+      $ \case
+        ErrWrongConstructorAppLength {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Detect default argument cycle in the arity checker"
+      $(mkRelDir "Internal")
+      $(mkRelFile "DefaultArgCycleArity.juvix")
+      $ \case
+        ErrDefaultArgLoop {} -> Nothing
+        _ -> wrongError
+  ]