Skip to content

Commit 3dbc68e

Browse files
datokratdatokrat
committed
pure
1 parent ad41875 commit 3dbc68e

File tree

3 files changed

+181
-0
lines changed

3 files changed

+181
-0
lines changed

‎src/Init/Data/Iterators/Consumers/Loop.lean‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,59 @@ def Iter.all {α β : Type w}
203203
(p : β → Bool) (it : Iter (α := α) β) : Bool :=
204204
(it.allM (fun x => pure (f := Id) (p x))).run
205205

206+
@[inline]
207+
def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
208+
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
209+
m (Option γ) :=
210+
ForIn.forIn it none (fun x _ => do
211+
match ← f x with
212+
| none => return .yield none
213+
| some fx => return .done (some fx))
214+
215+
@[inline]
216+
def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
217+
[Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
218+
(f : β → m (Option γ)) :
219+
m (Option γ) :=
220+
ForIn.forIn it none (fun x _ => do
221+
match ← f x with
222+
| none => return .yield none
223+
| some fx => return .done (some fx))
224+
225+
@[inline]
226+
def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
227+
[IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
228+
Option γ :=
229+
Id.run (it.findSomeM? (pure <| f ·))
230+
231+
@[inline]
232+
def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
233+
[IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
234+
Option γ :=
235+
Id.run (it.findSomeM? (pure <| f ·))
236+
237+
@[inline]
238+
def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
239+
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
240+
m (Option β) :=
241+
it.findSomeM? (fun x => return if (← f x).down then some x else none)
242+
243+
@[inline]
244+
def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
245+
[IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
246+
m (Option β) :=
247+
it.findSomeM? (fun x => return if (← f x).down then some x else none)
248+
249+
@[inline]
250+
def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
251+
[Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
252+
Id.run (it.findM? (pure <| .up <| f ·))
253+
254+
@[inline]
255+
def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
256+
(it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
257+
Id.run (it.findM? (pure <| .up <| f ·))
258+
206259
@[always_inline, inline, expose, inherit_doc IterM.size]
207260
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
208261
(it : Iter (α := α) β) : Nat :=

‎src/Init/Data/Iterators/Consumers/Monadic/Loop.lean‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -588,24 +588,51 @@ def IterM.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Ite
588588
| none => return .yield none
589589
| some fx => return .done (some fx))
590590

591+
@[inline]
592+
def IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
593+
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (Option γ)) :
594+
m (Option γ) :=
595+
ForIn.forIn it none (fun x _ => do
596+
match ← f x with
597+
| none => return .yield none
598+
| some fx => return .done (some fx))
599+
591600
@[inline]
592601
def IterM.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
593602
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Option γ) :
594603
m (Option γ) :=
595604
it.findSomeM? (pure <| f ·)
596605

606+
@[inline]
607+
def IterM.Partial.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
608+
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
609+
m (Option γ) :=
610+
it.findSomeM? (pure <| f ·)
611+
597612
@[inline]
598613
def IterM.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
599614
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → m (ULift Bool)) :
600615
m (Option β) :=
601616
it.findSomeM? (fun x => return if (← f x).down then some x else none)
602617

618+
@[inline]
619+
def IterM.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
620+
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (ULift Bool)) :
621+
m (Option β) :=
622+
it.findSomeM? (fun x => return if (← f x).down then some x else none)
623+
603624
@[inline]
604625
def IterM.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
605626
[IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Bool) :
606627
m (Option β) :=
607628
it.findM? (pure <| .up <| f ·)
608629

630+
@[inline]
631+
def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
632+
[IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Bool) :
633+
m (Option β) :=
634+
it.findM? (pure <| .up <| f ·)
635+
609636
section Size
610637

611638
/--

‎src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -729,4 +729,105 @@ theorem Iter.all_eq_not_any_not {α β : Type w} [Iterator α Id β]
729729
· simp [ihs ‹_›]
730730
· simp
731731

732+
theorem Iter.findSomeM?_eq_match_step {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
733+
[Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m]
734+
{it : Iter (α := α) β} {f : β → m (Option γ)} :
735+
it.findSomeM? f = (do
736+
match it.step.val with
737+
| .yield it' out =>
738+
match ← f out with
739+
| none => it'.findSomeM? f
740+
| some fx => return (some fx)
741+
| .skip it' => it'.findSomeM? f
742+
| .done => return none) := by
743+
rw [findSomeM?, forIn_eq_match_step]
744+
cases it.step using PlausibleIterStep.casesOn
745+
· simp only [bind_assoc]
746+
apply bind_congr; intro fx
747+
split <;> simp [findSomeM?]
748+
· simp [findSomeM?]
749+
· simp
750+
751+
theorem Iter.findSome?_eq_findSomeM? {α β : Type w} {γ : Type x}
752+
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
753+
{it : Iter (α := α) β} {f : β → Option γ} :
754+
it.findSome? f = Id.run (it.findSomeM? (pure <| f ·)) :=
755+
(rfl)
756+
757+
theorem Iter.findSome?_eq_findSome?_toIterM {α β γ : Type w}
758+
[Iterator α Id β] [IteratorLoop α Id Id.{w}] [Finite α Id]
759+
{it : Iter (α := α) β} {f : β → Option γ} :
760+
it.findSome? f = (it.toIterM.findSome? f).run :=
761+
(rfl)
762+
763+
theorem Iter.findSome?_eq_match_step {α β : Type w} {γ : Type x}
764+
[Iterator α Id β] [IteratorLoop α Id Id] [LawfulMonad Id] [Finite α Id]
765+
[LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} {f : β → Option γ} :
766+
it.findSome? f = (match it.step.val with
767+
| .yield it' out =>
768+
match f out with
769+
| none => it'.findSome? f
770+
| some fx => some fx
771+
| .skip it' => it'.findSome? f
772+
| .done => none) := by
773+
rw [findSome?_eq_findSomeM?, findSomeM?_eq_match_step]
774+
split
775+
· simp only [pure_bind, findSome?_eq_findSomeM?]
776+
split <;> simp
777+
· simp [findSome?_eq_findSomeM?]
778+
· simp
779+
780+
theorem Iter.findM?_eq_findSomeM? {α β : Type w} {m : Type w → Type w'} [Monad m]
781+
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
782+
{it : Iter (α := α) β} {f : β → m (ULift Bool)} :
783+
it.findM? f = it.findSomeM? (fun x => return if (← f x).down then some x else none) :=
784+
(rfl)
785+
786+
theorem Iter.findM?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m]
787+
[Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m]
788+
{it : Iter (α := α) β} {f : β → m (ULift Bool)} :
789+
it.findM? f = (do
790+
match it.step.val with
791+
| .yield it' out =>
792+
if (← f out).down then return (some out) else it'.findM? f
793+
| .skip it' => it'.findM? f
794+
| .done => return none) := by
795+
rw [findM?_eq_findSomeM?, findSomeM?_eq_match_step]
796+
split
797+
· simp only [bind_assoc]
798+
apply bind_congr; intro fx
799+
split <;> simp [findM?_eq_findSomeM?]
800+
· simp [findM?_eq_findSomeM?]
801+
· simp
802+
803+
theorem Iter.find?_eq_findM? {α β : Type w} [Iterator α Id β]
804+
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β → Bool} :
805+
it.find? f = Id.run (it.findM? (pure <| .up <| f ·)) :=
806+
(rfl)
807+
808+
theorem Iter.find?_eq_find?_toIterM {α β : Type w} [Iterator α Id β]
809+
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β → Bool} :
810+
it.find? f = (it.toIterM.find? f).run :=
811+
(rfl)
812+
813+
theorem Iter.find?_eq_findSome? {α β : Type w} [Iterator α Id β]
814+
[IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β → Bool} :
815+
it.find? f = it.findSome? (fun x => if f x then some x else none) := by
816+
simp [find?_eq_findM?, findSome?_eq_findSomeM?, findM?_eq_findSomeM?]
817+
818+
theorem Iter.find?_eq_match_step {α β : Type w}
819+
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
820+
{it : Iter (α := α) β} {f : β → Bool} :
821+
it.find? f = (match it.step.val with
822+
| .yield it' out =>
823+
if f out then some out else it'.find? f
824+
| .skip it' => it'.find? f
825+
| .done => none) := by
826+
rw [find?_eq_findM?, findM?_eq_match_step]
827+
split
828+
· simp only [pure_bind]
829+
split <;> simp [find?_eq_findM?]
830+
· simp [find?_eq_findM?]
831+
· simp
832+
732833
end Std.Iterators

0 commit comments

Comments
 (0)