-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A practical API for building recursive enumeration -- procedures and enumerating datatypes. -- -- 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. @package enumeration @version 0.2.0 -- | Utilities for constructing enumerations over datatypes. -- -- An Enumeration is a mapping between a particular datatype and a -- Path, which consists of a list of natural numbers. -- Conceptually, we can think of all the values of a given datatype as -- being organized into a tree, with nodes representing decisions that -- narrow down the choices. In such a scheme, a Path represents a -- path through the tree to a single value, and an Enumeration is -- a procedure for converting a Path to and from a value. -- -- An Enumeration has two key functions: fromPath and -- toPath, which translate between paths and instances of a -- datatype. These functions are expected to be inverses; or: -- -- -- -- Beyond this, there are no additional restrictions. Specifically, two -- paths may map to the same value. -- -- The numBranches function indicates the maximum value of the -- first path element for an Enumeration. The minimum value is -- always 0, and all values between 0 and numBranches must be -- valid. If there is no upper bound on the value of the first path -- element, numBranches returns Nothing. The -- toSizedPath maps a value to a path, which also contains the -- result of numBranches at each step in the path. -- -- The withPrefix function supplies a partial path to an -- Enumeration, yielding a new Enumeration that maps each -- value to the same path(s) as the original Enumeration, with the -- prefix added or removed. More formally, if -- -- -- -- Then -- -- -- -- With multiple uses of withPrefix, the following must be true: -- -- -- -- Finally, if a complete path is given to withPrefix, then the -- result is a singleton encoding that gives the value associated with -- that path. That is: -- -- -- -- This provides "warm-start" functionality for Enumerations. When -- translating a large number of Paths with the same prefix, it -- will generally be much more efficient to use withPrefix and use -- the resulting Enumeration than to translate the Paths -- directly. -- -- The prefix function gives the current prefix for an -- Enumeration. The following rule describes the relationship -- between prefix and withPrefix: -- -- -- -- Enumerations are similar to Encodings from the -- arith-encode library, except Enumerations are generally more -- flexible, and can more easily accomodate complex datatypes with -- invariants. However, as Paths are constructed from natural -- numbers, we can create an Enumeration using a series of -- Encodings for intermediate data. The functions in this module -- provide the ability to construct Enumerations using -- Encodings -- -- A singleton Enumeration can be constructed using the -- singleton and singletonWithPrefix functions. -- -- An Encoding for a datatype can be converted into an -- Enumeration (where all paths have a single element) using the -- fromEncoding and fromEncodingWithPrefix functions. -- -- The step and stepWithPrefix functions construct an -- Enumeration from an Encoding for an intermediate value, -- and a generator function that produces an Enumeration from the -- intermediate value. -- -- The withPrefix variants for each of these take a prefix path, -- where the non-withPrefix variants set the prefix to -- []. module Data.Enumeration -- | A datatype that represents a mapping between Paths and -- tys. Note that unlike Encodings, not all -- Paths are necessarily valid. data Enumeration ty -- | A path that uniquely identifies a value in an Enumeration. type Path = [Integer] -- | An exception thrown when a Path is invalid. data BadPath BadPath :: String -> BadPath -- | An exception to be thrown if an illegal argument is given to -- encode, decode. data IllegalArgument IllegalArgument :: !String -> IllegalArgument -- | Generate a ty from a Path fromPath :: Enumeration ty -> Path -> ty -- | Convert a ty to a Path toPath :: Enumeration ty -> ty -> Path -- | Convert to a list of pairs, where the fst holds the path -- entry, and snd holds numBranches. This is used -- primarily for encoding values as binary. toSizedPath :: Enumeration ty -> ty -> [(Integer, Maybe Integer)] -- | Given a prefix path, get an enumeration that generates tys -- from the rest of the path. withPrefix :: Enumeration ty -> Path -> Enumeration ty -- | Get the upper bound on values for the first path component, or -- Nothing if there is no bound. numBranches :: Enumeration ty -> Maybe Integer -- | The prefix path. prefix :: Enumeration ty -> Path -- | Create an Enumeration with an empty prefix that maps a single -- value to and from the empty path. Equivalent to -- singletonWithPrefix [] singleton :: Eq ty => ty -> Enumeration ty -- | Create an Enumeration with a given prefix path that maps a -- single value to and from the empty path. singletonWithPrefix :: Eq ty => Path -> ty -> Enumeration ty -- | Create an Enumeration with an empty prefix from a single -- Encoding. The Path will always be of length 1, and -- contains the encoded value. fromEncoding :: Eq ty => Encoding ty -> Enumeration ty -- | Create an Enumeration with a given prefix from a single -- Encoding. The Path will always be of length 1, and -- contains the encoded value. fromEncodingWithPrefix :: Eq ty => Path -> Encoding ty -> Enumeration ty -- | Create an Enumeration with an empty prefix that uses an -- Encoding to convert the first element of the path to an interim -- value, then uses that value to construct an Enumeration to -- decode the rest of the path. step :: Encoding ty1 -> (Path -> ty1 -> Enumeration ty2) -> (ty2 -> ty1) -> Enumeration ty2 -- | Create an Enumeration with a prefix that uses an -- Encoding to convert the first element of the path to an interim -- value, then uses that value to construct an Enumeration to -- decode the rest of the path. stepWithPrefix :: Path -> Encoding ty1 -> (Path -> ty1 -> Enumeration ty2) -> (ty2 -> ty1) -> Enumeration ty2 instance GHC.Show.Show Data.Enumeration.BadPath instance GHC.Exception.Type.Exception Data.Enumeration.BadPath -- | Functions for binary serialization/deserialization of datatypes using -- an Enumeration. These functions write out/read in binary data -- as a sequence of natural numbers representing a path (using the same -- coding scheme as Data.Encoding.Binary). module Data.Enumeration.Binary -- | Use an Enumeration to write out a ty as binary data putWithEnumeration :: Enumeration ty -> ty -> Put -- | Use an Enumeration to extract a ty from binary data. getWithEnumeration :: Enumeration ty -> Get ty -- | Functionality for traversing an Enumeration. -- -- This module provides a typeclass, Traversal, which represents a -- traversal scheme for Enumerations. Traversals should be largely -- independent of the Enumeration, though some variants like -- Prioritized cannot be wholly independent. -- -- Three Traversal instances are provided by this module: -- DepthFirst, BreadthFirst, and Prioritized. All -- traversals work by maintaining a set of positions, which consist of an -- Enumeration and an index (the next value to give as a first -- path element). At each step, some position is "expanded" by replacing -- it with two positions: one with the index as an additional prefix -- element, and one with the index incremented. -- -- DepthFirst is a simple depth-first scheme. It is not guaranteed -- to reach all elements, and in some Enumerations, it may never -- produce an answer. -- -- BreadthFirst is a breadth-first scheme, which tends to be -- better-behaved than DepthFirst. It explores paths in ascending -- order of path length. For Enumerations with infinite-sized -- branches, its behavior is not strictly breadth-first (as this would -- never yield an answer), but it should still behave well for this case. -- -- Prioritized is a scheme that uses a scoring function to rank -- paths. At each step, it will select the "best" (highest-ranked) option -- and expand it. module Data.Enumeration.Traversal -- | A typeclass representing a traversal scheme over an enumeration. class Traversal trav -- | Create a Traversal from an Enumeration. mkTraversal :: Traversal trav => Enumeration ty -> trav ty -- | Get the next item in the traversal. getNext :: Traversal trav => trav ty -> Maybe (ty, Path, trav ty) -- | Get all items in the traversal as a list. getAll :: Traversal trav => trav ty -> [(ty, Path)] -- | Depth-first traversal. Note that this style of traversal is not -- guaranteed to be complete (it may deep-dive and never visit some -- possibilities). However, this implementation should continue producing -- results even with infinite-sized branches, so long as the depth of any -- one path isn't too great. data DepthFirst ty -- | Breadth-first traversal. This style of traversal is guaranteed to be -- complete- that is, it will visit every possibility eventually. -- However, it may take a very long time to reach any given possibility. data BreadthFirst ty -- | Prioritized traversal. Will always pick the highest-scored option. -- Completeness depends entirely on the scoring function. data Prioritized ty -- | The scoring function used in a Prioritized traversal scheme. scoring :: Prioritized ty -> (Enumeration ty, Integer) -> Float -- | Create a prioritized traversal with a given scoring function. mkPrioritizedTraversal :: ((Enumeration ty, Integer) -> Float) -> Enumeration ty -> Prioritized ty instance Data.Enumeration.Traversal.Class.Traversal Data.Enumeration.Traversal.Prioritized instance Data.Enumeration.Traversal.Class.Traversal Data.Enumeration.Traversal.BreadthFirst instance Data.Enumeration.Traversal.Class.Traversal Data.Enumeration.Traversal.DepthFirst