mathlib documentation

data.mllist

Monadic lazy lists. #

An alternative construction of lazy lists (see also data.lazy_list), with "lazyness" controlled by an arbitrary monad.

The inductive construction is not allowed outside of meta (indeed, we can build infinite objects). This isn't so bad, as the typical use is with the tactic monad, in any case.

As we're in meta anyway, we don't bother with proofs about these constructions.

meta inductive tactic.mllist (m : Type uType u) (α : Type u) :
Type u

A monadic lazy list, controlled by an arbitrary monad.

meta def tactic.mllist.fix {α : Type u} {m : Type uType u} [alternative m] (f : α → m α) :
α → tactic.mllist m α

Construct an mllist recursively.

meta def tactic.mllist.fixl_with {α β : Type u} {m : Type uType u} [alternative m] [monad m] (f : α → m × list β)) :
α → list βtactic.mllist m β

Repeatedly apply a function f : α → m (α × list β) to an initial a : α, accumulating the elements of the resulting list β as a single monadic lazy list.

(This variant allows starting with a specified list β of elements, as well. )

meta def tactic.mllist.fixl {α β : Type u} {m : Type uType u} [alternative m] [monad m] (f : α → m × list β)) (s : α) :

Repeatedly apply a function f : α → m (α × list β) to an initial a : α, accumulating the elements of the resulting list β as a single monadic lazy list.

meta def tactic.mllist.uncons {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (option × tactic.mllist m α))

Deconstruct an mllist, returning inside the monad an optional pair α × mllist m α representing the head and tail of the list.

meta def tactic.mllist.empty {m : Type uType u} [alternative m] [monad m] {α : Type u} (xs : tactic.mllist m α) :

Compute, inside the monad, whether an mllist is empty.

meta def tactic.mllist.of_list {m : Type uType u} [alternative m] [monad m] {α : Type u} :
list αtactic.mllist m α

Convert a list to an mllist.

meta def tactic.mllist.m_of_list {m : Type uType u} [alternative m] [monad m] {α : Type u} :
list (m α)tactic.mllist m α

Convert a list of values inside the monad into an mllist.

meta def tactic.mllist.force {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (list α)

Extract a list inside the monad from an mllist.

meta def tactic.mllist.take {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αm (list α)

Take the first n elements, as a list inside the monad.

meta def tactic.mllist.map {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → β) :

Apply a function to every element of an mllist.

meta def tactic.mllist.mmap {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → m β) :

Apply a function which returns values in the monad to every element of an mllist.

meta def tactic.mllist.filter {m : Type uType u} [alternative m] [monad m] {α : Type u} (p : α → Prop) [decidable_pred p] :

Filter a mllist.

meta def tactic.mllist.mfilter {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (p : α → m β) :

Filter a mllist using a function which returns values in the (alternative) monad. Whenever the function "succeeds", we accept the element, and reject otherwise.

meta def tactic.mllist.filter_map {m : Type uType u} [alternative m] [monad m] {α β : Type u} (f : α → option β) :

Filter and transform a mllist using an option valued function.

meta def tactic.mllist.mfilter_map {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (f : α → m β) :

Filter and transform a mllist using a function that returns values inside the monad. We discard elements where the function fails.

meta def tactic.mllist.append {m : Type uType u} [alternative m] [monad m] {α : Type u} :

Concatenate two monadic lazty lists.

meta def tactic.mllist.join {m : Type uType u} [alternative m] [monad m] {α : Type u} :

Join a monadic lazy list of monadic lazy lists into a single monadic lazy list.

meta def tactic.mllist.squash {m : Type uType u} [alternative m] [monad m] {α : Type u} (t : m (tactic.mllist m α)) :

Lift a monadic lazy list inside the monad to a monadic lazy list.

meta def tactic.mllist.enum_from {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αtactic.mllist m ( × α)

Enumerate the elements of a monadic lazy list, starting at a specified offset.

meta def tactic.mllist.enum {m : Type uType u} [alternative m] [monad m] {α : Type u} :

Enumerate the elements of a monadic lazy list.

meta def tactic.mllist.range {m : Type → Type} [alternative m] :

The infinite monadic lazy list of natural numbers.

meta def tactic.mllist.concat {m : Type uType u} [alternative m] [monad m] {α : Type u} :
tactic.mllist m αα → tactic.mllist m α

Add one element to the end of a monadic lazy list.

meta def tactic.mllist.bind_ {m : Type uType u} [alternative m] [monad m] {α β : Type u} :
tactic.mllist m α(α → tactic.mllist m β)tactic.mllist m β

Apply a function returning a monadic lazy list to each element of a monadic lazy list, joining the results.

meta def tactic.mllist.monad_lift {m : Type uType u} [alternative m] [monad m] {α : Type u} (x : m α) :

Convert any value in the monad to the singleton monadic lazy list.

meta def tactic.mllist.head {m : Type uType u} [alternative m] [monad m] [alternative m] {α : Type u} (L : tactic.mllist m α) :
m α

Return the head of a monadic lazy list, as a value in the monad.

meta def tactic.mllist.mfirst {m : Type uType u} [alternative m] [monad m] [alternative m] {α β : Type u} (L : tactic.mllist m α) (f : α → m β) :
m β

Apply a function returning values inside the monad to a monadic lazy list, returning only the first successful result.