diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index b0b780622d..18cb917817 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -42,7 +42,9 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α simp [binderNameHint] rfl -- very strange why `simp` did not close it -/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/ +/-- +Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`. +-/ def ForInStep.value (x : ForInStep α) : α := match x with | ForInStep.done b => b @@ -385,14 +387,20 @@ def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] controlAt m f /-- - Typeclass for the polymorphic `forM` operation described in the "do unchained" paper. - Remark: - - `γ` is a "container" type of elements of type `α`. - - `α` is treated as an output parameter by the typeclass resolution procedure. - That is, it tries to find an instance using only `m` and `γ`. +Overloaded monadic iteration over some container type. + +An instance of `ForM m γ α` describes how to iterate a monadic operator over a container of type `γ` +with elements of type `α` in the monad `m`. The element type should be uniquely determined by the +monad and the container. + +Use `ForM.forIn` to construct a `ForIn` instance from a `ForM` instance, thus enabling the use of +the `for` operator in `do`-notation. -/ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where - forM [Monad m] : γ → (α → m PUnit) → m PUnit + /-- + Runs the monadic action `f` on each element of the collection `coll`. + -/ + forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit export ForM (forM) diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 5e91fa6ba4..3c76f52bd4 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -159,7 +159,9 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := { end end StateT -/-- Adapter to create a ForIn instance from a ForM instance -/ +/-- +Creates a suitable implementation of `ForIn.forIn` from a `ForM` instance. +-/ @[always_inline, inline] def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do diff --git a/src/Init/Core.lean b/src/Init/Core.lean index c4272025bb..f08cbf1b43 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -294,68 +294,78 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where | intro (w : α) (h : p w) : Exists p /-- -Auxiliary type used to compile `for x in xs` notation. +An indication of whether a loop's body terminated early that's used to compile the `for x in xs` +notation. -This is the return value of the body of a `ForIn` call, -representing the body of a for loop. It can be: - -* `.yield (a : α)`, meaning that we should continue the loop and `a` is the new state. - `.yield` is produced by `continue` and reaching the bottom of the loop body. -* `.done (a : α)`, meaning that we should early-exit the loop with state `a`. - `.done` is produced by calls to `break` or `return` in the loop, +A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic +action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state +used to implement features such as `let mut`. -/ inductive ForInStep (α : Type u) where - /-- `.done a` means that we should early-exit the loop. - `.done` is produced by calls to `break` or `return` in the loop. -/ + /-- + The loop should terminate early. + + `ForInStep.done` is produced by uses of `break` or `return` in the loop body. + -/ | done : α → ForInStep α - /-- `.yield a` means that we should continue the loop. - `.yield` is produced by `continue` and reaching the bottom of the loop body. -/ + /-- + The loop should continue with the next iteration, using the returned state. + + `ForInStep.yield` is produced by `continue` and by reaching the bottom of the loop body. + -/ | yield : α → ForInStep α deriving Inhabited /-- -`ForIn m ρ α` is the typeclass which supports `for x in xs` notation. -Here `xs : ρ` is the type of the collection to iterate over, `x : α` -is the element type which is made available inside the loop, and `m` is the monad -for the encompassing `do` block. +Monadic iteration in `do`-blocks, using the `for x in xs` notation. + +The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of +the collection being iterated over, and `α` is the type of elements. -/ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) where - /-- `forIn x b f : m β` runs a for-loop in the monad `m` with additional state `β`. - This traverses over the "contents" of `x`, and passes the elements `a : α` to - `f : α → β → m (ForInStep β)`. `b : β` is the initial state, and the return value - of `f` is the new state as well as a directive `.done` or `.yield` - which indicates whether to abort early or continue iteration. + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. - The expression - ``` - let mut b := ... - for x in xs do - b ← foo x b - ``` - in a `do` block is syntactic sugar for: - ``` - let b := ... - let b ← forIn xs b (fun x b => do - let b ← foo x b - return .yield b) - ``` - (Here `b` corresponds to the variables mutated in the loop.) -/ - forIn {β} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β + Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic + action passed to `ForIn.forIn` takes a starting state in addition to the current element of the + collection and returns an updated state together with an indication of whether iteration should + continue or terminate. If the action returns `ForInStep.done`, then `ForIn.forIn` should stop + iteration and return the updated state. If the action returns `ForInStep.yield`, then + `ForIn.forIn` should continue iterating if there are further elements, passing the updated state + to the action. + + More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean + reference manual](lean-manual://section/monad-iteration-syntax). + -/ + forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β export ForIn (forIn) /-- -`ForIn' m ρ α d` is a variation on the `ForIn m ρ α` typeclass which supports the -`for h : x in xs` notation. It is the same as `for x in xs` except that `h : x ∈ xs` -is provided as an additional argument to the body of the for-loop. +Monadic iteration in `do`-blocks with a membership proof, using the `for h : x in xs` notation. + +The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of +the collection being iterated over, `α` is the type of elements, and `d` is the specific membership +predicate to provide. -/ -class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam $ Membership α ρ) where - /-- `forIn' x b f : m β` runs a for-loop in the monad `m` with additional state `β`. - This traverses over the "contents" of `x`, and passes the elements `a : α` along - with a proof that `a ∈ x` to `f : (a : α) → a ∈ x → β → m (ForInStep β)`. - `b : β` is the initial state, and the return value - of `f` is the new state as well as a directive `.done` or `.yield` - which indicates whether to abort early or continue iteration. -/ +class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) where + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. At each iteration, the body of the loop is provided with a proof + that the current element is in the collection. + + Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic + action passed to `ForIn'.forIn'` takes a starting state in addition to the current element of the + collection with its membership proof. The action returns an updated state together with an + indication of whether iteration should continue or terminate. If the action returns + `ForInStep.done`, then `ForIn'.forIn'` should stop iteration and return the updated state. If the + action returns `ForInStep.yield`, then `ForIn'.forIn'` should continue iterating if there are + further elements, passing the updated state to the action. + + More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the + Lean reference manual](lean-manual://section/monad-iteration-syntax). + -/ forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β export ForIn' (forIn') diff --git a/src/Init/Data/Cast.lean b/src/Init/Data/Cast.lean index 8697e4d676..3931fa9fb5 100644 --- a/src/Init/Data/Cast.lean +++ b/src/Init/Data/Cast.lean @@ -44,25 +44,26 @@ Nat → Nat → ...`. Sometimes we also need to declare the `CoeHTCT` instance if we need to shadow another coercion. -/ -/-- Type class for the canonical homomorphism `Nat → R`. -/ +/-- +The canonical homomorphism `Nat → R`. In most use cases, the target type will have a (semi)ring +structure, and this homomorphism should be a (semi)ring homomorphism. + +`NatCast` and `IntCast` exist to allow different libraries with their own types that can be notated +as natural numbers to have consistent `simp` normal forms without needing to create coercion +simplification sets that are aware of all combinations. Libraries should make it easy to work with +`NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a +`NatCast R` instance) whenever `R` is an additive monoid with a `1`. + +The prototypical example is `Int.ofNat`. +-/ class NatCast (R : Type u) where /-- The canonical map `Nat → R`. -/ protected natCast : Nat → R instance : NatCast Nat where natCast n := n -/-- -Canonical homomorphism from `Nat` to a type `R`. - -It contains just the function, with no axioms. -In practice, the target type will likely have a (semi)ring structure, -and this homomorphism should be a ring homomorphism. - -The prototypical example is `Int.ofNat`. - -This class and `IntCast` exist to allow different libraries with their own types that can be notated as natural numbers to have consistent `simp` normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with `NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a `NatCast R` instance) whenever `R` is an additive monoid with a `1`. --/ -@[coe, reducible, match_pattern] protected def Nat.cast {R : Type u} [NatCast R] : Nat → R := +@[coe, reducible, match_pattern, inherit_doc NatCast] +protected def Nat.cast {R : Type u} [NatCast R] : Nat → R := NatCast.natCast -- see the notes about coercions into arbitrary types in the module doc-string diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 148b1156d7..7969ed1c88 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -401,8 +401,14 @@ instance : Max Int := maxOfLe end Int /-- -The canonical homomorphism `Int → R`. -In most use cases `R` will have a ring structure and this will be a ring homomorphism. +The canonical homomorphism `Int → R`. In most use cases, the target type will have a ring structure, +and this homomorphism should be a ring homomorphism. + +`IntCast` and `NatCast` exist to allow different libraries with their own types that can be notated +as natural numbers to have consistent `simp` normal forms without needing to create coercion +simplification sets that are aware of all combinations. Libraries should make it easy to work with +`IntCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus an +`IntCast R` instance) whenever `R` is an additive group with a `1`. -/ class IntCast (R : Type u) where /-- The canonical map `Int → R`. -/ @@ -410,12 +416,8 @@ class IntCast (R : Type u) where instance : IntCast Int where intCast n := n -/-- -Apply the canonical homomorphism from `Int` to a type `R` from an `IntCast R` instance. - -In Mathlib there will be such a homomorphism whenever `R` is an additive group with a `1`. --/ -@[coe, reducible, match_pattern] protected def Int.cast {R : Type u} [IntCast R] : Int → R := +@[coe, reducible, match_pattern, inherit_doc IntCast] +protected def Int.cast {R : Type u} [IntCast R] : Int → R := IntCast.intCast -- see the notes about coercions into arbitrary types in the module doc-string diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index c222e2fe8a..f026bf8c25 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -439,7 +439,17 @@ may throw an exception of type `IO.Error`, the result of the task is an `Except (prio := Task.Priority.default) (sync := false) : BaseIO (Task (Except IO.Error β)) := EIO.bindTask t f prio sync -/-- `IO` specialization of `EIO.chainTask`. -/ +/-- +Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result. +This new task has priority `prio`. + +This is a version of `IO.mapTask` that ignores the result value. + +Running the resulting `IO` action causes the task to be started eagerly. Unlike pure tasks created +by `Task.spawn`, tasks created by this function will run even if the last reference to the task is +dropped. The act should explicitly check for cancellation via `IO.checkCanceled` if it should be +terminated or otherwise react to the last reference being dropped. +-/ def chainTask (t : Task α) (f : α → IO Unit) (prio := Task.Priority.default) (sync := false) : IO Unit := EIO.chainTask t f prio sync