Idris-dev/test
David Raymond Christiansen f1e161d562 A new primitive tactic for getting source locations
The tactic sourceLocation fills the hole with the current location in
the file. If such information is unavailable, it fails.

This is to be used by DSL implementers to provide useful error
messages that can't be caught at type-check time. Additionally, it may
prove useful for debugging and assertion libraries, so they can report
errors.

Because the tactic merely fills out an implicit argument in a particular
way, it doesn't break referential transparency, at least not of the core
language. This is similar to the technique used in Scala Virtualized.
2014-11-27 21:36:46 -08:00
..
basic001 Fix use of %flag in test basic001 2014-11-09 12:10:38 +01:00
basic002 Fix usage in basic002. 2014-04-11 09:10:25 +01:00
basic003 Categorise tests 2014-01-30 17:24:08 +00:00
basic004 Categorise tests 2014-01-30 17:24:08 +00:00
basic005 Fixed some tests broken under renaming 2014-09-26 07:34:38 +02:00
basic006 Remove implicit qualifier for 'effect' 2014-05-25 17:05:27 +02:00
basic007 Return test033 to the original state. 2014-04-11 09:10:25 +01:00
basic008 Categorise tests 2014-01-30 17:24:08 +00:00
basic009 First renaming attempt 2014-09-26 07:34:28 +02:00
basic010 Fixed some tests broken under renaming 2014-09-26 07:34:38 +02:00
basic011 Data.Hash library 2014-10-09 08:46:28 +02:00
bounded001 Port Haskell's Bounded class 2014-02-21 14:47:24 +01:00
buffer001-disabled Temporarily disable buffer001 test 2014-02-01 20:36:51 +00:00
dsl001 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
dsl002 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
dsl003 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
effects001 Replace 'effects' with neweffects 2014-07-15 21:35:35 +02:00
effects002 Fixed some tests broken under renaming 2014-09-26 07:34:38 +02:00
error001 Categorise tests 2014-01-30 17:24:08 +00:00
error002 Categorise tests 2014-01-30 17:24:08 +00:00
error003 Pattern variables should be lifted to top level 2014-11-27 11:35:44 +00:00
error004 Fixed some accidentally wrong renamings. 2014-09-26 13:44:43 +02:00
ffi001 Avoid pollution of test case with ANSI codes 2014-02-04 13:27:57 +01:00
ffi002 Fixed broken provider test after providing () as Unit too 2014-09-26 14:52:27 +02:00
ffi003 Update test to avoid interactive-mode control chars 2014-02-04 13:50:45 +01:00
ffi004 Remove reliance on interactive output from test ffi004 2014-02-04 14:29:05 +01:00
ffi005 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
folding001 Tests for tail recursive implementations of foldr 2014-03-11 18:42:05 +01:00
folding002 Change type class top level method generation 2014-05-13 00:34:11 +01:00
idrisdoc001 Namespaces only containing private members is now correctly considered empty 2014-04-30 15:06:21 +02:00
idrisdoc002 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc003 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc004 Fixed typo 2014-04-25 01:52:07 +02:00
idrisdoc005 Removed test backups and converted tests to pure bash scripts 2014-04-23 02:13:29 +02:00
idrisdoc006 Updated idrisdoc006 to be more throughly 2014-04-30 16:37:45 +02:00
idrisdoc007 Made test resistant to differences among command implementations 2014-04-23 10:20:25 +02:00
idrisdoc008 Added IdrisDoc test which verifies inclusion of abstract and public namespace members 2014-04-30 17:08:42 +02:00
interactive001 First renaming attempt 2014-09-26 07:34:28 +02:00
interactive002 Improve inference in monadic code 2014-02-10 10:11:00 +00:00
interactive003 Fix interactive editing and tests 2014-05-02 14:36:34 +02:00
interactive004 Add :refine (:ref) command for refining a hole 2014-04-17 15:41:06 +01:00
interactive005 Support type errors in docstrings 2014-10-18 09:09:39 -07:00
interactive006 Allow REPL to run on another port (flag --port) 2014-09-27 13:54:26 +02:00
io001 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
io002 Categorise tests 2014-01-30 17:24:08 +00:00
io003 Fixed lack of renaming of lift to Lift in test 2014-09-26 16:58:28 +02:00
literate001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives002 Add test for new float primitive prim__negFloat 2014-09-22 11:56:03 +01:00
primitives003 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
proof001 First renaming attempt 2014-09-26 07:34:28 +02:00
proof002 Fixed some accidentally wrong renamings. 2014-09-26 13:44:43 +02:00
proof003 First renaming attempt 2014-09-26 07:34:28 +02:00
proof004 Categorise tests 2014-01-30 17:24:08 +00:00
proof005 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
proof006 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
proof007 Use a zipper-like proof state 2014-08-03 21:14:50 +01:00
quasiquote001 Renamed VoidElim to void in order to ensure further consistency 2014-10-11 20:52:06 +02:00
quasiquote002 Add goal types to quasiquotes. 2014-06-30 18:49:22 +02:00
quasiquote003 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
quasiquote004 First renaming attempt 2014-09-26 07:34:28 +02:00
records001 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
records002 Rename record002 test to the correct name! 2014-05-01 21:39:34 +02:00
records003 Generate better record projection types 2014-07-16 14:02:37 +02:00
reg001 Remove apply from reg001 since it's in the prelude! 2014-01-18 19:52:21 +00:00
reg002 Renamed VoidElim to void in order to ensure further consistency 2014-10-11 20:52:06 +02:00
reg003 Better treatment of unbound implicits 2014-07-08 02:40:37 +01:00
reg004 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg005 Categorise tests 2014-01-30 17:24:08 +00:00
reg006 First renaming attempt 2014-09-26 07:34:28 +02:00
reg007 First renaming attempt 2014-09-26 07:34:28 +02:00
reg009 Fixed some accidentally wrong renamings. 2014-09-26 13:44:43 +02:00
reg010 Inline with blocks 2014-08-19 16:21:00 +01:00
reg011 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg012 Renamed VoidElim to void in order to ensure further consistency 2014-10-11 20:52:06 +02:00
reg013 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg014 Add Prelude.Vect.transpose 2014-05-30 16:44:14 +02:00
reg015 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg016 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg017 First renaming attempt 2014-09-26 07:34:28 +02:00
reg018 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
reg019 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg020 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg021 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg022 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg023 Rewrite error printing to use the pretty-printer 2014-01-28 13:57:11 +01:00
reg024 Adjust tests to the changed String show instance 2013-11-25 18:10:46 +01:00
reg025 Finished making standard library naming consistent 2014-09-26 07:34:38 +02:00
reg026 Fixed some accidentally wrong renamings. 2014-09-26 13:44:43 +02:00
reg027 Unification changes 2014-02-17 00:01:05 +00:00
reg028 Inline with blocks 2014-08-19 16:21:00 +01:00
reg029 fix missing tests 2014-06-07 22:01:16 +02:00
reg030 Fix reg030. 2014-05-29 15:44:00 +01:00
reg031 Make reg031 char-sign-indifferent. 2014-01-19 22:05:11 +00:00
reg032 Categorise tests 2014-01-30 17:24:08 +00:00
reg033 Fix silly name shadowing bug and add new test 2014-02-04 18:03:18 +00:00
reg034 First renaming attempt 2014-09-26 07:34:28 +02:00
reg035 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
reg036 Fix parameter name propagation 2014-02-22 12:15:49 +00:00
reg037 Treat (=) as a special function name. 2014-03-05 12:46:23 +01:00
reg038 Tweak scoping rules in instance generation 2014-03-06 11:47:49 +00:00
reg039 Fix test reg039 and add it to idris.cabal 2014-04-15 13:26:39 +02:00
reg040 Rename test reg040 to avoid clash 2014-04-20 16:42:15 +01:00
reg041 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
reg042 Add a regression test. 2014-04-24 18:14:52 +01:00
reg044 First renaming attempt 2014-09-26 07:34:28 +02:00
reg045 Deal with 'Delay' in case building properly 2014-06-09 20:48:03 +01:00
reg046 Remove dodgy unification hack 2014-07-11 14:26:30 +01:00
reg047 Fixed some accidentally wrong renamings. 2014-09-26 13:44:43 +02:00
reg048 Fixed bug regarding insertion in SortedMap. 2014-07-19 20:34:12 +02:00
reg049 Renamed VoidElim to void in order to ensure further consistency 2014-10-11 20:52:06 +02:00
reg050 update test/reg050/expected [2] 2014-11-02 23:25:34 +01:00
reg051 Store parameters in function types 2014-08-08 13:06:03 +01:00
reg052 Enabled reg052 in travis and update its output 2014-10-07 17:35:11 +01:00
reg053 Unification fix for chains of solutions 2014-10-26 11:59:52 +00:00
sourceLocation001 A new primitive tactic for getting source locations 2014-11-27 21:36:46 -08:00
sugar001 Categorise tests 2014-01-30 17:24:08 +00:00
sugar002 Categorise tests 2014-01-30 17:24:08 +00:00
sugar003 Categorise tests 2014-01-30 17:24:08 +00:00
sugar004 Syntax for failures in pattern matching let/<- 2014-03-07 20:57:43 +00:00
totality001 Don't try to compile a test that doesn't have main 2014-05-06 19:55:20 +02:00
totality002 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
totality003 Fix a bug in qsort 2014-07-18 00:58:54 -07:00
totality004 Update test for totality warnings 2014-05-06 19:57:31 +02:00
totality005 Update for totality warnings 2014-05-06 19:50:32 +02:00
totality006 Really replaced lteZero with LTEZero 2014-09-26 18:38:51 +02:00
totality007 Stop building packages if there are totality mismatches 2014-05-09 20:48:41 +02:00
totality008 Find negative occurrences in positivity checker 2014-05-28 23:27:12 +02:00
tutorial001 Fix regression with data declarations in where 2014-03-10 20:47:41 +00:00
tutorial002 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial003 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial004 Removed '_|_' as a built in declaration and renamed it to 'Void', 2014-10-11 20:00:19 +02:00
tutorial005 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial006 Inline with blocks 2014-08-19 16:21:00 +01:00
unique001 Really fix output of unique001a... 2014-08-22 21:09:16 +01:00
unique002 Don't propagate unique names to 'where' 2014-08-26 09:25:10 +01:00
unique003 Fix universe errors, update tests 2014-08-22 20:31:11 +01:00
Makefile Take basic011 out of the javascript test suite 2014-10-09 08:46:28 +02:00
mktest.pl Change from shebangs with absolute references to using /usr/bin/env 2013-11-18 17:10:00 +00:00
README Added IdrisDoc tests 2014-04-22 23:44:15 +02:00
runtest.pl Add assert_smaller function 2014-02-01 22:52:22 +00:00

Tests are categorised as follows:

basic:       Basic language features, some complete programs
dsl:         Embedded DSLs and features to support DSL development
effects:     Effects package
error:       Error messages and error reflection
ffi:         FFI calls, including type providers
idrisdoc:    Documentation tool functionality
interactive: Interactive editing, proof search
io:          IO monad
literate:    .lidr files; literate programming
primitives:  Primitive types
proof:       Theorem proving, tactics
sugar:       Syntactic sugar, syntax extensions
totality:    Totality checking
tutorial:    Examples from the tutorial

reg:         Regression tests, covering previous bug fixes