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


-- | Tree automata on Compositional Data Types
--   
--   This library extends the <tt>compdata</tt> package with advanced
--   recursion schemes derived from tree automata. These recursion schemes
--   allow for a higher degree of modularity and make it possible to apply
--   fusion. See <i>Modular Tree Automata</i> (Mathematics of Program
--   Construction, 263-299, 2012,
--   <a>http://dx.doi.org/10.1007/978-3-642-31113-0_14</a>) and
--   <i>Programming Macro Tree Transducers</i> (Workshop on Generic
--   Programming, 61-72, 2013,
--   <a>http://dx.doi.org/10.1145/2502488.2502489</a>).
@package compdata-automata
@version 0.9.2


-- | This module defines stateful term homomorphisms. This (slightly
--   oxymoronic) notion extends per se stateless term homomorphisms with a
--   state that is maintained separately by a bottom-up or top-down state
--   transformation. Additionally, this module also provides combinators to
--   run state transformations themselves.
--   
--   Like regular term homomorphisms also stateful homomorphisms (as well
--   as transducers) can be lifted to annotated signatures (cf.
--   <a>Data.Comp.Annotation</a>).
--   
--   The recursion schemes provided in this module are derived from tree
--   automata. They allow for a higher degree of modularity and make it
--   possible to apply fusion. The implementation is based on the paper
--   <i>Modular Tree Automata</i> (Mathematics of Program Construction,
--   263-299, 2012, <a>http://dx.doi.org/10.1007/978-3-642-31113-0_14</a>).
module Data.Comp.Automata

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

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

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

-- | This function turns a stateful homomorphism with a fully polymorphic
--   state type into a (stateless) homomorphism.
pureHom :: (forall q. QHom f q g) -> Hom f g

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

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

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

-- | This function constructs a DTT from a given stateful term--
--   homomorphism with the state propagated by the given DTA.
downTrans :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> DownTrans f q g

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

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

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

-- | This is a variant of the <a>UpTrans</a> type that makes it easier to
--   define UTTs as it avoids the explicit use of <a>Hole</a> to inject
--   placeholders into the result.
type UpTrans' f q g = forall a. f (q, Context g a) -> (q, Context g a)

-- | This function turns a UTT defined using the type <a>UpTrans'</a> in to
--   the canonical form of type <a>UpTrans</a>.
mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g

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

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

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

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

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

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

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

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

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

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

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

-- | This type represents transition functions of generalised deterministic
--   bottom-up tree acceptors (GUTAs) which have access to an extended
--   state space.
type DUpState f p q = (q :< p) => DUpState' f p q

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

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

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

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

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

-- | This is a variant of the <a>DownTrans</a> type that makes it easier to
--   define DTTs as it avoids the explicit use of <a>Hole</a> to inject
--   placeholders into the result.
type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a

-- | This function turns a DTT defined using the type <a>DownTrans'</a> in
--   to the canonical form of type <a>DownTrans</a>.
mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g

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

-- | This function composes two DTTs. (see W.C. Rounds /Mappings and
--   grammars on trees/, Theorem 2.)
compDownTrans :: (Functor f, Functor g, Functor h) => DownTrans g p h -> DownTrans f q g -> DownTrans f (q, p) h

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

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

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

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

-- | This type represents transition functions of total, deterministic
--   top-down tree acceptors (DTAs).
type DownState f q = forall m a. Mapping m a => (q, f a) -> m q

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

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

-- | This type represents transition functions of generalised deterministic
--   top-down tree acceptors (GDTAs) which have access
type DDownState f p q = (q :< p) => DDownState' f p q

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

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

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

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

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

-- | left-biased union of two mappings.
(&) :: Mapping m k => m v -> m v -> m v
infixr 0 &

-- | This operator constructs a singleton mapping.
(|->) :: Mapping m k => k -> v -> m v
infix 1 |->

-- | This is the empty mapping.
empty :: Mapping m k => m v

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

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

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

-- | This function adds unique annotations to a term/context. Each node in
--   the term/context is annotated with its path from the root, which is
--   represented as an integer list. It is implemented as a DTT.
pathAnn :: forall g. (Traversable g) => CxtFun g (g :&: [Int])


-- | This module defines macro tree transducers (MTTs). It provides
--   functions to run MTTs and to compose them with top down tree
--   transducers. It also defines MTTs with regular look-ahead which
--   combines MTTs with bottom-up tree acceptors.
module Data.Comp.MacroAutomata

-- | This type represents total deterministic macro tree transducers
--   (MTTs).
type MacroTrans f q g = forall a. q a -> f (q (Context g a) -> a) -> Context g a

-- | This is a variant of the type <a>MacroTrans</a> that makes it easier
--   to define MTTs as it avoids the explicit use of <a>Hole</a> when using
--   placeholders in the result.
type MacroTrans' f q g = forall a. q (Context g a) -> f (q (Context g a) -> Context g a) -> Context g a

-- | This function turns an MTT defined using the more convenient type
--   <a>MacroTrans'</a> into its canonical form of type <a>MacroTrans</a>.
mkMacroTrans :: (Functor f, Functor q) => MacroTrans' f q g -> MacroTrans f q g

-- | This function defines the semantics of MTTs. It applies a given MTT to
--   an input with and an initial state.
runMacroTrans :: (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a

-- | This function composes a DTT followed by an MTT. The resulting MTT's
--   semantics is equivalent to the function composition of the semantics
--   of the original MTT and DTT.
compMacroDown :: (Functor f, Functor g, Functor h, Functor p) => MacroTrans g p h -> DownTrans f q g -> MacroTrans f (p :&: q) h

-- | This function composes an MTT followed by a DTT. The resulting MTT's
--   semantics is equivalent to first running the original MTT and then the
--   DTT.
compDownMacro :: forall f g h q p. (Functor f, Functor g, Functor h, Functor q) => DownTrans g p h -> MacroTrans f q g -> MacroTrans f (q :^: p) h

-- | This type is an instantiation of the <a>MacroTrans</a> type to a state
--   space with only a single state with a single accumulation parameter
--   (i.e. the state space is the identity functor).
type MacroTransId f g = forall a. a -> f (Context g a -> a) -> Context g a

-- | This type is a variant of the <a>MacroTransId</a> which is more
--   convenient to work with as it avoids the explicit use of <a>Hole</a>
--   to embed placeholders into the result.
type MacroTransId' f g = forall a. Context g a -> f (Context g a -> Context g a) -> Context g a

-- | This function transforms an MTT of type |MacroTransId| into the
--   canonical type such that it can be run.
fromMacroTransId :: Functor f => MacroTransId f g -> MacroTrans f I g

-- | This function transforms an MTT of type |MacroTransId'| into the
--   canonical type such that it can be run.
fromMacroTransId' :: Functor f => MacroTransId' f g -> MacroTrans f I g

-- | This type represents MTTs with regular look-ahead, i.e. MTTs that have
--   access to information that is generated by a separate UTA.
type MacroTransLA f q p g = forall a. q a -> p -> f (q (Context g a) -> a, p) -> Context g a

-- | This type is a more convenient variant of <a>MacroTransLA</a> with
--   which one can avoid using <a>Hole</a> explicitly when injecting
--   placeholders in the result.
type MacroTransLA' f q p g = forall a. q (Context g a) -> p -> f (q (Context g a) -> Context g a, p) -> Context g a

-- | This function turns an MTT with regular look-ahead defined using the
--   more convenient type |MacroTransLA'| into its canonical form of type
--   |MacroTransLA|.
mkMacroTransLA :: (Functor q, Functor f) => MacroTransLA' f q p g -> MacroTransLA f q p g

-- | This function defines the semantics of MTTs with regular look-ahead.
--   It applies a given MTT with regular look-ahead (including an
--   accompanying bottom-up state transition function) to an input with and
--   an initial state.
runMacroTransLA :: forall g f q p. (Functor g, Functor f, Functor q) => UpState f p -> MacroTransLA f q p g -> q (Term g) -> Term f -> Term g

-- | This function composes an MTT with regular look-ahead followed by a
--   DTT.
compDownMacroLA :: forall f g h q1 q2 p. (Functor f, Functor g, Functor h, Functor q1) => DownTrans g q2 h -> MacroTransLA f q1 p g -> MacroTransLA f (q1 :^: q2) p h

-- | This type constructor is used to define the state space of an MTT that
--   is obtained by composing an MTT followed by a DTT.
data ( q (:^:) p ) a
(:^:) :: q (p -> a) -> p -> (:^:) q p a

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

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

-- | Lift a macro tree transducer with regular look-ahead over signatures
--   <tt>f</tt> and <tt>g</tt> to a macro tree transducer with regular
--   look-ahead over the same signatures, but extended with annotations.
propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) => MacroTransLA f q p g -> MacroTransLA f' q p g'
instance GHC.Base.Functor q => GHC.Base.Functor (q Data.Comp.MacroAutomata.:^: p)