Niklas Larsson
fe380861a9
Merge pull request #286 from nickdrozd/contrib
...
Port over some stuff from contrib
2020-06-16 00:14:40 +02:00
Nick Drozd
f027346d52
Add note about cong
2020-06-15 14:56:19 -05:00
Nick Drozd
b096062858
Fill in missing Nat proofs
2020-06-15 14:56:19 -05:00
Nick Drozd
3b0496b8ab
Port over some contrib stuff
...
I didn't add any export labels because none of this is actually useful
for anything, but the proofs are cool.
2020-06-15 14:56:19 -05:00
Niklas Larsson
de6dc57502
Set the first supplied codegen as the default
2020-06-15 16:11:08 +02:00
Niklas Larsson
e32700cff8
Add test
...
It takes a long time to run, but it is basically all
the testing we need of the API, if this works it's
unlikely to be broken. It requires a change in the build
system, so don't enable it for now.
2020-06-15 16:11:08 +02:00
Niklas Larsson
2ec923d4f3
Add documentation
2020-06-15 16:11:08 +02:00
Niklas Larsson
5221954aca
Prepare for additional codegens
...
The idea is to make everything accessible via the API, so
codegen implementors will be able to reuse all infrastructure by calling
the appropriate function in Idris.Driver supplying their codegen.
2020-06-15 16:11:05 +02:00
Niklas Larsson
9f325945b9
Merge pull request #285 from ShinKage/code-in-errors
...
[RFC] Better error messages - show failing code in error messages
2020-06-15 16:07:30 +02:00
Giuseppe Lomurno
788ae023e3
Merge remote-tracking branch 'upstream/master' into code-in-errors
2020-06-15 15:12:49 +02:00
Giuseppe Lomurno
94e69f1d67
Rebase to master
2020-06-15 14:20:40 +02:00
Niklas Larsson
5751a12aa0
Merge pull request #306 from ska80/help-options-fmt
...
Improve help options formatting
2020-06-15 14:16:19 +02:00
Niklas Larsson
4dc151086c
Merge pull request #283 from timsueberkrueb/more-file-io
...
Extend Control.App.FileIO
2020-06-15 14:13:17 +02:00
Niklas Larsson
9ab5f55b57
Merge pull request #284 from clayrat/master
...
Various stdlib updates
2020-06-15 14:04:46 +02:00
Alex Gryzlov
2912b194d5
fix coverage010
2020-06-15 13:22:04 +02:00
Kamil Shakirov
3a67dee49c
Group similar help options
2020-06-15 15:29:48 +06:00
Kamil Shakirov
50303ffa88
Improve help options formatting
2020-06-15 14:14:18 +06:00
Alex Gryzlov
2ee42e777a
Merge remote-tracking branch 'upstream/master'
2020-06-15 03:01:57 +02:00
Niklas Larsson
ca20213adf
Merge pull request #290 from ska80/cmd-default-host-port
...
Remove hardcoded default 'host' and 'port' parts from command-line he…
2020-06-14 12:03:01 +02:00
Niklas Larsson
3c42e0e83d
Merge pull request #299 from melted/debug_buf
...
Debug printing for buffers
2020-06-14 11:52:31 +02:00
Niklas Larsson
d79d1b5587
Align last row with ugly hack
2020-06-14 00:57:53 +02:00
Giuseppe Lomurno
6d531cd310
Remove todo
2020-06-13 23:52:54 +02:00
Niklas Larsson
0afd1eb3a2
Add character printing
2020-06-13 22:09:51 +02:00
Niklas Larsson
1227f2e8a1
Add buffer dumping
2020-06-13 21:57:20 +02:00
Giuseppe Lomurno
c995fe4a01
Merge remote-tracking branch 'upstream/master' into code-in-errors
2020-06-13 18:20:12 +02:00
Giuseppe Lomurno
778d930f95
Updated tests
2020-06-13 16:51:05 +02:00
Giuseppe Lomurno
7b903be9ed
More precise token boundaries
2020-06-13 16:50:54 +02:00
Niklas Larsson
a33fc1ec16
Merge pull request #256 from vilunov/repl-package
...
"--repl" command for opening a REPL in a package
2020-06-12 17:50:50 +02:00
Niklas Larsson
232c69de0d
Merge pull request #245 from FrederikVigen/master
...
Added fix to recvAll that doesn't use signal (Left 0)
2020-06-12 17:50:05 +02:00
Tim Süberkrüb
30410eda52
Add fflush to Control.App.FileIO
2020-06-12 17:30:54 +02:00
Tim Süberkrüb
535918a3ac
Deduplicate Control.App.FileIO
2020-06-12 17:30:54 +02:00
Tim Süberkrüb
e9a80891b7
Extend Control.App.FileIO
2020-06-12 17:30:54 +02:00
Alex Gryzlov
4fffdec6e8
Merge remote-tracking branch 'upstream/master'
2020-06-12 16:39:37 +02:00
Edwin Brady
6246b8d702
Merge pull request #292 from edwinb/linear-things
...
Some small linearity improvements, and linear arrays
2020-06-12 14:53:34 +01:00
Edwin Brady
84adbe6dc8
Be explicit about multiplicity in Array
...
The bootstrap version can't infer it!
2020-06-12 14:18:57 +01:00
Edwin Brady
c3c556f192
Merge https://github.com/idris-lang/Idris2 into linear-things
2020-06-12 14:16:01 +01:00
Edwin Brady
ec89b97896
Add note to CHANGELOG
2020-06-12 14:12:32 +01:00
Edwin Brady
1c576cb068
Add experimental support for linear arrays
...
Backed by Data.IOArray. Also moved the array external primitives to a
separate module Data.IOArray.Prims, since the next step is to add a
linear bounded array type where the bounds checks are done at compile
time, so we'll want to read and write without bounds likes.
2020-06-12 14:08:00 +01:00
Niklas Larsson
9e4c7c3019
Merge pull request #289 from jfdm/comment-out-unimplemented-proofs-from-data-nat
...
Remove unsolved holes from `base`.
2020-06-12 14:57:12 +02:00
Niklas Larsson
405ebd0095
Merge pull request #287 from jfdm/safe-indexing-of-lists
...
Safe indexing of lists
2020-06-12 14:56:57 +02:00
Edwin Brady
b2c7029b6b
Improve inference of linearity in let
...
This involves a bit of backtracking in linearity checking, which I'd
prefer to avoid, but it won't hurt in the normal case. If checking a
binder fails due to linearity misuse, try again at linear multiplicity.
2020-06-12 13:47:15 +01:00
Jan de Muijnck-Hughes
da81146388
Remove unsolved holes from base
.
...
Having unsolved holes in a 'core' library unneccessarily pollutes the list of holes shown to the user.
Thus, having unfilled holes in a 'core' library is not right.
These constructs can be re-added once the holes have been filled in.
2020-06-12 13:13:48 +01:00
Jan de Muijnck-Hughes
f7cf2dfb06
Ported safe indexing of Lists from Idris1 prelude.
2020-06-12 13:12:15 +01:00
Niklas Larsson
d86d96f35a
Merge pull request #291 from melted/fix_refl003
...
Fix overly nitpicky reflection test
2020-06-12 13:16:48 +02:00
Niklas Larsson
4b7fbb0371
Fix overly nitpicky reflection test
...
See #287
2020-06-12 12:46:19 +02:00
Edwin Brady
c9b20911e1
Add linear pair/dependent pair to the prelude
...
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
2020-06-12 11:18:12 +01:00
Kamil Shakirov
658953681f
Remove hardcoded default 'host' and 'port' parts from command-line help options
2020-06-12 16:12:33 +06:00
Niklas Larsson
49290e44be
Merge pull request #288 from ska80/cmd-default-gc
...
Remove hardcoded default CG from command line options
2020-06-12 12:06:28 +02:00
Kamil Shakirov
4d7e6eef6e
Revert TTC changes
2020-06-12 15:36:38 +06:00
Kamil Shakirov
01c79f17d2
Change the TTC version
2020-06-12 15:31:48 +06:00