mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-07 08:18:12 +03:00
1d4c84171d
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`.
|
||
|---|---|---|
| .. | ||
| Bool | ||
| Fin | ||
| IOArray | ||
| List | ||
| Nat | ||
| Primitives | ||
| Vect | ||
| Bool.idr | ||
| Buffer.idr | ||
| DPair.idr | ||
| Either.idr | ||
| Fin.idr | ||
| Fuel.idr | ||
| Fun.idr | ||
| IOArray.idr | ||
| IORef.idr | ||
| List1.idr | ||
| List.idr | ||
| Maybe.idr | ||
| Morphisms.idr | ||
| Nat.idr | ||
| Ref.idr | ||
| Rel.idr | ||
| So.idr | ||
| Stream.idr | ||
| Strings.idr | ||
| Vect.idr | ||