idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-10 13:44:21 +03:00
Code Issues Projects Releases Wiki Activity
d712ea288a
Idris2/tests/Main.idr

190 lines
7.3 KiB
Idris
Raw Normal View History

Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
module Main
import Data.Maybe
import Data.List
[ refactor ] introduce List1 to remove impossible case (#520)
2020-08-04 22:03:18 +03:00
import Data.List1
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
import Data.Strings
import System
import System.Directory
import System.File
Be lenient with slashes and backslashes on Windows
2020-05-22 15:27:12 +03:00
import System.Info
Windows support
2020-05-20 19:14:38 +03:00
import System.Path
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
import Lib
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
%default covering
------------------------------------------------------------------------
-- Test cases
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
ttimpTests : TestPool
ttimpTests = MkTestPool []
["basic001", "basic002", "basic003", "basic004", "basic005",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
"basic006",
"coverage001", "coverage002",
"dot001",
"eta001", "eta002",
"lazy001",
"nest001", "nest002",
"perf001", "perf002", "perf003",
"record001", "record002", "record003",
Allow _ for names in pi binders This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope.
2020-05-25 15:14:51 +03:00
"qtt001", "qtt003",
Remove some tests which are no longer useful These are ttimp tests that are now subsumed by idris2 tests, and we'd need to implement some ttimp source that isn't really worth it at this stage.
2020-05-19 20:31:52 +03:00
"total001", "total002", "total003"]
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
idrisTests : TestPool
idrisTests = MkTestPool []
-- Fundamental language features
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
["basic001", "basic002", "basic003", "basic004", "basic005",
"basic006", "basic007", "basic008", "basic009", "basic010",
"basic011", "basic012", "basic013", "basic014", "basic015",
"basic016", "basic017", "basic018", "basic019", "basic020",
"basic021", "basic022", "basic023", "basic024", "basic025",
"basic026", "basic027", "basic028", "basic029", "basic030",
"basic031", "basic032", "basic033", "basic034", "basic035",
"basic036", "basic037", "basic038", "basic039", "basic040",
[ log ] stuck functions found during evaluation
2020-08-27 20:09:39 +03:00
"basic041", "basic042", "basic043", "basic044", "basic045",
Have lambda-case available everywhere lambda is (#819)
2020-12-07 14:34:48 +03:00
"basic046", "basic047", "basic048", "basic049", "basic050",
[ fix #833, #677 ] bound variables start with a lowercase letter
2020-12-10 20:09:16 +03:00
"basic051",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004",
More coverage checking fixes Still a couple of things to resolve in coverage and totality checking before we can switch on %default, so don't expect quite the right behaviour just yet. More progress though! Also working on this has caught a few totality errors in the Idris 2 code base that Idris 1 missed... so these are fixed on the way.
2020-05-24 14:52:07 +03:00
"coverage005", "coverage006", "coverage007", "coverage008",
[ fix ] recoverability criteria If the "can't convert" error arises from a mismatch between a type constructor and a primitive value, it is not recoverable.
2020-11-11 18:55:30 +03:00
"coverage009", "coverage010", "coverage011",
Initial implementation of :doc It's not pretty, but at least it exists now
2020-07-08 17:52:57 +03:00
-- Documentation strings
Add :browse Lists all the names in a namespace with their types, and the first line of their docstring if it exists
2020-07-08 19:56:54 +03:00
"docs001", "docs002",
[ fix #650 ] Lazier match in NPrimVal vs. ConCase (#655)
2020-09-09 19:17:07 +03:00
-- Evaluator
[ fix #735 ] Make sure type constructors are fully applied
2020-10-16 00:44:30 +03:00
"evaluator001", "evaluator002", "evaluator003", "evaluator004",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Error messages
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",
[ fix #735 ] Make sure type constructors are fully applied
2020-10-16 00:44:30 +03:00
"error011", "error012", "error013", "error014",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Modules and imports
Add "import X as Y" properly Instead of just the cursory name update that we used to do (which didn't work properly anyway for a lot of reasons), now we add aliases for all the names in the imported module. So, like Idris 1, every global has a canonical name by which we can refer to it, but it can also have aliases via "import ... as".
2020-07-04 22:26:49 +03:00
"import001", "import002", "import003", "import004", "import005",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Interactive editing support
"interactive001", "interactive002", "interactive003", "interactive004",
"interactive005", "interactive006", "interactive007", "interactive008",
"interactive009", "interactive010", "interactive011", "interactive012",
Look at intermediate results in program search This has involved quite a bit of reorganisation and some improvements in resugaring so that the results look nice. In summary: * Expression search now gives back a RawImp rather than a checked term, which allows it to include case expressions * Case with one pattern is resugared to a destructuring let * Some name generation issues address in function generation We look at intermediate results for local variables which are functions that return a concrete type, or recursive calls that return a single constructor type. In these cases, we: * let bind the local variable/recursive call * generate a new definition for the scope, as a 'case' function When we recursively generate the definition, it's a bit more restricted so as not to explode the search space. We only take the first result, we only look one constructor deep, and we go right to left on variable splitting so only deconstruct the name we've just added.
2020-08-04 14:51:57 +03:00
"interactive013", "interactive014", "interactive015", "interactive016",
Add a test for proof search
2020-08-04 22:55:48 +03:00
"interactive017", "interactive018",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Interfaces
"interface001", "interface002", "interface003", "interface004",
"interface005", "interface006", "interface007", "interface008",
"interface009", "interface010", "interface011", "interface012",
[ re #270 ] Mention the target type of the auto search
2020-06-11 16:28:34 +03:00
"interface013", "interface014", "interface015", "interface016",
Add missing test :# ../../../src/Compiler/.ANF.idr.swp
2020-12-14 16:38:40 +03:00
"interface017", "interface018", "interface019", "interface020",
Treat local hints differently in auto search Local hints need to reduce (just like global hints do) so we expand their definition to the lifted name before applying them. We're identifying the global hints by knowing that the binder name is a nested function name. This is a bit of hack, and it'd probably be better to record that information in the binder instead, but that's a more substantial change than I want to do right now.
2020-12-27 16:41:48 +03:00
"interface021",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Miscellaneous REPL
[ test ] making sure cast works
2020-09-23 20:52:38 +03:00
"interpreter001", "interpreter002", "interpreter003", "interpreter004",
Add it to REPL (#887) Co-authored-by: Michael Messer <michaelmesser@users.noreply.github.com>
2020-12-30 02:52:03 +03:00
"interpreter005", "interpreter006",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Implicit laziness, lazy evaluation
"lazy001",
-- QTT and linearity related
Remove linearity subtyping It's disappointing to have to do this, but I think necessary because various issue reports have shown it to be unsound (at least as far as inference goes) and, at the very least, confusing. This patch brings us back to the basic rules of QTT. On the one hand, this makes the 1 multiplicity less useful, because it means we can't flag arguments as being used exactly once which would be useful for optimisation purposes as well as precision in the type. On the other hand, it removes some complexity (and a hack) from unification, and has the advantage of being correct! Also, I still consider the 1 multiplicity an experiment. We can still do interesting things like protocol state tracking, which is my primary motivation at least. Ideally, if the 1 multiplicity is going to be more generall useful, we'll need some kind of way of doing multiplicity polymorphism in the future. I don't think subtyping is the way (I've pretty much always come to regret adding some form of subtyping). Fixes #73 (and maybe some others).
2020-12-27 22:58:35 +03:00
"linear001", "linear002", "linear003",
-- "linear004" -- disabled due to requiring linearity subtyping
"linear005",
Add experimental library for linear computations In Control.Linear.LIO - allows wrapping anything that supports chaining of linear computations (most usefully, IO).
2020-06-24 01:10:22 +03:00
"linear006", "linear007", "linear008", "linear009", "linear010",
Use precise inference for hole types That is, don't generalise multiplicities, because we need the hole type to be precise wrt multiplicities. Resolves #189
2020-06-29 00:16:15 +03:00
"linear011", "linear012",
Implement make-case
2020-06-27 20:14:14 +03:00
-- Literate
"literate001", "literate002", "literate003", "literate004",
"literate005", "literate006", "literate007", "literate008",
"literate009", "literate010", "literate011", "literate012",
Improving error messages (#786) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-11-26 14:35:55 +03:00
"literate013", "literate014", "literate015", "literate016",
change namespace parser to have minimum indentation The namespace parser was not requiring a minimum indentation and instead based its indentation on the following line, which meant that a line like: namespace Foo foodef : Int placed foodef into namespace Foo instead of the module's top level. And so made it unclear when a namespace ends.
2020-06-21 06:33:39 +03:00
-- Namespace blocks
"namespace001",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Parameters blocks
"params001",
-- Performance: things which have been slow in the past, or which
-- pose interesting challenges for the elaborator
[ fix #775 ] integerToNat is not, in fact, id (#799)
2020-11-27 21:48:19 +03:00
"perf001", "perf002", "perf003", "perf004", "perf005", "perf006",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Parse errors
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006",
-- Packages and ipkg files
[ fix #423 ] --repl should load the main file
2020-07-07 22:24:37 +03:00
"pkg001", "pkg002", "pkg003", "pkg004", "pkg005",
[ re #660 ] Positivity checking for empty types
2020-09-14 18:07:25 +03:00
-- Positivity checking
[ re #660 ] eta-contract parameter candidates
2020-09-16 16:28:18 +03:00
"positivity001", "positivity002", "positivity003",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Larger programs arising from real usage. Typically things with
-- interesting interactions between features
"real001", "real002",
-- Records, access and dependent update
Pay attention to implicits in record update Resolves #421
2020-07-06 19:39:55 +03:00
"record001", "record002", "record003", "record004", "record005",
Implement new application syntax Add syntax for bind-all-explicits Add new record update syntax Remove PInstance
2020-10-01 12:41:30 +03:00
"record006",
Make a start on reflection Don't get too excited yet - I want this in so that it doesn't get too out of sync, but I still have to think about exactly how it's going to work in practice.
2020-05-30 00:40:29 +03:00
-- Quotation and reflection
Add reflection operation for adding declarations Declarations can be quoted with `[ decl ]. See reflection004 for an example.
2020-06-01 17:01:52 +03:00
"reflection001", "reflection002", "reflection003", "reflection004",
Add reflection under (explicit) binders This allows writing a staged well typed interpreter, for example (see reflection008 test)
2020-06-03 11:17:37 +03:00
"reflection005", "reflection006", "reflection007", "reflection008",
Improve elaborator reflection performance In a 'Bind', normalise the result of the first action, rather than quoting the HNF. This improves performance since the HNF could be quite big when quoted back. Ideally, we wouldn't have to quote and unquote here, and we can probably achieve this by tinkering with the evaluator. This has an unfortunate effect on the reflection002 test, in that the "typed template Idris" example now evaluates too much. But, I think the overall performance is too important for the primary motivation behind elaborator reflection. I will return to this!
2020-07-17 17:18:23 +03:00
"reflection009",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Miscellaneous regressions
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
Look inside case blocks in conversion check This is quite fiddly as it the blocks might be in different contexts so we need to keep track of which variables correspond in the scrutinees of the blocks. Once that's done, check the terms at the leaves convert, then check the corresponding variables convert. This may not be perfect yet, because we only look at case scrutinees to find correspondence. It might also be a bit slower than it could be, but at least these checks are quite rare. Fixes #208 and maybe some others?
2020-06-04 20:21:44 +03:00
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
Use 'unify' rather than 'convert' if possible 'convert' doesn't solve holes, so might reject things that are solvable. This can be an issue when resolving interfaces, because we were using convert for arguments of the invertible holes that arise when trying to resolve them. Fixes #66.
2020-06-29 17:04:32 +03:00
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
Auto-implicit `__con` now added before implicits. (#659)
2020-12-07 14:41:47 +03:00
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- Totality checking
"total001", "total002", "total003", "total004", "total005",
Fix bug #654 Auxiliary functions introduced in elaboration (e.g., through case splits and with clauses) now have the same totality annotation as the function they're defined in. Moved auxiliary function `findSetTotal` into `Context.idr` since it's now used by `ProcessDef.idr` too. Added a totality requirement argument to `checkClause` so that the with-clause case could propagate it to the functions it generates in elaboration. Sandwhich the rhs elaboration in pattern matches with code that sets the global, default, totality requirement to the current one, and restores the previous default afterwards. It's a bit of a hacky way to do it, but I don't think we have a better alternative with the current design.
2020-09-09 19:09:48 +03:00
"total006", "total007", "total008", "total009", "total010",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
-- The 'with' rule
Apply the patch from idris2-boot.
2020-05-22 21:26:10 +03:00
"with001", "with002",
-- with-disambiguation
"with003"]
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
typeddTests : TestPool
typeddTests = MkTestPool []
["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
"chapter06", "chapter07", "chapter08", "chapter09", "chapter10",
"chapter11", "chapter12", "chapter13", "chapter14"]
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
chezTests : TestPool
chezTests = MkTestPool [Chez]
["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
Fix chez016 test
2020-05-19 23:02:15 +03:00
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
Add test for setenv and unsetenv
2020-06-16 13:22:21 +03:00
"chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
add `extraRuntime` option for Scheme backends (#578)
2020-08-21 11:34:57 +03:00
"chez025", "chez026", "chez027", "chez028", "chez029", "chez030",
add ability to target scheme flavor in foreign specifiers There's some missing flexibility in how foreign specifiers can be used with scheme that is addressed here with minimal changes to how scheme specifiers are read. This opens up uses for users that they otherwise would have had to modify the compiler's support files to accomplish.
2020-09-11 09:51:48 +03:00
"chez031",
Implement Futures as a Parallelism Primitive (#753) Co-authored-by: Christian Rasmussen <christian.rasmussen@me.com>
2020-12-04 13:58:26 +03:00
"concurrency001",
[ fix #724 ] Typo in the magic string (#726)
2020-10-03 16:39:13 +03:00
"perf001",
Fix chez016 test
2020-05-19 23:02:15 +03:00
"reg001"]
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Implement Racket Futures Support
2021-01-13 23:54:43 +03:00
racketTests : TestPool
racketTests = MkTestPool [Racket]
["concurrency001"]
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
nodeTests : TestPool
nodeTests = MkTestPool [Node]
[ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
node018 passes
2020-06-21 19:54:50 +03:00
, "node011", "node012", "node015", "node017", "node018", "node019" -- node014
add support for more casts from and to BitsN types (#548) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-08-20 17:01:09 +03:00
, "node021", "node022" --, "node020"
tests everywhere
2020-06-12 23:35:08 +03:00
, "reg001"
add test for js case clause scopes
2020-07-14 19:38:47 +03:00
, "syntax001"
self tail rec
2020-07-05 13:53:45 +03:00
, "tailrec001"
Make `NmLet` names unique in `Compiler.ES.Imperative` Since the imperative form has no nesting of scopes. Fixes #643
2020-09-19 22:09:36 +03:00
, "idiom001"
tests everywhere
2020-06-12 23:35:08 +03:00
]
first test
2020-06-11 12:52:54 +03:00
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
ideModeTests : TestPool
ideModeTests = MkTestPool []
[ "ideMode001", "ideMode002", "ideMode003", "ideMode004" ]
first test
2020-06-11 12:52:54 +03:00
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
preludeTests : TestPool
preludeTests = MkTestPool []
[ "reg001" ]
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Test templates (#585) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-11-27 18:40:02 +03:00
templateTests : TestPool
templateTests = MkTestPool []
[ "simple-test", "ttimp", "with-ipkg" ]
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
main : IO ()
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
main = runner
[ testPaths "ttimp" ttimpTests
, testPaths "idris2" idrisTests
, testPaths "typedd-book" typeddTests
, testPaths "ideMode" ideModeTests
, testPaths "prelude" preludeTests
, testPaths "chez" chezTests
Implement Racket Futures Support
2021-01-13 23:54:43 +03:00
, testPaths "racket" racketTests
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
, testPaths "node" nodeTests
Test templates (#585) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-11-27 18:40:02 +03:00
, testPaths "templates" templateTests
Make Idris2 test harness available for the many and not the few. (#719) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 11:26:23 +03:00
] where
testPaths : String -> TestPool -> TestPool
testPaths dir = record { testCases $= map ((dir ++ "/") ++) }
Reference in New Issue Copy Permalink