-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Compositional Data Types -- -- Based on Wouter Swierstra's Functional Pearl Data types a la -- carte (Journal of Functional Programming, 18(4):423-436, 2008, -- http://dx.doi.org/10.1017/S0956796808006758), this package -- provides a framework for defining recursive data types in a -- compositional manner. The fundamental idea of compositional data -- types (Workshop on Generic Programming, 83-94, 2011, -- http://dx.doi.org/10.1145/2036918.2036930) 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 domain-specific -- languages. -- -- In concrete terms, this package provides the following features: -- --

Compositional data types in the style of Wouter Swierstra's -- Functional Pearl Data types a la carte.
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.
Support for monadic computations via monadic variants of all -- recursion schemes.
Support of a succinct programming style over compositional data -- types via generic programming combinators that allow various forms of -- generic transformations and generic queries.
Generalisation of compositional data types (terms) to -- compositional data types "with holes" (contexts). This allows flexible -- reuse of a wide variety of catamorphisms (called term -- homomorphisms) as well as an efficient composition of them.
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.
Optimisation of the implementation of recursion schemes. This -- includes short-cut fusion style optimisation rules which yield -- a performance boost of up to factor six.
Automatic derivation of instances of all relevant type classes for -- using compositional data types via Template Haskell. This -- includes instances of Prelude.Eq, Prelude.Ord and -- Prelude.Show that are derived via instances for functorial -- variants of them. Additionally, also smart constructors, which -- allow to easily construct inhabitants of compositional data types, are -- automatically generated.
Mutually recursive data types and generalised algebraic -- data types (GADTs). All of the above is also lifted to families of -- mutually recursive data types and (more generally) GADTs. This -- extension resides in the module Data.Comp.Multi.
Parametric compositional data types (Workshop on -- Mathematically Structured Functional Programming, 3-24, 2012, -- http://dx.doi.org/10.4204/EPTCS.76.3). 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 Data.Comp.Param.
Generalised parametric compositional data types. 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 -- Data.Comp.MultiParam.
Advanced recursion schemes derived from tree automata. These -- recursion schemes allow for a higher degree of modularity and make it -- possible to apply fusion. See Modular Tree Automata -- (Mathematics of Program Construction, 263-299, 2012, -- http://dx.doi.org/10.1007/978-3-642-31113-0_14).

-- -- Examples of using (generalised) (parametric) compositional data types -- are bundled with the package in the libray examples. @package compdata @version 0.7 -- | 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 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 parametrised terms -- 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 Data.Comp.Param.Difunctor. 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 Context. data Hole -- | Phantom type used to define Term. 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 Trm values, which are parametric at -- top level, can be made into monadic Term 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 f and -- carrier a. type Alg f a = f a a -> a -- | Construct a catamorphism for contexts over f with holes of -- type b, 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 cata from terms over f to contexts -- over f, 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 Alg -- 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 f with -- holes of type b, 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 cataM from terms over f to -- contexts over f, 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 appSigFun. 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 -- SigFunM 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 -- HomM 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 appSigFunM. 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 f and -- carrier a. The list of (a,b)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 f is -- itself a binder, then the parameters bound by f 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 f -- and carrier a. 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 f and -- carrier a. 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 f -- and carrier a. 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 f and -- carrier a. 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 f -- and carrier a. 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 f and -- carrier a. 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 f -- and carrier a. 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 f and -- carrier a. The list of (a,b)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 f is -- itself a binder, then the parameters bound by f 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 -- f and carrier a. 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 -- f and carrier a. 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 g is compound of n atomic signatures, use -- projectn 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 termcontext to a termcontext over a -- sub-signature. If the signature g is compound of n -- atomic signatures, use deepProjectn 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 g is compound of n atomic signatures, use -- injectn 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 g is compound of n atomic signatures, use -- injectn 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 g is compound of n atomic signatures, -- use deepInjectn 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 f and g 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 f and -- g 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 project but applies to signatures -- with an annotation which is then ignored. 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 FreshM monad for generating fresh identifiers. class PEq a peq :: PEq a => a -> a -> FreshM Bool -- | Signature equality. An instance EqD f gives rise to an -- instance Eq (Term f). The equality test is performed inside -- the FreshM 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 OrdD f gives rise to an -- instance Ord (Term f). 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 & 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 -- whnf 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 whnfPr. 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 whnfPr. 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 Parametric -- Compositional Data Types. 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 -- examples/Examples/Param. module Data.Comp.Param -- | This modules defines the Desugar 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' 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 -- | 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 f to a. f -- :=> a is isomorphic to f :-> 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 :: (forall i. f i) -> A f unA :: A f -> forall i. f i data E f E :: f i -> E f unE :: E f -> f i runE :: (f :=> b) -> E f -> b -- | 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) instance [incoherent] Functor I -- | This module defines higher-order foldable functors. module Data.Comp.Multi.HFoldable -- | Higher-order functors that can be folded. -- -- Minimal complete definition: hfoldMap or hfoldr. class HFunctor h => HFoldable h where hfold = hfoldMap unK hfoldMap f = hfoldr (mappend . f) mempty hfoldr f z t = appEndo (hfoldMap (Endo . f) t) z hfoldl f z t = appEndo (getDual (hfoldMap (Dual . Endo . flip f) t)) z hfoldr1 f xs = fromMaybe (error "hfoldr1: empty structure") (hfoldr mf Nothing xs) where mf :: K a :=> (Maybe a -> Maybe a) mf (K x) Nothing = Just x mf (K x) (Just y) = Just (f x y) hfoldl1 f xs = fromMaybe (error "hfoldl1: empty structure") (hfoldl mf Nothing xs) where mf :: Maybe a -> K a :=> Maybe a mf Nothing (K y) = Just y mf (Just x) (K y) = Just (f x y) 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 :=> [E 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 the central notion of mutual recursive (or, -- higher-order) terms and its generalisation to (higher-order) -- contexts. All definitions are generalised versions of those in -- Data.Comp.Term. 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 Hole and NoHole. -- 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 Cxt might contain holes. data Hole -- | Phantom type that signals that a Cxt 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) -- | 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 E f E :: f i -> E f unE :: E f -> f i data A f A :: (forall i. f i) -> A f unA :: A f -> 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.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 generalised parametrised -- terms 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 Data.Comp.MultiParam.HDifunctor. 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 Context. data Hole -- | Phantom type used to define Term. 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 hfmap for Cxt. hfmapCxt :: HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b' -- | This is an instance of hdimapM for Cxt. 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 Trm values, which are parametric at -- top level, can be made into monadic Term 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 f and -- carrier a. type Alg f a = f a a :-> a -- | Construct a catamorphism for contexts over f with holes of -- type b, 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 cata from terms over f to contexts -- over f, 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 Alg -- but the return type is monadic. type AlgM m f a = NatM m (f a a) a -- | Construct a monadic catamorphism for contexts over f with -- holes of type b, 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 f with -- holes of type b, 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 appHom. 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 appHomM. 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 appSigFunM. 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 module Data.Comp.Automata.Product -- | An instance a :< b means that a is a component of -- b. a can be extracted from b via the method -- pr. class (:<) a b pr :: :< a b => b -> a 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 -- Difunctor, Difoldable, and Ditraversable. 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 Functor -- and ShowF for a signature Exp, use derive as follows -- (requires Template Haskell): -- --

--   $(derive [makeFunctor, makeShowF] [''Exp])
--

derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] -- | Signature equality. An instance EqD f gives rise to an -- instance Eq (Term f). The equality test is performed inside -- the FreshM 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 EqD for a type constructor of any -- parametric kind taking at least two arguments. makeEqD :: Name -> Q [Dec] -- | Signature ordering. An instance OrdD f gives rise to an -- instance Ord (Term f). class EqD f => OrdD f compareD :: (OrdD f, POrd a) => f Name a -> f Name a -> FreshM Ordering -- | Derive an instance of OrdD for a type constructor of any -- parametric kind taking at least two arguments. makeOrdD :: Name -> Q [Dec] -- | Signature printing. An instance ShowD f gives rise to an -- instance Show (Term f). class ShowD f showD :: ShowD f => f Name (FreshM String) -> FreshM String -- | Derive an instance of ShowD 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 Difunctor 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 Traversable 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: class ShowD f -- where ... is lifted as instance (ShowD f, ShowD g) => -- ShowD (f :+: g) where .... 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 ShowD f gives rise to an -- instance Show (Term f). 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 module provides functionality to number the components of a -- functorial value with consecutive integers. module Data.Comp.Number -- | This type is used for numbering components of a functorial value. newtype Numbered a Numbered :: (Int, a) -> Numbered a unNumbered :: Numbered a -> a -- | This function numbers the components of the given functorial value -- with consecutive integers starting at 0. number :: Traversable f => f a -> f (Numbered a) -- | Functors representing data structures that can be traversed from left -- to right. -- -- Minimal complete definition: traverse or sequenceA. -- -- Instances are similar to Functor, e.g. given a data type -- --

--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--

-- -- a suitable instance would be -- --

--   instance Traversable Tree where
--      traverse f Empty = pure Empty
--      traverse f (Leaf x) = Leaf <$> f x
--      traverse f (Node l k r) = Node <$> traverse f l <*> f k <*> traverse f r
--

-- -- This is suitable even for abstract types, as the laws for -- <*> imply a form of associativity. -- -- The superclass instances should satisfy the following: -- --

In the Functor instance, fmap should be equivalent -- to traversal with the identity applicative functor -- (fmapDefault).
In the Foldable instance, foldMap should be -- equivalent to traversal with a constant applicative functor -- (foldMapDefault).

class (Functor t, Foldable t) => Traversable (t :: * -> *) instance Ord (Numbered a) instance Eq (Numbered a) -- | 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 -- | 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 -- | 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 -- Data.Comp.Algebra. module Data.Comp.Multi.Algebra -- | This type represents multisorted f-algebras with a family -- e of carriers. type Alg f e = f e :-> e -- | Construct a catamorphism for contexts over f with holes of -- type b, 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 cata from terms over f to contexts -- over f, 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 Alg -- but the return type is monadic. type AlgM m f e = NatM m (f e) e -- | Construct a monadic catamorphism for contexts over f with -- holes of type b, 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 cata. 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 appHom. 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 appSigFun. 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 appHomM. 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 appSigFunM. 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 a -> Term -- f from the given coalgebra of type a -> f a to the -- final coalgebra Term f. 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 a -- -> Term f from the given coalgebra of type a -> f -- a to the final coalgebra Term f. anaM :: (HTraversable f, Monad m) => CoalgM m f a -> NatM m a (Term f) -- | This type represents r-algebras over functor f and with -- domain a. 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 m and -- functor f and with domain a. 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 f and with -- domain a. 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 m and -- functor f with domain a. 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 f and with -- domain a. 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 m and -- functor f, and with domain a. 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 Data.Comp.Ops. 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 -- | 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 -- | 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 -- --

--   data (f :&: a) (g ::  * -> *) e = f g e :&: a e
--

-- -- This is too general, however, for example for productHHom. 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 Data.Comp.Sum. 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 -- | 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 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 g is compound of n atomic signatures, use -- projectn 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 termcontext to a termcontext over a -- sub-signature. If the signature g is compound of n -- atomic signatures, use deepProjectn 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 g is compound of n atomic signatures, use -- injectn 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 g is compound of n atomic signatures, -- use deepInjectn 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 a to a -- family f of contexts (possibly terms) indexed by a. -- That is, each hole h is replaced by the context f h. 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 Data.Comp.Annotation. module Data.Comp.Multi.Annotation -- | This data type adds a constant product to a signature. Alternatively, -- this could have also been defined as -- --

--   data (f :&: a) (g ::  * -> *) e = f g e :&: a e
--

--   $(derive [makeFunctor, makeShowF] [''Exp])
--

derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] -- | Signature printing. An instance ShowHF f gives rise to an -- instance KShow (HTerm f). class ShowHF f where showHF = K . showHF' showHF' = unK . showHF 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 ShowHF for a type constructor of any -- higher-order kind taking at least two arguments. makeShowHF :: Name -> Q [Dec] -- | Signature equality. An instance EqHF f gives rise to an -- instance KEq (HTerm f). 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 EqHF for a type constructor of any -- higher-order kind taking at least two arguments. makeEqHF :: Name -> Q [Dec] -- | Signature ordering. An instance OrdHF f gives rise to an -- instance Ord (Term f). class EqHF f => OrdHF f compareHF :: (OrdHF f, KOrd a) => f a i -> f a j -> Ordering -- | Derive an instance of OrdHF 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 HFunctor 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: hfoldMap or hfoldr. class HFunctor h => HFoldable h where hfold = hfoldMap unK hfoldMap f = hfoldr (mappend . f) mempty hfoldr f z t = appEndo (hfoldMap (Endo . f) t) z hfoldl f z t = appEndo (getDual (hfoldMap (Dual . Endo . flip f) t)) z hfoldr1 f xs = fromMaybe (error "hfoldr1: empty structure") (hfoldr mf Nothing xs) where mf :: K a :=> (Maybe a -> Maybe a) mf (K x) Nothing = Just x mf (K x) (Just y) = Just (f x y) hfoldl1 f xs = fromMaybe (error "hfoldl1: empty structure") (hfoldl mf Nothing xs) where mf :: Maybe a -> K a :=> Maybe a mf Nothing (K y) = Just y mf (Just x) (K y) = Just (f x y) -- | Derive an instance of HFoldable 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 HTraversable 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 inject 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 injectA 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: -- class HShowF f where ... is lifted as instance (HShowF f, -- HShowF g) => HShowF (f :+: g) where .... liftSum :: Name -> Q [Dec] -- | 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 Data.Comp.Show. module Data.Comp.Multi.Show -- | Signature printing. An instance ShowHF f gives rise to an -- instance KShow (HTerm f). class ShowHF f where showHF = K . showHF' showHF' = unK . showHF 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 (Cxt h f a) => Show (Cxt h f a 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 ()) instance KShow (K String) -- | This module defines an abstract notion of (bound) variables in -- compositional data types, and scoped substitution. Capture-avoidance -- is not taken into account. All definitions are generalised -- versions of those in Data.Comp.Variables. module Data.Comp.Multi.Variables -- | This multiparameter class defines functors with variables. An instance -- HasVar f v denotes that values over f might contain -- and bind variables of type v. class HasVars (f :: (* -> *) -> * -> *) v where isVar _ = Nothing bindsVars _ = empty isVar :: HasVars f v => f a :=> Maybe v bindsVars :: (HasVars f v, KOrd a) => f a :=> Map (E a) (Set v) type GSubst v a = Map v (A a) type CxtSubst h a f v = GSubst v (Cxt h f a) type Subst f v = CxtSubst NoHole (K ()) f v varsToHoles :: (HTraversable f, HasVars f v, Ord v) => Term f :-> Context f (K v) -- | This function checks whether a variable is contained in a context. containsVar :: (Ord v, HasVars f v, HTraversable 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, HTraversable f, HFunctor f) => Cxt h f a :=> Set v -- | This function computes the list of variables occurring in a context. variableList :: (HasVars f v, HTraversable f, HFunctor f, Ord 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 appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a -- | This function composes two substitutions s1 and s2. -- That is, applying the resulting substitution is equivalent to first -- applying s2 and then s1. compSubst :: (Ord v, HasVars f v, HTraversable f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v -- | This combinator pairs every argument of a given constructor with the -- set of (newly) bound variables according to the corresponding -- HasVars type class instance. getBoundVars :: (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i instance [overlap ok] (SubstVars v t a, HFunctor f) => SubstVars v t (f a) instance [overlap ok] (Ord v, HasVars f v, HTraversable f) => SubstVars v (Cxt h f a) (Cxt h f a) instance [overlap ok] (HasVars f v0, HasVars g v0) => HasVars (f :+: g) v0 -- | 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 -- | 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 g is compound of n atomic signatures, use -- projectn 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 termcontext to a termcontext over a -- sub-signature. If the signature g is compound of n -- atomic signatures, use deepProjectn 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 g is compound of n atomic signatures, use -- injectn 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 g is compound of n atomic signatures, -- use deepInjectn 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 f and g 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 f and -- g 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 project but applies to signatures -- with an annotation which is then ignored. 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 FreshM monad for generating fresh identifiers. class PEq a peq :: PEq a => a i -> a j -> FreshM Bool -- | Signature equality. An instance EqHD f gives rise to an -- instance Eq (Term f i). The equality test is performed inside -- the FreshM 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 Generalised -- Parametric Compositional Data Types. 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 (Data.Comp.Multi) -- and Parametric Compositional Data Types (Data.Comp.Param). -- Examples of usage are bundled with the package in the library -- examples/Examples/MultiParam. module Data.Comp.MultiParam -- | This modules defines the Desugar type class for desugaring of -- terms. module Data.Comp.MultiParam.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' 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 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 OrdHD f gives rise to an -- instance Ord (Term f). 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 -- HDifunctor, ShowHD, and EqHD. 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 Functor -- and ShowF for a signature Exp, use derive as follows -- (requires Template Haskell): -- --

--   $(derive [makeFunctor, makeShowF] [''Exp])
--

derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] -- | Signature equality. An instance EqHD f gives rise to an -- instance Eq (Term f i). The equality test is performed inside -- the FreshM 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 EqHD for a type constructor of any -- parametric kind taking at least three arguments. makeEqHD :: Name -> Q [Dec] -- | Signature ordering. An instance OrdHD f gives rise to an -- instance Ord (Term f). class EqHD f => OrdHD f compareHD :: (OrdHD f, POrd a) => f Name a i -> f Name a j -> FreshM Ordering -- | Derive an instance of OrdHD for a type constructor of any -- parametric kind taking at least three arguments. makeOrdHD :: Name -> Q [Dec] -- | Signature printing. An instance ShowHD f gives rise to an -- instance Show (Term f i). class ShowHD f showHD :: ShowHD f => f Name (K (FreshM String)) i -> FreshM String -- | Derive an instance of ShowHD 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 HDifunctor 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: class ShowHD f where ... is lifted as instance -- (ShowHD f, ShowHD g) => ShowHD (f :+: g) where .... liftSum :: Name -> Q [Dec] -- | This module defines showing of signatures, which lifts to showing of -- terms. module Data.Comp.MultiParam.Show -- | Signature printing. An instance ShowHD f gives rise to an -- instance Show (Term f i). 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 central notion of terms 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 Hole and NoHole. -- 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 Cxt might contain holes. data Hole -- | Phantom type that signals that a Cxt 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 Term, 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 f. 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 f and carrier -- a. type Alg f a = f a -> a -- | Construct a catamorphism for contexts over f with holes of -- type a, 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 cata from terms over f to contexts -- over f, 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 Alg -- 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 f with -- holes of type a, 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 cataM from terms over f to -- contexts over f, 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 appHom. 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 appSigFun. 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 -- SigFunM 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 -- HomM 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 appHomM. 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 appSigFunM. 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 f and carrier -- a. 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 ana. ana' :: Functor f => Coalg f a -> a -> Term f -- | This type represents a monadic coalgebra over a functor f and -- carrier a. 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 f and -- carrier a. 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 f and -- carrier a. 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 f and -- carrier a. 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 f -- and carrier a. 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 f and -- carrier a. 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 f -- and carrier a. 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 f and -- carrier a. 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 -- f and carrier a. 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 f -- and carrier a. 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 state -- transformation. Additionally, this module also provides combinators to -- run state transformations themselves. -- -- Like regular term homomorphisms also stateful homomorphisms (as well -- as transducers) can be lifted to annotated signatures (cf. -- Data.Comp.Annotation). -- -- The recursion schemes provided in this module are derived from tree -- automata. They allow for a higher degree of modularity and make it -- possible to apply fusion. The implementation is based on the paper -- Modular Tree Automata (Mathematics of Program Construction, -- 263-299, 2012, http://dx.doi.org/10.1007/978-3-642-31113-0_14). module Data.Comp.Automata -- | This type represents stateful term homomorphisms. Stateful term -- homomorphisms have access to a state that is provided (separately) by -- a bottom-up or top-down state transformation function (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 -- below. below :: (?below :: a -> q, p :< q) => a -> p -- | This function provides access to components of the state from -- above above :: (?above :: q, p :< q) => p -- | This function turns a stateful homomorphism with a fully polymorphic -- state type into a (stateless) homomorphism. pureHom :: (forall q. QHom f q g) -> Hom f g -- | This function constructs a UTT from a given stateful term homomorphism -- with the state propagated by the given UTA. 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 UTA to a term. runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g -- | This is a variant of runUpHom 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 DTT from a given stateful term-- -- homomorphism with the state propagated by the given DTA. downTrans :: (Traversable f, Functor g) => 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 DTA to a term. runDownHom :: (Traversable 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 :: (Traversable 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 total, deterministic -- bottom-up tree transducers (UTTs). type UpTrans f q g = forall a. f (q, a) -> (q, Context g a) -- | This is a variant of the UpTrans type that makes it easier to -- define UTTs as it avoids the explicit use of Hole to inject -- placeholders into the result. type UpTrans' f q g = forall a. f (q, Context g a) -> (q, Context g a) -- | This function turns a UTT defined using the type UpTrans' in to -- the canonical form of type UpTrans. mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g -- | This function runs the given UTT on the given term. runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g -- | This function composes two UTTs. (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 UTT. compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h -- | This combinator composes a UTT 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 UTT. compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h -- | This combinator composes a UTT followed by a signature function. compSigUpTrans :: Functor g => SigFun g h -> UpTrans f q g -> UpTrans f q h -- | This function composes a UTT with an algebra. compAlgUpTrans :: Functor g => Alg g a -> UpTrans f q g -> Alg f (q, a) -- | This type represents transition functions of total, deterministic -- bottom-up tree acceptors (UTAs). type UpState f q = Alg f q -- | Changes the state space of the UTA using the given isomorphism. tagUpState :: Functor f => (q -> p) -> (p -> q) -> UpState f q -> UpState f p -- | This combinator runs the given UTA on a term returning the final state -- of the run. runUpState :: Functor f => UpState f q -> Term f -> q -- | This function combines the product UTA of the two given UTAs. 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 (GUTAs) 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 UTA into a GUTA. dUpState :: Functor f => UpState f q -> DUpState f p q -- | This combinator turns a GUTA with the smallest possible state space -- into a UTA. upState :: DUpState f q q -> UpState f q -- | This combinator runs a GUTA on a term. runDUpState :: Functor f => DUpState f q q -> Term f -> q -- | This combinator constructs the product of two GUTA. 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 total deterministic -- top-down tree transducers (DTTs). type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a -- | This is a variant of the DownTrans type that makes it easier to -- define DTTs as it avoids the explicit use of Hole to inject -- placeholders into the result. type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a -- | This function turns a DTT defined using the type DownTrans' in -- to the canonical form of type DownTrans. mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g -- | Thsis function runs the given DTT 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 DTTs. (see W.C. Rounds /Mappings and -- grammars on trees/, Theorem 2.) compDownTrans :: (Functor f, Functor g, Functor h) => DownTrans g p h -> DownTrans f q g -> DownTrans f (q, p) h -- | This function composes a DTT after a function. compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h -- | This function composes a signature function after a DTT. compSigDownTrans :: Functor g => SigFun g h -> DownTrans f q g -> DownTrans f q h -- | This function composes a DTT 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 DTT. compHomDownTrans :: (Functor g, Functor h) => Hom g h -> DownTrans f q g -> DownTrans f q h -- | This type represents transition functions of total, deterministic -- top-down tree acceptors (DTAs). type DownState f q = forall a. Ord a => (q, f a) -> Map a q -- | Changes the state space of the DTA using the given isomorphism. tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p -- | This function constructs the product DTA of the given two DTAs. prodDownState :: DownState f p -> DownState f q -> DownState f (p, q) -- | This type represents transition functions of generalised deterministic -- top-down tree acceptors (GDTAs) which have access 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 DTA into a GDTA. dDownState :: DownState f q -> DDownState f p q -- | This combinator turns a GDTA with the smallest possible state space -- into a DTA. 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 prodDDownState. (>*<) :: (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 :: Traversable 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 defines macro tree transducers (MTTs). It provides -- functions to run MTTs and to compose them with top down tree -- transducers. It also defines MTTs with regular look-ahead which -- combines MTTs with bottom-up tree acceptors. module Data.Comp.MacroAutomata -- | This type represents total deterministic macro tree transducers -- (MTTs). type MacroTrans f q g = forall a. q a -> f (q (Context g a) -> a) -> Context g a -- | This is a variant of the type MacroTrans that makes it easier -- to define MTTs as it avoids the explicit use of Hole when using -- placeholders in the result. type MacroTrans' f q g = forall a. q (Context g a) -> f (q (Context g a) -> Context g a) -> Context g a -- | This function turns an MTT defined using the more convenient type -- MacroTrans' into its canonical form of type MacroTrans. mkMacroTrans :: (Functor f, Functor q) => MacroTrans' f q g -> MacroTrans f q g -- | This function defines the semantics of MTTs. It applies a given MTT to -- an input with and an initial state. runMacroTrans :: (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a -- | This function composes a DTT followed by an MTT. The resulting MTT's -- semantics is equivalent to the function composition of the semantics -- of the original MTT and DTT. compMacroDown :: (Functor f, Functor g, Functor h, Functor p) => MacroTrans g p h -> DownTrans f q g -> MacroTrans f (p :&: q) h -- | This function composes an MTT followed by a DTT. The resulting MTT's -- semantics is equivalent to first running the original MTT and then the -- DTT. compDownMacro :: (Functor f, Functor g, Functor h, Functor q) => DownTrans g p h -> MacroTrans f q g -> MacroTrans f (q :^: p) h -- | This type is an instantiation of the MacroTrans type to a state -- space with only a single state with a single accumulation parameter -- (i.e. the state space is the identity functor). type MacroTransId f g = forall a. a -> f (Context g a -> a) -> Context g a -- | This type is a variant of the MacroTransId which is more -- convenient to work with as it avoids the explicit use of Hole -- to embed placeholders into the result. type MacroTransId' f g = forall a. Context g a -> f (Context g a -> Context g a) -> Context g a -- | This function transforms an MTT of type |MacroTransId| into the -- canonical type such that it can be run. fromMacroTransId :: Functor f => MacroTransId f g -> MacroTrans f I g -- | This function transforms an MTT of type |MacroTransId'| into the -- canonical type such that it can be run. fromMacroTransId' :: Functor f => MacroTransId' f g -> MacroTrans f I g -- | This type represents MTTs with regular look-ahead, i.e. MTTs that have -- access to information that is generated by a separate UTA. type MacroTransLA f q p g = forall a. q a -> p -> f (q (Context g a) -> a, p) -> Context g a -- | This type is a more convenient variant of MacroTransLA with -- which one can avoid using Hole explicitly when injecting -- placeholders in the result. type MacroTransLA' f q p g = forall a. q (Context g a) -> p -> f (q (Context g a) -> Context g a, p) -> Context g a -- | This function turns an MTT with regular look-ahead defined using the -- more convenient type |MacroTransLA'| into its canonical form of type -- |MacroTransLA|. mkMacroTransLA :: (Functor q, Functor f) => MacroTransLA' f q p g -> MacroTransLA f q p g -- | This function defines the semantics of MTTs with regular look-ahead. -- It applies a given MTT with regular look-ahead (including an -- accompanying bottom-up state transition function) to an input with and -- an initial state. runMacroTransLA :: (Functor g, Functor f, Functor q) => UpState f p -> MacroTransLA f q p g -> q (Term g) -> Term f -> Term g -- | This function composes an MTT with regular look-ahead followed by a -- DTT. compDownMacroLA :: (Functor f, Functor g, Functor h, Functor q1) => DownTrans g q2 h -> MacroTransLA f q1 p g -> MacroTransLA f (q1 :^: q2) p h -- | This type constructor is used to define the state space of an MTT that -- is obtained by composing an MTT followed by a DTT. data (:^:) q p a (:^:) :: q (p -> a) -> p -> :^: q p a -- | The identity Functor. newtype I a I :: a -> I a unI :: I a -> a instance Functor q => Functor (q :^: p) -- | 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 f :<: f :+: g and -- g :<: f :+: (g :+: h), non-examples include f :+: g -- :<: f :+: (g :+: h) and f :<: (f :+: g) :+: h. 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 -- | 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 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 g is compound of n atomic signatures, use -- projectn 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 termcontext to a termcontext over a -- sub-signature. If the signature g is compound of n -- atomic signatures, use deepProjectn 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 g is compound of n atomic signatures, use -- injectn 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 g is compound of n atomic signatures, -- use deepInjectn 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 a to a -- family f of contexts (possibly terms) indexed by a. -- That is, each hole h is replaced by the context f h. 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 f and g 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 f and -- g 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 f and -- g 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 f and -- g 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 macro tree transducer over signatures f and g -- to a macro tree transducer over the same signatures, but extended with -- annotations. propAnnMacro :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) => MacroTrans f q g -> MacroTrans f' q g' -- | Lift a macro tree transducer with regular look-ahead over signatures -- f and g to a macro tree transducer with regular -- look-ahead over the same signatures, but extended with annotations. propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) => MacroTransLA f q p g -> MacroTransLA f' q p g' -- | Lift a monadic term homomorphism over signatures f and -- g 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 -- | This function adds unique annotations to a term/context. Each node in -- the term/context is annotated with its path from the root, which is -- represented as an integer list. It is implemented as a DTT. pathAnn :: Traversable g => CxtFun g (g :&: [Int]) -- | This function is similar to project but applies to signatures -- with an annotation which is then ignored. project' :: (RemA f g, f :<: f1) => Cxt h f1 a -> Maybe (g (Cxt h f1 a)) -- | This module defines equality for signatures, which lifts to equality -- for terms and contexts. module Data.Comp.Equality -- | Signature equality. An instance EqF f gives rise to an -- instance Eq (Term f). class EqF f eqF :: (EqF f, Eq a) => f a -> f a -> Bool -- | This function implements equality of values of type f a -- modulo the equality of a itself. If two functorial values are -- equal in this sense, eqMod returns a Just 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 the subterm of a given term at the position -- specified by the given path or Nothing if the input term has -- no such subterm getSubterm :: (Functor g, Foldable g) => [Int] -> Term g -> Maybe (Term g) -- | This function returns the subterm of a given term at the position -- specified by the given path. This function is a variant of -- getSubterm which fails if there is no subterm at the given -- position. getSubterm' :: (Functor g, Foldable g) => [Int] -> Term g -> Term g -- | This function returns a list of all subterms of the given term. This -- function is similar to Uniplate's universe 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 -- transform 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 transform. 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 modules defines terms & 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 -- whnf 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 whnfPr. nfPr :: (Monad m, Traversable g, g :<: f) => TermT m f -> m (Term g) -- | This function inspects the topmost non-thunk node (using whnf) -- 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 -- whnf) 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 nf) 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 nf) 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 eval with flipped argument positions (#>) :: Monad m => TermT m f -> (f (TermT m f) -> TermT m f) -> TermT m f -- | Variant of deepEval 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 strict 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, 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 -- Functor, Foldable, and Traversable. 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 Functor -- and ShowF for a signature Exp, use derive as follows -- (requires Template Haskell): -- --

--   $(derive [makeFunctor, makeShowF] [''Exp])
--

derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] -- | Signature printing. An instance ShowF f gives rise to an -- instance Show (Term f). class ShowF f showF :: ShowF f => f String -> String -- | Derive an instance of ShowF for a type constructor of any -- first-order kind taking at least one argument. makeShowF :: Name -> Q [Dec] -- | Signature equality. An instance EqF f gives rise to an -- instance Eq (Term f). class EqF f eqF :: (EqF f, Eq a) => f a -> f a -> Bool -- | Derive an instance of EqF for a type constructor of any -- first-order kind taking at least one argument. makeEqF :: Name -> Q [Dec] -- | Signature ordering. An instance OrdF f gives rise to an -- instance Ord (Term f). class EqF f => OrdF f compareF :: (OrdF f, Ord a) => f a -> f a -> Ordering -- | Derive an instance of OrdF for a type constructor of any -- first-order kind taking at least one argument. makeOrdF :: Name -> Q [Dec] -- | The Functor class is used for types that can be mapped over. -- Instances of Functor should satisfy the following laws: -- --

--   fmap id  ==  id
--   fmap (f . g)  ==  fmap f . fmap g
--

-- -- The instances of Functor for lists, Maybe and IO -- satisfy these laws. class Functor (f :: * -> *) -- | Derive an instance of Functor 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: foldMap or foldr. -- -- For example, given a data type -- --

--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--

-- -- a suitable instance would be -- --

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

-- -- This is suitable even for abstract types, as the monoid is assumed to -- satisfy the monoid laws. Alternatively, one could define -- foldr: -- --

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

class Foldable (t :: * -> *) -- | Derive an instance of Foldable 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: traverse or sequenceA. -- -- Instances are similar to Functor, e.g. given a data type -- --

--   data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
--

-- -- a suitable instance would be -- --

--   instance Traversable Tree where
--      traverse f Empty = pure Empty
--      traverse f (Leaf x) = Leaf <$> f x
--      traverse f (Node l k r) = Node <$> traverse f l <*> f k <*> traverse f r
--

-- -- This is suitable even for abstract types, as the laws for -- <*> imply a form of associativity. -- -- The superclass instances should satisfy the following: -- --

In the Functor instance, fmap should be equivalent -- to traversal with the identity applicative functor -- (fmapDefault).
In the Foldable instance, foldMap should be -- equivalent to traversal with a constant applicative functor -- (foldMapDefault).

class (Functor t, Foldable t) => Traversable (t :: * -> *) -- | Derive an instance of Traversable for a type constructor of any -- first-order kind taking at least one argument. makeTraversable :: Name -> Q [Dec] -- | Derive an instance of HaskellStrict 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 ArbitraryF f gives rise to -- an instance Arbitrary (Term f). class ArbitraryF f where arbitraryF' = [(1, arbitraryF)] arbitraryF = frequency arbitraryF' shrinkF _ = [] 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 ArbitraryF 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 Arbitrary. 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 Arbitrary 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 NFData for a type constructor. makeNFData :: Name -> Q [Dec] -- | Signature normal form. An instance NFDataF f gives rise to an -- instance NFData (Term f). class NFDataF f rnfF :: (NFDataF f, NFData a) => f a -> () -- | Derive an instance of NFDataF 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 inject 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 injectA 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: class ShowF f where -- ... is lifted as instance (ShowF f, ShowF g) => ShowF (f -- :+: g) where .... liftSum :: Name -> Q [Dec] -- | This module defines ordering of signatures, which lifts to ordering of -- terms and contexts. module Data.Comp.Ordering -- | Signature ordering. An instance OrdF f gives rise to an -- instance Ord (Term f). 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 NFDataF f gives rise to an -- instance NFData (Term f). class NFDataF f rnfF :: (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) => NFDataF (f :&: a) 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 ArbitraryF f gives rise to -- an instance Arbitrary (Term f). class ArbitraryF f where arbitraryF' = [(1, arbitraryF)] arbitraryF = frequency arbitraryF' shrinkF _ = [] 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 showing of signatures, which lifts to showing of -- terms and contexts. module Data.Comp.Show -- | Signature printing. An instance ShowF f gives rise to an -- instance Show (Term f). 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 module defines an abstract notion of (bound) variables in -- compositional data types, and scoped substitution. Capture-avoidance -- is not taken into account. module Data.Comp.Variables -- | This multiparameter class defines functors with variables. An instance -- HasVar f v denotes that values over f might contain -- and bind variables of type v. class HasVars f v where isVar _ = Nothing bindsVars _ = empty isVar :: HasVars f v => f a -> Maybe v bindsVars :: (HasVars f v, Ord a) => f a -> Map a (Set 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 :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v -- | This function checks whether a variable is contained in a context. containsVar :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Cxt h f a -> Bool -- | This function computes the set of variables occurring in a context. variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v -- | This function computes the list of variables occurring in a context. variableList :: (Ord v, HasVars f v, Traversable 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 s1 and s2. -- That is, applying the resulting substitution is equivalent to first -- applying s2 and then s1. compSubst :: (Ord v, HasVars f v, Traversable f) => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v -- | This combinator pairs every argument of a given constructor with the -- set of (newly) bound variables according to the corresponding -- HasVars type class instance. getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a) instance [overlap ok] (SubstVars v t a, Functor f) => SubstVars v t (f a) instance [overlap ok] (Ord v, HasVars f v, Traversable f) => SubstVars v (Cxt h f a) (Cxt h f a) 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 c as the first argument and -- tries to match it against the term t (or in general a context -- with holes in a). The context c matches the term -- t if there is a matching substitution s that -- maps holes to terms (resp. contexts in general) such that if the holes -- in the context c are replaced according to the substitution -- s, the term t is obtained. Note that the context -- c 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 matchCxt but instead of a context -- it matches a term with variables against a context. matchTerm :: (Ord v, EqF f, Eq (Cxt h f a), Traversable 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 recursive program schemes. type RPS f g = Hom f g -- | This type represents variables. type Var = Int -- | This type represents term rewrite rules from signature f to -- signature g over variables of type v type Rule f g v = (Context f v, Context g v) -- | This type represents term rewriting systems (TRSs) from signature -- f to signature g over variables of type v. 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 False. Otherwise, the successor is returned together -- with True. 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 Nothing. 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 appRule until one rule is applicable. If no -- rule is applicable Nothing 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 f of type -- (t -> Maybe t) into functions f' of type t -- -> (t,Bool). f' x evaluates to (y,True) if -- f x evaluates to Just y, and to (x,False) -- if f x evaluates to Nothing. This function is useful -- to change the output of functions that apply rules such as -- appTRS. 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, Nothing 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, Nothing 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 where decomp t = case isVar t of { Just v -> Var v Nothing -> Fun sym args where sym = fmap (const ()) t args = arguments t } 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, Traversable 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), Traversable 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, Traversable f) => (v, Term f) -> UnifyM f v m () runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => UnifyM f v m () unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => Equation f -> UnifyM f v m () instance Error (UnifError f v) -- | This module defines the infrastructure necessary to use -- Compositional Data Types. Compositional Data Types is an -- extension of Wouter Swierstra's Functional Pearl: Data types a la -- carte. Examples of usage are bundled with the package in the -- library examples/Examples. module Data.Comp -- | This modules defines the Desugar type class for desugaring of -- terms. module Data.Comp.Desugar -- | The desugaring term homomorphism. class (Functor f, Functor 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 => 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 h, Desugar g h) => Desugar (f :+: g) h