idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity
1,646 Commits 6 Branches 9 Tags 114 MiB
d617290dd5
Commit Graph

196 Commits

Author SHA1 Message Date
Andy Lok
9f72a514f1 Rename startWith to isBaseOf 2020-12-07 15:26:00 +08:00
Andy Lok
5578761bdb Improve splitPath 2020-12-07 05:19:53 +08:00
Andy Lok
d3a74e0199 Update document 2020-12-07 04:27:54 +08:00
Andy Lok
f5e0853264 Refactor Utils.Path 2020-12-07 04:16:28 +08:00
Andy Lok
8eea90527a Refactor System.Path 2020-12-07 04:10:15 +08:00
Fabián Heredia Montiel
57a8ef4609
Implement Futures as a Parallelism Primitive (#753) 
Co-authored-by: Christian Rasmussen <christian.rasmussen@me.com>
 2020-12-04 10:58:26 +00:00
G. Allais
5e799563fa
[ contrib ] adding Data.Container (#781) 2020-11-27 15:29:19 +00:00
Alex Humphreys
71a638ef28 Add extra parsers 
This also changes the return type of `char` and `string`. They
previously returned `()`, they now return `Char` and `String`
repectively.

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-11-27 11:54:12 +00:00
Guillaume ALLAIS
a9ff13c663 [ new ] proof that evaluation is Domain-independent 2020-10-29 23:05:41 +00:00
Alex Gryzlov
f79b86ae41
contrib.Data.String.Parser updates (#713) 2020-10-24 12:33:15 +01: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
Guillaume ALLAIS
14d0141ca2 [ fix #735 ] Make sure type constructors are fully applied 2020-10-16 14:44:11 +01:00
Guillaume ALLAIS
482527063c [ new ] Variant with a runtime irrelevant Domain 
Rather than translating the constraints to a Dybjer-Setzer IR code
we can produce an ad-hoc definition of a `Domain` that we will be
able to make runtime irrelevant.

This means that compiled code will never need to construct a proof
that a value is in the domain of the function: it will simply run
the function!
 2020-10-15 17:03:32 +01:00
Guillaume ALLAIS
864be2c9dc [ contrib ] add McBride's General monad 2020-10-15 17:03:32 +01:00
Matus Tejiscak
f64163de1f Merge branch 'unscheme' into master 2020-10-11 08:20:01 +02:00
Ohad Kammar
ef730c7eb1
preorder reasoning: introduce a Step datatype (#734) 
Refactor the DIY equational reasoning library to be a bit more like
the generic pre-order reasoning library:

Change the `...` notation into a constructor for a new `Step` datatype.

This seems to help idris disambiguate between the two kinds of
reasoning when they're used in the same file (e.g., frex).

Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
 2020-10-07 17:44:18 +01: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
Ruslan Feizerahmanov
2e627ad16e
Remove invalid implicit in PreorderReasoning (#727) 2020-10-03 14:53:14 +01:00
Ohad Kammar
c02481fb55
[contrib] Add a Reflects datatype (#722) 
* [contrib] Add a `Reflects` datatype

as discussed in PR #695
 2020-10-02 17:41:36 +01: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
G. Allais
3df1f9c476
[ fix #63 ] interleaving let binders and local declarations (#691) 2020-09-28 13:15:22 +01:00
G. Allais
d105dd11a7
[ breaking ] remove List1 related ambiguities (#690) 2020-09-22 15:07:40 +01:00
Christian Rasmussen
9add729ca3 Add Data.String.Iterator implementation for JavaScript 2020-09-20 17:44:19 +02:00
Matus Tejiscak
0a203f8f52 Add a warning comment. 2020-09-20 17:42:50 +02:00
Matus Tejiscak
b58cc433c8 Index StringIterator with the String it refers to. 2020-09-20 10:36:04 +02:00
Matus Tejiscak
d26a9c55bf Tune Data.String.Iterator. 2020-09-20 10:02:18 +02:00
Matus Tejiscak
f73fa55075 Unpack strings into a lazy list. 2020-09-19 22:48:45 +02:00
Matus Tejiscak
e36c211cc0 Add a missing covering annotation. 2020-09-19 21:57:54 +02:00
Matus Tejiscak
74f592053e Make StringIterator abstract. 2020-09-19 21:54:34 +02:00
Matus Tejiscak
7b2d1190a1 Make the comments more explicit. 2020-09-19 15:22:29 +02:00
Matus Tejiscak
5360adcc23 String-related stdlib tweaks. 2020-09-19 14:22:54 +02:00
Ohad Kammar
2ae330785b
[contrib] Add misc libraries to contrib (#667) 
* [contrib] Add misc libraries to contrib

Expose some `private` function in libs/base that I needed, and seem like
their visibility was forgotten

I'd appreciate a code review, especially to tell me I'm
re-implementing something that's already elsewhere in the library

Mostly extending existing functionality:
* `Data/Void.idr`: add some utility functions for manipulating absurdity.
* `Decidable/Decidable/Extra.idr`: add support for double negation elimination in decidable relations
* `Data/Fun/Extra.idr`:
  + add `application` (total and partil) for n-ary functions
  + add (slightly) dependent versions of these operations
* `Decidable/Order/Strict.idr`: a strict preorder is what you get when
  you remove the diagonal from a pre-order. For example, `<` is the
  associated preorder for `<=` over `Nat`.
  Analogous to `Decidable.Order`. The proof search mechanism struggled
  a bit, so I had to hack it --- sorry.

Eventually we should move `Data.Fun.Extra.Pointwise` to `Data.Vect.Quantifiers` in base
but we don't have any interesting uses for it at the moment so it's not
urgent.

Co-authored by @gallais
 2020-09-14 16:22:46 +01:00
Shay Lewis
53c2bf5885 make constructor injectivity proofs use arguments at 0 multiplicity 2020-09-09 19:57:12 +01:00
foss-mc
d56b090c4c Add missing Data.Stream.Extra module to contrib.ipkg 
I forgot to add it
 2020-08-28 14:26:11 +01:00
foss-mc
4b7dc38e62 Add Data.Stream.Extra.startWith 2020-08-28 13:16:31 +01:00
Alex Gryzlov
969f5443a9 additional refactor of Data.String.Parser 2020-08-27 15:27:52 +01:00
Thomas Dziedzic
a7ff5aa71f
implement HVect (#563) 2020-08-26 15:48:19 +01:00
russoul
3a9b1ac656 Add supporting code 2020-08-25 14:30:57 +03:00
russoul
594105d5ac Eliminate schemeCall from the library 2020-08-24 19:38:29 +03:00
Alex Gryzlov
ef5299733a
refactor Data.String.Parser (#579) 2020-08-22 08:13:34 +01:00
Ohad Kammar
310b7a007c Move cong2 from contrib to Prelude.Basics 2020-08-20 07:53:45 +01:00
Ohad Kammar
080fbab20d Insert linearity annotations for cong2 
following review by @gallais
 2020-08-20 07:53:45 +01:00
Kamil Shakirov
8544e80076 Use the same naming convention for foreign primitives 2020-08-19 14:05:28 +01:00
Giuseppe Lomurno
df4f990b3c PTerm and error intial prettyprinting 2020-08-18 19:25:36 +01:00
Niklas Larsson
93ecb72012
Merge pull request #526 from alexhumphreys/feat/buildExpressionParser 
Add BuildExpressionParser to contrib
 2020-08-18 14:01:20 +02:00
Sventimir
01e6263a87 Introduce the notion of PropValidator so that value under validation gets ignored more explicitly in those. 2020-08-18 13:56:21 +02:00
Ohad Kammar
10b8698843 Remove forgotten linearity annotation on cong2 2020-08-16 08:20:31 +01:00
Ohad Kammar
d82a3e0e42 contrib: Add a 2-holed congruence function 
For lack of a better place, I've put it in `Syntax.PreorderReasoning`

These equations are natural in equational reasoning, but less so when
rewriting, so that's why it's there
 2020-08-16 08:20:31 +01:00
Sventimir
ba197a230e Port Control.Arrow from Idris. 2020-08-15 16:42:00 +02:00
Sventimir
886c70c196 Add Data.Either module ported from Idris. 2020-08-15 14:28:08 +02:00
Sventimir
c6d8ef30ed Add Control.Category module ported from Idris. 2020-08-15 14:27:27 +02:00
Sventimir
021a5a6154 Update the docs. 2020-08-13 18:28:39 +02:00
Sventimir
ffbfecb376 Fix broken name of the module. 2020-08-13 17:52:43 +02:00
Sventimir
daad29deb6 Remove redundant constructor to the ValidatorT type. 2020-08-13 17:49:22 +02:00
Sventimir
b0bcfe9180 Export EitherT monad transformer as well. 2020-08-12 18:37:00 +02:00
Sventimir
41444e5050 Export publicly the Validator type alias. 2020-08-12 17:37:48 +02:00
Sventimir
67bab6b088 Add Control.Validation module to contrib package. 2020-08-12 17:33:25 +02:00
Sventimir
208fb6fe04 Turn Validator into a proper monad transformer. 2020-08-11 20:52:13 +02:00
Sventimir
6389aa4099 Add initial validation framework. 2020-08-11 18:27:06 +02:00
Alex Humphreys
f47d9cfef2 Add integer paser and extra test 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Alex Humphreys
f020fd29e8 Use overloaded Fin literals 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Ohad Kammar
7f960ed938 Remove bindning to y as no longer necessary 2020-08-09 10:18:34 +01:00
Ohad Kammar
ff76dee6c7 Try a fix for the preorder reasoning error 
Correct the dependency in `FastDerivation` to use the RHS in `step`
Try to avoid shadowing `y` in the LHS of `Calc`
 2020-08-09 10:18:34 +01:00
Alex Humphreys
d4cbb8a620 Move natural and digit combinators 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-07 19:20:32 +02:00
Alex Humphreys
40427bd527 Move combinators to Data.String.Parser 2020-08-06 13:16:47 +02:00
Alex Humphreys
97b41d1ad9 Rename BuildExpressionParser to Parser.Expression 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:42:38 +02:00
Alex Humphreys
22915d23ca Remove LO function 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:27:42 +02:00
Alex Humphreys
eca083cdcc Add License comment to BuildExpressionParser 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00
Alex Humphreys
29e49a74c5 Add BuildExpressionParser to contrib 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00
Giuseppe Lomurno
723457fd6c Remove public export 2020-08-05 13:42:04 +02:00
Giuseppe Lomurno
c28133b7d9 Renamed IsString to FromString 
- Renaming of the string overload interface
- Added test cases for both string and integer literals overload
 2020-08-05 02:33:05 +02:00
Giuseppe Lomurno
b7ba5e88eb Overloaded strings interface 
As for integer literals, adds an interface for overloaded string
literals, and the implementation for the prettyprinter library in
contrib.
 2020-08-05 02:00:05 +02: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
Giuseppe Lomurno
39f23ffd9b Prec version of pretty interface 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
ab1f383912 Laziness annotations for performance 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
62524e8462 Tree representation for prettyprinting 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
3d51af46c2 Namespace change 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
eb659ba907 Added prettyprinting library 2020-07-24 15:19:17 +01:00
Nick Drozd
a2bdf8e6d7 Add some algebra implementations 2020-07-17 08:25:20 -05:00
Mark Barbone
acda3b44a9
Make Text.Parser.between lazy (#385) 2020-07-14 14:33:22 +01:00
G. Allais
0908e76515
[ fix #346 ] Pull List.length into prelude (#450) 2020-07-14 12:15:57 +01:00
Nick Drozd
6519b5608d Further simplify List 2020-07-12 21:00:33 -05:00
Nick Drozd
7d1ee9dd08 Simplify Equality 2020-07-07 10:48:23 +01:00
Michael Birch
5c9339bde8
Merge sort implementation for Vect (#417) 2020-07-07 10:25:42 +01:00
Niklas Larsson
52c6db09d1 Add <?> for replacing error messages 2020-07-06 14:13:56 +02:00
Niklas Larsson
60a067fab1 Remove dumpState 2020-07-06 13:57:13 +02:00
Niklas Larsson
5060eaafaf Make things public export to work with bootstrap 2020-07-05 21:51:12 +02:00
Niklas Larsson
af83c9303b Add test and documentation 2020-07-05 21:51:12 +02:00
Niklas Larsson
d779c85df4 Add optional 2020-07-05 21:51:11 +02:00
Niklas Larsson
0e51124a43 Add option 2020-07-05 21:51:11 +02:00
Niklas Larsson
bba15974a5 Add takeWhile 
add substring and length primitives to Data.Strings
 2020-07-05 21:51:11 +02:00
Niklas Larsson
39535bf11a Add lifting 2020-07-05 21:51:11 +02:00
Niklas Larsson
d97789190d Add bounds checking 2020-07-05 21:51:11 +02:00
Niklas Larsson
f290c6c3ce Start on a simple string parser 2020-07-05 21:51:11 +02:00
Edwin Brady
a9478875b3
Merge pull request #392 from buzden/append-properties 
Injectivity and similar properties were added for lists'a append
 2020-07-05 14:08:07 +01:00
Edwin Brady
9d1bb82c48
Merge pull request #242 from nickdrozd/algebra 
Add Algebra interfaces and laws
 2020-07-05 00:04:13 +01:00
Denis Buzdalov
77f1d69acb Injectivity and similar properties were added for lists'a append. 2020-06-30 17:00:47 +03:00
Denis Buzdalov
df60e07962 List's snoc injectivity property was renamed approporiately. 2020-06-30 13:18:42 +01: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