idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 08:42:11 +03:00
Code Issues Projects Releases Wiki Activity
718 Commits 6 Branches 9 Tags 113 MiB
6673f49731
Commit Graph

718 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
6673f49731 Convert Data.Buffer to HasIO 2020-07-01 23:33:30 +02:00
André Videla
5996361488
Update INSTALL.md 
Fix typo on INSTALL.md
 2020-07-01 18:15:49 +01:00
André Videla
cec56561c6
Merge pull request #387 from LibreCybernetics/fix-export-vect 
Make Applicative implementation of Vect n public export.
 2020-07-01 17:26:08 +01:00
Edwin Brady
c4d56e5481
Merge pull request #396 from edwinb/lazy-lazy 
Don't commit to a Force too early
 2020-07-01 12:29:52 +01:00
Edwin Brady
e7830b2b40 Merge github.com:idris-lang/Idris2 into lazy-lazy 2020-07-01 11:59:35 +01:00
Edwin Brady
c216e1c560 Update test output 2020-07-01 11:53:06 +01:00
Edwin Brady
0d4db3ee75 Add 'force' and 'delay' as functions 
Since Force and Delay are keywords now, these may help in higher order
cases in particular.
 2020-07-01 11:35:27 +01:00
Edwin Brady
669e50ff55 Remove my debugging noise from test case 2020-07-01 00:43:33 +01:00
Edwin Brady
25491060e2 Don't commit to a Force too early 
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes #395
 2020-07-01 00:40:44 +01:00
Mark Barbone
4916dd23a9
Make Data.Vect linear (#333) 2020-06-30 15:05:19 +01:00
Denis Buzdalov
df60e07962 List's snoc injectivity property was renamed approporiately. 2020-06-30 13:18:42 +01:00
Edwin Brady
393c1ed464
Merge pull request #388 from edwinb/samples-dir 
Copy samples directory from Idris2-boot
 2020-06-30 11:23:40 +01:00
Edwin Brady
4f10bfcfd2 Copy samples directory from Idris2-boot 
This is referred to in the documentation, so should be there
 2020-06-30 10:51:09 +01:00
Fabián Heredia Montiel
e488c6cf0e Make applicative implementation of Vect public export 2020-06-29 18:27:57 -05:00
Niklas Larsson
53621f84c5
Merge pull request #370 from ShinKage/ansi 
Adds ANSI codes support in contrib
 2020-06-29 19:43:46 +02:00
Edwin Brady
a35965be84
Merge pull request #384 from edwinb/unify-invert 
Use 'unify' rather than 'convert' if possible
 2020-06-29 16:22:31 +01:00
Edwin Brady
a52308d77d Add test files 2020-06-29 15:13:42 +01:00
Edwin Brady
ffbea6d160 Use 'unify' rather than 'convert' if possible 
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes #66.
 2020-06-29 15:04:32 +01:00
Edwin Brady
84477adfc9
Merge pull request #383 from edwinb/coverwhere 
Pay attention to nested names in coverage check
 2020-06-29 13:52:32 +01:00
Edwin Brady
b2da2fe558 Pay attention to nested names in coverage check 
Fixes #164
 2020-06-29 13:27:00 +01:00
Niklas Larsson
4db58171f9
Merge pull request #381 from chrrasmussen/avoid-traversing-modules-twice 
Avoid traversing all Idris modules twice when installing
 2020-06-29 12:03:08 +02:00
Edwin Brady
31b486c8ed
Merge pull request #382 from edwinb/linear-holes 
Use precise inference for hole types
 2020-06-28 23:17:59 +01:00
Edwin Brady
cc03a4cb3b Add missing test file 
Apparently I forgot the input for linear012. Oops!
 2020-06-28 22:28:56 +01:00
Edwin Brady
ff7d3a0246 Use precise inference for hole types 
That is, don't generalise multiplicities, because we need the hole type
to be precise wrt multiplicities. Resolves #189
 2020-06-28 22:16:15 +01:00
Christian Rasmussen
24bb84fcf5 Avoid traversing all Idris modules twice when installing 2020-06-28 21:36:48 +02:00
Edwin Brady
e175bb8310
Merge pull request #379 from edwinb/interface-type 
Record implicit parameters of interfaces
 2020-06-28 15:31:47 +01:00
Edwin Brady
8ddac9c1d5 Record implicit parameters of interfaces 
We need to make sure they are inferred again when elaborating methods,
so substitute in a _ in method types before substituting in the explicit
parameters.

In future, it might (probably will) also be useful to allow giving the
implicit parameters explicitly when defining implementations.

Fixes #374
 2020-06-28 14:58:57 +01:00
Niklas Larsson
cd777a00ce
Merge pull request #376 from andrevidela/kleisli-arrow 
Add Kleisli arrow operators to contrib
 2020-06-28 00:18:04 +02:00
André Videla
8d04881356 Add Kleisli arrow operators to contrib 2020-06-27 22:02:05 +01:00
Edwin Brady
fb9f79e3c6
Merge pull request #375 from edwinb/interactive 
Add new clause at next blank line
 2020-06-27 21:36:59 +01:00
Edwin Brady
17fec60d7a Add new clause at next blank line 
This fixes a thing that's been annoying me in the vim mode. It's usually
something that's left to the editor, but we do all the work for the vim
mode! (This is hard to test conveniently, sorry...)
 2020-06-27 21:09:03 +01:00
Edwin Brady
35e328a505
Merge pull request #373 from edwinb/interactive 
Various interactive editing improvements
 2020-06-27 19:10:16 +01:00
Edwin Brady
929c5504c5 Implement make-case 2020-06-27 18:28:09 +01:00
Edwin Brady
c043fc3c57 Do make-with IDE command properly 
Now updates the file rather than just printing the output, in update
mode. Also adds bird tracks where appropriate in literate mode.
 2020-06-27 17:06:17 +01:00
Edwin Brady
1b695bcc52 Display binder if it's not implicitly bindable 
This is particularly important if we're generating something that needs
to be parsed and checked again. Fixes #185
 2020-06-27 16:26:34 +01:00
Ohad Kammar
f31318f5e6
Merge pull request #372 from ohad/export-length-correct 
Export the `lengthCorrect` proof, as users might want to use it
 2020-06-27 16:21:04 +01:00
Ohad Kammar
6683a2147f Export the lengthCorrect proof, as users might want to use it 
Change the `len` to be irrelevant, as it's uniquely determined by
matching on the input vector
 2020-06-27 15:54:35 +01:00
Edwin Brady
6c007fc046 Use full names for constructors in case split 
Fixes #184
 2020-06-27 15:47:38 +01:00
Ohad Kammar
574524d8de
Merge pull request #368 from ohad/fstrings 
Add a simple DYI f-string / string interpolation library
 2020-06-26 21:12:13 +01:00
Giuseppe Lomurno
28018d9573 Fixed typo 2020-06-26 21:26:36 +02:00
Giuseppe Lomurno
36c62c754a Updated documentation 2020-06-26 19:16:14 +02:00
Giuseppe Lomurno
5ccc6a397d Added Control.ANSI module in contrib 2020-06-26 19:10:02 +02:00
Ohad Kammar
ac1fa28890 Add a simple DYI f-string / string interpolation library 
Apparently the concrete syntax is controversial ("{apples}"
vs. "$oranges"), so I'm just adding a simple DYI version until we
agree on a concrete syntax
 2020-06-26 16:52:37 +01:00
Edwin Brady
176f2516da
Merge pull request #365 from edwinb/lineario 
Add linear network library
 2020-06-25 12:58:26 +01:00
Edwin Brady
33957c4328 contrib needs to be built before network now 2020-06-25 12:12:20 +01:00
Edwin Brady
531170e949 Add linear network API 
This involves updating the bootstrap code since it needs a fix in
interface resolution. It shouldn't affect the Idris2-boot build though,
since it's in the libraries not the Idris2 source.
 2020-06-25 12:07:33 +01:00
Edwin Brady
9576fdc1d3 LIO.run needs exporting 
It's useless without it!
 2020-06-25 11:57:17 +01:00
Niklas Larsson
534fc0e073
Merge pull request #353 from stepancheg/modns 
Better TTC data is in an older format message
 2020-06-25 10:47:46 +02:00
Niklas Larsson
8d75d70fac
Merge pull request #342 from csabahruska/master 
add unit test for constructor duplicate
 2020-06-25 10:39:25 +02:00
Edwin Brady
0f71464ab5
Merge pull request #363 from edwinb/lineario 
More on the Linear IO experiment
 2020-06-25 00:10:09 +01:00