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
reg029: executor doesn’t crash receiving a NULL String from C
-												Fix obscure where naming bug

											
										
										
											2011-12-22 02:06:26 +04:00
+								Tests:
 : Well-typed interpreter
 : Universe checking
 : Literate source and string processing
 : File operations
 : Num class resolution [regression]; span & break; ad-hoc overloading
-												New test

											
										
										
											2012-01-01 23:59:46 +04:00
+: Provisional definitions; class resolution in patterns
-												Test for idiom brackets and Applicative class

											
										
										
											2012-01-04 15:05:37 +04:00
+: 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
+: case and pattern matching let
-												Numeric ranges [a..b], [a,b .. c] and list monad

											
										
										
											2012-01-06 19:11:11 +04:00
+: ranges and list monad
-												Added record test

											
										
										
											2012-01-28 01:21:31 +04:00
+: total
 : record projection and update
-												Check patterns are inaccessible

											
										
										
											2012-04-24 17:57:55 +04:00
+: various error regressions
-												Added binding form to syntax rules (and updated tutorial accordingly)

											
										
										
											2012-05-30 13:32:57 +04:00
+: 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
+: resource DSL
 : 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
+: codata
-												Deal with higher order recursive arguments in size change graphs

											
										
										
											2012-10-26 18:40:44 +04:00
+: mutually recursive totality checking
-												Added raw (non-typesafe) message passing library
(System.Concurrency.Raw)

											
										
										
											2012-10-30 17:29:22 +04:00
+: Message passing concurrency (raw form)
-												Only apply unique implicit conversions (and add test)

											
										
										
											2013-02-25 14:39:14 +04:00
+: magic with
 : implicit conversions
-												Added effects package and associated tests

											
										
										
											2013-03-01 17:52:51 +04:00
+: effects
-												Test for dynamic loading of C libs + interpreter IO

											
										
										
											2013-03-21 21:57:54 +04:00
+: dynamic C library loading and interpreter IO
-												Added new tests to the test README

											
										
										
											2013-04-04 18:03:21 +04:00
+: trivial (non-I/O) type providers
 : interpreter I/O
-												Test for simple file-based type providers

											
										
										
											2013-04-23 01:01:23 +04:00
+: memory effects
 : 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
+: class constraints in using block
-												Add test documentation

											
										
										
											2013-11-06 08:27:04 +04:00
+: 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
+: match_refine and apply by type
-												Add test documentation

											
										
										
											2013-11-06 08:27:04 +04:00
+: %reflection for functions running on syntax
 : error reflection
 : control idris via stdin
 : 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
+: 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
-												Add regression test for possibly-null foreign strings in the executor

											
										
										
											2013-12-20 23:55:22 +04:00
+								reg029: executor doesn’t crash receiving a NULL String from C
-												Regression test for StrLen.

											
										
										
											2013-07-11 21:17:11 +04:00