-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Compositional Data Types
--
-- This library implements the ideas of Data types a la carte
-- (Journal of Functional Programming, 18(4):423-436, 2008,
-- http://dx.doi.org/10.1017/S0956796808006758) as outlined in the
-- paper Compositional data types (Workshop on Generic
-- Programming, 83-94, 2011,
-- http://dx.doi.org/10.1145/2036918.2036930). The purpose of this
-- library is to allow the programmer to construct data types -- as well
-- as the functions defined on them -- in a modular fashion. The
-- underlying idea is to separate the signature of a data type from the
-- fixed point construction that produces its recursive structure.
-- Signatures can then be composed and decomposed freely.
--
-- Building on that foundation, this library provides additional
-- extensions and (run-time) optimisations which make compositional data
-- types usable for practical implementations. In particular, it provides
-- an excellent framework for manipulating and analysing abstract syntax
-- trees in a type-safe manner. Thus, it is perfectly suited for
-- programming language implementations, especially, in an environment
-- consisting of a family of tightly interwoven domain-specific
-- languages.
--
-- In concrete terms, this library provides the following features:
--
--
-- - Compositional data types in the style of Wouter Swierstra's
-- Functional Pearl Data types a la carte. The implementation of
-- signature subsumption is based on the paper Composing and
-- Decomposing Data Types (Workshop on Generic Programming, 2014, to
-- appear), which makes signature composition more flexible.
-- - Modular definition of functions on compositional data types
-- through catamorphisms and anamorphisms as well as more structured
-- recursion schemes such as primitive recursion and co-recursion, and
-- course-of-value iteration and co-iteration.
-- - Support for monadic computations via monadic variants of all
-- recursion schemes.
-- - Support of a succinct programming style over compositional data
-- types via generic programming combinators that allow various forms of
-- generic transformations and generic queries.
-- - Generalisation of compositional data types (terms) to
-- compositional data types "with holes" (contexts). This allows flexible
-- reuse of a wide variety of catamorphisms (called term
-- homomorphisms) as well as an efficient composition of them.
-- - Operations on signatures, for example, to add and remove
-- annotations of abstract syntax trees. This includes combinators to
-- propagate annotations fully automatically through certain term
-- homomorphisms.
-- - Optimisation of the implementation of recursion schemes. This
-- includes short-cut fusion style optimisation rules which yield
-- a performance boost of up to factor six.
-- - Automatic derivation of instances of all relevant type classes for
-- using compositional data types via Template Haskell. This
-- includes instances of Prelude.Eq, Prelude.Ord and
-- Prelude.Show that are derived via instances for functorial
-- variants of them. Additionally, also smart constructors, which
-- allow to easily construct inhabitants of compositional data types, are
-- automatically generated.
-- - Mutually recursive data types and generalised algebraic
-- data types (GADTs). All of the above is also lifted to families of
-- mutually recursive data types and (more generally) GADTs. This
-- extension resides in the module Data.Comp.Multi.
--
--
-- Examples of using (generalised) compositional data types are bundled
-- with the package in the folder examples.
--
-- There are some supplementary packages, some of which were included in
-- previous versions of this package:
--
--
@package compdata
@version 0.10.1
-- | 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
-- | A higher-order functor f also maps a natural transformation
-- g :-> h to a natural transformation f g :-> f
-- 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 t
instance Data.Traversable.Traversable (Data.Comp.Multi.HFunctor.K a)
instance Data.Foldable.Foldable (Data.Comp.Multi.HFunctor.K a)
instance GHC.Base.Functor (Data.Comp.Multi.HFunctor.K a)
instance Data.Traversable.Traversable Data.Comp.Multi.HFunctor.I
instance Data.Foldable.Foldable Data.Comp.Multi.HFunctor.I
instance GHC.Base.Functor Data.Comp.Multi.HFunctor.I
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Comp.Multi.HFunctor.K a i)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Comp.Multi.HFunctor.K a i)
instance GHC.Base.Functor f => Data.Comp.Multi.HFunctor.HFunctor (Data.Functor.Compose.Compose f)
-- | 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
-- | Map each element of a structure to a monadic action, evaluate these
-- actions from left to right, and collect the results.
--
-- Alternative type in terms of natural transformations using functor
-- composition :.::
--
--
-- hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)
--
hmapM :: (HTraversable t, Monad m) => NatM m a b -> NatM m (t a) (t b)
htraverse :: (HTraversable t, Applicative f) => NatM f a b -> NatM f (t a) (t b)
-- | This module provides functionality to construct mappings from
-- positions in a functorial value.
module Data.Comp.Multi.Mapping
-- | This type is used for numbering components of a functorial value.
data 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
class Mapping m (k :: * -> *) | m -> k
-- | left-biased union of two mappings.
(&) :: Mapping m k => m v -> m v -> m v
-- | This operator constructs a singleton mapping.
(|->) :: Mapping m k => k i -> v -> m v
-- | This is the empty mapping.
empty :: Mapping m k => m v
-- | This function constructs the pointwise product of two maps each with a
-- default value.
prodMap :: Mapping m k => v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
-- | Returns the value at the given key or returns the given default when
-- the key is not an element of the map.
findWithDefault :: Mapping m k => a -> k i -> m a -> a
lookupNumMap :: a -> Int -> NumMap t a -> a
instance GHC.Base.Functor (Data.Comp.Multi.Mapping.NumMap k)
instance Data.Comp.Multi.Mapping.Mapping (Data.Comp.Multi.Mapping.NumMap k) (Data.Comp.Multi.Mapping.Numbered k)
-- | 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 Data.Comp.Multi.HFunctor.HFunctor f => Data.Comp.Multi.HFunctor.HFunctor (Data.Comp.Multi.Term.Cxt h f)
instance Data.Comp.Multi.HFoldable.HFoldable f => Data.Comp.Multi.HFoldable.HFoldable (Data.Comp.Multi.Term.Cxt h f)
instance Data.Comp.Multi.HTraversable.HTraversable f => Data.Comp.Multi.HTraversable.HTraversable (Data.Comp.Multi.Term.Cxt h f)
-- | This module provides a generic projection function pr for
-- arbitrary nested binary products.
module Data.Comp.Projection
-- | This function projects the component of type e out or the
-- compound value of type p.
pr :: (p :< q) => q -> p
-- | The constraint e :< p expresses that e is a
-- component of the type p. That is, p is formed by
-- binary products using the type e. The occurrence of
-- e must be unique. For example we have Int :<
-- (Bool,(Int,Bool)) but not Bool :< (Bool,(Int,Bool)).
type (:<) f g = Proj (ComprEmb (Elem f g)) f g
instance Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found 'Data.Comp.SubsumeCommon.Here) f f
instance Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Le p)) f (g, g')
instance Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Ri p)) f (g', g)
instance (Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found p1) f1 g, Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found p2) f2 g) => Data.Comp.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Sum p1 p2)) (f1, f2) g
-- | This module provides functionality to construct mappings from
-- positions in a functorial value.
module Data.Comp.Mapping
-- | This type is used for numbering components of a functorial value.
data 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.
--
-- 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 :: * -> *)
class Functor m => Mapping m k | m -> k
-- | left-biased union of two mappings.
(&) :: Mapping m k => m v -> m v -> m v
-- | This operator constructs a singleton mapping.
(|->) :: Mapping m k => k -> v -> m v
-- | This is the empty mapping.
empty :: Mapping m k => m v
-- | This function constructs the pointwise product of two maps each with a
-- default value.
prodMapWith :: Mapping m k => (v1 -> v2 -> v) -> v1 -> v2 -> m v1 -> m v2 -> m v
-- | Returns the value at the given key or returns the given default when
-- the key is not an element of the map.
findWithDefault :: Mapping m k => a -> k -> m a -> a
-- | This function constructs the pointwise product of two maps each with a
-- default value.
prodMap :: Mapping m k => v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
lookupNumMap :: a -> Int -> NumMap t a -> a
lookupNumMap' :: Int -> NumMap t a -> Maybe a
data NumMap k v
instance Data.Traversable.Traversable (Data.Comp.Mapping.NumMap k)
instance Data.Foldable.Foldable (Data.Comp.Mapping.NumMap k)
instance GHC.Base.Functor (Data.Comp.Mapping.NumMap k)
instance Data.Comp.Mapping.Mapping (Data.Comp.Mapping.NumMap k) (Data.Comp.Mapping.Numbered k)
-- | This module defines some utility functions for deriving instances for
-- functor based type classes.
module Data.Comp.Derive.Utils
data DataInfo
DataInfo :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> DataInfo
-- | This is the Q-lifted version of 'abstractNewtype.
abstractNewtypeQ :: Q Info -> Q (Maybe DataInfo)
-- | This function abstracts away newtype declaration, it turns
-- them into data declarations.
abstractNewtype :: Info -> Maybe DataInfo
-- | This function provides the name and the arity of the given data
-- constructor, and if it is a GADT also its type.
normalCon :: Con -> (Name, [StrictType], Maybe Type)
normalCon' :: Con -> (Name, [Type], Maybe Type)
-- | Same as normalCon' but expands type synonyms.
normalConExp :: Con -> Q (Name, [Type], Maybe Type)
-- | Same as normalConExp' but retains strictness annotations.
normalConStrExp :: Con -> Q (Name, [StrictType], Maybe Type)
-- | Auxiliary function to extract the first argument of a binary type
-- application (the second argument of this function). If the second
-- argument is Nothing or not of the right shape, the first
-- argument is returned as a default.
getBinaryFArg :: Type -> Maybe Type -> Type
-- | Auxiliary function to extract the first argument of a type application
-- (the second argument of this function). If the second argument is
-- Nothing or not of the right shape, the first argument is
-- returned as a default.
getUnaryFArg :: Type -> Maybe Type -> Type
-- | 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]
-- | Apply a class name to type arguments to construct a type class
-- constraint.
mkClassP :: Name -> [Type] -> Type
-- | This function checks whether the given type constraint is an equality
-- constraint. If so, the types of the equality constraint are returned.
isEqualP :: Type -> Maybe (Type, Type)
mkInstanceD :: Cxt -> Type -> [Dec] -> 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 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
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
-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a -> s' a
-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a -> (s a, p)
class RemA s s' | s -> s'
-- | Remove annotations from a signature.
remA :: RemA s s' => s a -> s' a
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (f Data.Comp.Ops.:+: g)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable g) => Data.Foldable.Foldable (f Data.Comp.Ops.:+: g)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable g) => Data.Traversable.Traversable (f Data.Comp.Ops.:+: g)
instance Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found 'Data.Comp.SubsumeCommon.Here) f f
instance Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Le p)) f (g Data.Comp.Ops.:+: g')
instance Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Ri p)) f (g' Data.Comp.Ops.:+: g)
instance (Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p1) f1 g, Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p2) f2 g) => Data.Comp.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Sum p1 p2)) (f1 Data.Comp.Ops.:+: f2) g
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (f Data.Comp.Ops.:*: g)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable g) => Data.Foldable.Foldable (f Data.Comp.Ops.:*: g)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable g) => Data.Traversable.Traversable (f Data.Comp.Ops.:*: g)
instance GHC.Base.Functor f => GHC.Base.Functor (f Data.Comp.Ops.:&: a)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (f Data.Comp.Ops.:&: a)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (f Data.Comp.Ops.:&: a)
instance forall (k :: BOX) (f :: k -> *) p (s :: k -> *) (s' :: k -> *). Data.Comp.Ops.RemA s s' => Data.Comp.Ops.RemA ((f Data.Comp.Ops.:&: p) Data.Comp.Ops.:+: s) (f Data.Comp.Ops.:+: s')
instance forall (k :: BOX) (f :: k -> *) p. Data.Comp.Ops.RemA (f Data.Comp.Ops.:&: p) f
instance forall (k :: BOX) (f :: k -> *) p. Data.Comp.Ops.DistAnn f p (f Data.Comp.Ops.:&: p)
instance forall (k :: BOX) (f :: k -> *) (s :: k -> *) p (s' :: k -> *). Data.Comp.Ops.DistAnn s p s' => Data.Comp.Ops.DistAnn (f Data.Comp.Ops.:+: s) p ((f Data.Comp.Ops.:&: p) Data.Comp.Ops.:+: s')
-- | 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
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
-- | 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
-- | This function injects an annotation over a signature.
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
-- | 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
instance (Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.HFunctor.HFunctor g) => Data.Comp.Multi.HFunctor.HFunctor (f Data.Comp.Multi.Ops.:+: g)
instance (Data.Comp.Multi.HFoldable.HFoldable f, Data.Comp.Multi.HFoldable.HFoldable g) => Data.Comp.Multi.HFoldable.HFoldable (f Data.Comp.Multi.Ops.:+: g)
instance (Data.Comp.Multi.HTraversable.HTraversable f, Data.Comp.Multi.HTraversable.HTraversable g) => Data.Comp.Multi.HTraversable.HTraversable (f Data.Comp.Multi.Ops.:+: g)
instance Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found 'Data.Comp.SubsumeCommon.Here) f f
instance Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Le p)) f (g Data.Comp.Multi.Ops.:+: g')
instance Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Ri p)) f (g' Data.Comp.Multi.Ops.:+: g)
instance (Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p1) f1 g, Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found p2) f2 g) => Data.Comp.Multi.Ops.Subsume ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Sum p1 p2)) (f1 Data.Comp.Multi.Ops.:+: f2) g
instance Data.Comp.Multi.HFunctor.HFunctor f => Data.Comp.Multi.HFunctor.HFunctor (f Data.Comp.Multi.Ops.:&: a)
instance Data.Comp.Multi.HFoldable.HFoldable f => Data.Comp.Multi.HFoldable.HFoldable (f Data.Comp.Multi.Ops.:&: a)
instance Data.Comp.Multi.HTraversable.HTraversable f => Data.Comp.Multi.HTraversable.HTraversable (f Data.Comp.Multi.Ops.:&: a)
instance Data.Comp.Multi.Ops.RemA s s' => Data.Comp.Multi.Ops.RemA ((f Data.Comp.Multi.Ops.:&: p) Data.Comp.Multi.Ops.:+: s) (f Data.Comp.Multi.Ops.:+: s')
instance Data.Comp.Multi.Ops.RemA (f Data.Comp.Multi.Ops.:&: p) f
instance Data.Comp.Multi.Ops.DistAnn f p (f Data.Comp.Multi.Ops.:&: p)
instance Data.Comp.Multi.Ops.DistAnn s p s' => Data.Comp.Multi.Ops.DistAnn (f Data.Comp.Multi.Ops.:+: s) p ((f Data.Comp.Multi.Ops.:&: p) Data.Comp.Multi.Ops.:+: s')
-- | 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
-- | This function injects an annotation over a signature.
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 GHC.Classes.Eq a => Data.Comp.Multi.Equality.KEq (Data.Comp.Multi.HFunctor.K a)
instance Data.Comp.Multi.Equality.KEq a => GHC.Classes.Eq (Data.Comp.Multi.HFunctor.E a)
instance (Data.Comp.Multi.Equality.EqHF f, Data.Comp.Multi.Equality.EqHF g) => Data.Comp.Multi.Equality.EqHF (f Data.Comp.Multi.Ops.:+: g)
instance Data.Comp.Multi.Equality.EqHF f => Data.Comp.Multi.Equality.EqHF (Data.Comp.Multi.Term.Cxt h f)
instance (Data.Comp.Multi.Equality.EqHF f, Data.Comp.Multi.Equality.KEq a) => Data.Comp.Multi.Equality.KEq (Data.Comp.Multi.Term.Cxt h f a)
instance (Data.Comp.Multi.Equality.EqHF f, Data.Comp.Multi.Equality.KEq a) => GHC.Classes.Eq (Data.Comp.Multi.Term.Cxt h f a i)
-- | 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 (Data.Comp.Multi.Desugar.Desugar f h, Data.Comp.Multi.Desugar.Desugar g h) => Data.Comp.Multi.Desugar.Desugar (f Data.Comp.Multi.Ops.:+: g) h
instance (Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.HFunctor.HFunctor g, f Data.Comp.Multi.Ops.:<: g) => Data.Comp.Multi.Desugar.Desugar f g
-- | 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 Data.Comp.Multi.Ordering.KOrd f => GHC.Classes.Ord (Data.Comp.Multi.HFunctor.E f)
instance GHC.Classes.Ord a => Data.Comp.Multi.Ordering.KOrd (Data.Comp.Multi.HFunctor.K a)
instance (Data.Comp.Multi.Ordering.OrdHF f, Data.Comp.Multi.Ordering.OrdHF g) => Data.Comp.Multi.Ordering.OrdHF (f Data.Comp.Multi.Ops.:+: g)
instance (Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.Ordering.OrdHF f) => Data.Comp.Multi.Ordering.OrdHF (Data.Comp.Multi.Term.Cxt h f)
instance (Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.Ordering.OrdHF f, Data.Comp.Multi.Ordering.KOrd a) => Data.Comp.Multi.Ordering.KOrd (Data.Comp.Multi.Term.Cxt h f a)
instance (Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.Ordering.OrdHF f, Data.Comp.Multi.Ordering.KOrd a) => GHC.Classes.Ord (Data.Comp.Multi.Term.Cxt h f a i)
-- | 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 (Data.Comp.Multi.Derive.Show.ShowHF f, Data.Comp.Multi.Derive.Show.ShowHF g) => Data.Comp.Multi.Derive.Show.ShowHF (f Data.Comp.Multi.Ops.:+: g)
instance Data.Comp.Multi.Derive.Show.KShow (Data.Comp.Multi.HFunctor.K GHC.Base.String)
instance Data.Comp.Multi.Derive.Show.KShow (Data.Comp.Multi.HFunctor.K ())
instance (Data.Comp.Multi.Derive.Show.ShowHF f, Data.Comp.Multi.HFunctor.HFunctor f) => Data.Comp.Multi.Derive.Show.ShowHF (Data.Comp.Multi.Term.Cxt h f)
instance (Data.Comp.Multi.Derive.Show.ShowHF f, Data.Comp.Multi.HFunctor.HFunctor f, Data.Comp.Multi.Derive.Show.KShow a) => Data.Comp.Multi.Derive.Show.KShow (Data.Comp.Multi.Term.Cxt h f a)
instance Data.Comp.Multi.Derive.Show.KShow (Data.Comp.Multi.Term.Cxt h f a) => GHC.Show.Show (Data.Comp.Multi.Term.Cxt h f a i)
instance (Data.Comp.Multi.Derive.Show.ShowHF f, GHC.Show.Show p) => Data.Comp.Multi.Derive.Show.ShowHF (f Data.Comp.Multi.Ops.:&: p)
-- | 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
-- | Indicates whether the f constructor is a variable. The
-- default implementation returns Nothing.
isVar :: HasVars f v => f a :=> Maybe v
-- | Indicates the set of variables bound by the f constructor for
-- each argument of the constructor. For example for a non-recursive let
-- binding:
--
--
-- data Let i e = Let Var (e i) (e i)
-- instance HasVars Let Var where
-- bindsVars (Let v x y) = y |-> Set.singleton v
--
--
-- If, instead, the let binding is recursive, the methods has to be
-- implemented like this:
--
--
-- bindsVars (Let v x y) = x |-> Set.singleton v &
-- y |-> Set.singleton v
--
--
-- This indicates that the scope of the bound variable also extends to
-- the right-hand side of the variable binding.
--
-- The default implementation returns the empty map.
bindsVars :: (HasVars f v, Mapping m a) => f a :=> m (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
-- | left-biased union of two mappings.
(&) :: Mapping m k => m v -> m v -> m v
-- | This operator constructs a singleton mapping.
(|->) :: Mapping m k => k i -> v -> m v
-- | This is the empty mapping.
empty :: Mapping m k => m v
instance (Data.Comp.Multi.Variables.HasVars f v0, Data.Comp.Multi.Variables.HasVars g v0) => Data.Comp.Multi.Variables.HasVars (f Data.Comp.Multi.Ops.:+: g) v0
instance (GHC.Classes.Ord v, Data.Comp.Multi.Variables.HasVars f v, Data.Comp.Multi.HTraversable.HTraversable f) => Data.Comp.Multi.Variables.SubstVars v (Data.Comp.Multi.Term.Cxt h f a) (Data.Comp.Multi.Term.Cxt h f a)
instance (Data.Comp.Multi.Variables.SubstVars v t a, Data.Comp.Multi.HFunctor.HFunctor f) => Data.Comp.Multi.Variables.SubstVars v t (f a)
-- | This module provides a generic projection function pr for
-- arbitrary nested binary products.
module Data.Comp.Multi.Projection
-- | This function projects the component of type e out or the
-- compound value of type p.
pr :: (p :< q) => q a -> p a
-- | The constraint e :< p expresses that e is a
-- component of the type p. That is, p is formed by
-- binary products using the type e. The occurrence of
-- e must be unique. For example we have Int :<
-- (Bool,(Int,Bool)) but not Bool :< (Bool,(Int,Bool)).
type (:<) f g = Proj (ComprEmb (Elem f g)) f g
-- | 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
instance Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found 'Data.Comp.SubsumeCommon.Here) f f
instance Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Le p)) f (g Data.Comp.Ops.:*: g')
instance Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found p) f g => Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Ri p)) f (g' Data.Comp.Ops.:*: g)
instance (Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found p1) f1 g, Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found p2) f2 g) => Data.Comp.Multi.Projection.Proj ('Data.Comp.SubsumeCommon.Found ('Data.Comp.SubsumeCommon.Sum p1 p2)) (f1 Data.Comp.Ops.:*: f2) g
-- | This module defines the central notion of terms and its
-- generalisation to contexts.
module Data.Comp.Term
-- | This data type represents contexts over a signature. Contexts are
-- terms containing zero or more holes. The first type parameter is
-- supposed to be one of the phantom types Hole and NoHole.
-- The second parameter is the signature of the context. The third
-- parameter is the type of the holes.
data Cxt :: * -> (* -> *) -> * -> *
Term :: f (Cxt h f a) -> Cxt h f a
Hole :: a -> Cxt Hole f a
-- | Phantom type that signals that a Cxt might contain holes.
data Hole
-- | Phantom type that signals that a Cxt does not contain holes.
data NoHole
type Context = Cxt Hole
-- | A term is a context with no holes.
type Term f = Cxt NoHole f ()
-- | Polymorphic definition of a term. This formulation is more natural
-- than Term, it leads to impredicative types in some cases,
-- though.
type PTerm f = forall h a. Cxt h f a
type Const f = f ()
-- | This function unravels the given term at the topmost layer.
unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)
-- | Convert a functorial value into a context.
simpCxt :: Functor f => f a -> Context f a
-- | Cast a term over a signature to a context over the same signature.
toCxt :: Functor f => Term f -> Cxt h f a
-- | This function converts a constant to a term. This assumes that the
-- argument is indeed a constant, i.e. does not have a value for the
-- argument type of the functor f.
constTerm :: (Functor f) => Const f -> Term f
instance GHC.Base.Functor f => GHC.Base.Functor (Data.Comp.Term.Cxt h f)
instance GHC.Base.Functor f => GHC.Base.Applicative (Data.Comp.Term.Context f)
instance GHC.Base.Functor f => GHC.Base.Monad (Data.Comp.Term.Context f)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Data.Comp.Term.Cxt h f)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Data.Comp.Term.Cxt h f)
-- | 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 Data.Comp.Derive.Equality.EqF GHC.Base.Maybe
instance Data.Comp.Derive.Equality.EqF []
instance GHC.Classes.Eq a0 => Data.Comp.Derive.Equality.EqF ((,) a0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0) => Data.Comp.Derive.Equality.EqF ((,,) a0 b0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0) => Data.Comp.Derive.Equality.EqF ((,,,) a0 b0 c0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0) => Data.Comp.Derive.Equality.EqF ((,,,,) a0 b0 c0 d0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0, GHC.Classes.Eq e0) => Data.Comp.Derive.Equality.EqF ((,,,,,) a0 b0 c0 d0 e0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0, GHC.Classes.Eq e0, GHC.Classes.Eq f0) => Data.Comp.Derive.Equality.EqF ((,,,,,,) a0 b0 c0 d0 e0 f0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0, GHC.Classes.Eq e0, GHC.Classes.Eq f0, GHC.Classes.Eq g0) => Data.Comp.Derive.Equality.EqF ((,,,,,,,) a0 b0 c0 d0 e0 f0 g0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0, GHC.Classes.Eq e0, GHC.Classes.Eq f0, GHC.Classes.Eq g0, GHC.Classes.Eq h0) => Data.Comp.Derive.Equality.EqF ((,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0)
instance (GHC.Classes.Eq a0, GHC.Classes.Eq b0, GHC.Classes.Eq c0, GHC.Classes.Eq d0, GHC.Classes.Eq e0, GHC.Classes.Eq f0, GHC.Classes.Eq g0, GHC.Classes.Eq h0, GHC.Classes.Eq i0) => Data.Comp.Derive.Equality.EqF ((,,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0 i0)
instance (Data.Comp.Derive.Equality.EqF f, GHC.Classes.Eq a) => GHC.Classes.Eq (Data.Comp.Term.Cxt h f a)
instance Data.Comp.Derive.Equality.EqF f => Data.Comp.Derive.Equality.EqF (Data.Comp.Term.Cxt h f)
instance (Data.Comp.Derive.Equality.EqF f, Data.Comp.Derive.Equality.EqF g) => Data.Comp.Derive.Equality.EqF (f Data.Comp.Ops.:+: g)
-- | This module defines the notion of algebras and catamorphisms, and
-- their generalizations to e.g. monadic versions and other (co)recursion
-- schemes.
module Data.Comp.Algebra
-- | This type represents an algebra over a functor f and carrier
-- a.
type Alg f a = f a -> a
-- | Construct a catamorphism for contexts over f with holes of
-- type a, from the given algebra.
free :: (Functor f) => Alg f b -> (a -> b) -> Cxt h f a -> b
-- | Construct a catamorphism from the given algebra.
cata :: (Functor f) => Alg f a -> Term f -> a
-- | A generalisation of cata from terms over f to contexts
-- over f, where the holes have the type of the algebra carrier.
cata' :: (Functor f) => Alg f a -> Cxt h f a -> a
-- | This function applies a whole context into another context.
appCxt :: (Functor f) => Context f (Cxt h f a) -> Cxt h f a
-- | This type represents a monadic algebra. It is similar to Alg
-- but the return type is monadic.
type AlgM m f a = f a -> m a
-- | Convert a monadic algebra into an ordinary algebra with a monadic
-- carrier.
algM :: (Traversable f, Monad m) => AlgM m f a -> Alg f (m a)
-- | Construct a monadic catamorphism for contexts over f with
-- holes of type a, from the given monadic algebra.
freeM :: (Traversable f, Monad m) => AlgM m f b -> (a -> m b) -> Cxt h f a -> m b
-- | Construct a monadic catamorphism from the given monadic algebra.
cataM :: (Traversable f, Monad m) => AlgM m f a -> Term f -> m a
-- | A generalisation of cataM from terms over f to
-- contexts over f, where the holes have the type of the monadic
-- algebra carrier.
cataM' :: (Traversable f, Monad m) => AlgM m f a -> Cxt h f a -> m a
-- | This type represents a context function.
type CxtFun f g = forall a h. Cxt h f a -> Cxt h g a
-- | This type represents a signature function.
type SigFun f g = forall a. f a -> g a
-- | This type represents a term homomorphism.
type Hom f g = SigFun f (Context g)
-- | This function applies the given term homomorphism to a term/context.
appHom :: (Functor f, Functor g) => Hom f g -> CxtFun f g
-- | Apply a term homomorphism recursively to a term/context. This is a
-- top-down variant of appHom.
appHom' :: (Functor g) => Hom f g -> CxtFun f g
-- | Compose two term homomorphisms.
compHom :: (Functor g, Functor h) => Hom g h -> Hom f g -> Hom f h
-- | This function applies a signature function to the given context.
appSigFun :: (Functor f) => SigFun f g -> CxtFun f g
-- | This function applies a signature function to the given context. This
-- is a top-down variant of appSigFun.
appSigFun' :: (Functor g) => SigFun f g -> CxtFun f g
-- | This function composes two signature functions.
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
-- | This function composes a signature function with a term homomorphism.
compSigFunHom :: (Functor g) => SigFun g h -> Hom f g -> Hom f h
-- | This function composes a term homomorphism with a signature function.
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h
-- | This function composes an algebra with a signature function.
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a
-- | Lifts the given signature function to the canonical term homomorphism.
hom :: (Functor g) => SigFun f g -> Hom f g
-- | Compose an algebra with a term homomorphism to get a new algebra.
compAlg :: (Functor g) => Alg g a -> Hom f g -> Alg f a
-- | Compose a term homomorphism with a coalgebra to get a cv-coalgebra.
compCoalg :: Hom f g -> Coalg f a -> CVCoalg' g a
-- | Compose a term homomorphism with a cv-coalgebra to get a new
-- cv-coalgebra.
compCVCoalg :: (Functor f, Functor g) => Hom f g -> CVCoalg' f a -> CVCoalg' g a
-- | This type represents a monadic context function.
type CxtFunM m f g = forall a h. Cxt h f a -> m (Cxt h g a)
-- | This type represents a monadic signature function.
type SigFunM m f g = forall a. f a -> m (g a)
-- | This type represents a monadic term homomorphism.
type HomM m f g = SigFunM m f (Context g)
-- | This type represents a monadic signature function. It is similar to
-- SigFunM but has monadic values also in the domain.
type SigFunMD m f g = forall a. f (m a) -> m (g a)
-- | This type represents a monadic term homomorphism. It is similar to
-- HomM but has monadic values also in the domain.
type HomMD m f g = SigFunMD m f (Context g)
-- | Lift the given signature function to a monadic signature function.
-- Note that term homomorphisms are instances of signature functions.
-- Hence this function also applies to term homomorphisms.
sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g
-- | Lift the give monadic signature function to a monadic term
-- homomorphism.
hom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> HomM m f g
-- | Apply a monadic term homomorphism recursively to a term/context.
appHomM :: (Traversable f, Functor g, Monad m) => HomM m f g -> CxtFunM m f g
-- | Apply a monadic term homomorphism recursively to a term/context. This
-- a top-down variant of appHomM.
appHomM' :: (Traversable g, Monad m) => HomM m f g -> CxtFunM m f g
-- | Lift the given signature function to a monadic term homomorphism.
homM :: (Functor g, Monad m) => SigFunM m f g -> HomM m f g
-- | This function constructs the unique monadic homomorphism from the
-- initial term algebra to the given term algebra.
homMD :: (Traversable f, Functor g, Monad m) => HomMD m f g -> CxtFunM m f g
-- | This function applies a monadic signature function to the given
-- context.
appSigFunM :: (Traversable f, Monad m) => SigFunM m f g -> CxtFunM m f g
-- | This function applies a monadic signature function to the given
-- context. This is a top-down variant of appSigFunM.
appSigFunM' :: (Traversable g, Monad m) => SigFunM m f g -> CxtFunM m f g
-- | This function applies a signature function to the given context.
appSigFunMD :: (Traversable f, Functor g, Monad m) => SigFunMD m f g -> CxtFunM m f g
-- | Compose two monadic term homomorphisms.
compHomM :: (Traversable g, Functor h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h
-- | This function composes two monadic signature functions.
compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunHomM :: (Traversable g, Functor h, Monad m) => SigFunM m g h -> HomM m f g -> HomM m f h
-- | This function composes two monadic signature functions.
compHomSigFunM :: (Monad m) => HomM m g h -> SigFunM m f g -> HomM m f h
-- | This function composes two monadic signature functions.
compAlgSigFunM :: (Monad m) => AlgM m g a -> SigFunM m f g -> AlgM m f a
-- | Compose a monadic algebra with a monadic term homomorphism to get a
-- new monadic algebra.
compAlgM :: (Traversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a
-- | Compose a monadic algebra with a term homomorphism to get a new
-- monadic algebra.
compAlgM' :: (Traversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
-- | This type represents a coalgebra over a functor f and carrier
-- a.
type Coalg f a = a -> f a
-- | Construct an anamorphism from the given coalgebra.
ana :: Functor f => Coalg f a -> a -> Term f
-- | Shortcut fusion variant of ana.
ana' :: Functor f => Coalg f a -> a -> Term f
-- | This type represents a monadic coalgebra over a functor f and
-- carrier a.
type CoalgM m f a = a -> m (f a)
-- | Construct a monadic anamorphism from the given monadic coalgebra.
anaM :: (Traversable f, Monad m) => CoalgM m f a -> a -> m (Term f)
-- | This type represents an r-algebra over a functor f and
-- carrier a.
type RAlg f a = f (Term f, a) -> a
-- | Construct a paramorphism from the given r-algebra.
para :: (Functor f) => RAlg f a -> Term f -> a
-- | This type represents a monadic r-algebra over a functor f and
-- carrier a.
type RAlgM m f a = f (Term f, a) -> m a
-- | Construct a monadic paramorphism from the given monadic r-algebra.
paraM :: (Traversable f, Monad m) => RAlgM m f a -> Term f -> m a
-- | This type represents an r-coalgebra over a functor f and
-- carrier a.
type RCoalg f a = a -> f (Either (Term f) a)
-- | Construct an apomorphism from the given r-coalgebra.
apo :: (Functor f) => RCoalg f a -> a -> Term f
-- | This type represents a monadic r-coalgebra over a functor f
-- and carrier a.
type RCoalgM m f a = a -> m (f (Either (Term f) a))
-- | Construct a monadic apomorphism from the given monadic r-coalgebra.
apoM :: (Traversable f, Monad m) => RCoalgM m f a -> a -> m (Term f)
-- | This type represents a cv-algebra over a functor f and
-- carrier a.
type CVAlg f a f' = f (Term f') -> a
-- | Construct a histomorphism from the given cv-algebra.
histo :: (Functor f, DistAnn f a f') => CVAlg f a f' -> Term f -> a
-- | This type represents a monadic cv-algebra over a functor f
-- and carrier a.
type CVAlgM m f a f' = f (Term f') -> m a
-- | Construct a monadic histomorphism from the given monadic cv-algebra.
histoM :: (Traversable f, Monad m, DistAnn f a f') => CVAlgM m f a f' -> Term f -> m a
-- | This type represents a cv-coalgebra over a functor f and
-- carrier a.
type CVCoalg f a = a -> f (Context f a)
-- | Construct a futumorphism from the given cv-coalgebra.
futu :: Functor f => CVCoalg f a -> a -> Term f
-- | This type represents a generalised cv-coalgebra over a functor
-- f and carrier a.
type CVCoalg' f a = a -> Context f a
-- | Construct a futumorphism from the given generalised cv-coalgebra.
futu' :: Functor f => CVCoalg' f a -> a -> Term f
-- | This type represents a monadic cv-coalgebra over a functor f
-- and carrier a.
type CVCoalgM m f a = a -> m (f (Context f a))
-- | Construct a monadic futumorphism from the given monadic cv-coalgebra.
futuM :: (Traversable f, Monad m) => CVCoalgM m f a -> a -> m (Term f)
-- | This module defines 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
-- | Inject an annotation over a signature.
injectA :: DistAnn s p s' => p -> s a -> s' a
-- | Project an annotation from a signature.
projectA :: DistAnn s p s' => s' a -> (s a, p)
class RemA s s' | s -> s'
-- | Remove annotations from a signature.
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 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 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 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
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 (GHC.Show.Show (f a), GHC.Show.Show (g a)) => GHC.Show.Show ((Data.Comp.Ops.:+:) f g a)
instance (GHC.Classes.Ord (f a), GHC.Classes.Ord (g a)) => GHC.Classes.Ord ((Data.Comp.Ops.:+:) f g a)
instance (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Data.Comp.Ops.:+:) f g 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 a list of all subterms of the given term. This
-- function is similar to Uniplate's universe function.
subterms :: Foldable f => Term f -> [Term f]
-- | This function returns a list of all subterms of the given term that
-- are constructed from a particular functor.
subterms' :: (Foldable f, g :<: f) => Term f -> [g (Term f)]
-- | This function transforms every subterm according to the given function
-- in a bottom-up manner. This function is similar to Uniplate's
-- transform function.
transform :: (Functor f) => (Term f -> Term f) -> Term f -> Term f
transform' :: (Functor f) => (Term f -> Maybe (Term f)) -> Term f -> Term f
-- | Monadic version of transform.
transformM :: (Traversable f, Monad m) => (Term f -> m (Term f)) -> Term f -> m (Term f)
query :: Foldable f => (Term f -> r) -> (r -> r -> r) -> Term f -> r
gsize :: Foldable f => Term f -> Int
-- | This function computes the generic size of the given term, i.e. the
-- its number of subterm occurrences.
size :: Foldable f => Cxt h f a -> Int
-- | This function computes the generic height of the given term.
height :: Foldable f => Cxt h f a -> Int
-- | This modules defines terms & contexts with thunks, with deferred
-- monadic computations.
module Data.Comp.Thunk
-- | This type represents terms with thunks.
type TermT m f = Term (m :+: f)
-- | This type represents contexts with thunks.
type CxtT m h f a = Cxt h (m :+: f) a
-- | This function turns a monadic computation into a thunk.
thunk :: m (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.
--
-- 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
--
--
-- Foldable instances are expected to satisfy the following
-- laws:
--
--
-- foldr f z t = appEndo (foldMap (Endo . f) t ) z
--
--
--
-- foldl f z t = appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z
--
--
--
-- fold = foldMap id
--
--
-- sum, product, maximum, and minimum
-- should all be essentially equivalent to foldMap forms, such
-- as
--
--
-- sum = getSum . foldMap Sum
--
--
-- but may be less defined.
--
-- If the type is also a Functor instance, it should satisfy
--
--
-- foldMap f = fold . fmap f
--
--
-- which implies that
--
--
-- foldMap f . fmap g = foldMap (f . g)
--
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.
--
-- 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
-- | A generator for values of the given type.
arbitrary :: Arbitrary a => Gen a
-- | Produces a (possibly) empty list of all the possible immediate shrinks
-- of the given value. The default implementation returns the empty list,
-- so will not try to shrink the value.
--
-- Most implementations of shrink should try at least three
-- things:
--
--
-- - Shrink a term to any of its immediate subterms.
-- - Recursively apply shrink to all immediate subterms.
-- - Type-specific shrinkings such as replacing a constructor by a
-- simpler constructor.
--
--
-- For example, suppose we have the following implementation of binary
-- trees:
--
--
-- data Tree a = Nil | Branch a (Tree a) (Tree a)
--
--
-- We can then define shrink as follows:
--
--
-- shrink Nil = []
-- shrink (Branch x l r) =
-- -- shrink Branch to Nil
-- [Nil] ++
-- -- shrink to subterms
-- [l, r] ++
-- -- recursively shrink subterms
-- [Branch x' l' r' | (x', l', r') <- shrink (x, l, r)]
--
--
-- There are a couple of subtleties here:
--
--
-- - QuickCheck tries the shrinking candidates in the order they appear
-- in the list, so we put more aggressive shrinking steps (such as
-- replacing the whole tree by Nil) before smaller ones (such as
-- recursively shrinking the subtrees).
-- - It is tempting to write the last line as [Branch x' l' r' | x'
-- <- shrink x, l' <- shrink l, r' <- shrink r] but this is
-- the wrong thing! It will force QuickCheck to shrink x,
-- l and r in tandem, and shrinking will stop once
-- one of the three is fully shrunk.
--
--
-- There is a fair bit of boilerplate in the code above. We can avoid it
-- with the help of some generic functions; note that these only work on
-- GHC 7.2 and above. The function genericShrink tries shrinking a
-- term to all of its subterms and, failing that, recursively shrinks the
-- subterms. Using it, we can define shrink as:
--
--
-- shrink x = shrinkToNil x ++ genericShrink x
-- where
-- shrinkToNil Nil = []
-- shrinkToNil (Branch _ l r) = [Nil]
--
--
-- genericShrink is a combination of subterms, which
-- shrinks a term to any of its subterms, and recursivelyShrink,
-- which shrinks all subterms of a term. These may be useful if you need
-- a bit more control over shrinking than genericShrink gives you.
--
-- A final gotcha: we cannot define shrink as simply
-- shrink x = Nil:genericShrink x as this shrinks
-- Nil to Nil, and shrinking will go into an infinite
-- loop.
--
-- If all this leaves you bewildered, you might try shrink =
-- genericShrink to begin with, after deriving
-- Generic for your type. However, if your data type has any
-- special invariants, you will need to check that genericShrink
-- can't break those invariants.
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 should reduce its argument to normal form (that is, fully
-- evaluate all sub-components), and then return '()'.
--
--
--
-- Starting with GHC 7.2, you can automatically derive instances for
-- types possessing a Generic instance.
--
--
-- {-# LANGUAGE DeriveGeneric #-}
--
-- import GHC.Generics (Generic)
-- import Control.DeepSeq
--
-- data Foo a = Foo a String
-- deriving (Eq, Generic)
--
-- instance NFData a => NFData (Foo a)
--
-- data Colour = Red | Green | Blue
-- deriving Generic
--
-- instance NFData Colour
--
--
-- Starting with GHC 7.10, the example above can be written more
-- concisely by enabling the new DeriveAnyClass extension:
--
--
-- {-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
--
-- import GHC.Generics (Generic)
-- import Control.DeepSeq
--
-- data Foo a = Foo a String
-- deriving (Eq, Generic, NFData)
--
-- data Colour = Red | Green | Blue
-- deriving (Generic, NFData)
--
--
-- Compatibility with previous deepseq versions
--
-- Prior to version 1.4.0.0, the default implementation of the rnf
-- method was defined as
--
--
-- rnf a = seq a ()
--
--
-- However, starting with deepseq-1.4.0.0, the default
-- implementation is based on DefaultSignatures allowing for
-- more accurate auto-derived NFData instances. If you need the
-- previously used exact default rnf method implementation
-- semantics, use
--
--
-- instance NFData Colour where rnf x = seq x ()
--
--
-- or alternatively
--
--
-- {-# LANGUAGE BangPatterns #-}
-- instance NFData Colour where rnf !_ = ()
--
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 Data.Comp.Derive.Ordering.OrdF GHC.Base.Maybe
instance Data.Comp.Derive.Ordering.OrdF []
instance GHC.Classes.Ord a0 => Data.Comp.Derive.Ordering.OrdF ((,) a0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0) => Data.Comp.Derive.Ordering.OrdF ((,,) a0 b0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0) => Data.Comp.Derive.Ordering.OrdF ((,,,) a0 b0 c0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0) => Data.Comp.Derive.Ordering.OrdF ((,,,,) a0 b0 c0 d0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0, GHC.Classes.Ord e0) => Data.Comp.Derive.Ordering.OrdF ((,,,,,) a0 b0 c0 d0 e0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0, GHC.Classes.Ord e0, GHC.Classes.Ord f0) => Data.Comp.Derive.Ordering.OrdF ((,,,,,,) a0 b0 c0 d0 e0 f0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0, GHC.Classes.Ord e0, GHC.Classes.Ord f0, GHC.Classes.Ord g0) => Data.Comp.Derive.Ordering.OrdF ((,,,,,,,) a0 b0 c0 d0 e0 f0 g0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0, GHC.Classes.Ord e0, GHC.Classes.Ord f0, GHC.Classes.Ord g0, GHC.Classes.Ord h0) => Data.Comp.Derive.Ordering.OrdF ((,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0)
instance (GHC.Classes.Ord a0, GHC.Classes.Ord b0, GHC.Classes.Ord c0, GHC.Classes.Ord d0, GHC.Classes.Ord e0, GHC.Classes.Ord f0, GHC.Classes.Ord g0, GHC.Classes.Ord h0, GHC.Classes.Ord i0) => Data.Comp.Derive.Ordering.OrdF ((,,,,,,,,,) a0 b0 c0 d0 e0 f0 g0 h0 i0)
instance (Data.Comp.Derive.Ordering.OrdF f, GHC.Classes.Ord a) => GHC.Classes.Ord (Data.Comp.Term.Cxt h f a)
instance Data.Comp.Derive.Ordering.OrdF f => Data.Comp.Derive.Ordering.OrdF (Data.Comp.Term.Cxt h f)
instance (Data.Comp.Derive.Ordering.OrdF f, Data.Comp.Derive.Ordering.OrdF g) => Data.Comp.Derive.Ordering.OrdF (f Data.Comp.Ops.:+: g)
-- | 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 Data.Comp.Derive.DeepSeq.NFDataF GHC.Base.Maybe
instance Data.Comp.Derive.DeepSeq.NFDataF []
instance Control.DeepSeq.NFData a0 => Data.Comp.Derive.DeepSeq.NFDataF ((,) a0)
instance (Data.Comp.Derive.DeepSeq.NFDataF f, Data.Comp.Derive.DeepSeq.NFDataF g) => Data.Comp.Derive.DeepSeq.NFDataF (f Data.Comp.Ops.:+: g)
instance (Data.Comp.Derive.DeepSeq.NFDataF f, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Data.Comp.Term.Cxt h f a)
instance (Data.Comp.Derive.DeepSeq.NFDataF f, Control.DeepSeq.NFData a) => Data.Comp.Derive.DeepSeq.NFDataF (f Data.Comp.Ops.:&: 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 Data.Comp.Derive.Arbitrary.ArbitraryF GHC.Base.Maybe
instance Data.Comp.Derive.Arbitrary.ArbitraryF []
instance Test.QuickCheck.Arbitrary.Arbitrary b0 => Data.Comp.Derive.Arbitrary.ArbitraryF ((,) b0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,) b0 c0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,) b0 c0 d0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,) b0 c0 d0 e0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0, Test.QuickCheck.Arbitrary.Arbitrary f0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,,) b0 c0 d0 e0 f0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0, Test.QuickCheck.Arbitrary.Arbitrary f0, Test.QuickCheck.Arbitrary.Arbitrary g0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,,,) b0 c0 d0 e0 f0 g0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0, Test.QuickCheck.Arbitrary.Arbitrary f0, Test.QuickCheck.Arbitrary.Arbitrary g0, Test.QuickCheck.Arbitrary.Arbitrary h0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,,,,) b0 c0 d0 e0 f0 g0 h0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0, Test.QuickCheck.Arbitrary.Arbitrary f0, Test.QuickCheck.Arbitrary.Arbitrary g0, Test.QuickCheck.Arbitrary.Arbitrary h0, Test.QuickCheck.Arbitrary.Arbitrary i0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,,,,,) b0 c0 d0 e0 f0 g0 h0 i0)
instance (Test.QuickCheck.Arbitrary.Arbitrary b0, Test.QuickCheck.Arbitrary.Arbitrary c0, Test.QuickCheck.Arbitrary.Arbitrary d0, Test.QuickCheck.Arbitrary.Arbitrary e0, Test.QuickCheck.Arbitrary.Arbitrary f0, Test.QuickCheck.Arbitrary.Arbitrary g0, Test.QuickCheck.Arbitrary.Arbitrary h0, Test.QuickCheck.Arbitrary.Arbitrary i0, Test.QuickCheck.Arbitrary.Arbitrary j0) => Data.Comp.Derive.Arbitrary.ArbitraryF ((,,,,,,,,,) b0 c0 d0 e0 f0 g0 h0 i0 j0)
instance Data.Comp.Derive.Arbitrary.ArbitraryF f => Test.QuickCheck.Arbitrary.Arbitrary (Data.Comp.Term.Term f)
instance (Data.Comp.Derive.Arbitrary.ArbitraryF f, Test.QuickCheck.Arbitrary.Arbitrary p) => Data.Comp.Derive.Arbitrary.ArbitraryF (f Data.Comp.Ops.:&: p)
instance Data.Comp.Derive.Arbitrary.ArbitraryF f => Data.Comp.Derive.Arbitrary.ArbitraryF (Data.Comp.Term.Context f)
instance (Data.Comp.Derive.Arbitrary.ArbitraryF f, Test.QuickCheck.Arbitrary.Arbitrary a) => Test.QuickCheck.Arbitrary.Arbitrary (Data.Comp.Term.Context f a)
instance (Data.Comp.Derive.Arbitrary.ArbitraryF f, Data.Comp.Derive.Arbitrary.ArbitraryF g) => Data.Comp.Derive.Arbitrary.ArbitraryF (f Data.Comp.Ops.:+: g)
-- | 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 (Data.Comp.Derive.Show.ShowConstr f, Data.Comp.Derive.Show.ShowConstr g) => Data.Comp.Derive.Show.ShowConstr (f Data.Comp.Ops.:+: g)
instance Data.Comp.Derive.Show.ShowF GHC.Base.Maybe
instance Data.Comp.Derive.Show.ShowF []
instance GHC.Show.Show a0 => Data.Comp.Derive.Show.ShowF ((,) a0)
instance (Data.Comp.Derive.Show.ShowConstr f, GHC.Show.Show p) => Data.Comp.Derive.Show.ShowConstr (f Data.Comp.Ops.:&: p)
instance (Data.Comp.Derive.Show.ShowF f, Data.Comp.Derive.Show.ShowF g) => Data.Comp.Derive.Show.ShowF (f Data.Comp.Ops.:+: g)
instance (GHC.Base.Functor f, Data.Comp.Derive.Show.ShowF f) => Data.Comp.Derive.Show.ShowF (Data.Comp.Term.Cxt h f)
instance (GHC.Base.Functor f, Data.Comp.Derive.Show.ShowF f, GHC.Show.Show a) => GHC.Show.Show (Data.Comp.Term.Cxt h f a)
instance (Data.Comp.Derive.Show.ShowF f, GHC.Show.Show p) => Data.Comp.Derive.Show.ShowF (f Data.Comp.Ops.:&: p)
-- | 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
-- | Indicates whether the f constructor is a variable. The
-- default implementation returns Nothing.
isVar :: HasVars f v => f a -> Maybe v
-- | Indicates the set of variables bound by the f constructor for
-- each argument of the constructor. For example for a non-recursive let
-- binding:
--
--
-- data Let e = Let Var e e
-- instance HasVars Let Var where
-- bindsVars (Let v x y) = y |-> Set.singleton v
--
--
-- If, instead, the let binding is recursive, the methods has to be
-- implemented like this:
--
--
-- bindsVars (Let v x y) = x |-> Set.singleton v &
-- y |-> Set.singleton v
--
--
-- This indicates that the scope of the bound variable also extends to
-- the right-hand side of the variable binding.
--
-- The default implementation returns the empty map.
bindsVars :: (HasVars f v, Mapping m a) => f a -> m (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)
-- | left-biased union of two mappings.
(&) :: Mapping m k => m v -> m v -> m v
-- | This operator constructs a singleton mapping.
(|->) :: Mapping m k => k -> v -> m v
-- | This is the empty mapping.
empty :: Mapping m k => m v
instance (Data.Comp.Variables.HasVars f v0, Data.Comp.Variables.HasVars g v0) => Data.Comp.Variables.HasVars (f Data.Comp.Ops.:+: g) v0
instance Data.Comp.Variables.HasVars f v => Data.Comp.Variables.HasVars (f Data.Comp.Ops.:&: a) v
instance (GHC.Classes.Ord v, Data.Comp.Variables.HasVars f v, Data.Traversable.Traversable f) => Data.Comp.Variables.SubstVars v (Data.Comp.Term.Cxt h f a) (Data.Comp.Term.Cxt h f a)
instance (Data.Comp.Variables.SubstVars v t a, GHC.Base.Functor f) => Data.Comp.Variables.SubstVars v t (f a)
-- | 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 }
-- | This function decomposes a functorial value.
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 (Data.Comp.Variables.HasVars f v, GHC.Base.Functor f, Data.Foldable.Foldable f) => Data.Comp.Decompose.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 ()
-- | 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 (Data.Comp.Render.Render f, Data.Comp.Render.Render g) => Data.Comp.Render.Render (f Data.Comp.Ops.:+: 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 (Data.Comp.Desugar.Desugar f h, Data.Comp.Desugar.Desugar g h) => Data.Comp.Desugar.Desugar (f Data.Comp.Ops.:+: g) h
instance (GHC.Base.Functor f, GHC.Base.Functor g, f Data.Comp.Ops.:<: g) => Data.Comp.Desugar.Desugar f g