Definition of iterators #
This module defines iterators and what it means for an iterator to be finite and productive.
An iterator that sequentially emits values of type β
in the monad m
. It may be finite
or infinite.
See the root module Std.Data.Iterators
for a more comprehensive overview over the iterator
framework.
See Std.Data.Iterators.Producers
for ways to iterate over common data structures.
By convention, the monadic iterator associated with an object can be obtained via dot notation.
For example, List.iterM IO
creates an iterator over a list in the monad IO
.
See Std.Data.Iterators.Consumers
for ways to use an iterator. For example, it.toList
will
convert a provably finite iterator it
into a list and it.allowNontermination.toList
will
do so even if finiteness cannot be proved. It is also always possible to manually iterate using
it.step
, relying on the termination measures it.finitelyManySteps
and it.finitelyManySkips
.
See Iter
for a more convenient interface in case that no monadic effects are needed (m = Id
).
Internally, IterM m β
wraps an element of type α
containing state information.
The type α
determines the implementation of the iterator using a typeclass mechanism.
The concrete typeclass implementing the iterator is Iterator α m β
.
When using combinators, α
can become very complicated. It is an implicit parameter
of α
so that the pretty printer will not print this large type by default. If a declaration
returns an iterator, the following will not work:
def x : IterM IO Nat := [1, 2, 3].iterM IO
Instead the declaration type needs to be completely omitted:
def x := [1, 2, 3].iterM IO
-- if you want to ensure that `x` is an iterator in `IO` emitting `Nat`
def x := ([1, 2, 3].iterM IO : IterM IO Nat)
- internalState : α
Internal implementation detail of the iterator.
Instances For
An iterator that sequentially emits values of type β
. It may be finite
or infinite.
See the root module Std.Data.Iterators
for a more comprehensive overview over the iterator
framework.
See Std.Data.Iterators.Producers
for ways to iterate over common data structures.
By convention, the monadic iterator associated with an object can be obtained via dot notation.
For example, List.iterM IO
creates an iterator over a list in the monad IO
.
See Std.Data.Iterators.Consumers
for ways to use an iterator. For example, it.toList
will
convert a provably finite iterator it
into a list and it.allowNontermination.toList
will
do so even if finiteness cannot be proved. It is also always possible to manually iterate using
it.step
, relying on the termination measures it.finitelyManySteps
and it.finitelyManySkips
.
See IterM
for iterators that operate in a monad.
Internally, Iter β
wraps an element of type α
containing state information.
The type α
determines the implementation of the iterator using a typeclass mechanism.
The concrete typeclass implementing the iterator is Iterator α m β
.
When using combinators, α
can become very complicated. It is an implicit parameter
of α
so that the pretty printer will not print this large type by default. If a declaration
returns an iterator, the following will not work:
def x : Iter Nat := [1, 2, 3].iter
Instead the declaration type needs to be completely omitted:
def x := [1, 2, 3].iter
-- if you want to ensure that `x` is an iterator emitting `Nat`
def x := ([1, 2, 3].iter : Iter Nat)
- internalState : α
Internal implementation detail of the iterator.
Instances For
IterStep α β
represents a step taken by an iterator (Iter β
or IterM m β
).
- yield
{α : Sort u_1}
{β : Sort u_2}
(it : α)
(out : β)
: IterStep α β
IterStep.yield it out
describes the situation that an iterator emitsout
and providesit
as the succeeding iterator. - skip
{α : Sort u_1}
{β : Sort u_2}
(it : α)
: IterStep α β
IterStep.skip it
describes the situation that an iterator does not emit anything in this iteration and providesit'
as the succeeding iterator.Allowing
skip
steps is necessary to generate efficient code from a loop over an iterator. - done
{α : Sort u_1}
{β : Sort u_2}
: IterStep α β
IterStep.done
describes the situation that an iterator has finished and will neither emit more values nor cause any monadic effects. In this case, no succeeding iterator is provided.
Instances For
Returns the succeeding iterator stored in an iterator step or none
if the step is .done
and the iterator has finished.
Equations
Instances For
If present, applies f
to the iterator of an IterStep
and replaces the iterator
with the result of the application of f
.
Equations
- Std.Iterators.IterStep.mapIterator f (Std.Iterators.IterStep.yield it out) = Std.Iterators.IterStep.yield (f it) out
- Std.Iterators.IterStep.mapIterator f (Std.Iterators.IterStep.skip it) = Std.Iterators.IterStep.skip (f it)
- Std.Iterators.IterStep.mapIterator f Std.Iterators.IterStep.done = Std.Iterators.IterStep.done
Instances For
A variant of IterStep
that bundles the step together with a proof that it is "plausible".
The plausibility predicate will later be chosen to assert that a state is a plausible successor
of another state. Having this proof bundled up with the step is important for termination proofs.
See IterM.Step
and Iter.Step
for the concrete choice of the plausibility predicate.
Equations
- Std.Iterators.PlausibleIterStep IsPlausibleStep = Subtype IsPlausibleStep
Instances For
Match pattern for the yield
case. See also IterStep.yield
.
Equations
- Std.Iterators.PlausibleIterStep.yield it' out h = ⟨Std.Iterators.IterStep.yield it' out, h⟩
Instances For
Match pattern for the skip
case. See also IterStep.skip
.
Equations
Instances For
Match pattern for the done
case. See also IterStep.done
.
Instances For
A more convenient cases
eliminator for PlausibleIterStep
.
Equations
- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.yield it' out, h⟩ yield skip done = yield it' out h
- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.skip it', h⟩ yield skip done = skip it' h
- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.done, h⟩ yield skip done = done h
Instances For
The typeclass providing the step function of an iterator in Iter (α := α) β
or
IterM (α := α) m β
.
In order to allow intrinsic termination proofs when iterating with the step
function, the
step object is bundled with a proof that it is a "plausible" step for the given current iterator.
- step (it : IterM m β) : m (PlausibleIterStep (IsPlausibleStep it))
Instances
Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
is up to the Iterator
instance but it should be strong enough to allow termination proofs.
Instances For
The type of the step object returned by IterM.step
, containing an IterStep
and a proof that this is a plausible step for the given iterator.
Equations
Instances For
Asserts that a certain output value could plausibly be emitted by the given iterator in its next step.
Equations
- it.IsPlausibleOutput out = ∃ (it' : Std.IterM m β), it.IsPlausibleStep (Std.Iterators.IterStep.yield it' out)
Instances For
Asserts that a certain iterator it'
could plausibly be the directly succeeding iterator of another
given iterator it
.
Equations
- it'.IsPlausibleSuccessorOf it = ∃ (step : Std.Iterators.IterStep (Std.IterM m β) β), step.successor = some it' ∧ it.IsPlausibleStep step
Instances For
Asserts that a certain iterator it'
could plausibly be the directly succeeding iterator of another
given iterator it
while no value is emitted (see IterStep.skip
).
Equations
- it'.IsPlausibleSkipSuccessorOf it = it.IsPlausibleStep (Std.Iterators.IterStep.skip it')
Instances For
Makes a single step with the given iterator it
, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures it.finitelyManySteps
and it.finitelyManySkips
.
Equations
- it.step = Std.Iterators.Iterator.step it
Instances For
Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
is up to the Iterator
instance but it should be strong enough to allow termination proofs.
Equations
Instances For
Converts an Iter.Step
into an IterM.Step
.
Equations
Instances For
Converts an IterM.Step
into an Iter.Step
.
Equations
Instances For
Asserts that a certain output value could plausibly be emitted by the given iterator in its next step.
Equations
- it.IsPlausibleOutput out = it.toIterM.IsPlausibleOutput out
Instances For
Asserts that a certain iterator it'
could plausibly be the directly succeeding iterator of another
given iterator it
.
Equations
- it'.IsPlausibleSuccessorOf it = it'.toIterM.IsPlausibleSuccessorOf it.toIterM
Instances For
Asserts that a certain iterator it'
could plausibly be the directly succeeding iterator of another
given iterator it
while no value is emitted (see IterStep.skip
).
Equations
- it'.IsPlausibleSkipSuccessorOf it = it'.toIterM.IsPlausibleSkipSuccessorOf it.toIterM
Instances For
Makes a single step with the given iterator it
, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures it.finitelyManySteps
and it.finitelyManySkips
.
Instances For
Finite α m
asserts that IterM (α := α) m
terminates after finitely many steps. Technically,
this means that the relation of plausible successors is well-founded.
Given this typeclass, termination proofs for well-founded recursion over an iterator it
can use
it.finitelyManySteps
as a termination measure.
Instances
This type is a wrapper around IterM
so that it becomes a useful termination measure for
recursion over finite iterators. See also IterM.finitelyManySteps
and Iter.finitelyManySteps
.
- it : IterM m β
Instances For
The relation of plausible successors on IterM.TerminationMeasures.Finite
. It is well-founded
if there is a Finite
instance.
Equations
Instances For
Termination measure to be used in well-founded recursive functions recursing over a finite iterator
(see also Finite
).
Equations
- it.finitelyManySteps = { it := it }
Instances For
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with IterM.finitelyManySteps
.
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with IterM.finitelyManySteps
.
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with IterM.finitelyManySteps
.
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with IterM.finitelyManySteps
.
Productive α m
asserts that IterM (α := α) m
terminates or emits a value after finitely many
skips. Technically, this means that the relation of plausible successors during skips is
well-founded.
Given this typeclass, termination proofs for well-founded recursion over an iterator it
can use
it.finitelyManySkips
as a termination measure.
Instances
This type is a wrapper around IterM
so that it becomes a useful termination measure for
recursion over productive iterators. See also IterM.finitelyManySkips
and Iter.finitelyManySkips
.
- it : IterM m β
Instances For
The relation of plausible successors while skipping on IterM.TerminationMeasures.Productive
.
It is well-founded if there is a Productive
instance.
Equations
Instances For
Equations
Termination measure to be used in well-founded recursive functions recursing over a productive
iterator (see also Productive
).
Equations
- it.finitelyManySkips = { it := it }
Instances For
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with IterM.finitelyManySkips
.
Termination measure to be used in well-founded recursive functions recursing over a productive
iterator (see also Productive
).
Equations
Instances For
This theorem is used by a decreasing_trivial
extension. It powers automatic termination proofs
with Iter.finitelyManySkips
.