A library providing tools for building enumeration procedures for recursively-
enumerable datatypes. This is built atop the arith-encode library, and makes
use of the natural number isomorphisms it provides to represent individual
decisions in the enumeration procedure. As such, each enumeration result is
denoted by a unique path, consisting of a sequence of natural numbers. An
enumeration procedure is simply a (partial) mapping between sequences
and a given datatype.
The library provides functionality for constructing enumeration procedures,
as well as facilities for performing enumeration according to various search
strategies (depth-first, breadth-first, etc). These procedures can also be
"warm-started" using a path or a set of paths. Obvious applications include
exhaustive search, testing, automated proving, and others.
Additionally, as a path is simply a sequence of natural numbers, an
enumeration procedure can double as a binary serializer/deserializer. For
well-behaved enumeration procedures (ie. those where the mapping is an
isomorphism), the resulting binary format should be very nearly succinct.