mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Split Idris Test Pool
This commit is contained in:
Fabián Heredia Montiel
G. Allais
parent
a23871e57e
commit
932ded4207
119
tests/Main.idr
119
tests/Main.idr
@ -32,8 +32,8 @@ ttimpTests = MkTestPool []
|
||||
"qtt001", "qtt003",
|
||||
"total001", "total002", "total003"]
|
||||
|
||||
idrisTests : TestPool
|
||||
idrisTests = MkTestPool []
|
||||
idrisTestsBasic : TestPool
|
||||
idrisTestsBasic = MkTestPool []
|
||||
-- Fundamental language features
|
||||
["basic001", "basic002", "basic003", "basic004", "basic005",
|
||||
"basic006", "basic007", "basic008", "basic009", "basic010",
|
||||
@ -45,60 +45,91 @@ idrisTests = MkTestPool []
|
||||
"basic036", "basic037", "basic038", "basic039", "basic040",
|
||||
"basic041", "basic042", "basic043", "basic044", "basic045",
|
||||
"basic046", "basic047", "basic048", "basic049", "basic050",
|
||||
"basic051",
|
||||
"basic051"]
|
||||
|
||||
idrisTestsCoverage : TestPool
|
||||
idrisTestsCoverage = MkTestPool []
|
||||
-- Coverage checking
|
||||
"coverage001", "coverage002", "coverage003", "coverage004",
|
||||
["coverage001", "coverage002", "coverage003", "coverage004",
|
||||
"coverage005", "coverage006", "coverage007", "coverage008",
|
||||
"coverage009", "coverage010", "coverage011",
|
||||
-- Documentation strings
|
||||
"docs001", "docs002",
|
||||
-- Evaluator
|
||||
"evaluator001", "evaluator002", "evaluator003", "evaluator004",
|
||||
"coverage009", "coverage010", "coverage011"]
|
||||
|
||||
idrisTestsError : TestPool
|
||||
idrisTestsError = MkTestPool []
|
||||
-- Error messages
|
||||
"error001", "error002", "error003", "error004", "error005",
|
||||
["error001", "error002", "error003", "error004", "error005",
|
||||
"error006", "error007", "error008", "error009", "error010",
|
||||
"error011", "error012", "error013", "error014",
|
||||
-- Modules and imports
|
||||
"import001", "import002", "import003", "import004", "import005",
|
||||
-- Parse errors
|
||||
"perror001", "perror002", "perror003", "perror004", "perror005",
|
||||
"perror006"]
|
||||
|
||||
idrisTestsInteractive : TestPool
|
||||
idrisTestsInteractive = MkTestPool []
|
||||
-- Interactive editing support
|
||||
"interactive001", "interactive002", "interactive003", "interactive004",
|
||||
["interactive001", "interactive002", "interactive003", "interactive004",
|
||||
"interactive005", "interactive006", "interactive007", "interactive008",
|
||||
"interactive009", "interactive010", "interactive011", "interactive012",
|
||||
"interactive013", "interactive014", "interactive015", "interactive016",
|
||||
"interactive017", "interactive018", "interactive019",
|
||||
"interactive017", "interactive018", "interactive019"]
|
||||
|
||||
idrisTestsInterface : TestPool
|
||||
idrisTestsInterface = MkTestPool []
|
||||
-- Interfaces
|
||||
"interface001", "interface002", "interface003", "interface004",
|
||||
["interface001", "interface002", "interface003", "interface004",
|
||||
"interface005", "interface006", "interface007", "interface008",
|
||||
"interface009", "interface010", "interface011", "interface012",
|
||||
"interface013", "interface014", "interface015", "interface016",
|
||||
"interface017", "interface018", "interface019", "interface020",
|
||||
"interface021",
|
||||
"interface021"]
|
||||
|
||||
idrisTestsLinear : TestPool
|
||||
idrisTestsLinear = MkTestPool []
|
||||
-- QTT and linearity related
|
||||
["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping
|
||||
"linear005", "linear006", "linear007", "linear008",
|
||||
"linear009", "linear010", "linear011", "linear012"]
|
||||
|
||||
idrisTestsLiterate : TestPool
|
||||
idrisTestsLiterate = MkTestPool []
|
||||
-- Literate
|
||||
["literate001", "literate002", "literate003", "literate004",
|
||||
"literate005", "literate006", "literate007", "literate008",
|
||||
"literate009", "literate010", "literate011", "literate012",
|
||||
"literate013", "literate014", "literate015", "literate016"]
|
||||
|
||||
idrisTestsPerformance : TestPool
|
||||
idrisTestsPerformance = MkTestPool []
|
||||
-- Performance: things which have been slow in the past, or which
|
||||
-- pose interesting challenges for the elaborator
|
||||
["perf001", "perf002", "perf003", "perf004", "perf005", "perf006"]
|
||||
|
||||
idrisTestsRegression : TestPool
|
||||
idrisTestsRegression = MkTestPool []
|
||||
-- Miscellaneous regressions
|
||||
["reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
|
||||
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
|
||||
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
|
||||
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035"]
|
||||
|
||||
idrisTests : TestPool
|
||||
idrisTests = MkTestPool []
|
||||
-- Documentation strings
|
||||
["docs001", "docs002",
|
||||
-- Evaluator
|
||||
"evaluator001", "evaluator002", "evaluator003", "evaluator004",
|
||||
-- Modules and imports
|
||||
"import001", "import002", "import003", "import004", "import005",
|
||||
-- Miscellaneous REPL
|
||||
"interpreter001", "interpreter002", "interpreter003", "interpreter004",
|
||||
"interpreter005", "interpreter006",
|
||||
-- Implicit laziness, lazy evaluation
|
||||
"lazy001",
|
||||
-- QTT and linearity related
|
||||
"linear001", "linear002", "linear003",
|
||||
-- "linear004" -- disabled due to requiring linearity subtyping
|
||||
"linear005",
|
||||
"linear006", "linear007", "linear008", "linear009", "linear010",
|
||||
"linear011", "linear012",
|
||||
-- Literate
|
||||
"literate001", "literate002", "literate003", "literate004",
|
||||
"literate005", "literate006", "literate007", "literate008",
|
||||
"literate009", "literate010", "literate011", "literate012",
|
||||
"literate013", "literate014", "literate015", "literate016",
|
||||
-- Namespace blocks
|
||||
"namespace001",
|
||||
-- Parameters blocks
|
||||
"params001",
|
||||
-- Performance: things which have been slow in the past, or which
|
||||
-- pose interesting challenges for the elaborator
|
||||
"perf001", "perf002", "perf003", "perf004", "perf005", "perf006",
|
||||
-- Parse errors
|
||||
"perror001", "perror002", "perror003", "perror004", "perror005",
|
||||
"perror006",
|
||||
-- Packages and ipkg files
|
||||
"pkg001", "pkg002", "pkg003", "pkg004", "pkg005",
|
||||
-- Positivity checking
|
||||
@ -113,12 +144,6 @@ idrisTests = MkTestPool []
|
||||
"reflection001", "reflection002", "reflection003", "reflection004",
|
||||
"reflection005", "reflection006", "reflection007", "reflection008",
|
||||
"reflection009",
|
||||
-- Miscellaneous regressions
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
|
||||
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
|
||||
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
|
||||
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
|
||||
-- Totality checking
|
||||
"total001", "total002", "total003", "total004", "total005",
|
||||
"total006", "total007", "total008", "total009", "total010",
|
||||
@ -151,9 +176,10 @@ racketTests = MkTestPool [Racket]
|
||||
|
||||
nodeTests : TestPool
|
||||
nodeTests = MkTestPool [Node]
|
||||
[ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
|
||||
, "node011", "node012", "node015", "node017", "node018", "node019" -- node014
|
||||
, "node021", "node022" --, "node020"
|
||||
[ "node001", "node002", "node003", "node004", "node005", "node006"
|
||||
, "node007", "node008", "node009", "node011", "node012", "node015"
|
||||
, "node017", "node018", "node019", "node021", "node022"
|
||||
-- , "node14", "node020"
|
||||
, "reg001"
|
||||
, "syntax001"
|
||||
, "tailrec001"
|
||||
@ -175,6 +201,15 @@ templateTests = MkTestPool []
|
||||
main : IO ()
|
||||
main = runner
|
||||
[ testPaths "ttimp" ttimpTests
|
||||
, testPaths "idris2" idrisTestsBasic
|
||||
, testPaths "idris2" idrisTestsCoverage
|
||||
, testPaths "idris2" idrisTestsError
|
||||
, testPaths "idris2" idrisTestsInteractive
|
||||
, testPaths "idris2" idrisTestsInterface
|
||||
, testPaths "idris2" idrisTestsLiterate
|
||||
, testPaths "idris2" idrisTestsLinear
|
||||
, testPaths "idris2" idrisTestsPerformance
|
||||
, testPaths "idris2" idrisTestsRegression
|
||||
, testPaths "idris2" idrisTests
|
||||
, testPaths "typedd-book" typeddTests
|
||||
, testPaths "ideMode" ideModeTests
|
||||
|
||||
Loading…
Reference in New Issue
Block a user