1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 21:23:53 +03:00
Commit Graph

15 Commits

Author SHA1 Message Date
Guillaume ALLAIS
2ee06e9db0 [ fix ] Productive cantor for Colist1 2021-10-21 16:01:02 +01:00
Fabián Heredia Montiel
d5167a0108
[ fix ] public export Range functions and implementations ()
Since `[a..b]` uses `takeUntil`/`takeBefore` indirectly those too had to
be changed to `public export` clashing with `Data.Stream` definitions.

A small readability refactor was made with the `compare` function from
`EqOrd`.
2021-06-28 16:52:23 +01:00
Alex Gryzlov
71abc8e33b
Add Path@contrib & small changes () 2021-03-25 16:01:32 +00:00
G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' () 2021-03-01 08:29:43 +00:00
Denis Buzdalov
7a8c12771b
[ base ] A property of interaction between zipWith and index () 2021-03-01 08:29:17 +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
Kamiλ Shakirov
140879f7b9
[ new ] Zippable interface () 2021-01-27 18:23:08 +00:00
Kamiλ Shakirov
3bbf52025a
Add zip*/unzip* for List1 () 2021-01-26 10:39:16 +00:00
Kamil Shakirov
b540313c57 Add unzipWith and unzipWith3 for Stream 2021-01-22 10:41:16 +00:00
Edwin Brady
3621c5d1bd
Merge pull request from edwinb/no-linearity-subtyping
Remove linearity subtyping
2021-01-12 12:33:26 +00:00
stefan-hoeck
c39df89f84 deleted 'head' from Data.Stream 2021-01-11 09:36:13 +00:00
Edwin Brady
5b97cd4499 Fix annotaion in Stream 2020-12-27 20:13:21 +00:00
Denis Buzdalov
60e9cf44b0 Add List, LazyList and Stream unfolds and some LazyList's functions 2020-12-18 22:54:03 +00: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
Edwin Brady
dec7dff622 Add libraries 2020-05-18 14:00:08 +01:00