Data.Comp.Automata

This module defines stateful term homomorphisms. This (slightly oxymoronic) notion extends per se stateless term homomorphisms with a state that is maintained separately by a bottom-up or top-down state transformation. Additionally, this module also provides combinators to run state transformations themselves.

Like regular term homomorphisms also stateful homomorphisms (as well as transducers) can be lifted to annotated signatures (cf. Data.Comp.Annotation).

The recursion schemes provided in this module are derived from tree automata. They allow for a higher degree of modularity and make it possible to apply fusion. The implementation is based on the paper Modular Tree Automata (Mathematics of Program Construction, 263-299, 2012, http://dx.doi.org/10.1007/978-3-642-31113-0_14).

Stateful Term Homomorphisms

type QHom f q g = forall a. (?below :: a -> q, ?above :: q) => f a -> Context g a

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

below :: (?below :: a -> q, p :< q) => a -> p

This function provides access to components of the states from "below".

above :: (?above :: q, p :< q) => p

This function provides access to components of the state from "above"

pureHom :: (forall q. QHom f q g) -> Hom f g

This function turns a stateful homomorphism with a fully polymorphic state type into a (stateless) homomorphism.

Bottom-Up State Propagation

upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g

This function constructs a UTT from a given stateful term homomorphism with the state propagated by the given UTA.

runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g

This function applies a given stateful term homomorphism with a state space propagated by the given UTA to a term.

runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q, Term g)

This is a variant of runUpHom that also returns the final state of the run.

Top-Down State Propagation

downTrans :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> DownTrans f q g

This function constructs a DTT from a given stateful term-- homomorphism with the state propagated by the given DTA.

runDownHom :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> q -> Term f -> Term g

This function applies a given stateful term homomorphism with a state space propagated by the given DTA to a term.

Bidirectional State Propagation

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 combinator runs a stateful term homomorphisms with a state space produced both on a bottom-up and a top-down state transformation.

Deterministic Bottom-Up Tree Transducers

type UpTrans f q g = forall a. f (q, a) -> (q, Context g a)

This type represents transition functions of total, deterministic bottom-up tree transducers (UTTs).

type UpTrans' f q g = forall a. f (q, Context g a) -> (q, Context g a)

This is a variant of the UpTrans type that makes it easier to define UTTs as it avoids the explicit use of Hole to inject placeholders into the result.

mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g

This function turns a UTT defined using the type UpTrans' in to the canonical form of type UpTrans.

runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g

This function runs the given UTT on the given term.

compUpTrans :: (Functor f, Functor g, Functor h) => UpTrans g p h -> UpTrans f q g -> UpTrans f (q, p) h

This function composes two UTTs. (see TATA, Theorem 6.4.5)

compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h

This combinator composes a homomorphism followed by a UTT.

compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h

This combinator composes a UTT followed by a homomorphism.

compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h

This combinator composes a signature function followed by a UTT.

compSigUpTrans :: Functor g => SigFun g h -> UpTrans f q g -> UpTrans f q h

This combinator composes a UTT followed by a signature function.

compAlgUpTrans :: Functor g => Alg g a -> UpTrans f q g -> Alg f (q, a)

This function composes a UTT with an algebra.

Deterministic Bottom-Up Tree State Transformations

Monolithic State

type UpState f q = Alg f q

This type represents transition functions of total, deterministic bottom-up tree acceptors (UTAs).

tagUpState :: Functor f => (q -> p) -> (p -> q) -> UpState f q -> UpState f p

Changes the state space of the UTA using the given isomorphism.

runUpState :: Functor f => UpState f q -> Term f -> q

This combinator runs the given UTA on a term returning the final state of the run.

prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p, q)

This function combines the product UTA of the two given UTAs.

Modular State

type DUpState f p q = q :< p => DUpState' f p q

This type represents transition functions of generalised deterministic bottom-up tree acceptors (GUTAs) which have access to an extended state space.

dUpState :: Functor f => UpState f q -> DUpState f p q

This combinator turns an arbitrary UTA into a GUTA.

upState :: DUpState f q q -> UpState f q

This combinator turns a GUTA with the smallest possible state space into a UTA.

runDUpState :: Functor f => DUpState f q q -> Term f -> q

This combinator runs a GUTA on a term.

prodDUpState :: (p :< c, q :< c) => DUpState f c p -> DUpState f c q -> DUpState f c (p, q)

This combinator constructs the product of two GUTA.

(|*|) :: (p :< c, q :< c) => DUpState f c p -> DUpState f c q -> DUpState f c (p, q)

Deterministic Top-Down Tree Transducers

type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a

This type represents transition functions of total deterministic top-down tree transducers (DTTs).

type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a

This is a variant of the DownTrans type that makes it easier to define DTTs as it avoids the explicit use of Hole to inject placeholders into the result.

mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g

This function turns a DTT defined using the type DownTrans' in to the canonical form of type DownTrans.

runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a

Thsis function runs the given DTT on the given tree.

compDownTrans :: (Functor f, Functor g, Functor h) => DownTrans g p h -> DownTrans f q g -> DownTrans f (q, p) h

This function composes two DTTs. (see W.C. Rounds /Mappings and grammars on trees/, Theorem 2.)

compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h

This function composes a DTT after a function.

compSigDownTrans :: Functor g => SigFun g h -> DownTrans f q g -> DownTrans f q h

This function composes a signature function after a DTT.

compDownTransHom :: (Functor g, Functor h) => DownTrans g q h -> Hom f g -> DownTrans f q h

This function composes a DTT after a homomorphism.

compHomDownTrans :: (Functor g, Functor h) => Hom g h -> DownTrans f q g -> DownTrans f q h

This function composes a homomorphism after a DTT.

Deterministic Top-Down Tree State Transformations

Monolithic State

type DownState f q = forall m a. Mapping m a => (q, f a) -> m q

This type represents transition functions of total, deterministic top-down tree acceptors (DTAs).

tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p

Changes the state space of the DTA using the given isomorphism.

prodDownState :: DownState f p -> DownState f q -> DownState f (p, q)

This function constructs the product DTA of the given two DTAs.

Modular State

type DDownState f p q = q :< p => DDownState' f p q

This type represents transition functions of generalised deterministic top-down tree acceptors (GDTAs) which have access

dDownState :: DownState f q -> DDownState f p q

This combinator turns an arbitrary DTA into a GDTA.

downState :: DDownState f q q -> DownState f q

This combinator turns a GDTA with the smallest possible state space into a DTA.

prodDDownState :: (p :< c, q :< c) => DDownState f c p -> DDownState f c q -> DDownState f c (p, q)

This combinator constructs the product of two dependant top-down state transformations.

(>*<) :: (p :< c, q :< c, Functor f) => DDownState f c p -> DDownState f c q -> DDownState f c (p, q)

This is a synonym for prodDDownState.

Bidirectional Tree State Transformations

runDState :: Traversable f => DUpState' f (u, d) u -> DDownState' f (u, d) d -> d -> Term f -> u

This combinator combines a bottom-up and a top-down state transformations. Both state transformations can depend mutually recursive on each other.

Operators for Finite Mappings

(&) :: Mapping m k => m v -> m v -> m v infixr 0

left-biased union of two mappings.

(|->) :: Mapping m k => k -> v -> m v infix 1

This operator constructs a singleton mapping.

empty :: Mapping m k => m v

This is the empty mapping.

Product State Spaces

module Data.Projection

Annotations

propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g) => QHom f q g -> QHom f' q g'

Lift a stateful term homomorphism over signatures f and g to a stateful term homomorphism 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 bottom-up tree transducer over signatures f and g to a bottom-up tree transducer over the same signatures, but extended with annotations.

propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) => DownTrans f q g -> DownTrans f' q g'

Lift a top-down tree transducer over signatures f and g to a top-down tree transducer over the same signatures, but extended with annotations.

pathAnn :: forall g. Traversable g => CxtFun g (g :&: [Int])

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.