This PR provides the iterator combinator `filterMap` in a pure and
monadic version and specializations `map` and `filter`. This new
combinator allows to apply a function to the emitted values of a stream
while filtering out certain elements.
`map` should have an optimized `IteratorCollect` implementation but it
turns out that this is not possible without a major refactor of
`IteratorCollect`: `toArrayMapped` requires a proof that the iterator is
finite. If `it.mapM f` is `Finite` but `it` is not, then such a proof
does not exist. `IteratorCollect` needs to take a proof that the loop
will terminate for the given monadic function `f` instead. This will not
be done in this PR.
This PR provides the `take` iterator combinator that transforms any
iterator into an iterator that stops after a given number of steps. The
change contains the implementation and lemmas.
`take` has a special implementation of `IteratorLoop` that relies on a
potentially more efficient `forIn` implementation of the inner iterator.
The mysterious `@[specialize]` on a test has been removed because it is
not necessary anymore according to a manual inspection of the IR. Either
I erroneously concluded from experiments that it was necessary of
something has changed in the meantime that makes it unnecessary.
This PR reworks the `simp` set around the `Id` monad, to not elide or
unfold `pure` and `Id.run`
In particular, it stops encoding the "defeq abuse" of `Id X = X` in the
statements of theorems, instead using `Id.run` and `pure` to pass back
and forth between these two spellings. Often when writing these with
`pure`, they generalize to other lawful monads; though such changes were
split off to other PRs.
This fixes the problem with the current simp set where `Id.run (pure x)`
is simplified to `Id.run x`, instead of the desirable `x`.
This is particularly bad because the` x` is sometimes inferred with type
`Id X` instead of `X`, which prevents other `simp` lemmas about `X` from
firing.
Making `Id` reducible instead is not an option, as then the `Monad`
instances would have nothing to key on.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR provides simple lemmas about `toArray`, `toList` and `toListRev`
for the iterator library.
It also changes the definition of `Iter` and `IterM` so that they aren't
equal anymore and in particular not definitionally equal. While it was
very convenient to have them be definitionally equal when working with
dependent code, it was also confusing and annoying that one would
sometimes end up with something like `it.toList = IterM.toList it`,
where `it : Iter β`.
This PR introduces a very minimal version of the new iterator library.
It comes with list iterators and various consumers, namely `toArray`,
`toList`, `toListRev`, `ForIn`, `fold`, `foldM` and `drain`. All
consumers also come in a partial variant that can be used without any
proofs. This limited version of the iterator library generates decent
code, even with the old code generator.
