mirror of
https://github.com/anoma/juvix.git
synced 2024-12-16 10:56:14 +03:00
ed78f2636b
* Embed stdlib in minijuvix library We add a new step at the beginning of the pipeline called Setup that registers the modules in the standard library with the Files effect. The standard library is then used when the Scoper queries the Files effect for modules as it resolves import statements. Use of the standard library can be disabled using the global `--no-stdlib` command-line option. * CI: Checkout submodules recursively for stdlib * Add a new `--no-stdlib` option to shell check * Poke CI * CI: Checkout submodules in the test job
79 lines
2.3 KiB
Haskell
79 lines
2.3 KiB
Haskell
module Termination.Positive where
|
|
|
|
import Base
|
|
import MiniJuvix.Pipeline
|
|
import Termination.Negative qualified as N
|
|
|
|
data PosTest = PosTest
|
|
{ _name :: String,
|
|
_relDir :: FilePath,
|
|
_file :: FilePath
|
|
}
|
|
|
|
root :: FilePath
|
|
root = "tests/positive/Termination"
|
|
|
|
testDescr :: PosTest -> TestDescr
|
|
testDescr PosTest {..} =
|
|
let tRoot = root </> _relDir
|
|
in TestDescr
|
|
{ _testName = _name,
|
|
_testRoot = tRoot,
|
|
_testAssertion = Single $ do
|
|
let entryPoint = defaultEntryPoint _file
|
|
(void . runIO) (upToMicroJuvix entryPoint)
|
|
}
|
|
|
|
--------------------------------------------------------------------------------
|
|
-- Testing --no-termination flag with all termination negative tests
|
|
--------------------------------------------------------------------------------
|
|
|
|
rootNegTests :: FilePath
|
|
rootNegTests = "tests/negative/Termination"
|
|
|
|
testDescrFlag :: N.NegTest -> TestDescr
|
|
testDescrFlag N.NegTest {..} =
|
|
let tRoot = rootNegTests </> _relDir
|
|
in TestDescr
|
|
{ _testName = _name,
|
|
_testRoot = tRoot,
|
|
_testAssertion = Single $ do
|
|
let entryPoint = EntryPoint "." True True (pure _file)
|
|
(void . runIO) (upToMicroJuvix entryPoint)
|
|
}
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
tests :: [PosTest]
|
|
tests =
|
|
[ PosTest "Ackerman nice def. is terminating" "." "Ack.mjuvix",
|
|
PosTest "Recursive functions on Lists" "." "Data/List.mjuvix"
|
|
]
|
|
|
|
testsWithKeyword :: [PosTest]
|
|
testsWithKeyword =
|
|
[ PosTest "terminating added to fx:=fx" "." "ToEmpty.mjuvix",
|
|
PosTest "terminating for all functions in the mutual block" "." "Mutual.mjuvix",
|
|
PosTest "Undefined is terminating by assumption" "." "Undefined.mjuvix"
|
|
]
|
|
|
|
negTests :: [N.NegTest]
|
|
negTests = N.tests
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
allTests :: TestTree
|
|
allTests =
|
|
testGroup
|
|
"Positive tests"
|
|
[ testGroup
|
|
"Well-known terminating functions"
|
|
(map (mkTest . testDescr) tests),
|
|
testGroup
|
|
"Bypass checking using --non-termination flag on negative tests"
|
|
(map (mkTest . testDescrFlag) negTests),
|
|
testGroup
|
|
"Terminating keyword"
|
|
(map (mkTest . testDescr) testsWithKeyword)
|
|
]
|