2022-09-23 16:43:18 +03:00
|
|
|
module Typecheck.Negative where
|
2022-03-29 20:01:19 +03:00
|
|
|
|
|
|
|
import Base
|
2022-11-07 16:47:56 +03:00
|
|
|
import Juvix.Compiler.Builtins (iniState)
|
2022-08-03 14:20:40 +03:00
|
|
|
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
|
|
|
|
import Juvix.Compiler.Pipeline
|
2022-03-29 20:01:19 +03:00
|
|
|
|
|
|
|
type FailMsg = String
|
|
|
|
|
|
|
|
data NegTest = NegTest
|
2022-04-07 19:10:53 +03:00
|
|
|
{ _name :: String,
|
2022-12-20 15:05:40 +03:00
|
|
|
_relDir :: Path Rel Dir,
|
|
|
|
_file :: Path Rel File,
|
2022-04-22 11:06:34 +03:00
|
|
|
_checkErr :: TypeCheckerError -> Maybe FailMsg
|
2022-04-05 20:57:21 +03:00
|
|
|
}
|
2022-04-01 14:00:15 +03:00
|
|
|
|
2022-03-29 20:01:19 +03:00
|
|
|
testDescr :: NegTest -> TestDescr
|
2022-04-05 20:57:21 +03:00
|
|
|
testDescr NegTest {..} =
|
2022-12-20 15:05:40 +03:00
|
|
|
let tRoot = root <//> _relDir
|
|
|
|
file' = tRoot <//> _file
|
2022-04-07 19:10:53 +03:00
|
|
|
in TestDescr
|
|
|
|
{ _testName = _name,
|
|
|
|
_testRoot = tRoot,
|
|
|
|
_testAssertion = Single $ do
|
2022-12-20 15:05:40 +03:00
|
|
|
let entryPoint = defaultEntryPoint tRoot file'
|
2022-11-07 16:47:56 +03:00
|
|
|
result <- runIOEither iniState entryPoint upToInternalTyped
|
2022-07-08 14:59:45 +03:00
|
|
|
case mapLeft fromJuvixError result of
|
2022-05-26 18:52:08 +03:00
|
|
|
Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
|
2023-01-17 11:41:07 +03:00
|
|
|
Left Nothing -> assertFailure "An error ocurred but it was not in the type checker."
|
|
|
|
Right _ -> assertFailure "The type checker did not find an error."
|
2022-04-07 19:10:53 +03:00
|
|
|
}
|
2022-03-29 20:01:19 +03:00
|
|
|
|
|
|
|
allTests :: TestTree
|
2022-04-05 20:57:21 +03:00
|
|
|
allTests =
|
|
|
|
testGroup
|
2022-07-23 10:27:12 +03:00
|
|
|
"Typecheck negative tests"
|
|
|
|
[ testGroup
|
|
|
|
"General typechecking errors"
|
|
|
|
(map (mkTest . testDescr) tests),
|
|
|
|
testGroup
|
|
|
|
"Non-strictly positive data types"
|
|
|
|
(map (mkTest . testDescr) negPositivityTests)
|
|
|
|
]
|
2022-03-29 20:01:19 +03:00
|
|
|
|
2022-12-20 15:05:40 +03:00
|
|
|
root :: Path Abs Dir
|
|
|
|
root = relToProject $(mkRelDir "tests/negative")
|
2022-03-29 20:01:19 +03:00
|
|
|
|
|
|
|
wrongError :: Maybe FailMsg
|
|
|
|
wrongError = Just "Incorrect error"
|
|
|
|
|
|
|
|
tests :: [NegTest]
|
2022-04-05 20:57:21 +03:00
|
|
|
tests =
|
|
|
|
[ NegTest
|
|
|
|
"Constructor in pattern type error"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "PatternConstructor.juvix")
|
2022-04-05 20:57:21 +03:00
|
|
|
$ \case
|
2022-04-22 11:06:34 +03:00
|
|
|
ErrWrongConstructorType {} -> Nothing
|
2022-04-05 20:57:21 +03:00
|
|
|
_ -> wrongError,
|
2022-07-15 18:57:04 +03:00
|
|
|
NegTest
|
|
|
|
"Check pattern with hole type"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "265")
|
|
|
|
$(mkRelFile "M.juvix")
|
2022-07-15 18:57:04 +03:00
|
|
|
$ \case
|
|
|
|
ErrWrongConstructorType {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-04-05 20:57:21 +03:00
|
|
|
NegTest
|
|
|
|
"Type vs inferred type mismatch"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "WrongType.juvix")
|
2022-04-05 20:57:21 +03:00
|
|
|
$ \case
|
2022-04-22 11:06:34 +03:00
|
|
|
ErrWrongType {} -> Nothing
|
2022-04-05 20:57:21 +03:00
|
|
|
_ -> wrongError,
|
|
|
|
NegTest
|
|
|
|
"Function application with non-function type"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "ExpectedFunctionType.juvix")
|
2022-04-05 20:57:21 +03:00
|
|
|
$ \case
|
2022-04-22 11:06:34 +03:00
|
|
|
ErrExpectedFunctionType {} -> Nothing
|
2022-04-05 20:57:21 +03:00
|
|
|
_ -> wrongError,
|
2022-06-02 14:02:07 +03:00
|
|
|
NegTest
|
|
|
|
"Unsolved hole"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "UnsolvedMeta.juvix")
|
2022-06-02 14:02:07 +03:00
|
|
|
$ \case
|
|
|
|
ErrUnsolvedMeta {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-04-05 20:57:21 +03:00
|
|
|
NegTest
|
|
|
|
"Multiple type errors are captured"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "MultiWrongType.juvix")
|
2022-04-05 20:57:21 +03:00
|
|
|
$ \case
|
2022-04-22 11:06:34 +03:00
|
|
|
ErrWrongType {} -> Nothing
|
2022-06-21 18:53:35 +03:00
|
|
|
_ -> wrongError,
|
2022-07-20 11:33:52 +03:00
|
|
|
NegTest
|
|
|
|
"Unexpected braces in pattern"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "issue1337")
|
|
|
|
$(mkRelFile "Braces.juvix")
|
2022-07-20 11:33:52 +03:00
|
|
|
$ \case
|
|
|
|
ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-06-21 18:53:35 +03:00
|
|
|
NegTest
|
|
|
|
"Wrong return type name for a constructor of a simple data type"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "WrongReturnType.juvix")
|
2022-06-21 18:53:35 +03:00
|
|
|
$ \case
|
|
|
|
ErrWrongReturnType {} -> Nothing
|
|
|
|
_ -> wrongError,
|
|
|
|
NegTest
|
2022-06-22 12:42:59 +03:00
|
|
|
"Too few arguments for the return type of a constructor"
|
2022-12-20 15:05:40 +03:00
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "WrongReturnTypeTooFewArguments.juvix")
|
2022-06-21 18:53:35 +03:00
|
|
|
$ \case
|
2022-07-25 13:30:18 +03:00
|
|
|
ErrWrongType {} -> Nothing
|
2022-06-22 12:42:59 +03:00
|
|
|
_ -> wrongError,
|
2023-01-09 20:56:28 +03:00
|
|
|
NegTest
|
|
|
|
"Ambiguous hole"
|
|
|
|
$(mkRelDir "Internal")
|
|
|
|
$(mkRelFile "IdenFunctionArgsNoExplicit.juvix")
|
|
|
|
$ \case
|
|
|
|
ErrUnsolvedMeta {} -> Nothing
|
2022-04-05 20:57:21 +03:00
|
|
|
_ -> wrongError
|
|
|
|
]
|
2022-07-23 10:27:12 +03:00
|
|
|
|
|
|
|
negPositivityTests :: [NegTest]
|
|
|
|
negPositivityTests =
|
2022-12-20 15:05:40 +03:00
|
|
|
[ NegTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError,
|
2022-12-20 15:05:40 +03:00
|
|
|
NegTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $
|
2022-07-23 10:27:12 +03:00
|
|
|
\case
|
|
|
|
ErrNoPositivity {} -> Nothing
|
|
|
|
_ -> wrongError
|
|
|
|
]
|