1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Idris2/tests/Main.idr

247 lines
7.6 KiB
Idris
Raw Normal View History

module Main
import System
import System.Directory
import System.File
import Test.Golden
%default covering
------------------------------------------------------------------------
-- Test cases
2023-09-01 13:10:49 +03:00
ttimpTests : IO TestPool
ttimpTests = testsInDir "ttimp" "TTImp"
2023-09-01 13:10:49 +03:00
idrisTestsBasic : IO TestPool
idrisTestsBasic = testsInDir "idris2/basic" "Fundamental language features"
2023-09-01 13:10:49 +03:00
idrisTestsDebug : IO TestPool
idrisTestsDebug = testsInDir "idris2/debug" "Debug features"
2023-09-01 13:10:49 +03:00
idrisTestsCoverage : IO TestPool
idrisTestsCoverage = testsInDir "idris2/coverage" "Coverage checking"
2023-09-01 13:10:49 +03:00
idrisTestsTermination : IO TestPool
idrisTestsTermination = testsInDir "idris2/termination" "Termination checking"
2023-09-01 13:10:49 +03:00
idrisTestsCasetree : IO TestPool
idrisTestsCasetree = testsInDir "idris2/casetree" "Case tree building"
2023-09-01 13:10:49 +03:00
idrisTestsWarning : IO TestPool
idrisTestsWarning = testsInDir "idris2/warning" "Warnings"
2023-09-01 13:10:49 +03:00
idrisTestsFailing : IO TestPool
idrisTestsFailing = testsInDir "idris2/failing" "Failing blocks"
2023-09-01 13:10:49 +03:00
||| Error messages, including parse errors ("perror")
idrisTestsError : IO TestPool
idrisTestsError = testsInDir "idris2/error" "Error messages"
2023-09-01 13:10:49 +03:00
idrisTestsInteractive : IO TestPool
idrisTestsInteractive = testsInDir "idris2/interactive" "Interactive editing"
2023-09-01 13:10:49 +03:00
idrisTestsInterface : IO TestPool
idrisTestsInterface = testsInDir "idris2/interface" "Interface"
2023-09-01 13:10:49 +03:00
||| QTT and linearity related
idrisTestsLinear : IO TestPool
idrisTestsLinear = testsInDir "idris2/linear" "Quantities"
2020-12-08 01:51:33 +03:00
2023-09-01 13:10:49 +03:00
idrisTestsLiterate : IO TestPool
idrisTestsLiterate = testsInDir "idris2/literate" "Literate programming"
2023-09-01 13:10:49 +03:00
||| Performance: things which have been slow in the past, or which
||| pose interesting challenges for the elaborator
idrisTestsPerformance : IO TestPool
idrisTestsPerformance = testsInDir "idris2/perf" "Performance"
2023-09-01 13:10:49 +03:00
idrisTestsRegression : IO TestPool
idrisTestsRegression = testsInDir "idris2/reg" "Various regressions"
2023-09-01 13:10:49 +03:00
||| Data types, including records
idrisTestsData : IO TestPool
idrisTestsData = testsInDir "idris2/data" "Data and record types"
2023-09-01 13:10:49 +03:00
||| %builtin related tests for the frontend (type-checking)
idrisTestsBuiltin : IO TestPool
idrisTestsBuiltin = testsInDir "idris2/builtin" "Builtin types and functions"
2023-09-01 13:10:49 +03:00
||| Evaluator, REPL, specialisation
idrisTestsEvaluator : IO TestPool
idrisTestsEvaluator = testsInDir "idris2/evaluator" "Evaluation"
2023-09-01 13:10:49 +03:00
idrisTestsREPL : IO TestPool
idrisTestsREPL = testsInDir "idris2/repl" "REPL commands and help"
2023-09-01 13:10:49 +03:00
idrisTestsAllSchemes : Requirement -> IO TestPool
idrisTestsAllSchemes cg = testsInDir "allschemes"
("Test across all scheme backends: " ++ show cg ++ " instance")
{codegen = Just cg}
idrisTestsAllBackends : Requirement -> TestPool
idrisTestsAllBackends cg = MkTestPool
("Test across all backends: " ++ show cg ++ " instance")
[] (Just cg)
2022-05-10 17:09:53 +03:00
-- RefC implements IEEE standard and distinguishes between 0.0 and -0.0
-- unlike other backends. So turn this test for now.
$ ([ "issue2362" ] <* guard (cg /= C))
++ ([ "popen2" ] <* guard (cg /= Node))
2022-05-10 17:09:53 +03:00
++ [ -- Evaluator
"evaluator004",
-- Unfortunately the behaviour of Double is platform dependent so the
-- following test is turned off.
-- "evaluator005",
"basic048",
"perf006"]
2023-09-01 13:10:49 +03:00
||| Totality checking, including positivity
idrisTestsTotality : IO TestPool
idrisTestsTotality = testsInDir "idris2/total" "Totality checking"
Experimental Scheme based evaluator (#1956) This is for compiled evaluation at compile-time, for full normalisation. You can try it by setting the evaluation mode to scheme (that is, :set eval scheme at the REPL). It's certainly an order of magnitude faster than the standard evaluator, based on my playing around with it, although still quite a bit slower than compilation for various reasons, including: * It has to evaluate under binders, and therefore deal with blocked symbols * It has to maintain enough information to be able to read back a Term from the evaluated scheme object, which means retaining things like types and other metadata * We can't do a lot of the optimisations we'd do for runtime evaluation particularly setting things up so we don't need to do arity checking Also added a new option evaltiming (set with :set evaltiming) to display how long evaluation itself takes, which is handy for checking performance. I also don't think we should aim to replace the standard evaluator, in general, at least not for a while, because that will involve rewriting a lot of things and working out how to make it work as Call By Name (which is clearly possible, but fiddly). Still, it's going to be interesting to experiment with it! I think it will be a good idea to use it for elaborator reflection and type providers when we eventually get around to implementing them. Original commit details: * Add ability to evaluate open terms via Scheme Still lots of polish and more formal testing to do here before we can use it in practice, but you can still use ':scheme <term>' at the REPL to evaluate an expression by compiling to scheme then reading back the result. Also added 'evaltiming' option at the REPL, which, when set, displays how long normalisaton takes (doesn't count resugaring, just the normalisation step). * Add scheme evaluation mode Different when evaluating everything, vs only evaluating visible things. We want the latter when type checking, the former at the REPL. * Bring support.rkt up to date A couple of missing things required for interfacing with scheme objects * More Scheme readback machinery We need these things in the next version so that the next-but-one version can have a scheme evaluator! * Add top level interface to scheme based normaliser Also check it's available - currently chez only - and revert to the default slow normaliser if it's not. * Bring Context up to date with changes in main * Now need Idris 0.5.0 to build * Add SNF type for scheme values This will allow us to incrementally evaluate under lambdas, which will be useful for elaborator reflection and type providers. * Add Quote for scheme evaluator So, we can now get a weak head normal form, and evaluate the scope of a binder when we have an argument to plug in, or just quote back the whole thing. * Add new 'scheme' evaluator mode at the REPL Replacing the temporary 'TmpScheme', this is a better way to try out the scheme based evaluator * Fix name generation for new UN format * Add scheme evaluator support to Racket * Add another scheme eval test With metavariables this time * evaltiming now times execution too This was handy for finding out the difference between the scheme based evaluator and compilation. Compilation was something like 20 times faster in my little test, so that'd be about 4-500 times faster than the standard evaluator. Ouch! * Fix whitespace errors * Error handling when trying to evaluate Scheme
2021-09-24 22:38:55 +03:00
-- This will only work with an Idris compiled via Chez or Racket, but at
-- least for the moment we're not officially supporting self hosting any
-- other way. If we do, we'll need to have a way to disable these.
2023-09-01 13:10:49 +03:00
idrisTestsSchemeEval : IO TestPool
idrisTestsSchemeEval = testsInDir "idris2/schemeeval" "Scheme Evaluator"
2023-09-01 13:10:49 +03:00
idrisTestsReflection : IO TestPool
idrisTestsReflection = testsInDir "idris2/reflection" "Quotation and Reflection"
2023-09-01 13:10:49 +03:00
idrisTestsWith : IO TestPool
idrisTestsWith = testsInDir "idris2/with" "With abstraction"
2023-09-01 13:10:49 +03:00
2023-10-18 14:06:36 +03:00
idrisTestsOperators : IO TestPool
idrisTestsOperators = testsInDir "idris2/operators" "Operator and fixities"
2023-09-01 13:10:49 +03:00
idrisTestsIPKG : IO TestPool
idrisTestsIPKG = testsInDir "idris2/pkg" "Package and .ipkg files"
2020-12-08 01:51:33 +03:00
idrisTests : TestPool
idrisTests = MkTestPool "Misc" [] Nothing
2020-12-08 01:51:33 +03:00
-- Documentation strings
2022-03-08 21:14:40 +03:00
["docs001", "docs002", "docs003", "docs004", "docs005",
-- Eta equality
"eta001",
2020-12-08 01:51:33 +03:00
-- Modules and imports
"import001", "import002", "import003", "import004", "import005", "import006",
2023-07-31 10:35:16 +03:00
"import007", "import008", "import009",
-- Implicit laziness, lazy evaluation
"lazy001", "lazy002", "lazy003", "lazy004",
-- Namespace blocks
"namespace001", "namespace002", "namespace003", "namespace004", "namespace005",
-- Parameters blocks
"params001", "params002", "params003",
-- Larger programs arising from real usage. Typically things with
-- interesting interactions between features
"real001", "real002",
-- Inlining
"inlining001",
2020-05-22 21:26:10 +03:00
-- with-disambiguation
"with003",
-- pretty printing
2021-12-02 14:30:38 +03:00
"pretty001", "pretty002",
-- PrimIO
"primloop",
-- golden file testing
"golden001",
-- quantifiers
2022-07-08 16:16:25 +03:00
"quantifiers001",
-- unification
"unification001"
]
typeddTests : IO TestPool
typeddTests = testsInDir "typedd-book" "Type Driven Development"
2023-09-01 13:10:49 +03:00
chezTests : IO TestPool
chezTests = testsInDir "chez" "Chez backend" {codegen = Just Chez}
refcTests : IO TestPool
refcTests = testsInDir "refc" "Reference counting C backend" {codegen = Just C}
2023-09-01 13:10:49 +03:00
racketTests : IO TestPool
racketTests = testsInDir "racket" "Racket backend" {codegen = Just Racket}
{ pred = not . (`elem` ["conditions006", "conditions007"]) }
2023-09-01 13:10:49 +03:00
nodeTests : IO TestPool
nodeTests = testsInDir "node" "Node backend" {codegen = Just Node}
2020-06-11 12:52:54 +03:00
vmcodeInterpTests : IO TestPool
vmcodeInterpTests = testsInDir "vmcode" "VMCode interpreter"
2021-07-07 19:06:59 +03:00
ideModeTests : IO TestPool
ideModeTests = testsInDir "ideMode" "IDE mode"
2020-06-11 12:52:54 +03:00
preludeTests : IO TestPool
preludeTests = testsInDir "prelude" "Prelude library"
templateTests : IO TestPool
templateTests = testsInDir "templates" "Test templates"
-- base library tests are run against
-- each codegen supported and to keep
-- things simple it's all one test group
-- that only runs if all backends are
-- available.
baseLibraryTests : IO TestPool
baseLibraryTests = testsInDir "base" "Base library" {requirements = [Chez, Node]}
2021-04-22 10:30:56 +03:00
-- same behavior as `baseLibraryTests`
contribLibraryTests : IO TestPool
contribLibraryTests = testsInDir "contrib" "Contrib library" {requirements = [Chez, Node]}
2021-04-22 10:30:56 +03:00
codegenTests : IO TestPool
codegenTests = testsInDir "codegen" "Code generation"
main : IO ()
main = runner $
2023-09-01 13:10:49 +03:00
[ !ttimpTests
, !idrisTestsBasic
, !idrisTestsCoverage
, !idrisTestsTermination
, !idrisTestsCasetree
, !idrisTestsError
, !idrisTestsFailing
, !idrisTestsWarning
, !idrisTestsInteractive
, !idrisTestsInterface
, !idrisTestsLiterate
, !idrisTestsLinear
, !idrisTestsPerformance
, !idrisTestsRegression
, !idrisTestsData
, !idrisTestsBuiltin
, !idrisTestsEvaluator
, !idrisTestsREPL
, !idrisTestsTotality
, !idrisTestsSchemeEval
, !idrisTestsReflection
, !idrisTestsWith
2023-10-18 14:06:36 +03:00
, !idrisTestsOperators
2023-09-01 13:10:49 +03:00
, !idrisTestsDebug
, !idrisTestsIPKG
, testPaths "idris2/misc" idrisTests
, !typeddTests
, !ideModeTests
, !preludeTests
, !baseLibraryTests
, !contribLibraryTests
2023-09-01 13:10:49 +03:00
, !chezTests
, !refcTests
2023-09-01 13:10:49 +03:00
, !racketTests
, !nodeTests
, !vmcodeInterpTests
, !templateTests
, !codegenTests
]
2023-09-01 13:10:49 +03:00
++ !(traverse idrisTestsAllSchemes [Chez, Racket])
2022-05-10 17:09:53 +03:00
++ map (testPaths "allbackends" . idrisTestsAllBackends) [Chez, Node, Racket, C]
where
testPaths : String -> TestPool -> TestPool
testPaths dir = { testCases $= map ((dir ++ "/") ++) }