Monadic zip
combinator #
This file provides an iterator combinator IterM.zip
that combines two iterators into an iterator
of pairs.
Lifts an ordering relation to Option
, such that none
is the greatest element.
It can be understood as adding a distinguished greatest element, represented by none
, to both α
and β
.
Caution: Given LT α
, Option.SomeLtNone.lt LT.lt
differs from the LT (Option α)
instance,
which is implemented by Option.lt Lt.lt
.
Examples:
Option.lt (fun n k : Nat => n < k) none none = False
Option.lt (fun n k : Nat => n < k) none (some 3) = False
Option.lt (fun n k : Nat => n < k) (some 3) none = True
Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True
Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False
Equations
Instances For
it.PlausibleStep step
is the proposition that step
is a possible next step from the
zip
iterator it
. This is mostly internally relevant, except if one needs to manually
prove termination (Finite
or Productive
instances, for example) of a zip
iterator.
- yieldLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) {it' : IterM m β₁} {out : β₁} (hp : it.internalState.left.IsPlausibleStep (IterStep.yield it' out)) : PlausibleStep it (IterStep.skip { internalState := { left := it', memoizedLeft := some ⟨out, ⋯⟩, right := it.internalState.right } })
- skipLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) {it' : IterM m β₁} (hp : it.internalState.left.IsPlausibleStep (IterStep.skip it')) : PlausibleStep it (IterStep.skip { internalState := { left := it', memoizedLeft := none, right := it.internalState.right } })
- doneLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) (hp : it.internalState.left.IsPlausibleStep IterStep.done) : PlausibleStep it IterStep.done
- yieldRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) {it₂' : IterM m β₂} {out₂ : β₂} (hp : it.internalState.right.IsPlausibleStep (IterStep.yield it₂' out₂)) : PlausibleStep it (IterStep.yield { internalState := { left := it.internalState.left, memoizedLeft := none, right := it₂' } } (out₁.val, out₂))
- skipRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) {it₂' : IterM m β₂} (hp : it.internalState.right.IsPlausibleStep (IterStep.skip it₂')) : PlausibleStep it (IterStep.skip { internalState := { left := it.internalState.left, memoizedLeft := some out₁, right := it₂' } })
- doneRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) (hp : it.internalState.right.IsPlausibleStep IterStep.done) : PlausibleStep it IterStep.done
Instances For
Given two iterators left
and right
, left.zip right
is an iterator that yields pairs of
outputs of left
and right
. When one of them terminates,
the zip
iterator will also terminate.
Marble diagram:
left --a ---b --c
right --x --y --⊥
left.zip right -----(a, x)------(b, y)-----⊥
Termination properties:
Finite
instance: only if eitherleft
orright
is finite and the other is productiveProductive
instance: only ifleft
andright
are productive
There are situations where left.zip right
is finite (or productive) but none of the instances
above applies. For example, if the computation happens in an Except
monad and left
immediately
fails when calling step
, then left.zip right
will also do so. In such a case, the Finite
(or Productive
) instance needs to be proved manually.
Performance:
This combinator incurs an additional O(1) cost with each step taken by left
or right
.
Right now, the compiler does not unbox the internal state, leading to worse performance than possible.
Equations
Instances For
Equations
- Std.Iterators.Zip.instFinitenessRelation₁ = { rel := Std.Iterators.Zip.Rel₁ m, wf := ⋯, subrelation := ⋯ }
Instances For
Equations
- Std.Iterators.Zip.instFinitenessRelation₂ = { rel := Std.Iterators.Zip.Rel₂ m, wf := ⋯, subrelation := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Std.Iterators.Zip.instProductivenessRelation = { rel := Std.Iterators.Zip.Rel₃ m, wf := ⋯, subrelation := ⋯ }