1085 Commits

Author	SHA1	Message	Date
Justus Matthiesen	873b3edd29	[ fix #3143 ] traverse as-patterns when constructing terms matching an impossible LHS (#3146) ... * [ fix #3143 ] traverse as-patterns in `getImpossibleTerm` * [ test ] impossible as-pattern	2023-11-23 08:29:15 +00:00
Steve Dunham	af10fbaf94	[ error ] Improve parse errors in ipkg files	2023-11-12 10:09:50 +00:00
Denis Buzdalov	1aff26e94c	[ test ] Reduce the need of frequent golden vals updates in one test	2023-11-09 22:05:36 +00:00
Denis Buzdalov	2c328a51c0	[ elab ] Support more applicative traversals of TTImp	2023-11-09 22:05:36 +00:00
CodingCellist	d80bc1537d	[ base ] Add bindings for ieee Double number consts (#3116)	2023-11-09 14:01:40 +00:00
Steve Dunham	a945b5d2df	[ ffi ] Fix missing structure declarations in scheme ffi	2023-11-09 14:00:20 +00:00
Justus Matthiesen	bc386dab4e	[ cleanup ] bring formatting of sc-graphs in tests back in sync	2023-11-06 20:10:21 +00:00
Justus Matthiesen	e5788a3e86	[ test ] tracking size-change across applications	2023-11-06 20:10:21 +00:00
Justus Matthiesen	f435256812	[ test ] tracking size-change in dot patterns	2023-11-06 20:10:21 +00:00
Justus Matthiesen	2798d8f226	[ cleanup ] update expected test outputs ... Changes to the termination checker brought along some otherwise insignificant changes to debug and error messages.	2023-11-06 20:10:21 +00:00
Denis Buzdalov	64ad807f83	[ deriving ] Try to reduce a type before searching it's showable	2023-10-30 10:07:39 +00:00
G. Allais	bee59d5fde	[ fix ] missing modules in .ipkg files (#3124) ... Additionally, we now have bash options to make sure we will fail hard were this situation to arise once again.	2023-10-27 20:37:00 +01:00
Denis Buzdalov	5f29b0b9c5	[ elab ] Add an ability to inspect in which function we currently are	2023-10-26 15:42:26 +01:00
Denis Buzdalov	50a579fa18	[ elab ] Implement an operation of returning referred defs of a def	2023-10-26 15:42:26 +01:00
Adowrath	ea093ffaed	[ warning ] for incompatible visibilities on forward decls and definitions. (#3063)	2023-10-25 11:24:43 +01:00
Denis Buzdalov	6c35157087	[ ux ] Make isType fail with positioned errors	2023-10-17 18:05:54 +01:00
Aleksei Volkov	3e5d8a54d4	[ fix ] Prevent relative path traversal in elaborator scripts	2023-10-16 09:43:22 +01:00
Steve Dunham	c04404a95b	[ fix #3097 ] Fix issues parsing %logging followed by named impls (#3098) ... Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>	2023-10-13 19:02:58 +01:00
Denis Buzdalov	419a440dad	[ impl ] Support default implicits in named implementations (#3100)	2023-10-13 15:26:42 +01:00
Denis Buzdalov	f7d4b7f4ed	[ base ] Add a bridge between MonadState and Ref	2023-10-13 13:47:31 +01:00
Denis Buzdalov	6815aefbe0	[ elab ] Implement file operations, e.g. applicable for type providers	2023-10-13 13:26:46 +01:00
Denis Buzdalov	cbbd0c8caa	[ elab ] Make %macro-function be callable without the extension	2023-10-11 13:20:12 +01:00
Denis Buzdalov	a5b02747b6	[ re #3066 ] Make the rest of tests to use the same form as the others	2023-10-04 14:34:03 +01:00
Denis Buzdalov	567f019230	[ test ] Set IDRIS2_PREFIX to a local dir when testing	2023-10-04 14:34:03 +01:00
Denis Buzdalov	0c40a76c2c	[ re #2884 ] Move existing test to an appropriate category	2023-10-01 07:16:20 +01:00
Steve Dunham	46483fd120	[ fix ] support .lidr.md and .lidr.tex extensions (#3071)	2023-09-25 22:25:26 +01:00
Denis Buzdalov	3886200d29	[ fix ] Make traverse and friends lazy for LazyList	2023-09-25 19:51:17 +01:00
Denis Buzdalov	a643e3af62	[ elab ] Print script's FC in the bad elaboration script error	2023-09-22 11:55:34 +01:00
Steve Dunham	0029257eec	[ fix ] consider nest when guessing scrutinee (#3070)	2023-09-14 14:29:41 +01:00
Steve Dunham	8c14e9527b	[ test ] move test to correct location	2023-09-07 20:26:18 -07:00
Steve Dunham	e4fe90e1a3	Merge branch 'main' into foo	2023-09-07 20:19:26 -07:00
Guillaume Allais	b4d7bba550	[ cleanup ] use default arguments ... This simplifies most calls to `testsInDir`.	2023-09-07 14:57:22 +01:00
Robert Wright	424bc20c27	Group tests by directory	2023-09-07 14:57:22 +01:00
Robert Wright	2bde9104e0	Add filter_test_dir test utility	2023-09-07 14:57:22 +01:00
Robert Wright	61878ef1b6	Remove trivial testing input files	2023-09-07 14:57:22 +01:00
Robert Wright	09466a96bb	Add testing utilities script	2023-09-07 14:57:22 +01:00
G. Allais	c52b029986	[ new ] function options for case blocks (#3062)	2023-09-01 11:35:52 +01:00
Aleksei Volkov	af7ba2fa67	[ ttc ] Compare modification time with nanosecond precision (#3046)	2023-08-31 11:55:57 +01:00
Guillaume Allais	e3214586a5	[ fix #3057 ] properly handle char literals in comments	2023-08-31 11:52:32 +01:00
Denis Buzdalov	cf9a73f86c	[ prelude ] Add some lacking %tcinlines	2023-08-23 11:04:53 +01:00
Janus Troelsen	694b1650c8	[ racket ] Add library loading (#3049)	2023-08-23 11:04:01 +01:00
Aleksei Volkov	115c9e0889	[ unelab ] Properly unelaborate metavariables originating from %search (#3055) ... * [ unelab ] Properly unelaborate `%search` * [ test ] Added regression test that checks quotation of `%search`	2023-08-23 08:02:11 +01:00
Steve Dunham	0b3e04aef0	update tests for DCon in size change	2023-08-12 13:55:07 -07:00
Steve Dunham	878187d7f7	[ fix ] Totality checker misses indirect references to partial data	2023-08-12 12:57:28 -07:00
Steve Dunham	bde1a66075	[ fix ] Fix pattern match issue with function application in Refl (#3027)	2023-08-04 13:46:04 +01:00
Steve Dunham	f0f776c288	[ error ] Improve error messages for Delay &co	2023-08-04 13:39:39 +01:00
Steve Dunham	b481994bef	[ fix ] Fixes build broken by #3021	2023-08-01 08:01:12 +01:00
scarf	c7abb148e8	feat: even and odd for Nat and Integral (#3021)	2023-07-31 08:36:40 +01:00
André Videla	1fa638494d	[ new ] Fixity access modifier (#3011)	2023-07-31 08:35:16 +01:00
Robert Wright	cbbe761c51	Add fromTTImp, fromName, and fromDecls for custom TTImp, Name, and Decls literals	2023-07-31 08:17:55 +01:00