Lazy lists

The type LazyList α is a lazy list with elements of type α. In the VM, these are potentially infinite lists where all elements after the first are computed on-demand. (This is only useful for execution in the VM, logically we can prove that LazyList α is isomorphic to List α.)

inductive LazyList (α : Type u) : Type u

Lazy list. All elements (except the first) are computed lazily.

• nil: {α : Type u} → LazyList α
• cons: {α : Type u} → α → Thunk (LazyList α) → LazyList α

instance LazyList.instInhabitedLazyList {α : Type u} : Inhabited (LazyList α)

Equations

• LazyList.instInhabitedLazyList = { default := LazyList.nil }

def LazyList.singleton {α : Type u} : α → LazyList α

The singleton lazy list.

Equations

• LazyList.singleton x = let a := x; LazyList.cons a (Thunk.pure LazyList.nil)

def LazyList.ofList {α : Type u} : List α → LazyList α

Constructs a lazy list from a list.

Equations

• LazyList.ofList [] = LazyList.nil
• LazyList.ofList (h :: t) = LazyList.cons h { fn := fun (x : Unit) => LazyList.ofList t }

def LazyList.toList {α : Type u} : LazyList α → List α

Converts a lazy list to a list. If the lazy list is infinite, then this function does not terminate.

Equations

• LazyList.toList LazyList.nil = []
• LazyList.toList (LazyList.cons h t) = h :: LazyList.toList (Thunk.get t)

def LazyList.headI {α : Type u} [Inhabited α] : LazyList α → α

Returns the first element of the lazy list, or default if the lazy list is empty.

Equations

• LazyList.headI x = match x with | LazyList.nil => default | LazyList.cons h tl => h

def LazyList.tail {α : Type u} : LazyList α → LazyList α

Removes the first element of the lazy list.

Equations

• LazyList.tail x = match x with | LazyList.nil => LazyList.nil | LazyList.cons hd t => Thunk.get t

def LazyList.append {α : Type u} : LazyList α → Thunk (LazyList α) → LazyList α

Appends two lazy lists.

Equations

• LazyList.append LazyList.nil x = Thunk.get x
• LazyList.append (LazyList.cons h t) x = LazyList.cons h { fn := fun (x_1 : Unit) => LazyList.append (Thunk.get t) x }

def LazyList.map {α : Type u} {β : Type v} (f : α → β) : LazyList α → LazyList β

Maps a function over a lazy list.

Equations

• LazyList.map f LazyList.nil = LazyList.nil
• LazyList.map f (LazyList.cons h t) = LazyList.cons (f h) { fn := fun (x : Unit) => LazyList.map f (Thunk.get t) }

def LazyList.map₂ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) : LazyList α → LazyList β → LazyList δ

Maps a binary function over two lazy list. Like LazyList.zip, the result is only as long as the smaller input.

Equations

• LazyList.map₂ f LazyList.nil x = LazyList.nil
• LazyList.map₂ f x LazyList.nil = LazyList.nil
• LazyList.map₂ f (LazyList.cons h₁ t₁) (LazyList.cons h₂ t₂) = LazyList.cons (f h₁ h₂) { fn := fun (x : Unit) => LazyList.map₂ f (Thunk.get t₁) (Thunk.get t₂) }

def LazyList.zip {α : Type u} {β : Type v} : LazyList α → LazyList β → LazyList (α × β)

Zips two lazy lists.

Equations

• LazyList.zip = LazyList.map₂ Prod.mk

def LazyList.join {α : Type u} : LazyList (LazyList α) → LazyList α

The monadic join operation for lazy lists.

Equations

• LazyList.join LazyList.nil = LazyList.nil
• LazyList.join (LazyList.cons h t) = LazyList.append h { fn := fun (x : Unit) => LazyList.join (Thunk.get t) }

def LazyList.for {α : Type u} {β : Type v} (l : LazyList α) (f : α → β) : LazyList β

Maps a function over a lazy list. Same as LazyList.map, but with swapped arguments.

Equations

• LazyList.for l f = LazyList.map f l

def LazyList.approx {α : Type u} : Nat → LazyList α → List α

The list containing the first n elements of a lazy list.

Equations

• LazyList.approx 0 x = []
• LazyList.approx x LazyList.nil = []
• LazyList.approx (Nat.succ a) (LazyList.cons h t) = h :: LazyList.approx a (Thunk.get t)

def LazyList.filter {α : Type u} (p : α → Prop) [DecidablePred p] : LazyList α → LazyList α

The lazy list of all elements satisfying the predicate. If the lazy list is infinite and none of the elements satisfy the predicate, then this function will not terminate.

Equations

• LazyList.filter p LazyList.nil = LazyList.nil
• LazyList.filter p (LazyList.cons h t) = if p h then LazyList.cons h { fn := fun (x : Unit) => LazyList.filter p (Thunk.get t) } else LazyList.filter p (Thunk.get t)

def LazyList.nth {α : Type u} : LazyList α → Nat → Option α

The nth element of a lazy list as an option (like List.get?).

Equations

• LazyList.nth LazyList.nil x = none
• LazyList.nth (LazyList.cons a tl) 0 = some a
• LazyList.nth (LazyList.cons hd l) (Nat.succ n) = LazyList.nth (Thunk.get l) n

unsafe def LazyList.iterates {α : Type u} (f : α → α) : α → LazyList α

The infinite lazy list [x, f x, f (f x), ...] of iterates of a function. This definition is meta because it creates an infinite list.

Equations

• LazyList.iterates f x = let x := x; LazyList.cons x { fn := fun (x_1 : Unit) => LazyList.iterates f (f x) }

unsafe def LazyList.iota (i : Nat) : LazyList Nat

The infinite lazy list [i, i+1, i+2, ...]

Equations

• LazyList.iota i = LazyList.iterates Nat.succ i