idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity
3,263 Commits 6 Branches 9 Tags 115 MiB
2739c3a389
Commit Graph

3263 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Michael Neumann
60a3b80c19
Fix build on FreeBSD (#2852) 2023-01-14 08:19:12 -06:00
Zoe Stafford
d78d0bff60
Merge pull request #2845 from Z-snails/case-of-case 
Allow case-of-case to work on cases with defaults
 2023-01-13 13:06:35 +00: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
Zoe Stafford
fd217722bb
Merge pull request #2847 from Z-snails/js-bigint 
Use built-in bigint truncation on js backend
 2023-01-08 17:15:35 +00:00
Zoe Stafford
ae974af1d1
Use built-in bigint truncation on js backend 2023-01-08 12:50:26 +00:00
Alexander
304c29ed79 Fix typo 2023-01-08 12:44:19 +00:00
Zoe Stafford
b098de933d
Allow case-of-case to work on cases with defaults 
The inner case can now have a default alternative.
This means `Prelude.Types.prim__integerToNat` is better optimised

before
```js
/* Prelude.Types.prim__integerToNat : Integer -> Nat */
function Prelude_Types_prim__integerToNat($0) {
 let $1;
 switch(((0n<=$0)?1:0)) {
  case 0: {
   $1 = 0;
   break;
  }
  default: $1 = 1;
 }
 switch($1) {
  case 1: return $0;
  case 0: return 0n;
 }
}
```
after
```js
/* Prelude.Types.prim__integerToNat : Integer -> Nat */
function Prelude_Types_prim__integerToNat($0) {
 switch(((0n<=$0)?1:0)) {
  case 0: return 0n;
  default: return $0;
 }
}
```
 2023-01-08 11:01:53 +00:00
Nicolas Biri
f630675cfb Update flake 2023-01-07 17:32:48 -06:00
Mathew Polzin
63a22b819d
[docs] javascript FFIs and packaging of JS or C support files (#2842) 
* Add documentation on javascript FFIs and packaging of JS or C support files.

* Add to changelog.

* line length

* add some detail about the install directories for packages.
 2023-01-07 21:40:47 +00:00
Stefan Höck
8db12f5a49
[ performance ] improve some Char functions (#2839) 2023-01-06 09:08:38 +00:00
Zoe Stafford
f9dc56a5f4
[ performance ] String builder on all scheme backends (#2838) 
* [ performance ] String builder on all scheme backends
    this makes it about 50x faster at printing scheme code

* [ lint ]

* Add new module

* [ fix ] miscompilation on racket
 2023-01-03 11:53:52 +00:00
Zoe Stafford
ab0ff2754a
Merge pull request #2836 from mattpolzin/library-data 
[ new ] [ proposal ] Allow libraries to ship a data dir
 2023-01-03 10:38:30 +00:00
Steve Dunham
a84a5a32d9 Fix at-pattern leak in recursive with blocks (#2834) 2022-12-28 09:08:09 +00:00
Mathew Polzin
d53a277a34 Allow libraries to ship a data dir at a standard location within their install directory. 2022-12-27 20:44:16 -06:00
Zoe Stafford
947432fa30
Merge pull request #2829 from Z-snails/js-clock 
add javascript support to `System.Clock`
 2022-12-23 16:39:48 +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
Zoe Stafford
217271a623
Js shebang (#2830) 
* add shebang to outputted node file
after `chmod`ing the file, it can be run directly
ie `./build/exec/test` rather than `node ./build/exec/test``

* update CHANGELOG.md

* [ linter ]

* [ linter ] again...
 2022-12-22 14:56:44 +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
45fc038300
Merge pull request #2827 from Z-snails/clock 
export `{to,from}Nano` in `System.Clock`
 2022-12-21 17:22:22 +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
Guillaume Allais
1092804726 [ fix #2821 ] Failing blocks should force delayed holes 2022-12-21 11:16:26 +00:00
Zoe Stafford
f57e6f6ebb
Merge pull request #2825 from cypheon/feature/aarch64-machine-type 
[chez] Detect AArch64 machine/OS combinations correctly
 2022-12-21 08:59:03 +00:00
Stefan Höck
d2c8cf461b
[ performance ] Compile non-recursive top-level constants to constants in Chez (#2817) 2022-12-21 08:48:20 +00:00
Johann Rudloff
018ef1fd8b [chez] Detect AArch64 machine/OS combinations correctly 2022-12-20 20:28:26 +01:00
Denis Buzdalov
f4ebcadfad [ base ] Add forgetting conversions of Vect.Quantifiers 2022-12-20 16:36:27 +00:00
Denis Buzdalov
2dfd7e5259 [ doc ] Minor syntactic correction in the code example 2022-12-20 16:36:27 +00:00
Sridhar Ratnakumar
9ab23c78bc docs: Fix link to libraries 2022-12-20 15:36:11 +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
Guillaume Allais
1d73e359e0 [ ci ] only run latest job 
As discussed on discord a while ago, this kills runs when a new
commit lands on the same branch. It should save some CI ressources.
 2022-12-09 14:40:14 +00:00
Guillaume Allais
caeb55b495 [ ci ] fix initialise step 
Github is now failing hard on multiline commit messages it seems.
 2022-12-09 14:40:14 +00:00
Guillaume Allais
9bcaa104f3 [ new ] logging topics autocompletion in the emacs REPL 2022-12-08 21:06:39 +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
Thomas E. Hansen
7a41606573 [ admin ] Fix PR template 2022-12-08 11:24:37 +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
G. Allais
32f92746b3
[ perf ] compile Core.CompileExpr.Pretty faster (#2800) 2022-12-07 10:08:31 +00:00
Guillaume Allais
085ea348ae [ perf ] use integers in the buffer state 2022-12-06 21:13:55 +00:00
Guillaume Allais
ebc406c519 [ perf ] cherrypick fast weakenNVar from yaffle 2022-12-06 12:28:16 +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
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
Denis Buzdalov
c8f625cad9 [ typo ] Fix typo in an issue template 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