idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity
1,328 Commits 6 Branches 9 Tags 115 MiB
738c9d77d2
Commit Graph

211 Commits

Author SHA1 Message Date
MarcelineVQ
209de36ba0
add EitherT transformer (#590) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-08-25 11:14:09 +01:00
Matus Tejiscak
f69443985b Revert addition to ES preamble. 2020-08-25 10:25:45 +02:00
Matus Tejiscak
e9e5ef3d6a Fix FFI specifier. 2020-08-25 10:23:07 +02:00
Matus Tejiscak
1eaecc5d66 Implement stringConcat in Node. 2020-08-25 09:46:35 +02:00
Matus Tejiscak
969a6e1a45 Make fastAppend a deprecated alias of fastConcat. 2020-08-24 19:51:23 +02:00
Matus Tejiscak
362d2204ab Make fastAppend a foreign call. 2020-08-24 19:51:22 +02:00
russoul
594105d5ac Eliminate schemeCall from the library 2020-08-24 19:38:29 +03:00
G. Allais
da78ac4783
[ new ] topics for logging levels (#569) 2020-08-20 18:45:34 +01:00
Cole Brown
f227735cec Add local to MonadReader interface 2020-08-20 16:33:50 +01:00
Cole Brown
6c3ab219bc Implement MonadReader and related types/instances 
This includes:
- ReaderT transformer
- Instances for Functor, Applicative, Monad, MonadTrans, HasIO,
  Alternative
- asks helper function
- Reader alias
 2020-08-20 16:33:50 +01:00
Kamil Shakirov
8544e80076 Use the same naming convention for foreign primitives 2020-08-19 14:05:28 +01:00
Arnaud Bailly
8ecf664ff6
Port Decidable.Order from Idris1 (#543) 2020-08-18 22:26:56 +01:00
Niklas Larsson
84ae9d7c6e
Merge pull request #523 from mb64/hasio-statet 
Implement HasIO for StateT
 2020-08-18 14:02:02 +02:00
Thomas Dziedzic
a1739a69a0
Update app docs (#537) 2020-08-10 10:05:23 +01:00
Mark Barbone
10d28efd52
Implement HasIO for StateT 2020-08-04 17:19:45 -04:00
G. Allais
0a7ea69df5
[ refactor ] introduce List1 to remove impossible case (#520) 2020-08-04 20:03:18 +01:00
Edwin Brady
2761a27357
Merge pull request #476 from nickdrozd/algebra-implementations 
Add some algebra implementations
 2020-08-04 13:21:12 +01:00
Ohad Kammar
5cfbac4a51 Add irrelevance annotations to Data.List functions taking NonEmpty 2020-07-30 06:01:42 +01:00
Alex Gryzlov
69612bf6bf
Add list lemmas (#491) 2020-07-29 10:51:07 +01:00
Ohad Kammar
915b7bea38 Add various instances from stdlib interfaces (Eq, Ord, DecEq) 
For Void and Either

This is because I ended up using them elsewhere, so why not include them in the stdlib.

Also expose left/rightInjective functions, as are used in the DecEq proofs.
 2020-07-26 10:47:38 +01:00
Niklas Larsson
8a210d536e
Merge pull request #408 from melted/buffer_api 
Add concatBuffers and splitBuffer to Data.Buffer
 2020-07-21 10:43:17 +02:00
Jonathan Chan
dab2b0d146 Export (~>) publicly. 
If `(~>)` isn't publicly exported, the type checker doesn't know that `Mor` constructs something of type `~>`.
 2020-07-20 15:55:24 +01:00
Edwin Brady
f303e469fb Improve elaborator reflection performance 
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.

Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.

This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
 2020-07-17 15:18:23 +01:00
Nick Drozd
a2bdf8e6d7 Add some algebra implementations 2020-07-17 08:25:20 -05:00
G. Allais
0908e76515
[ fix #346 ] Pull List.length into prelude (#450) 2020-07-14 12:15:57 +01:00
Nicolas Biri
aba76206c9 Remove dependency to Vector length in deleteAt 2020-07-14 09:45:33 +01:00
Nick Drozd
e14a589e90 Consolidate boolean expressions 2020-07-12 21:00:33 -05:00
Nick Drozd
6519b5608d Further simplify List 2020-07-12 21:00:33 -05:00
Nick Drozd
718da3d7e6 Simplify Vect 2020-07-12 20:59:00 -05:00
Edwin Brady
b3bb73cfd6
Merge pull request #455 from edwinb/export-nat-prfs 
Data.Nat proofs should be exported
 2020-07-10 23:30:09 +01:00
Edwin Brady
58e28170ac Data.Nat proofs should be exported 
I assumed these were copied directly from the Idris 1 libraries, where
there was an %access directive that we don't have any more.
 2020-07-10 22:59:46 +01:00
Jan de Muijnck-Hughes
fcbfcf6fe2 Added take to Vect. 2020-07-10 21:00:38 +01:00
Ohad Kammar
eceaf98007 Generalise cons-specialised linear zipWith to linear zipWith (lzipWith) 2020-07-10 17:17:19 +01:00
Ohad Kammar
8f09ef9b93 Include a (non-linear) definition for transpose that uses zipWith, 
as it might be easier to reason about, since users may already have proved
stuff about zipWith that they want to reuse
 2020-07-10 12:47:05 +01:00
Edwin Brady
23cbc28b1d
Merge pull request #415 from rbarreiro/javascript 
Javascript
 2020-07-08 22:27:58 +01:00
Matus Tejiscak
3484510f5a Implement postfix dotted application. 2020-07-07 21:06:35 +01:00
Rui Barreiro
2feb4b8299 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-07 14:18:00 +01:00
Markus Pfeiffer
63ddd149ed Remove a superflousy declared argument to idris2_openFile 
This didn't cause a problem before as it was likely just ignored by the C
function. According to Edwin the extra argument is a leftover from when this
was a pure scheme call.
 2020-07-07 11:44:37 +01:00
Nick Drozd
2ae6e06565 Simplify Fin 2020-07-07 10:48:23 +01:00
Nick Drozd
7d1ee9dd08 Simplify Equality 2020-07-07 10:48:23 +01:00
Nick Drozd
48fe4382eb Simplify List 2020-07-07 10:48:23 +01:00
Nick Drozd
877f3702ad Simplify Maybe 2020-07-07 10:48:23 +01:00
Nick Drozd
465be9cb86 Simplify Either 2020-07-07 10:48:23 +01:00
Nick Drozd
faabbfcea1 Add some Uninhabited implementations 2020-07-07 10:48:23 +01:00
Nick Drozd
7c923944ae Add %default total to a few modules 2020-07-07 10:48:23 +01:00
Rui Barreiro
3acc30599e Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 17:09:11 +01:00
Rui Barreiro
68c9990c8a moved big foreign functions to support and added outputDir 2020-07-06 16:58:02 +01:00
Rui Barreiro
b3216758e9 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 11:32:59 +01:00
Niklas Larsson
bba15974a5 Add takeWhile 
add substring and length primitives to Data.Strings
 2020-07-05 21:51:11 +02:00
Edwin Brady
5487290499
Merge pull request #282 from ether42/master 
Fix MkRecord signature
 2020-07-05 14:03:57 +01:00
Rui Barreiro
88f8e745b1 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-05 12:19:45 +01:00
Jan de Muijnck-Hughes
874236aac0 A port of Subset and Exists from Idris1. 
The ports are rather straight forward and I have purposefully written
the documentation to be beginner friendly.

Note, I have diverged from Idris1 over the naming of the projection
functions to make them consistent with `Pair` and `DPair`.
 2020-07-04 11:03:14 +01:00
Alex Gryzlov
afde930e7a
Vect updates (#335) 2020-07-04 11:02:04 +01:00
Niklas Larsson
862bbeb308 Reverse the size check 
I'm unsure how it would handle zero-size buffers if size==pos and no one
would need those anyway.
 2020-07-04 11:37:51 +02:00
Niklas Larsson
ce3096f919 Add concatBuffers and splitBuffer to Data.Buffer 
Expand the buffer test.
 2020-07-04 02:25:41 +02:00
Guillaume ALLAIS
bd14d37ddc [ fix ] make some exports public 2020-07-03 12:01:09 +01:00
Jan de Muijnck-Hughes
5abf053818 Fixed visibility of some list functions. 2020-07-03 11:59:55 +01:00
Niklas Larsson
6673f49731 Convert Data.Buffer to HasIO 2020-07-01 23:33:30 +02: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
Mark Barbone
4916dd23a9
Make Data.Vect linear (#333) 2020-06-30 15:05:19 +01:00
Fabián Heredia Montiel
e488c6cf0e Make applicative implementation of Vect public export 2020-06-29 18:27:57 -05: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
5ed27947cb Small concurrency fixes 
Conditional variables with timeout in Chez didn't work, so changed to a
consistent meaning of the timeout (microseconds). Also fix linearity of
unsafePerformIO.
 2020-06-23 19:06:30 +01:00
Edwin Brady
1e6314c4cc
Merge pull request #345 from edwinb/hasio 
HasIO interface for IO actions
 2020-06-21 20:24:29 +01:00
Edwin Brady
dbdf7dab3d Back to HasIO, remove MonadIO 
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:

- it's easier for backend authors if the type of IO operations is
  slightly less restrictive. For example, if it's in HasIO, that limits
  alternative implementations, which might be awkward for some
  alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
  be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
  instance (I have personally never encountered one - if they turns out
  to exist, again, we can revisit!)
 2020-06-21 19:21:22 +01:00
Rui Barreiro
ca0c8f9d42 node018 passes 2020-06-21 17:54:50 +01:00
Edwin Brady
28855088c2 Split HasIO into HasIO and MonadIO 
For things which don't require (>>=), HasIO is fine, otherwise MonadIO
gives access to the monad interface.
 2020-06-21 14:46:14 +01:00
Matthew Baulch
916c3e7090 Import fgetc and listen from libc (where they actually reside) rather than the support libs 2020-06-21 15:24:45 +10:00
Edwin Brady
d12487f529 HasIO interface for IO actions 
Also updates the Prelude and some base libraries to use HasIO rather
than using IO directly.
 2020-06-21 01:18:43 +01:00
Rui Barreiro
1d2f3d8883 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-06-20 15:11:08 +01:00
Edwin Brady
8c556d0c26
Merge pull request #340 from edwinb/strefs 
Control.Monad.ST and Refs interface
 2020-06-20 13:16:27 +01:00
Edwin Brady
d18aac7afd Move Data.ST to Control.Monad.ST 
Seems a more appropriate place in the hierarchy (also roughly consistent
with where it is in Haskell base)
 2020-06-20 12:51:38 +01:00
Edwin Brady
ab03249d49 Add Data.STRef and a generic Ref interface 2020-06-20 00:46:20 +01:00
Denis Buzdalov
c121181776
Function mapping Not (x=True) to x=False was added for Bools (#322) 2020-06-19 11:13:13 +01:00
Nicolas Biri
c72cb849a8 Add missing modules in base.ipkg 2020-06-18 10:32:51 +01:00
Rui Barreiro
f8f09858e8 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-06-17 23:48:39 +01:00
Rui Barreiro
cb7dc7bffc test node004 passes 2020-06-17 23:29:54 +01:00
Niklas Larsson
630e4219fc Fix unsetenv 
implement Windows support
 2020-06-16 12:09:22 +02:00
Nick Drozd
b096062858 Fill in missing Nat proofs 2020-06-15 14:56:19 -05: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
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
c3c556f192 Merge https://github.com/idris-lang/Idris2 into linear-things 2020-06-12 14:16:01 +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
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
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
Alex Gryzlov
cd443f24f6 various stdlib updates 2020-06-11 23:14:11 +02:00
Kevin Boulain
c148003265 Fix MkRecord signature 
Otherwise we'd get:
  When unifying Name and Maybe Name
  Mismatch between:
          Name
  and
          Maybe Name
  Can't reify as Decl
 2020-06-11 21:54:40 +02:00
Edwin Brady
07ae16123c Only open in binary mode on windows 2020-06-11 14:53:54 +01:00
Edwin Brady
4b1667fdcf Open files in binary mode 
Needed for windows, and harmless on Unix (Idris 1 did it this way).
 2020-06-11 14:35:26 +01:00
Edwin Brady
0a246af449 Make Buffer more primitive 
Meaning that the FFI is aware of it, so you can send arbitrary byte data
to foreign calls. Fixes #209

This means that we no longer need the hacky way of reading and writing
binary data via scheme, so can have a more general interface for reading
and writing buffer data in files.

It will also enable more interesting high level interfaces to binary
data, with C calls being used where necessary.

Note that the Buffer primitive are unsafe! They always have been, of
course... so perhaps (later) they should have 'unsafe' as part of their
name and better high level safe interfaces on top.

This requires updating the scheme to support Buffer as an FFI primitive,
but shouldn't affect Idris2-boot which loads buffers its own way.
 2020-06-11 14:05:52 +01:00
Edwin Brady
4cc4099ace
Merge branch 'master' into nats 2020-06-08 12:11:10 +01:00
Alex Gryzlov
14002213a1 Merge remote-tracking branch 'upstream/master' 2020-06-08 00:27:58 +02:00
Nick Drozd
5665cfab21 Copy over more Nat proofs 2020-06-07 12:19:32 -05:00
Nick Drozd
4292d735eb Simplify Nat proofs 
These changes are strictly nonfunctional.
 2020-06-07 12:19:32 -05:00
Edwin Brady
d5e4dec119 Reflect 'display names' and record field names 
These arise in interface declarations (to give a nicer way of displaying
auto generated names) and for record fields.
 2020-06-07 11:51:09 +01:00