Commit Graph

227 Commits

Author SHA1 Message Date
André Videla
75032a7164
Emit warning for fixities with no export modifiers (#3234)
* Emit warning for fixities with no export modifiers

This is to help update all the existing code to program with explicit
fixity export directives in preparation for the behavioral change where
they will become private by default.
2024-04-03 15:41:57 +01:00
G. Allais
2c2aa85048
[ prelude ] the is linear in its input (#3239)
* [ prelude ] `the` is linear in its input

* [ fix ] eta-expand tests
2024-03-27 14:09:14 +00:00
Denis Buzdalov
0e831ed5ef [ prelude ] Make able to implement provably total showPrec recursively 2023-12-26 10:16:57 +00:00
Denis Buzdalov
82bb12cf72 [ cleanup ] Post v0.7.0 cleanup 2023-12-25 13:49:26 +00:00
Thomas E. Hansen
ea180d0721 [ rc ] Prepare for 0.7.0
A lot more sensible all around  : )
2023-12-22 14:44:30 +01:00
Thomas E. Hansen
a3b078cb0d [ rc ] For v0.6.9 - to see if the process was right
Good luck everybody...

v0.6.9 - Nice!  ^^
2023-12-22 14:44:30 +01:00
Denis Buzdalov
e3ff0b7786 [ minor ] Remove a compilation warning from prelude 2023-12-08 18:54:57 +00:00
russoul
f2e6dc4313 Add dependent congruence of arity 1 and 2 for heterogeneous equality 2023-11-30 10:08:54 +00:00
Joel Berkeley
f6c000e27e Fix typo in namespace for [bi]traversable composition 2023-09-20 09:15:56 +02:00
Denis Buzdalov
cf9a73f86c [ prelude ] Add some lacking %tcinlines 2023-08-23 11:04:53 +01:00
Marshall Abrams
bdb6531b86 Add documentation for Not. 2023-08-15 20:07:21 -05:00
Robert Wright
af3c5fd454 Generalize Prelude proof helpers 2023-07-05 16:36:09 +01:00
Thomas E. Hansen
009eb270c1 Revert "[ fix ] Rename Prelude.Interface NS Lazy to ILazy"
This reverts commit bd231c2076, which is a
separate thing that should be its own PR.
2023-05-30 09:46:24 +02:00
Thomas E. Hansen
bcbe2b8c4f [ fix ] Rename Prelude.Interface NS Lazy to ILazy
This is required due to `Lazy` now being a reserved compiler primitive.

N.B. This may also break other dependencies and/or tools. Notably stuff
     outwith the Idris2 upstream. There's been some discussion in #2987.
2023-05-30 09:46:24 +02:00
Denis Buzdalov
55efd7dd7b [ new ] Add Compose instances for Bi* interfaces, analogous to present 2023-04-25 12:59:25 +01:00
G. Allais
b185f1ff85
[ new ] %unsafe pragma for escape hatches (#2937) 2023-04-03 21:42:47 +01: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
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
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
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
G. Allais
85bb822f3b
[ perf ] manually eta-expand unsaturated io_bind calls (#2785) 2022-12-01 15:31:00 +00: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
Guillaume Allais
5631608782 [ base ] deriving Foldable 2022-09-24 10:20:25 +01:00
Stefan Höck
08f24e79fd
[ performance ] constant folding for all integral expressions (#2662) 2022-09-21 10:05:02 +01:00
Nil Geisweiller
719b5ad17f
[ cleanup ] Remove extraneous show and simplify printLn (#2618) 2022-08-10 21:22:58 +01:00
Guillaume Allais
2060535d08 [ new ] name hints for primitive types 2022-06-14 16:07:37 +01:00
kasiaMarek
094a9ab06d
List proofs (#2497)
* Modified bind definition

* bind proofs and list elem proof

Co-authored-by: Katarzyna Marek <katarzynamarek@Katarzynas-MBP.lan>
2022-06-01 13:16:17 +01:00
Xerz
e9f562f435
[ prelude ] Add Range implementation for Char (#2505) 2022-05-27 07:57:59 +01:00
G. Allais
10a6734bcb
[ new ] Katla-powered landing page (#2483) 2022-05-18 08:43:47 +01:00
Vit Brunner
4a761ea523 [ doc ] Foldable's all is a conjunction 2022-05-02 21:15:28 +01:00
vfrinken
b1f45f2748
RefC backend improvements (#2425)
* RefC backend improvements

1. OnCollect had the wrong number of arguments. The code creator expects
   3 arguments, but onCollect in prim.h expected 4 arguments. The first of which
   was an erased arguments. That is now fixed.

2. OnCollect did not call `newReference` when creating a new reference to the pointer
   and the freeing function

3. OnCollect and OnCollectAny still had a spurious printf statement

Those issues have been fixed, the test case can be found in
  tests/refc/garbageCollect

4. The IORef mechanism expects that the %World token will be passed around
   consistently. This is not the case. States in Control.App make use of
   IORefs, but the function created from Control.App.prim_app_bind
   had the world token erased to NULL.
   Now, IORefs are managed using a global variable,
   IORef_Storage * global_IORef_Storage;
   referenced in cBackend.h, defined in the created .c file, and set to NULL
   in main();

5. While multithreading and forking is still not supported, compiling a program
   that makes use of Control.App demands a C implementation of prim_fork.
   Files support/refc/threads.c and support/refc/threads.h provide a
   dummy implementation for it, so that Control.App programs compile and run.

A test for these 2 issues is given in tests/refc/issue2424

* format changes

to make the linter happy

* format changes

to make the linter happy

* format changes

to make the linter happy

* spelling mistake braket -> bracket

Co-authored-by: Volkmar Frinken <volkmar@onutechnology.com>
2022-04-27 13:59:32 +01:00
Robert Wright
1d6c3eb84f Add Reverse Ord instance 2022-03-31 10:50:51 +01:00
Denis Buzdalov
e8d3d788c1
[ base ] Add some more properties, functions and interface implementations (#2361) 2022-03-23 13:33:13 +00:00
Ohad Kammar
319c7f7b86
Move Syntax.PreorderReasoning into base (#2368) 2022-03-22 20:58:36 +00:00
Joel Berkeley
399d6016a9
[ prelude ] add subtract (#2357) 2022-03-17 18:24:42 +00:00
G. Allais
1c396744d9
[ doc ] :printdef for interface implementations (#2340) 2022-03-07 11:47:20 +00:00
Joel Berkeley
f436388a6b
adopt backend implementations of pow (#2334) 2022-03-03 23:39:25 +00:00
G. Allais
1011cc6162
[ papers ] Tychonoff (Part I) (#2332) 2022-02-24 11:12:53 +00:00
Jan de Muijnck-Hughes
4ba3bb6670
[ fix ] Literate things (#2312)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-02-18 11:29:52 +00:00
Denis Buzdalov
b727ae4a97 [ new ] Add a Monoid instance of the f a where f is Applicative 2022-02-16 14:23:56 +00:00
Denis Buzdalov
e2487106fd
[ prelude ] Ease Compose compositions (#2324) 2022-02-16 14:19:25 +00:00
madman-bob
0ee9632e45
[ refactor ] Abstract Prelude.elem to work with all Foldables (#2294) 2022-02-01 21:34:29 +00:00
Stefan Höck
44245e1683
[ fix ] issue #2288 (#2289) 2022-01-28 09:01:09 +00:00
G. Allais
ec5afa5065
[ libs ] move propaganda out of contrib (#2213) 2022-01-25 12:25:55 +00:00
James Cook
e82600c4d6
[ opt ] transform rule making List.length tail-recursive. (#2100) 2022-01-24 16:12:29 +00:00
MarcelineVQ
6d10ca09b4 [ base ] add Show for Ordering 2022-01-19 22:12:36 +00:00
Denis Buzdalov
f1941cecac [ cleanup ] Remove piece of dead code from prelude 2021-11-26 10:14:47 +00:00