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
1,618 Commits 6 Branches 9 Tags 113 MiB
d2eeb7ce86
Commit Graph

195 Commits

Author SHA1 Message Date
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095) 2021-02-24 11:07:16 +00:00
Guillaume ALLAIS
00067e8151 [ fix #637 ] force indentation after a with 2021-02-23 10:52:22 +00:00
G. Allais
74b051589b
[ new ] Perfect binary trees (#1063) 2021-02-22 09:54:16 +00:00
Mathew Polzin
c3a42966e7 fix indentation in Golden so that prompt happens after both paths under expected and actual outputs don't match. 2021-02-22 09:39:57 +00:00
Guillaume ALLAIS
5b5bdfe769 [ contrib ] Positions in strings 
This is an alternative to using `fastUnpack` and `fastPack` to work
on lists of characters.

Using this to refactor the lexer and benchmarking the resulting
compiler on building idris2 shows it's 3 to 5s slower than the
current implementation that goes via `List Char`.

This may be backend-dependent so I still push this to contrib,
with the plan of running further benchmarks in the future.
 2021-02-18 17:52: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
Giuseppe Lomurno
70d1505c5c Change PreorderReasoning arguments to 0 2021-02-14 15:12:17 +00:00
Michael Messer
4baacc322b Generalize Category 2021-02-11 09:38:26 +00:00
G. Allais
8ba3d8572b
[ new ] Data.OpenUnion (#1050) 2021-02-10 15:25:35 +00:00
Ohad Kammar
aa72203fc8
Preliminary datatypes for telescopes (#703) 
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-02-09 14:18:41 +00:00
stefan-hoeck
8102e9e495 add Data.Int.Order to contrib.ipkg 2021-02-07 11:49:35 +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
G. Allais
d9e0841245
[ contrib ] support for C backend (#1015) 2021-02-02 15:31:30 +00:00
Denis Buzdalov
72229e3232 Important LazyList's operations were made to be truly lazy. 2021-01-27 19:38:08 +00:00
Guillaume ALLAIS
708b5c300a [ new ] Order relations on Int 2021-01-27 18:23:40 +00:00
stefan-hoeck
7ef6b79ab1 Remove Control.Monad.Trans.Either from contrib 2021-01-22 08:10:47 +01:00
stefan-hoeck
8074ad1f8d Make Control.Validation use Control.Monad.Error.Either 2021-01-22 08:08:34 +01:00
André Videla
60527d127f
Merge pull request #554 from Sventimir/validation 
Input validation
 2021-01-22 01:30:07 +00:00
André Videla
3bd2fae525
Update Arrow.idr 2021-01-22 00:54:58 +00:00
André Videla
2e063544e8
Update Category.idr 2021-01-22 00:53:59 +00:00
André Videla
016cd213b9
Delete Either.idr 2021-01-22 00:53:12 +00:00
Stefan Hoeck
0906ac30b9
added System.Console.GetOpt to contrib (#974) 2021-01-21 17:59:06 +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
Ruslan Feizerahmanov
515453329a
Revert back to linear iterators (#938) 2021-01-21 12:37:30 +00:00
Stefan Hoeck
fb08004041
removed trailing whitespace (#955) 2021-01-21 11:33:03 +00:00
Fabián Heredia Montiel
a23871e57e Execute tests concurrently 2021-01-19 18:40:35 +00:00
Edwin Brady
efae2682bd
Merge pull request #896 from Russoul/toString-iterators 
Add withIteratorString
 2021-01-16 15:47:45 +00:00
Alex Gryzlov
c67fc5d7c0
add Inspect idiom (#919) 2021-01-16 14:18:34 +00:00
Edwin Brady
96257f23c3
Merge pull request #914 from stefan-hoeck/lazy-list-impls 
Eq, Ord, and Show instances for LazyList
 2021-01-16 14:07:26 +00:00
Stiopa Koltsov
b76c9d91e0 Remove trailing whitespaces and add trailing newlines 2021-01-16 10:00:03 +00:00
André Videla
bea840418a
Merge pull request #823 from andylokandy/path 
Changes to System.Path

- Rename `startWith` to `isBaseOf`
- Rename `stripPrefix` to `dropBase`
- Add `dropExtension`
- Add `splitPath`
 2021-01-14 22:09:04 +00:00
Andy Lok
4f8bd22b35 Use present tense in doc for Path 2021-01-14 05:26:42 +08:00
Andy Lok
f1d6d4d6f4 Use dot syntax to avoid path argument 2021-01-14 05:05:59 +08:00
André Videla
c1bd61b58d
Merge branch 'master' into validation 2021-01-13 17:07:18 +00: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
530e62a156 Eq, Ord, and Show instances for LazyList 2021-01-11 11:45:56 +01:00
Mathew Polzin
ab96d771c9 finish removing duplication between the exported 'list reverse' properties in base and those in contrib. 2021-01-10 20:40:45 -08:00
Felix Springer
54d400dad4
Add countExactly to Text.Parser in libs/contrib to return a Vect (#875) 2021-01-01 10:01:42 +00:00
russoul
79d0cd1ba6 Add withIteratorString 2020-12-31 20:36:07 +03:00
Edwin Brady
3b987b10e9 Another multiplicity subtyping fix 2020-12-29 21:47:53 +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
b75dcd5c17 Some multiplicity fixes in the libraries 2020-12-29 21:25:00 +00:00
Joey Eremondi
0eef8e58f9
Some utilities for Fin, relations and decidability (#857) 2020-12-28 21:41:12 +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
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
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
9f72a514f1 Rename startWith to isBaseOf 2020-12-07 15:26:00 +08:00