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


-- | Parametric Compositional Data Types
--   
@package compdata-param
@version 0.8


-- | This module defines a monad for generating fresh, abstract names,
--   useful e.g. for defining equality on terms.
module Data.Comp.Param.Multi.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 Functor FreshM
instance Applicative FreshM
instance Eq (Name i)
instance Ord (Name i)
instance Show (Name i)


-- | 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.Param.Multi.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 E (f :: * -> *) :: (* -> *) -> *
E :: f i -> E f
unE :: E f -> f i
data A (f :: * -> *) :: (* -> *) -> *
A :: (forall i. f i) -> A
unA :: A -> forall i. 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.Param.Multi.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 provides operators on higher-order difunctors.
module Data.Comp.Param.Multi.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

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

-- | 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 defines the central notion of <i>generalised parametrised
--   terms</i> and their generalisation to generalised parametrised
--   contexts.
module Data.Comp.Param.Multi.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.Multi.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.Param.Multi.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 provides the infrastructure to extend signatures.
module Data.Comp.Param.Multi.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

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

-- | This function is similar to <a>project</a> but applies to signatures
--   with an annotation which is then ignored.
project' :: (RemA f f', 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.Param.Multi.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 ordering of signatures, which lifts to ordering of
--   terms and contexts.
module Data.Comp.Param.Multi.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.Param.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 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]


-- | This module defines showing of signatures, which lifts to showing of
--   terms.
module Data.Comp.Param.Multi.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 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/Param.Multi</tt>.
module Data.Comp.Param.Multi


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

-- | The desugaring term homomorphism.
class (HDifunctor f, HDifunctor g) => Desugar f g where desugHom = desugHom' . hfmap Hole desugHom' x = appCxt (desugHom x)
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'

-- | Default desugaring instance.
instance [overlap ok] (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f h, Desugar g h) => Desugar (f :+: g) h


-- | 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 Applicative FreshM
instance Functor 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 where dimapM f = disequence . fmap f disequence = dimapM id
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

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

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

-- | This combinator maps a function over a context by applying the
--   function to each hole.
cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c

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

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

-- | This function is similar to <a>project</a> but applies to signatures
--   with an annotation which is then ignored.
project' :: (RemA f f', 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 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 where dimapM f = disequence . fmap f disequence = dimapM id

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


-- | 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 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 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 where desugHom = desugHom' . fmap Hole desugHom' x = appCxt (desugHom x)
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'

-- | Default desugaring instance.
instance [overlap ok] (Difunctor f, Difunctor g, f :<: g) => Desugar f g
instance [overlap ok] (Desugar f h, Desugar g h) => Desugar (f :+: g) h