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


-- | Generic programming library with representation types
--   
--   Generic programming library providing structural polymorphism, simple
--   programming with binders, and other features.
@package RepLib
@version 0.3


-- | A slow, but hopefully correct implementation of permutations.
module Generics.RepLib.Bind.PermM
data Perm a
single :: Ord a => a -> a -> Perm a

-- | Compose two permutations. The right-hand permutation will be applied
--   first.
(<>) :: Ord a => Perm a -> Perm a -> Perm a
apply :: Ord a => Perm a -> a -> a
support :: Ord a => Perm a -> [a]

-- | isid -- do all keys map to themselves?
isid :: Ord a => Perm a -> Bool

-- | Join two permutation. Fail if the two permutations map the same name
--   to two different variables.
join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
empty :: Perm a
restrict :: Ord a => Perm a -> [a] -> Perm a
instance Show a => Show (Perm a)
instance Ord a => Eq (Perm a)


-- | Basic data structure and class for representation types
module Generics.RepLib.R

-- | A value of type <tt>R a</tt> is a representation of a type <tt>a</tt>.
data R a
Int :: R Int
Char :: R Char
Integer :: R Integer
Float :: R Float
Double :: R Double
Rational :: R Rational
IOError :: R IOError
IO :: R a -> R (IO a)
Arrow :: R a -> R b -> R (a -> b)
Data :: DT -> [Con R a] -> R a
Abstract :: DT -> R a

-- | Representation of a data constructor includes an embedding between the
--   datatype and a list of other types as well as the representation of
--   that list of other types.
data Con r a
Con :: (Emb l a) -> (MTup r l) -> Con r a

-- | An embedding between a list of types <tt>l</tt> and a datatype
--   <tt>a</tt>, based on a particular data constructor. The to function is
--   a wrapper for the constructor, the from function pattern matches on
--   the constructor.
data Emb l a
Emb :: (l -> a) -> (a -> Maybe l) -> Maybe [String] -> String -> Fixity -> Emb l a
to :: Emb l a -> l -> a
from :: Emb l a -> a -> Maybe l
labels :: Emb l a -> Maybe [String]
name :: Emb l a -> String
fixity :: Emb l a -> Fixity
data Fixity
Nonfix :: Fixity
Infix :: Int -> Fixity
prec :: Fixity -> Int
Infixl :: Int -> Fixity
prec :: Fixity -> Int
Infixr :: Int -> Fixity
prec :: Fixity -> Int

-- | Information about a datatype, including its fully qualified name and
--   representation of its type arguments.
data DT
DT :: String -> (MTup R l) -> DT

-- | An empty list of types
data Nil
Nil :: Nil

-- | Cons for a list of types
data (:*:) a l
(:*:) :: a -> l -> :*: a l
data Ex f
Ex :: (f a) -> Ex f

-- | A heterogeneous list
data MTup r l
MNil :: MTup r Nil
(:+:) :: r a -> MTup r l -> MTup r (a :*: l)
MEx :: MTup r (f a) -> MTup r (Ex f)

-- | A Class of representatble types
class Rep a
rep :: Rep a => R a
rUnitEmb :: Emb Nil ()
rUnit :: R ()
rTup2 :: (Rep a, Rep b) => R (a, b)
rPairEmb :: Emb (a :*: (b :*: Nil)) (a, b)
rList :: Rep a => R [a]
rNilEmb :: Emb Nil [a]
rConsEmb :: Emb (a :*: ([a] :*: Nil)) [a]
instance Rep a => Rep [a]
instance (Rep a, Rep b) => Rep (a, b)
instance Rep ()
instance (Rep a, Rep b) => Rep (a -> b)
instance Rep IOError
instance Rep a => Rep (IO a)
instance Rep Integer
instance Rep Float
instance Rep Rational
instance Rep Double
instance Rep Char
instance Rep Int
instance Ord (R a)
instance Eq (R a)
instance Show (MTup R l)
instance Show DT
instance Show (R a)


module Generics.RepLib.R1
data R1 ctx a
Int1 :: R1 ctx Int
Char1 :: R1 ctx Char
Integer1 :: R1 ctx Integer
Float1 :: R1 ctx Float
Double1 :: R1 ctx Double
Rational1 :: R1 ctx Rational
IOError1 :: R1 ctx IOError
IO1 :: ctx a -> R1 ctx (IO a)
Arrow1 :: ctx a -> ctx b -> R1 ctx (a -> b)
Data1 :: DT -> [Con ctx a] -> R1 ctx a
Abstract1 :: DT -> R1 ctx a
class Sat a
dict :: Sat a => a
class Rep a => Rep1 ctx a
rep1 :: Rep1 ctx a => R1 ctx a

-- | Access a representation, given a proxy
getRepC :: Rep b => c b -> R b

-- | Transform a parameterized rep to a vanilla rep
toR :: R1 c a -> R a
rTup2_1 :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a, b)
rList1 :: Rep a => ctx a -> ctx [a] -> R1 ctx [a]
instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a]
instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a, b)
instance Rep1 ctx ()
instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => Rep1 ctx (a -> b)
instance (Rep a, Sat (ctx a)) => Rep1 ctx (IO a)
instance Rep1 ctx Rational
instance Rep1 ctx IOError
instance Rep1 ctx Double
instance Rep1 ctx Float
instance Rep1 ctx Integer
instance Rep1 ctx Char
instance Rep1 ctx Int
instance Show (R1 c a)


-- | Automatically derive representations and instance declarations for
--   user defined datatypes. The typical use is <tt> $(derive [''MyType1,
--   ''MyType2]) </tt>
module Generics.RepLib.Derive

-- | Generate representations (both basic and parameterized) for a list of
--   types.
derive :: [Name] -> Q [Dec]

-- | Generate abstract representations for a list of types.
derive_abstract :: [Name] -> Q [Dec]


-- | Representations for Prelude types, necessary to (automatically) derive
--   representations of user defined types.
module Generics.RepLib.PreludeReps
rBool1 :: R1 ctx[aaHE] Bool
rBool :: R Bool
rMaybe1 :: Rep a[a1IU] => ctx[aaHu] a[a1IU] -> R1 ctx[aaHu] (Maybe a[a1IU])
rMaybe :: Rep a[a1IU] => R (Maybe a[a1IU])
rEither1 :: (Rep a[aaH6], Rep b[aaH5]) => ctx[aaHf] a[aaH6] -> ctx[aaHf] b[aaH5] -> R1 ctx[aaHf] (Either a[aaH6] b[aaH5])
rEither :: (Rep a[aaH6], Rep b[aaH5]) => R (Either a[aaH6] b[aaH5])
rOrdering1 :: R1 ctx[aaGY] Ordering
rOrdering :: R Ordering
rTup3_1 :: (Rep a[12], Rep b[13], Rep c[14]) => ctx[aaGG] a[12] -> ctx[aaGG] b[13] -> ctx[aaGG] c[14] -> R1 ctx[aaGG] ((,,) a[12] b[13] c[14])
rTup3 :: (Rep a[12], Rep b[13], Rep c[14]) => R ((,,) a[12] b[13] c[14])
rTup4_1 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15]) => ctx[aaGj] a[12] -> ctx[aaGj] b[13] -> ctx[aaGj] c[14] -> ctx[aaGj] d[15] -> R1 ctx[aaGj] ((,,,) a[12] b[13] c[14] d[15])
rTup4 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15]) => R ((,,,) a[12] b[13] c[14] d[15])
rTup5_1 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16]) => ctx[aaFR] a[12] -> ctx[aaFR] b[13] -> ctx[aaFR] c[14] -> ctx[aaFR] d[15] -> ctx[aaFR] e[16] -> R1 ctx[aaFR] ((,,,,) a[12] b[13] c[14] d[15] e[16])
rTup5 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16]) => R ((,,,,) a[12] b[13] c[14] d[15] e[16])
rTup6_1 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17]) => ctx[aaFk] a[12] -> ctx[aaFk] b[13] -> ctx[aaFk] c[14] -> ctx[aaFk] d[15] -> ctx[aaFk] e[16] -> ctx[aaFk] f[17] -> R1 ctx[aaFk] ((,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
rTup6 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17]) => R ((,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
rTup7_1 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17], Rep g[18]) => ctx[aaEI] a[12] -> ctx[aaEI] b[13] -> ctx[aaEI] c[14] -> ctx[aaEI] d[15] -> ctx[aaEI] e[16] -> ctx[aaEI] f[17] -> ctx[aaEI] g[18] -> R1 ctx[aaEI] ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
rTup7 :: (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17], Rep g[18]) => R ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
instance Rep1 ctx[aaHE] Bool
instance Rep Bool
instance (Rep a[a1IU], Sat (ctx[aaHu] a[a1IU])) => Rep1 ctx[aaHu] (Maybe a[a1IU])
instance Rep a[a1IU] => Rep (Maybe a[a1IU])
instance (Rep a[aaH6], Rep b[aaH5], Sat (ctx[aaHf] a[aaH6]), Sat (ctx[aaHf] b[aaH5])) => Rep1 ctx[aaHf] (Either a[aaH6] b[aaH5])
instance (Rep a[aaH6], Rep b[aaH5]) => Rep (Either a[aaH6] b[aaH5])
instance Rep1 ctx[aaGY] Ordering
instance Rep Ordering
instance (Rep a[12], Rep b[13], Rep c[14], Sat (ctx[aaGG] a[12]), Sat (ctx[aaGG] b[13]), Sat (ctx[aaGG] c[14])) => Rep1 ctx[aaGG] (a[12], b[13], c[14])
instance (Rep a[12], Rep b[13], Rep c[14]) => Rep (a[12], b[13], c[14])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Sat (ctx[aaGj] a[12]), Sat (ctx[aaGj] b[13]), Sat (ctx[aaGj] c[14]), Sat (ctx[aaGj] d[15])) => Rep1 ctx[aaGj] (a[12], b[13], c[14], d[15])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15]) => Rep (a[12], b[13], c[14], d[15])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Sat (ctx[aaFR] a[12]), Sat (ctx[aaFR] b[13]), Sat (ctx[aaFR] c[14]), Sat (ctx[aaFR] d[15]), Sat (ctx[aaFR] e[16])) => Rep1 ctx[aaFR] (a[12], b[13], c[14], d[15], e[16])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16]) => Rep (a[12], b[13], c[14], d[15], e[16])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17], Sat (ctx[aaFk] a[12]), Sat (ctx[aaFk] b[13]), Sat (ctx[aaFk] c[14]), Sat (ctx[aaFk] d[15]), Sat (ctx[aaFk] e[16]), Sat (ctx[aaFk] f[17])) => Rep1 ctx[aaFk] (a[12], b[13], c[14], d[15], e[16], f[17])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17]) => Rep (a[12], b[13], c[14], d[15], e[16], f[17])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17], Rep g[18], Sat (ctx[aaEI] a[12]), Sat (ctx[aaEI] b[13]), Sat (ctx[aaEI] c[14]), Sat (ctx[aaEI] d[15]), Sat (ctx[aaEI] e[16]), Sat (ctx[aaEI] f[17]), Sat (ctx[aaEI] g[18])) => Rep1 ctx[aaEI] (a[12], b[13], c[14], d[15], e[16], f[17], g[18])
instance (Rep a[12], Rep b[13], Rep c[14], Rep d[15], Rep e[16], Rep f[17], Rep g[18]) => Rep (a[12], b[13], c[14], d[15], e[16], f[17], g[18])


-- | Auxiliary operations to aid in the definition of type-indexed
--   functions
module Generics.RepLib.RepAux

-- | Determine if two reps are for the same type
eqR :: R a -> R b -> Bool

-- | The type-safe cast operation, implicit arguments
cast :: (Rep a, Rep b) => a -> Maybe b

-- | The type-safe cast operation, explicit arguments
castR :: R a -> R b -> a -> Maybe b

-- | Leibniz equality between types, implicit representations
gcast :: (Rep a, Rep b) => c a -> Maybe (c b)

-- | Leibniz equality between types, explicit representations
gcastR :: R a -> R b -> c a -> Maybe (c b)

-- | Heterogeneous Ordering
compareR :: R a -> R b -> Ordering

-- | Given a list of constructor representations for a datatype, determine
--   which constructor formed the datatype.
findCon :: [Con ctx a] -> a -> Val ctx a

-- | A datastructure to store the results of findCon
data Val ctx a
Val :: (Emb l a) -> (MTup ctx l) -> l -> Val ctx a

-- | A fold left for heterogeneous lists
foldl_l :: (forall a. Rep a => ctx a -> b -> a -> b) -> b -> (MTup ctx l) -> l -> b

-- | A fold right operation for heterogeneous lists, that folds a function
--   expecting a type type representation across each element of the list.
foldr_l :: (forall a. Rep a => ctx a -> a -> b -> b) -> b -> (MTup ctx l) -> l -> b

-- | A map for heterogeneous lists
map_l :: (forall a. Rep a => ctx a -> a -> a) -> (MTup ctx l) -> l -> l

-- | Transform a heterogeneous list in to a standard list
mapQ_l :: (forall a. Rep a => ctx a -> a -> r) -> MTup ctx l -> l -> [r]

-- | mapM for heterogeneous lists
mapM_l :: Monad m => (forall a. Rep a => ctx a -> a -> m a) -> MTup ctx l -> l -> m l

-- | Generate a heterogeneous list from metadata
fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l

-- | Generate a heterogeneous list from metadata, in a monad
fromTupM :: Monad m => (forall a. Rep a => ctx a -> m a) -> MTup ctx l -> m l

-- | Generate a normal lists from metadata
toList :: (forall a. Rep a => ctx a -> b) -> MTup ctx l -> [b]

-- | A SYB style traversal
type Traversal = forall a. Rep a => a -> a

-- | SYB style query type
type Query r = forall a. Rep a => a -> r

-- | SYB style monadic map type
type MapM m = forall a. Rep a => a -> m a

-- | Map a traversal across the kids of a data structure
gmapT :: Rep a => Traversal -> a -> a
gmapQ :: Rep a => Query r -> a -> [r]
gmapM :: (Rep a, Monad m) => MapM m -> a -> m a
type Traversal1 ctx = forall a. Rep a => ctx a -> a -> a
type Query1 ctx r = forall a. Rep a => ctx a -> a -> r
type MapM1 ctx m = forall a. Rep a => ctx a -> a -> m a
gmapT1 :: Rep1 ctx a => Traversal1 ctx -> a -> a
gmapQ1 :: Rep1 ctx a => Query1 ctx r -> a -> [r]
gmapM1 :: (Rep1 ctx a, Monad m) => MapM1 ctx m -> a -> m a
data Typed a
(:::) :: a -> R a -> Typed a
data Spine a
Constr :: a -> Spine a
(:<>) :: Spine (a -> b) -> Typed a -> Spine b
toSpine :: Rep a => a -> Spine a
fromSpine :: Spine a -> a
instance Ord DT
instance Eq DT


module Generics.RepLib.SYB.Aliases

-- | Make a generic transformation; start from a type-specific case;
--   preserve the term otherwise
mkT :: (Rep a, Rep b) => (b -> b) -> a -> a

-- | Make a generic query; start from a type-specific case; return a
--   constant otherwise
mkQ :: (Rep a, Rep b) => r -> (b -> r) -> a -> r

-- | Make a generic monadic transformation; start from a type-specific
--   case; resort to return otherwise
mkM :: (Monad m, Rep a, Rep b) => (b -> m b) -> a -> m a

-- | Make a generic monadic transformation for MonadPlus; use "const mzero"
--   (i.e., failure) instead of return as default.
mkMp :: (MonadPlus m, Rep a, Rep b) => (b -> m b) -> a -> m a

-- | Make a generic builder; start from a type-specific ase; resort to no
--   build (i.e., mzero) otherwise
mkR :: (MonadPlus m, Rep a, Rep b) => m b -> m a

-- | Flexible type extension
ext0 :: (Rep a, Rep b) => c a -> c b -> c a

-- | Extend a generic transformation by a type-specific case
extT :: (Rep a, Rep b) => (a -> a) -> (b -> b) -> a -> a

-- | Extend a generic query by a type-specific case
extQ :: (Rep a, Rep b) => (a -> q) -> (b -> q) -> a -> q

-- | Extend a generic monadic transformation by a type-specific case
extM :: (Monad m, Rep a, Rep b) => (a -> m a) -> (b -> m b) -> a -> m a

-- | Extend a generic MonadPlus transformation by a type-specific case
extMp :: (MonadPlus m, Rep a, Rep b) => (a -> m a) -> (b -> m b) -> a -> m a

-- | Extend a generic builder
extB :: (Rep a, Rep b) => a -> b -> a

-- | Extend a generic reader
extR :: (Monad m, Rep a, Rep b) => m a -> m b -> m a

-- | Generic transformations, i.e., take an "a" and return an "a"
type GenericT = forall a. Rep a => a -> a

-- | Generic queries of type "r", i.e., take any "a" and return an "r"
type GenericQ r = forall a. Rep a => a -> r

-- | Generic monadic transformations, i.e., take an "a" and compute an "a"
type GenericM m = forall a. Rep a => a -> m a

-- | Generic builders i.e., produce an "a".
type GenericB = forall a. Rep a => a

-- | Generic readers, say monadic builders, i.e., produce an "a" with the
--   help of a monad "m".
type GenericR m = forall a. Rep a => m a

-- | The general scheme underlying generic functions assumed by gfoldl;
--   there are isomorphisms such as GenericT = Generic T.
type Generic c = forall a. Rep a => a -> c a

-- | Wrapped generic functions; recall: [Generic c] would be legal but
--   [Generic' c] not.
data Generic' c
Generic' :: Generic c -> Generic' c
unGeneric' :: Generic' c -> Generic c

-- | Other first-class polymorphic wrappers
newtype GenericT'
GT :: (forall a. Rep a => a -> a) -> GenericT'
unGT :: GenericT' -> forall a. Rep a => a -> a
newtype GenericQ' r
GQ :: GenericQ r -> GenericQ' r
unGQ :: GenericQ' r -> GenericQ r
newtype GenericM' m
GM :: (forall a. Rep a => a -> m a) -> GenericM' m
unGM :: GenericM' m -> forall a. Rep a => a -> m a

-- | Left-biased choice on maybies
orElse :: Maybe a -> Maybe a -> Maybe a

-- | Recover from the failure of monadic transformation by identity
recoverMp :: MonadPlus m => GenericM m -> GenericM m

-- | Recover from the failure of monadic query by a constant
recoverQ :: MonadPlus m => r -> GenericQ (m r) -> GenericQ (m r)

-- | Choice for monadic transformations
choiceMp :: MonadPlus m => GenericM m -> GenericM m -> GenericM m

-- | Choice for monadic queries
choiceQ :: MonadPlus m => GenericQ (m r) -> GenericQ (m r) -> GenericQ (m r)


-- | Derived from Data.Generics.Schemes Only modification: <a>Data</a>
--   class becomes <a>Rep</a> class otherwise import our version of the
--   libraries For now, missing <a>somewhere</a> (lacking mapMp)
module Generics.RepLib.SYB.Schemes

-- | Apply a transformation everywhere in bottom-up manner
everywhere :: (forall a. Rep a => a -> a) -> (forall a. Rep a => a -> a)

-- | Apply a transformation everywhere in top-down manner
everywhere' :: (forall a. Rep a => a -> a) -> (forall a. Rep a => a -> a)

-- | Variation on everywhere with an extra stop condition
everywhereBut :: GenericQ Bool -> GenericT -> GenericT

-- | Monadic variation on everywhere
everywhereM :: Monad m => GenericM m -> GenericM m

-- | Apply a monadic transformation at least somewhere somewhere ::
--   MonadPlus m =&gt; GenericM m -&gt; GenericM m
--   
--   Summarise all nodes in top-down, left-to-right order
everything :: (r -> r -> r) -> GenericQ r -> GenericQ r

-- | Get a list of all entities that meet a predicate
listify :: Rep r => (r -> Bool) -> GenericQ [r]

-- | Look up a subterm by means of a maybe-typed filter
something :: GenericQ (Maybe u) -> GenericQ (Maybe u)

-- | Bottom-up synthesis of a data structure; 1st argument z is the initial
--   element for the synthesis; 2nd argument o is for reduction of results
--   from subterms; 3rd argument f updates the synthesised data according
--   to the given term
synthesize :: s -> (s -> s -> s) -> GenericQ (s -> s) -> GenericQ s

-- | Compute size of an arbitrary data structure
gsize :: Rep a => a -> Int

-- | Count the number of immediate subterms of the given term
glength :: GenericQ Int

-- | Determine depth of the given term
gdepth :: GenericQ Int

-- | Determine the number of all suitable nodes in a given term
gcount :: GenericQ Bool -> GenericQ Int

-- | Determine the number of all nodes in a given term
gnodecount :: GenericQ Int

-- | Determine the number of nodes of a given type in a given term
gtypecount :: Rep a => a -> GenericQ Int

-- | Find (unambiguously) an immediate subterm of a given type
gfindtype :: (Rep x, Rep y) => x -> Maybe y


-- | A library of type-indexed functions
module Generics.RepLib.Lib

-- | Produce all children of a datastructure with the same type. Note that
--   subtrees is available for all representable types. For those that are
--   not recursive datatypes, subtrees will always return the empty list.
--   But, these trivial instances are convenient to have for the Shrink
--   operation below.
subtrees :: Rep a => a -> [a]

-- | Recursively force the evaluation of the first argument. For example,
--   <tt> deepSeq ( x , y ) z where x = ... y = ... </tt> will evaluate
--   both <tt>x</tt> and <tt>y</tt> then return <tt>z</tt>
deepSeq :: Rep a => a -> b -> b

-- | Force the evaluation of *datatypes* to their normal forms. Other types
--   are left alone and not forced.
rnf :: Rep a => a -> a

-- | Add together all of the <tt>Int</tt>s in a datastructure For example:
--   gsum ( 1 , True, (<a>a</a>, Maybe 3, []) , Nothing) 4
class Rep1 GSumD a => GSum a
gsum :: GSum a => a -> Int

-- | Create a zero element of a type <tt> ( zero :: ((Int, Maybe Int),
--   Float)) ((0, Nothing), 0.0) </tt>
class Rep1 ZeroD a => Zero a
zero :: Zero a => a

-- | Generate elements of a type up to a certain depth
class Rep1 GenerateD a => Generate a
generate :: Generate a => Int -> [a]

-- | enumerate the elements of a type, in DFS order.
class Rep1 EnumerateD a => Enumerate a
enumerate :: Enumerate a => [a]

-- | Given an element, return smaller elements of the same type for
--   example, to automatically find small counterexamples when testing
class Rep1 ShrinkD a => Shrink a
shrink :: Shrink a => a -> [a]

-- | A general version of fold left, use for Fold class below
class Rep1 (LreduceD b) a => Lreduce b a
lreduce :: Lreduce b a => b -> a -> b

-- | A general version of fold right, use for Fold class below
class Rep1 (RreduceD b) a => Rreduce b a
rreduce :: Rreduce b a => a -> b -> b

-- | All of the functions below are defined using instances of the
--   following class
class Fold f
foldRight :: (Fold f, Rep a) => (a -> b -> b) -> f a -> b -> b
foldLeft :: (Fold f, Rep a) => (b -> a -> b) -> b -> f a -> b

-- | Fold a bindary operation left over a datastructure
crush :: (Rep a, Fold t) => (a -> a -> a) -> a -> t a -> a

-- | Multiply all elements together
gproduct :: (Rep a, Num a, Fold t) => t a -> a

-- | Ensure all booleans are true
gand :: Fold t => t Bool -> Bool

-- | Ensure at least one boolean is true
gor :: Fold t => t Bool -> Bool

-- | Convert to list
flatten :: (Rep a, Fold t) => t a -> [a]

-- | Count number of <tt>a</tt>s that appear in the argument
count :: (Rep a, Fold t) => t a -> Int

-- | Compose all functions in the datastructure together
comp :: (Rep a, Fold t) => t (a -> a) -> a -> a

-- | Concatenate all lists in the datastructure together
gconcat :: (Rep a, Fold t) => t [a] -> [a]

-- | Ensure property holds of all data
gall :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool

-- | Ensure property holds of some element
gany :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool

-- | Is an element stored in a datastructure
gelem :: (Rep a, Eq a, Fold t) => a -> t a -> Bool
data GSumD a
GSumD :: (a -> Int) -> GSumD a
gsumD :: GSumD a -> a -> Int
data ZeroD a
ZD :: a -> ZeroD a
zeroD :: ZeroD a -> a
data GenerateD a
GenerateD :: (Int -> [a]) -> GenerateD a
generateD :: GenerateD a -> Int -> [a]
data EnumerateD a
EnumerateD :: [a] -> EnumerateD a
enumerateD :: EnumerateD a -> [a]
data ShrinkD a
ShrinkD :: (a -> [a]) -> ShrinkD a
shrinkD :: ShrinkD a -> a -> [a]
data LreduceD b a
LreduceD :: (b -> a -> b) -> LreduceD b a
lreduceD :: LreduceD b a -> b -> a -> b
data RreduceD b a
RreduceD :: (a -> b -> b) -> RreduceD b a
rreduceD :: RreduceD b a -> a -> b -> b
rnfR :: R a -> a -> a
deepSeqR :: R a -> a -> b -> b
gsumR1 :: R1 GSumD a -> a -> Int
zeroR1 :: R1 ZeroD a -> a
generateR1 :: R1 GenerateD a -> Int -> [a]
enumerateR1 :: R1 EnumerateD a -> [a]
lreduceR1 :: R1 (LreduceD b) a -> b -> a -> b
rreduceR1 :: R1 (RreduceD b) a -> a -> b -> b
instance Fold []
instance Rreduce c a => Rreduce c [a]
instance (Rreduce c a, Rreduce c b) => Rreduce c (a, b)
instance Rreduce b Bool
instance Rreduce b Char
instance Rreduce b ()
instance Rreduce b Int
instance Lreduce c a => Lreduce c [a]
instance (Lreduce c a, Lreduce c b) => Lreduce c (a, b)
instance Lreduce b Bool
instance Lreduce b Char
instance Lreduce b ()
instance Lreduce b Int
instance Lreduce b a => Sat (LreduceD b a)
instance Rreduce b a => Sat (RreduceD b a)
instance (Shrink a, Shrink b) => Shrink (a, b)
instance Shrink ()
instance Shrink Char
instance Shrink a => Shrink [a]
instance Shrink Int
instance Monad M
instance Shrink a => Sat (ShrinkD a)
instance Enumerate a => Sat (EnumerateD a)
instance Generate a => Generate [a]
instance (Generate a, Generate b) => Generate (a, b)
instance Generate ()
instance Generate Double
instance Generate Float
instance Generate Integer
instance Generate Char
instance Generate Int
instance Generate a => Sat (GenerateD a)
instance Zero a => Zero [a]
instance (Zero a, Zero b) => Zero (a, b)
instance Zero Bool
instance Zero ()
instance Zero IOError
instance Zero Double
instance Zero Float
instance Zero Integer
instance (Zero a, Zero b) => Zero (a -> b)
instance Zero Char
instance Zero Int
instance Zero a => Sat (ZeroD a)
instance GSum a => GSum [a]
instance (GSum a, GSum b) => GSum (a, b)
instance GSum Double
instance GSum Char
instance GSum Integer
instance GSum ()
instance GSum Bool
instance GSum Int
instance GSum Float
instance GSum a => Sat (GSumD a)


-- | The module PreludeLib contains generic operations to derive members of
--   the standard prelude classess: Eq, Bounded, Compare, Show (TODO: add
--   Enum and Read)
--   
--   Although these classes may already be automatically derived via the
--   <a>deriving</a> mechanism, this module is included for two reasons:
--   
--   <ul>
--   <li>Deriving only works when datatypes are defined. This library
--   allows instances of these classes to be generated anywhere. For
--   example, suppose some other module contains the definition of the
--   datatype T and exposes all of its constructors, but, frustratingly,
--   does not derive an instance of the Show class.</li>
--   </ul>
--   
--   You could define a Show instance of <tt>T</tt> in your own module with
--   the following code:
--   
--   <pre>
--   import RepLib
--   
--   (repr1 ''T)  -- make the Rep1 instance of T available
--   
--   instance Show T where
--     showsPrec = showsPrecR1 rep1   -- showsPrecR1 is defined in this module
--   </pre>
--   
--   <ul>
--   <li>This library also serves as a model for generic functions that are
--   slight modifications to these prelude operations. For example, if you
--   wanted to define reverse lexicographic ordering or an XML pretty
--   printer for datatypes, you might start here. This library is also a
--   good place to start learning how to define your own generic
--   operations, because the behavior of these operations should match the
--   deriving mechanism specified by Haskell 98.</li>
--   </ul>
module Generics.RepLib.PreludeLib
data EqD a

-- | Polymorphic equality, given an R1 representation
eqR1 :: R1 EqD a -> a -> a -> Bool
data OrdD a

-- | Minimal completion of the Ord class
compareR1 :: R1 OrdD a -> a -> a -> Ordering
data BoundedD a

-- | To generate the Bounded class
minBoundR1 :: R1 BoundedD a -> a

-- | To generate the Bounded class
maxBoundR1 :: R1 BoundedD a -> a
data ShowD a

-- | Minimal completion of the show class
showsPrecR1 :: R1 ShowD a -> Int -> a -> ShowS
instance Show a => Sat (ShowD a)
instance Bounded a => Sat (BoundedD a)
instance Ord a => Sat (OrdD a)
instance Eq a => Sat (EqD a)

module Generics.RepLib.Unify
data Proxy a
type UnifyError = String
type UM n a b = ErrorT UnifyError (State (UnificationState n a)) b
data UnifySubD n a b
UnifySubD :: (Proxy (n, a) -> b -> b -> UM n a ()) -> (n -> a -> b -> b) -> (n -> Proxy a -> b -> Bool) -> UnifySubD n a b
unifyStepD :: UnifySubD n a b -> Proxy (n, a) -> b -> b -> UM n a ()
substD :: UnifySubD n a b -> n -> a -> b -> b
occursCheckD :: UnifySubD n a b -> n -> Proxy a -> b -> Bool
data UConstraint n a
UC :: (UnifySubD n a b) -> b -> b -> UConstraint n a
data UnificationState n a
UState :: [UConstraint n a] -> [(n, a)] -> UnificationState n a
uConstraints :: UnificationState n a -> [UConstraint n a]
uSubst :: UnificationState n a -> [(n, a)]
class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b
unifyStep :: Unify n a b => Proxy (n, a) -> b -> b -> UM n a ()

-- | Generic unifyStep. almost identical to polymorphic equality
unifyStepR1 :: (Eq n, Show n, Show a, Show b, HasVar n a) => R1 (UnifySubD n a) b -> Proxy (n, a) -> b -> b -> UM n a ()
addConstraintsRL1 :: MTup (UnifySubD n a) l -> Proxy (n, a) -> l -> l -> UM n a ()
dequeueConstraint :: UM n a (Maybe (UConstraint n a))
queueConstraint :: UConstraint n a -> UM n a ()
extendSubstitution :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => (n, a) -> UM n a ()
solveUnification :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => [(a, a)] -> Maybe [(n, a)]
solveUnification' :: (HasVar n a, Eq n, Show n, Show a, Show b, Rep1 (UnifySubD n a) b) => Proxy (n, a) -> [(b, b)] -> Maybe [(n, a)]
class HasVar a b
is_var :: HasVar a b => b -> Maybe a
var :: HasVar a b => a -> b
class Subst a t t'
subst :: Subst a t t' => a -> t -> t' -> t'
substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t'
class Occurs n a b
occursCheck :: Occurs n a b => n -> Proxy a -> b -> Bool
occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool
instance [incoherent] (Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a
instance [incoherent] Rep1 (UnifySubD n a) b => Occurs n a b
instance [incoherent] (Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t
instance [incoherent] Rep1 (UnifySubD a t) t' => Subst a t t'
instance [incoherent] (Eq n, Show n, Show a, HasVar n a, Rep1 (UnifySubD n a) a) => Unify n a a
instance [incoherent] (Eq n, Show n, Show a, Show b, HasVar n a, Rep1 (UnifySubD n a) b) => Unify n a b
instance [incoherent] (Unify n a b, Subst n a b, Occurs n a b) => Sat (UnifySubD n a b)


module Generics.RepLib


-- | Generic implementation of name binding functions, based on the library
--   RepLib. This version uses a nominal representation of binding
--   structure.
--   
--   DISCLAIMER: this module probably contains bugs and is noticeably
--   slower than <a>Generics.RepLib.Bind.LocallyNameless</a>. At this point
--   we recommend it only for the curious or intrepid.
--   
--   Datatypes with binding defined using the <a>Name</a> and <a>Bind</a>
--   types. Important classes are <a>Alpha</a> -- the class of types that
--   include binders. These classes are generic, and default
--   implementations exist for all representable types. This file also
--   defines a third generic class, <a>Subst</a> -- for subtitution
--   functions.
module Generics.RepLib.Bind.Nominal

-- | Names are things that get bound. The usual protocol is for names to
--   get created by some automatic process, that preserves alpha renaming
--   under operations over Binding instances.
data Name a

-- | Type of a binding. Morally, the type a should be in the class
--   <tt>Pattern</tt> and the type b should be in the class <a>Alpha</a>.
--   The Pattern class contains the constructor and a safe destructor for
--   these types. We can Bind an <a>a</a> object in a <a>b</a> object if we
--   can create <a>fresh</a> a objects, and Names can be swapped in
--   <a>b</a> objects. Often <a>a</a> is Name but that need not be the
--   case.
data Bind a b

-- | An annotation is a <tt>hole</tt> in a pattern where variables can be
--   used, but not bound. For example patterns may include type
--   annotations, and those annotations can reference variables without
--   binding them. Annotations do nothing special when they appear
--   elsewhere in terms
newtype Annot a
Annot :: a -> Annot a

-- | Rebinding is for telescopes --- i.e. to support patterns that also
--   bind variables that appear later
data Rebind a b
integer2Name :: Rep a => Integer -> Name a
string2Name :: Rep a => String -> Name a
name2Integer :: Name a -> Integer

-- | Get the string part of a <a>Name</a>.
name2String :: Name a -> String
makeName :: Rep a => String -> Integer -> Name a
name1 :: Rep a => Name a
name2 :: Rep a => Name a
name3 :: Rep a => Name a
name4 :: Rep a => Name a
name5 :: Rep a => Name a
name6 :: Rep a => Name a
name7 :: Rep a => Name a
name8 :: Rep a => Name a
name9 :: Rep a => Name a
name10 :: Rep a => Name a

-- | The Alpha class is for all terms that may contain binders The
--   <a>Rep1</a> class constraint means that we can only make instances of
--   this class for types that have generic representations. (Derive these
--   using TH and RepLib.)
class Rep1 (AlphaD) a => Alpha a
aeq' :: Alpha a => AlphaCtx -> a -> a -> Bool
swapall' :: Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' :: Alpha a => AlphaCtx -> Perm AnyName -> a -> a
fv' :: Alpha a => AlphaCtx -> a -> Set AnyName
binders' :: Alpha a => AlphaCtx -> a -> [AnyName]
match' :: Alpha a => AlphaCtx -> a -> a -> Maybe (Perm AnyName)
freshen' :: (Alpha a, Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
lfreshen' :: (Alpha a, LFresh m) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b

-- | The method <a>swaps</a> applys a permutation to all free variables in
--   the term.
swaps :: Alpha a => Perm AnyName -> a -> a

-- | List the binding variables in a pattern
binders :: (Rep b, Alpha b) => b -> [AnyName]

-- | Set of variables that occur freely in annotations (not binding)
patfv :: (Rep a, Alpha b) => b -> Set (Name a)

-- | calculate the free variables of the term
fv :: (Rep b, Alpha a) => a -> Set (Name b)
aeq :: Alpha a => a -> a -> Bool

-- | Smart constructor for binders
bind :: (Alpha b, Alpha c) => b -> c -> Bind b c

-- | A destructor for binders that does not guarantee fresh names for the
--   binders.
unsafeUnBind :: Bind a b -> (a, b)

-- | A monad <a>m</a> supports the <a>fresh</a> operation if it can
--   generate a new unique names.
class (Monad m, HasNext m) => Fresh m
fresh :: Fresh m => Name a -> m (Name a)

-- | An object of type <a>b</a> can be freshened if a new copy of <a>b</a>
--   can be produced where all old *binding* Names in <a>b</a> are replaced
--   with new fresh Names, and the permutation reports which Names were
--   swapped by others.
freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)

-- | Unbind is the destructor of a binding. It ensures that the names in
--   the binding b are fresh.
unbind :: (Alpha b, Fresh m, Alpha c) => Bind b c -> m (b, c)

-- | Destruct two bindings simultanously, if they match, using the same
--   list of fresh names
unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))

-- | A monad <a>m</a> supports the nextInteger operation if it can generate
--   new fresh integers
class Monad m => HasNext m
nextInteger :: HasNext m => m Integer
resetNext :: HasNext m => Integer -> m ()

-- | Locally fresh monad This is the class of monads that support freshness
--   in an (implicit) local scope. Names drawn are fresh for this
--   particular scope, but not globally fresh. This class has a basic
--   instance based on the reader monad.
class Monad m => LFresh m
lfresh :: (LFresh m, Rep a) => Name a -> m (Name a)
avoid :: LFresh m => [AnyName] -> m a -> m a

-- | <a>Locally</a> freshen an object
lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m b

-- | Destruct a binding in the LFresh monad.
lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)
lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))

-- | Constructor for binding in patterns
rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b

-- | destructor for binding patterns, the external names should have
--   already been freshen'ed. We swap the internal names so that they use
--   the external names
reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
class Rep1 (SubstD b) a => Subst b a
isvar :: Subst b a => a -> Maybe (Name b, b -> a)
lsubst :: (Subst b a, LFresh m) => Name b -> b -> a -> m a
lsubsts :: (Subst b a, LFresh m) => [Name b] -> [b] -> a -> m a

-- | Many of the operations in the <a>Alpha</a> class take an
--   <a>AlphaCtx</a>: stored information about the iteration as it
--   progresses. This type is abstract, as classes that override these
--   operations should just pass the context on.
data AlphaCtx
matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
rName :: Rep a[aqf1] => R (Name a[aqf1])
rBind :: (Rep a[aqeZ], Rep b[aqf0]) => R (Bind a[aqeZ] b[aqf0])
rRebind :: (Rep a[aqeV], Rep b[aqeW]) => R (Rebind a[aqeV] b[aqeW])
rAnnot :: Rep a[aqeX] => R (Annot a[aqeX])
instance Subst Exp Exp
instance Alpha Exp
instance (Sat (ctx[arvn] (Name Exp)), Sat (ctx[arvn] Exp), Sat (ctx[arvn] (Bind (Name Exp) Exp))) => Rep1 ctx[arvn] Exp
instance Rep Exp
instance Show Exp
instance Show AlphaCtx
instance Eq AlphaCtx
instance Read AlphaCtx
instance Subst c a => Subst c (Annot a)
instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b)
instance (Subst c a, Alpha a, Subst c b, Alpha b) => Subst c (Bind a b)
instance Rep a => Subst b (Name a)
instance Rep a => Subst b (R a)
instance (Subst c a, Subst c b) => Subst c (Either a b)
instance Subst c a => Subst c (Maybe a)
instance Subst c a => Subst c [a]
instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f)
instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e)
instance (Subst c a, Subst c b, Subst c d) => Subst c (a, b, d)
instance (Subst c a, Subst c b) => Subst c (a, b)
instance Subst b Double
instance Subst b Float
instance Subst b Integer
instance Subst b Char
instance Subst b ()
instance Subst b Bool
instance Subst b Int
instance Subst c AnyName
instance Subst b a => Sat (SubstD b a)
instance LFresh (Reader Integer)
instance HasNext m => Fresh m
instance Rep a => Alpha (R a)
instance (Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e)
instance (Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d)
instance (Alpha a, Alpha b, Alpha c) => Alpha (a, b, c)
instance (Alpha a, Alpha b) => Alpha (a, b)
instance (Alpha a, Alpha b) => Alpha (Either a b)
instance Alpha a => Alpha (Maybe a)
instance Alpha Char
instance Alpha Double
instance Alpha Integer
instance Alpha Int
instance Alpha a => Alpha [a]
instance Alpha ()
instance Alpha Float
instance Alpha Bool
instance (Eq a, Alpha a) => Alpha (Annot a)
instance (Alpha a, Alpha b) => Alpha (Rebind a b)
instance (Alpha a, Alpha b) => Alpha (Bind a b)
instance Alpha AnyName
instance Rep a => Alpha (Name a)
instance Alpha a => Sat (AlphaD a)
instance (Alpha a, Show a, Show b) => Show (Rebind a b)
instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b)
instance Show a => Show (Annot a)
instance (Show a, Show b) => Show (Bind a b)
instance Show (Name a)
instance Ord AnyName
instance Eq AnyName
instance Show AnyName
instance Rep1 ctx[aqvK] AnyName
instance Rep AnyName
instance (Rep a[aqeZ], Rep b[aqf0], Sat (ctx[aqpv] a[aqeZ]), Sat (ctx[aqpv] b[aqf0])) => Rep1 ctx[aqpv] (Bind a[aqeZ] b[aqf0])
instance (Rep a[aqeZ], Rep b[aqf0]) => Rep (Bind a[aqeZ] b[aqf0])
instance (Rep a[aqf1], Sat (ctx[aqpi] (R a[aqf1])), Sat (ctx[aqpi] (String, Integer))) => Rep1 ctx[aqpi] (Name a[aqf1])
instance Rep a[aqf1] => Rep (Name a[aqf1])
instance (Rep a[aqeX], Sat (ctx[aqpa] a[aqeX])) => Rep1 ctx[aqpa] (Annot a[aqeX])
instance Rep a[aqeX] => Rep (Annot a[aqeX])
instance (Rep a[aqeV], Rep b[aqeW], Sat (ctx[aqoX] a[aqeV]), Sat (ctx[aqoX] (Bind [AnyName] b[aqeW]))) => Rep1 ctx[aqoX] (Rebind a[aqeV] b[aqeW])
instance (Rep a[aqeV], Rep b[aqeW]) => Rep (Rebind a[aqeV] b[aqeW])
instance Read a => Read (Annot a)
instance Eq a => Eq (Annot a)
instance Eq (Name a)
instance Ord (Name a)
instance Rep a[a2Jp] => Rep1 ctx[aqdM] (R a[a2Jp])
instance Rep a[a2Jp] => Rep (R a[a2Jp])


-- | A generic implementation of name binding functions using a locally
--   nameless representation. Datatypes with binding can be defined using
--   the <a>Name</a> and <a>Bind</a> types. Expressive patterns for binding
--   come from the <a>Annot</a> and <a>Rebind</a> types.
--   
--   Important classes are:
--   
--   <ul>
--   <li><a>Alpha</a> -- the class of types and patterns that include
--   binders,</li>
--   <li><a>Subst</a> -- for subtitution functions.</li>
--   </ul>
--   
--   Name generation is controlled via monads which implement the
--   <a>Fresh</a> and <a>LFresh</a> classes.
module Generics.RepLib.Bind.LocallyNameless

-- | <a>Name</a>s are things that get bound. This type is intentionally
--   abstract; to create a <a>Name</a> you can use <a>string2Name</a> or
--   <a>integer2Name</a>. The type parameter is a tag, or <i>sort</i>,
--   which tells us what sorts of things this name may stand for. The sort
--   must be an instance of the <a>Rep</a> type class.
data Name a

-- | A name with a hidden (existentially quantified) sort.
data AnyName
AnyName :: (Name a) -> AnyName

-- | The type of a binding. We can <a>Bind</a> an <tt>a</tt> object in a
--   <tt>b</tt> object if we can create "fresh" <tt>a</tt> objects, and
--   <tt>a</tt> objects can occur unbound in <tt>b</tt> objects. Often
--   <tt>a</tt> is <a>Name</a> but that need not be the case.
--   
--   Like <a>Name</a>, <a>Bind</a> is also abstract. You can create
--   bindings using <a>bind</a> and take them apart with <a>unbind</a> and
--   friends.
data Bind a b

-- | An annotation is a "hole" in a pattern where variables can be used,
--   but not bound. For example, patterns may include type annotations, and
--   those annotations can reference variables without binding them.
--   Annotations do nothing special when they appear elsewhere in terms.
newtype Annot a
Annot :: a -> Annot a

-- | <a>Rebind</a> supports "telescopes" --- that is, patterns where bound
--   variables appear in multiple subterms.
data Rebind a b

-- | Create a <a>Name</a> from an <a>Integer</a>.
integer2Name :: Rep a => Integer -> Name a

-- | Create a <a>Name</a> from a <a>String</a>.
string2Name :: Rep a => String -> Name a

-- | Create a <a>Name</a> from a <tt>String</tt> and an <tt>Integer</tt>
--   index.
makeName :: Rep a => String -> Integer -> Name a

-- | Get the integer index of a <a>Name</a>.
name2Integer :: Name a -> Integer

-- | Get the string part of a <a>Name</a>.
name2String :: Name a -> String

-- | Get the integer index of an <a>AnyName</a>.
anyName2Integer :: AnyName -> Integer

-- | Get the string part of an <a>AnyName</a>.
anyName2String :: AnyName -> String
name1 :: Rep a => Name a
name2 :: Rep a => Name a
name3 :: Rep a => Name a
name4 :: Rep a => Name a
name5 :: Rep a => Name a
name6 :: Rep a => Name a
name7 :: Rep a => Name a
name8 :: Rep a => Name a
name9 :: Rep a => Name a
name10 :: Rep a => Name a

-- | The <a>Alpha</a> type class is for types which may contain names. The
--   <a>Rep1</a> constraint means that we can only make instances of this
--   class for types that have generic representations (which can be
--   automatically derived by RepLib.)
--   
--   Note that the methods of <a>Alpha</a> should never be called directly!
--   Instead, use other methods provided by this module which are defined
--   in terms of <a>Alpha</a> methods. (The only reason they are exported
--   is to make them available to automatically-generated code.)
--   
--   Most of the time, the default definitions of these methods will
--   suffice, so you can make an instance for your data type by simply
--   declaring
--   
--   <pre>
--   instance Alpha MyType
--   </pre>
class (Show a, Rep1 AlphaD a) => Alpha a
swaps' :: Alpha a => AlphaCtx -> Perm AnyName -> a -> a
fv' :: Alpha a => AlphaCtx -> a -> Set AnyName
lfreshen' :: (Alpha a, LFresh m) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
freshen' :: (Alpha a, Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
match' :: Alpha a => AlphaCtx -> a -> a -> Maybe (Perm AnyName)
close :: (Alpha a, Alpha b) => AlphaCtx -> b -> a -> a
open :: (Alpha a, Alpha b) => AlphaCtx -> b -> a -> a
nthpatrec :: Alpha a => a -> Integer -> (Integer, Maybe AnyName)
findpatrec :: Alpha a => a -> AnyName -> (Integer, Bool)

-- | Apply a permutation to a term.
swaps :: Alpha a => Perm AnyName -> a -> a

-- | Apply a permutation to the annotations in a pattern. Binding names are
--   left alone by the permutation.
swapsAnnots :: Alpha a => Perm AnyName -> a -> a

-- | Apply a permutation to the binding variables in a pattern. Annotations
--   are left alone by the permutation.
swapsBinders :: Alpha a => Perm AnyName -> a -> a

-- | Compare two data structures and produce a permutation of their
--   <a>Name</a>s that will make them alpha-equivalent to each other
--   (<a>Name</a>s that appear in annotations must match exactly). Return
--   <a>Nothing</a> if no such renaming is possible. Note that two terms
--   are alpha-equivalent if the empty permutation is returned.
match :: Alpha a => a -> a -> Maybe (Perm AnyName)

-- | Compare two patterns, ignoring the names of binders, and produce a
--   permutation of their annotations to make them alpha-equivalent to
--   eachother. Return <a>Nothing</a> if no such renaming is possible.
matchAnnots :: Alpha a => a -> a -> Maybe (Perm AnyName)

-- | Compare two patterns for equality and produce a permutation of their
--   binding <tt>Names</tt> to make them alpha-equivalent to each other
--   (<a>Name</a>s that appear in annotations must match exactly). Return
--   <a>Nothing</a> if no such renaming is possible.
matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName)

-- | Calculate the free variables of a particular sort contained in a term.
fv :: (Rep b, Alpha a) => a -> Set (Name b)

-- | List variables of a particular sort that occur freely in annotations
--   (not bindings).
patfv :: (Rep a, Alpha b) => b -> Set (Name a)

-- | List all the binding variables (of a particular sort) in a pattern.
binders :: (Rep a, Alpha b) => b -> Set (Name a)

-- | Determine alpha-equivalence.
aeq :: Alpha a => a -> a -> Bool

-- | Determine (alpha-)equivalence of patterns
aeqBinders :: Alpha a => a -> a -> Bool

-- | A smart constructor for binders, also sometimes known as "close".
bind :: (Alpha b, Alpha c) => b -> c -> Bind b c

-- | A destructor for binders that does <i>not</i> guarantee fresh names
--   for the binders.
unsafeUnBind :: (Alpha a, Alpha b) => Bind a b -> (a, b)

-- | Type class for monads which can generate new globally unique
--   <a>Name</a>s based on a given <a>Name</a>.
class Monad m => Fresh m
fresh :: Fresh m => Name a -> m (Name a)

-- | Freshen a term by replacing all old <i>binding</i> <a>Name</a>s with
--   new fresh <a>Name</a>s, returning a new term and a <tt><a>Perm</a>
--   <a>Name</a></tt> specifying how <a>Name</a>s were replaced.
freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)

-- | Unbind (also known as "open") is the destructor for bindings. It
--   ensures that the names in the binding are fresh.
unbind :: (Fresh m, Alpha b, Alpha c) => Bind b c -> m (b, c)

-- | Unbind two terms with the same fresh names, provided the binders
--   match.
unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))

-- | Type class for contexts which can generate new globally fresh
--   integers.
class HasNext m
nextInteger :: HasNext m => m Integer
resetNext :: HasNext m => Integer -> m ()

-- | This is the class of monads that support freshness in an (implicit)
--   local scope. Generated names are fresh for the current local scope,
--   but not globally fresh. This class has a basic instance based on the
--   reader monad.
class Monad m => LFresh m
lfresh :: (LFresh m, Rep a) => Name a -> m (Name a)
avoid :: LFresh m => [AnyName] -> m a -> m a

-- | "Locally" freshen a term. TODO: explain this type signature a bit
--   better.
lfreshen :: (Alpha a, LFresh m) => a -> (a -> Perm AnyName -> m b) -> m b

-- | Destruct a binding in an <a>LFresh</a> monad.
lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m c

-- | Unbind two terms with the same fresh names, provided the binders
--   match.
lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> (Maybe (b, c, d) -> m e) -> m e

-- | Unbind three terms with the same fresh names, provided the binders
--   match.
lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> (Maybe (b, c, d, e) -> m f) -> m f

-- | Constructor for binding in patterns.
rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b

-- | destructor for binding patterns, the names should have already been
--   freshened.
reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)

-- | The <a>Subst</a> class governs capture-avoiding substitution. To
--   derive this class, you only need to indicate where the variables are
--   in the data type, by overriding the method <a>isvar</a>.
class Rep1 (SubstD b) a => Subst b a
isvar :: Subst b a => a -> Maybe (Name b, b -> a)
subst :: Subst b a => Name b -> b -> a -> a
substs :: Subst b a => [Name b] -> [b] -> a -> a
abs_swaps :: t -> t1 -> t2 -> t2
abs_fv :: t -> t1 -> Set a
abs_freshen :: Monad m => t -> t1 -> m (t1, Perm a)
abs_match :: Eq a => t -> a -> a -> Maybe (Perm a1)
abs_nthpatrec :: t -> t1 -> (t1, Maybe a)
abs_findpatrec :: Num a => t -> t1 -> (a, Bool)
abs_close :: t -> t1 -> t2 -> t2
abs_open :: t -> t1 -> t2 -> t2

-- | Match returns a <a>permutation ordering</a>. Either the terms are
--   known to be LT or GT, or there is some permutation that can make them
--   equal to eachother data POrdering = PLT | PEq (Perm AnyName) | PGT
--   
--   Many of the operations in the <a>Alpha</a> class take an
--   <a>AlphaCtx</a>: stored information about the iteration as it
--   progresses. This type is abstract, as classes that override these
--   operations should just pass the context on.
data AlphaCtx
matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
rName :: Rep a[aKgL] => R (Name a[aKgL])
rBind :: (Rep a[aKgI], Rep b[aKgJ]) => R (Bind a[aKgI] b[aKgJ])
rRebind :: (Rep a[aKgD], Rep b[aKgE]) => R (Rebind a[aKgD] b[aKgE])
rAnnot :: Rep a[aKgF] => R (Annot a[aKgF])
instance Subst Exp Exp
instance Alpha Exp
instance (Sat (ctx[aLzp] (Name Exp)), Sat (ctx[aLzp] Exp), Sat (ctx[aLzp] (Bind (Name Exp) Exp))) => Rep1 ctx[aLzp] Exp
instance Rep Exp
instance Show Exp
instance Show Mode
instance Eq Mode
instance Read Mode
instance Subst c a => Subst c (Annot a)
instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b)
instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
instance (Subst c a, Subst c b) => Subst c (Either a b)
instance Subst c a => Subst c (Maybe a)
instance Subst c a => Subst c [a]
instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f)
instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e)
instance (Subst c a, Subst c b, Subst c d) => Subst c (a, b, d)
instance (Subst c a, Subst c b) => Subst c (a, b)
instance Rep a => Subst b (Name a)
instance Rep a => Subst b (R a)
instance Subst b AnyName
instance Subst b Double
instance Subst b Float
instance Subst b Integer
instance Subst b Char
instance Subst b ()
instance Subst b Bool
instance Subst b Int
instance Subst b a => Sat (SubstD b a)
instance LFresh (Reader (Set AnyName))
instance LFresh (Reader Integer)
instance (Monad m, HasNext m) => Fresh m
instance (Show a, Show b) => Show (Rebind a b)
instance (Alpha a, Alpha b, Eq b) => Eq (Rebind a b)
instance (Show a, Show b) => Show (Bind a b)
instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b)
instance Rep a => Alpha (R a)
instance (Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e)
instance (Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d)
instance (Alpha a, Alpha b, Alpha c) => Alpha (a, b, c)
instance (Alpha a, Alpha b) => Alpha (a, b)
instance (Alpha a, Alpha b) => Alpha (Either a b)
instance Alpha a => Alpha (Maybe a)
instance Alpha Char
instance Alpha Double
instance Alpha Integer
instance Alpha Int
instance Alpha a => Alpha [a]
instance Alpha ()
instance Alpha Float
instance Alpha Bool
instance Alpha a => Alpha (Annot a)
instance (Alpha a, Alpha b) => Alpha (Rebind a b)
instance (Alpha a, Alpha b) => Alpha (Bind a b)
instance Alpha AnyName
instance Rep a => Alpha (Name a)
instance Alpha a => Sat (AlphaD a)
instance Show (Name a)
instance Ord AnyName
instance Eq AnyName
instance Show AnyName
instance Rep1 ctx[aKum] AnyName
instance Rep AnyName
instance (Rep a[aKgI], Rep b[aKgJ], Sat (ctx[aKnS] a[aKgI]), Sat (ctx[aKnS] b[aKgJ])) => Rep1 ctx[aKnS] (Bind a[aKgI] b[aKgJ])
instance (Rep a[aKgI], Rep b[aKgJ]) => Rep (Bind a[aKgI] b[aKgJ])
instance (Rep a[aKgL], Sat (ctx[aKnq] (R a[aKgL])), Sat (ctx[aKnq] (String, Integer)), Sat (ctx[aKnq] Integer)) => Rep1 ctx[aKnq] (Name a[aKgL])
instance Rep a[aKgL] => Rep (Name a[aKgL])
instance (Rep a[aKgF], Sat (ctx[aKni] a[aKgF])) => Rep1 ctx[aKni] (Annot a[aKgF])
instance Rep a[aKgF] => Rep (Annot a[aKgF])
instance (Rep a[aKgD], Rep b[aKgE], Sat (ctx[aKn5] a[aKgD]), Sat (ctx[aKn5] b[aKgE])) => Rep1 ctx[aKn5] (Rebind a[aKgD] b[aKgE])
instance (Rep a[aKgD], Rep b[aKgE]) => Rep (Rebind a[aKgD] b[aKgE])
instance Show a => Show (Annot a)
instance Read a => Read (Annot a)
instance Eq a => Eq (Annot a)
instance Eq (Name a)
instance Ord (Name a)
instance Rep a[a2Jp] => Rep1 ctx[aKfo] (R a[a2Jp])
instance Rep a[a2Jp] => Rep (R a[a2Jp])