Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Negative tests for --new-typechecker #2532

Merged
merged 5 commits into from
Nov 28, 2023
Merged

Negative tests for --new-typechecker #2532

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
3f1a40c
add all old tests
janmasrovira Nov 22, 2023
9af4b66
wip
janmasrovira Nov 24, 2023
7748e87
adapt arity tests
janmasrovira Nov 24, 2023
aa05a77
fix negative tests
janmasrovira Nov 24, 2023
df59054
ormolu
janmasrovira Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -538,7 +538,7 @@ matchIsImplicit expected actual =
unless
(expected == actual ^. patternArgIsImplicit)
( throw
( ErrArity
( ErrArityCheckerError
( ErrWrongPatternIsImplicit
WrongPatternIsImplicit
{ _wrongPatternIsImplicitExpected = expected,
Expand Down Expand Up @@ -629,7 +629,7 @@ checkPattern = go
return app {_constrAppType = Just appTy, _constrAppParameters = pis}
appErr :: ConstructorApp -> Int -> TypeCheckerError
appErr app expected =
ErrArity
ErrArityCheckerError
( ErrWrongConstructorAppLength
( WrongConstructorAppLength
{ _wrongConstructorAppLength = app,
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -652,7 +652,7 @@ matchIsImplicit expected actual =
unless
(expected == actual ^. patternArgIsImplicit)
. throw
. ErrArity
. ErrArityCheckerError
$ ErrWrongPatternIsImplicit
WrongPatternIsImplicit
{ _wrongPatternIsImplicitExpected = expected,
Expand Down Expand Up @@ -745,7 +745,7 @@ checkPattern = go

appErr :: ConstructorApp -> Int -> TypeCheckerError
appErr app expected =
ErrArity
ErrArityCheckerError
( ErrWrongConstructorAppLength
( WrongConstructorAppLength
{ _wrongConstructorAppLength = app,
Expand Down Expand Up @@ -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
Expand Down
33 changes: 29 additions & 4 deletions src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,17 +10,17 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.E
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types
import Juvix.Prelude
import Prelude (show)

data TypeCheckerError
= ErrWrongConstructorType WrongConstructorType
| ErrWrongReturnType WrongReturnType
| ErrArity ArityCheckerError
| ErrWrongType WrongType
| ErrUnsolvedMeta UnsolvedMeta
| ErrExpectedFunctionType ExpectedFunctionType
| ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
| ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
| ErrImpracticalPatternMatching ImpracticalPatternMatching
| ErrInvalidPatternMatching InvalidPatternMatching
| ErrNoPositivity NoPositivity
| ErrUnsupportedTypeFunction UnsupportedTypeFunction
| ErrInvalidInstanceType InvalidInstanceType
Expand All @@ -42,13 +42,12 @@ instance ToGenericError TypeCheckerError where
genericError = \case
ErrWrongConstructorType e -> genericError e
ErrWrongReturnType e -> genericError e
ErrArity e -> genericError e
ErrWrongType e -> genericError e
ErrUnsolvedMeta e -> genericError e
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
Expand All @@ -64,3 +63,29 @@ instance ToGenericError TypeCheckerError where
ErrTraitNotTerminating e -> genericError e
ErrArityCheckerError e -> genericError e
ErrDefaultArgLoop e -> genericError e

instance Show TypeCheckerError where
show = \case
ErrWrongConstructorType {} -> "ErrWrongConstructorType"
ErrWrongReturnType {} -> "ErrWrongReturnType"
ErrWrongType {} -> "ErrWrongType"
ErrUnsolvedMeta {} -> "ErrUnsolvedMeta"
ErrExpectedFunctionType {} -> "ErrExpectedFunctionType"
ErrTooManyArgumentsIndType {} -> "ErrTooManyArgumentsIndType"
ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType"
ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching"
ErrNoPositivity {} -> "ErrNoPositivity"
ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction"
ErrInvalidInstanceType {} -> "ErrInvalidInstanceType"
ErrInvalidCoercionType {} -> "ErrInvalidCoercionType"
ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument"
ErrCoercionCycles {} -> "ErrCoercionCycles"
ErrTargetNotATrait {} -> "ErrTargetNotATrait"
ErrNotATrait {} -> "ErrNotATrait"
ErrNoInstance {} -> "ErrNoInstance"
ErrAmbiguousInstances {} -> "ErrAmbiguousInstances"
ErrSubsumedInstance {} -> "ErrSubsumedInstance"
ErrExplicitInstanceArgument {} -> "ErrExplicitInstanceArgument"
ErrTraitNotTerminating {} -> "ErrTraitNotTerminating"
ErrArityCheckerError {} -> "ErrArityCheckerError"
ErrDefaultArgLoop {} -> "ErrDefaultArgLoop"
6 changes: 3 additions & 3 deletions src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion test/Arity/Negative.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
module Arity.Negative (allTests) where
module Arity.Negative where

import Base
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
Expand Down
3 changes: 2 additions & 1 deletion test/Typecheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,9 @@ module Typecheck (allTests) where

import Base
import Typecheck.Negative qualified as N
import Typecheck.NegativeNew qualified as NewNeg
import Typecheck.Positive qualified as P
import Typecheck.PositiveNew qualified as New

allTests :: TestTree
allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests]
allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests, NewNeg.allTests]
Loading