Commit Graph

1055 Commits

Author SHA1 Message Date
Katarzyna Marek
a2c82e934e
[ contrib ] Sufficient view of lists (#2841) 2023-02-22 12:13:13 +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
crisoagf
7f9db70e15
Add PreorderReasoning comforts (#2778)
* Add PreorderReasoning comforts

* Drop interface approach in favour of computation

* Update libs/base/Syntax/PreorderReasoning.idr

---------

Co-authored-by: Cristóvão Gomes Ferreira <crisoagf@melo-gibson>
Co-authored-by: Ohad Kammar <ohad.kammar@gmail.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
CI integration co-authored-by: @stefan-hoeck
2023-02-17 17:47:54 +00:00
Stefan Höck
b543daf5ab
[ contrib ] move SortedMap and SortedSet to base (#2884) 2023-02-16 11:02:43 -06:00
Zoe Stafford
ff822a747b
Js char io (#2887)
* Implement `{get,put}Char` for javascript backend

* Update changelog
2023-02-13 15:48:07 +00:00
Guillaume Allais
b173267f50 [ cleanup ] now that we can assert_total on data 2023-02-08 17:42:02 +00:00
G. Allais
7c66d10eae
[ papers ] Type-based Divide & Conquer (#2860) 2023-02-08 17:19:24 +00:00
Alex1005a
f3e8970f2c
Adding new properties to Data.Nat.Order.Properties (#2879)
* Add succLeftLte function

* Refactor fuelLemma

* Removal of redundant function and rename succLeftLte to decomposeLte

* Fix the style issues
2023-02-07 07:58:41 +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
Denis Buzdalov
bbe96929f1 [ minor, base ] Relax requirement of the These.bifold 2023-01-26 22:15:15 +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
G. Allais
ea4a4c0f85
[ base ] fix the definition of die (#2854) 2023-01-19 11:09:28 +00:00
Mathew Polzin
24ac56de88
Moving Data.List.HasLength into base (#2844) 2023-01-16 00:07:21 -06:00
Denis Buzdalov
936b7270ae [ prelude ] Add lacking implementation of Traversable for Pair 2023-01-09 15:56:21 +00:00
Mathew Polzin
4005b40a95
[new] Vect.Quantifiers.All QoL (#2843)
* Add Show for Vect.All

* Add an alias for HVect to Data.Vect.Quantifiers.All

* Add a few utilities for Vect.Quantifiers.All to make it more at home in listy uses.

* Add CHANGELOG entries.
2023-01-09 00:57:00 -06:00
Stefan Höck
8db12f5a49
[ performance ] improve some Char functions (#2839) 2023-01-06 09:08:38 +00:00
Zoe Stafford
ae2d4efc17 add javascript support to System.Clock
This may behave incorrectly when used with web workers
2022-12-22 11:47:44 +00:00
Zoe Stafford
18ffb852de export {to,from}Nano in System.Clock
also rename some arguments and add docs
2022-12-21 15:49:32 +00:00
Denis Buzdalov
f4ebcadfad [ base ] Add forgetting conversions of Vect.Quantifiers 2022-12-20 16:36:27 +00:00
G. Allais
2f55a3ef8a
[ fix ] elaboration of records' telescopes of parameters (#2816) 2022-12-15 17:55:50 +00:00
Denis Buzdalov
ff6afb0c59 [ minor ] Make NotBothZero parameter of standard gcd to be erased 2022-12-05 15:10:16 +00:00
Denis Buzdalov
8d7b993cca [ cleanup ] Use several library functions instead of their code 2022-12-05 15:10:16 +00:00
Denis Buzdalov
33fe3f44db [ cleanup ] Clean up existing code in the Arrow module 2022-12-05 15:10:16 +00:00
Guillaume Allais
99eda4dd2b [ papers ] fill last hole in lambda pi formalisation 2022-12-05 15:02:04 +00:00
G. Allais
85bb822f3b
[ perf ] manually eta-expand unsaturated io_bind calls (#2785) 2022-12-01 15:31:00 +00:00
G. Allais
f96c5ca596
[ papers ] LambdaPi (#2780) 2022-12-01 13:48:48 +00:00
0xd34df00d
c6a8c9e7a7 [ base ] Move the worker outside of the Vect's reverse definition 2022-11-21 10:52:47 +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
Robert Wright
b2c42280bb Erase Fin fromInteger upper bound 2022-11-11 15:34:58 +00:00
Guillaume Allais
8556c81014 [ new ] typed ABT 2022-11-04 16:20:46 +00:00
G. Allais
fd46e31da3
[ new ] typed Krivine (#2749) 2022-11-04 10:05:31 +00:00
stefan-hoeck
6f5b19c389 [ cleanup ] bifoldMap already in Prelude 2022-11-03 14:11:15 +00:00
G. Allais
ad817538e0
[ new ] typed SECD (#2743) 2022-11-02 12:58:13 +00:00
G. Allais
4cd38a8c5d
[ new ] deriving Show (#2741) 2022-11-02 11:57:07 +00:00
G. Allais
ee8113bb9d
[ papers ] A Completely Unique Account of Enumeration (#2659) 2022-11-01 16:31:57 +00:00
Stefan Höck
85ddafbac5
[ fix ] bump version of linear and papers packages (#2735) 2022-10-28 08:55:35 +01:00
Edwin Brady
e125c9014f
Prepare release 0.6.0 (#2733)
* Prepare release 0.6.0

* Fix bootstrap chez

* Correct version in bootstrap chez
2022-10-27 16:32:16 +01:00
Stefan Höck
57c589ca80
[ performance ] More stack safety in the Prelude (#2704) 2022-10-26 09:54:53 +01:00
Aleksei Volkov
c906720ee3
[ base ] Change Reader to fix search for MonadReader instance (#2729) 2022-10-22 19:13:52 +01:00
G. Allais
475d13bb11
[ fix ] parsing of test lib's options (#2725)
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2022-10-21 21:01:54 +01:00
CodingCellist
47c2de3148
[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)
A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.

Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.

This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.

* [ repl ] Use unlines for detailed help (see #2087)

  Ideally, the lines affected should be multiline strings. But for some
  arcane reason, newlines in those get swallowed in Nix and Windows
  **CI** only Ô.o
  This was already documented in issue #2087.

* [ new ] --except for golden testing lib

  To allow CI to pass despite #2087

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-21 14:35:33 +02:00
QDelta
e0a19aa01e
[ fix #2719 ] --only behavior in Test.Golden (#2720)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-18 12:36:09 +01:00
Denis Buzdalov
eb4cc0054b [ golden ] Make options to store more flexible tests filter 2022-10-14 15:03:05 +01:00
Denis Buzdalov
2744a3a5a2
[ golden ] Truncate long test names when printing the results (#2553) 2022-10-06 19:18:34 +01:00