Idris-dev/test/README

Tests:

001: Well-typed interpreter
002: Universe checking
003: Literate source and string processing
004: File operations
005: Num class resolution [regression]; span & break; ad-hoc overloading
006: Provisional definitions; class resolution in patterns
007: Applicative and idiom brackets
008: case and pattern matching let
009: ranges and list monad
010: total
011: record projection and update
012: various error regressions
013: binding syntax
014: resource DSL
015: verified binary adder
016: codata
017: mutually recursive totality checking
018: Message passing concurrency (raw form)
019: magic with
020: implicit conversions
021: effects
022: dynamic C library loading and interpreter IO
023: trivial (non-I/O) type providers
024: interpreter I/O
025: memory effects
026: simple file-I/O-based type provider
027: class constraints in using block
028: hello world with comment and block comment syntax in idr file
029: match_refine and apply by type
030: %reflection for functions running on syntax
031: error reflection 
032: control idris via stdin
033: null pointer creation and check
034: presence of floating point primitives in backends

regxxx: various regression tests
reg020: working strlen
Fix obscure where naming bug 2011-12-22 02:06:26 +04:00			`Tests:`

			`001: Well-typed interpreter`
			`002: Universe checking`
			`003: Literate source and string processing`
			`004: File operations`
			`005: Num class resolution [regression]; span & break; ad-hoc overloading`
New test 2012-01-01 23:59:46 +04:00			`006: Provisional definitions; class resolution in patterns`
Test for idiom brackets and Applicative class 2012-01-04 15:05:37 +04:00			`007: Applicative and idiom brackets`
Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaboration 2012-01-06 04:10:12 +04:00			`008: case and pattern matching let`
Numeric ranges [a..b], [a,b .. c] and list monad 2012-01-06 19:11:11 +04:00			`009: ranges and list monad`
Added record test 2012-01-28 01:21:31 +04:00			`010: total`
			`011: record projection and update`
Check patterns are inaccessible 2012-04-24 17:57:55 +04:00			`012: various error regressions`
Added binding form to syntax rules (and updated tutorial accordingly) 2012-05-30 13:32:57 +04:00			`013: binding syntax`
Warn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) 2012-10-18 23:52:17 +04:00			`014: resource DSL`
			`015: verified binary adder`
Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructor 2012-10-23 03:37:55 +04:00			`016: codata`
Deal with higher order recursive arguments in size change graphs 2012-10-26 18:40:44 +04:00			`017: mutually recursive totality checking`
Added raw (non-typesafe) message passing library (System.Concurrency.Raw) 2012-10-30 17:29:22 +04:00			`018: Message passing concurrency (raw form)`
Only apply unique implicit conversions (and add test) 2013-02-25 14:39:14 +04:00			`019: magic with`
			`020: implicit conversions`
Added effects package and associated tests 2013-03-01 17:52:51 +04:00			`021: effects`
Test for dynamic loading of C libs + interpreter IO 2013-03-21 21:57:54 +04:00			`022: dynamic C library loading and interpreter IO`
Added new tests to the test README 2013-04-04 18:03:21 +04:00			`023: trivial (non-I/O) type providers`
			`024: interpreter I/O`
Test for simple file-based type providers 2013-04-23 01:01:23 +04:00			`025: memory effects`
			`026: simple file-I/O-based type provider`
Allow type class constraints in 'using' clauses e.g. if a using block is given as using (C a b c) block Then any declaration in the block which uses all of a, b and c in its type will have the class constraint C a b c added implicitly. See test027 for an example 2013-05-16 22:27:45 +04:00			`027: class constraints in using block`
Add test documentation 2013-11-06 08:27:04 +04:00			`028: hello world with comment and block comment syntax in idr file`
Try all names in refine to resolve ambiguity Fixes #426 2013-08-04 17:55:01 +04:00			`029: match_refine and apply by type`
Add test documentation 2013-11-06 08:27:04 +04:00			`030: %reflection for functions running on syntax`
			`031: error reflection`
			`032: control idris via stdin`
			`033: null pointer creation and check`
Add floating point primitives to LLVM backend * implement floating point primitives in LLVM codegen * add a test for the presence of floating point primitives in a given backend 2013-11-19 14:08:59 +04:00			`034: presence of floating point primitives in backends`
Warn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) 2012-10-18 23:52:17 +04:00
			`regxxx: various regression tests`
Regression test for StrLen. 2013-07-11 21:17:11 +04:00			`reg020: working strlen`