-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Boltzmann sampler utilities for lambda calculus.
--   
--   Uniform generation of plain and closed lambda terms in the de Bruijn
--   notation.
@package lambda-sampler
@version 1.0


-- | Size notion framework of Gittenberger and Gołębiewski for lambda terms
--   in the de Bruijn notation. A size definition constitutes the weights
--   for lambda abstraction, term application, successor and zero.
module Data.Lambda.Model

-- | Lambda term size model.
data Model a
Model :: a -> a -> a -> a -> Model a

-- | Size of zero
[zeroW] :: Model a -> a

-- | Size of successor
[succW] :: Model a -> a

-- | Size of the abstraction
[absW] :: Model a -> a

-- | Size of the application
[appW] :: Model a -> a

-- | The natural size notion.
natural :: Integral a => Model a

-- | The binary size notion.
binary :: Integral a => Model a

-- | Checks whether the given size model is valid in the framework of
--   Gittenberger and Gołębiewski.
valid :: Integral a => Model a -> Bool

-- | Given a size notion, returns a tuple (a,b,c,d) where a denotes the
--   size of the de Bruijn zero, b denotes the size of the de Bruijn
--   successor, c denotes the size of the lambda abstraction and finally d
--   denotes the size of the application.
weights :: Model a -> (a, a, a, a)


-- | Lambda terms in the de Bruijn notation where instead of variables, we
--   use natural indices encoded as a sequence of successors of zero.
--   
--   Each index captures the distance to its binding lambda - Z corresponds
--   to a variable bound by the first lambda abstraction on its way to the
--   term root. The successor S increases the distance of its argument by
--   one. If an index points to a lambda abstraction outside of the term,
--   then that index represents a free variable in the term. Such a
--   representation for lambda terms avoids using explicit variable names
--   and hence eliminates the use of alpha-conversion.
module Data.Lambda

-- | Lambda terms with de Bruijn indices.
data Lambda

-- | de Bruijn indices.
Var :: Index -> Lambda

-- | Lambda abstraction.
Abs :: Lambda -> Lambda

-- | Term application.
App :: Lambda -> Lambda -> Lambda

-- | Predicate defining closed lambda terms.
isClosed :: Lambda -> Bool

-- | Computes the size of the given lambda term.
size :: Num a => Model a -> Lambda -> a

-- | Computes the size of the given de Bruijn index.
sizeVar :: Num a => Model a -> Index -> a

-- | Finds the maximal index in the given lambda term.
maxIndex :: (Num a, Ord a) => Lambda -> a

-- | de Bruijn indices in unary notation.
data Index
S :: Index -> Index
Z :: Index

-- | Translates the given index to a corresponding positive integer.
toInt :: (Num a) => Index -> a

-- | Translates the given positive integer to a corresponding index.
toIndex :: (Num a, Eq a) => a -> Index
instance GHC.Show.Show Data.Lambda.Index
instance GHC.Show.Show Data.Lambda.Lambda


-- | Boltzmann oracles finding numerical approximations of the generating
--   function singularities, dictating the asymptotic growth rate of
--   (closed h-shallow) lambda terms.
--   
--   The approximations are guaranteed to converge to the singularities
--   quadratically as the Newton-Raphson root finding algorithm is used.
module Data.Lambda.Random.Oracle

-- | Finds the dominating singularity of the plain lambda term ordinary
--   generating function.
domSing :: (Floating a, Ord a, Integral b) => Model b -> a -> a

-- | Successive root approximations of the plain lambda terms dominating
--   singularity.
roots :: (Floating a, Integral b) => Model b -> a -> [a]

-- | Finds the dominating singularity of the closed h-shallow lambda term
--   ordinary generating function.
domSingH :: (Floating a, Ord a, Integral b) => Model b -> b -> a -> a

-- | Successive root approximations of the closed h-shallow lambda terms
--   dominating singularity.
rootsH :: (Floating a, Integral b) => Model b -> b -> a -> [a]


-- | Combinatorial specification defining plain lambda terms in the de
--   Bruijn notation.
module Data.Lambda.Random.PlainSystem

-- | An expression defining the branching probabilities in the Boltzmann
--   model for plain lambda terms.
data PlainSystem a
PlainSystem :: a -> a -> a -> PlainSystem a

-- | Abstraction probability.
[abs] :: PlainSystem a -> a

-- | Application probability.
[app] :: PlainSystem a -> a

-- | Zero constructor probability.
[zero] :: PlainSystem a -> a

-- | Computes the Boltzmann model for plain lambda terms evaluated in the
--   given parameter.
boltzmannSystem :: (Floating a, Integral b) => Model b -> a -> PlainSystem a

-- | Boltzmann sampler specification consisting of a Boltzmann system with
--   a corresponding size notion model.
data PlainSampler a b
PlainSampler :: PlainSystem a -> Model b -> PlainSampler a b

-- | Boltzmann system.
[system] :: PlainSampler a b -> PlainSystem a

-- | Size notion.
[model] :: PlainSampler a b -> Model b

-- | Computes the Boltzmann sampler specification for plain lambda terms
--   evaluated in the given parameter.
boltzmannSampler :: (Floating a, Integral b) => Model b -> a -> PlainSampler a b

-- | Computes the rejection Boltzmann sampler for plain lambda terms
--   evaluated near the dominating singularity.
rejectionSampler :: (Floating a, Ord a, Integral b) => Model b -> a -> PlainSampler a b
instance GHC.Show.Show a => GHC.Show.Show (Data.Lambda.Random.PlainSystem.PlainSystem a)


-- | Combinatorial system defining closed h-shallow lambda terms in the de
--   Bruijn notation.
module Data.Lambda.Random.System

-- | An expression defining the branching probabilities in the Boltzmann
--   model for closed h-shallow lambda terms.
data Expr a
Expr :: a -> a -> [a] -> Expr a

-- | Abstraction probability.
[abs] :: Expr a -> a

-- | Application probability.
[app] :: Expr a -> a

-- | Probabilities for de Bruijn indices
[idx] :: Expr a -> [a]

-- | Combinatorial system specification for closed h-shallow lambda terms.
type System a = [Expr a]

-- | Computes the Boltzmann model for closed h-shallow lambda terms
--   evaluated in the given parameter.
boltzmannSystem :: (Floating a, Integral b) => Model b -> b -> a -> System a

-- | Boltzmann sampler specification consisting of a Boltzmann system with
--   a corresponding size notion model.
data Sampler a b
Sampler :: System a -> Model b -> Sampler a b

-- | Boltzmann system.
[system] :: Sampler a b -> System a

-- | Size notion.
[model] :: Sampler a b -> Model b

-- | Computes the Boltzmann sampler specification for closed h-shallow
--   lambda terms evaluated in the given parameter.
boltzmannSampler :: (Floating a, Integral b) => Model b -> b -> a -> Sampler a b

-- | Computes the rejection Boltzmann sampler for closed h-shallow lambda
--   terms evaluated near the dominating singularity.
rejectionSampler :: (Floating a, Ord a, Integral b) => Model b -> b -> a -> Sampler a b
instance GHC.Show.Show a => GHC.Show.Show (Data.Lambda.Random.System.Expr a)


-- | Boltzmann samplers for plain and closed h-shallow lambda terms (closed
--   lambda terms in which each de Bruijn index is bounded by h).
--   
--   The exact outcome size of a Boltzmann sampler is a random variable.
--   Its moments, in particular expectation, can be calibrated by adjusting
--   the formal evaluation parameter (see <a>Data.Lambda.Random.System</a>
--   or <a>Data.Lambda.Random.PlainSystem</a>). Boltzmann samplers
--   guarantee that terms of equal size have equal probability of being
--   chosen.
module Data.Lambda.Random

-- | Samples a random closed h-shallow lambda term in the given size range.
closedLambda :: (Random a, Num a, Ord a, Integral b, RandomGen g) => Sampler a b -> b -> b -> Rand g Lambda

-- | Samples a random closed h-shallow lambda term in the given size range
--   using the IO monad. See <a>closedLambda</a> for more details.
closedLambdaIO :: (Random a, Num a, Ord a, Integral b) => Sampler a b -> b -> b -> IO Lambda

-- | Samples a random closed h-shallow lambda term in the given size range.
--   In addition, the term has to satisfy the given predicate. See also
--   <a>closedLambda</a>.
filterClosed :: (Random a, Num a, Ord a, Integral b, RandomGen g) => (Lambda -> Bool) -> Sampler a b -> b -> b -> Rand g Lambda

-- | Samples a random closed h-shallow lambda term in the given size range.
--   In addition, the term has to satisfy the given predicate. The IO monad
--   is used as the source of random numbers. See also <a>filterClosed</a>.
filterClosedIO :: (Random a, Num a, Ord a, Integral b) => (Lambda -> Bool) -> Sampler a b -> b -> b -> IO Lambda

-- | Samples a random plain lambda term in the given size range.
plainLambda :: (Random a, Num a, Ord a, Integral b, RandomGen g) => PlainSampler a b -> b -> b -> Rand g Lambda

-- | Samples a random plain lambda term in the given size range using the
--   IO monad. See <a>plainLambda</a> for more details.
plainLambdaIO :: (Random a, Num a, Ord a, Integral b) => PlainSampler a b -> b -> b -> IO Lambda

-- | Samples a random plain lambda term in the given size range. In
--   addition, the term has to satisfy the given predicate. See also
--   <a>plainLambda</a>.
filterPlain :: (Random a, Num a, Ord a, Integral b, RandomGen g) => (Lambda -> Bool) -> PlainSampler a b -> b -> b -> Rand g Lambda

-- | Samples a random plain lambda term in the given size range. In
--   addition, the term has to satisfy the given predicate. The IO monad is
--   used as the source of random numbers. See also <a>filterPlain</a>.
filterPlainIO :: (Random a, Num a, Ord a, Integral b) => (Lambda -> Bool) -> PlainSampler a b -> b -> b -> IO Lambda