idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Code Issues Projects Releases Wiki Activity
1,316 Commits 6 Branches 9 Tags 115 MiB
5b97cd4499
Commit Graph

1316 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Alex Humphreys
71a638ef28 Add extra parsers 
This also changes the return type of `char` and `string`. They
previously returned `()`, they now return `Char` and `String`
repectively.

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-11-27 11:54:12 +00:00
Guillaume ALLAIS
c3082d8465 [ re #524 ] Debug + positivity check 2020-11-27 09:29:44 +00:00
Rui Barreiro
910711afe9
prim void to js codegen (#782) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-11-26 16:50:08 +00:00
Yu Zhang
08a35d694c
Improving error messages (#786) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-11-26 11:35:55 +00:00
Denis Buzdalov
60c8695a6d Editor was made run apostrophe-containing modules from REPL normally. 2020-11-26 11:17:36 +00:00
Denis Buzdalov
9990b5ad29 Namespaces were shadowed in all standard codegens. 
This allows, for exmaple, to have apostrophes in module names.
Test was added only for chez, however this should be viable for all
targets with `:exec` implemented.
 2020-11-26 11:17:36 +00:00
russoul
a7cb2745bc Fix CI 2020-11-23 18:06:23 +00:00
Guillaume ALLAIS
22bfa90971 [ fix ] recoverability criteria 
If the "can't convert" error arises from a mismatch between a type
constructor and a primitive value, it is not recoverable.
 2020-11-11 19:10:34 +00:00
Guillaume ALLAIS
ec6c70c6e1 [ log ] for coverage, impossible & empty check 2020-11-11 19:10:34 +00:00
Tim Engler
72af040e7e Fixes Issue #74. The problem is that if the function is defined in a sub 
module, then the current namespace (accessed by calling getNS) differs
from the function namespace, therefore it is not considered visible by
TTImp.Elab.App.checkVisibleNS
 2020-11-11 10:28:51 +00:00
Cotton Hou
52ba8b00a6 Fix broken url to JS code gen page in faq 2020-11-01 11:07:06 +00:00
Jonas Claesson
9f9abc8025 Gambit: add GAMBIT_GSC_BACKEND env configuration 
Gambit after version v4.9.3 supports the -cc option, which configures
the compiler backend Gambit will use to build the binary. Currently to
get this functionality Gambit needs to be built from source, since it is
not yet available in a released version.
 2020-10-31 10:19:55 +01:00
Jonas Claesson
e4d892490d Add option to compile to C on Gambit CG 
Use the '--codegen gambit --directive C' compilation flags.
 2020-10-31 09:14:15 +01:00
Guillaume ALLAIS
a9ff13c663 [ new ] proof that evaluation is Domain-independent 2020-10-29 23:05:41 +00:00
DavidTheBugWriter
b4b800e967 Update starting.rst 
Hellow world execute fails on Macos as it doesn't have realpath by default & one needs to install it with coreutils first.
 2020-10-24 12:35:13 +01:00
Christian Rasmussen
66fe57f340 Run tests chez029 and node022 via code generator 2020-10-24 12:34:04 +01:00
Alex Gryzlov
f79b86ae41
contrib.Data.String.Parser updates (#713) 2020-10-24 12:33:15 +01:00
Niklas Larsson
aa6e36ef43
Merge pull request #749 from ska80/remove-refc-schemecall 
[refc] Remove 'schemeCall' as it is not used anymore
 2020-10-21 16:53:59 +02:00
Kamil Shakirov
544208ec92 [refc] Update 'sysOS' to recognize more BSD flavors 2020-10-21 17:20:51 +06:00
Kamil Shakirov
0b36a5fe3b [refc] Remove 'schemeCall' as it is not used anymore 2020-10-21 16:57:05 +06:00
Edwin Brady
ccdfc363e3
Merge pull request #739 from edwinb/refcount-c 
Experimental C backend with reference counting
 2020-10-21 11:12:28 +01:00
Edwin Brady
77ba750abf
Merge pull request #5 from MarcelineVQ/refcount-c 
remove some redundancy, make tiny style changes
 2020-10-21 10:15:27 +01:00
Edwin Brady
0a705f846c
Merge pull request #4 from melted/refcount-c 
Make it build on windows
 2020-10-21 10:14:31 +01:00
Jan de Muijnck-Hughes
de58c66ab2
Make Idris2 test harness available for the many and not the few. (#719) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-10-19 09:26:23 +01:00
Guillaume ALLAIS
14d0141ca2 [ fix #735 ] Make sure type constructors are fully applied 2020-10-16 14:44:11 +01:00
Guillaume ALLAIS
7192ef28a3 [ test ] add IDRIS2_TESTS_CG env variable 2020-10-16 14:44:11 +01:00
Guillaume ALLAIS
482527063c [ new ] Variant with a runtime irrelevant Domain 
Rather than translating the constraints to a Dybjer-Setzer IR code
we can produce an ad-hoc definition of a `Domain` that we will be
able to make runtime irrelevant.

This means that compiled code will never need to construct a proof
that a value is in the domain of the function: it will simply run
the function!
 2020-10-15 17:03:32 +01:00
Guillaume ALLAIS
864be2c9dc [ contrib ] add McBride's General monad 2020-10-15 17:03:32 +01:00
Matúš Tejiščák
1483b61091
Merge pull request #741 from ShinKage/ide-flush 
Flush stdout in IDE mode first message
 2020-10-14 09:12:37 +02:00
Giuseppe Lomurno
37c4fd5771 Flush stdout in IDE mode first message 2020-10-14 03:32:54 +02:00
russoul
3ad87e97f1 Adjust to the removal of ad-hoc postfix projections, Bump up ttc version 2020-10-12 17:55:47 +03:00
russoul
fd90141ed9 Merge branch 'master' of https://github.com/idris-lang/Idris2 into master 2020-10-12 17:36:45 +03:00
MarcelineVQ
50faacf69c remove some redundancy, make tiny style changes 2020-10-11 22:18:51 -07:00
Niklas Larsson
604e7ea99e Make it build on windows 2020-10-11 23:36:52 +02:00
Edwin Brady
0972e69287 Update changelog 2020-10-11 18:55:43 +01:00
Edwin Brady
97e5f04c34 Add believe_me and crash primitives to refc 2020-10-11 18:51:45 +01:00
Edwin Brady
3007b5a99d Generate an executable via CC 
This builds a .o from the generated C, and statically links with the
libidris2_support library. It doesn't yet dynamically link with any
additional libraries.
 2020-10-11 18:35:51 +01:00