2980155f5c
This PR significantly changes the signature of the `ToIterator` type class. The obtained iterators' state is no longer dependently typed and is an `outParam` instead of being bundled inside the class. Among other benefits, `simp` can now rewrite inside of `Slice.toList` and `Slice.toArray`. The downside is that we lose flexibility. For example, the former combinator-based implementation of `Subarray`'s iterators is no longer feasible because the states are dependently typed. Therefore, this PR provides a hand-written iterator for `Subarray`, which does not require a dependently typed state and is faster than the previous one. Converting a family of dependently typed iterators into a simply typed one using a `Sigma`-state iterator generates forbiddingly bad code, so that we do provide such a combinator. This PR adds a benchmark for this problem. |
||
|---|---|---|
| .. | ||
| SPred | ||
| Triple | ||
| WP | ||
| PostCond.lean | ||
| PredTrans.lean | ||
| SPred.lean | ||
| Triple.lean | ||
| WP.lean | ||