1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-04 06:23:13 +03:00

w.i.p Fixing test suite

This commit is contained in:
Jonathan Prieto-Cubides 2022-04-07 18:10:53 +02:00
parent 4c58b82588
commit beb2556111
17 changed files with 194 additions and 126 deletions

View File

@ -23,6 +23,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base qualified as M
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text qualified as T
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.MicroJuvix.Error qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.Language qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi qualified as Micro
import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as Micro
@ -350,7 +351,7 @@ runCommand c = do
micro <- miniToMicro root o
case Micro.checkModule micro of
Right _ -> putStrLn "Well done! It type checks"
Left es -> sequence_ (intersperse (putStrLn "") (printErrorAnsi <$> toList es)) >> exitFailure
Left (Micro.TypeCheckerErrors es) -> sequence_ (intersperse (putStrLn "") (printErrorAnsi <$> toList es)) >> exitFailure
MiniHaskell o -> do
a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root o))
let micro = Micro.translateModule a
@ -358,7 +359,7 @@ runCommand c = do
Right checkedMicro -> do
minihaskell <- fromRightIO' putStrLn (return $ Hask.translateModule checkedMicro)
Hask.printPrettyCodeDefault minihaskell
Left es -> mapM_ printErrorAnsi es >> exitFailure
Left es -> printErrorAnsi es >> exitFailure
Termination (Calls opts@CallsOptions {..}) -> do
a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root opts))
let callMap0 = T.buildCallMap a

View File

@ -14,6 +14,7 @@ import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix
import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
import MiniJuvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix
import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract
@ -31,8 +32,13 @@ type family StageResult c = res | res -> c where
StageResult 'Scoping = Scoper.ScoperResult
StageResult 'Abstract = Abstract.AbstractResult
--------------------------------------------------------------------------------
runIOEither :: Sem '[Files, Error AJuvixError, Embed IO] a -> IO (Either AJuvixError a)
runIOEither = runM . runError . runFilesIO
runIO :: Sem '[Files, Error AJuvixError, Embed IO] a -> IO a
runIO = (runM . runError . runFilesIO) >=> mayThrow
runIO = runIOEither >=> mayThrow
where
mayThrow :: Either AJuvixError r -> IO r
mayThrow = \case
@ -53,8 +59,8 @@ upToAbstract = upToScoping >=> pipelineAbstract
upToMicroJuvix :: Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MicroJuvix.MicroJuvixResult
upToMicroJuvix = upToAbstract >=> pipelineMicroJuvix
-- upToMicroJuvixTyped :: Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MicroJuvixTyped.MicroJuvixTypedResult
-- upToMicroJuvixTyped = upToMicroJuvix >=> pipelineMicroJuvixTyped
upToMicroJuvixTyped :: Members '[Files, Error AJuvixError] r => EntryPoint -> Sem r MicroJuvix.MicroJuvixTypedResult
upToMicroJuvixTyped = upToMicroJuvix >=> pipelineMicroJuvixTyped
--------------------------------------------------------------------------------
@ -76,8 +82,9 @@ pipelineMicroJuvix ::
Sem r MicroJuvix.MicroJuvixResult
pipelineMicroJuvix = mapError (toAJuvixError @Text) . MicroJuvix.entryMicroJuvix
-- pipelineMicroJuvixTyped ::
-- Members '[Files, Error AJuvixError] r =>
-- Abstract.AbstractResult ->
-- Sem r MicroJuvix.MicroJuvixResult
-- pipelineMicroJuvixTyped = mapError (toAJuvixError @Text) . MicroJuvix.entryMicroJuvixTyped
-- TODO:
pipelineMicroJuvixTyped ::
Members '[Files, Error AJuvixError] r =>
MicroJuvix.MicroJuvixResult ->
Sem r MicroJuvix.MicroJuvixTypedResult
pipelineMicroJuvixTyped = undefined

View File

@ -6,5 +6,6 @@ data EntryPoint = EntryPoint
{ _entryRoot :: FilePath,
_entryModulePaths :: NonEmpty FilePath
}
deriving stock (Eq, Show)
makeLenses ''EntryPoint

View File

@ -33,6 +33,15 @@ fromAJuvixError (AJuvixError e) = cast e
throwJuvixError :: (JuvixError err, Member (Error AJuvixError) r) => err -> Sem r a
throwJuvixError = throw . toAJuvixError
runErrorIO ::
(JuvixError a, Member (Embed IO) r) =>
Sem (Error a ': r) b ->
Sem r b
runErrorIO =
runError >=> \case
Left err -> embed (printErrorAnsi err >> exitFailure)
Right a -> return a
instance JuvixError Text where
renderText = id

View File

@ -38,12 +38,12 @@ data Module s = Module
{ _moduleName :: S.Name' s,
_moduleBody :: ModuleBody
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
newtype ModuleBody = ModuleBody
{ _moduleStatements :: [Statement]
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data Statement
= StatementInductive InductiveDef
@ -52,39 +52,39 @@ data Statement
| StatementForeign ForeignBlock
| StatementLocalModule LocalModule
| StatementAxiom AxiomDef
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data FunctionDef = FunctionDef
{ _funDefName :: FunctionName,
_funDefTypeSig :: Expression,
_funDefClauses :: NonEmpty FunctionClause
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data FunctionClause = FunctionClause
{ _clausePatterns :: [Pattern],
_clauseBody :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
newtype FunctionRef = FunctionRef
{_functionRefName :: Name}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype ConstructorRef = ConstructorRef
{_constructorRefName :: Name}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype InductiveRef = InductiveRef
{_inductiveRefName :: Name}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype AxiomRef = AxiomRef
{_axiomRefName :: Name}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
deriving newtype (Hashable)
data Iden
@ -93,7 +93,7 @@ data Iden
| IdenVar VarName
| IdenInductive InductiveRef
| IdenAxiom AxiomRef
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data Expression
= ExpressionIden Iden
@ -103,7 +103,7 @@ data Expression
| ExpressionLiteral LiteralLoc
--- | ExpressionMatch Match
--- ExpressionLambda Lambda not supported yet
deriving stock (Show, Eq)
deriving stock (Eq, Show)
instance HasAtomicity Expression where
atomicity e = case e of
@ -117,45 +117,45 @@ data Match = Match
{ _matchExpression :: Expression,
_matchAlts :: [MatchAlt]
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data MatchAlt = MatchAlt
{ _matchAltPattern :: Pattern,
_matchAltBody :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data Application = Application
{ _appLeft :: Expression,
_appRight :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
instance HasAtomicity Application where
atomicity = const (Aggregate appFixity)
newtype Lambda = Lambda
{_lambdaClauses :: [LambdaClause]}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data LambdaClause = LambdaClause
{ _lambdaParameters :: NonEmpty Pattern,
_lambdaBody :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data FunctionParameter = FunctionParameter
{ _paramName :: Maybe VarName,
_paramUsage :: Usage,
_paramType :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data Function = Function
{ _funParameter :: FunctionParameter,
_funReturn :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
instance HasAtomicity Function where
atomicity = const (Aggregate funFixity)
@ -165,14 +165,14 @@ data ConstructorApp = ConstructorApp
{ _constrAppConstructor :: ConstructorRef,
_constrAppParameters :: [Pattern]
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data Pattern
= PatternVariable VarName
| PatternConstructorApp ConstructorApp
| PatternWildcard
| PatternEmpty
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data InductiveDef = InductiveDef
{ _inductiveName :: InductiveName,
@ -180,20 +180,20 @@ data InductiveDef = InductiveDef
_inductiveType :: Maybe Expression,
_inductiveConstructors :: [InductiveConstructorDef]
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data InductiveConstructorDef = InductiveConstructorDef
{ _constructorName :: ConstrName,
_constructorType :: Expression
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
data AxiomDef = AxiomDef
{ _axiomName :: AxiomName,
_axiomType :: Expression,
_axiomBackendItems :: [BackendItem]
}
deriving stock (Show, Eq)
deriving stock (Eq, Show)
makeLenses ''Module
makeLenses ''FunctionParameter

View File

@ -7,6 +7,6 @@ import MiniJuvix.Prelude
data Stage
= Parsed
| Scoped
deriving stock (Show)
deriving stock (Eq, Show)
$(genSingletons [''Stage])

View File

@ -7,5 +7,6 @@ newtype InfoTable = InfoTable
{ _infoParsedItems :: [ParsedItem]
}
deriving newtype (Semigroup, Monoid)
deriving stock (Eq, Show)
makeLenses ''InfoTable

View File

@ -10,5 +10,6 @@ data ParserResult = ParserResult
_resultTable :: InfoTable,
_resultModules :: NonEmpty (Module 'Parsed 'ModuleTop)
}
deriving stock (Eq, Show)
makeLenses ''ParserResult

View File

@ -7,19 +7,23 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
newtype FunctionInfo = FunctionInfo
{ _functionInfoType :: Expression
}
deriving stock (Eq, Show)
newtype ConstructorInfo = ConstructorInfo
{ _constructorInfoType :: Expression
}
deriving stock (Eq, Show)
data AxiomInfo = AxiomInfo
{ _axiomInfoType :: Expression,
_axiomInfoBackends :: [BackendItem]
}
deriving stock (Eq, Show)
newtype InductiveInfo = InductiveInfo
{ _inductiveInfoDef :: InductiveDef 'Scoped
}
deriving stock (Eq, Show)
data InfoTable = InfoTable
{ _infoConstructors :: HashMap ConstructorRef ConstructorInfo,
@ -29,6 +33,7 @@ data InfoTable = InfoTable
_infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped),
_infoNames :: [S.Name]
}
deriving stock (Eq, Show)
emptyInfoTable :: InfoTable
emptyInfoTable =

View File

@ -11,5 +11,6 @@ data ScoperResult = ScoperResult
_resultScoperTable :: Scoped.InfoTable,
_resultModules :: NonEmpty (Module 'Scoped 'ModuleTop)
}
deriving stock (Eq, Show)
makeLenses ''ScoperResult

View File

@ -18,6 +18,7 @@ getAllModules m =
allImports (MkScopedModule _ w) =
concat [i : allImports (mkScopedModule t) | StatementImport i@(Import t) <- _moduleBody w]
<> concatMap (allImports . mkScopedModule) [l | StatementModule l <- _moduleBody w]
singl :: Module 'Scoped 'ModuleTop -> (S.NameId, Module 'Scoped 'ModuleTop)
singl n = (S._nameId (_modulePath n), n)

View File

@ -5,12 +5,18 @@ module MiniJuvix.Syntax.MicroJuvix.Error
)
where
import MiniJuvix.Prelude
--------------------------------------------------------------------------------
import Data.Text qualified as Text
import MiniJuvix.Prelude qualified as Prelude
import MiniJuvix.Prelude.Base
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
import MiniJuvix.Syntax.MicroJuvix.Error.Pretty qualified as P
import MiniJuvix.Syntax.MicroJuvix.Error.Types
import Prettyprinter
--------------------------------------------------------------------------------
data TypeCheckerError
= ErrTooManyPatterns TooManyPatterns
| ErrWrongConstructorType WrongConstructorType
@ -19,6 +25,13 @@ data TypeCheckerError
| ErrExpectedFunctionType ExpectedFunctionType
deriving stock (Show)
newtype TypeCheckerErrors = TypeCheckerErrors
{ _unTypeCheckerErrors :: NonEmpty TypeCheckerError
}
deriving stock (Show)
makeLenses ''TypeCheckerErrors
ppTypeCheckerError :: TypeCheckerError -> Doc Eann
ppTypeCheckerError = \case
ErrWrongConstructorType e -> ppError e
@ -30,9 +43,16 @@ ppTypeCheckerError = \case
docStream :: TypeCheckerError -> SimpleDocStream Eann
docStream = layoutPretty defaultLayoutOptions . ppTypeCheckerError
instance JuvixError TypeCheckerError where
instance Prelude.JuvixError TypeCheckerError where
renderAnsiText :: TypeCheckerError -> Text
renderAnsiText = renderAnsi . docStream
renderText :: TypeCheckerError -> Text
renderText = P.renderText . docStream
instance Prelude.JuvixError TypeCheckerErrors where
renderAnsiText :: TypeCheckerErrors -> Text
renderAnsiText TypeCheckerErrors {..} = (Text.unlines . toList) (fmap Prelude.renderAnsiText _unTypeCheckerErrors)
renderText :: TypeCheckerErrors -> Text
renderText TypeCheckerErrors {..} = (Text.unlines . toList) (fmap Prelude.renderText _unTypeCheckerErrors)

View File

@ -14,12 +14,12 @@ newtype LocalVars = LocalVars
makeLenses ''LocalVars
checkModule :: Module -> Either (NonEmpty TypeCheckerError) Module
checkModule :: Module -> Either TypeCheckerErrors Module
checkModule m = run $ do
(es, checkedModule) <- runOutputList $ runReader (buildTable m) (checkModule' m)
return $ case es of
[] -> Right checkedModule
(x : xs) -> Left (x :| xs)
return $ case nonEmpty es of
Nothing -> Right checkedModule
Just xs -> Left (TypeCheckerErrors {_unTypeCheckerErrors = xs})
checkModule' ::
Members '[Reader InfoTable, Output TypeCheckerError] r =>

View File

@ -7,38 +7,35 @@ module Base
where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.Abstract.Language qualified as A
import MiniJuvix.Syntax.Concrete.Language qualified as M
import MiniJuvix.Syntax.Concrete.Parser qualified as M
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as M
import MiniJuvix.Translation.ScopedToAbstract qualified as A
import Test.Tasty
import Test.Tasty.HUnit
parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
parseModuleIO = fromRightIO id . Parser.runModuleParserIO
-- parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
-- parseModuleIO = fromRightIO id . Parser.runModuleParserIO
parseTextModuleIO :: Text -> IO (M.Module 'M.Parsed 'M.ModuleTop)
parseTextModuleIO = fromRightIO id . return . Parser.runModuleParser "literal string"
-- parseTextModuleIO :: Text -> IO (M.Module 'M.Parsed 'M.ModuleTop)
-- parseTextModuleIO = fromRightIO id . return . Parser.runModuleParser "literal string"
scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop)
scopeModuleIO = fmap (head . Scoper._resultModules) . fromRightIO' printErrorAnsi . Scoper.scopeCheck1IO "."
-- scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop)
-- scopeModuleIO = fmap (head . Scoper._resultModules) . fromRightIO' printErrorAnsi . Scoper.scopeCheck1IO "."
translateModuleIO :: M.Module 'M.Scoped 'M.ModuleTop -> IO A.TopModule
translateModuleIO = fmap snd . fromRightIO id . return . A.translateModule
-- translateModuleIO :: M.Module 'M.Scoped 'M.ModuleTop -> IO A.TopModule
-- translateModuleIO = fmap snd . fromRightIO id . return . A.translateModule
data AssertionDescr
= Single Assertion
| Steps ((String -> IO ()) -> Assertion)
data TestDescr = TestDescr
{ testName :: String,
testRoot :: FilePath,
{ _testName :: String,
_testRoot :: FilePath,
-- | relative to root
testAssertion :: AssertionDescr
_testAssertion :: AssertionDescr
}
makeLenses ''TestDescr
mkTest :: TestDescr -> TestTree
mkTest TestDescr {..} = case testAssertion of
Single assertion -> testCase testName $ withCurrentDirectory testRoot assertion
Steps steps -> testCaseSteps testName (withCurrentDirectory testRoot . steps)
mkTest TestDescr {..} = case _testAssertion of
Single assertion -> testCase _testName $ withCurrentDirectory _testRoot assertion
Steps steps -> testCaseSteps _testName (withCurrentDirectory _testRoot . steps)

View File

@ -1,29 +1,40 @@
module Scope.Negative (allTests) where
import Base
import MiniJuvix.Pipeline
import MiniJuvix.Syntax.Concrete.Scoped.Error
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as M
type FailMsg = String
data NegTest = NegTest
{ name :: String,
relDir :: FilePath,
file :: FilePath,
checkErr :: ScopeError -> Maybe FailMsg
{ _name :: String,
_relDir :: FilePath,
_file :: FilePath,
_checkErr :: ScopeError -> Maybe FailMsg
}
makeLenses ''NegTest
root :: FilePath
root = "tests/negative"
testDescr :: NegTest -> TestDescr
testDescr NegTest {..} =
TestDescr
{ testName = name,
testRoot = root </> relDir,
testAssertion = Single $ do
p <- parseModuleIO file >>= M.scopeCheck1IO "."
case p of
Left err -> whenJust (checkErr err) assertFailure
Right _ -> assertFailure "The scope checker did not find an error."
}
let tRoot = root </> _relDir
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Single $ do
let entryPoint = EntryPoint tRoot (pure _file)
res <- runIOEither (upToScoping entryPoint)
let msg1 = "The scope checker did not find an error."
let msg2 = "An error ocurred but it was not in the scoper."
case mapLeft fromAJuvixError res of
Left (Just err) -> whenJust (_checkErr err) assertFailure
Left Nothing -> assertFailure msg1
Right _ -> assertFailure msg2
}
allTests :: TestTree
allTests =
@ -31,9 +42,6 @@ allTests =
"Scope negative tests"
(map (mkTest . testDescr) tests)
root :: FilePath
root = "tests/negative"
wrongError :: Maybe FailMsg
wrongError = Just "Incorrect error"

View File

@ -4,55 +4,70 @@ import Base
import Data.Algorithm.Diff
import Data.Algorithm.DiffOutput
import Data.HashMap.Strict qualified as HashMap
import MiniJuvix.Pipeline
import MiniJuvix.Prelude
import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text qualified as M
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as M
import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
import MiniJuvix.Syntax.Concrete.Scoped.Utils
import Text.Show.Pretty hiding (Html)
data PosTest = PosTest
{ name :: String,
relDir :: FilePath,
file :: FilePath
{ _name :: String,
_relDir :: FilePath,
_file :: FilePath
}
makeLenses ''PosTest
root :: FilePath
root = "tests/positive"
testDescr :: PosTest -> TestDescr
testDescr PosTest {..} =
TestDescr
{ testName = name,
testRoot = root </> relDir,
testAssertion = Steps $ \step -> do
step "Parse"
p <- parseModuleIO file
let testRoot = root </> _relDir
in TestDescr
{ _testName = _name,
_testRoot = testRoot,
_testAssertion = Steps $ \step -> do
let entryPoint = EntryPoint testRoot (pure _file)
step "Scope"
s <- scopeModuleIO p
let fs :: HashMap FilePath Text
fs =
HashMap.fromList
[ (getModuleFilePath m, M.renderPrettyCodeDefault m)
| m <- toList (getAllModules s)
]
step "Parsing"
p :: Parser.ParserResult <- runIO (upToParsing entryPoint)
step "Pretty"
let scopedPretty = M.renderPrettyCodeDefault s
let parsedPretty = M.renderPrettyCodeDefault p
let p2 = head (p ^. Parser.resultModules)
step "Parse again"
p' <- parseTextModuleIO scopedPretty
parsedPretty' <- parseTextModuleIO parsedPretty
step "Scoping"
s :: Scoper.ScoperResult <- runIO (pipelineScoper p)
step "Scope again"
s' <-
head . Scoper._resultModules
<$> fromRightIO' printErrorAnsi (return (Scoper.scopeCheck1Pure fs "." p'))
step "Checks"
assertEqDiff "check: scope . parse . pretty . scope . parse = scope . parse" s s'
assertEqDiff "check: parse . pretty . scope . parse = parse" p p'
assertEqDiff "check: parse . pretty . parse = parse" p parsedPretty'
}
let s2 = head (s ^. Scoper.resultModules)
let fs :: HashMap FilePath Text
fs =
HashMap.fromList
[ (getModuleFilePath m, M.renderPrettyCodeDefault m)
| m <- toList (getAllModules s2)
]
let scopedPretty = M.renderPrettyCodeDefault s2
let parsedPretty = M.renderPrettyCodeDefault p2
step "Parsing pretty scoped"
let fs2 = HashMap.singleton _file scopedPretty
p' :: Parser.ParserResult <- (runM . runErrorIO @AJuvixError . runFilesPure fs2) (upToParsing entryPoint)
step "Parsing pretty parsed"
let fs3 = HashMap.singleton _file parsedPretty
parsedPretty' :: Parser.ParserResult <- (runM . runErrorIO @AJuvixError . runFilesPure fs3) (upToParsing entryPoint)
step "Scoping the scoped"
s' :: Scoper.ScoperResult <- (runM . runErrorIO @AJuvixError . runFilesPure fs) (upToScoping entryPoint)
step "Checks"
assertEqDiff "check: scope . parse . pretty . scope . parse = scope . parse" s s'
assertEqDiff "check: parse . pretty . scope . parse = parse" p p'
assertEqDiff "check: parse . pretty . parse = parse" p parsedPretty'
}
assertEqDiff :: (Eq a, Show a) => String -> a -> a -> Assertion
assertEqDiff msg a b

View File

@ -1,6 +1,7 @@
module TypeCheck.Negative (allTests) where
import Base
import MiniJuvix.Pipeline
import MiniJuvix.Syntax.MicroJuvix.Error
import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as T
import MiniJuvix.Translation.AbstractToMicroJuvix qualified as A
@ -8,29 +9,29 @@ import MiniJuvix.Translation.AbstractToMicroJuvix qualified as A
type FailMsg = String
data NegTest = NegTest
{ name :: String,
relDir :: FilePath,
file :: FilePath,
checkErr :: [TypeCheckerError] -> Maybe FailMsg
{ _name :: String,
_relDir :: FilePath,
_file :: FilePath,
_checkErr :: TypeCheckerErrors -> Maybe FailMsg
}
testDescr :: NegTest -> TestDescr
testDescr NegTest {..} =
TestDescr
{ testName = name,
testRoot = root </> relDir,
testAssertion = Single $ do
result <-
parseModuleIO file
>>= scopeModuleIO
>>= translateModuleIO
>>| A.translateModule
>>| T.checkModule
let tRoot = root </> _relDir
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Single $ do
let entryPoint = EntryPoint tRoot (pure _file)
case result of
Left es -> whenJust (checkErr (toList es)) assertFailure
Right _ -> assertFailure "The type checker did not find an error."
}
result <- runIOEither (upToMicroJuvixTyped entryPoint)
let msg1 = "The type checker did not find an error."
let msg2 = "An error ocurred but it was not in the type checker."
case mapLeft fromAJuvixError result of
Left (Just err) -> whenJust (_checkErr err) assertFailure
Left Nothing -> assertFailure msg1
Right _ -> assertFailure msg2
}
allTests :: TestTree
allTests =