idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 06:13:26 +03:00
Code Issues Projects Releases Wiki Activity
1,804 Commits 5 Branches 9 Tags 112 MiB
c3e5689a62
Commit Graph

227 Commits

Author SHA1 Message Date
Tung Alissa
881a5e7fbc
[ fix #1328 ] print infix functions enclosed in grave accents (#1331) 2021-04-25 18:56:08 +01:00
André Videla
9f39ad6ba8 Implement new parameters syntax 
Previously, parameter block reused the same syntax as in Idris1:

```
parameters (v1 : t1, … , vn : tn)
```

Unfortunately this syntax presents some issues:
 - It does not allow to declare implicit parameters
 - It does not allow to specify which multiplicity to use
 - It is inconsistent with the syntax used for named arguments elsewhere
   in the language.

This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:

```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```

It also enables other features like multiple declarations of arguments
with the same type:

```
parameters (v1, v2 : Type)
```
 2021-04-23 19:02:48 +01:00
Zoe Stafford
c75b3f7f14
Add Agda-like builtins (#1253) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-22 13:08:32 +01:00
stefan-hoeck
181b26b250 [ fix ] broken unicode parsing in JSON 2021-04-22 10:59:14 +01:00
claymager
d6583048d8
Fixes for processPackage (#1304) 2021-04-21 10:15:39 +01:00
Tung Alissa
1bf46bc458
[ REPL ] Improving :doc (fixity, totality, colours) (#1316) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-21 09:39:18 +01:00
Guillaume ALLAIS
f6f2f5f5c6 [ fix #962 ] solve defaults on LHS even in case 2021-04-16 18:12:40 +01:00
G. Allais
5946442dc2
[ new ] idris2 --init (#1299) 2021-04-15 14:08:50 +01:00
Ohad Kammar
b65907f770
Support Multi-declarations (#1280) 2021-04-07 12:21:17 +01:00
Edwin Brady
12f40f538f Use correct multiplicity in scope of lets 
The scope should be checked at the same multiplicity as the enclosing
expression.
 2021-04-04 18:10:34 +01:00
Guillaume ALLAIS
99b87c8156 [ fix #1248 ] Bring qualified names back for data & record types 2021-03-31 23:17:53 +01:00
Atomotron
a1e7221c32
[ fix #1200 ] Switch scheme backend to flonum functions (#1203) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-03-31 23:17:41 +01:00
Zoe Stafford
f255026d1b
[ fix #1220 ] Update arity of constuctors to reflect erased args (#1225) 2021-03-29 15:08:06 +01:00
G. Allais
238eb62da6
[ fix #1230 ] Better error messages for out-of-scope identifiers (#1233) 2021-03-29 10:45:48 +01:00
CodingCellist
ec77ad21ab
[ re #1185 ] Add primitive for obtaining number of processors (#1209) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-03-26 18:27:25 +00:00
Denis Buzdalov
8abd60535b [ fix ] Ability for data types to be operators was restored 2021-03-25 14:16:47 +00:00
G. Allais
97fb5d7b94
[ fix #893 ] proof gadget for with clauses (#1222) 2021-03-25 10:02:06 +00:00
G. Allais
21f2913527
[ fix #710 ] Enforce assumptions about capitalised idents (#1207) 
Given we keep getting tripped up by this, here we go:

* Namespaces
* Data names
* Record names
* Data constructor names (except for operators)
* Record constructor names (except for operators)
* Interface constructor names (except for operators)
 2021-03-22 13:22:52 +00:00
Guillaume ALLAIS
f600182999 [ close #31 ] test case for the issue 2021-03-18 10:38:48 +00:00
G. Allais
f959987a51
[ fix #834 ] Fix implicitsAs for local definitions (#1199) 2021-03-17 10:54:25 +00:00
Stefan Höck
591797ebaf
[ new ] Support overloaded floating point literals (#1177) 2021-03-16 14:08:50 +00:00
CodingCellist
89a84a34a4
Patch CVs and sleep in Racket (#1059) 2021-03-15 13:43:12 +00:00
Matúš Tejiščák
f4a790ded4
Identify prefix and postfix record projections (#1183) 
`.proj` and `proj` are identically defined but separate functions.
This patch fixes it by defining `.proj` only once, and adding `proj = (.proj)`
for every projection.
 2021-03-15 13:40:13 +00:00
Edwin Brady
17cdc7fa88
Merge pull request #1171 from edwinb/fix1163 
Correct multiplicities when checking Pi binders
 2021-03-09 18:36:08 +00:00
Mathew Polzin
06586d401a
Add a test package to the Idris 2 project (#1162) 2021-03-09 18:27:05 +00:00
Edwin Brady
04a0f5001f Correct multiplicities when checking Pi binders 
We've always just used 0, which isn't correct if the function is going
to be used in a runtime pattern match. Now calculate correctly so that
we're explicit about which type level variables are used at runtime.

This might cause some programs to fail to compile, if they use functions
that calculate Pi types. The solution is to make those functions
explicitly 0 multiplicity. If that doesn't work, you may have been
accidentally trying to use compile-time only data at run time!

Fixes #1163
 2021-03-09 17:23:05 +00:00
Ruslan Feizerahmanov
50c60185a7
[ auto ] Ignore hidden names in Core.Context.getSearchData (#1143) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-03-09 14:13:29 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base (#1033) 2021-03-04 20:59:56 +00:00
Edwin Brady
6887a5f95f Record local hints in delayed elaborators 
We might not have set up search problems yet when delaying an
elaborator, so we need to know what the local hints were at the point of
delay.
 2021-03-03 13:49:32 +00:00
Edwin Brady
1d965627c9 Check current holes only at end of elaboration 
Fixes #1140 - when checking holes were solved, we checked all of them,
but there may still be some open if there's a local definition.
 2021-03-01 19:11:15 +00:00
Edwin Brady
37cc095f7a Merge github.com:idris-lang/Idris2 into versions 2021-02-27 18:00:18 +00:00
Edwin Brady
1d8166b1b2 Version number constraints in 'depends' field 
Now reporting an error if we can't find a package that satisfies the
constraints. The version number field can still be a string (as it used
to be) but will give a deprecation warning - and the old style version
string wasn't used anyway.

Version constraints can have an upper and/or lower bound, which can be
inclusive or not.
 2021-02-27 17:58:52 +00:00
G. Allais
59de5f1326
[ fix #762 ] Different case tree building strategy (#1125) 2021-02-26 09:33:07 +00:00
G. Allais
fcd834c423
[ fix #110 ] Check the LHS' head is not shadowed (#1121) 2021-02-25 08:51:27 +00:00
Guillaume ALLAIS
da88b80481 [ fix #794 ] missing cases in recoverable 2021-02-24 20:25:04 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095) 2021-02-24 11:07:16 +00:00
Denis Buzdalov
95af3cf4be
More compose instances and one usage of them (#1089) 2021-02-23 10:53:43 +00:00
Guillaume ALLAIS
00067e8151 [ fix #637 ] force indentation after a with 2021-02-23 10:52:22 +00:00
G. Allais
c10c1d65a5
[ fix #1022 ] detect more impossible cases (#1108) 2021-02-23 10:51:38 +00:00
G. Allais
30d402ed7f
[ fix #899 ] Be careful when generating an impossible LHS (#1081) 2021-02-22 09:53:30 +00:00
Guillaume ALLAIS
7ccc47712e [ re #1087 ] Better error messages in the REPL 
(as well as in type signatures now that I know how to do that)
 2021-02-19 12:34:19 +00:00
Andy Lok
26464357c1
Implement interpolated string (#1056) 2021-02-18 13:07:22 +00:00
Mathew Polzin
9f8a8b5d76
Add a total way of reading files in. (#1070) 2021-02-18 11:13:25 +00:00
G. Allais
399a2adb15
[ fix #1043 ] throw error if compileExpr failed (#1052) 
Also adding a CI target testing the gambit backend.
 2021-02-10 21:10:27 +00:00
Z-snails
4eac2dd0b9
[ new ] support record projections in refc backend (#1054) 2021-02-10 14:46:41 +00:00
Stefan Hoeck
f721281bdc
[ re #1043 ] Fix typo in support.scm (#1047) 2021-02-10 01:00:42 +00:00
stefan-hoeck
f50b22548f tests for bitops 2021-02-08 15:47:23 +00:00
stefan-hoeck
1104776430 fix 1037 2021-02-08 15:47:23 +00:00
Wen Kokke
bd683938bf
Overhaul of concurrency primitives (#968) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-02-05 16:16:20 +00:00
GustavoMF31
7f495999bd
Make :typeat a useful command (#998) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-02-05 16:15:40 +00:00