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 u Type u) (α : Type u) :

A monadic lazy list, controlled by an arbitrary monad.

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

Construct an mllist recursively.

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

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 u Type u} [monad m] [alternative 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 u Type u} [monad m] {α : Type u} :

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 u Type u} [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 u Type u} [monad m] {α : Type u} :

Convert a list to an mllist.

meta def tactic.mllist.m_of_list {m : Type u Type u} [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 u Type u} [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 u Type u} [monad m] {α : Type u} :

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

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

Apply a function to every element of an mllist.

meta def tactic.mllist.mmap {m : Type u Type u} [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 u Type u} [monad m] {α : Type u} (p : α Prop) [decidable_pred p] :

Filter a mllist.

meta def tactic.mllist.mfilter {m : Type u Type u} [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 u Type u} [monad m] {α β : Type u} (f : α option β) :

Filter and transform a mllist using an option valued function.

meta def tactic.mllist.mfilter_map {m : Type u Type u} [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 u Type u} [monad m] {α : Type u} :

Concatenate two monadic lazty lists.

meta def tactic.mllist.join {m : Type u Type u} [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 u Type u} [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 u Type u} [monad m] {α : Type u} :

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

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

Enumerate the elements of a monadic lazy list.

The infinite monadic lazy list of natural numbers.

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

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

meta def tactic.mllist.bind_ {m : Type u Type u} [monad m] {α β : Type u} :

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 u Type u} [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 u Type u} [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 u Type u} [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.