Skip to content
This repository was archived by the owner on Aug 22, 2025. It is now read-only.

Commit e36a335

Browse files
datokratdatokrat
committed
reorganize modules
1 parent c12633d commit e36a335

File tree

3 files changed

+107
-101
lines changed

3 files changed

+107
-101
lines changed

‎Iterator/Consumers/Access.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Paul Reichert
55
-/
66
prelude
7-
import Iterator.Consumers.Monadic.Access
87
import Iterator.Consumers.Partial
98

109
@[specialize]

‎Iterator/Producers.lean‎

Lines changed: 1 addition & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -4,103 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Paul Reichert
55
-/
66
prelude
7-
import Iterator.Basic
8-
import Iterator.Consumers.Collect
9-
import Iterator.Consumers.Loop
10-
import Iterator.Pure
11-
import Init.Data.Nat.Lemmas
12-
13-
section ListIterator
14-
15-
variable {α : Type w} {m : Type w → Type w'}
16-
17-
structure ListIterator (α : Type w) where
18-
list : List α
19-
20-
/--
21-
Returns a finite iterator for the given list.
22-
The iterator yields the elements of the list in order and then terminates.
23-
-/
24-
@[always_inline, inline]
25-
def List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :
26-
IterM (α := ListIterator α) m α :=
27-
toIter { list := l } m α
28-
29-
@[always_inline, inline]
30-
def List.iter {α : Type w} (l : List α) :
31-
Iter (α := ListIterator α) α :=
32-
((l.iterM Id).toPureIter : Iter α)
33-
34-
instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
35-
plausible_step it
36-
| .yield it' out => it.inner.list = out :: it'.inner.list
37-
| .skip _ => False
38-
| .done => it.inner.list = []
39-
step it := pure (match it with
40-
| ⟨⟨[]⟩⟩ => ⟨.done, rfl⟩
41-
| ⟨⟨x :: xs⟩⟩ => ⟨.yield (toIter ⟨xs⟩ m α) x, rfl⟩)
42-
43-
instance [Pure m] : FinitenessRelation (ListIterator α) m where
44-
rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.inner)
45-
wf := InvImage.wf _ WellFoundedRelation.wf
46-
subrelation {it it'} h := by
47-
simp_wf
48-
obtain ⟨step, h, h'⟩ := h
49-
cases step <;> simp_all [IterStep.successor, IterM.plausible_step, Iterator.plausible_step]
50-
51-
instance {α : Type w} [Monad m] : IteratorToArray (ListIterator α) m :=
52-
.defaultImplementation
53-
54-
instance {α : Type w} [Monad m] : IteratorToArrayPartial (ListIterator α) m :=
55-
.defaultImplementation
56-
57-
instance {α : Type w} [Monad m] [Monad n] : IteratorFor (ListIterator α) m n :=
58-
.defaultImplementation
59-
60-
instance {α : Type w} [Monad m] [Monad n] : IteratorForPartial (ListIterator α) m n :=
61-
.defaultImplementation
62-
63-
end ListIterator
64-
65-
section Unfold
66-
67-
universe u v
68-
69-
variable {α : Type w} {m : Type w → Type w'} {f : α → α}
70-
71-
structure UnfoldIterator (α : Type u) (f : α → α) where
72-
next : α
73-
74-
instance [Pure m] : Iterator (UnfoldIterator α f) m α where
75-
plausible_step it
76-
| .yield it' out => out = it.inner.next ∧ it' = toIter ⟨f it.inner.next⟩ m α
77-
| .skip _ => False
78-
| .done => False
79-
step it := pure <| .yield (toIter ⟨f it.inner.next⟩ m α) it.inner.next (by simp)
80-
81-
/--
82-
Creates an infinite, productive iterator. First it yields `init`.
83-
If the last step yielded `a`, the next will yield `f a`.
84-
-/
85-
@[always_inline, inline]
86-
def IterM.unfold (m : Type w → Type w') [Pure m] {α : Type w} (init : α) (f : α → α) :=
87-
toIter (UnfoldIterator.mk (f := f) init) m α
88-
89-
@[always_inline, inline]
90-
def Iter.unfold {α : Type w} (init : α) (f : α → α) :=
91-
((IterM.unfold Id init f).toPureIter : Iter α)
92-
93-
instance [Pure m] : ProductivenessRelation (UnfoldIterator α f) m where
94-
rel := emptyWf.rel
95-
wf := emptyWf.wf
96-
subrelation {it it'} h := by cases h
97-
98-
instance {α : Type w} {f : α → α} [Monad m] [Monad n] : IteratorFor (UnfoldIterator α f) m n :=
99-
.defaultImplementation
100-
101-
instance {α : Type w} {f : α → α} [Monad m] [Monad n] : IteratorForPartial (UnfoldIterator α f) m n :=
102-
.defaultImplementation
103-
104-
-- We do *not* implement `IteratorToArrayPartial` because there is no change at all that it will terminate.
105-
106-
end Unfold
7+
import Iterator.Producers.Basic

‎Iterator/Producers/Basic.lean‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
prelude
7+
import Iterator.Basic
8+
import Iterator.Consumers.Collect
9+
import Iterator.Consumers.Loop
10+
import Iterator.Pure
11+
import Init.Data.Nat.Lemmas
12+
13+
section ListIterator
14+
15+
variable {α : Type w} {m : Type w → Type w'}
16+
17+
structure ListIterator (α : Type w) where
18+
list : List α
19+
20+
/--
21+
Returns a finite iterator for the given list.
22+
The iterator yields the elements of the list in order and then terminates.
23+
-/
24+
@[always_inline, inline]
25+
def List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :
26+
IterM (α := ListIterator α) m α :=
27+
toIter { list := l } m α
28+
29+
@[always_inline, inline]
30+
def List.iter {α : Type w} (l : List α) :
31+
Iter (α := ListIterator α) α :=
32+
((l.iterM Id).toPureIter : Iter α)
33+
34+
instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
35+
plausible_step it
36+
| .yield it' out => it.inner.list = out :: it'.inner.list
37+
| .skip _ => False
38+
| .done => it.inner.list = []
39+
step it := pure (match it with
40+
| ⟨⟨[]⟩⟩ => ⟨.done, rfl⟩
41+
| ⟨⟨x :: xs⟩⟩ => ⟨.yield (toIter ⟨xs⟩ m α) x, rfl⟩)
42+
43+
instance [Pure m] : FinitenessRelation (ListIterator α) m where
44+
rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.inner)
45+
wf := InvImage.wf _ WellFoundedRelation.wf
46+
subrelation {it it'} h := by
47+
simp_wf
48+
obtain ⟨step, h, h'⟩ := h
49+
cases step <;> simp_all [IterStep.successor, IterM.plausible_step, Iterator.plausible_step]
50+
51+
instance {α : Type w} [Monad m] : IteratorToArray (ListIterator α) m :=
52+
.defaultImplementation
53+
54+
instance {α : Type w} [Monad m] : IteratorToArrayPartial (ListIterator α) m :=
55+
.defaultImplementation
56+
57+
instance {α : Type w} [Monad m] [Monad n] : IteratorFor (ListIterator α) m n :=
58+
.defaultImplementation
59+
60+
instance {α : Type w} [Monad m] [Monad n] : IteratorForPartial (ListIterator α) m n :=
61+
.defaultImplementation
62+
63+
end ListIterator
64+
65+
section Unfold
66+
67+
universe u v
68+
69+
variable {α : Type w} {m : Type w → Type w'} {f : α → α}
70+
71+
structure UnfoldIterator (α : Type u) (f : α → α) where
72+
next : α
73+
74+
instance [Pure m] : Iterator (UnfoldIterator α f) m α where
75+
plausible_step it
76+
| .yield it' out => out = it.inner.next ∧ it' = toIter ⟨f it.inner.next⟩ m α
77+
| .skip _ => False
78+
| .done => False
79+
step it := pure <| .yield (toIter ⟨f it.inner.next⟩ m α) it.inner.next (by simp)
80+
81+
/--
82+
Creates an infinite, productive iterator. First it yields `init`.
83+
If the last step yielded `a`, the next will yield `f a`.
84+
-/
85+
@[always_inline, inline]
86+
def IterM.unfold (m : Type w → Type w') [Pure m] {α : Type w} (init : α) (f : α → α) :=
87+
toIter (UnfoldIterator.mk (f := f) init) m α
88+
89+
@[always_inline, inline]
90+
def Iter.unfold {α : Type w} (init : α) (f : α → α) :=
91+
((IterM.unfold Id init f).toPureIter : Iter α)
92+
93+
instance [Pure m] : ProductivenessRelation (UnfoldIterator α f) m where
94+
rel := emptyWf.rel
95+
wf := emptyWf.wf
96+
subrelation {it it'} h := by cases h
97+
98+
instance {α : Type w} {f : α → α} [Monad m] [Monad n] : IteratorFor (UnfoldIterator α f) m n :=
99+
.defaultImplementation
100+
101+
instance {α : Type w} {f : α → α} [Monad m] [Monad n] : IteratorForPartial (UnfoldIterator α f) m n :=
102+
.defaultImplementation
103+
104+
-- We do *not* implement `IteratorToArrayPartial` because there is no change at all that it will terminate.
105+
106+
end Unfold

0 commit comments

Comments
 (0)