c79d74d9a1
This PR moves many constants of the iterator API from `Std.Iterators` to the `Std` namespace in order to make them more convenient to use. These constants include, but are not limited to, `Iter`, `IterM` and `IteratorLoop`. This is a breaking change. If something breaks, try adding `open Std` in order to make these constants available again. If some constants in the `Std.Iterators` namespace cannot be found, they can be found directly in `Std` now.
51 lines
2.1 KiB
Text
51 lines
2.1 KiB
Text
/-
|
||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Paul Reichert
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Init.Data.Iterators.Combinators.FilterMap
|
||
public import Init.Data.Iterators.Combinators.Monadic.FlatMap
|
||
|
||
set_option doc.verso true
|
||
|
||
/-!
|
||
# {lit}`flatMap` combinator
|
||
|
||
This file provides the {lit}`flatMap` iterator combinator and variants of it.
|
||
|
||
If {lit}`it` is any iterator, {lit}`it.flatMap f` maps each output of {lit}`it` to an iterator using
|
||
{lit}`f`.
|
||
|
||
{lit}`it.flatMap f` first emits all outputs of the first obtained iterator, then of the second,
|
||
and so on. In other words, {lit}`it` flattens the iterator of iterators obtained by mapping with
|
||
{lit}`f`.
|
||
-/
|
||
|
||
namespace Std
|
||
|
||
@[always_inline, inherit_doc IterM.flatMapAfterM]
|
||
public def Iter.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
|
||
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
|
||
(f : β → m (IterM (α := α₂) m γ)) (it₁ : Iter (α := α) β) (it₂ : Option (IterM (α := α₂) m γ)) :=
|
||
((it₁.mapM pure).flatMapAfterM f it₂ : IterM m γ)
|
||
|
||
@[always_inline, expose, inherit_doc IterM.flatMapM]
|
||
public def Iter.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
|
||
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
|
||
(f : β → m (IterM (α := α₂) m γ)) (it : Iter (α := α) β) :=
|
||
(it.flatMapAfterM f none : IterM m γ)
|
||
|
||
@[always_inline, inherit_doc IterM.flatMapAfter]
|
||
public def Iter.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
|
||
{γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
|
||
(f : β → Iter (α := α₂) γ) (it₁ : Iter (α := α) β) (it₂ : Option (Iter (α := α₂) γ)) :=
|
||
((it₁.toIterM.flatMapAfter (fun b => (f b).toIterM) (Iter.toIterM <$> it₂)).toIter : Iter γ)
|
||
|
||
@[always_inline, expose, inherit_doc IterM.flatMap]
|
||
public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
|
||
{γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
|
||
(f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) :=
|
||
(it.flatMapAfter f none : Iter γ)
|