idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity
1,877 Commits 6 Branches 9 Tags 114 MiB
5cb389769e
Commit Graph

1877 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
b2f08c0e81
Merge pull request #1264 from melted/refc_idris_build 
Fixes from trying to compile idris with the refc backend
 2021-04-02 17:04:50 +02:00
Niklas Larsson
e49916cea9 Fixes from trying to compile idris with the refc backend 
* fix doublequoting in constArray
* substitute tildes in names
* Add negate functions
* Add string comparisons

Several things remain, notably missing _argList functions.
 2021-04-02 15:02:40 +02:00
Kamil Shakirov
b27001136b [ tests ] Ignore test artifacts 2021-04-01 10:06:14 +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
Kamil Shakirov
43d0b94567 [ docs ] Update Control.App docs 2021-03-31 18:01:39 +01:00
Guillaume ALLAIS
5af1efb56e [ refactor ] introduce NonZero 
This has a much better behaviour with respect to proof search and
the coverage checker realising we don't need to consider the Z case
than the `Not (x = Z)` we used earlier.
 2021-03-31 17:59:58 +01:00
Guillaume ALLAIS
09d8e25441 [ refactor ] more efficient implementation of range 2021-03-30 10:51:56 +01:00
Zoe Stafford
f255026d1b
[ fix #1220 ] Update arity of constuctors to reflect erased args (#1225) 2021-03-29 15:08:06 +01:00
Ruslan Feizerakhmanov
802113772f Tune precedence of (===), (~=~) and (<+>) 2021-03-29 11:29:58 +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
Ben Hormann
b1c7f75bbe [ fix ] bootstrap-stage2: IDRIS2_CG not set correctly 2021-03-26 15:45:06 +00:00
stefan-hoeck
6824111fd8 [ performance ] add fastUnlines to base 2021-03-26 12:35:29 +00:00
Zoe Stafford
028f82f70c
Add Data.Monoid.Exponentiation to contrib.ipkg (#1232) 2021-03-26 12:35:19 +00:00
Denis Buzdalov
a6a82a18b5 [ prelude ] foldlM was made to be in the Foldable interface. 2021-03-26 00:59:13 +03:00
Denis Buzdalov
9ee0063a7f [ contrib ] Some useful functions were added for lazy lists. 2021-03-26 00:59:13 +03:00
Alex Gryzlov
71abc8e33b
Add Path@contrib & small changes (#1229) 2021-03-25 16:01:32 +00:00
Guillaume ALLAIS
2df49ebdd4 [ fix #1224 ] moduleIdent must be capitalised 2021-03-25 15:59:46 +00:00
Guillaume ALLAIS
00929deed6 [ cosmetic ] nicer error messages for uncaught exceptions 2021-03-25 15:59:46 +00:00
Guillaume ALLAIS
dad1954a39 [ debug ] for read attempts 2021-03-25 15:59:46 +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
Guilherme Silva
4e3f652c6f
[ fix #1212 ] Removed apps from nix flakes (#1213) 2021-03-22 11:25:38 +00:00
Denis Buzdalov
0749165245 [ base ] Properties of indexing after replaceAt were added for Vect 2021-03-18 16:07:48 +00:00
Denis Buzdalov
941e3963fa [ base ] DecEq implementations of Fin and Vect were exported publicly 2021-03-18 16:07:21 +00:00
Guillaume ALLAIS
f600182999 [ close #31 ] test case for the issue 2021-03-18 10:38:48 +00:00
Andy Lok
da92f9d676
Cleanup List1 (#1091) 2021-03-17 14:07:52 +00:00
G. Allais
f959987a51
[ fix #834 ] Fix implicitsAs for local definitions (#1199) 2021-03-17 10:54:25 +00:00
G. Allais
8f71aae705
[ fix #1193 ] Fine tune REPL's typesearch (#1196) 2021-03-17 10:54:09 +00:00
André Videla
405c266b5e
[ refactor ] Multiline error report (#1155) 2021-03-16 14:10:45 +00:00
Stefan Höck
591797ebaf
[ new ] Support overloaded floating point literals (#1177) 2021-03-16 14:08:50 +00:00
Guillaume ALLAIS
80f8a0f8fe [ re #1185 ] add threads option to test runner 2021-03-16 14:03:46 +00:00
Denis Buzdalov
c7f510c9de [ fix ] Change one implementation according to recent lib change 2021-03-15 15:18:16 +00:00
Denis Buzdalov
cf981d4c68
Validated data structure was added (#1098) 2021-03-15 14:33:01 +00:00
Guilherme Silva
4144510bb3
Added new nix functionalities (#1154) 2021-03-15 14:21:50 +00:00
CodingCellist
89a84a34a4
Patch CVs and sleep in Racket (#1059) 2021-03-15 13:43:12 +00:00
Stefan Höck
1784593abb
[ new ] Applicative and Monad for Pair (#1188) 2021-03-15 13:42:04 +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
robert
9300d22c31 colist 2021-03-15 13:36:05 +00:00
Raoul Hidalgo Charman
3e85e23638
Namespace checks for resugaring (#1161) 
This avoids resugaring to the wrong type when there are user defined
symbols which conflicts with builtins such as Pair.

Changed the test linear002 which was relying on this behaviour for a
user defined Unit.

Fixes #634.
 2021-03-15 13:34:54 +00:00
Michael Messer
d08c0c78b3
Change :doc to use PTerm instead of Name (#1178) 2021-03-12 09:46:46 +00:00
Kamil Shakirov
ca071a96c3 [ docs ] Update Control.App docs 2021-03-10 23:30:46 +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
John Mager
a8952faebc Fix package paths in for Nix 2021-03-09 11:31:25 +00:00
Ruslan Feizerakhmanov
0ef8f08594 Revert #878 (the test stays put) 2021-03-09 11:26:56 +00:00