ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity
e5bc47eec3
Idris-dev/test
History
David Raymond Christiansen e5bc47eec3 Distinguish postulate providers and type providers at use site 
This is not backwards compatible, but as far as I know, there are no
users of postulate providers who are not me.

The old system allowed both the definition of the provider and the use
site to be involved in the determination of what is a postulate and what
is not. This is not good - users should always be in full control of
this.

The new implementation has two syntaxes:

%provide (x : t) with p

%provide postulate x with p

The first is the type provider syntax we know and love. The second
requires that the provider in fact return a type, which is then made
into the type of the resulting postulate.
2014-06-05 13:53:03 +02:00
..
basic001 Fix reg005. 2014-04-11 09:08:27 +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 Categorise tests 2014-01-30 17:24:08 +00: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 Add application context to all error messages 2014-03-22 10:01:11 +01:00
basic010 Add a timeout. 2014-05-29 13:55:04 +01: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 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
dsl002 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
effects001 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
effects002 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
error001 Categorise tests 2014-01-30 17:24:08 +00:00
error002 Categorise tests 2014-01-30 17:24:08 +00:00
error003 Support mixed induction/coinduction with Inf type 2014-03-22 17:46:14 +00:00
error004 Coverage checker fix 2014-04-02 00:04:07 +01:00
ffi001 Avoid pollution of test case with ANSI codes 2014-02-04 13:27:57 +01:00
ffi002 Test updates for executor and type provider update 2014-02-03 11:07:11 +01: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 Distinguish postulate providers and type providers at use site 2014-06-05 13:53:03 +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 Fix interactive editing and tests 2014-05-02 14:36:34 +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
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 Remove | annotation, make Force/Delay implicit 2014-02-13 18:17:26 +00:00
literate001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives001 Categorise tests 2014-01-30 17:24:08 +00:00
primitives002 Categorise tests 2014-01-30 17:24:08 +00:00
primitives003 Categorise tests 2014-01-30 17:24:08 +00:00
proof001 Categorise tests 2014-01-30 17:24:08 +00:00
proof002 Update for new unification error messages 2014-03-20 20:00:18 +01:00
proof003 Add --nowarnreach to two tests. 2014-04-11 09:10:26 +01:00
proof004 Categorise tests 2014-01-30 17:24:08 +00:00
proof005 'Reject' cases to default arg substitution tests. 2014-04-06 02:06:46 +03:00
proof006 'Reject' cases to default arg substitution tests. 2014-04-06 02:06:46 +03:00
proof007 Tests on default args and substitution 2014-04-06 01:22:27 +03: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 Added nested record access syntax 2014-05-02 08:58:57 +02:00
reg001 Remove apply from reg001 since it's in the prelude! 2014-01-18 19:52:21 +00:00
reg002 Make --nowarnreach the default (for now). 2014-04-11 09:10:26 +01:00
reg003 Implicit "module Main" added 2014-01-18 22:11:59 +00: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 Fix earlier %assert_total propagation 2014-01-03 01:31:01 +00:00
reg007 Support mixed induction/coinduction with Inf type 2014-03-22 17:46:14 +00:00
reg008 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg009 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg010 Rewrite error printing to use the pretty-printer 2014-01-28 13:57:11 +01:00
reg011 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg012 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00: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 Reset test runscripts to mode 0755 2013-11-18 22:36:55 +00:00
reg018 Merge pull request #1204 from david-christiansen/totality-warning 2014-05-08 17:17:15 +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 Fix usage in reg025. 2014-04-11 09:10:26 +01:00
reg026 Unification changes 2014-02-17 00:01:05 +00:00
reg027 Unification changes 2014-02-17 00:01:05 +00:00
reg028 Update result of reg028 2013-11-30 13:53:23 +00:00
reg029 started working on new cmd arg parser 2014-05-14 18:39:47 +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 Add application context to all error messages 2014-03-22 10:01:11 +01:00
reg035 Evaluator bug fix 2014-02-21 17:57:11 +00: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 Fix precedence of application vs arrows in pprint 2014-05-04 19:43:12 +02:00
reg042 Add a regression test. 2014-04-24 18:14:52 +01:00
reg043 Fix precedence of application vs arrows in pprint 2014-05-04 19:43:12 +02:00
reg044 Check that proof steps introduce no new problems 2014-05-22 12:14:51 +01: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 Categorise tests 2014-01-30 17:24:08 +00:00
totality003 Add assert_smaller function 2014-02-01 22:52:22 +00: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 Tweak notion of recoverability in coverage checker 2014-04-20 21:51:34 +01: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 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial005 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
tutorial006 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00
Makefile Replace records003 test 2014-05-04 13:27:53 +01: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

README 

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