-- 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,
--   <a>http://dx.doi.org/10.1017/S0956796808006758</a>), this package
--   provides a framework for defining recursive data types in a
--   compositional manner. The fundamental idea of <i>compositional data
--   types</i> (Workshop on Generic Programming, 83-94, 2011,
--   <a>http://dx.doi.org/10.1145/2036918.2036930</a>) 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, compositional data types enable to combine data types in a
--   flexible way. The key point of Wouter Swierstra's original work is to
--   define functions on compositional data types 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 make 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 functions 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>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> and <i>generalised algebraic
--   data types (GADTs)</i>. All of the above is also lifted to families of
--   mutually recursive data types and (more generally) GADTs. This
--   extension resides in the module <a>Data.Comp.Multi</a>.</li>
--   <li><i>Parametric compositional data types</i>. All of the above is
--   also lifted to parametric data types, which enables support for
--   parametric higher-order abstract syntax (PHOAS). This extension
--   resides in the module <a>Data.Comp.Param</a>.</li>
--   <li><i>Generalised parametric compositional data types</i>. All of the
--   above is also lifted to generalised parametric data types, which
--   enables support for typed parametric higher-order abstract syntax
--   (PHOAS). This extension resides in the module
--   <a>Data.Comp.MultiParam</a>.</li>
--   </ul>
--   
--   Examples of using (generalised) (parametric) compositional data types
--   are bundled with the package in the libray <tt>examples</tt>.
@package compdata
@version 0.5


-- | This module defines a monad for generating fresh, abstract names,
--   useful e.g. for defining equality on terms.
module Data.Comp.MultiParam.FreshM

-- | Monad for generating fresh (abstract) names.
data FreshM a

-- | Abstract notion of a name (the constructor is hidden).
data Name i

-- | Run the given computation with the next available name.
withName :: (Name i -> FreshM a) -> FreshM a

-- | Change the type tag of a name.
nameCoerce :: Name i -> Name j

-- | Evaluate a computation that uses fresh names.
evalFreshM :: FreshM a -> a
instance Monad FreshM
instance Eq (Name i)
instance Ord (Name i)
instance Show (Name i)


-- | This module defines a monad for generating fresh, abstract names,
--   useful e.g. for defining equality on terms.
module Data.Comp.Param.FreshM

-- | Monad for generating fresh (abstract) names.
data FreshM a

-- | Abstract notion of a name (the constructor is hidden).
data Name

-- | Run the given computation with the next available name.
withName :: (Name -> FreshM a) -> FreshM a

-- | Evaluate a computation that uses fresh names.
evalFreshM :: FreshM a -> a
instance Monad FreshM
instance Eq Name
instance Ord Name
instance Show Name


-- | This module defines difunctors (Meijer, Hutton, FPCA '95), i.e. binary
--   type constructors that are contravariant in the first argument and
--   covariant in the second argument.
module Data.Comp.Param.Difunctor
difmap :: Difunctor f => (a -> b) -> f c a -> f c b

-- | This class represents difunctors, i.e. binary type constructors that
--   are contravariant in the first argument and covariant in the second
--   argument.
class Difunctor f
dimap :: Difunctor f => (a -> b) -> (c -> d) -> f b c -> f a d
instance Difunctor f => Functor (f a)
instance Difunctor (->)


-- | This module defines traversable difunctors.
module Data.Comp.Param.Ditraversable

-- | Difunctors representing data structures that can be traversed from
--   left to right.
class Difunctor f => Ditraversable f
dimapM :: (Ditraversable f, Monad m) => (b -> m c) -> f a b -> m (f a c)
disequence :: (Ditraversable f, Monad m) => f a (m b) -> m (f a b)


-- | This module provides operators on difunctors.
module Data.Comp.Param.Ops

-- | Formal sum of signatures (difunctors).
data (:+:) f g a b
Inl :: (f a b) -> :+: f g a b
Inr :: (g a b) -> :+: f g a b

-- | 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 b -> sup a b
proj :: :<: sub sup => sup a b -> Maybe (sub a b)

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

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

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a b -> s' a b
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'
remA :: RemA s s' => s a b -> s' a b
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] Ditraversable f => Ditraversable (f :&: p)
instance [incoherent] Difunctor f => Difunctor (f :&: p)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (Ditraversable f, Ditraversable g) => Ditraversable (f :+: g)
instance [incoherent] (Difunctor f, Difunctor g) => Difunctor (f :+: g)


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

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes, and zero or more parameters. The
--   first parameter is a phantom type indicating whether the context has
--   holes. The second paramater is the signature of the context, in the
--   form of a <a>Data.Comp.Param.Difunctor</a>. The third parameter is the
--   type of parameters, and the fourth parameter is the type of holes.
data Cxt :: * -> (* -> * -> *) -> * -> * -> *
In :: f a (Cxt h f a b) -> Cxt h f a b
Hole :: b -> Cxt Hole f a b
Var :: a -> Cxt h f a b

-- | Phantom type used to define <a>Context</a>.
data Hole

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

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric.
newtype Term f
Term :: (forall a. Trm f a) -> Term f
unTerm :: Term f -> forall a. Trm f a

-- | "Preterms"
type Trm f a = Cxt NoHole f a ()

-- | A context may contain holes.
type Context = Cxt Hole

-- | Convert a difunctorial value into a context.
simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
toCxt :: Difunctor f => Trm f a -> Cxt h f a b

-- | Monads for which embedded <tt>Trm</tt> values, which are parametric at
--   top level, can be made into monadic <tt>Term</tt> values, i.e.
--   "pushing the parametricity inwards".
class ParamFunctor m
termM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)
instance ParamFunctor []
instance ParamFunctor (Either a)
instance ParamFunctor Maybe


-- | 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.Param.Algebra

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

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

-- | Construct a catamorphism from the given algebra.
cata :: Difunctor 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' :: Difunctor f => Alg f a -> Cxt h f a a -> a

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

-- | 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 a -> m a

-- | Convert a monadic algebra into an ordinary algebra with a monadic
--   carrier.
algM :: (Ditraversable 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>b</tt>, from the given monadic algebra.
freeM :: (Ditraversable f, Monad m) => AlgM m f a -> (b -> m a) -> Cxt h f a b -> m a

-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: (Ditraversable 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' :: (Ditraversable f, Monad m) => AlgM m f a -> Cxt h f a (m a) -> m a

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

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

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

-- | Apply a term homomorphism recursively to a term/context.
appHom :: (Difunctor f, Difunctor g) => Hom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context.
appHom' :: Difunctor g => Hom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compHom :: (Difunctor g, Difunctor h) => Hom g h -> Hom f g -> Hom f h

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

-- | This function applies a signature function to the given context. This
--   is a top-bottom variant of <a>appSigFun</a>.
appSigFun' :: Difunctor g => SigFun f g -> CxtFun f g

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

-- | This function composes a term homomorphism and a signature function.
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h

-- | This function composes a term homomorphism and a signature function.
compSigFunHom :: Difunctor g => SigFun g h -> Hom f g -> Hom f h

-- | Lifts the given signature function to the canonical term homomorphism.
hom :: Difunctor g => SigFun f g -> Hom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (Difunctor f, Difunctor g) => Alg g a -> Hom f g -> Alg f a
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a

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

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

-- | This type represents a monadic term homomorphism.
type HomM 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 SigFunMD m f g = forall a b. f a (m b) -> m (g a b)

-- | This type represents a monadic term homomorphism. It is similar to
--   <a>HomM</a> but has monadic values also in the domain.
type HomMD m f g = SigFunMD 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

-- | Apply a monadic term homomorphism recursively to a term/context. The
--   monad is sequenced bottom-up.
appHomM :: (Ditraversable f, Difunctor g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM| which only works for terms.
appTHomM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => HomM m f g -> Term f -> m (Term g)

-- | Apply a monadic term homomorphism recursively to a term/context. The
--   monad is sequence top-down.
appHomM' :: (Ditraversable g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM'| which only works for terms.
appTHomM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g) => HomM m f g -> Term f -> m (Term g)

-- | Lift the given signature function to a monadic term homomorphism.
homM :: (Difunctor g, Monad m) => SigFunM m f g -> HomM m f g

-- | This function constructs the unique monadic homomorphism from the
--   initial term algebra to the given term algebra.
homMD :: (Difunctor f, Difunctor g, Monad m) => HomMD m f g -> CxtFunM m f g

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

-- | A restricted form of |appSigFunM| which only works for terms.
appTSigFunM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => SigFunM m f g -> Term f -> m (Term g)

-- | This function applies a monadic signature function to the given
--   context. This is a 'top-down variant of <a>appSigFunM</a>.
appSigFunM' :: (Ditraversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM'| which only works for terms.
appTSigFunM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g) => SigFunM m f g -> Term f -> m (Term g)

-- | This function applies a signature function to the given context.
appSigFunMD :: (Ditraversable f, Difunctor g, Monad m) => SigFunMD m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunMD| which only works for terms.
appTSigFunMD :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g) => SigFunMD m f g -> Term f -> m (Term g)

-- | Compose two monadic term homomorphisms.
compHomM :: (Ditraversable g, Difunctor h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h

-- | Compose two monadic term homomorphisms.
compHomM' :: (Ditraversable h, Monad m) => HomM m g h -> HomM m f g -> HomM 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 two monadic term homomorphisms.
compSigFunHomM :: (Ditraversable g, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h

-- | Compose two monadic term homomorphisms.
compSigFunHomM' :: (Ditraversable h, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h

-- | Compose a monadic algebra with a monadic signature function to get a
--   new monadic algebra.
compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a

-- | Compose a monadic algebra with a signature function to get a new
--   monadic algebra.
compAlgSigFunM' :: AlgM m g a -> SigFun f g -> AlgM m f a

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

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

-- | This type represents a coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>. The list of <tt>(a,b)</tt>s represent the
--   parameters that may occur in the constructed value. The first
--   component represents the seed of the parameter, and the second
--   component is the (polymorphic) parameter itself. If <tt>f</tt> is
--   itself a binder, then the parameters bound by <tt>f</tt> can be passed
--   to the covariant argument, thereby making them available to sub terms.
type Coalg f a = forall b. a -> [(a, b)] -> Either b (f b (a, [(a, b)]))

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

-- | This type represents a monadic coalgebra over a difunctor <tt>f</tt>
--   and carrier <tt>a</tt>.
type CoalgM m f a = forall b. a -> [(a, b)] -> m (Either b (f b (a, [(a, b)])))

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

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

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

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

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

-- | This type represents an r-coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>.
type RCoalg f a = forall b. a -> [(a, b)] -> Either b (f b (Either (Trm f b) (a, [(a, b)])))

-- | Construct an apomorphism from the given r-coalgebra.
apo :: Difunctor 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 = forall b. a -> [(a, b)] -> m (Either b (f b (Either (Trm f b) (a, [(a, b)]))))

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

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

-- | Construct a histomorphism from the given cv-algebra.
histo :: (Difunctor f, DistAnn 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 a (Trm f' a) -> m a

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

-- | This type represents a cv-coalgebra over a difunctor <tt>f</tt> and
--   carrier <tt>a</tt>. The list of <tt>(a,b)</tt>s represent the
--   parameters that may occur in the constructed value. The first
--   component represents the seed of the parameter, and the second
--   component is the (polymorphic) parameter itself. If <tt>f</tt> is
--   itself a binder, then the parameters bound by <tt>f</tt> can be passed
--   to the covariant argument, thereby making them available to sub terms.
type CVCoalg f a = forall b. a -> [(a, b)] -> Either b (f b (Context f b (a, [(a, b)])))

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

-- | This type represents a generalised cv-coalgebra over a difunctor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalg' f a = forall b. a -> [(a, b)] -> Context f b (a, [(a, b)])

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

-- | This type represents a monadic cv-coalgebra over a difunctor
--   <tt>f</tt> and carrier <tt>a</tt>.
type CVCoalgM m f a = forall b. a -> [(a, b)] -> m (Either b (f b (Context f b (a, [(a, b)]))))

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


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.Param.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 b -> sup a b
proj :: :<: sub sup => sup a b -> Maybe (sub a b)

-- | Formal sum of signatures (difunctors).
data (:+:) f g a b
proj2 :: (:<: g1 f, :<: g2 f) => f a b -> Maybe (:+: g2 g1 a b)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a b -> Maybe (:+: g3 (:+: g2 g1) a b)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b)
proj6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a b)
proj7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a b)
proj8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => f a b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b)
proj9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => f a b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b)
proj10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => f a b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: :<: g f => Cxt h f a b -> Maybe (g a (Cxt h f a b))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a b -> Maybe (:+: g2 g1 a (Cxt h f a b))
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b))
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a b -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a (Cxt h f a b))
project5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a b -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a (Cxt h f a b))
project6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a b -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a (Cxt h f a b))
project7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Cxt h f a b -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b))
project8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Cxt h f a b -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b))
project9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Cxt h f a b -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b))
project10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Cxt h f a b -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b))

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (Ditraversable g, :<: g f) => Term f -> Maybe (Term g)
deepProject2 :: (Ditraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => Term f -> Maybe (Term (:+: g2 g1))
deepProject3 :: (Ditraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => Term f -> Maybe (Term (:+: g3 (:+: g2 g1)))
deepProject4 :: (Ditraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Term f -> Maybe (Term (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject5 :: (Ditraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Term f -> Maybe (Term (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
deepProject6 :: (Ditraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Term f -> Maybe (Term (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))
deepProject7 :: (Ditraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Term f -> Maybe (Term (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))
deepProject8 :: (Ditraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Term f -> Maybe (Term (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))
deepProject9 :: (Ditraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Term f -> Maybe (Term (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))
deepProject10 :: (Ditraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Term f -> Maybe (Term (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a b -> g a b
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b -> g a b
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b -> g a b
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b -> g a b
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a b -> g a b
inj7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a b -> g a b
inj8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a b -> g a b
inj9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a b -> g a b
inj10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a b -> g a b

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: :<: g f => g a (Cxt h f a b) -> Cxt h f a b

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject' :: (Difunctor g, :<: g f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) -> Cxt h g a b
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) -> Cxt h g a b
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) -> Cxt h g a b
inject5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a (Cxt h g a b) -> Cxt h g a b
inject6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a (Cxt h g a b) -> Cxt h g a b
inject7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a (Cxt h g a b) -> Cxt h g a b
inject8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a (Cxt h g a b) -> Cxt h g a b
inject9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a (Cxt h g a b) -> Cxt h g a b
inject10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a (Cxt h g a b) -> Cxt h g a b

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (Difunctor g, :<: g f) => Term g -> Term f
deepInject2 :: (Difunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (Difunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (Difunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (Difunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (Difunctor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) g
deepInject7 :: (Difunctor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) g
deepInject8 :: (Difunctor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) g
deepInject9 :: (Difunctor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) g
deepInject10 :: (Difunctor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) g

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

-- | This function lifts the given functor to a context.
liftCxt :: (Difunctor f, :<: g f) => g a b -> Cxt Hole f a b
instance [incoherent] (Eq (f a b), Eq (g a b)) => Eq ((:+:) f g a b)
instance [incoherent] (Ord (f a b), Ord (g a b)) => Ord ((:+:) f g a b)
instance [incoherent] (Show (f a b), Show (g a b)) => Show ((:+:) f g a b)


-- | This module defines annotations on signatures.
module Data.Comp.Param.Annotation

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

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

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a b -> s' a b
projectA :: DistAnn s p s' => s' a b -> (s a b, p)
class RemA s s' | s -> s'
remA :: RemA s s' => s a b -> s' a b

-- | 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 annotation.
liftA :: RemA s s' => (s' a b -> t) -> s a b -> 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 annotation.
liftA' :: (DistAnn s' p s, Difunctor s') => (s' a b -> Cxt h s' c d) -> s a b -> Cxt h s c d

-- | Strip the annotations from a term over a functor with annotations.
stripA :: (RemA g f, Difunctor g) => CxtFun g f

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   annotations.
propAnn :: (DistAnn f p f', DistAnn g p g', Difunctor g) => Hom f g -> Hom f' g'

-- | Lift a monadic term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a monadic term homomorphism over the same signatures,
--   but extended with annotations.
propAnnM :: (DistAnn f p f', DistAnn g p g', Difunctor g, Monad m) => HomM m f g -> HomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, Difunctor f) => p -> CxtFun f g
project' :: (RemA s s', :<: s f) => Cxt h f a b -> Maybe (s' a (Cxt h f a b))


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

-- | Equality on parametric values. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class PEq a
peq :: PEq a => a -> a -> FreshM Bool

-- | Signature equality. An instance <tt>EqD f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqD f
eqD :: (EqD f, PEq a) => f Name a -> f Name a -> FreshM Bool
instance [incoherent] (Difunctor f, EqD f) => Eq (Term f)
instance [incoherent] (EqD f, PEq a) => PEq (Cxt h f Name a)
instance [incoherent] EqD f => EqD (Cxt h f)
instance [incoherent] (EqD f, EqD g) => EqD (f :+: g)
instance [incoherent] Eq a => PEq a
instance [incoherent] PEq a => PEq [a]


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

-- | Ordering of parametric values.
class PEq a => POrd a
pcompare :: POrd a => a -> a -> FreshM Ordering

-- | Signature ordering. An instance <tt>OrdD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqD f => OrdD f
compareD :: (OrdD f, POrd a) => f Name a -> f Name a -> FreshM Ordering
compList :: [Ordering] -> Ordering
instance [incoherent] (Difunctor f, OrdD f) => Ord (Term f)
instance [incoherent] (OrdD f, POrd a) => POrd (Cxt h f Name a)
instance [incoherent] OrdD f => OrdD (Cxt h f)
instance [incoherent] (OrdD f, OrdD g) => OrdD (f :+: g)
instance [incoherent] Ord a => POrd a
instance [incoherent] POrd a => POrd [a]


-- | This modules defines terms &amp; contexts with thunks, with deferred
--   monadic computations.
module Data.Comp.Param.Thunk

-- | This type represents terms with thunks.
type TermT m f = Term (Thunk m :+: f)

-- | This type represents terms with thunks.
type TrmT m f a = Trm (Thunk m :+: f) a

-- | This type represents contexts with thunks.
type CxtT h m f a = Cxt h (Thunk m :+: f) a
data Thunk m a b

-- | This function turns a monadic computation into a thunk.
thunk :: :<: (Thunk m) f => m (Cxt h f a b) -> Cxt h f a b

-- | This function evaluates all thunks until a non-thunk node is found.
whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))
whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)

-- | This function first evaluates the argument term into whnf via
--   <a>whnf</a> and then projects the top-level signature to the desired
--   subsignature. Failure to do the projection is signalled as a failure
--   in the monad.
whnfPr :: (Monad m, :<: g f) => TrmT m f a -> m (g a (TrmT m f a))

-- | This function evaluates all thunks.
nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)

-- | This function evaluates all thunks.
nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)

-- | This function evaluates all thunks while simultaneously projecting the
--   term to a smaller signature. Failure to do the projection is signalled
--   as a failure in the monad as in <a>whnfPr</a>.
nfPr :: (Monad m, Ditraversable g, :<: g f) => TrmT m f a -> m (Trm g a)

-- | This function evaluates all thunks while simultaneously projecting the
--   term to a smaller signature. Failure to do the projection is signalled
--   as a failure in the monad as in <a>whnfPr</a>.
nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, :<: g f) => TermT m f -> m (Term g)
evalStrict :: (Ditraversable g, Monad m, :<: g f) => (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a) -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a

-- | This type represents algebras which have terms with thunks as carrier.
type AlgT m f g = Alg f (TermT m g)

-- | This combinator makes the evaluation of the given functor application
--   strict by evaluating all thunks of immediate subterms.
strict :: (:<: f g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a

-- | This combinator makes the evaluation of the given functor application
--   strict by evaluating all thunks of immediate subterms.
strict' :: (:<: f g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a


-- | This module defines the infrastructure necessary to use <i>Parametric
--   Compositional Data Types</i>. Parametric Compositional Data Types is
--   an extension of Compositional Data Types with parametric higher-order
--   abstract syntax (PHOAS) for usage with binders. Examples of usage are
--   bundled with the package in the library
--   <tt>examples/Examples/Param</tt>.
module Data.Comp.Param


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

-- | 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.
newtype I a
I :: a -> I a
unI :: I a -> a

-- | The parametrised constant functor.
newtype K a i
K :: a -> K a i
unK :: K a i -> 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 foldable functors.
module Data.Comp.Multi.HFoldable

-- | 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.HTraversable
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 higher-order difunctors, a hybrid between
--   higher-order functors (Johann, Ghani, POPL '08), and difunctors
--   (Meijer, Hutton, FPCA '95). Higher-order difunctors are used to define
--   signatures for compositional parametric generalised data types.
module Data.Comp.MultiParam.HDifunctor

-- | This class represents higher-order difunctors.
class HDifunctor f
hdimap :: HDifunctor f => (a :-> b) -> (c :-> d) -> f b c :-> f a d

-- | 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

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

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

-- | This type represents natural transformations.
type :-> f g = forall i. f i -> g i
type NatM m f g = forall i. f i -> m (g i)
instance HDifunctor f => HFunctor (f a)


-- | This module defines traversable higher-order difunctors.
module Data.Comp.MultiParam.HDitraversable

-- | HDifunctors representing data structures that can be traversed from
--   left to right.
class HDifunctor f => HDitraversable f
hdimapM :: (HDitraversable f, Monad m) => NatM m b c -> NatM m (f a b) (f a c)
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 <i>generalised parametrised
--   terms</i> and their generalisation to generalised parametrised
--   contexts.
module Data.Comp.MultiParam.Term

-- | This data type represents contexts over a signature. Contexts are
--   terms containing zero or more holes, and zero or more parameters. The
--   first parameter is a phantom type indicating whether the context has
--   holes. The second paramater is the signature of the context, in the
--   form of a <a>Data.Comp.MultiParam.HDifunctor</a>. The third parameter
--   is the type of parameters, the fourth parameter is the type of holes,
--   and the fifth parameter is the GADT type.
data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> *
In :: f a (Cxt h f a b) i -> Cxt h f a b i
Hole :: b i -> Cxt Hole f a b i
Var :: a i -> Cxt h f a b i

-- | Phantom type used to define <a>Context</a>.
data Hole

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

-- | A term is a context with no holes, where all occurrences of the
--   contravariant parameter is fully parametric.
newtype Term f i
Term :: (forall a. Trm f a i) -> Term f i
unTerm :: Term f i -> forall a. Trm f a i

-- | "Preterms" |
type Trm f a = Cxt NoHole f a (K ())

-- | A context may contain holes.
type Context = Cxt Hole

-- | Convert a difunctorial value into a context.
simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b

-- | This is an instance of <a>hfmap</a> for <a>Cxt</a>.
hfmapCxt :: HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'

-- | This is an instance of <a>hdimapM</a> for <a>Cxt</a>.
hdimapMCxt :: (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')

-- | Monads for which embedded <tt>Trm</tt> values, which are parametric at
--   top level, can be made into monadic <tt>Term</tt> values, i.e.
--   "pushing the parametricity inwards".
class ParamFunctor m
termM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)
instance ParamFunctor []
instance ParamFunctor (Either a)
instance ParamFunctor Maybe


-- | 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.MultiParam.Algebra

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

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

-- | Construct a catamorphism from the given algebra.
cata :: HDifunctor 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' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a

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

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

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

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

-- | This type represents a monadic algebra, but where the covariant
--   argument is also a monadic computation.
type AlgM' m f a = NatM m (f a (Compose m a)) a

-- | Right-to-left composition of functors. The composition of applicative
--   functors is always applicative, but the composition of monads is not
--   always a monad.
newtype Compose f :: (* -> *) g :: (* -> *) a :: (* -> *) -> (* -> *) -> * -> *
Compose :: f (g a) -> Compose a
getCompose :: Compose a -> f (g a)

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

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

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

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

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

-- | Apply a term homomorphism recursively to a term/context.
appHom :: (HDifunctor f, HDifunctor g) => Hom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context. This is a
--   top-down variant of <a>appHom</a>.
appHom' :: HDifunctor g => Hom f g -> CxtFun f g

-- | Compose two term homomorphisms.
compHom :: (HDifunctor g, HDifunctor h) => Hom g h -> Hom f g -> Hom f h

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

-- | This function applies a signature function to the given context.
appSigFun' :: HDifunctor 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.
hom :: HDifunctor g => SigFun f g -> Hom f g

-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> Hom f g -> Alg f a

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

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

-- | This type represents a monadic term homomorphism.
type HomM m f g = SigFunM m f (Cxt Hole 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.
hom' :: (HDifunctor f, HDifunctor g, Monad m) => SigFunM m f g -> HomM m f g

-- | Apply a monadic term homomorphism recursively to a term/context.
appHomM :: (HDitraversable f, Monad m, HDifunctor g) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM| which only works for terms.
appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g) => HomM m f g -> Term f i -> m (Term g i)

-- | Apply a monadic term homomorphism recursively to a term/context. This
--   is a top-down variant of <a>appHomM</a>.
appHomM' :: (HDitraversable g, Monad m) => HomM m f g -> CxtFunM m f g

-- | A restricted form of |appHomM'| which only works for terms.
appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g) => HomM m f g -> Term f i -> m (Term g i)

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

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

-- | A restricted form of |appSigFunM| which only works for terms.
appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g) => SigFunM m f g -> Term f i -> m (Term g i)

-- | This function applies a monadic signature function to the given
--   context. This is a top-down variant of <a>appSigFunM</a>.
appSigFunM' :: (HDitraversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | A restricted form of |appSigFunM'| which only works for terms.
appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g) => SigFunM m f g -> Term f i -> m (Term g i)

-- | Compose two monadic term homomorphisms.
compHomM :: (HDitraversable g, HDifunctor h, Monad m) => HomM m g h -> HomM m f g -> HomM 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 :: (HDitraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a

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


-- | 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>Hole</a> and <a>NoHole</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 Cxt h f a i
Term :: f (Cxt h f a) i -> Cxt h f a i
Hole :: a i -> Cxt Hole f a i

-- | 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

-- | A context might contain holes.
type Context = Cxt Hole

-- | A (higher-order) term is a context with no holes.
type Term f = Cxt NoHole f (K ())
type Const 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.
constTerm :: HFunctor f => Const f :-> Term f

-- | This function unravels the given term at the topmost layer.
unTerm :: Term f t -> f (Term f) t

-- | Cast a term over a signature to a context over the same signature.
toCxt :: HFunctor f => Term f :-> Context f a
simpCxt :: HFunctor f => f a i -> Context f a i
instance [incoherent] HTraversable f => HTraversable (Cxt h f)
instance [incoherent] HFoldable f => HFoldable (Cxt h f)
instance [incoherent] HFunctor f => HFunctor (Cxt h f)


module Data.Comp.Zippable

-- | Instances of this class provide a generalisation of the zip function
--   on the list functor.
class Functor f => Zippable f
fzip :: Zippable f => Stream a -> f b -> f (a, b)
fzipWith :: Zippable f => (a -> b -> c) -> Stream a -> f b -> f c

-- | This type is used for applying a DDTAs.
newtype Numbered a
Numbered :: (Int, a) -> Numbered a
unNumbered :: Numbered a -> a
number :: Zippable f => f a -> f (Numbered a)
number' :: Zippable f => f a -> f (Int, a)
data Stream a
Cons :: a -> (Stream a) -> Stream a

-- | The <tt> &lt;:&gt; </tt> operator is an infix version of the
--   <a>Cons</a> constructor.
(<:>) :: a -> Stream a -> Stream a
instance Eq a => Eq (Stream a)
instance Ord a => Ord (Stream a)
instance Zippable []
instance Ord (Numbered a)
instance Eq (Numbered a)


module Data.Comp.Automata.Product

-- | An instance <tt>a :&lt; b</tt> means that <tt>a</tt> is a component of
--   <tt>b</tt>. <tt>a</tt> can be extracted from <tt>b</tt> via the method
--   <tt>ex</tt>.
class :< a b
pr :: :< a b => b -> a
up :: :< a b => a -> b -> b
instance [incoherent] c :< b => c :< (a, b)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, (a6, (a7, a0))))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, (a6, (a0, a7))))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, (a6, a0)))))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, ((a6, a0), a7)))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, ((a0, a6), a7)))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, (a0, a6)))))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a5, a0))))), a6)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, ((a5, (a6, a0)), a7))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, ((a5, (a0, a6)), a7))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, ((a5, a0), a6))))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (((a5, a0), a6), a7))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (((a0, a5), a6), a7))))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, ((a0, a5), a6))))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, (a0, a5))))), a6)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a4, a0)))), a5)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, (a5, (a6, a0))), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, (a5, (a0, a6))), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, (a5, a0)), a6)))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, ((a5, a0), a6)), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, ((a0, a5), a6)), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, (a0, a5)), a6)))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a4, a0), a5)))), a6)
instance [incoherent] a0 :< ((a1, (a2, (a3, (((a4, (a5, a0)), a6), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (((a4, (a0, a5)), a6), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (((a4, a0), a5), a6)))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((((a4, a0), a5), a6), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((((a0, a4), a5), a6), a7)))), a8)
instance [incoherent] a0 :< ((a1, (a2, (a3, (((a0, a4), a5), a6)))), a7)
instance [incoherent] a0 :< ((a1, (a2, (a3, ((a0, a4), a5)))), a6)
instance [incoherent] a0 :< ((a1, (a2, (a3, (a0, a4)))), a5)
instance [incoherent] a0 :< ((a1, (a2, (a3, a0))), a4)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, (a5, (a6, a0)))), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, (a5, (a0, a6)))), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, (a5, a0))), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, ((a5, a0), a6))), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, ((a0, a5), a6))), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, (a0, a5))), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a4, a0)), a5))), a6)
instance [incoherent] a0 :< ((a1, (a2, ((a3, ((a4, (a5, a0)), a6)), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, ((a4, (a0, a5)), a6)), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, ((a4, a0), a5)), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (((a4, a0), a5), a6)), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (((a0, a4), a5), a6)), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((a3, ((a0, a4), a5)), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, ((a3, (a0, a4)), a5))), a6)
instance [incoherent] a0 :< ((a1, (a2, ((a3, a0), a4))), a5)
instance [incoherent] a0 :< ((a1, (a2, (((a3, (a4, (a5, a0))), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, (((a3, (a4, (a0, a5))), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, (((a3, (a4, a0)), a5), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, (((a3, ((a4, a0), a5)), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, (((a3, ((a0, a4), a5)), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, (((a3, (a0, a4)), a5), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, (((a3, a0), a4), a5))), a6)
instance [incoherent] a0 :< ((a1, (a2, ((((a3, (a4, a0)), a5), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((((a3, (a0, a4)), a5), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((((a3, a0), a4), a5), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, (((((a3, a0), a4), a5), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, (((((a0, a3), a4), a5), a6), a7))), a8)
instance [incoherent] a0 :< ((a1, (a2, ((((a0, a3), a4), a5), a6))), a7)
instance [incoherent] a0 :< ((a1, (a2, (((a0, a3), a4), a5))), a6)
instance [incoherent] a0 :< ((a1, (a2, ((a0, a3), a4))), a5)
instance [incoherent] a0 :< ((a1, (a2, (a0, a3))), a4)
instance [incoherent] a0 :< ((a1, (a2, a0)), a3)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, (a5, (a6, a0))))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, (a5, (a0, a6))))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, (a5, a0)))), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, ((a5, a0), a6)))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, ((a0, a5), a6)))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, (a0, a5)))), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a4, a0))), a5)), a6)
instance [incoherent] a0 :< ((a1, ((a2, (a3, ((a4, (a5, a0)), a6))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, ((a4, (a0, a5)), a6))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, ((a4, a0), a5))), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (((a4, a0), a5), a6))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (((a0, a4), a5), a6))), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (a3, ((a0, a4), a5))), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, (a3, (a0, a4))), a5)), a6)
instance [incoherent] a0 :< ((a1, ((a2, (a3, a0)), a4)), a5)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, (a4, (a5, a0))), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, (a4, (a0, a5))), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, (a4, a0)), a5)), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, ((a4, a0), a5)), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, ((a0, a4), a5)), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, (a0, a4)), a5)), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, ((a3, a0), a4)), a5)), a6)
instance [incoherent] a0 :< ((a1, ((a2, (((a3, (a4, a0)), a5), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (((a3, (a0, a4)), a5), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (((a3, a0), a4), a5)), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, ((((a3, a0), a4), a5), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, ((((a0, a3), a4), a5), a6)), a7)), a8)
instance [incoherent] a0 :< ((a1, ((a2, (((a0, a3), a4), a5)), a6)), a7)
instance [incoherent] a0 :< ((a1, ((a2, ((a0, a3), a4)), a5)), a6)
instance [incoherent] a0 :< ((a1, ((a2, (a0, a3)), a4)), a5)
instance [incoherent] a0 :< ((a1, ((a2, a0), a3)), a4)
instance [incoherent] a0 :< ((a1, (((a2, (a3, (a4, (a5, a0)))), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, (a3, (a4, (a0, a5)))), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, (a3, (a4, a0))), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, (((a2, (a3, ((a4, a0), a5))), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, (a3, ((a0, a4), a5))), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, (a3, (a0, a4))), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, (((a2, (a3, a0)), a4), a5)), a6)
instance [incoherent] a0 :< ((a1, (((a2, ((a3, (a4, a0)), a5)), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, ((a3, (a0, a4)), a5)), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, ((a3, a0), a4)), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, (((a2, (((a3, a0), a4), a5)), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, (((a0, a3), a4), a5)), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((a2, ((a0, a3), a4)), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, (((a2, (a0, a3)), a4), a5)), a6)
instance [incoherent] a0 :< ((a1, (((a2, a0), a3), a4)), a5)
instance [incoherent] a0 :< ((a1, ((((a2, (a3, (a4, a0))), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, ((((a2, (a3, (a0, a4))), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, ((((a2, (a3, a0)), a4), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, ((((a2, ((a3, a0), a4)), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, ((((a2, ((a0, a3), a4)), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, ((((a2, (a0, a3)), a4), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, ((((a2, a0), a3), a4), a5)), a6)
instance [incoherent] a0 :< ((a1, (((((a2, (a3, a0)), a4), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((((a2, (a0, a3)), a4), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((((a2, a0), a3), a4), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, ((((((a2, a0), a3), a4), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, ((((((a0, a2), a3), a4), a5), a6), a7)), a8)
instance [incoherent] a0 :< ((a1, (((((a0, a2), a3), a4), a5), a6)), a7)
instance [incoherent] a0 :< ((a1, ((((a0, a2), a3), a4), a5)), a6)
instance [incoherent] a0 :< ((a1, (((a0, a2), a3), a4)), a5)
instance [incoherent] a0 :< ((a1, ((a0, a2), a3)), a4)
instance [incoherent] a0 :< ((a1, (a0, a2)), a3)
instance [incoherent] a0 :< ((a1, a0), a2)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, (a5, (a6, a0)))))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, (a5, (a0, a6)))))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, (a5, a0))))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, ((a5, a0), a6))))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, ((a0, a5), a6))))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, (a0, a5))))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a4, a0)))), a5), a6)
instance [incoherent] a0 :< (((a1, (a2, (a3, ((a4, (a5, a0)), a6)))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, ((a4, (a0, a5)), a6)))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, ((a4, a0), a5)))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, (a3, (((a4, a0), a5), a6)))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, (((a0, a4), a5), a6)))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (a3, ((a0, a4), a5)))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, (a3, (a0, a4)))), a5), a6)
instance [incoherent] a0 :< (((a1, (a2, (a3, a0))), a4), a5)
instance [incoherent] a0 :< (((a1, (a2, ((a3, (a4, (a5, a0))), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, ((a3, (a4, (a0, a5))), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, ((a3, (a4, a0)), a5))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, ((a3, ((a4, a0), a5)), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, ((a3, ((a0, a4), a5)), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, ((a3, (a0, a4)), a5))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, ((a3, a0), a4))), a5), a6)
instance [incoherent] a0 :< (((a1, (a2, (((a3, (a4, a0)), a5), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (((a3, (a0, a4)), a5), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (((a3, a0), a4), a5))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, ((((a3, a0), a4), a5), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, ((((a0, a3), a4), a5), a6))), a7), a8)
instance [incoherent] a0 :< (((a1, (a2, (((a0, a3), a4), a5))), a6), a7)
instance [incoherent] a0 :< (((a1, (a2, ((a0, a3), a4))), a5), a6)
instance [incoherent] a0 :< (((a1, (a2, (a0, a3))), a4), a5)
instance [incoherent] a0 :< (((a1, (a2, a0)), a3), a4)
instance [incoherent] a0 :< (((a1, ((a2, (a3, (a4, (a5, a0)))), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, (a3, (a4, (a0, a5)))), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, (a3, (a4, a0))), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, ((a2, (a3, ((a4, a0), a5))), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, (a3, ((a0, a4), a5))), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, (a3, (a0, a4))), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, ((a2, (a3, a0)), a4)), a5), a6)
instance [incoherent] a0 :< (((a1, ((a2, ((a3, (a4, a0)), a5)), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, ((a3, (a0, a4)), a5)), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, ((a3, a0), a4)), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, ((a2, (((a3, a0), a4), a5)), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, (((a0, a3), a4), a5)), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((a2, ((a0, a3), a4)), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, ((a2, (a0, a3)), a4)), a5), a6)
instance [incoherent] a0 :< (((a1, ((a2, a0), a3)), a4), a5)
instance [incoherent] a0 :< (((a1, (((a2, (a3, (a4, a0))), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, (((a2, (a3, (a0, a4))), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, (((a2, (a3, a0)), a4), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, (((a2, ((a3, a0), a4)), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, (((a2, ((a0, a3), a4)), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, (((a2, (a0, a3)), a4), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, (((a2, a0), a3), a4)), a5), a6)
instance [incoherent] a0 :< (((a1, ((((a2, (a3, a0)), a4), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((((a2, (a0, a3)), a4), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((((a2, a0), a3), a4), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, (((((a2, a0), a3), a4), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, (((((a0, a2), a3), a4), a5), a6)), a7), a8)
instance [incoherent] a0 :< (((a1, ((((a0, a2), a3), a4), a5)), a6), a7)
instance [incoherent] a0 :< (((a1, (((a0, a2), a3), a4)), a5), a6)
instance [incoherent] a0 :< (((a1, ((a0, a2), a3)), a4), a5)
instance [incoherent] a0 :< (((a1, (a0, a2)), a3), a4)
instance [incoherent] a0 :< (((a1, a0), a2), a3)
instance [incoherent] a0 :< ((((a1, (a2, (a3, (a4, (a5, a0))))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, (a3, (a4, (a0, a5))))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, (a3, (a4, a0)))), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, (a2, (a3, ((a4, a0), a5)))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, (a3, ((a0, a4), a5)))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, (a3, (a0, a4)))), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, (a2, (a3, a0))), a4), a5), a6)
instance [incoherent] a0 :< ((((a1, (a2, ((a3, (a4, a0)), a5))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, ((a3, (a0, a4)), a5))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, ((a3, a0), a4))), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, (a2, (((a3, a0), a4), a5))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, (((a0, a3), a4), a5))), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (a2, ((a0, a3), a4))), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, (a2, (a0, a3))), a4), a5), a6)
instance [incoherent] a0 :< ((((a1, (a2, a0)), a3), a4), a5)
instance [incoherent] a0 :< ((((a1, ((a2, (a3, (a4, a0))), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, ((a2, (a3, (a0, a4))), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, ((a2, (a3, a0)), a4)), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, ((a2, ((a3, a0), a4)), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, ((a2, ((a0, a3), a4)), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, ((a2, (a0, a3)), a4)), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, ((a2, a0), a3)), a4), a5), a6)
instance [incoherent] a0 :< ((((a1, (((a2, (a3, a0)), a4), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (((a2, (a0, a3)), a4), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (((a2, a0), a3), a4)), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, ((((a2, a0), a3), a4), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, ((((a0, a2), a3), a4), a5)), a6), a7), a8)
instance [incoherent] a0 :< ((((a1, (((a0, a2), a3), a4)), a5), a6), a7)
instance [incoherent] a0 :< ((((a1, ((a0, a2), a3)), a4), a5), a6)
instance [incoherent] a0 :< ((((a1, (a0, a2)), a3), a4), a5)
instance [incoherent] a0 :< ((((a1, a0), a2), a3), a4)
instance [incoherent] a0 :< (((((a1, (a2, (a3, (a4, a0)))), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, (a2, (a3, (a0, a4)))), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, (a2, (a3, a0))), a4), a5), a6), a7)
instance [incoherent] a0 :< (((((a1, (a2, ((a3, a0), a4))), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, (a2, ((a0, a3), a4))), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, (a2, (a0, a3))), a4), a5), a6), a7)
instance [incoherent] a0 :< (((((a1, (a2, a0)), a3), a4), a5), a6)
instance [incoherent] a0 :< (((((a1, ((a2, (a3, a0)), a4)), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, ((a2, (a0, a3)), a4)), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, ((a2, a0), a3)), a4), a5), a6), a7)
instance [incoherent] a0 :< (((((a1, (((a2, a0), a3), a4)), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, (((a0, a2), a3), a4)), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((a1, ((a0, a2), a3)), a4), a5), a6), a7)
instance [incoherent] a0 :< (((((a1, (a0, a2)), a3), a4), a5), a6)
instance [incoherent] a0 :< (((((a1, a0), a2), a3), a4), a5)
instance [incoherent] a0 :< ((((((a1, (a2, (a3, a0))), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< ((((((a1, (a2, (a0, a3))), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< ((((((a1, (a2, a0)), a3), a4), a5), a6), a7)
instance [incoherent] a0 :< ((((((a1, ((a2, a0), a3)), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< ((((((a1, ((a0, a2), a3)), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< ((((((a1, (a0, a2)), a3), a4), a5), a6), a7)
instance [incoherent] a0 :< ((((((a1, a0), a2), a3), a4), a5), a6)
instance [incoherent] a0 :< (((((((a1, (a2, a0)), a3), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((((a1, (a0, a2)), a3), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((((a1, a0), a2), a3), a4), a5), a6), a7)
instance [incoherent] a0 :< ((((((((a1, a0), a2), a3), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< ((((((((a0, a1), a2), a3), a4), a5), a6), a7), a8)
instance [incoherent] a0 :< (((((((a0, a1), a2), a3), a4), a5), a6), a7)
instance [incoherent] a0 :< ((((((a0, a1), a2), a3), a4), a5), a6)
instance [incoherent] a0 :< (((((a0, a1), a2), a3), a4), a5)
instance [incoherent] a0 :< ((((a0, a1), a2), a3), a4)
instance [incoherent] a0 :< (((a0, a1), a2), a3)
instance [incoherent] a0 :< ((a0, a1), a2)
instance [incoherent] a0 :< (a0, a1)
instance [incoherent] a :< a


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>Difunctor</a>, <tt>Difoldable</tt>, and <a>Ditraversable</a>.
module Data.Comp.Param.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 <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

-- | Signature equality. An instance <tt>EqD f</tt> gives rise to an
--   instance <tt>Eq (Term f)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqD f
eqD :: (EqD f, PEq a) => f Name a -> f Name a -> FreshM Bool

-- | Derive an instance of <a>EqD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeEqD :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqD f => OrdD f
compareD :: (OrdD f, POrd a) => f Name a -> f Name a -> FreshM Ordering

-- | Derive an instance of <a>OrdD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeOrdD :: Name -> Q [Dec]

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

-- | Derive an instance of <a>ShowD</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeShowD :: Name -> Q [Dec]

-- | This class represents difunctors, i.e. binary type constructors that
--   are contravariant in the first argument and covariant in the second
--   argument.
class Difunctor f

-- | Derive an instance of <a>Difunctor</a> for a type constructor of any
--   parametric kind taking at least two arguments.
makeDifunctor :: Name -> Q [Dec]

-- | Difunctors representing data structures that can be traversed from
--   left to right.
class Difunctor f => Ditraversable f

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

-- | Derive smart constructors for a difunctor. The smart constructors are
--   similar to the ordinary constructors, but a 'inject . dimap Var id' is
--   automatically inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with annotations for a difunctor. The smart
--   constructors are similar to the ordinary constructors, but a 'injectA
--   . dimap Var id' is automatically inserted.
smartAConstructors :: Name -> Q [Dec]

-- | Given the name of a type class, where the first parameter is a
--   difunctor, lift it to sums of difunctors. Example: <tt>class ShowD f
--   where ...</tt> is lifted as <tt>instance (ShowD f, ShowD g) =&gt;
--   ShowD (f :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]

-- | Utility function to case on a difunctor sum, without exposing the
--   internal representation of sums.
caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c


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

-- | Signature printing. An instance <tt>ShowD f</tt> gives rise to an
--   instance <tt>Show (Term f)</tt>.
class ShowD f
showD :: ShowD f => f Name (FreshM String) -> FreshM String
instance [incoherent] (ShowD f, Show p) => ShowD (f :&: p)
instance [incoherent] (Difunctor f, ShowD f) => Show (Term f)
instance [incoherent] (Difunctor f, ShowD f) => ShowD (Cxt h f)
instance [incoherent] (ShowD f, ShowD g) => ShowD (f :+: g)


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.Param.Desugar

-- | The desugaring term homomorphism.
class (Difunctor f, Difunctor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => f a (Cxt h g a b) -> Cxt h g a b

-- | Desugar a term.
desugar :: Desugar f g => Term f -> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (Difunctor f', Difunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' -> Term g'
instance [overlap ok] (Difunctor f, Difunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g0, Desugar g g0) => Desugar (f :+: g) g0


-- | 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 (annotation) to a signature.
data (:&:) f a e
(:&:) :: f e -> a -> :&: f a e

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a -> s' a
projectA :: DistAnn s p s' => s' a -> (s a, p)
class RemA s s' | s -> s'
remA :: RemA s s' => s a -> s' a
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
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] (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

-- | This type represents multisorted <tt>f</tt>-algebras with a family
--   <tt>e</tt> of carriers.
type Alg f e = f e :-> e

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

-- | Construct a catamorphism from the given algebra.
cata :: HFunctor 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' :: HFunctor f => Alg f e -> Cxt h f e :-> e

-- | This function applies a whole context into another context.
appCxt :: HFunctor 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 e = NatM m (f e) e

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

-- | This is a monadic version of <a>cata</a>.
cataM :: (HTraversable f, Monad m) => AlgM m f a -> NatM m (Term f) a
cataM' :: (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a

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

-- | This type represents context function.
type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)

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

-- | This type represents term homomorphisms.
type Hom f g = SigFun f (Context g)

-- | This function applies the given term homomorphism to a term/context.
appHom :: (HFunctor f, HFunctor g) => Hom f g -> CxtFun f g

-- | This function applies the given term homomorphism to a term/context.
--   This is the top-down variant of <a>appHom</a>.
appHom' :: HFunctor g => Hom f g -> CxtFun f g

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

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

-- | This function applies a signature function to the given context. This
--   is the top-down variant of <a>appSigFun</a>.
appSigFun' :: HFunctor 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.
hom :: HFunctor g => SigFun f g -> Hom f g

-- | This function composes a term algebra with an algebra.
compAlg :: HFunctor g => Alg g a -> Hom f g -> Alg f a

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

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

-- | This type represents monadic term algebras.
type HomM m f g = SigFunM m f (Context 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.
sigFunM :: Monad m => SigFun f g -> SigFunM m f g

-- | This function lifts the give monadic signature function to a monadic
--   term algebra.
hom' :: (HFunctor f, HFunctor g, Monad m) => SigFunM m f g -> HomM m f g

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

-- | This function applies the given monadic term homomorphism to the given
--   term/context. This is a top-down variant of <a>appHomM</a>.
appHomM' :: (HTraversable g, Monad m) => HomM m f g -> CxtFunM m f g

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

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

-- | This function applies the given monadic signature function to the
--   given context. This is a top-down variant of <a>appSigFunM</a>.
appSigFunM' :: (HTraversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

-- | This function composes two monadic term algebras.
compHomM :: (HTraversable g, HFunctor h, Monad m) => HomM m g h -> HomM m f g -> HomM 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

-- | This function composes a monadic term algebra with a monadic algebra
compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a

-- | This function composes a monadic term algebra with a monadic algebra.
compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
type Coalg 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; Term
--   f</tt> from the given coalgebra of type <tt>a -&gt; f a</tt> to the
--   final coalgebra <tt>Term f</tt>.
ana :: HFunctor f => Coalg f a -> a :-> Term f
type CoalgM 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; Term f</tt> from the given coalgebra of type <tt>a -&gt; f
--   a</tt> to the final coalgebra <tt>Term f</tt>.
anaM :: (HTraversable f, Monad m) => CoalgM m f a -> NatM m a (Term f)

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

-- | This function constructs a paramorphism from the given r-algebra
para :: HFunctor f => RAlg f a -> Term 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 RAlgM m f a = NatM m (f (Term f :*: a)) a

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

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

-- | This function constructs an apomorphism from the given r-coalgebra.
apo :: HFunctor f => RCoalg f a -> a :-> Term f

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

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

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

-- | This function constructs the unique futumorphism from the given
--   cv-coalgebra to the term algebra.
futu :: HFunctor f => CVCoalg f a -> a :-> Term f

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

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


-- | 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
Inl :: (f h e) -> :+: f g e
Inr :: (g h e) -> :+: f g e

-- | The subsumption relation.
class :<: sub :: ((* -> *) -> * -> *) sup
inj :: :<: sub sup => sub a :-> sup a
proj :: :<: sub sup => NatM Maybe (sup a) (sub a)
data (:*:) f g a
(:*:) :: f a -> g a -> :*: f g a
fst :: (f :*: g) a -> f a
snd :: (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;: a) (g ::  * -&gt; *) e = f g e :&amp;: a e
--   </pre>
--   
--   This is too general, however, for example for <tt>productHHom</tt>.
data (:&:) f a g :: (* -> *) e
(:&:) :: f g e -> a -> :&: f a e

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s :: ((* -> *) -> * -> *) p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a :-> s' a
projectA :: DistAnn s p s' => s' a :-> (s a :&: p)
class RemA s :: ((* -> *) -> * -> *) s' | s -> s'
remA :: RemA s s' => s a :-> s' a
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((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] (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
inj :: :<: sub sup => sub a :-> sup a
proj :: :<: sub sup => NatM Maybe (sup a) (sub a)

-- | Data type defining coproducts.
data (:+:) f g h :: (* -> *) e
proj2 :: (:<: g1 f, :<: g2 f) => f a i -> Maybe (:+: g2 g1 a i)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a i -> Maybe (:+: g3 (:+: g2 g1) a i)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a i)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a i)
proj6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a i)
proj7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a i)
proj8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => f a i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a i)
proj9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => f a i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a i)
proj10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => f a i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a i)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: :<: g f => NatM Maybe (Cxt h f a) (g (Cxt h f a))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a i -> Maybe (:+: g2 g1 (Cxt h f a) i)
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a i -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a) i)
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a) i)
project5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a) i)
project6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a) i)
project7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Cxt h f a i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a) i)
project8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Cxt h f a i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a) i)
project9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Cxt h f a i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a) i)
project10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Cxt h f a i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a) i)

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (HTraversable g, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (HTraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (HTraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (HTraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (HTraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject6 :: (HTraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
deepProject7 :: (HTraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => CxtFunM Maybe f (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))
deepProject8 :: (HTraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => CxtFunM Maybe f (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))
deepProject9 :: (HTraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => CxtFunM Maybe f (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))
deepProject10 :: (HTraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => CxtFunM Maybe f (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a i -> g a i
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a i -> g a i
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a i -> g a i
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a i -> g a i
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a i -> g a i
inj7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a i -> g a i
inj8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a i -> g a i
inj9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a i -> g a i
inj10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a i -> g a i

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: :<: g f => g (Cxt h f a) :-> Cxt h f a
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 (Cxt h g a) i -> Cxt h g a i
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) (Cxt h g a) i -> Cxt h g a i
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) i -> Cxt h g a i
inject5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) i -> Cxt h g a i
inject6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) (Cxt h g a) i -> Cxt h g a i
inject7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) (Cxt h g a) i -> Cxt h g a i
inject8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) (Cxt h g a) i -> Cxt h g a i
inject9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) (Cxt h g a) i -> Cxt h g a i
inject10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) (Cxt h g a) i -> Cxt h g a i

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (HFunctor g, :<: g f) => CxtFun g f
deepInject2 :: (HFunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (HFunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (HFunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (HFunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (HFunctor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) g
deepInject7 :: (HFunctor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) g
deepInject8 :: (HFunctor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) g
deepInject9 :: (HFunctor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) g
deepInject10 :: (HFunctor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) g
injectConst :: (HFunctor g, :<: g f) => Const g :-> Cxt h f a
injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, :<: f1 g, :<: f2 g) => Const (f1 :+: f2) :-> Cxt h g a
injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g, :<: f1 g, :<: f2 g, :<: f3 g) => Const (f1 :+: (f2 :+: f3)) :-> Cxt h g a
projectConst :: (HFunctor g, :<: g f) => NatM Maybe (Cxt h f a) (Const g)

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

-- | This function lifts the given functor to a context.
liftCxt :: (HFunctor 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 :: (HFunctor f, HFunctor g, :<: f g) => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a


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

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

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s :: ((* -> *) -> * -> *) p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a :-> s' a
projectA :: DistAnn s p s' => s' a :-> (s a :&: p)
class RemA s :: ((* -> *) -> * -> *) s' | s -> s'
remA :: RemA 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 annotation.
liftA :: RemA 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).
ann :: (DistAnn f p g, HFunctor f) => p -> CxtFun f g

-- | 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 annotation.
liftA' :: (DistAnn s' p s, HFunctor s') => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a

-- | This function strips the annotations from a term over a functor with
--   annotations.
stripA :: (RemA g f, HFunctor g) => CxtFun g f
propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g) => Hom f g -> Hom f' g'
project' :: (RemA s s', :<: s f) => Cxt h f a i -> Maybe (s' (Cxt h f a) i)


-- | 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>EqHF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class EqHF f
eqHF :: (EqHF 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 :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]
instance (EqHF f, KEq a) => Eq (Cxt h f a i)
instance (EqHF f, KEq a) => KEq (Cxt h f a)
instance EqHF f => EqHF (Cxt h f)
instance (EqHF f, EqHF g) => EqHF (f :+: g)
instance KEq a => Eq (A a)
instance Eq a => KEq (K a)


-- | This module defines type generic functions and recursive schemes along
--   the lines of the Uniplate library. All definitions are generalised
--   versions of those in <a>Data.Comp.Generic</a>.
module Data.Comp.Multi.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 :: HFoldable f => Term f :=> [A (Term f)]

-- | This function returns a list of all subterms of the given term that
--   are constructed from a particular functor.
subterms' :: (HFoldable f, :<: g f) => Term f :=> [A (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 :: HFunctor f => (Term f :-> Term f) -> Term f :-> Term f

-- | Monadic version of <a>transform</a>.
transformM :: (HTraversable f, Monad m) => NatM m (Term f) (Term f) -> NatM m (Term f) (Term f)
query :: HFoldable f => (Term f :=> r) -> (r -> r -> r) -> Term f :=> r
subs :: HFoldable f => Term f :=> [A (Term f)]
subs' :: (HFoldable f, :<: g f) => Term f :=> [A (g (Term f))]

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

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


-- | This module defines the infrastructure necessary to use <i>Generalised
--   Compositional Data Types</i>. Generalised Compositional Data Types is
--   an extension of Compositional Data Types with mutually recursive data
--   types, and more generally GADTs. Examples of usage are bundled with
--   the package in the library <tt>examples/Examples/Multi</tt>.
module Data.Comp.Multi


-- | This module defines ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.Multi.Ordering
class KEq f => KOrd f
kcompare :: KOrd f => f i -> f j -> Ordering

-- | Signature ordering. An instance <tt>OrdHF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHF f => OrdHF f
compareHF :: (OrdHF f, KOrd a) => f a i -> f a j -> Ordering
instance [incoherent] (HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i)
instance [incoherent] (HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a)
instance [incoherent] (HFunctor f, OrdHF f) => OrdHF (Cxt h f)
instance [incoherent] (OrdHF f, OrdHF g) => OrdHF (f :+: g)
instance [incoherent] Ord a => KOrd (K a)


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>HFunctor</a>, <a>HFoldable</a>, and <a>HTraversable</a>.
module Data.Comp.Multi.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 <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

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

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

-- | Signature equality. An instance <tt>EqHF f</tt> gives rise to an
--   instance <tt>KEq (HTerm f)</tt>.
class EqHF f
eqHF :: (EqHF 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>EqHF</a> for a type constructor of any
--   higher-order kind taking at least two arguments.
makeEqHF :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdHF f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHF f => OrdHF f
compareHF :: (OrdHF f, KOrd a) => f a i -> f a j -> Ordering

-- | Derive an instance of <a>OrdHF</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeOrdHF :: 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.
makeHFunctor :: 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.
makeHFoldable :: 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.
makeHTraversable :: 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>inject</a> is automatically
--   inserted.
smartConstructors :: Name -> Q [Dec]

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

-- | Given the name of a type class, where the first parameter is a
--   higher-order functor, lift it to sums of higher-order. Example:
--   <tt>class HShowF f where ...</tt> is lifted as <tt>instance (HShowF f,
--   HShowF g) =&gt; HShowF (f :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]

-- | Utility function to case on a higher-order functor sum, without
--   exposing the internal representation of sums.
caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c


-- | 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>ShowHF f</tt> gives rise to an
--   instance <tt>KShow (HTerm f)</tt>.
class ShowHF f
showHF :: ShowHF f => Alg f (K String)
showHF' :: ShowHF f => f (K String) :=> String
instance (ShowHF f, ShowHF g) => ShowHF (f :+: g)
instance (ShowHF f, Show p) => ShowHF (f :&: p)
instance KShow f => Show (f i)
instance (ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a)
instance (ShowHF f, HFunctor f) => ShowHF (Cxt h f)
instance KShow (K String)


-- | This module defines an abstract notion of (bound) variables in
--   compositional data types, and scoped substitution. Capture-avoidance
--   is <i>not</i> taken into account. All definitions are generalised
--   versions of those in <a>Data.Comp.Variables</a>.
module Data.Comp.Multi.Variables

-- | This multiparameter class defines functors with variables. An instance
--   <tt>HasVar f v</tt> denotes that values over <tt>f</tt> might contain
--   and bind variables of type <tt>v</tt>.
class HasVars f :: ((* -> *) -> * -> *) v
isVar :: HasVars f v => f a :=> Maybe v
bindsVars :: HasVars f v => f a :=> [v]
type GSubst v a = NatM Maybe (K v) a
type CxtSubst h a f v = GSubst v (Cxt h f a)
type Subst f v = CxtSubst NoHole (K ()) f v
varsToHoles :: (HFunctor f, HasVars f v, Eq v) => Term f :-> Context f (K v)

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

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

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

-- | This function computes the set of variables occurring in a context.
variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f) => Const f :=> Set v
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) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst 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 (Cxt h f a) (Cxt h f a)
instance [overlap ok] HasVars f v => HasVars (Cxt h f) v
instance [overlap ok] (HasVars f v0, HasVars g v0) => HasVars (f :+: g) v0


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.Multi.Desugar

-- | The desugaring term homomorphism.
class (HFunctor f, HFunctor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => Alg f (Context g a)

-- | Desugar a term.
desugar :: Desugar f g => Term f :-> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' :-> Term g'
instance [overlap ok] (HFunctor f, HFunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g0, Desugar g g0) => Desugar (f :+: g) g0


-- | This module provides operators on higher-order difunctors.
module Data.Comp.MultiParam.Ops

-- | Formal sum of signatures (difunctors).
data (:+:) f g a :: (* -> *) b :: (* -> *) i
Inl :: (f a b i) -> :+: f g i
Inr :: (g a b i) -> :+: f g i

-- | 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 b :-> sup a b
proj :: :<: sub sup => NatM Maybe (sup a b) (sub a b)

-- | Formal product of signatures (higher-order difunctors).
data (:*:) f g a b
(:*:) :: f a b -> g a b -> :*: f g a b
ffst :: (f :*: g) a b -> f a b
fsnd :: (f :*: g) a b -> g a b

-- | This data type adds a constant product to a signature.
data (:&:) f p a :: (* -> *) b :: (* -> *) i
(:&:) :: f a b i -> p -> :&: f p i

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s :: ((* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a b :-> s' a b
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA s :: ((* -> *) -> (* -> *) -> * -> *) s' | s -> s'
remA :: RemA s s' => s a b :-> s' a b
instance [incoherent] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [incoherent] DistAnn f p (f :&: p)
instance [incoherent] RemA (f :&: p) f
instance [incoherent] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [incoherent] HDitraversable f => HDitraversable (f :&: p)
instance [incoherent] HDifunctor f => HDifunctor (f :&: p)
instance [incoherent] f :<: g => f :<: (h :+: g)
instance [incoherent] f :<: (f :+: g)
instance [incoherent] f :<: f
instance [incoherent] (HDitraversable f, HDitraversable g) => HDitraversable (f :+: g)
instance [incoherent] (HDifunctor f, HDifunctor g) => HDifunctor (f :+: g)


-- | This module provides the infrastructure to extend signatures.
module Data.Comp.MultiParam.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 b :-> sup a b
proj :: :<: sub sup => NatM Maybe (sup a b) (sub a b)

-- | Formal sum of signatures (difunctors).
data (:+:) f g a :: (* -> *) b :: (* -> *) i
proj2 :: (:<: g1 f, :<: g2 f) => f a b i -> Maybe (:+: g2 g1 a b i)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a b i -> Maybe (:+: g3 (:+: g2 g1) a b i)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a b i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a b i)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a b i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a b i)
proj6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a b i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a b i)
proj7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a b i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a b i)
proj8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => f a b i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a b i)
proj9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => f a b i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a b i)
proj10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => f a b i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a b i)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: :<: g f => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a b i -> Maybe (:+: g2 g1 a (Cxt h f a b) i)
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a b i -> Maybe (:+: g3 (:+: g2 g1) a (Cxt h f a b) i)
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a b i -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a (Cxt h f a b) i)
project5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a b i -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a (Cxt h f a b) i)
project6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a b i -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a (Cxt h f a b) i)
project7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Cxt h f a b i -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a (Cxt h f a b) i)
project8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Cxt h f a b i -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a (Cxt h f a b) i)
project9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Cxt h f a b i -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a (Cxt h f a b) i)
project10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Cxt h f a b i -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a (Cxt h f a b) i)

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (HDitraversable g, :<: g f) => Term f i -> Maybe (Term g i)
deepProject2 :: (HDitraversable (:+: g2 g1), :<: g1 f, :<: g2 f) => Term f i -> Maybe (Term (:+: g2 g1) i)
deepProject3 :: (HDitraversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => Term f i -> Maybe (Term (:+: g3 (:+: g2 g1)) i)
deepProject4 :: (HDitraversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Term f i -> Maybe (Term (:+: g4 (:+: g3 (:+: g2 g1))) i)
deepProject5 :: (HDitraversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Term f i -> Maybe (Term (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) i)
deepProject6 :: (HDitraversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Term f i -> Maybe (Term (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) i)
deepProject7 :: (HDitraversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Term f i -> Maybe (Term (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) i)
deepProject8 :: (HDitraversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Term f i -> Maybe (Term (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) i)
deepProject9 :: (HDitraversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Term f i -> Maybe (Term (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) i)
deepProject10 :: (HDitraversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Term f i -> Maybe (Term (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))) i)
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a b i -> g a b i
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a b i -> g a b i
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a b i -> g a b i
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a b i -> g a b i
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a b i -> g a b i
inj7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a b i -> g a b i
inj8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a b i -> g a b i
inj9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a b i -> g a b i
inj10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a b i -> g a b i

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: :<: g f => g a (Cxt h f a b) :-> Cxt h f a b
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a (Cxt h g a b) i -> Cxt h g a b i
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a (Cxt h g a b) i -> Cxt h g a b i
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a (Cxt h g a b) i -> Cxt h g a b i
inject5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a (Cxt h g a b) i -> Cxt h g a b i
inject6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a (Cxt h g a b) i -> Cxt h g a b i
inject7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a (Cxt h g a b) i -> Cxt h g a b i
inject8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a (Cxt h g a b) i -> Cxt h g a b i
inject9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a (Cxt h g a b) i -> Cxt h g a b i
inject10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a (Cxt h g a b) i -> Cxt h g a b i

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (HDifunctor g, :<: g f) => CxtFun g f
deepInject2 :: (HDifunctor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (HDifunctor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (HDifunctor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (HDifunctor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (HDifunctor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) g
deepInject7 :: (HDifunctor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) g
deepInject8 :: (HDifunctor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) g
deepInject9 :: (HDifunctor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) g
deepInject10 :: (HDifunctor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) g

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

-- | This function lifts the given functor to a context.
liftCxt :: (HDifunctor f, :<: g f) => g a b :-> Cxt Hole f a b
instance [incoherent] (Eq (f a b i), Eq (g a b i)) => Eq ((:+:) f g a b i)
instance [incoherent] (Ord (f a b i), Ord (g a b i)) => Ord ((:+:) f g a b i)
instance [incoherent] (Show (f a b i), Show (g a b i)) => Show ((:+:) f g a b i)


-- | This module defines annotations on signatures.
module Data.Comp.MultiParam.Annotation

-- | This data type adds a constant product to a signature.
data (:&:) f p a :: (* -> *) b :: (* -> *) i
(:&:) :: f a b i -> p -> :&: f p i

-- | Formal product of signatures (higher-order difunctors).
data (:*:) f g a b
(:*:) :: f a b -> g a b -> :*: f g a b

-- | This class defines how to distribute an annotation over a sum of
--   signatures.
class DistAnn s :: ((* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a b :-> s' a b
projectA :: DistAnn s p s' => s' a b :-> (s a b :&: p)
class RemA s :: ((* -> *) -> (* -> *) -> * -> *) s' | s -> s'
remA :: RemA s s' => s a b :-> s' a b

-- | Transform a function with a domain constructed from a higher-order
--   difunctor to a function with a domain constructed with the same
--   higher-order difunctor, but with an additional annotation.
liftA :: RemA s s' => (s' a b :-> t) -> s a b :-> t

-- | Transform a function with a domain constructed from a higher-order
--   difunctor to a function with a domain constructed with the same
--   higher-order difunctor, but with an additional annotation.
liftA' :: (DistAnn s' p s, HDifunctor s') => (s' a b :-> Cxt h s' c d) -> s a b :-> Cxt h s c d

-- | Strip the annotations from a term over a higher-order difunctor with
--   annotations.
stripA :: (RemA g f, HDifunctor g) => CxtFun g f

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   annotations.
propAnn :: (DistAnn f p f', DistAnn g p g', HDifunctor g) => Hom f g -> Hom f' g'

-- | Lift a monadic term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a monadic term homomorphism over the same signatures,
--   but extended with annotations.
propAnnM :: (DistAnn f p f', DistAnn g p g', HDifunctor g, Monad m) => HomM m f g -> HomM m f' g'

-- | Annotate each node of a term with a constant value.
ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g
project' :: (RemA s s', :<: s f) => Cxt h f a b i -> Maybe (s' a (Cxt h f a b) i)


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

-- | Equality on parametric values. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class PEq a
peq :: PEq a => a i -> a j -> FreshM Bool

-- | Signature equality. An instance <tt>EqHD f</tt> gives rise to an
--   instance <tt>Eq (Term f i)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqHD f
eqHD :: (EqHD f, PEq a) => f Name a i -> f Name a j -> FreshM Bool
instance [incoherent] (HDifunctor f, EqHD f) => Eq (Term f i)
instance [incoherent] (EqHD f, PEq a) => PEq (Cxt h f Name a)
instance [incoherent] EqHD f => EqHD (Cxt h f)
instance [incoherent] PEq Name
instance [incoherent] (EqHD f, EqHD g) => EqHD (f :+: g)
instance [incoherent] Eq a => PEq (K a)


-- | This module defines the infrastructure necessary to use <i>Generalised
--   Parametric Compositional Data Types</i>. Generalised Parametric
--   Compositional Data Types is an extension of Compositional Data Types
--   with parametric higher-order abstract syntax (PHOAS) for usage with
--   binders, and GADTs. Generalised Parametric Compositional Data Types
--   combines Generalised Compositional Data Types (<a>Data.Comp.Multi</a>)
--   and Parametric Compositional Data Types (<a>Data.Comp.Param</a>).
--   Examples of usage are bundled with the package in the library
--   <tt>examples/Examples/MultiParam</tt>.
module Data.Comp.MultiParam


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

-- | Ordering of parametric values.
class PEq a => POrd a
pcompare :: POrd a => a i -> a j -> FreshM Ordering

-- | Signature ordering. An instance <tt>OrdHD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHD f => OrdHD f
compareHD :: (OrdHD f, POrd a) => f Name a i -> f Name a j -> FreshM Ordering
instance [incoherent] (HDifunctor f, OrdHD f) => Ord (Term f i)
instance [incoherent] (OrdHD f, POrd a) => POrd (Cxt h f Name a)
instance [incoherent] POrd Name
instance [incoherent] OrdHD f => OrdHD (Cxt h f)
instance [incoherent] (OrdHD f, OrdHD g) => OrdHD (f :+: g)
instance [incoherent] Ord a => POrd (K a)


-- | This module contains functionality for automatically deriving
--   boilerplate code using Template Haskell. Examples include instances of
--   <a>HDifunctor</a>, <a>ShowHD</a>, and <a>EqHD</a>.
module Data.Comp.MultiParam.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 <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''Exp])
--   </pre>
derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec]

-- | Signature equality. An instance <tt>EqHD f</tt> gives rise to an
--   instance <tt>Eq (Term f i)</tt>. The equality test is performed inside
--   the <a>FreshM</a> monad for generating fresh identifiers.
class EqHD f
eqHD :: (EqHD f, PEq a) => f Name a i -> f Name a j -> FreshM Bool

-- | Derive an instance of <a>EqHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeEqHD :: Name -> Q [Dec]

-- | Signature ordering. An instance <tt>OrdHD f</tt> gives rise to an
--   instance <tt>Ord (Term f)</tt>.
class EqHD f => OrdHD f
compareHD :: (OrdHD f, POrd a) => f Name a i -> f Name a j -> FreshM Ordering

-- | Derive an instance of <a>OrdHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeOrdHD :: Name -> Q [Dec]

-- | Signature printing. An instance <tt>ShowHD f</tt> gives rise to an
--   instance <tt>Show (Term f i)</tt>.
class ShowHD f
showHD :: ShowHD f => f Name (K (FreshM String)) i -> FreshM String

-- | Derive an instance of <a>ShowHD</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeShowHD :: Name -> Q [Dec]

-- | This class represents higher-order difunctors.
class HDifunctor f

-- | Derive an instance of <a>HDifunctor</a> for a type constructor of any
--   parametric kind taking at least three arguments.
makeHDifunctor :: Name -> Q [Dec]

-- | Derive smart constructors for a higher-order difunctor. The smart
--   constructors are similar to the ordinary constructors, but a 'inject .
--   hdimap Var id' is automatically inserted.
smartConstructors :: Name -> Q [Dec]

-- | Derive smart constructors with annotations for a higher-order
--   difunctor. The smart constructors are similar to the ordinary
--   constructors, but a 'injectA . hdimap Var id' is automatically
--   inserted.
smartAConstructors :: Name -> Q [Dec]

-- | Given the name of a type class, where the first parameter is a
--   higher-order difunctor, lift it to sums of higher-order difunctors.
--   Example: <tt>class ShowHD f where ...</tt> is lifted as <tt>instance
--   (ShowHD f, ShowHD g) =&gt; ShowHD (f :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]

-- | Utility function to case on a higher-order difunctor sum, without
--   exposing the internal representation of sums.
caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c


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

-- | Signature printing. An instance <tt>ShowHD f</tt> gives rise to an
--   instance <tt>Show (Term f i)</tt>.
class ShowHD f
showHD :: ShowHD f => f Name (K (FreshM String)) i -> FreshM String
instance [incoherent] (ShowHD f, Show p) => ShowHD (f :&: p)
instance [incoherent] (HDifunctor f, ShowHD f) => Show (Term f i)
instance [incoherent] (HDifunctor f, ShowHD f) => ShowHD (Cxt h f)
instance [incoherent] (ShowHD f, ShowHD g) => ShowHD (f :+: g)


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.MultiParam.Desugar

-- | The desugaring term homomorphism.
class (HDifunctor f, HDifunctor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => f a (Cxt h g a b) :-> Cxt h g a b

-- | Desugar a term.
desugar :: Desugar f g => Term f :-> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' :-> Term g'
instance [overlap ok] (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g0, Desugar g g0) => Desugar (f :+: g) g0


-- | 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

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

-- | 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 :: Functor f => 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)


-- | 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 Hom f g = SigFun f (Context g)

-- | This function applies the given term homomorphism to a term/context.
appHom :: (Functor f, Functor g) => Hom f g -> CxtFun f g

-- | Apply a term homomorphism recursively to a term/context. This is a
--   top-down variant of <a>appHom</a>.
appHom' :: Functor g => Hom f g -> CxtFun f g

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

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

-- | This function applies a signature function to the given context. This
--   is a top-down variant of <a>appSigFun</a>.
appSigFun' :: Functor g => SigFun f g -> CxtFun f g

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

-- | This function composes a signature function with a term homomorphism.
compSigFunHom :: Functor g => SigFun g h -> Hom f g -> Hom f h

-- | This function composes a term homomorphism with a signature function.
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h

-- | This function composes an algebra with a signature function.
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a

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

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

-- | Compose a term homomorphism with a coalgebra to get a cv-coalgebra.
compCoalg :: Hom 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) => Hom 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 HomM 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 SigFunMD m f g = forall a. f (m a) -> m (g a)

-- | This type represents a monadic term homomorphism. It is similar to
--   <a>HomM</a> but has monadic values also in the domain.
type HomMD m f g = SigFunMD 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.
hom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> HomM m f g

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

-- | Apply a monadic term homomorphism recursively to a term/context. This
--   a top-down variant of <a>appHomM</a>.
appHomM' :: (Traversable g, Monad m) => HomM m f g -> CxtFunM m f g

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

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

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

-- | This function applies a monadic signature function to the given
--   context. This is a top-down variant of <a>appSigFunM</a>.
appSigFunM' :: (Traversable g, Monad m) => SigFunM m f g -> CxtFunM m f g

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

-- | Compose two monadic term homomorphisms.
compHomM :: (Traversable g, Functor h, Monad m) => HomM m g h -> HomM m f g -> HomM 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
compSigFunHomM :: (Traversable g, Functor h, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h

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

-- | This function composes two monadic signature functions.
compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a

-- | Compose a monadic algebra with a monadic term homomorphism to get a
--   new monadic algebra.
compAlgM :: (Traversable g, Monad m) => AlgM m g a -> HomM 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 -> Hom 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, DistAnn 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, DistAnn 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)


-- | This module defines stateful term homomorphisms. This (slightly
--   oxymoronic) notion extends per se stateless term homomorphisms with a
--   state that is maintained separately by a bottom-up or top-down tree
--   automaton.
module Data.Comp.Automata

-- | This type represents stateful term homomorphisms. Stateful term
--   homomorphisms have access to a state that is provided (separately) by
--   a DUTA or a DDTA (or both).
type QHom f q g = forall a. (?below :: a -> q, ?above :: q) => f a -> Context g a

-- | This function provides access to components of the states from
--   <a>below</a>.
below :: (?below :: a -> q, :< p q) => a -> p

-- | This function provides access to components of the state from
--   <a>above</a>
above :: (?above :: q, :< p q) => p

-- | This function constructs a DUTT from a given stateful term
--   homomorphism with the state propagated by the given DUTA.
upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g

-- | This function applies a given stateful term homomorphism with a state
--   space propagated by the given DUTA to a term.
runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g

-- | This is a variant of <a>runUpHom</a> that also returns the final state
--   of the run.
runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q, Term g)

-- | This function constructs a DDTT from a given stateful term--
--   homomorphism with the state propagated by the given DDTA.
downTrans :: Zippable f => DownState f q -> QHom f q g -> DownTrans f q g

-- | This function applies a given stateful term homomorphism with a state
--   space propagated by the given DDTA to a term.
runDownHom :: (Zippable f, Functor g) => DownState f q -> QHom f q g -> q -> Term f -> Term g

-- | This combinator runs a stateful term homomorphisms with a state space
--   produced both on a bottom-up and a top-down state transformation.
runQHom :: (Zippable f, Functor g) => DUpState f (u, d) u -> DDownState f (u, d) d -> QHom f (u, d) g -> d -> Term f -> (u, Term g)

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

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

-- | This function composes two DUTTs. (see TATA, Theorem 6.4.5)
compUpTrans :: (Functor f, Functor g, Functor h) => UpTrans g p h -> UpTrans f q g -> UpTrans f (q, p) h

-- | This combinator composes a homomorphism followed by a DUTT.
compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h

-- | This combinator composes a DUTT followed by a homomorphism.
compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h

-- | This combinator composes a signature function followed by a DUTT.
compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h

-- | This combinator composes a DUTT followed by a signature function.
compSigUpTrans :: Functor g => SigFun g h -> UpTrans f q g -> UpTrans f q h

-- | This function composes a DUTT with an algebra.
compAlgUpTrans :: Functor g => Alg g a -> UpTrans f q g -> Alg f (q, a)

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

-- | Changes the state space of the DUTA using the given isomorphism.
tagUpState :: Functor f => (q -> p) -> (p -> q) -> UpState f q -> UpState f p

-- | This combinator runs the given DUTA on a term returning the final
--   state of the run.
runUpState :: Functor f => UpState f q -> Term f -> q

-- | This function combines the product DUTA of the two given DUTAs.
prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p, q)

-- | This type represents transition functions of generalised deterministic
--   bottom-up tree acceptors (GDUTAs) which have access to an extended
--   state space.
type DUpState f p q = forall a. (?below :: a -> p, ?above :: p, :< q p) => f a -> q

-- | This combinator turns an arbitrary DUTA into a GDUTA.
dUpState :: Functor f => UpState f q -> DUpState f p q

-- | This combinator turns a GDUTA with the smallest possible state space
--   into a DUTA.
upState :: DUpState f q q -> UpState f q

-- | This combinator runs a GDUTA on a term.
runDUpState :: Functor f => DUpState f q q -> Term f -> q

-- | This combinator constructs the product of two GDUTA.
prodDUpState :: (:< p c, :< q c) => DUpState f c p -> DUpState f c q -> DUpState f c (p, q)
(<*>) :: (:< p c, :< q c) => DUpState f c p -> DUpState f c q -> DUpState f c (p, q)

-- | This type represents transition functions of deterministic top-down
--   tree transducers (DDTTs).
type DownTrans f q g = forall a. (q, f a) -> Context g (q, a)

-- | Thsis function runs the given DDTT on the given tree.
runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a

-- | This function composes two DDTTs. (see Z. Flp, H. Vogler
--   <a>Syntax-Directed Semantics</a>, Theorem 3.39)
compDownTrans :: (Functor f, Functor g, Functor h) => DownTrans g p h -> DownTrans f q g -> DownTrans f (q, p) h

-- | This function composes a DDTT after a function.
compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h

-- | This function composes a signature function after a DDTT.
compSigDownTrans :: Functor g => SigFun g h -> DownTrans f q g -> DownTrans f q h

-- | This function composes a DDTT after a homomorphism.
compDownTransHom :: (Functor g, Functor h) => DownTrans g q h -> Hom f g -> DownTrans f q h

-- | This function composes a homomorphism after a DDTT.
compHomDownTrans :: (Functor g, Functor h) => Hom g h -> DownTrans f q g -> DownTrans f q h

-- | This type represents transition functions of deterministic top-down
--   tree acceptors (DDTAs).
type DownState f q = forall a. Ord a => (q, f a) -> Map a q

-- | Changes the state space of the DDTA using the given isomorphism.
tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p

-- | This function constructs the product DDTA of the given two DDTAs.
prodDownState :: DownState f p -> DownState f q -> DownState f (p, q)

-- | This type represents transition functions of generalised deterministic
--   top-down tree acceptors (GDDTAs) which have access to an extended
--   state space.
type DDownState f p q = forall i. (Ord i, ?below :: i -> p, ?above :: p, :< q p) => f i -> Map i q

-- | This combinator turns an arbitrary DDTA into a GDDTA.
dDownState :: DownState f q -> DDownState f p q

-- | This combinator turns a GDDTA with the smallest possible state space
--   into a DDTA.
downState :: DDownState f q q -> DownState f q

-- | This combinator constructs the product of two dependant top-down state
--   transformations.
prodDDownState :: (:< p c, :< q c) => DDownState f c p -> DDownState f c q -> DDownState f c (p, q)

-- | This is a synonym for <a>prodDDownState</a>.
(>*<) :: (:< p c, :< q c, Functor f) => DDownState f c p -> DDownState f c q -> DDownState f c (p, q)

-- | This combinator combines a bottom-up and a top-down state
--   transformations. Both state transformations can depend mutually
--   recursive on each other.
runDState :: Zippable f => DUpState f (u, d) u -> DDownState f (u, d) d -> d -> Term f -> u

-- | left-biased union of two mappings.
(&) :: Ord k => Map k v -> Map k v -> Map k v

-- | This operator constructs a singleton mapping.
(|->) :: k -> a -> Map k a

-- | This is the empty mapping.
o :: Map k 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
proj2 :: (:<: g1 f, :<: g2 f) => f a -> Maybe (:+: g2 g1 a)
proj3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => f a -> Maybe (:+: g3 (:+: g2 g1) a)
proj4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) a)
proj5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) a)
proj6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) a)
proj7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) a)
proj8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) a)
proj9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) a)
proj10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) a)

-- | Project the outermost layer of a term to a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>project</tt><i>n</i> instead.
project :: :<: g f => Cxt h f a -> Maybe (g (Cxt h f a))
project2 :: (:<: g1 f, :<: g2 f) => Cxt h f a -> Maybe (:+: g2 g1 (Cxt h f a))
project3 :: (:<: g1 f, :<: g2 f, :<: g3 f) => Cxt h f a -> Maybe (:+: g3 (:+: g2 g1) (Cxt h f a))
project4 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => Cxt h f a -> Maybe (:+: g4 (:+: g3 (:+: g2 g1)) (Cxt h f a))
project5 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => Cxt h f a -> Maybe (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))) (Cxt h f a))
project6 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => Cxt h f a -> Maybe (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))) (Cxt h f a))
project7 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => Cxt h f a -> Maybe (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))) (Cxt h f a))
project8 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => Cxt h f a -> Maybe (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))) (Cxt h f a))
project9 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => Cxt h f a -> Maybe (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))) (Cxt h f a))
project10 :: (:<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => Cxt h f a -> Maybe (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))) (Cxt h f a))

-- | Tries to coerce a term<i>context to a term</i>context over a
--   sub-signature. If the signature <tt>g</tt> is compound of <i>n</i>
--   atomic signatures, use <tt>deepProject</tt><i>n</i> instead.
deepProject :: (Traversable g, :<: g f) => CxtFunM Maybe f g
deepProject2 :: (Traversable (:+: g2 g1), :<: g1 f, :<: g2 f) => CxtFunM Maybe f (:+: g2 g1)
deepProject3 :: (Traversable (:+: g3 (:+: g2 g1)), :<: g1 f, :<: g2 f, :<: g3 f) => CxtFunM Maybe f (:+: g3 (:+: g2 g1))
deepProject4 :: (Traversable (:+: g4 (:+: g3 (:+: g2 g1))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f) => CxtFunM Maybe f (:+: g4 (:+: g3 (:+: g2 g1)))
deepProject5 :: (Traversable (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f) => CxtFunM Maybe f (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))
deepProject6 :: (Traversable (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f) => CxtFunM Maybe f (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))
deepProject7 :: (Traversable (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f) => CxtFunM Maybe f (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))
deepProject8 :: (Traversable (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f) => CxtFunM Maybe f (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))
deepProject9 :: (Traversable (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f) => CxtFunM Maybe f (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))
deepProject10 :: (Traversable (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1))))))))), :<: g1 f, :<: g2 f, :<: g3 f, :<: g4 f, :<: g5 f, :<: g6 f, :<: g7 f, :<: g8 f, :<: g9 f, :<: g10 f) => CxtFunM Maybe f (:+: g10 (:+: g9 (:+: g8 (:+: g7 (:+: g6 (:+: g5 (:+: g4 (:+: g3 (:+: g2 g1)))))))))
inj2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 a -> g a
inj3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) a -> g a
inj4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) a -> g a
inj5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) a -> g a
inj6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) a -> g a
inj7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) a -> g a
inj8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) a -> g a
inj9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) a -> g a
inj10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) a -> g a

-- | Inject a term where the outermost layer is a sub signature. If the
--   signature <tt>g</tt> is compound of <i>n</i> atomic signatures, use
--   <tt>inject</tt><i>n</i> instead.
inject :: :<: g f => g (Cxt h f a) -> Cxt h f a
inject2 :: (:<: f1 g, :<: f2 g) => :+: f2 f1 (Cxt h g a) -> Cxt h g a
inject3 :: (:<: f1 g, :<: f2 g, :<: f3 g) => :+: f3 (:+: f2 f1) (Cxt h g a) -> Cxt h g a
inject4 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => :+: f4 (:+: f3 (:+: f2 f1)) (Cxt h g a) -> Cxt h g a
inject5 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => :+: f5 (:+: f4 (:+: f3 (:+: f2 f1))) (Cxt h g a) -> Cxt h g a
inject6 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => :+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) (Cxt h g a) -> Cxt h g a
inject7 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => :+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) (Cxt h g a) -> Cxt h g a
inject8 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => :+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) (Cxt h g a) -> Cxt h g a
inject9 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => :+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) (Cxt h g a) -> Cxt h g a
inject10 :: (:<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => :+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) (Cxt h g a) -> Cxt h g a

-- | Inject a term over a sub signature to a term over larger signature. If
--   the signature <tt>g</tt> is compound of <i>n</i> atomic signatures,
--   use <tt>deepInject</tt><i>n</i> instead.
deepInject :: (Functor g, :<: g f) => CxtFun g f
deepInject2 :: (Functor (:+: f2 f1), :<: f1 g, :<: f2 g) => CxtFun (:+: f2 f1) g
deepInject3 :: (Functor (:+: f3 (:+: f2 f1)), :<: f1 g, :<: f2 g, :<: f3 g) => CxtFun (:+: f3 (:+: f2 f1)) g
deepInject4 :: (Functor (:+: f4 (:+: f3 (:+: f2 f1))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g) => CxtFun (:+: f4 (:+: f3 (:+: f2 f1))) g
deepInject5 :: (Functor (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g) => CxtFun (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))) g
deepInject6 :: (Functor (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g) => CxtFun (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))) g
deepInject7 :: (Functor (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g) => CxtFun (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))) g
deepInject8 :: (Functor (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g) => CxtFun (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))) g
deepInject9 :: (Functor (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g) => CxtFun (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1)))))))) g
deepInject10 :: (Functor (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))), :<: f1 g, :<: f2 g, :<: f3 g, :<: f4 g, :<: f5 g, :<: f6 g, :<: f7 g, :<: f8 g, :<: f9 g, :<: f10 g) => CxtFun (:+: f10 (:+: f9 (:+: f8 (:+: f7 (:+: f6 (:+: f5 (:+: f4 (:+: f3 (:+: f2 f1))))))))) g
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 annotations on signatures.
module Data.Comp.Annotation

-- | This data type adds a constant product (annotation) 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 an annotation over a sum of
--   signatures.
class DistAnn s p s' | s' -> s, s' -> p
injectA :: DistAnn s p s' => p -> s a -> s' a
projectA :: DistAnn s p s' => s' a -> (s a, p)
class RemA s s' | s -> s'
remA :: RemA 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 annotation.
liftA :: RemA 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 annotation.
liftA' :: (DistAnn s' p s, Functor s') => (s' a -> Cxt h s' a) -> s a -> Cxt h s a

-- | Strip the annotations from a term over a functor with annotations.
stripA :: (RemA g f, Functor g) => CxtFun g f

-- | Lift a term homomorphism over signatures <tt>f</tt> and <tt>g</tt> to
--   a term homomorphism over the same signatures, but extended with
--   annotations.
propAnn :: (DistAnn f p f', DistAnn g p g', Functor g) => Hom f g -> Hom f' g'

-- | Lift a stateful term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a stateful term homomorphism over the same signatures,
--   but extended with annotations.
propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g) => QHom f q g -> QHom f' q g'

-- | Lift a bottom-up tree transducer over signatures <tt>f</tt> and
--   <tt>g</tt> to a bottom-up tree transducer over the same signatures,
--   but extended with annotations.
propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g) => UpTrans f q g -> UpTrans f' q g'

-- | Lift a top-down tree transducer over signatures <tt>f</tt> and
--   <tt>g</tt> to a top-down tree transducer over the same signatures, but
--   extended with annotations.
propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) => DownTrans f q g -> DownTrans f' q g'

-- | Lift a monadic term homomorphism over signatures <tt>f</tt> and
--   <tt>g</tt> to a monadic term homomorphism over the same signatures,
--   but extended with annotations.
propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m) => HomM m f g -> HomM m f' g'

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


-- | 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 a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0, Eq h0, Eq i0) => EqF ((,,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0 i0)
instance (Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0, Eq h0) => EqF ((,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0)
instance (Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0) => EqF ((,,,,,,,) a0 b0 c0 d0 e0 f0 g0)
instance (Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0) => EqF ((,,,,,,) a0 b0 c0 d0 e0 f0)
instance (Eq a0, Eq b0, Eq c0, Eq d0, Eq e0) => EqF ((,,,,,) a0 b0 c0 d0 e0)
instance (Eq a0, Eq b0, Eq c0, Eq d0) => EqF ((,,,,) a0 b0 c0 d0)
instance (Eq a0, Eq b0, Eq c0) => EqF ((,,,) a0 b0 c0)
instance (Eq a0, Eq b0) => EqF ((,,) a0 b0)
instance Eq a0 => EqF ((,) a0)
instance EqF []
instance EqF Maybe
instance (EqF f, EqF g) => EqF (f :+: g)
instance EqF f => EqF (Cxt h f)
instance (EqF f, Eq a) => Eq (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 height of the given term.
height :: Foldable f => Cxt h f a -> Int


-- | 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 a0 => ShowF ((,) a0)
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 modules defines terms &amp; contexts with thunks, with deferred
--   monadic computations.
module Data.Comp.Thunk

-- | This type represents terms with thunks.
type TermT m f = Term (m :+: f)

-- | This type represents contexts with thunks.
type CxtT m h f a = Cxt h (m :+: f) a

-- | This function turns a monadic computation into a thunk.
thunk :: :<: m f => m (Cxt h f a) -> Cxt h f a

-- | This function evaluates all thunks until a non-thunk node is found.
whnf :: Monad m => TermT m f -> m (f (TermT m f))
whnf' :: Monad m => TermT m f -> m (TermT m f)

-- | This function first evaluates the argument term into whnf via
--   <a>whnf</a> and then projects the top-level signature to the desired
--   subsignature. Failure to do the projection is signalled as a failure
--   in the monad.
whnfPr :: (Monad m, :<: g f) => TermT m f -> m (g (TermT m f))

-- | This function evaluates all thunks.
nf :: (Monad m, Traversable f) => TermT m f -> m (Term f)

-- | This function evaluates all thunks while simultaneously projecting the
--   term to a smaller signature. Failure to do the projection is signalled
--   as a failure in the monad as in <a>whnfPr</a>.
nfPr :: (Monad m, Traversable g, :<: g f) => TermT m f -> m (Term g)

-- | This function inspects the topmost non-thunk node (using <a>whnf</a>)
--   according to the given function.
eval :: Monad m => (f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f

-- | This function inspects the topmost non-thunk nodes of two terms (using
--   <a>whnf</a>) according to the given function.
eval2 :: Monad m => (f (TermT m f) -> f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f -> TermT m f

-- | This function inspects a term (using <a>nf</a>) according to the given
--   function.
deepEval :: (Traversable f, Monad m) => (Term f -> TermT m f) -> TermT m f -> TermT m f

-- | This function inspects two terms (using <a>nf</a>) according to the
--   given function.
deepEval2 :: (Monad m, Traversable f) => (Term f -> Term f -> TermT m f) -> TermT m f -> TermT m f -> TermT m f

-- | Variant of <a>eval</a> with flipped argument positions
(#>) :: Monad m => TermT m f -> (f (TermT m f) -> TermT m f) -> TermT m f

-- | Variant of <a>deepEval</a> with flipped argument positions
(#>>) :: (Monad m, Traversable f) => TermT m f -> (Term f -> TermT m f) -> TermT m f

-- | This type represents algebras which have terms with thunks as carrier.
type AlgT m f g = Alg f (TermT m g)

-- | This combinator runs a catamorphism on a term with thunks.
cataT :: (Traversable f, Monad m) => Alg f a -> TermT m f -> m a

-- | This combinator runs a monadic catamorphism on a term with thunks
cataTM :: (Traversable f, Monad m) => AlgM m f a -> TermT m f -> m a

-- | This function decides equality of terms with thunks.
eqT :: (EqF f, Foldable f, Functor f, Monad m) => TermT m f -> TermT m f -> m Bool

-- | This combinator makes the evaluation of the given functor application
--   strict by evaluating all thunks of immediate subterms.
strict :: (:<: f g, Traversable f, Monad m) => f (TermT m g) -> TermT m g

-- | This combinator is a variant of <a>strict</a> that only makes a subset
--   of the arguments of a functor application strict. The first argument
--   of this combinator specifies which positions are supposed to be
--   strict.
strictAt :: (:<: f g, Traversable f, Zippable f, Monad m) => Pos f -> f (TermT m g) -> TermT m g


-- | 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 <tt>ShowF</tt> for a signature <tt>Exp</tt>, use derive as follows
--   (requires Template Haskell):
--   
--   <pre>
--   $(derive [makeFunctor, makeShowF] [''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.
makeShowF :: 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.
makeEqF :: 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.
makeOrdF :: 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.
makeFunctor :: 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.
makeFoldable :: 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.
makeTraversable :: Name -> Q [Dec]

-- | Derive an instance of <a>HaskellStrict</a> for a type constructor of
--   any first-order kind taking at least one argument.
makeHaskellStrict :: Name -> Q [Dec]
haskellStrict :: (Monad m, HaskellStrict f, :<: f g) => f (TermT m g) -> TermT m g
haskellStrict' :: (Monad m, HaskellStrict f, :<: f g) => f (TermT m g) -> TermT m g

-- | 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>.
makeArbitraryF :: 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.
makeArbitrary :: 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.
makeNFData :: 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.
makeNFDataF :: 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]

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

-- | Given the name of a type class, where the first parameter is a
--   functor, lift it to sums of functors. Example: <tt>class ShowF f where
--   ...</tt> is lifted as <tt>instance (ShowF f, ShowF g) =&gt; ShowF (f
--   :+: g) where ... </tt>.
liftSum :: Name -> Q [Dec]

-- | Utility function to case on a functor sum, without exposing the
--   internal representation of sums.
caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b


-- | 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 a0, Ord b0, Ord c0, Ord d0, Ord e0, Ord f0, Ord g0, Ord h0, Ord i0) => OrdF ((,,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0 i0)
instance (Ord a0, Ord b0, Ord c0, Ord d0, Ord e0, Ord f0, Ord g0, Ord h0) => OrdF ((,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0)
instance (Ord a0, Ord b0, Ord c0, Ord d0, Ord e0, Ord f0, Ord g0) => OrdF ((,,,,,,,) a0 b0 c0 d0 e0 f0 g0)
instance (Ord a0, Ord b0, Ord c0, Ord d0, Ord e0, Ord f0) => OrdF ((,,,,,,) a0 b0 c0 d0 e0 f0)
instance (Ord a0, Ord b0, Ord c0, Ord d0, Ord e0) => OrdF ((,,,,,) a0 b0 c0 d0 e0)
instance (Ord a0, Ord b0, Ord c0, Ord d0) => OrdF ((,,,,) a0 b0 c0 d0)
instance (Ord a0, Ord b0, Ord c0) => OrdF ((,,,) a0 b0 c0)
instance (Ord a0, Ord b0) => OrdF ((,,) a0 b0)
instance Ord a0 => OrdF ((,) a0)
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 a0 => NFDataF ((,) a0)
instance NFDataF []
instance NFDataF Maybe
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 b0, Arbitrary c0, Arbitrary d0, Arbitrary e0, Arbitrary f0, Arbitrary g0, Arbitrary h0, Arbitrary i0, Arbitrary j0) => ArbitraryF ((,,,,,,,,,) b0 c0 d0 e0 f0 g0 h0 i0 j0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0, Arbitrary e0, Arbitrary f0, Arbitrary g0, Arbitrary h0, Arbitrary i0) => ArbitraryF ((,,,,,,,,) b0 c0 d0 e0 f0 g0 h0 i0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0, Arbitrary e0, Arbitrary f0, Arbitrary g0, Arbitrary h0) => ArbitraryF ((,,,,,,,) b0 c0 d0 e0 f0 g0 h0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0, Arbitrary e0, Arbitrary f0, Arbitrary g0) => ArbitraryF ((,,,,,,) b0 c0 d0 e0 f0 g0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0, Arbitrary e0, Arbitrary f0) => ArbitraryF ((,,,,,) b0 c0 d0 e0 f0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0, Arbitrary e0) => ArbitraryF ((,,,,) b0 c0 d0 e0)
instance (Arbitrary b0, Arbitrary c0, Arbitrary d0) => ArbitraryF ((,,,) b0 c0 d0)
instance (Arbitrary b0, Arbitrary c0) => ArbitraryF ((,,) b0 c0)
instance Arbitrary b0 => ArbitraryF ((,) b0)
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 an abstract notion of (bound) variables in
--   compositional data types, and scoped substitution. Capture-avoidance
--   is <i>not</i> taken into account.
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
--   and bind variables of type <tt>v</tt>.
class HasVars f v
isVar :: HasVars f v => f a -> Maybe v
bindsVars :: HasVars f v => f a -> [v]

-- | This type represents substitutions of terms, i.e. finite mappings from
--   variables to terms.
type Subst f v = CxtSubst NoHole () f v

-- | This type represents substitutions of contexts, i.e. finite mappings
--   from variables to contexts.
type CxtSubst h a f v = Map v (Cxt h f a)

-- | Convert variables to holes, except those that are bound.
varsToHoles :: (Functor f, HasVars f v, Eq 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 constant.
variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
substVars :: SubstVars v t a => (v -> Maybe t) -> a -> a

-- | Apply the given substitution.
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 v0, HasVars g v0) => HasVars (f :+: g) v0


-- | 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 = Hom f g

-- | This type represents variables.
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]

-- | This type represents a potential single step reduction from any input.
type Step t = t -> Maybe t

-- | This type represents a potential single step reduction from any input.
--   If there is no single step then the return value is the input together
--   with <tt>False</tt>. Otherwise, the successor is returned together
--   with <tt>True</tt>.
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))

-- | This function tries to match the rules of the given TRS against the
--   given term (resp. context in general) at the root. The first rule in
--   the TRS that matches is then used and the corresponding right-hand
--   side as well the matching substitution is returned.
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 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

-- | This is used in order to signal a failed occurs check during
--   unification.
failedOccursCheck :: MonadError (UnifError f v) m => v -> Term f -> m a

-- | This is used in order to signal a head symbol mismatch during
--   unification.
headSymbolMismatch :: MonadError (UnifError f v) m => Term f -> Term f -> m a

-- | This function applies a substitution to each term in a list of
--   equations.
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)

-- | This type represents the state for the unification algorithm.
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

-- | This is the unification monad that is used to run the unification
--   algorithm.
type UnifyM f v m a = StateT (UnifyState f v) m a

-- | This function runs a unification monad with the given initial list of
--   equations.
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 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 bundled with the package in the
--   library <tt>examples/Examples</tt>.
module Data.Comp


-- | This modules defines the <a>Desugar</a> type class for desugaring of
--   terms.
module Data.Comp.Desugar

-- | The desugaring term homomorphism.
class (Functor f, Functor g) => Desugar f g
desugHom :: Desugar f g => Hom f g
desugHom' :: Desugar f g => Alg f (Context g a)

-- | Desugar a term.
desugar :: Desugar f g => Term f -> Term g

-- | Lift desugaring to annotated terms.
desugarA :: (Functor f', Functor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' -> Term g'
instance [overlap ok] (Functor f, Functor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f g0, Desugar g g0) => Desugar (f :+: g) g0