Init.Data.Stream

Module docstring

{"Remark: we considered using the following alternative design ``` structure Stream (α : Type u) where stream : Type u next? : stream → Option (α × stream)

class ToStream (collection : Type u) (value : outParam (Type v)) where toStream : collection → Stream value ``whereStreamis not a class, and its state is encapsulated. The key problem is that the typeStream α\"lives\" in a universe higher thanα. This is a problem because we want to useStream`s in monadic code. "}

ToStream structure

(collection : Type u) (stream : outParam (Type u))

Full source

/--
  Streams are used to implement parallel `for` statements.
  Example:
  ```
  for x in xs, y in ys do
    ...
  ```
  is expanded into
  ```
  let mut s := toStream ys
  for x in xs do
    match Stream.next? s with
    | none => break
    | some (y, s') =>
      s := s'
      ...
  ```
-/
class ToStream (collection : Type u) (stream : outParam (Type u)) : Type u where
  toStream : collection → stream

Collection to Stream Conversion

Informal description

The structure `ToStream` provides a way to convert a collection of type `collection` into a stream of type `stream`, where `stream` is an output parameter that represents the type of the stream. This is used to implement parallel `for` loops by iterating over multiple collections simultaneously.

Stream structure

(stream : Type u) (value : outParam (Type v))

Full source

class Stream (stream : Type u) (value : outParam (Type v)) : Type (max u v) where
  next? : stream → Option (value × stream)

Stream of values with underlying state type

Informal description

The structure `Stream` represents a stream of values of type `value` with an underlying state type `stream`. It provides a function `next?` that, given a state of type `stream`, returns an optional pair consisting of the next value of type `value` and the next state of type `stream`, or `None` if the stream has terminated.

Stream.forIn definition

[Stream ρ α] [Monad m] (s : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

Full source

protected partial def Stream.forIn [Stream ρ α] [Monad m] (s : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
  let _ : Inhabited (m β) := ⟨pure b⟩
  let rec visit (s : ρ) (b : β) : m β := do
    match Stream.next? s with
    | some (a, s) => match (← f a b) with
      | ForInStep.done b  => return b
      | ForInStep.yield b => visit s b
    | none => return b
  visit s b

Monadic iteration over a stream

Informal description

Given a monad `m`, a stream state `s` of type `ρ`, an initial accumulator value `b` of type `β`, and a function `f : α → β → m (ForInStep β)`, the function `Stream.forIn` iterates over the stream, applying `f` to each element and the current accumulator value. The iteration continues until the stream is exhausted or `f` returns a `ForInStep.done` value. The final accumulator value is returned in the monadic context.

instForInOfStream instance

[Stream ρ α] : ForIn m ρ α

Full source

instance (priority := low) [Stream ρ α] : ForIn m ρ α where
  forIn := Stream.forIn

Monadic Iteration Structure for Streams

Informal description

For any monad `m`, any stream type `ρ` with elements of type `α`, there exists a monadic iteration structure that allows iteration over the stream in the monad `m`.

instToStreamList instance

: ToStream (List α) (List α)

Full source

instance : ToStream (List α) (List α) where
  toStream c := c

List to Stream Conversion

Informal description

For any type $\alpha$, a list of elements of type $\alpha$ can be converted into a stream of elements of the same type.

instToStreamArraySubarray instance

: ToStream (Array α) (Subarray α)

Full source

instance : ToStream (Array α) (Subarray α) where
  toStream a := a[:a.size]

Array to Subarray Stream Conversion

Informal description

For any type $\alpha$, an array of elements of type $\alpha$ can be converted into a stream of subarrays of type $\alpha$.

instToStreamSubarray instance

: ToStream (Subarray α) (Subarray α)

Full source

instance : ToStream (Subarray α) (Subarray α) where
  toStream a := a

Subarray to Stream Conversion

Informal description

For any type $\alpha$, a subarray of elements of type $\alpha$ can be converted into a stream of elements of the same type.

instToStreamStringSubstring instance

: ToStream String Substring

Full source

instance : ToStream String Substring where
  toStream s := s.toSubstring

String to Substring Stream Conversion

Informal description

Strings can be converted into streams of substrings, where each substring represents a segment of the original string.

instToStreamRange instance

: ToStream Std.Range Std.Range

Full source

instance : ToStream Std.Range Std.Range where
  toStream r := r

Range to Stream Conversion

Informal description

The range type `Std.Range` can be converted into a stream of type `Std.Range`.

instStreamProd instance

[Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β)

Full source

instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
  next?
    | (s₁, s₂) =>
      match Stream.next? s₁ with
      | none => none
      | some (a, s₁) => match Stream.next? s₂ with
        | none => none
        | some (b, s₂) => some ((a, b), (s₁, s₂))

Stream Structure on Product Types

Informal description

For any types $\rho$ and $\gamma$ that can be viewed as streams of values of types $\alpha$ and $\beta$ respectively, the product type $\rho \times \gamma$ can be viewed as a stream of pairs of type $\alpha \times \beta$.

instStreamList instance

: Stream (List α) α

Full source

instance : Stream (List α) α where
  next?
    | []    => none
    | a::as => some (a, as)

Lists as Streams

Informal description

For any type $\alpha$, the type `List α` of linked lists of elements of type $\alpha$ can be viewed as a stream of elements of type $\alpha$. The stream's state is the list itself, and the `next?` function returns the head and tail of the list as the next value and state, or `None` if the list is empty.

instStreamSubarray instance

: Stream (Subarray α) α

Full source

instance : Stream (Subarray α) α where
  next? s :=
    if h : s.start < s.stop then
      have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
      some (s.array[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
        { s with start := s.start + 1, start_le_stop := this })
    else
      none

Subarrays as Streams

Informal description

For any type $\alpha$, a subarray of $\alpha$ can be viewed as a stream of elements of type $\alpha$. The stream's state is the subarray itself, and the `next?` function returns the next element and the remaining subarray, or `None` if the subarray is empty.

instStreamRangeNat instance

: Stream Std.Range Nat

Full source

instance : Stream Std.Range Nat where
  next? r :=
    if r.start < r.stop then
      some (r.start, { r with start := r.start + r.step })
    else
      none

Natural Number Ranges as Streams

Informal description

The type `Std.Range` representing ranges of natural numbers can be viewed as a stream of natural numbers. The stream's state is the range itself, and the `next?` function returns the next value in the range along with the remaining range, or `None` if the range is exhausted.

instStreamSubstringChar instance

: Stream Substring Char

Full source

instance : Stream Substring Char where
  next? s :=
    if s.startPos < s.stopPos then
      some (s.str.get s.startPos, { s with startPos := s.str.next s.startPos })
    else
      none

Substrings as Streams of Characters

Informal description

A substring can be viewed as a stream of Unicode characters. The stream's state is the substring itself, and the `next?` function returns the next character and the remaining substring, or `None` if the substring is empty.