idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-08 08:52:22 +03:00
Code Issues Projects Releases Wiki Activity
1,105 Commits 6 Branches 9 Tags 120 MiB
a6d767f8fa
Commit Graph

302 Commits

Author SHA1 Message Date
0xd34df00d
7dbafae052 Port Idris 1's Data.Vect.Quantifiers 2020-08-31 12:34:13 +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
russoul
5d156167d3 Add dup 2020-08-27 18:30:31 +01:00
Alex Gryzlov
969f5443a9 additional refactor of Data.String.Parser 2020-08-27 15:27:52 +01:00
Guillaume ALLAIS
1d4c84171d [ refactor ] suggested during SPLV 
Main change
===========

The main change is to the type of function dealing with an untouched
segment of the local scope. e.g.

```
weak : {outer, vars : _} -> (ns : List Name) ->
       tm (outer ++ inner) -> tm (outer ++ ns ++ inner)
```

Instead we now write

```
weak : SizeOf ns -> tm (outer ++ inner) -> tm (outer ++ ns ++ inner)
```

meaning that we do not need the values of `outer`, `inner` and `ns`
at runtime. Instead we only demand a `SizeOf ns` which is a `Nat`
together with an (erased) proof that `ns` is of that length.

Other modifications
===================

Quadratic behaviour
-------------------

A side effect of this refactor is the removal of two sources of
quadratic behaviour. They typically arise in a situation where
work is done on a scope of the form

```
outer ++ done ++ ns ++ inner
```

When `ns` is non-empty, some work is performed and then the variable
is moved to the pile of things we are `done` with. This leads to
recursive calls of the form `f done` -> `f (done ++ [v])` leading
to a cost quadratic in the size of `ns`.

Now that we only care about `SizeOf done`, the recursive call is
(once all the runtime irrelevant content is erased) for the form
`f n` -> `f (S n)`!

More runtime irrelevance
------------------------

In some places we used to rely on a list of names `vars` being
available. However once we only care about the length of `vars`,
the fact it is not available is not a limitation.

For instance a `SizeOf vars` can be reconstructed from an environment
assigning values to `vars` even if `vars` is irrelevant. Indeed the
size of the environment is the same as that of `vars`.
 2020-08-27 10:14:55 +01:00
Guillaume ALLAIS
d9c0e5938e [ fix ] succInjective does not use its arguments 2020-08-27 10:14:55 +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
50ac934747 Merge branch 'master' of https://github.com/idris-lang/Idris2 into master 2020-08-25 13:57:26 +03:00
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
Alex Gryzlov
ef5299733a
refactor Data.String.Parser (#579) 2020-08-22 08:13:34 +01: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
karroffel
7d046652d8
add support for more casts from and to BitsN types (#548) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-08-20 15:01:09 +01:00
Thomas Dziedzic
5d1b937035
add prim__getNullAnyPtr and prim__castPtr (#525) 2020-08-20 11:52:51 +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
Arnaud Bailly
8ecf664ff6
Port Decidable.Order from Idris1 (#543) 2020-08-18 22:26:56 +01:00
Giuseppe Lomurno
df4f990b3c PTerm and error intial prettyprinting 2020-08-18 19:25:36 +01:00
Niklas Larsson
76ee7a3b34
Merge pull request #351 from petithug/fixity-precedence-master 
Restore Bool operators precedence
 2020-08-18 14:08:20 +02:00
Niklas Larsson
84ae9d7c6e
Merge pull request #523 from mb64/hasio-statet 
Implement HasIO for StateT
 2020-08-18 14:02:02 +02:00
Niklas Larsson
93ecb72012
Merge pull request #526 from alexhumphreys/feat/buildExpressionParser 
Add BuildExpressionParser to contrib
 2020-08-18 14:01:20 +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
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
Thomas Dziedzic
a1739a69a0
Update app docs (#537) 2020-08-10 10:05:23 +01: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
russoul
d387c76e9b update stdio docs 2020-08-08 12:49:33 +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
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