idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 13:11:30 +03:00
Code Issues Projects Releases Wiki Activity
1,303 Commits 6 Branches 9 Tags 115 MiB
043faf8baf
Commit Graph

1303 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
raptazure
043faf8baf docs: fix grammar 2020-12-16 10:02:34 +00:00
Edwin Brady
771e4034fa
Merge pull request #846 from edwinb/interfaces 
Local hints (basic version)
 2020-12-14 14:46:18 +00:00
Edwin Brady
6c9ad81c12 Add missing test 
:#	../../../src/Compiler/.ANF.idr.swp
 2020-12-14 13:38:40 +00:00
Edwin Brady
c1f58d963f
Merge branch 'master' into interfaces 2020-12-14 13:34:31 +00:00
Edwin Brady
252292451f Add local hints (basic version) 
This gives us the ability to define and use implementations locally, in
where clauses/local let bindings, as well as flag local definitions as
hints.
It's not yet quite equivalent to global hints, however, since it translated
the hint to a local let binding, which doesn't reduce, so if something
relies on the reduction behaviour of the hint, it won't work. This
refinement is coming later
 2020-12-14 13:25:50 +00:00
Wen Kokke
daff1f2fb8
Added assert_linear. (#844) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-12-13 16:06:18 +00:00
G. Allais
3f6b99e979
[ fix #657 ] RigCount for interface parameters (#808) 2020-12-11 11:58:26 +00:00
Dong Tsing-hsuen
88aa55e875
[ new ] null method in Foldable (#832) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-12-10 18:04:23 +00:00
Guillaume ALLAIS
4356d377c5 [ refactor ] parser for lambda & lambdacase 2020-12-10 18:01:14 +00:00
Guillaume ALLAIS
4025896572 [ fix #833, #677 ] bound variables start with a lowercase letter 2020-12-10 18:01:14 +00:00
Guillaume ALLAIS
0a685f8d2c [ debug ] remove max from log 
Users should be allowed to de-escalate the level of detail they're
getting.
 2020-12-10 14:27:02 +00:00
Guillaume ALLAIS
5de647cc3f [ refactor ] use difference list for efficient append 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
0675e58cca [ error ] crash rather than generating garbage 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
89daa5c1f6 [ cleanup ] existing list function & needlessly effectfule ones 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
3c0ff432bd [ cleanup ] redundant parens, language keyword 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
243ed5df2c [ cleanup ] remove trailing "pure ()" 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
39f26e7ed6 [ minor ] avoid repetition 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
f8c248dc7a [ refactor ] introduce Core.update 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
e5c6dfac5b [ refactor ] remove toString, natMinus 
* toString is an inefficient fastPack
* natMinus is an inefficient minus (we have already checked isLTE)
 2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
98674fc40a [ cleanup ] use pattern-matching binds in monadic code 2020-12-08 13:07:53 +00:00
Denis Buzdalov
a1b624a3bc Tiny fix of the formatting in the recently added documentation. 2020-12-08 08:56:38 +00:00
Fabián Heredia Montiel
87358f19da Increase timings of concurrency tests due to flaky windows runs 2020-12-07 21:20:09 +00:00
Ruslan Feizerahmanov
1dba32a0c4
[ doc ] new application syntax (#820) 2020-12-07 18:59:49 +00:00
Jan de Muijnck-Hughes
3a6e779acf Extended Literate support to include LaTeX. 2020-12-07 14:54:35 +00:00
Jan de Muijnck-Hughes
9c5198cde3 Fixed docs and improved Literate mode. 
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
 2020-12-07 14:54:35 +00:00
Nicolas A. Schmidt
ef6cbcf658
Auto-implicit __con now added before implicits. (#659) 2020-12-07 11:41:47 +00:00
Denis Buzdalov
b3542d66fc
Have lambda-case available everywhere lambda is (#819) 2020-12-07 11:34:48 +00:00
Guillaume ALLAIS
d30e984137 [ debug ] Give the option to log off 2020-12-07 11:33:37 +00:00
David Smith
c6abab438c
export a function to parse ipkg files (#822) 2020-12-07 10:53:01 +00:00
Edwin Brady
63a46722ef Force/Delay need to be inlined in Builtins 
Otherwise (especially in the case of delay) the argument might be
evaluated prematurely.
 2020-12-06 20:00:48 +00:00
Andor Penzes
aeab632c7e [doc] JS FFI examples. 2020-12-06 19:07:34 +00:00
Andy Lok
9e22a6e07b
Add javascript FFI for fastUnpack (#816) 2020-12-06 09:54:58 +00:00
Edwin Brady
22a534f400 Elaborate implementations in the right environment 
This involves a small extension to IPragma, because to properly
elaborate names in a local scope we need to know which names are defined
in that scope so that they get applied to the environment when needed.

This means we can now define implementations of interfaces locally (but
there's still some work to do, because we don't yet have a way of
applying locally defined hints in auto search. It's coming soon!)
 2020-12-05 20:53:03 +00:00
Denis Buzdalov
13cc27da1f An alternative (Fin-based) indexing function was added for lists. 2020-12-04 19:09:05 +00:00
Denis Buzdalov
4364793484 Type definition from Decidable.Equality was moved to a separate module 
This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).
 2020-12-04 19:09:05 +00:00
Edwin Brady
bfea7d785a
Merge pull request #766 from mokshasoft/gambit-cg 
Gambit cg
 2020-12-04 15:51:22 +00:00
Edwin Brady
778d6026e5
Merge pull request #607 from Russoul/record-init 
New syntax for named applications and "record" updates
 2020-12-04 11:35:05 +00:00
Denis Buzdalov
f2596318e5 Proof of list bounds was made to be not present at runtime when indexing 2020-12-04 11:26:11 +00:00
Fabián Heredia Montiel
57a8ef4609
Implement Futures as a Parallelism Primitive (#753) 
Co-authored-by: Christian Rasmussen <christian.rasmussen@me.com>
 2020-12-04 10:58:26 +00:00
Jonas Claesson
924166a911 Add GAMBIT_GSC_BACKEND and C directive to Gambit docs 2020-12-03 18:02:54 +01:00
russoul
46519237cd Merge 2020-12-03 15:28:20 +03:00
Edwin Brady
2e6aa126a4
Merge pull request #750 from ska80/refc-sysos 
[refc] Update 'sysOS' to recognize more BSD flavors
 2020-12-03 11:59:33 +00:00
Edwin Brady
b244d26cd1
Merge pull request #731 from rbarreiro/issue_596 
adds mutual recursion optimisation to the javascript backend
 2020-12-03 11:48:44 +00:00
Guillaume ALLAIS
e9126aafd8 [ doc ] :browse made aware of namespace nesting 2020-12-02 20:38:32 +00:00
Andor Penzes
a5a5d89d0c Resolves #804 
Introduces parenthesis around parts of let expressions and closes
parenthesis for the case expression.
 2020-11-29 22:30:48 +00:00
Mathew Polzin
6ca03acd71
Add replaceWhen for lists. (#755) 2020-11-27 19:10:08 +00:00
G. Allais
502f544d73
[ fix #775 ] integerToNat is not, in fact, id (#799) 2020-11-27 18:48:19 +00:00
Giuseppe Lomurno
c82e2393d4
Test templates (#585) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-11-27 15:40:02 +00:00
G. Allais
5e799563fa
[ contrib ] adding Data.Container (#781) 2020-11-27 15:29:19 +00:00
Kamil Shakirov
127db79a6b Require all definitions to be total in tests/typedd-book/chapter11/ArithCmdDo.idr 2020-11-27 11:59:30 +00:00