Justus Matthiesen
ba19fae07a
[ fix ] handle printing of empty matrices gracefully
2023-11-06 20:10:21 +00:00
Justus Matthiesen
39f3aeeb08
[ cleanup ] remove 1 suffix from Vector1 functions
2023-11-06 20:10:21 +00:00
Justus Matthiesen
291d60da08
[ cleanup ] move auxiliary function to where block
2023-11-06 20:10:21 +00:00
Justus Matthiesen
03484f2dfa
[ cleanup ] split Vector and Vector1 into separate namespaces
2023-11-06 20:10:21 +00:00
Justus Matthiesen
c36be9291d
[ doc ] clarification on neutrals
2023-11-06 20:10:21 +00:00
Justus Matthiesen
c36625d1db
[ cleanup ] remove duplicate and unused functions
2023-11-06 20:10:21 +00:00
Justus Matthiesen
d9cc448d3e
[ debug ] sc-graphs now have labels "l" and "r" for LHS and RHS
2023-11-06 20:10:21 +00:00
Justus Matthiesen
8c7c59a5d0
[ new ] labels for pretty-printed sparse matrices
2023-11-06 20:10:21 +00:00
Justus Matthiesen
8822040f37
[ new ] replicateChar, an analogue to spaces but for arbitrary Chars
2023-11-06 20:10:21 +00:00
Justus Matthiesen
80657feb34
[ doc ] sparse matrix invariants
2023-11-06 20:10:21 +00:00
Justus Matthiesen
b3c186900c
[ fix #2954 ] use matrices to represent sc-graphs
...
We also update sc-graph generation to
- fully traverse `As` patterns
- go under `Dotted` patterns
- consider `f x <= f`
2023-11-06 20:10:21 +00:00
Justus Matthiesen
c4677edc5f
[ new ] Pretty instance for SizeChange
2023-11-06 20:10:21 +00:00
Justus Matthiesen
8a9bf396ea
[ new ] semiring instance for SizeChange
2023-11-06 20:10:21 +00:00
Justus Matthiesen
aac6e8600c
[ new ] sparse matrices
2023-11-06 20:10:21 +00:00
Justus Matthiesen
4f7f5a2ed4
[ cleanup ] use information order for SizeChange
2023-11-06 20:10:21 +00:00
Justus Matthiesen
d76361e0f6
[ refactor ] move SizeChange to a separate file
2023-11-06 20:10:21 +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
Steve Dunham
73507a826b
[ cleanup ] remove duplicate copy of header parsing ( #3122 )
2023-10-27 13:08:17 +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
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
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
Steve Dunham
46483fd120
[ fix ] support .lidr.md and .lidr.tex extensions ( #3071 )
2023-09-25 22:25:26 +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
e4fe90e1a3
Merge branch 'main' into foo
2023-09-07 20:19:26 -07: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
Ohad Kammar
d3dc9b7c44
[ refactor ] S-Exp protocols to depend on fewer Idris modules ( #3060 )
2023-08-31 11:53:14 +01:00
Guillaume Allais
e3214586a5
[ fix #3057 ] properly handle char literals in comments
2023-08-31 11:52:32 +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
Jens Petersen
48dbc3251b
implement DESTDIR support for distros
...
both 'make install' and 'idris2 --install*' should respect DESTDIR now
2023-08-22 16:44:13 +01: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
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
Steve Dunham
8d7791ba55
[ base ] Add getTermCols and getTermLines to base library and fix pri… ( #3009 )
2023-07-18 09:42:47 -05:00
Steve Dunham
113c3930f3
[ fix ] deduplicate definedInBlock results
2023-07-16 09:01:13 -07:00
Steve Dunham
5165c79b67
[ fix ] Ensure local defs with no claim are local
2023-07-15 18:18:48 -07:00
CodingCellist
6729fa8c89
Revert "Treat unit types as erased in constructors ( #3002 )"
...
This reverts commit 677acf0d84
2023-07-07 17:48:07 +02:00
Zoe Stafford
677acf0d84
Treat unit types as erased in constructors ( #3002 )
...
* Treat unit types as erased in constructors
* Cleanup + dump ttc version
* Update CHANGELOG.md
2023-07-05 19:51:34 +01:00
Robert Wright
af3c5fd454
Generalize Prelude proof helpers
2023-07-05 16:36:09 +01:00
Steve Dunham
ecf4765c4b
[ fix ] Fix issue with eager evaluation of crashing functions ( fixes #3003 ) ( #3004 )
...
* [ fix ] Fix issue with eager evaluation of crashing functions
* Mark functions that call unsafe builtins as non-constant
* Better detection of crash primop when deciding if functions can be constant
2023-06-28 08:32:48 +01:00
Denis Buzdalov
5dcf62499d
[ elab ] Make elab scripts be able to record warnings ( #2999 )
2023-06-19 16:34:19 +01:00
