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


-- | Compositional Data Types
--   
--   Based on Wouter Swierstra's Functional Pearl <i>Data types à la
--   carte</i> (Journal of Functional Programming, 18(4):423-436, 2008),
--   this package provides a framework for defining recursive data types in
--   a compositional manner. The fundamental idea of compositional data
--   types is to separate the signature of a data type from the fixed point
--   construction that produces its recursive structure. By allowing to
--   compose and decompose signatures, <i>compositional data types</i>
--   enable to combine data types in a flexible way. The key point of
--   Wouter Swierstra's original work is to define functions on
--   <i>compositional data types</i> in a compositional manner as well by
--   leveraging Haskell's type class machinery.
--   
--   Building on that foundation, this library provides additional
--   extensions and (run-time) optimisations which makes compositional data
--   types usable for practical implementations. In particular, it provides
--   an excellent framework for manipulating and analysing abstract syntax
--   trees in a type-safe manner. Thus, it is perfectly suited for
--   programming language implementations, especially, in an environment
--   consisting of a family of tightly interwoven <i>domain-specific
--   languages</i>.
--   
--   In concrete terms, this package provides the following features:
--   
--   <ul>
--   <li>Compositional data types in the style of Wouter Swierstra's
--   Functional Pearl <i>Data types à la carte</i>.</li>
--   <li>Modular definition of function on compositional data types through
--   catamorphisms and anamorphisms as well as more structured recursion
--   schemes such as primitive recursion and co-recursion, and
--   course-of-value iteration and co-iteration.</li>
--   <li>Support for monadic computations via monadic variants of all
--   recursion schemes.</li>
--   <li>Support of a succinct programming style over compositional data
--   types via generic programming combinators that allow various forms of
--   generic transformations and generic queries.</li>
--   <li>Generalisation of compositional data types (terms) to
--   compositional data types "with holes" (contexts). This allows flexible
--   reuse of a wide variety of catamorphisms (called <i>term
--   homomorphisms</i>) as well as an efficient composition of them.</li>
--   <li>Operations on signatures, for example, to add and remove
--   annotations of abstract syntax trees. This includes combinators to
--   propagate annotations fully automatically through certain term
--   homomorphisms.</li>
--   <li>Optimisation of the implementation of recursion schemes. This
--   includes <i>short-cut fusion</i> style optimisation rules which yield
--   a performance boost of up to factor six.</li>
--   <li>Efficient implementation of catamorphisms on non-polynomial
--   signatures that contain function types. This allows to represent
--   <i>higher-order abstract syntax</i> with compositional data
--   types.</li>
--   <li>Automatic derivation of instances of all relevant type classes for
--   using compositional data types via <i>Template Haskell</i>. This
--   includes instances of <a>Prelude.Eq</a>, <a>Prelude.Ord</a> and
--   <a>Prelude.Show</a> that are derived via instances for functorial
--   variants of them. Additionally, also <i>smart constructors</i>, which
--   allow to easily construct inhabitants of compositional data types, are
--   automatically generated.</li>
--   <li><i>Mutually recursive data types</i>. All of the above is also
--   lifted to families of mutually recursive data types.</li>
--   </ul>
--   
--   For examples illustrating the use of compositional data types, consult
--   <a>Data.Comp</a> resp. <a>Data.Comp.Multi</a> for mutually recursive
--   data types.
@package compdata
@version 0.1


-- | This module defines higher-order functors (Johann, Ghani, POPL '08),
--   i.e. endofunctors on the category of endofunctors.
module Data.Comp.Multi.Functor

-- | This class represents higher-order functors (Johann, Ghani, POPL '08)
--   which are endofunctors on the category of endofunctors.
class HFunctor h
hfmap :: HFunctor h => (f :-> g) -> h f :-> h g

-- | This type represents natural transformations.
type :-> f g = forall i. f i -> g i

-- | This type represents co-cones from <tt>f</tt> to <tt>a</tt>. <tt>f
--   :=&gt; a</tt> is isomorphic to f :-&gt; K a
type :=> f a = forall i. f i -> a
type NatM m f g = forall i. f i -> m (g i)

-- | The identity Functor.
data I a
I :: a -> I a
unI :: I a -> a

-- | The parametrised constant functor.
data K a b
K :: a -> K a b
unK :: K a b -> a
data A f
A :: f i -> A f
unA :: A f -> f i

-- | This data type denotes the composition of two functor families.
data (:.:) f g e t
Comp :: f -> (g e) -> t -> :.: f g e t
instance [incoherent] Ord a => Ord (K a i)
instance [incoherent] Eq a => Eq (K a i)
instance [incoherent] Functor (K a)


-- | This module defines higher-order exponential functors.
module Data.Comp.Multi.ExpFunctor

-- | Higher-order exponential functors are higher-order functors that may
--   be both covariant (as ordinary higher-order functors) and
--   contravariant.
class HExpFunctor f
hxmap :: HExpFunctor f => (a :-> b) -> (b :-> a) -> f a :-> f b


-- | This module defines higher-order foldable functors.
module Data.Comp.Multi.Foldable

-- | Higher-order functors that can be folded.
--   
--   Minimal complete definition: <a>hfoldMap</a> or <a>hfoldr</a>.
class HFunctor h => HFoldable h
hfold :: (HFoldable h, Monoid m) => h (K m) :=> m
hfoldMap :: (HFoldable h, Monoid m) => (a :=> m) -> h a :=> m
hfoldr :: HFoldable h => (a :=> (b -> b)) -> b -> h a :=> b
hfoldl :: HFoldable h => (b -> a :=> b) -> b -> h a :=> b
hfoldr1 :: HFoldable h => (a -> a -> a) -> h (K a) :=> a
hfoldl1 :: HFoldable h => (a -> a -> a) -> h (K a) :=> a
kfoldr :: HFoldable f => (a -> b -> b) -> b -> f (K a) :=> b
kfoldl :: HFoldable f => (b -> a -> b) -> b -> f (K a) :=> b
htoList :: HFoldable f => f a :=> [A a]


-- | This module defines higher-order traversable functors.
module Data.Comp.Multi.Traversable
class HFoldable t => HTraversable t
hmapM :: (HTraversable t, Monad m) => NatM m a b -> NatM m (t a) (t b)
htraverse :: (HTraversable t, Applicative f) => NatM f a b -> NatM f (t a) (t b)


-- | This module defines the central notion of mutual recursive (or,
--   higher-order) <i>terms</i> and its generalisation to (higher-order)
--   contexts. All definitions are generalised versions of those in
--   <a>Data.Comp.Term</a>.
module Data.Comp.Multi.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes. The first type parameter is
--   supposed to be one of the phantom types <a>HHole</a> and
--   <a>HNoHole</a>. The second parameter is the signature of the context.
--   The third parameter is the type family of the holes. The last
--   parameter is the index/label.
data HCxt h f a i
HTerm :: f (HCxt h f a) i -> HCxt h f a i
HHole :: a i -> HCxt HHole f a i

-- | Phantom type that signals that a <a>HCxt</a> might contain holes.
data HHole

-- | Phantom type that signals that a <a>HCxt</a> does not contain holes.
data HNoHole

-- | A context might contain holes.
type HContext = HCxt HHole

-- | Phantom type family used to define <a>HTerm</a>.
data HNothing :: * -> *

-- | A (higher-order) term is a context with no holes.
type HTerm f = HCxt HNoHole f HNothing
type HConst f :: ((* -> *) -> * -> *) = f (K ())

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the functor f.
constHTerm :: HFunctor f => HConst f :-> HTerm f

-- | This function unravels the given term at the topmost layer.
unHTerm :: HTerm f t -> f (HTerm f) t
toHCxt :: HTerm f i -> HContext f a i
simpHCxt :: HFunctor f => f a i -> HContext f a i
instance [incoherent] HFunctor f => HFunctor (HCxt h f)
instance [incoherent] Ord (HNothing i)
instance [incoherent] Eq (HNothing i)
instance [incoherent] Show (HNothing i)


-- | Exponential functors, see
--   <a>http://comonad.com/reader/2008/rotten-bananas/</a>.
module Data.Comp.ExpFunctor

-- | Exponential functors are functors that may be both covariant (as
--   ordinary functors) and contravariant.
class ExpFunctor f
xmap :: ExpFunctor f => (a -> b) -> (b -> a) -> f a -> f b


-- | This module provides operators on functors.
module Data.Comp.Ops

-- | Formal sum of signatures (functors).
data (:+:) f g e
Inl :: (f e) -> :+: f g e
Inr :: (g e) -> :+: f g e

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class :<: sub sup
inj :: :<: sub sup => sub a -> sup a
proj :: :<: sub sup => sup a -> Maybe (sub a)

-- | Formal product of signatures (functors).
data (:*:) f g a
(:*:) :: f a -> g a -> :*: f g a
ffst :: (f :*: g) a -> f a
fsnd :: (f :*: g) a -> g a

-- | This data type adds a constant product to a signature.
data (:&:) f a e
(:&:) :: f e -> a -> :&: f a e

-- | This class defines how to distribute a product over a sum of
--   signatures.
class DistProd s p s' | s' -> s, s' -> p
injectP :: DistProd s p s' => p -> s a -> s' a
projectP :: DistProd s p s' => s' a -> (s a, p)
class RemoveP s s' | s -> s'
removeP :: RemoveP s s' => s a -> s' a
instance [incoherent] DistProd s p s' => DistProd (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistProd f p (f :&: p)
instance [incoherent] RemoveP (f :&: p) f
instance [incoherent] RemoveP s s' => RemoveP ((f :&: p) :+: s) (f :+: s')
instance [incoherent] ExpFunctor f => ExpFunctor (f :&: a)
instance [incoherent] Traversable f => Traversable (f :&: a)
instance [incoherent] Foldable f => Foldable (f :&: a)
instance [incoherent] Functor f => Functor (f :&: a)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (ExpFunctor f, ExpFunctor g) => ExpFunctor (f :+: g)
instance [incoherent] (Traversable f, Traversable g) => Traversable (f :+: g)
instance [incoherent] (Foldable f, Foldable g) => Foldable (f :+: g)
instance [incoherent] (Functor f, Functor g) => Functor (f :+: g)


-- | This module defines the notion of algebras and catamorphisms, and
--   their generalizations to e.g. monadic versions and other (co)recursion
--   schemes. All definitions are generalised versions of those in
--   <a>Data.Comp.Algebra</a>.
module Data.Comp.Multi.Algebra
type HAlg f e = f e :-> e
hfree :: HFunctor f => HAlg f b -> (a :-> b) -> HCxt h f a :-> b
hcata :: HFunctor f => HAlg f a -> HTerm f :-> a
hcata' :: HFunctor f => HAlg f e -> HCxt h f e :-> e

-- | This function applies a whole context into another context.
appHCxt :: HFunctor f => HContext f (HCxt h f a) :-> HCxt h f a
type HAlgM m f e = NatM m (f e) e
hfreeM :: (HTraversable f, Monad m) => HAlgM m f b -> NatM m a b -> NatM m (HCxt h f a) b

-- | This is a monadic version of <a>hcata</a>.
hcataM :: (HTraversable f, Monad m) => HAlgM m f a -> NatM m (HTerm f) a
hcataM' :: (Monad m, HTraversable f) => HAlgM m f a -> NatM m (HCxt h f a) a

-- | This function lifts a many-sorted algebra to a monadic domain.
liftMHAlg :: (Monad m, HTraversable f) => HAlg f I -> HAlg f m

-- | This type represents context function.
type HCxtFun f g = forall a h. HCxt h f a :-> HCxt h g a

-- | This type represents uniform signature function specification.
type HSigFun f g = forall a. f a :-> g a

-- | This type represents a term algebra.
type HTermHom f g = HSigFun f (HContext g)

-- | This function applies the given term homomorphism to a term/context.
appHTermHom :: (HFunctor f, HFunctor g) => HTermHom f g -> HCxtFun f g

-- | This function composes two term algebras.
compHTermHom :: (HFunctor g, HFunctor h) => HTermHom g h -> HTermHom f g -> HTermHom f h

-- | This function applies a signature function to the given context.
appHSigFun :: (HFunctor f, HFunctor g) => HSigFun f g -> HCxtFun f g

-- | This function composes two signature functions.
compHSigFun :: HSigFun g h -> HSigFun f g -> HSigFun f h

-- | Lifts the given signature function to the canonical term homomorphism.
htermHom :: HFunctor g => HSigFun f g -> HTermHom f g

-- | This function composes a term algebra with an algebra.
compHAlg :: HFunctor g => HAlg g a -> HTermHom f g -> HAlg f a

-- | This type represents monadic context function.
type HCxtFunM m f g = forall a h. NatM m (HCxt h f a) (HCxt h g a)

-- | This type represents monadic signature functions.
type HSigFunM m f g = forall a. NatM m (f a) (g a)

-- | This type represents monadic term algebras.
type HTermHomM m f g = HSigFunM m f (HContext g)

-- | This function lifts the given signature function to a monadic
--   signature function. Note that term algebras are instances of signature
--   functions. Hence this function also applies to term algebras.
hsigFunM :: Monad m => HSigFun f g -> HSigFunM m f g

-- | This function applies the given monadic term homomorphism to the given
--   term/context.
appHTermHomM :: (HTraversable f, HFunctor g, Monad m) => HTermHomM m f g -> HCxtFunM m f g

-- | This function lifts the given signature function to a monadic term
--   algebra.
htermHomM :: (HFunctor g, Monad m) => HSigFun f g -> HTermHomM m f g

-- | This function applies the given monadic signature function to the
--   given context.
appHSigFunM :: (HTraversable f, HFunctor g, Monad m) => HSigFunM m f g -> HCxtFunM m f g

-- | This function composes two monadic term algebras.
compHTermHomM :: (HTraversable g, HFunctor h, Monad m) => HTermHomM m g h -> HTermHomM m f g -> HTermHomM m f h

-- | This function composes two monadic signature functions.
compHSigFunM :: Monad m => HSigFunM m g h -> HSigFunM m f g -> HSigFunM m f h

-- | This function composes a monadic term algebra with a monadic algebra
compHAlgM :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHomM m f g -> HAlgM m f a

-- | This function composes a monadic term algebra with a monadic algebra.
compHAlgM' :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHom f g -> HAlgM m f a
type HCoalg f a = a :-> f a

-- | This function unfolds the given value to a term using the given
--   unravelling function. This is the unique homomorphism <tt>a -&gt;
--   HTerm f</tt> from the given coalgebra of type <tt>a -&gt; f a</tt> to
--   the final coalgebra <tt>HTerm f</tt>.
hana :: HFunctor f => HCoalg f a -> a :-> HTerm f
type HCoalgM m f a = NatM m a (f a)

-- | This function unfolds the given value to a term using the given
--   monadic unravelling function. This is the unique homomorphism <tt>a
--   -&gt; HTerm f</tt> from the given coalgebra of type <tt>a -&gt; f
--   a</tt> to the final coalgebra <tt>HTerm f</tt>.
hanaM :: (HTraversable f, Monad m) => HCoalgM m f a -> NatM m a (HTerm f)

-- | This type represents r-algebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type HRAlg f a = f (HTerm f :*: a) :-> a

-- | This function constructs a paramorphism from the given r-algebra
hpara :: HFunctor f => HRAlg f a -> HTerm f :-> a

-- | This type represents monadic r-algebras over monad <tt>m</tt> and
--   functor <tt>f</tt> and with domain <tt>a</tt>.
type HRAlgM m f a = NatM m (f (HTerm f :*: a)) a

-- | This function constructs a monadic paramorphism from the given monadic
--   r-algebra
hparaM :: (HTraversable f, Monad m) => HRAlgM m f a -> NatM m (HTerm f) a

-- | This type represents r-coalgebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type HRCoalg f a = a :-> f (HTerm f :+: a)

-- | This function constructs an apomorphism from the given r-coalgebra.
hapo :: HFunctor f => HRCoalg f a -> a :-> HTerm f

-- | This type represents monadic r-coalgebras over monad <tt>m</tt> and
--   functor <tt>f</tt> with domain <tt>a</tt>.
type HRCoalgM m f a = NatM m a (f (HTerm f :+: a))

-- | This function constructs a monadic apomorphism from the given monadic
--   r-coalgebra.
hapoM :: (HTraversable f, Monad m) => HRCoalgM m f a -> NatM m a (HTerm f)

-- | This type represents cv-coalgebras over functor <tt>f</tt> and with
--   domain <tt>a</tt>.
type HCVCoalg f a = a :-> f (HContext f a)

-- | This function constructs the unique futumorphism from the given
--   cv-coalgebra to the term algebra.
hfutu :: HFunctor f => HCVCoalg f a -> a :-> HTerm f

-- | This type represents monadic cv-coalgebras over monad <tt>m</tt> and
--   functor <tt>f</tt>, and with domain <tt>a</tt>.
type HCVCoalgM m f a = NatM m a (f (HContext f a))

-- | This function constructs the unique monadic futumorphism from the
--   given monadic cv-coalgebra to the term algebra.
hfutuM :: (HTraversable f, Monad m) => HCVCoalgM m f a -> NatM m a (HTerm f)

-- | Variant of <a>appHTermHom</a> for term homomorphisms from and to
--   <a>HExpFunctor</a> signatures.
appHTermHomE :: (HExpFunctor f, HExpFunctor g) => HTermHom f g -> HTerm f :-> HTerm g

-- | Catamorphism for higher-order exponential functors.
hcataE :: HExpFunctor f => HAlg f a -> HTerm f :-> a

-- | Variant of <a>appHCxt</a> for contexts over <a>HExpFunctor</a>
--   signatures.
appHCxtE :: HExpFunctor f => HContext f (HCxt h f a) :-> HCxt h f a


-- | This module provides operators on higher-order functors. All
--   definitions are generalised versions of those in <a>Data.Comp.Ops</a>.
module Data.Comp.Multi.Ops

-- | Data type defining coproducts.
data (:++:) f g h :: (* -> *) e
HInl :: (f h e) -> :++: f g e
HInr :: (g h e) -> :++: f g e

-- | The subsumption relation.
class :<<: sub :: ((* -> *) -> * -> *) sup
hinj :: :<<: sub sup => sub a :-> sup a
hproj :: :<<: sub sup => NatM Maybe (sup a) (sub a)
data (:**:) f g a
(:**:) :: f a -> g a -> :**: f g a
hfst :: (f :**: g) a -> f a
hsnd :: (f :**: g) a -> g a

-- | This data type adds a constant product to a signature. Alternatively,
--   this could have also been defined as
--   
--   <pre>
--   data (f :&amp;&amp;: a) (g ::  * -&gt; *) e = f g e :&amp;&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for
--   <tt>productHTermHom</tt>.
data (:&&:) f a g :: (* -> *) e
(:&&:) :: f g e -> a -> :&&: f a e

-- | This class defines how to distribute a product over a sum of
--   signatures.
class HDistProd s :: ((* -> *) -> * -> *) p s' | s' -> s, s' -> p
hinjectP :: HDistProd s p s' => p -> s a :-> s' a
hprojectP :: HDistProd s p s' => s' a :-> (s a :&: p)
class HRemoveP s :: ((* -> *) -> * -> *) s' | s -> s'
hremoveP :: HRemoveP s s' => s a :-> s' a
instance [incoherent] HDistProd s p s' => HDistProd (f :++: s) p ((f :&&: p) :++: s')
instance [incoherent] HDistProd f p (f :&&: p)
instance [incoherent] HRemoveP (f :&&: p) f
instance [incoherent] HRemoveP s s' => HRemoveP ((f :&&: p) :++: s) (f :++: s')
instance [incoherent] HTraversable f => HTraversable (f :&&: a)
instance [incoherent] HFoldable f => HFoldable (f :&&: a)
instance [incoherent] HFunctor f => HFunctor (f :&&: a)
instance [incoherent] f :<<: g => f :<<: (h :++: g)
instance [incoherent] f :<<: (f :++: g)
instance [incoherent] f :<<: f
instance [incoherent] (HExpFunctor f, HExpFunctor g) => HExpFunctor (f :++: g)
instance [incoherent] (HTraversable f, HTraversable g) => HTraversable (f :++: g)
instance [incoherent] (HFoldable f, HFoldable g) => HFoldable (f :++: g)
instance [incoherent] (HFunctor f, HFunctor g) => HFunctor (f :++: g)


-- | This module defines sums on signatures. All definitions are
--   generalised versions of those in <a>Data.Comp.Sum</a>.
module Data.Comp.Multi.Sum

-- | The subsumption relation.
class :<<: sub :: ((* -> *) -> * -> *) sup
hinj :: :<<: sub sup => sub a :-> sup a
hproj :: :<<: sub sup => NatM Maybe (sup a) (sub a)

-- | Data type defining coproducts.
data (:++:) f g h :: (* -> *) e
HInl :: (f h e) -> :++: f g e
HInr :: (g h e) -> :++: f g e

-- | A variant of <a>hproj</a> for binary sum signatures.
hproj2 :: (:<<: g1 f, :<<: g2 f) => f a i -> Maybe (((g1 :++: g2) a) i)

-- | A variant of <a>hproj</a> for ternary sum signatures.
hproj3 :: (:<<: g1 f, :<<: g2 f, :<<: g3 f) => f a i -> Maybe (((g1 :++: (g2 :++: g3)) a) i)

-- | Project the outermost layer of a term to a sub signature.
hproject :: :<<: g f => NatM Maybe (HCxt h f a) (g (HCxt h f a))

-- | Project the outermost layer of a term to a binary sub signature.
hproject2 :: (:<<: g1 f, :<<: g2 f) => NatM Maybe (HCxt h f a) ((g1 :++: g2) (HCxt h f a))

-- | Project the outermost layer of a term to a ternary sub signature.
hproject3 :: (:<<: g1 f, :<<: g2 f, :<<: g3 f) => NatM Maybe (HCxt h f a) ((g1 :++: (g2 :++: g3)) (HCxt h f a))

-- | Project a term to a term over a sub signature.
deepHProject :: (HTraversable f, HFunctor g, :<<: g f) => NatM Maybe (HCxt h f a) (HCxt h g a)

-- | Project a term to a term over a binary sub signature.
deepHProject2 :: (HTraversable f, HFunctor g1, HFunctor g2, :<<: g1 f, :<<: g2 f) => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: g2) a)

-- | Project a term to a term over a ternary sub signature.
deepHProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3, :<<: g1 f, :<<: g2 f, :<<: g3 f) => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: (g2 :++: g3)) a)

-- | A variant of <a>hinj</a> for binary sum signatures.
hinj2 :: (:<<: f1 g, :<<: f2 g) => (f1 :++: f2) a :-> g a

-- | A variant of <a>hinj</a> for ternary sum signatures.
hinj3 :: (:<<: f1 g, :<<: f2 g, :<<: f3 g) => (f1 :++: (f2 :++: f3)) a :-> g a

-- | Inject a term where the outermost layer is a sub signature.
hinject :: :<<: g f => g (HCxt h f a) :-> HCxt h f a

-- | Inject a term where the outermost layer is a binary sub signature.
hinject2 :: (:<<: f1 g, :<<: f2 g) => (f1 :++: f2) (HCxt h g a) :-> HCxt h g a

-- | Inject a term where the outermost layer is a ternary sub signature.
hinject3 :: (:<<: f1 g, :<<: f2 g, :<<: f3 g) => (f1 :++: (f2 :++: f3)) (HCxt h g a) :-> HCxt h g a

-- | Inject a term over a sub signature to a term over larger signature.
deepHInject :: (HFunctor g, HFunctor f, :<<: g f) => HCxt h g a :-> HCxt h f a

-- | Inject a term over a binary sub signature to a term over larger
--   signature.
deepHInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, :<<: f1 g, :<<: f2 g) => HCxt h (f1 :++: f2) a :-> HCxt h g a

-- | Inject a term over a ternary sub signature to a term over larger
--   signature.
deepHInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, :<<: f1 g, :<<: f2 g, :<<: f3 g) => HCxt h (f1 :++: (f2 :++: f3)) a :-> HCxt h g a

-- | A variant of <a>deepHInject</a> for exponential signatures.
deepHInjectE :: (HExpFunctor g, :<<: g f) => HTerm g :-> HTerm f

-- | A variant of <a>deepHInject2</a> for exponential signatures.
deepHInjectE2 :: (HExpFunctor g1, HExpFunctor g2, :<<: g1 f, :<<: g2 f) => HTerm (g1 :++: g2) :-> HTerm f

-- | A variant of <a>deepHInject3</a> for exponential signatures.
deepHInjectE3 :: (HExpFunctor g1, HExpFunctor g2, HExpFunctor g3, :<<: g1 f, :<<: g2 f, :<<: g3 f) => HTerm (g1 :++: (g2 :++: g3)) :-> HTerm f
hinjectHConst :: (HFunctor g, :<<: g f) => HConst g :-> HCxt h f a
hinjectHConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, :<<: f1 g, :<<: f2 g) => HConst (f1 :++: f2) :-> HCxt h g a
hinjectHConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, :<<: f1 g, :<<: f2 g, :<<: f3 g) => HConst (f1 :++: (f2 :++: f3)) :-> HCxt h g a
hprojectHConst :: (HFunctor g, :<<: g f) => NatM Maybe (HCxt h f a) (HConst g)

-- | This function injects a whole context into another context.
hinjectHCxt :: (HFunctor g, :<<: g f) => HCxt h' g (HCxt h f a) :-> HCxt h f a

-- | This function lifts the given functor to a context.
liftHCxt :: (HFunctor f, :<<: g f) => g a :-> HContext f a

-- | This function applies the given context with hole type <tt>a</tt> to a
--   family <tt>f</tt> of contexts (possibly terms) indexed by <tt>a</tt>.
--   That is, each hole <tt>h</tt> is replaced by the context <tt>f h</tt>.
substHHoles :: (HFunctor f, HFunctor g, :<<: f g) => (v :-> HCxt h g a) -> HCxt h' f v :-> HCxt h g a


-- | This module defines an abstraction notion of a variable in a term. All
--   definitions are generalised versions of those in
--   <a>Data.Comp.Variables</a>.
module Data.Comp.Multi.Variables
type GSubst v a = NatM Maybe (K v) a
type HCxtSubst h a f v = GSubst v (HCxt h f a)
type Subst f v = HCxtSubst HNoHole HNothing f v

-- | This multiparameter class defines functors with variables. An instance
--   <tt>HasVar f v</tt> denotes that values over <tt>f</tt> might contain
--   variables of type <tt>v</tt>.
class HasVars f :: ((* -> *) -> * -> *) v
isVar :: HasVars f v => f a :=> Maybe v
varsToHHoles :: (HFunctor f, HasVars f v) => HTerm f :-> HContext f (K v)
containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> HAlg f (K Bool)

-- | This function checks whether a variable is contained in a context.
containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f) => v -> HCxt h f a :=> Bool
variableListAlg :: (HasVars f v, HFoldable f) => HAlg f (K [v])

-- | This function computes the list of variables occurring in a context.
variableList :: (HasVars f v, HFoldable f, HFunctor f) => HCxt h f a :=> [v]
variablesAlg :: (Ord v, HasVars f v, HFoldable f) => HAlg f (K (Set v))

-- | This function computes the set of variables occurring in a context.
variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => HCxt h f a :=> Set v

-- | This function computes the set of variables occurring in a context.
variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => HConst f :=> Set v
substAlg :: HasVars f v => HCxtSubst h a f v -> HAlg f (HCxt h f a)

-- | This function substitutes variables in a context according to a
--   partial mapping from variables to contexts.
class SubstVars v t a
substVars :: SubstVars v t a => GSubst v t -> a :-> a
appSubst :: SubstVars v t a => GSubst v t -> a :-> a

-- | This function composes two substitutions <tt>s1</tt> and <tt>s2</tt>.
--   That is, applying the resulting substitution is equivalent to first
--   applying <tt>s2</tt> and then <tt>s1</tt>.
compSubst :: (Ord v, HasVars f v, HFunctor f) => HCxtSubst h a f v -> HCxtSubst h a f v -> HCxtSubst h a f v
instance [overlap ok] (SubstVars v t a, HFunctor f) => SubstVars v t (f a)
instance [overlap ok] (Ord v, HasVars f v, HFunctor f) => SubstVars v (HCxt h f a) (HCxt h f a)
instance [overlap ok] HasVars f v => HasVars (HCxt h f) v
instance [overlap ok] (HasVars f v, HasVars g v) => HasVars (f :++: g) v


-- | This module defines products on signatures. All definitions are
--   generalised versions of those in <a>Data.Comp.Product</a>.
module Data.Comp.Multi.Product

-- | This data type adds a constant product to a signature. Alternatively,
--   this could have also been defined as
--   
--   <pre>
--   data (f :&amp;&amp;: a) (g ::  * -&gt; *) e = f g e :&amp;&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for
--   <tt>productHTermHom</tt>.
data (:&&:) f a g :: (* -> *) e
(:&&:) :: f g e -> a -> :&&: f a e

-- | This class defines how to distribute a product over a sum of
--   signatures.
class HDistProd s :: ((* -> *) -> * -> *) p s' | s' -> s, s' -> p
hinjectP :: HDistProd s p s' => p -> s a :-> s' a
hprojectP :: HDistProd s p s' => s' a :-> (s a :&: p)
class HRemoveP s :: ((* -> *) -> * -> *) s' | s -> s'
hremoveP :: HRemoveP s s' => s a :-> s' a

-- | This function transforms a function with a domain constructed from a
--   functor to a function with a domain constructed with the same functor
--   but with an additional product.
liftP :: HRemoveP s s' => (s' a :-> t) -> s a :-> t

-- | This function annotates each sub term of the given term with the given
--   value (of type a).
constP :: (HDistProd f p g, HFunctor f, HFunctor g) => p -> HCxt h f a :-> HCxt h g a

-- | This function transforms a function with a domain constructed from a
--   functor to a function with a domain constructed with the same functor
--   but with an additional product.
liftP' :: (HDistProd s' p s, HFunctor s, HFunctor s') => (s' a :-> HCxt h s' a) -> s a :-> HCxt h s a

-- | This function strips the products from a term over a functor whith
--   products.
stripP :: (HFunctor f, HRemoveP g f, HFunctor g) => HCxt h g a :-> HCxt h f a
productHTermHom :: (HDistProd f p f', HDistProd g p g', HFunctor g, HFunctor g') => HTermHom f g -> HTermHom f' g'
hproject' :: (HRemoveP g s', :<<: g f) => HCxt h f a i -> Maybe (s' (HCxt h f a) i)


-- | This module defines the infrastructure necessary to use compositional
--   data types for mutually recursive data types. Examples of usage are
--   provided below.
module Data.Comp.Multi


-- | This module defines the central notion of <i>terms</i> and its
--   generalisation to contexts.
module Data.Comp.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes. The first type parameter is
--   supposed to be one of the phantom types <a>Hole</a> and <a>NoHole</a>.
--   The second parameter is the signature of the context. The third
--   parameter is the type of the holes.
data Cxt :: * -> (* -> *) -> * -> *
Term :: f (Cxt h f a) -> Cxt h f a
Hole :: a -> Cxt Hole f a

-- | Phantom type that signals that a <a>Cxt</a> might contain holes.
data Hole

-- | Phantom type that signals that a <a>Cxt</a> does not contain holes.
data NoHole
type Context = Cxt Hole

-- | Phantom type used to define <a>Term</a>.
data Nothing

-- | A term is a context with no holes.
type Term f = Cxt NoHole f Nothing

-- | Polymorphic definition of a term. This formulation is more natural
--   than <a>Term</a>, it leads to impredicative types in some cases,
--   though.
type PTerm f = forall h a. Cxt h f a
type Const f = f ()

-- | This function unravels the given term at the topmost layer.
unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)

-- | Convert a functorial value into a context.
simpCxt :: Functor f => f a -> Context f a

-- | Cast a term over a signature to a context over the same signature.
toCxt :: Term f -> Cxt h f a

-- | This function converts a constant to a term. This assumes that the
--   argument is indeed a constant, i.e. does not have a value for the
--   argument type of the functor <tt>f</tt>.
constTerm :: Functor f => Const f -> Term f
instance Traversable f => Traversable (Cxt h f)
instance Foldable f => Foldable (Cxt h f)
instance Functor f => Functor (Cxt h f)
instance Show Nothing
instance Ord Nothing
instance Eq Nothing


-- | This module defines the notion of algebras and catamorphisms, and
--   their generalizations to e.g. monadic versions and other (co)recursion
--   schemes.
module Data.Comp.Algebra

-- | This type represents an algebra over a functor <tt>f</tt> and carrier
--   <tt>a</tt>.
type Alg f a = f a -> a

-- | Construct a catamorphism for contexts over <tt>f</tt> with holes of
--   type <tt>a</tt>, from the given algebra.
free :: Functor f => Alg f b -> (a -> b) -> Cxt h f a -> b

-- | Construct a catamorphism from the given algebra.
cata :: Functor f => Alg f a -> Term f -> a

-- | A generalisation of <a>cata</a> from terms over <tt>f</tt> to contexts
--   over <tt>f</tt>, where the holes have the type of the algebra carrier.
cata' :: Functor f => Alg f a -> Cxt h f a -> a

-- | This function applies a whole context into another context.
appCxt :: Functor f => Context f (Cxt h f a) -> Cxt h f a

-- | This type represents a monadic algebra. It is similar to <a>Alg</a>
--   but the return type is monadic.
type AlgM m f a = f a -> m a

-- | Convert a monadic algebra into an ordinary algebra with a monadic
--   carrier.
algM :: (Traversable f, Monad m) => AlgM m f a -> Alg f (m a)

-- | Construct a monadic catamorphism for contexts over <tt>f</tt> with
--   holes of type <tt>a</tt>, from the given monadic algebra.
freeM :: (Traversable f, Monad m) => AlgM m f b -> (a -> m b) -> Cxt h f a -> m b

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: (Traversable f, Monad m) => AlgM m f a -> Term f -> m a

-- | A generalisation of <a>cataM</a> from terms over <tt>f</tt> to
--   contexts over <tt>f</tt>, where the holes have the type of the monadic
--   algebra carrier.
cataM' :: (Traversable f, Monad m) => AlgM m f a -> Cxt h f a -> m a

-- | This type represents a context function.
type CxtFun f g = forall a h. Cxt h f a -> Cxt h g a

-- | This type represents a signature function.
type SigFun f g = forall a. f a -> g a

-- | This type represents a term homomorphism.
type TermHom f g = SigFun f (Context g)

-- | Apply a term homomorphism recursively to a term/context.
appTermHom :: (Traversable f, Functor g) => TermHom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compTermHom :: (Functor g, Functor h) => TermHom g h -> TermHom f g -> TermHom f h

-- | This function applies a signature function to the given context.
appSigFun :: (Functor f, Functor g) => SigFun f g -> CxtFun f g

-- | This function composes two signature functions.
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h

-- | Lifts the given signature function to the canonical term homomorphism.
termHom :: Functor g => SigFun f g -> TermHom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: Functor g => Alg g a -> TermHom f g -> Alg f a

-- | Compose a term homomorphism with a coalgebra to get a cv-coalgebra.
compCoalg :: TermHom f g -> Coalg f a -> CVCoalg' g a

-- | Compose a term homomorphism with a cv-coalgebra to get a new
--   cv-coalgebra.
compCVCoalg :: (Functor f, Functor g) => TermHom f g -> CVCoalg' f a -> CVCoalg' g a

-- | This type represents a monadic context function.
type CxtFunM m f g = forall a h. Cxt h f a -> m (Cxt h g a)

-- | This type represents a monadic signature function.
type SigFunM m f g = forall a. f a -> m (g a)

-- | This type represents a monadic term homomorphism.
type TermHomM m f g = SigFunM m f (Context g)

-- | This type represents a monadic signature function. It is similar to
--   <a>SigFunM</a> but has monadic values also in the domain.
type SigFunM' m f g = forall a. f (m a) -> m (g a)

-- | This type represents a monadic term homomorphism. It is similar to
--   <a>TermHomM</a> but has monadic values also in the domain.
type TermHomM' m f g = SigFunM' m f (Context g)

-- | Lift the given signature function to a monadic signature function.
--   Note that term homomorphisms are instances of signature functions.
--   Hence this function also applies to term homomorphisms.
sigFunM :: Monad m => SigFun f g -> SigFunM m f g

-- | Lift the give monadic signature function to a monadic term
--   homomorphism.
termHom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> TermHomM m f g

-- | Apply a monadic term homomorphism recursively to a term/context.
appTermHomM :: (Traversable f, Functor g, Monad m) => TermHomM m f g -> CxtFunM m f g

-- | Lift the given signature function to a monadic term homomorphism.
termHomM :: (Functor g, Monad m) => SigFun f g -> TermHomM m f g

-- | This function constructs the unique monadic homomorphism from the
--   initial term algebra to the given term algebra.
termHomM' :: (Traversable f, Functor g, Monad m) => TermHomM' m f g -> CxtFunM m f g

-- | This function applies a monadic signature function to the given
--   context.
appSigFunM :: (Traversable f, Functor g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | This function applies a signature function to the given context.
appSigFunM' :: (Traversable f, Functor g, Monad m) => SigFunM' m f g -> CxtFunM m f g

-- | Compose two monadic term homomorphisms.
compTermHomM :: (Traversable g, Functor h, Monad m) => TermHomM m g h -> TermHomM m f g -> TermHomM m f h

-- | This function composes two monadic signature functions.
compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h

-- | Compose a monadic algebra with a monadic term homomorphism to get a
--   new monadic algebra.
compAlgM :: (Traversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a

-- | Compose a monadic algebra with a term homomorphism to get a new
--   monadic algebra.
compAlgM' :: (Traversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a

-- | This type represents a coalgebra over a functor <tt>f</tt> and carrier
--   <tt>a</tt>.
type Coalg f a = a -> f a

-- | Construct an anamorphism from the given coalgebra.
ana :: Functor f => Coalg f a -> a -> Term f

-- | Shortcut fusion variant of <a>ana</a>.
ana' :: Functor f => Coalg f a -> a -> Term f

-- | This type represents a monadic coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CoalgM m f a = a -> m (f a)

-- | Construct a monadic anamorphism from the given monadic coalgebra.
anaM :: (Traversable f, Monad m) => CoalgM m f a -> a -> m (Term f)

-- | This type represents an r-algebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RAlg f a = f (Term f, a) -> a

-- | Construct a paramorphism from the given r-algebra.
para :: Functor f => RAlg f a -> Term f -> a

-- | This type represents a monadic r-algebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RAlgM m f a = f (Term f, a) -> m a

-- | Construct a monadic paramorphism from the given monadic r-algebra.
paraM :: (Traversable f, Monad m) => RAlgM m f a -> Term f -> m a

-- | This type represents an r-coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RCoalg f a = a -> f (Either (Term f) a)

-- | Construct an apomorphism from the given r-coalgebra.
apo :: Functor f => RCoalg f a -> a -> Term f

-- | This type represents a monadic r-coalgebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type RCoalgM m f a = a -> m (f (Either (Term f) a))

-- | Construct a monadic apomorphism from the given monadic r-coalgebra.
apoM :: (Traversable f, Monad m) => RCoalgM m f a -> a -> m (Term f)

-- | This type represents a cv-algebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CVAlg f a f' = f (Term f') -> a

-- | Construct a histomorphism from the given cv-algebra.
histo :: (Functor f, DistProd f a f') => CVAlg f a f' -> Term f -> a

-- | This type represents a monadic cv-algebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CVAlgM m f a f' = f (Term f') -> m a

-- | Construct a monadic histomorphism from the given monadic cv-algebra.
histoM :: (Traversable f, Monad m, DistProd f a f') => CVAlgM m f a f' -> Term f -> m a

-- | This type represents a cv-coalgebra over a functor <tt>f</tt> and
--   carrier <tt>a</tt>.
type CVCoalg f a = a -> f (Context f a)

-- | Construct a futumorphism from the given cv-coalgebra.
futu :: Functor f => CVCoalg f a -> a -> Term f

-- | This type represents a generalised cv-coalgebra over a functor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalg' f a = a -> Context f a

-- | Construct a futumorphism from the given generalised cv-coalgebra.
futu' :: Functor f => CVCoalg' f a -> a -> Term f

-- | This type represents a monadic cv-coalgebra over a functor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CVCoalgM m f a = a -> m (f (Context f a))

-- | Construct a monadic futumorphism from the given monadic cv-coalgebra.
futuM :: (Traversable f, Monad m) => CVCoalgM m f a -> a -> m (Term f)

-- | Variant of <a>appTermHom</a> for term homomorphisms from and to
--   <a>ExpFunctor</a> signatures.
appTermHomE :: (ExpFunctor f, ExpFunctor g) => TermHom f g -> Term f -> Term g

-- | Catamorphism for exponential functors. The intermediate
--   <tt>cataFS</tt> originates from
--   <a>http://comonad.com/reader/2008/rotten-bananas/</a>.
cataE :: ExpFunctor f => Alg f a -> Term f -> a

-- | Anamorphism for exponential functors.
anaE :: ExpFunctor f => Coalg f a -> a -> Term f

-- | Variant of <a>appCxt</a> for contexts over <a>ExpFunctor</a>
--   signatures.
appCxtE :: ExpFunctor f => Context f (Cxt h f a) -> Cxt h f a


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.Sum

-- | Signature containment relation for automatic injections. The left-hand
--   must be an atomic signature, where as the right-hand side must have a
--   list-like structure. Examples include <tt>f :&lt;: f :+: g</tt> and
--   <tt>g :&lt;: f :+: (g :+: h)</tt>, non-examples include <tt>f :+: g
--   :&lt;: f :+: (g :+: h)</tt> and <tt>f :&lt;: (f :+: g) :+: h</tt>.
class :<: sub sup
inj :: :<: sub sup => sub a -> sup a
proj :: :<: sub sup => sup a -> Maybe (sub a)

-- | Formal sum of signatures (functors).
data (:+:) f g e
Inl :: (f e) -> :+: f g e
Inr :: (g e) -> :+: f g e

-- | A variant of <a>proj</a> for binary sum signatures.
proj2 :: (:<: g1 f, :<: g2 f) => f a -> Maybe ((g1 :+: g2) a)

-- | A variant of <a>proj</a> for ternary sum signatures.
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a -> Maybe ((g1 :+: (g2 :+: g3)) a)

-- | Project the outermost layer of a term to a sub signature.
project :: :<: g f => Cxt h f a -> Maybe (g (Cxt h f a))

-- | Project the outermost layer of a term to a binary sub signature.
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a -> Maybe ((g1 :+: g2) (Cxt h f a))

-- | Project the outermost layer of a term to a ternary sub signature.
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a -> Maybe ((g1 :+: (g2 :+: g3)) (Cxt h f a))

-- | Project a term to a term over a sub signature.
deepProject :: (Traversable f, Functor g, :<: g f) => Cxt h f a -> Maybe (Cxt h g a)

-- | Project a term to a term over a binary sub signature.
deepProject2 :: (Traversable f, Functor g1, Functor g2, :<: g1 f, :<: g2 f) => Cxt h f a -> Maybe (Cxt h (g1 :+: g2) a)

-- | Project a term to a term over a ternary sub signature.
deepProject3 :: (Traversable f, Functor g1, Functor g2, Functor g3, :<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a -> Maybe (Cxt h (g1 :+: (g2 :+: g3)) a)

-- | A variant of <a>deepProject</a> where the sub signature is required to
--   be <a>Traversable</a> rather than the whole signature.
deepProject' :: (Traversable g, :<: g f) => Cxt h f a -> Maybe (Cxt h g a)

-- | A variant of <a>deepProject2</a> where the sub signatures are required
--   to be <a>Traversable</a> rather than the whole signature.
deepProject2' :: (Traversable g1, Traversable g2, :<: g1 f, :<: g2 f) => Cxt h f a -> Maybe (Cxt h (g1 :+: g2) a)

-- | A variant of <a>deepProject3</a> where the sub signatures are required
--   to be <a>Traversable</a> rather than the whole signature.
deepProject3' :: (Traversable g1, Traversable g2, Traversable g3, :<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a -> Maybe (Cxt h (g1 :+: (g2 :+: g3)) a)

-- | A variant of <a>inj</a> for binary sum signatures.
inj2 :: (:<: f1 g, :<: f2 g) => (f1 :+: f2) a -> g a

-- | A variant of <a>inj</a> for ternary sum signatures.
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => (f1 :+: (f2 :+: f3)) a -> g a

-- | Inject a term where the outermost layer is a sub signature.
inject :: :<: g f => g (Cxt h f a) -> Cxt h f a

-- | Inject a term where the outermost layer is a binary sub signature.
inject2 :: (:<: f1 g, :<: f2 g) => (f1 :+: f2) (Cxt h g a) -> Cxt h g a

-- | Inject a term where the outermost layer is a ternary sub signature.
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => (f1 :+: (f2 :+: f3)) (Cxt h g a) -> Cxt h g a

-- | Inject a term over a sub signature to a term over larger signature.
deepInject :: (Functor g, Functor f, :<: g f) => Cxt h g a -> Cxt h f a

-- | Inject a term over a binary sub signature to a term over larger
--   signature.
deepInject2 :: (Functor f1, Functor f2, Functor g, :<: f1 g, :<: f2 g) => Cxt h (f1 :+: f2) a -> Cxt h g a

-- | Inject a term over a ternary signature to a term over larger
--   signature.
deepInject3 :: (Functor f1, Functor f2, Functor f3, Functor g, :<: f1 g, :<: f2 g, :<: f3 g) => Cxt h (f1 :+: (f2 :+: f3)) a -> Cxt h g a

-- | A variant of <a>deepInject</a> for exponential signatures.
deepInjectE :: (ExpFunctor g, :<: g f) => Term g -> Term f

-- | A variant of <a>deepInject2</a> for exponential signatures.
deepInjectE2 :: (ExpFunctor g1, ExpFunctor g2, :<: g1 f, :<: g2 f) => Term (g1 :+: g2) -> Term f

-- | A variant of <a>deepInject3</a> for exponential signatures.
deepInjectE3 :: (ExpFunctor g1, ExpFunctor g2, ExpFunctor g3, :<: g1 f, :<: g2 f, :<: g3 f) => Term (g1 :+: (g2 :+: g3)) -> Term f
injectConst :: (Functor g, :<: g f) => Const g -> Cxt h f a
injectConst2 :: (Functor f1, Functor f2, Functor g, :<: f1 g, :<: f2 g) => Const (f1 :+: f2) -> Cxt h g a
injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, :<: f1 g, :<: f2 g, :<: f3 g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g a
projectConst :: (Functor g, :<: g f) => Cxt h f a -> Maybe (Const g)

-- | This function injects a whole context into another context.
injectCxt :: (Functor g, :<: g f) => Cxt h' g (Cxt h f a) -> Cxt h f a

-- | This function lifts the given functor to a context.
liftCxt :: (Functor f, :<: g f) => g a -> Context f a

-- | This function applies the given context with hole type <tt>a</tt> to a
--   family <tt>f</tt> of contexts (possibly terms) indexed by <tt>a</tt>.
--   That is, each hole <tt>h</tt> is replaced by the context <tt>f h</tt>.
substHoles :: (Functor f, Functor g, :<: f g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles' :: (Functor f, Functor g, :<: f g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
instance [incoherent] (Eq (f a), Eq (g a)) => Eq ((:+:) f g a)
instance [incoherent] (Ord (f a), Ord (g a)) => Ord ((:+:) f g a)
instance [incoherent] (Show (f a), Show (g a)) => Show ((:+:) f g a)
instance [incoherent] Functor f => Monad (Context f)


-- | This module defines products on signatures.
module Data.Comp.Product

-- | This data type adds a constant product to a signature.
data (:&:) f a e
(:&:) :: f e -> a -> :&: f a e

-- | Formal product of signatures (functors).
data (:*:) f g a
(:*:) :: f a -> g a -> :*: f g a

-- | This class defines how to distribute a product over a sum of
--   signatures.
class DistProd s p s' | s' -> s, s' -> p
injectP :: DistProd s p s' => p -> s a -> s' a
projectP :: DistProd s p s' => s' a -> (s a, p)
class RemoveP s s' | s -> s'
removeP :: RemoveP s s' => s a -> s' a

-- | Transform a function with a domain constructed from a functor to a
--   function with a domain constructed with the same functor, but with an
--   additional product.
liftP :: RemoveP s s' => (s' a -> t) -> s a -> t

-- | Transform a function with a domain constructed from a functor to a
--   function with a domain constructed with the same functor, but with an
--   additional product.
liftP' :: (DistProd s' p s, Functor s, Functor s') => (s' a -> Cxt h s' a) -> s a -> Cxt h s a

-- | Strip the products from a term over a functor with products.
stripP :: (Functor f, RemoveP g f, Functor g) => Cxt h g a -> Cxt h f a

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   products.
productTermHom :: (DistProd f p f', DistProd g p g', Functor g, Functor g') => TermHom f g -> TermHom f' g'

-- | Annotate each node of a term with a constant value.
constP :: (DistProd f p g, Functor f, Functor g) => p -> Cxt h f a -> Cxt h g a
project' :: (RemoveP g s', :<: g f) => Cxt h f a -> Maybe (s' (Cxt h f a))


-- | This module defines type generic functions and recursive schemes along
--   the lines of the Uniplate library.
module Data.Comp.Generic

-- | This function returns a list of all subterms of the given term. This
--   function is similar to Uniplate's <tt>universe</tt> function.
subterms :: Foldable f => Term f -> [Term f]

-- | This function returns a list of all subterms of the given term that
--   are constructed from a particular functor.
subterms' :: (Foldable f, :<: g f) => Term f -> [g (Term f)]

-- | This function transforms every subterm according to the given function
--   in a bottom-up manner. This function is similar to Uniplate's
--   <tt>transform</tt> function.
transform :: Functor f => (Term f -> Term f) -> Term f -> Term f
transform' :: Functor f => (Term f -> Maybe (Term f)) -> Term f -> Term f

-- | Monadic version of <a>transform</a>.
transformM :: (Traversable f, Monad m) => (Term f -> m (Term f)) -> Term f -> m (Term f)
query :: Foldable f => (Term f -> r) -> (r -> r -> r) -> Term f -> r
gsize :: Foldable f => Term f -> Int

-- | This function computes the generic size of the given term, i.e. the
--   its number of subterm occurrences.
size :: Foldable f => Cxt h f a -> Int

-- | This function computes the generic depth of the given term.
depth :: Foldable f => Cxt h f a -> Int


-- | This module defines an abstraction notion of a variable in
--   compositional data type.
module Data.Comp.Variables

-- | This multiparameter class defines functors with variables. An instance
--   <tt>HasVar f v</tt> denotes that values over <tt>f</tt> might contain
--   variables of type <tt>v</tt>.
class HasVars f v
isVar :: HasVars f v => f a -> Maybe v
type Subst f v = CxtSubst NoHole Nothing f v
type CxtSubst h a f v = Map v (Cxt h f a)
varsToHoles :: (Functor f, HasVars f v) => Term f -> Context f v

-- | This function checks whether a variable is contained in a context.
containsVar :: (Eq v, HasVars f v, Foldable f, Functor f) => v -> Cxt h f a -> Bool

-- | This function computes the set of variables occurring in a context.
variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set v

-- | This function computes the list of variables occurring in a context.
variableList :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> [v]

-- | This function computes the set of variables occurring in a context.
variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
substVars :: SubstVars v t a => (v -> Maybe t) -> a -> a
appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a

-- | This function composes two substitutions <tt>s1</tt> and <tt>s2</tt>.
--   That is, applying the resulting substitution is equivalent to first
--   applying <tt>s2</tt> and then <tt>s1</tt>.
compSubst :: (Ord v, HasVars f v, Functor f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
instance [overlap ok] (SubstVars v t a, Functor f) => SubstVars v t (f a)
instance [overlap ok] (Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a)
instance [overlap ok] HasVars f v => HasVars (Cxt h f) v
instance [overlap ok] (HasVars f v, HasVars g v) => HasVars (f :+: g) v


-- | This module implements the decomposition of terms into function
--   symbols and arguments resp. variables.
module Data.Comp.Decompose

-- | This type represents decompositions of functorial values.
data Decomp f v a
Var :: v -> Decomp f v a
Fun :: (Const f) -> [a] -> Decomp f v a

-- | This type represents decompositions of terms.
type DecompTerm f v = Decomp f v (Term f)

-- | This class specifies the decomposability of a functorial value.
class (HasVars f v, Functor f, Foldable f) => Decompose f v
decomp :: Decompose f v => f a -> Decomp f v a

-- | This function computes the structure of a functorial value.
structure :: Functor f => f a -> Const f

-- | This function computes the arguments of a functorial value.
arguments :: Foldable f => f a -> [a]

-- | This function decomposes a term.
decompose :: Decompose f v => Term f -> DecompTerm f v
instance (HasVars f v, Functor f, Foldable f) => Decompose f v


-- | This module implements a simple unification algorithm using
--   compositional data types.
module Data.Comp.Unification

-- | This type represents equations between terms over a specific
--   signature.
type Equation f = (Term f, Term f)

-- | This type represents list of equations.
type Equations f = [Equation f]

-- | This type represents errors that might occur during the unification.
data UnifError f v
FailedOccursCheck :: v -> (Term f) -> UnifError f v
HeadSymbolMismatch :: (Term f) -> (Term f) -> UnifError f v
UnifError :: String -> UnifError f v
failedOccursCheck :: MonadError (UnifError f v) m => v -> Term f -> m a
headSymbolMismatch :: MonadError (UnifError f v) m => Term f -> Term f -> m a
appSubstEq :: (Ord v, HasVars f v, Functor f) => Subst f v -> Equation f -> Equation f

-- | This function returns the most general unifier of the given equations
--   using the algorithm of Martelli and Montanari.
unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => Equations f -> m (Subst f v)
data UnifyState f v
UnifyState :: Equations f -> Subst f v -> UnifyState f v
usEqs :: UnifyState f v -> Equations f
usSubst :: UnifyState f v -> Subst f v
type UnifyM f v m a = StateT (UnifyState f v) m a
runUnifyM :: MonadError (UnifError f v) m => UnifyM f v m a -> Equations f -> m (Subst f v)
withNextEq :: Monad m => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()
putEqs :: Monad m => Equations f -> UnifyM f v m ()
putBinding :: (Monad m, Ord v, HasVars f v, Functor f) => (v, Term f) -> UnifyM f v m ()
runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => UnifyM f v m ()
unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) => Equation f -> UnifyM f v m ()
instance Error (UnifError f v)


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>Functor</a>, <a>Foldable</a>, and <a>Traversable</a>.
module Data.Comp.Derive

-- | Helper function for generating a list of instances for a list of named
--   signatures. For example, in order to derive instances <a>Functor</a>
--   and <a>ShowF</a> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [instanceFunctor, instanceShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

-- | Signature printing. An instance <tt>ShowF f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowF f
showF :: ShowF f => f String -> String

-- | Derive an instance of <a>ShowF</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceShowF :: Name -> Q [Dec]

-- | Signature equality. An instance <tt>EqF f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>.
class EqF f
eqF :: (EqF f, Eq a) => f a -> f a -> Bool

-- | Derive an instance of <a>EqF</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceEqF :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqF f => OrdF f
compareF :: (OrdF f, Ord a) => f a -> f a -> Ordering

-- | Derive an instance of <a>OrdF</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceOrdF :: Name -> Q [Dec]

-- | The <a>Functor</a> class is used for types that can be mapped over.
--   Instances of <a>Functor</a> should satisfy the following laws:
--   
--   <pre>
--   fmap id  ==  id
--   fmap (f . g)  ==  fmap f . fmap g
--   </pre>
--   
--   The instances of <a>Functor</a> for lists, <tt>Data.Maybe.Maybe</tt>
--   and <tt>System.IO.IO</tt> satisfy these laws.
class Functor f :: (* -> *)

-- | Derive an instance of <a>Functor</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceFunctor :: Name -> Q [Dec]

-- | Data structures that can be folded.
--   
--   Minimal complete definition: <a>foldMap</a> or <a>foldr</a>.
--   
--   For example, given a data type
--   
--   <pre>
--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--   </pre>
--   
--   a suitable instance would be
--   
--   <pre>
--   instance Foldable Tree where
--      foldMap f Empty = mempty
--      foldMap f (Leaf x) = f x
--      foldMap f (Node l k r) = foldMap f l `mappend` f k `mappend` foldMap f r
--   </pre>
--   
--   This is suitable even for abstract types, as the monoid is assumed to
--   satisfy the monoid laws. Alternatively, one could define
--   <tt>foldr</tt>:
--   
--   <pre>
--   instance Foldable Tree where
--      foldr f z Empty = z
--      foldr f z (Leaf x) = f x z
--      foldr f z (Node l k r) = foldr f (f k (foldr f z r)) l
--   </pre>
class Foldable t :: (* -> *)

-- | Derive an instance of <a>Foldable</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceFoldable :: Name -> Q [Dec]

-- | Functors representing data structures that can be traversed from left
--   to right.
--   
--   Minimal complete definition: <a>traverse</a> or <a>sequenceA</a>.
--   
--   Instances are similar to <a>Functor</a>, e.g. given a data type
--   
--   <pre>
--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--   </pre>
--   
--   a suitable instance would be
--   
--   <pre>
--   instance Traversable Tree where
--      traverse f Empty = pure Empty
--      traverse f (Leaf x) = Leaf &lt;$&gt; f x
--      traverse f (Node l k r) = Node &lt;$&gt; traverse f l &lt;*&gt; f k &lt;*&gt; traverse f r
--   </pre>
--   
--   This is suitable even for abstract types, as the laws for
--   <a>&lt;*&gt;</a> imply a form of associativity.
--   
--   The superclass instances should satisfy the following:
--   
--   <ul>
--   <li>In the <a>Functor</a> instance, <a>fmap</a> should be equivalent
--   to traversal with the identity applicative functor
--   (<a>fmapDefault</a>).</li>
--   <li>In the <a>Foldable</a> instance, <tt>Data.Foldable.foldMap</tt>
--   should be equivalent to traversal with a constant applicative functor
--   (<a>foldMapDefault</a>).</li>
--   </ul>
class (Functor t, Foldable t) => Traversable t :: (* -> *)

-- | Derive an instance of <a>Traversable</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceTraversable :: Name -> Q [Dec]

-- | Exponential functors are functors that may be both covariant (as
--   ordinary functors) and contravariant.
class ExpFunctor f

-- | Derive an instance of <a>ExpFunctor</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceExpFunctor :: Name -> Q [Dec]

-- | Signature arbitration. An instance <tt>ArbitraryF f</tt> gives rise to
--   an instance <tt>Arbitrary (Term f)</tt>.
class ArbitraryF f
arbitraryF' :: (ArbitraryF f, Arbitrary v) => [(Int, Gen (f v))]
arbitraryF :: (ArbitraryF f, Arbitrary v) => Gen (f v)
shrinkF :: (ArbitraryF f, Arbitrary v) => f v -> [f v]

-- | Derive an instance of <a>ArbitraryF</a> for a type constructor of any
--   first-order kind taking at least one argument. It is necessary that
--   all types that are used by the data type definition are themselves
--   instances of <a>Arbitrary</a>.
instanceArbitraryF :: Name -> Q [Dec]

-- | Random generation and shrinking of values.
class Arbitrary a
arbitrary :: Arbitrary a => Gen a
shrink :: Arbitrary a => a -> [a]

-- | Derive an instance of <a>Arbitrary</a> for a type constructor.
instanceArbitrary :: Name -> Q [Dec]

-- | A class of types that can be fully evaluated.
class NFData a
rnf :: NFData a => a -> ()

-- | Derive an instance of <a>NFData</a> for a type constructor.
instanceNFData :: Name -> Q [Dec]

-- | Signature normal form. An instance <tt>NFDataF f</tt> gives rise to an
--   instance <tt>NFData (Term f)</tt>.
class NFDataF f
rnfF :: (NFDataF f, NFData a) => f a -> ()

-- | Derive an instance of <a>NFDataF</a> for a type constructor of any
--   first-order kind taking at least one argument.
instanceNFDataF :: Name -> Q [Dec]

-- | Derive smart constructors for a type constructor of any first-order
--   kind taking at least one argument. The smart constructors are similar
--   to the ordinary constructors, but an <a>inject</a> is automatically
--   inserted.
smartConstructors :: Name -> Q [Dec]

-- | Signature printing. An instance <tt>HShowF f</tt> gives rise to an
--   instance <tt>KShow (HTerm f)</tt>.
class HShowF f
hshowF :: HShowF f => HAlg f (K String)
hshowF' :: HShowF f => f (K String) :=> String
class KShow a
kshow :: KShow a => a i -> K String i

-- | Derive an instance of <a>HShowF</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
instanceHShowF :: Name -> Q [Dec]

-- | Signature equality. An instance <tt>HEqF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class HEqF f
heqF :: (HEqF f, KEq g) => f g i -> f g j -> Bool
class KEq f
keq :: KEq f => f i -> f j -> Bool

-- | Derive an instance of <a>HEqF</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
instanceHEqF :: Name -> Q [Dec]

-- | This class represents higher-order functors (Johann, Ghani, POPL '08)
--   which are endofunctors on the category of endofunctors.
class HFunctor h

-- | Derive an instance of <a>HFunctor</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
instanceHFunctor :: Name -> Q [Dec]

-- | Higher-order functors that can be folded.
--   
--   Minimal complete definition: <a>hfoldMap</a> or <a>hfoldr</a>.
class HFunctor h => HFoldable h

-- | Derive an instance of <a>HFoldable</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
instanceHFoldable :: Name -> Q [Dec]
class HFoldable t => HTraversable t

-- | Derive an instance of <a>HTraversable</a> for a type constructor of
--   any higher-order kind taking at least two arguments.
instanceHTraversable :: Name -> Q [Dec]

-- | Higher-order exponential functors are higher-order functors that may
--   be both covariant (as ordinary higher-order functors) and
--   contravariant.
class HExpFunctor f

-- | Derive an instance of <a>HExpFunctor</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
instanceHExpFunctor :: Name -> Q [Dec]

-- | Derive smart constructors for a type constructor of any higher-order
--   kind taking at least two arguments. The smart constructors are similar
--   to the ordinary constructors, but an <a>hinject</a> is automatically
--   inserted.
smartHConstructors :: Name -> Q [Dec]


-- | This module defines equality for signatures, which lifts to equality
--   for terms and contexts.
module Data.Comp.Equality

-- | Signature equality. An instance <tt>EqF f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>.
class EqF f
eqF :: (EqF f, Eq a) => f a -> f a -> Bool

-- | This function implements equality of values of type <tt>f a</tt>
--   modulo the equality of <tt>a</tt> itself. If two functorial values are
--   equal in this sense, <a>eqMod</a> returns a <a>Just</a> value
--   containing a list of pairs consisting of corresponding components of
--   the two functorial values.
eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a, b)]
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19], Eq i[1a]) => EqF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19]) => EqF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18]) => EqF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17]) => EqF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16]) => EqF ((,,,,,) a[12] b[13] c[14] d[15] e[16])
instance (Eq a[12], Eq b[13], Eq c[14], Eq d[15]) => EqF ((,,,,) a[12] b[13] c[14] d[15])
instance (Eq a[12], Eq b[13], Eq c[14]) => EqF ((,,,) a[12] b[13] c[14])
instance (Eq a[12], Eq b[13]) => EqF ((,,) a[12] b[13])
instance Eq a[12] => EqF ((,) a[12])
instance EqF Maybe
instance EqF []
instance (EqF f, Eq a) => Eq (Cxt h f a)
instance EqF f => EqF (Cxt h f)
instance (EqF f, EqF g) => EqF (f :+: g)


-- | This module implements matching of contexts or terms with variables
--   againts terms
module Data.Comp.Matching

-- | This function takes a context <tt>c</tt> as the first argument and
--   tries to match it against the term <tt>t</tt> (or in general a context
--   with holes in <tt>a</tt>). The context <tt>c</tt> matches the term
--   <tt>t</tt> if there is a <i>matching substitution</i> <tt>s</tt> that
--   maps holes to terms (resp. contexts in general) such that if the holes
--   in the context <tt>c</tt> are replaced according to the substitution
--   <tt>s</tt>, the term <tt>t</tt> is obtained. Note that the context
--   <tt>c</tt> might be non-linear, i.e. has multiple holes that are
--   equal. According to the above definition this means that holes with
--   equal holes have to be instantiated by equal terms!
matchCxt :: (Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f) => Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v)

-- | This function is similar to <a>matchCxt</a> but instead of a context
--   it matches a term with variables against a context.
matchTerm :: (Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f, HasVars f v) => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v)


-- | This module defines term rewriting systems (TRSs) using compositional
--   data types.
module Data.Comp.TermRewriting

-- | This type represents <i>recursive program schemes</i>.
type RPS f g = TermHom f g
type Var = Int

-- | This type represents term rewrite rules from signature <tt>f</tt> to
--   signature <tt>g</tt> over variables of type <tt>v</tt>
type Rule f g v = (Context f v, Context g v)

-- | This type represents term rewriting systems (TRSs) from signature
--   <tt>f</tt> to signature <tt>g</tt> over variables of type <tt>v</tt>.
type TRS f g v = [Rule f g v]
type Step t = t -> Maybe t
type BStep t = t -> (t, Bool)

-- | This function tries to match the given rule against the given term
--   (resp. context in general) at the root. If successful, the function
--   returns the right hand side of the rule and the matching substitution.
matchRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
matchRules :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))

-- | This function tries to apply the given rule at the root of the given
--   term (resp. context in general). If successful, the function returns
--   the result term of the rewrite step; otherwise <tt>Nothing</tt>.
appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f f v -> Step (Cxt h f a)

-- | This function tries to apply one of the rules in the given TRS at the
--   root of the given term (resp. context in general) by trying each rule
--   one by one using <a>appRule</a> until one rule is applicable. If no
--   rule is applicable <tt>Nothing</tt> is returned.
appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f f v -> Step (Cxt h f a)

-- | This is an auxiliary function that turns function <tt>f</tt> of type
--   <tt>(t -&gt; Maybe t)</tt> into functions <tt>f'</tt> of type <tt>t
--   -&gt; (t,Bool)</tt>. <tt>f' x</tt> evaluates to <tt>(y,True)</tt> if
--   <tt>f x</tt> evaluates to <tt>Just y</tt>, and to <tt>(x,False)</tt>
--   if <tt>f x</tt> evaluates to <tt>Nothing</tt>. This function is useful
--   to change the output of functions that apply rules such as
--   <a>appTRS</a>.
bStep :: Step t -> BStep t

-- | This function performs a parallel reduction step by trying to apply
--   rules of the given system to all outermost redexes. If the given term
--   contains no redexes, <tt>Nothing</tt> is returned.
parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)

-- | This function performs a parallel reduction step by trying to apply
--   rules of the given system to all outermost redexes and then
--   recursively in the variable positions of the redexes. If the given
--   term does not contain any redexes, <tt>Nothing</tt> is returned.
parallelStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)

-- | This function applies the given reduction step repeatedly until a
--   normal form is reached.
reduce :: Step t -> t -> t


-- | This module defines ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.Ordering

-- | Signature ordering. An instance <tt>OrdF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqF f => OrdF f
compareF :: (OrdF f, Ord a) => f a -> f a -> Ordering
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19], Ord i[1a]) => OrdF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18], Ord h[19]) => OrdF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17], Ord g[18]) => OrdF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16], Ord f[17]) => OrdF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15], Ord e[16]) => OrdF ((,,,,,) a[12] b[13] c[14] d[15] e[16])
instance (Ord a[12], Ord b[13], Ord c[14], Ord d[15]) => OrdF ((,,,,) a[12] b[13] c[14] d[15])
instance (Ord a[12], Ord b[13], Ord c[14]) => OrdF ((,,,) a[12] b[13] c[14])
instance (Ord a[12], Ord b[13]) => OrdF ((,,) a[12] b[13])
instance Ord a[12] => OrdF ((,) a[12])
instance OrdF []
instance OrdF Maybe
instance (OrdF f, OrdF g) => OrdF (f :+: g)
instance OrdF f => OrdF (Cxt h f)
instance (OrdF f, Ord a) => Ord (Cxt h f a)


-- | This module defines full evaluation of signatures, which lifts to full
--   evaluation of terms and contexts.
module Data.Comp.DeepSeq

-- | Signature normal form. An instance <tt>NFDataF f</tt> gives rise to an
--   instance <tt>NFData (Term f)</tt>.
class NFDataF f
rnfF :: (NFDataF f, NFData a) => f a -> ()

-- | Fully evaluate a value over a foldable signature.
rnfF' :: (Foldable f, NFDataF f, NFData a) => f a -> ()
instance NFData a[12] => NFDataF ((,) a[12])
instance NFDataF []
instance NFDataF Maybe
instance NFData Nothing
instance (NFDataF f, NFDataF g) => NFDataF (f :+: g)
instance (NFDataF f, NFData a) => NFData (Cxt h f a)


-- | This module defines generation of arbitrary values for signatures,
--   which lifts to generating arbitrary terms.
module Data.Comp.Arbitrary

-- | Signature arbitration. An instance <tt>ArbitraryF f</tt> gives rise to
--   an instance <tt>Arbitrary (Term f)</tt>.
class ArbitraryF f
arbitraryF' :: (ArbitraryF f, Arbitrary v) => [(Int, Gen (f v))]
arbitraryF :: (ArbitraryF f, Arbitrary v) => Gen (f v)
shrinkF :: (ArbitraryF f, Arbitrary v) => f v -> [f v]
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19], Arbitrary i[1a], Arbitrary j[1b]) => ArbitraryF ((,,,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a] j[1b])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19], Arbitrary i[1a]) => ArbitraryF ((,,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18], Arbitrary h[19]) => ArbitraryF ((,,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18] h[19])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17], Arbitrary g[18]) => ArbitraryF ((,,,,,,) b[13] c[14] d[15] e[16] f[17] g[18])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16], Arbitrary f[17]) => ArbitraryF ((,,,,,) b[13] c[14] d[15] e[16] f[17])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15], Arbitrary e[16]) => ArbitraryF ((,,,,) b[13] c[14] d[15] e[16])
instance (Arbitrary b[13], Arbitrary c[14], Arbitrary d[15]) => ArbitraryF ((,,,) b[13] c[14] d[15])
instance (Arbitrary b[13], Arbitrary c[14]) => ArbitraryF ((,,) b[13] c[14])
instance Arbitrary b[13] => ArbitraryF ((,) b[13])
instance ArbitraryF []
instance ArbitraryF Maybe
instance (ArbitraryF f, ArbitraryF g) => ArbitraryF (f :+: g)
instance (ArbitraryF f, Arbitrary a) => Arbitrary (Context f a)
instance ArbitraryF f => ArbitraryF (Context f)
instance (ArbitraryF f, Arbitrary p) => ArbitraryF (f :&: p)
instance ArbitraryF f => Arbitrary (Term f)


-- | This module defines showing of signatures, which lifts to showing of
--   terms and contexts.
module Data.Comp.Show

-- | Signature printing. An instance <tt>ShowF f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowF f
showF :: ShowF f => f String -> String
instance Show a[12] => ShowF ((,) a[12])
instance ShowF []
instance ShowF Maybe
instance (ShowF f, ShowF g) => ShowF (f :+: g)
instance (ShowF f, Show p) => ShowF (f :&: p)
instance (Functor f, ShowF f, Show a) => Show (Cxt h f a)
instance (Functor f, ShowF f) => ShowF (Cxt h f)


-- | This module defines showing of (higher-order) signatures, which lifts
--   to showing of (higher-order) terms and contexts. All definitions are
--   generalised versions of those in <a>Data.Comp.Show</a>.
module Data.Comp.Multi.Show

-- | Signature printing. An instance <tt>HShowF f</tt> gives rise to an
--   instance <tt>KShow (HTerm f)</tt>.
class HShowF f
hshowF :: HShowF f => HAlg f (K String)
hshowF' :: HShowF f => f (K String) :=> String
instance (HShowF f, HShowF g) => HShowF (f :++: g)
instance (HShowF f, Show p) => HShowF (f :&&: p)
instance KShow f => Show (f i)
instance (HShowF f, HFunctor f, KShow a) => KShow (HCxt h f a)
instance (HShowF f, HFunctor f) => HShowF (HCxt h f)
instance KShow (K String)
instance KShow HNothing


-- | This module defines equality for (higher-order) signatures, which
--   lifts to equality for (higher-order) terms and contexts. All
--   definitions are generalised versions of those in
--   <a>Data.Comp.Equality</a>.
module Data.Comp.Multi.Equality

-- | Signature equality. An instance <tt>HEqF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class HEqF f
heqF :: (HEqF f, KEq g) => f g i -> f g j -> Bool
class KEq f
keq :: KEq f => f i -> f j -> Bool

-- | This function implements equality of values of type <tt>f a</tt>
--   modulo the equality of <tt>a</tt> itself. If two functorial values are
--   equal in this sense, <tt>eqMod</tt> returns a <a>Just</a> value
--   containing a list of pairs consisting of corresponding components of
--   the two functorial values.
heqMod :: (HEqF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]
instance KEq HNothing
instance (HEqF f, KEq a) => KEq (HCxt h f a)
instance HEqF f => HEqF (HCxt h f)
instance (HEqF f, HEqF g) => HEqF (f :++: g)


-- | This module defines the infrastructure necessary to use
--   <i>Compositional Data Types</i>. Compositional Data Types is an
--   extension of Wouter Swierstra's Functional Pearl: <i>Data types a la
--   carte</i>. Examples of usage are provided below.
module Data.Comp


-- | This module defines tree automata based on compositional data types.
module Data.Comp.Automata

-- | This type represents transition functions of deterministic bottom-up
--   tree acceptors (DUTAs).
type DUTATrans f q = Alg f q

-- | This data type represents deterministic bottom-up tree acceptors
--   (DUTAs).
data DUTA f q
DUTA :: DUTATrans f q -> (q -> Bool) -> DUTA f q
dutaTrans :: DUTA f q -> DUTATrans f q
dutaAccept :: DUTA f q -> q -> Bool

-- | This function runs the transition function of a DUTA on the given
--   term.
runDUTATrans :: Functor f => DUTATrans f q -> Term f -> q

-- | This function checks whether a given DUTA accepts a term.
duta :: Functor f => DUTA f q -> Term f -> Bool

-- | This type represents transition functions of non-deterministic
--   bottom-up tree acceptors (NUTAs).
type NUTATrans f q = AlgM [] f q

-- | This type represents non-deterministic bottom-up tree acceptors.
data NUTA f q
NUTA :: AlgM [] f q -> (q -> Bool) -> NUTA f q
nutaTrans :: NUTA f q -> AlgM [] f q
nutaAccept :: NUTA f q -> q -> Bool

-- | This function runs the given transition function of a NUTA on the
--   given term
runNUTATrans :: Traversable f => NUTATrans f q -> Term f -> [q]

-- | This function checks whether a given NUTA accepts a term.
nuta :: Traversable f => NUTA f q -> Term f -> Bool

-- | This function determinises the given NUTA.
determNUTA :: Traversable f => NUTA f q -> DUTA f [q]

-- | This function represents transition functions of deterministic
--   bottom-up tree transducers (DUTTs).
type DUTTTrans f g q = forall a. f (q, a) -> (q, Cxt Hole g a)

-- | This function transforms a DUTT transition function into an algebra.
duttTransAlg :: (Functor f, Functor g) => DUTTTrans f g q -> Alg f (q, Term g)

-- | This function runs the given DUTT transition function on the given
--   term.
runDUTTTrans :: (Functor f, Functor g) => DUTTTrans f g q -> Term f -> (q, Term g)

-- | This data type represents deterministic bottom-up tree transducers.
data DUTT f g q
DUTT :: DUTTTrans f g q -> (q -> Bool) -> DUTT f g q
duttTrans :: DUTT f g q -> DUTTTrans f g q
duttAccept :: DUTT f g q -> q -> Bool

-- | This function transforms the given term according to the given DUTT
--   and returns the resulting term provided it is accepted by the DUTT.
dutt :: (Functor f, Functor g) => DUTT f g q -> Term f -> Maybe (Term g)

-- | This type represents transition functions of non-deterministic
--   bottom-up tree transducers (NUTTs).
type NUTTTrans f g q = forall a. f (q, a) -> [(q, Cxt Hole g a)]

-- | This function transforms a NUTT transition function into a monadic
--   algebra.
nuttTransAlg :: (Functor f, Functor g) => NUTTTrans f g q -> AlgM [] f (q, Term g)

-- | This function runs the given NUTT transition function on the given
--   term.
runNUTTTrans :: (Traversable f, Functor g) => NUTTTrans f g q -> Term f -> [(q, Term g)]

-- | This data type represents non-deterministic bottom-up tree transducers
--   (NUTTs).
data NUTT f g q
NUTT :: NUTTTrans f g q -> (q -> Bool) -> NUTT f g q
nuttTrans :: NUTT f g q -> NUTTTrans f g q
nuttAccept :: NUTT f g q -> q -> Bool

-- | This function transforms the given term according to the given NUTT
--   and returns a list containing all accepted results.
nutt :: (Traversable f, Functor g) => NUTT f g q -> Term f -> [Term g]