-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Compositional Data Types
--
@package compdata
@version 0.8.1.2
-- | 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)
module Data.Comp.Automata.Product
type (:<) e p = IsElem (Elem e p) e p
pr :: e :< p => p -> e
instance [incoherent] IsElem ('Found pos) e p => IsElem ('Found ('Ri pos)) e (p', p)
instance [incoherent] IsElem ('Found pos) e p => IsElem ('Found ('Le pos)) e (p, p')
instance [incoherent] IsElem ('Found 'Here) e e
-- | This module defines some utility functions for deriving instances for
-- functor based type classes.
module Data.Comp.Derive.Utils
-- | This is the Q-lifted version of 'abstractNewtypeQ.
abstractNewtypeQ :: Q Info -> Q Info
-- | This function abstracts away newtype declaration, it turns
-- them into data declarations.
abstractNewtype :: Info -> Info
-- | This function provides the name and the arity of the given data
-- constructor.
normalCon :: Con -> (Name, [StrictType])
normalCon' :: Con -> (Name, [Type])
-- | Same as normalCon' but expands type synonyms.
normalConExp :: Con -> Q (Name, [Type])
-- | Same as normalConExp' but retains strictness annotations.
normalConStrExp :: Con -> Q (Name, [StrictType])
-- | This function provides the name and the arity of the given data
-- constructor.
abstractConType :: Con -> (Name, Int)
-- | This function returns the name of a bound type variable
tyVarBndrName :: TyVarBndr -> Name
containsType :: Type -> Type -> Bool
containsType' :: Type -> Type -> [Int]
-- | This function provides a list (of the given length) of new names based
-- on the given string.
newNames :: Int -> String -> Q [Name]
tupleTypes :: Int -> Int -> [Name]
-- | 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]
-- | This function lifts type class instances over sums ofsignatures. To
-- this end it assumes that it contains only methods with types of the
-- form f t1 .. tn -> t where f is the signature
-- that is used to construct sums. Since this function is generic it
-- assumes as its first argument the name of the function that is used to
-- lift methods over sums i.e. a function of type
--
--
-- (f t1 .. tn -> t) -> (g t1 .. tn -> t) -> ((f :+: g) t1 .. tn -> t)
--
--
-- where :+: is the sum type constructor. The second argument to
-- this function is expected to be the name of that constructor. The last
-- argument is the name of the class whose instances should be lifted
-- over sums.
liftSumGen :: Name -> Name -> Name -> Q [Dec]
findSig :: [Name] -> [Dec] -> Q (Maybe ([Name], [Name]))
-- | 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.
--
-- A definition of traverse must satisfy the following laws:
--
--
--
-- A definition of sequenceA must satisfy the following laws:
--
--
--
-- where an applicative transformation is a function
--
--
-- t :: (Applicative f, Applicative g) => f a -> g a
--
--
-- preserving the Applicative operations, i.e.
--
--
--
-- and the identity functor Identity and composition of functors
-- Compose are defined as
--
--
-- newtype Identity a = Identity a
--
-- instance Functor Identity where
-- fmap f (Identity x) = Identity (f x)
--
-- instance Applicative Indentity where
-- pure x = Identity x
-- Identity f <*> Identity x = Identity (f x)
--
-- newtype Compose f g a = Compose (f (g a))
--
-- instance (Functor f, Functor g) => Functor (Compose f g) where
-- fmap f (Compose x) = Compose (fmap (fmap f) x)
--
-- instance (Applicative f, Applicative g) => Applicative (Compose f g) where
-- pure x = Compose (pure (pure x))
-- Compose f <*> Compose x = Compose ((<*>) <$> f <*> x)
--
--
-- (The naturality law is implied by parametricity.)
--
-- 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
fromInl :: (f :+: g) e -> Maybe (f e)
fromInr :: (f :+: g) e -> Maybe (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
data Proxy a
P :: Proxy a
class Subsume (e :: Emb) (f :: * -> *) (g :: * -> *)
inj' :: Subsume e f g => Proxy e -> f a -> g a
prj' :: Subsume e f g => Proxy e -> g a -> Maybe (f a)
-- | A constraint f :<: g expresses that the signature
-- f is subsumed by g, i.e. f can be used to
-- construct elements in g.
type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
inj :: f :<: g => f a -> g a
proj :: f :<: g => g a -> Maybe (f a)
type (:=:) f g = (f :<: g, g :<: f)
spl :: f :=: (f1 :+: f2) => (f1 a -> b) -> (f2 a -> b) -> f a -> b
-- | 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 DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance DistAnn f p (f :&: p)
instance RemA (f :&: p) f
instance RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance Traversable f => Traversable (f :&: a)
instance Foldable f => Foldable (f :&: a)
instance Functor f => Functor (f :&: a)
instance (Subsume ('Found p1) f1 g, Subsume ('Found p2) f2 g) => Subsume ('Found ('Sum p1 p2)) (f1 :+: f2) g
instance Subsume ('Found p) f g => Subsume ('Found ('Ri p)) f (g' :+: g)
instance Subsume ('Found p) f g => Subsume ('Found ('Le p)) f (g :+: g')
instance Subsume ('Found 'Here) f f
instance (Traversable f, Traversable g) => Traversable (f :+: g)
instance (Foldable f, Foldable g) => Foldable (f :+: g)
instance (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
data Proxy a
P :: Proxy a
class Subsume (e :: Emb) (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
inj' :: Subsume e f g => Proxy e -> f a :-> g a
prj' :: Subsume e f g => Proxy e -> NatM Maybe (g a) (f a)
-- | A constraint f :<: g expresses that the signature
-- f is subsumed by g, i.e. f can be used to
-- construct elements in g.
type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
inj :: f :<: g => f a :-> g a
proj :: f :<: g => NatM Maybe (g a) (f a)
type (:=:) f g = (f :<: g, g :<: f)
spl :: f :=: (f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
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 [overlap ok] DistAnn s p s' => DistAnn (f :+: s) p ((f :&: p) :+: s')
instance [overlap ok] DistAnn f p (f :&: p)
instance [overlap ok] RemA (f :&: p) f
instance [overlap ok] RemA s s' => RemA ((f :&: p) :+: s) (f :+: s')
instance [overlap ok] HTraversable f => HTraversable (f :&: a)
instance [overlap ok] HFoldable f => HFoldable (f :&: a)
instance [overlap ok] HFunctor f => HFunctor (f :&: a)
instance [overlap ok] (Subsume ('Found p1) f1 g, Subsume ('Found p2) f2 g) => Subsume ('Found ('Sum p1 p2)) (f1 :+: f2) g
instance [overlap ok] Subsume ('Found p) f g => Subsume ('Found ('Ri p)) f (g' :+: g)
instance [overlap ok] Subsume ('Found p) f g => Subsume ('Found ('Le p)) f (g :+: g')
instance [overlap ok] Subsume ('Found 'Here) f f
instance [overlap ok] (HTraversable f, HTraversable g) => HTraversable (f :+: g)
instance [overlap ok] (HFoldable f, HFoldable g) => HFoldable (f :+: g)
instance [overlap ok] (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
-- | A constraint f :<: g expresses that the signature
-- f is subsumed by g, i.e. f can be used to
-- construct elements in g.
type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
-- | 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
proj :: f :<: g => NatM Maybe (g a) (f 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 => NatM Maybe (Cxt h f a) (g (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 :: (HTraversable g, g :<: f) => CxtFunM Maybe f g
inj :: f :<: g => f 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
-- | 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
split :: f :=: (f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f 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 type generic functions and recursive schemes along
-- the lines of the Uniplate library. All definitions are generalised
-- versions of those in Data.Comp.Generic.
module Data.Comp.Multi.Generic
-- | This function returns a list of all subterms of the given term. This
-- function is similar to Uniplate's universe function.
subterms :: HFoldable f => Term f :=> [E (Term f)]
-- | This function returns a list of all subterms of the given term that
-- are constructed from a particular functor.
subterms' :: (HFoldable f, g :<: f) => Term f :=> [E (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 :: HFunctor f => (Term f :-> Term f) -> Term f :-> Term f
-- | Monadic version of transform.
transformM :: (HTraversable f, Monad m) => NatM m (Term f) (Term f) -> NatM m (Term f) (Term f)
query :: HFoldable f => (Term f :=> r) -> (r -> r -> r) -> Term f :=> r
subs :: HFoldable f => Term f :=> [E (Term f)]
subs' :: (HFoldable f, g :<: f) => Term f :=> [E (g (Term f))]
-- | This function computes the generic size of the given term, i.e. the
-- its number of subterm occurrences.
size :: HFoldable f => Cxt h f a :=> Int
-- | This function computes the generic depth of the given term.
depth :: HFoldable f => Cxt h f a :=> Int
-- | This module defines 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
--
--
-- 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
-- | This function transforms a function with a domain constructed from a
-- functor to a function with a domain constructed with the same functor
-- but with an additional annotation.
liftA :: RemA s s' => (s' a :-> t) -> s a :-> t
-- | This function annotates each sub term of the given term with the given
-- value (of type a).
ann :: (DistAnn f p g, HFunctor f) => p -> CxtFun f g
-- | This function transforms a function with a domain constructed from a
-- functor to a function with a domain constructed with the same functor
-- but with an additional annotation.
liftA' :: (DistAnn s' p s, HFunctor s') => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a
-- | This function strips the annotations from a term over a functor with
-- annotations.
stripA :: (RemA g f, HFunctor g) => CxtFun g f
propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g) => Hom f g -> Hom f' g'
-- | This function is similar to project but applies to signatures
-- with an annotation which is then ignored.
project' :: (RemA f f', s :<: f') => Cxt h f a i -> Maybe (s (Cxt h f a) i)
-- | This module defines equality for (higher-order) signatures, which
-- lifts to equality for (higher-order) terms and contexts. All
-- definitions are generalised versions of those in
-- Data.Comp.Equality.
module Data.Comp.Multi.Equality
-- | 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
-- | 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.
heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(E a, E b)]
instance (EqHF f, KEq a) => Eq (Cxt h f a i)
instance (EqHF f, KEq a) => KEq (Cxt h f a)
instance EqHF f => EqHF (Cxt h f)
instance (EqHF f, EqHF g) => EqHF (f :+: g)
instance KEq a => Eq (E a)
instance Eq a => KEq (K a)
-- | This module defines the infrastructure necessary to use Generalised
-- Compositional Data Types. Generalised Compositional Data Types is
-- an extension of Compositional Data Types with mutually recursive data
-- types, and more generally GADTs. Examples of usage are bundled with
-- the package in the library examples/Examples/Multi.
module Data.Comp.Multi
-- | This modules defines the Desugar type class for desugaring of
-- terms.
module Data.Comp.Multi.Desugar
-- | The desugaring term homomorphism.
class (HFunctor f, HFunctor 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 => Alg f (Context g a)
-- | Desugar a term.
desugar :: Desugar f g => Term f :-> Term g
-- | Lift desugaring to annotated terms.
desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g', Desugar f g) => Term f' :-> Term g'
-- | Default desugaring instance.
instance [overlap ok] (HFunctor f, HFunctor 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.Multi.Ordering
class KEq f => KOrd f
kcompare :: KOrd f => f i -> f j -> Ordering
-- | 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
instance [incoherent] (HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i)
instance [incoherent] (HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a)
instance [incoherent] (HFunctor f, OrdHF f) => OrdHF (Cxt h f)
instance [incoherent] (OrdHF f, OrdHF g) => OrdHF (f :+: g)
instance [incoherent] Ord a => KOrd (K a)
instance [incoherent] KOrd f => Ord (E f)
-- | This module provides functionality to number the components of a
-- functorial value with consecutive integers.
module Data.Comp.Multi.Number
-- | This type is used for numbering components of a functorial value.
newtype Numbered a i
Numbered :: (Int, a i) -> Numbered a i
unNumbered :: Numbered a :-> a
-- | This function numbers the components of the given functorial value
-- with consecutive integers starting at 0.
number :: HTraversable f => f a :-> f (Numbered a)
class HFoldable t => HTraversable t
instance KOrd (Numbered a)
instance KEq (Numbered a)
-- | This module contains functionality for automatically deriving
-- boilerplate code using Template Haskell. Examples include instances of
-- HFunctor, HFoldable, and HTraversable.
module Data.Comp.Multi.Derive
-- | Helper function for generating a list of instances for a list of named
-- signatures. For example, in order to derive instances 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 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 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 => Monad (Context f)
instance Functor f => Applicative (Context 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 provides the infrastructure to extend signatures.
module Data.Comp.Sum
-- | A constraint f :<: g expresses that the signature
-- f is subsumed by g, i.e. f can be used to
-- construct elements in g.
type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
type (:=:) f g = (f :<: g, g :<: f)
-- | 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
data Proxy a
P :: Proxy a
proj :: f :<: g => g a -> Maybe (f 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))
-- | 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
-- | 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_ :: (SigFunM Maybe f g) -> Cxt h f a -> Maybe (g (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 => (SigFunM Maybe f g) -> CxtFunM Maybe f g
inj :: f :<: g => f 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
-- | 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
-- | 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_ :: (SigFun g f) -> g (Cxt h f a) -> Cxt h f 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 => SigFun g f -> CxtFun g f
split :: f :=: (f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f 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 [overlap ok] (Eq (f a), Eq (g a)) => Eq ((:+:) f g a)
instance [overlap ok] (Ord (f a), Ord (g a)) => Ord ((:+:) f g a)
instance [overlap ok] (Show (f a), Show (g a)) => Show ((:+:) f g 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 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 = q :< p => DUpState' f p 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 = q :< p => DDownState' f p 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 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 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 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 f', s :<: f') => Cxt h f a -> Maybe (s (Cxt h f a))
-- | 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 (CxtT m h f a) -> CxtT m 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]
-- | Constructor printing.
class ShowConstr f
showConstr :: ShowConstr f => f a -> String
-- | Derive an instance of showConstr for a type constructor of any
-- first-order kind taking at least one argument.
makeShowConstr :: 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.
--
-- A definition of traverse must satisfy the following laws:
--
--
--
-- A definition of sequenceA must satisfy the following laws:
--
--
--
-- where an applicative transformation is a function
--
--
-- t :: (Applicative f, Applicative g) => f a -> g a
--
--
-- preserving the Applicative operations, i.e.
--
--
--
-- and the identity functor Identity and composition of functors
-- Compose are defined as
--
--
-- newtype Identity a = Identity a
--
-- instance Functor Identity where
-- fmap f (Identity x) = Identity (f x)
--
-- instance Applicative Indentity where
-- pure x = Identity x
-- Identity f <*> Identity x = Identity (f x)
--
-- newtype Compose f g a = Compose (f (g a))
--
-- instance (Functor f, Functor g) => Functor (Compose f g) where
-- fmap f (Compose x) = Compose (fmap (fmap f) x)
--
-- instance (Applicative f, Applicative g) => Applicative (Compose f g) where
-- pure x = Compose (pure (pure x))
-- Compose f <*> Compose x = Compose ((<*>) <$> f <*> x)
--
--
-- (The naturality law is implied by parametricity.)
--
-- 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 :<: (m :+: g)) => f (TermT m g) -> TermT m g
haskellStrict' :: (Monad m, HaskellStrict f, f :<: (m :+: 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.
--
-- Since: 1.1.0.0
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 (ShowConstr f, ShowConstr g) => ShowConstr (f :+: g)
instance (ShowConstr f, Show p) => ShowConstr (f :&: p)
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
module Data.Comp.Render
-- | The stringTree algebra of a functor. The default instance
-- creates a tree with the same structure as the term.
class (Functor f, Foldable f, ShowConstr f) => Render f where stringTreeAlg f = Node (showConstr f) $ toList f
stringTreeAlg :: Render f => Alg f (Tree String)
-- | Convert a term to a Tree
stringTree :: Render f => Term f -> Tree String
-- | Show a term using ASCII art
showTerm :: Render f => Term f -> String
-- | Print a term using ASCII art
drawTerm :: Render f => Term f -> IO ()
-- | Write a term to an HTML file with foldable nodes
writeHtmlTerm :: Render f => FilePath -> Term f -> IO ()
instance (Render f, Render g) => Render (f :+: g)
-- | 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'
-- | Default desugaring instance.
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