New optimization pass for eliminating unreachable branches that occur
very often when using `ExceptT` and `EState`.
The current commit implements an abstract interpreter for computing
an approximation of the kinds of values returned by a function.
TODO:
- Implement `FnBody.jmp`.
- Implement `interpDecl`
- Remove unreachable branches in `FnBody.case`
This change allows the monadic traversal operations on arrays to use monads that
are defined to raise universe levels. This happens, for example, when defining
monads using certain continuation-passing idioms.
In Lean 4, we will support the more general
`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`
This commit also removes Array.hmap.
Motivation: I wanted to use Array.hmap as an example in the paper, but
I found it would be too distracting to explain why we had `Array.hmap`
and `Array.map`.
cc @kha
@kha I added `qsort` for sorting environment extension entries, but I am
wondering if we could use it as a benchmark in our paper. It is a pure implementation; it is
fast; it implements the real quick sort algorithm with in-place updates if the
input array is not shared. If the array is shared it performs
a single copy and then switches to in-place updates.
@kha Trying again :)
I started using the prefix `f` for the `Fin` version (e.g., `fswap` and
`fswapAt`). So, it seemed natural to use the prefix `f` for the `Fin`
versions of `get` and `set`.
BTW, is it too crazy to use `a[i]` (without spaces) as notation for
`a.get i`? The constraint is to make sure `f a [i]` is not ambiguous.
That is, `f a[i]` is `f (a.get i)` and `f a [i]` is `f a (i::nil)`.
This is doable with the new parser.
Then, we could have `a[i]` as notation for `a.fget i` if `i` is a `Fin`,
and `a.get i` if `i` is `Nat`.
Similarly, `a[i := v]` would be notation for `a.fset i v` if `i` is
`Fin`, and `a.set i` if `i` is `Nat`.
It would also be awesome to have
```
let a[i] := v in
e
```
as notation for
```
let a := a[i := v] in
```
