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 %tcinline
s
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
André Videla
a39bfc6ce3
Merge branch 'main' into constant_fin
2023-07-18 23:46:07 +09: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
5165c79b67
[ fix ] Ensure local defs with no claim are local
2023-07-15 18:18:48 -07:00
Robert Wright
af3c5fd454
Generalize Prelude proof helpers
2023-07-05 16:36:09 +01:00
stefan-hoeck
c1a5be9b5b
[ performance ] make Eq and Ord for Fin run in constant time
2023-07-05 15:58:41 +02: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
Andre Videla
9797a79b53
[ new ] Allow fixities to be hidden with %hide
...
* Change the printing of namespaced operator to show
parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities
2023-06-14 11:19:59 +01:00
Alexander
63fa070efa
add test for parse error let-in in do block
2023-06-13 11:01:42 +03:00
Justus Matthiesen
6c6867490c
[ test ] lazy functions
2023-06-12 11:04:59 +01:00
Aleksei Volkov
e594669210
[ fix #1878 ] Programmer-provided terms should be alwaysReduce
( #2977 )
...
* [ fix ] Programmer-provided terms should be alwaysReduce
This ports Edwin's commit that fixes the original issue back to Idris
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
* [ tests ] Added regression test for #1878
* Updated CHANGELOG.md and CONTRIBUTORS
---------
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
2023-06-01 17:08:02 +01:00
Justus Matthiesen
00af44c708
Ignore UseSide
annotation in non-linear as-patterns ( #2984 )
...
Co-authored-by: Aleksei Volkov <volkov.aa@phystech.edu>
2023-06-01 14:34:57 +01:00
Thomas E. Hansen
5519e5117f
[ test ] Test :doc for laziness primitives
2023-05-30 09:46:24 +02:00
Steve Dunham
d3e896ea09
[ fix ] Improve error messages at end of if statements
2023-05-20 09:16:25 +01:00
Stefan Höck
2739c3a389
[ codegen ] more flexible array implementation on JS backends ( #2966 )
2023-05-14 06:45:50 +01:00
Steve Dunham
edc000c568
[ fix ] Fix issue parsing __LOC__ arguments
2023-05-14 06:45:33 +01:00
Steve Dunham
7221c99e93
[ error ] Improve error messages for indentation issues
2023-05-13 10:25:38 +01:00
Denis Buzdalov
c285ef06dd
[ re #2960 ] Move defs of closures data types to a separate module
2023-05-11 15:31:45 +01:00
Robert Wright
9bfa04921a
Add symmetric and transitive closure relations
2023-05-08 11:53:21 +01:00
stefan-hoeck
3c9393e5a8
[ codegen ] constant fold believe_me
2023-05-06 14:52:14 +01:00
Stefan Höck
e34b5a64f0
[ codegen ] get rid of trivial let statements ( #2961 )
2023-05-06 08:35:17 +01:00
madman-bob
a00b7ee7ec
Public export TTImp reflection functions ( #2947 )
...
Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
Co-authored-by: Ohad Kammar <ohad.kammar@gmail.com>
2023-05-05 10:33:32 +01:00
Denis Buzdalov
55efd7dd7b
[ new ] Add Compose
instances for Bi* interfaces, analogous to present
2023-04-25 12:59:25 +01:00
Steve Dunham
97b7697a0e
[ fix ] Issue in totality checking
2023-04-23 17:42:04 +01:00
Steve Dunham
3ad391d597
[ fix ] codegen issue when using partial case statements in prelude. ( #2952 )
2023-04-23 11:07:04 +01:00
Steve Dunham
9544162bc4
[ new ] Add support for bi-directional pipes on POSIX systems ( resolves #2935 ) ( #2944 )
2023-04-15 09:39:17 -05:00
Steve Dunham
a75161cb20
[ parser ] Improve error message for missing comma or period in forall.
2023-04-07 08:42:42 +01:00
G. Allais
b185f1ff85
[ new ] %unsafe pragma for escape hatches ( #2937 )
2023-04-03 21:42:47 +01:00
Zoe Stafford
442c5b529f
Collect constructors on the left hand side of case alternatives ( #2919 )
...
* [ fix ] collect constructors on LHS of cases alts
* [ tests ] Updated expected
These functions do refer to these constructors at runtime, so this is the correct output
* Update CHANGELOG.md
* [test] update test output again
2023-03-14 15:05:19 +00:00
G. Allais
b5197d5c5d
[ fix ] partial evaluation implementation ( #2899 )
2023-03-07 08:31:29 +00:00
Denis Buzdalov
b5fe607f4e
[ regression ] Do toFullNames
only when logging happens
2023-03-06 12:56:39 +00:00
CodingCellist
7972c6acbd
[ new ] Implement bit-rotation operators ( #2903 )
...
* [ new ] Implement bit-rotation operators
Whereas `shiftR` and `shiftL` throw bits off the edge, the `rotR` and
`rotL` operations wrap the bits around to the start of the bit-stream.
* [ test ] visualise bit patterns instead
* [ fix ] print bit patterns the right way around
---------
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-03-04 14:41:54 +00:00
André Videla
24a69089bc
Merge pull request #2900 from mjustus/fix2895
...
[ fix #2895 ] don't erase argument when type is erased
2023-03-04 09:34:28 +00:00
CodingCellist
ba24892e2f
[ new ] Couple of useful things for Vect ( #2904 )
...
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: André Videla <andre.videla@gmail.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-03-03 15:58:44 +00:00
G. Allais
310a8f12cd
[ new ] missing buffer primitives ( #2893 )
2023-02-26 17:50:52 +00:00
Andre Videla
0f4464a690
add logs to linear check
2023-02-25 22:29:34 +00:00
Andre Videla
891c1751ed
add tests
2023-02-25 12:19:29 +00:00
Alex1005a
a9ad1dd0cc
[ contrib ] Performance improvement gcd in Data.Nat.Factor ( #2886 )
2023-02-22 12:08:49 +00:00
G. Allais
dc1b5387b8
[ re #2832 ] warn about conflicting fixity declarations ( #2889 )
2023-02-19 16:29:10 +00:00
pinselimo
2dbb824a93
[ doc ] Add constructor docstrings ( #2789 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-02-19 10:15:39 +00:00
Guillaume Allais
3bccf8e212
[ fix ] highlight record constructor
2023-02-13 15:41:56 +00:00
Guillaume Allais
f76c4c4307
[ fix ] respect visibility in forward data declarations
2023-02-08 22:00:25 +00:00
Justus Matthiesen
6edbfc59a5
[ test ] non-terminating function from issue #2448
2023-02-08 16:13:04 +00:00
Justus Matthiesen
914d68858b
[ termination ] faithful implementation of size-change graph termination analysis
...
- call sequences in termination errors now carry location information
- new error message (`BadPath`) for late-starting loops
- [ fix ] transitive closure of size-change graphs no longer ignores function arguments
- update existing tests accordingly
2023-02-08 16:13:04 +00:00
Justus Matthiesen
2b54c23073
[ test ] examples from termination paper
2023-02-08 16:13:04 +00:00
G. Allais
fba9f16a1c
[ fix ] positivity checker: assert_total & Lazy ( #2876 )
2023-02-07 12:35:33 +00:00
Steve Dunham
464797944a
[ error ] Fix location of type errors in do block pattern matching
2023-02-04 23:07:49 +00:00
Guillaume Allais
21fa60ae6a
[ re #2871 ] Fix the resolvedN issue for good
2023-02-04 16:10:47 +00:00
Stefan Höck
f6a731695d
[ new ] constructor plus trivial impl for Interpolation ( #2871 )
...
* [ new ] constructor plus trivial impl for Interpolation
* [ doc ] update CHANGELOG
* [ test ] adjust expected test output
2023-02-04 07:47:28 -06:00
Mathew Polzin
ad12f8335c
[ new ] popen
/pclose
for the NodeJS backend. ( #2857 )
...
* implement popen and pclose (to an extent) for NodeJS
* bring node020 back into tests.
* ah, I see what was being done here. Fix the idris for the test.
* fix test's unreachable clause warning
* fix expectation
* Add note to CHANGELOG
* small tweaks to get popen into merge-ready state.
2023-01-30 09:38:42 -06:00
G. Allais
966a4813fb
[ fix ] respect totality annotations for data ( #2862 )
2023-01-26 11:03:22 +00:00
Denis Buzdalov
f4b44ba109
[ prelude ] Make some higher-kinded functions be tc-inlined
2023-01-25 16:51:11 +00:00
Marek L
7ec96cea7f
[ doc ] Remove typo from Prelude.plus
doc string and
...
reformat doc string for `Prelude.minus`
2023-01-24 23:35:03 +00:00
Mathew Polzin
4bedaac811
[ fix ] make color output toggling simpler and also more robust. ( #2848 )
...
* make color output toggling simpler and also more robust
* don't unintentionally assert that tests are run in an environment where colors are turned on.
* Update src/Idris/Env.idr
2023-01-22 13:35:57 -06:00
Denis Buzdalov
936b7270ae
[ prelude ] Add lacking implementation of Traversable
for Pair
2023-01-09 15:56:21 +00:00
Stefan Höck
8db12f5a49
[ performance ] improve some Char functions ( #2839 )
2023-01-06 09:08:38 +00:00
Steve Dunham
a84a5a32d9
Fix at-pattern leak in recursive with blocks ( #2834 )
2022-12-28 09:08:09 +00:00
Zoe Stafford
d82c5d633f
Merge pull request #2815 from mjustus/test_pkg017_ignore
...
[ cleanup ] ignore generated file
2022-12-22 15:02:50 +00:00
Guillaume Allais
1092804726
[ fix #2821 ] Failing blocks should force delayed holes
2022-12-21 11:16:26 +00:00
G. Allais
0194539ef7
[ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings ( #2819 )
...
* [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings
* [ fix ] the point is to test whitespace being ignored
* [ fix ] golden values
2022-12-17 18:12:39 +00:00
G. Allais
2f55a3ef8a
[ fix ] elaboration of records' telescopes of parameters ( #2816 )
2022-12-15 17:55:50 +00:00
Justus Matthiesen
5718be2b45
[ cleanup ] ignore generated file
2022-12-12 14:47:33 +00:00
Justus Matthiesen
e673d05a67
[ fix ] jump-to-definition (":name-at" IDE command) ( #2811 )
2022-12-09 17:02:57 +00:00
Markus Pfeiffer
c3bbdb30a1
Add mustWork
in GADT data declaration parser ( #2805 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-12-09 16:04:11 +00:00
locriacyber
cb30d7cda8
Install *.ttm on idris2 --install
( #2796 )
...
Co-authored-by: Justus Matthiesen <mail@justusmatthiesen.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-12-08 21:06:17 +00:00
Ruslan
d44ddc7f11
Let qualified do-notation apply to pure
and to idiom brackets ( #2786 )
2022-12-07 22:27:58 +00:00
Ellis Kesterton
9931f35b6b
Improve parser error messages when using reserved identifiers in decls ( #2803 )
...
Co-authored-by: Ellis Kesterton <erk4@st-andrews.ac.uk>
2022-12-07 16:09:26 +00:00
Guillaume Allais
001f48fba8
[ test ] for io_bind inlining
2022-12-06 11:55:28 +00:00
G. Allais
fcbd9e9190
[ fix #2794 ] Do not ignore notinline lets in identity detection ( #2795 )
2022-12-06 11:41:30 +00:00
G. Allais
85bb822f3b
[ perf ] manually eta-expand unsaturated io_bind calls ( #2785 )
2022-12-01 15:31:00 +00:00
Steve Dunham
f443723f4e
[ parser ] fix issue where indentation is not checked in record parameters
2022-11-25 08:22:37 +00:00
Steve Dunham
56a9bc6be4
[ error ] Improve locality of parse errors in implicit arguments
2022-11-21 10:40:40 +00:00
Tim Engler
bff18428b4
Added seqL to Control.App and updated docs to fix #2761
...
Also updated test real002 to use the actual Control.App from
libs/base/Control/App.idr. Before it was using a different version that
existed within its test directory, tests/idris2/real002/Control/App.idr
2022-11-21 10:39:43 +00:00
Hattori, Hiroki
5c9f8e36a1
[ RefC ] Add 16 and 32 bit access to base/Data.Buffer . ( #2609 )
...
* Fix symbom mangling
* Revert "Fix symbom mangling"
This reverts commit 6481e80155
.
* Fix typo
* [RefC] Add missed prims of setBuffer* .
* [ fix ] formatting
* [ re #2609 ] Use 'UInt' instead of 'Word'
More descriptive/to the point / Less assumed knowledge.
There are no *LE suffixes for UInt8, since endianness is to do with
multiple bytes and UInt8 is a single one.
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
2022-11-15 12:15:06 +01:00
CodingCellist
70ef197cf6
[ base ] Deprecate setByte in favour of setBits8 ( #2764 )
...
* [ base ] Deprecate setByte in favour of setBits8
Deprecate getByte; fix Core.Binary.Prims
Along with `setByte`, the `getByte` function should similarly be
deprecated since it also assumes the value will have the given size,
rather than guaranteeing it in the type.
CI highlighted some required changes in `Core.Binary.Prims` thanks to
`-Werror`. The fix was to add some `cast` calls where the old `getByte`
and `setByte` used to be.
The RefC buffer test will need updating once we remove the functions
completely. Added a note for future peeps.
2022-11-15 10:42:07 +01:00
Denis Buzdalov
f5f7e2eb80
[ error ] Make failing IAlternative
w/ FirstSuccess
print all errors
2022-11-15 10:28:59 +01:00
Steve Dunham
85c93c8018
[ error ] Add FC for errors on interface constructors ( #2769 )
2022-11-12 22:17:42 -08:00
Steve Dunham
ea733181c5
[ error ] Add an FC to record constructors for better error messages ( #2769 )
2022-11-12 21:59:16 -08:00