Guillaume ALLAIS
09d8e25441
[ refactor ] more efficient implementation of range
2021-03-30 10:51:56 +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
stefan-hoeck
6824111fd8
[ performance ] add fastUnlines to base
2021-03-26 12:35:29 +00:00
Alex Gryzlov
71abc8e33b
Add Path@contrib & small changes ( #1229 )
2021-03-25 16:01:32 +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
Andy Lok
da92f9d676
Cleanup List1 ( #1091 )
2021-03-17 14:07:52 +00:00
CodingCellist
89a84a34a4
Patch CVs and sleep
in Racket ( #1059 )
2021-03-15 13:43:12 +00:00
robert
9300d22c31
colist
2021-03-15 13:36:05 +00:00
stefan-hoeck
0fd9ed0555
[ new ] Interface implementations for Subset
2021-03-09 11:25:03 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base ( #1033 )
2021-03-04 20:59:56 +00:00
Stefan Höck
4c7d0db4bc
[ fix #1148 ] Support hyphenated package names ( #1151 )
2021-03-04 19:09:15 +00:00
G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' ( #1093 )
2021-03-01 08:29:43 +00:00
Denis Buzdalov
7a8c12771b
[ base ] A property of interaction between zipWith
and index
( #1128 )
2021-03-01 08:29:17 +00:00
Edwin Brady
4726c32d94
Add --ignore-missing-ipkg flag
...
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.
We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
2021-02-27 19:39:47 +00:00
Edwin Brady
37cc095f7a
Merge github.com:idris-lang/Idris2 into versions
2021-02-27 18:00:18 +00:00
Edwin Brady
1052c41a3c
Use version number field in ipkg
...
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
2021-02-27 14:15:19 +00:00
André Videla
aa27ccbdb6
Merge pull request #1097 from andylokandy/multiline
...
Implement multi-line string
2021-02-26 21:50:54 +00:00
G. Allais
59de5f1326
[ fix #762 ] Different case tree building strategy ( #1125 )
2021-02-26 09:33:07 +00:00
claymager
33e336ad27
Give App1 implementation of (>>) ( #1122 )
2021-02-25 17:09:24 +00:00
Andy Lok
5fed5c2b7a
Merge branch 'master' of https://github.com/idris-lang/Idris2 into multiline
2021-02-25 19:52:42 +08:00
Denis Buzdalov
874496e1ae
[base] Constructor's injectivity proofs for Exists
and Subset
( #1118 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-02-24 19:11:41 +00:00
Denis Buzdalov
69be8f2102
[base] bimap
functions were added for dependent pairs.
2021-02-24 16:41:33 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) ( #1095 )
2021-02-24 11:07:16 +00:00
Mark Barbone
0f7fa149c7
Make zip
infixr 6
2021-02-23 10:54:28 +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
Donovan Crichton
1b9a220c42
Added comment descriptions for FC and FilePos.
2021-02-22 09:55:34 +00:00
G. Allais
74b051589b
[ new ] Perfect binary trees ( #1063 )
2021-02-22 09:54:16 +00:00
G. Allais
30d402ed7f
[ fix #899 ] Be careful when generating an impossible LHS ( #1081 )
2021-02-22 09:53:30 +00:00
Andy Lok
22a769e6b5
Implement multiline string
2021-02-20 18:05:26 +08:00
Mathew Polzin
d5d0b64b4a
withFile & writeFile cleanup ( #1085 )
2021-02-18 17:51:45 +00:00
Mathew Polzin
9f8a8b5d76
Add a total way of reading files in. ( #1070 )
2021-02-18 11:13:25 +00:00
Denis Buzdalov
b355b12cdb
Some cleanup was done. Changed code is mosly equivalent to the former.
...
A lot of useless matches of implicit arguments were removed.
2021-02-16 19:05:33 +00:00
Denis Buzdalov
0ac34538ec
A function from Not (x = y)
to decEq x y = No _
was added.
2021-02-16 12:43:50 +00:00
Denis Buzdalov
4f28b92a19
Zero quantities were added to some interface usages.
2021-02-12 20:51:13 +00:00
Denis Buzdalov
123fbb7f33
weakenN
's n
parameter was made to have zero quantity.
2021-02-09 14:15:59 +00:00
SmiVan
952e20cc57
IOArray.fromList moved to HasIO
2021-02-06 20:37:15 +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
Denis Buzdalov
5beda25da6
Seemingly outdated and non-typechecking module was removed.
2021-02-01 16:10:54 +00:00
Kamil Shakirov
173edb14a6
Remove unused modules
2021-02-01 14:26:18 +00:00
Stefan Hoeck
39824c6295
[new] Add Colist and Colist1 to base ( #997 )
2021-02-01 10:27:07 +00:00
Stiopa Koltsov
cff7db38cb
Control.App: use new type instead of Void as marker for I/O
...
Took me some time to figure out that `Void` means `IO`.
Express that knowledge more explicitly.
2021-01-31 11:58:10 +00:00
Andy Lok
5b367da2c9
[ refactor ] Rename Data.Strings to Data.String (1/2) ( #987 )
2021-01-27 19:18:34 +00:00
Kamiλ Shakirov
140879f7b9
[ new ] Zippable interface ( #990 )
2021-01-27 18:23:08 +00:00
Kamiλ Shakirov
3bbf52025a
Add zip*/unzip* for List1 ( #986 )
2021-01-26 10:39:16 +00:00
Rodrigo B. de Oliveira
dbea094a31
Fix Language.Reflection
definition of INamespace
...
Fixes #943
2021-01-22 18:10:01 +00:00
mapf0ld
e15b1f0c78
[ refactor ] ltrim in terms of asList ( #894 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-01-22 15:07:23 +00:00
Kamil Shakirov
b540313c57
Add unzipWith and unzipWith3 for Stream
2021-01-22 10:41:16 +00:00
Kamil Shakirov
29cd9e86ec
Add unzipWith and unzipWith3 for Vect
2021-01-22 10:41:16 +00:00
André Videla
60527d127f
Merge pull request #554 from Sventimir/validation
...
Input validation
2021-01-22 01:30:07 +00:00
G. Allais
af94feb18e
Merge pull request #960 from stefan-hoeck/transformer-overhaul
2021-01-21 16:30:59 +00:00
Kamiλ Shakirov
db30dd3f16
Port Data.List.unzip from Idris1 ( #972 )
2021-01-21 16:30:00 +00:00
André Videla
0c665bc952
Merge pull request #884 from mattpolzin/list-reverse-involutory
...
Add proof that list reverse is involutive into base.
2021-01-21 13:33:34 +00:00
Jakub Okoński
1376bdf3f2
libs: mark Data.Nat.lteAddRight as public export
2021-01-21 12:40:17 +00:00
Stiopa Koltsov
0d363c9732
Add isYes function and friends
...
Added several functions for `Dec`. The set of functions and names
are picked consistently with `Maybe`:
* `isNothing` -> `isNo`
* `isJust` -> `isYes`
* `IsJust` -> `IsYes`
* `isItJust` -> `isItYes`
This is follow-up to #942
2021-01-21 12:36:02 +00:00
stefan-hoeck
92b9833ee2
fixed doc for WriterT
2021-01-21 13:25:48 +01:00
stefan-hoeck
fd4851c0f5
strict, not stricht
2021-01-21 13:24:40 +01:00
Stefan Hoeck
fb08004041
removed trailing whitespace ( #955 )
2021-01-21 11:33:03 +00:00
stefan-hoeck
d36a234041
finished MonadRWS
2021-01-20 05:58:19 +01:00
stefan-hoeck
e906b28cae
removed MonadState functions from RWS.CPS.idr
2021-01-20 05:51:39 +01:00
stefan-hoeck
e8f2f56768
removed MonadWriter functions from RWS.CPS.idr
2021-01-20 05:48:43 +01:00
stefan-hoeck
6f2e358f1b
removed MonadReader functions from RWS.CPS.idr
2021-01-20 05:45:32 +01:00
stefan-hoeck
2776eaa1b1
remove MonadWriter functions from Writer.CPS module
2021-01-20 05:41:01 +01:00
stefan-hoeck
b6e5ba0830
minor MonadWriter cleanup
2021-01-20 05:27:56 +01:00
stefan-hoeck
313f52a88a
explicit lambdas for mapXYZ functions
2021-01-20 05:27:08 +01:00
stefan-hoeck
a42a34e9f0
removed trailing whitespace
2021-01-19 17:53:42 +01:00
stefan-hoeck
b5ab96477c
some cleanups in State
2021-01-19 17:47:06 +01:00
stefan-hoeck
8c9e318a6d
some cleanups in Reader
2021-01-19 17:43:47 +01:00
stefan-hoeck
7999420e88
made functions in EitherT and MaybeT public export
2021-01-19 17:38:59 +01:00
stefan-hoeck
c75d14fa8a
implemented MonadWriter
2021-01-19 16:19:27 +01:00
stefan-hoeck
01ba3aa365
moved MonadState to its interface module
2021-01-19 15:45:19 +01:00
stefan-hoeck
dac566152b
moved MonadReader to its interface module
2021-01-19 15:12:36 +01:00
stefan-hoeck
12f1ff493e
added mapStateT function
2021-01-19 14:57:10 +01:00
stefan-hoeck
8eb0e855f1
removed RWST function reader
2021-01-19 14:41:26 +01:00
stefan-hoeck
8cb2220e58
implemented cps-style Writer
2021-01-19 14:34:15 +01:00
stefan-hoeck
b9f7683fbd
mapRWST needs only a Functor
2021-01-19 14:11:06 +01:00
stefan-hoeck
b2e7384a80
implemented cps-style RWST
2021-01-19 13:58:18 +01:00
stefan-hoeck
81efdd7992
implementations for MonadError
2021-01-19 12:35:05 +01:00
stefan-hoeck
124afd89b1
moved transformer impls to their own directory
2021-01-19 11:53:23 +01:00
stefan-hoeck
b926e13b96
new transformer layout
2021-01-19 11:45:54 +01:00
Stiopa Koltsov
7264d40c56
Make isElem, DecEq public, not just export
...
... so they could be used in proof search.
Follow-up to #942
2021-01-18 10:37:57 +00:00
Edwin Brady
c7783c553c
Make the linter happier
2021-01-16 17:18:38 +00:00
Edwin Brady
6df2955a72
Merge pull request #909 from stefan-hoeck/maybeT
...
added MaybeT monad transformer to base
2021-01-16 15:43:14 +00:00
Edwin Brady
70c87e49da
Merge pull request #920 from stefan-hoeck/eithert-foldable-fix
...
fixed bug in Foldable of EitherT
2021-01-16 15:40:33 +00:00
Stiopa Koltsov
b76c9d91e0
Remove trailing whitespaces and add trailing newlines
2021-01-16 10:00:03 +00:00
Denis Buzdalov
4f05d227a6
List-level quantifier conversion to element-level and vice-versa
2021-01-15 18:57:01 +00:00
Denis Buzdalov
bcc8da5a6d
Currying and uncurrying functions for dependent pairs were added.
2021-01-15 18:53:40 +00:00
Denis Buzdalov
6d2dd935c4
Special variants of DPair
as records ( #922 )
2021-01-15 17:19:20 +00:00
André Videla
c1bd61b58d
Merge branch 'master' into validation
2021-01-13 17:07:18 +00:00
stefan-hoeck
7b73072554
fixed bug in Foldable of EitherT
2021-01-13 13:21:20 +01:00
Stefan Hoeck
77a911aa8a
Update libs/base/Control/Monad/Maybe.idr
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-01-13 11:19:03 +01:00
stefan-hoeck
e52b658d78
no linearity annotation for MkMaybeT
2021-01-13 05:34:07 +01:00
Edwin Brady
3621c5d1bd
Merge pull request #879 from edwinb/no-linearity-subtyping
...
Remove linearity subtyping
2021-01-12 12:33:26 +00:00
Edwin Brady
d4abbfdae2
Add HasLinearIO
...
Ideally, liftIO would always be linear, but that has lots of knock-on
effects for other monads which we might want to put in HasIO, now that
subtyping is gone. We'll have to revisit this when we have some kind of
multiplicity polymorphism.
2021-01-11 11:24:43 +00:00
stefan-hoeck
c39df89f84
deleted 'head' from Data.Stream
2021-01-11 09:36:13 +00:00
stefan-hoeck
31f50a793c
added prelude function 'on'
2021-01-11 05:26:17 +01:00
Mathew Polzin
a32aa42d3f
Merge branch 'master' into list-reverse-involutory
2021-01-10 20:17:55 -08:00
stefan-hoeck
c1912cb212
Monad prerequisite for Semigroup instance
2021-01-11 05:05:33 +01:00
stefan-hoeck
e71c7b8946
added MaybeT monad transformer to base
2021-01-08 06:04:41 +01:00
André Videla
3478297557
Merge pull request #905 from alebahn/master
...
Add public export to types/functions in Data.Fin.Order
2021-01-07 13:46:23 +00:00
Mathew Polzin
e9324fcd60
Rename to reverseInvolutive
2021-01-06 08:45:44 -08:00
André Videla
e4fcd4a089
Merge pull request #900 from andrevidela/vect-snoc
...
Add `snoc` to Data.Vect
2021-01-05 21:54:47 +00:00
Michael Messer
a1f3424ab8
Remove lamdaRequire
2021-01-05 16:30:11 +00:00
Aaron Lebahn
ce6465e279
Add public export to types/functions in Data.Fin.Order
2021-01-05 07:56:04 -06:00
André Videla
738c9d77d2
Add snoc
to Data.Vect
...
Snoc add an element at the end of the vector. The main use case
for such a function is to get the expected type signature
Vect n a -> a -> Vect (S n) a instead of
Vect n a -> a -> Vect (n + 1) a which you get by using `++ [x]`
Snoc gets is name from `cons` by reversin each letter, indicating
tacking on the element at the end rather than the begining.
`append` would also be a suitable name.
2021-01-03 21:48:31 +00:00
Edwin Brady
cc6530026d
Merge github.com:idris-lang/Idris2 into no-linearity-subtyping
2020-12-29 21:37:56 +00:00
Edwin Brady
8d034a0a91
Relax some linearities in the base libraries
2020-12-29 21:34:35 +00:00
Edwin Brady
b75dcd5c17
Some multiplicity fixes in the libraries
2020-12-29 21:25:00 +00:00
Mathew Polzin
bc76809288
Add proof that list reverse is involutory.
2020-12-28 17:30:24 -08:00
Joey Eremondi
0eef8e58f9
Some utilities for Fin, relations and decidability ( #857 )
2020-12-28 21:41:12 +00:00
Edwin Brady
5b97cd4499
Fix annotaion in Stream
2020-12-27 20:13:21 +00:00
Edwin Brady
61ba5e086f
Fix linearity annotation in take
...
Hopefully this fixes the bootstrap build
2020-12-27 20:11:06 +00:00
Edwin Brady
ad632d825d
Remove linearity subtyping
...
It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes #73 (and maybe some others).
2020-12-27 19:58:35 +00:00
André Videla
9c400a185e
Add Traversable to List1
2020-12-21 15:10:00 +00:00
Denis Buzdalov
60e9cf44b0
Add List, LazyList and Stream unfolds and some LazyList's functions
2020-12-18 22:54:03 +00:00
Denis Buzdalov
bff74807fd
Some functions, mostly for lazy lists ( #854 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2020-12-18 10:33:56 +00:00
tensorknower69
aa940c3d18
change runState's signature
2020-12-17 10:10:18 +00:00
tensorknower69
c48b1e090e
add execStateT and evalStateT
2020-12-17 10:10:18 +00:00
G. Allais
3f6b99e979
[ fix #657 ] RigCount for interface parameters ( #808 )
2020-12-11 11:58:26 +00:00
Dong Tsing-hsuen
88aa55e875
[ new ] null method in Foldable ( #832 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-12-10 18:04:23 +00:00
Andy Lok
9e22a6e07b
Add javascript FFI for fastUnpack
( #816 )
2020-12-06 09:54:58 +00:00
Denis Buzdalov
13cc27da1f
An alternative (Fin-based) indexing function was added for lists.
2020-12-04 19:09:05 +00:00
Denis Buzdalov
4364793484
Type definition from Decidable.Equality
was moved to a separate module
...
This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).
2020-12-04 19:09:05 +00:00
Edwin Brady
778d6026e5
Merge pull request #607 from Russoul/record-init
...
New syntax for named applications and "record" updates
2020-12-04 11:35:05 +00:00
Denis Buzdalov
f2596318e5
Proof of list bounds was made to be not present at runtime when indexing
2020-12-04 11:26:11 +00:00
russoul
46519237cd
Merge
2020-12-03 15:28:20 +03:00
Mathew Polzin
6ca03acd71
Add replaceWhen
for lists. ( #755 )
2020-11-27 19:10:08 +00:00
G. Allais
5e799563fa
[ contrib ] adding Data.Container ( #781 )
2020-11-27 15:29:19 +00:00
Jan de Muijnck-Hughes
de58c66ab2
Make Idris2 test harness available for the many and not the few. ( #719 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-10-19 09:26:23 +01:00
russoul
fd90141ed9
Merge branch 'master' of https://github.com/idris-lang/Idris2 into master
2020-10-12 17:36:45 +03:00
Matus Tejiscak
f64163de1f
Merge branch 'unscheme' into master
2020-10-11 08:20:01 +02:00
Matus Tejiscak
668762e693
Merge branch 'revert-projections' into master
2020-10-11 08:12:00 +02:00
Ohad Kammar
0c1a124704
Division theorem ( #695 )
...
Division Theorem. For every natural number `x` and positive natural
number `n`, there is a unique decomposition:
`x = q*n + r`
with `q`,`r` natural and `r` < `n`.
`q` is the quotient when dividing `x` by `n`
`r` is the remainder when dividing `x` by `n`.
This commit adds a proof for this fact, in case
we want to reason about modular arithmetic (for example, when dealing
with binary representations). A future, more systematic, development could
perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics:
https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idr
https://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idr
https://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr
In the process, it bulks up the stdlib with:
+ a generic PreorderReasoning module for arbitrary preorders,
analogous for the equational reasoning module
+ some missing facts about Nat operations.
+ Refactor some Nat order properties using a 'reflect' function
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2020-10-06 13:09:02 +01:00
russoul
98bfff4a27
Merge branch 'master' of https://github.com/idris-lang/Idris2 into master
2020-10-03 11:51:48 +03:00
G. Allais
4a61146ba0
[ fix #705 ] Normalise primitives in mkPat ( #718 )
...
[ log ] prettier log for pats & clauses
[ re #650 ] Even lazier
[ fix #705 ] normalise primitives in mkPat
[ refactor ] introduce getPrimitiveNames
2020-10-02 12:22:57 +01:00
russoul
b57b28a64e
Implement new application syntax
...
Add syntax for bind-all-explicits
Add new record update syntax
Remove PInstance
2020-10-01 12:43:43 +03:00
Arnaud Bailly
85f5d00054
fix totality annotation on some Nat functions
2020-09-30 10:51:51 +01:00
Ruslan Feizerahmanov
1d99a28176
Add Bifunctor interface ( #701 )
2020-09-30 10:51:07 +01:00
G. Allais
3df1f9c476
[ fix #63 ] interleaving let binders and local declarations ( #691 )
2020-09-28 13:15:22 +01:00
MarcelineVQ
315fc8ce2d
change ForeignFn to use TTImp to match RawImp version
2020-09-24 09:00:00 +01:00
G. Allais
d105dd11a7
[ breaking ] remove List1 related ambiguities ( #690 )
2020-09-22 15:07:40 +01:00
Ohad Kammar
e77b9b4631
[minor] Make base/Data.Nat.divNatNZ
compile-time reducible ( #689 )
...
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
2020-09-22 09:53:05 +01:00
MarcelineVQ
e03096188a
add more Name reflections
...
broaden what Names can be reflected and refied
I did not add the Names I wasn't sure how to test but have put placeholders
that produce clearer error messages.
2020-09-20 00:54:49 -07:00
Matus Tejiscak
e73c6ae3c6
Add comments to fastUnpack and fastConcat.
2020-09-19 19:19:09 +02:00
Matus Tejiscak
63c3ebf124
Remove ambiguities.
2020-09-19 14:46:12 +02:00
Matus Tejiscak
5f9c94a4e1
Fix access modifiers of fastUnpack and fastConcat.
2020-09-19 14:43:08 +02:00
Matus Tejiscak
5360adcc23
String-related stdlib tweaks.
2020-09-19 14:22:54 +02:00
MarcelineVQ
ea0df039fe
change runReader's to take state first to allow easier use
...
following up on the change made in 5c76053cf3
to encourage people to do it in this manner going forward
2020-09-15 22:46:07 +01:00