Language.AbstractSyntax.TTTAS

Library for Typed Transformations of Typed Abstract Syntax.

The library is documented in the paper: Typed Transformations of Typed Abstract Syntax

Bibtex entry: http://www.cs.uu.nl/wiki/bin/viewfile/Center/TTTAS?rev=1;filename=TTTAS.bib

For more documentation see the TTTAS webpage: http://www.cs.uu.nl/wiki/bin/view/Center/TTTAS.

For an example see examples/CSE1.hs

Typed References and Environments

module Language.AbstractSyntax.TTTAS.Common

Transformation Library

Trafo

data Trafo m t s a b

The type Trafo is the type of the transformation steps on a heterogeneous collection. The argument m stands for the type of the meta-data. A |Trafo| takes the meta-data on the current environment |env1| as input and yields meta-data for the (possibly extended) environment |env2|. The type t is the type of the terms stored in the environment. The type variable s represents the type of the final result, which we do expose. Its role is similar to the s in the type ST s a. The arguments a and b are the Arrow's input and output, respectively.

Constructors

Trafo (forall env1. m env1 -> TrafoE m t s env1 a b)

Instances

Category * (Trafo m t s)

Arrow (Trafo m t s)

ArrowLoop (Trafo m t s)

data TrafoE m t s env1 a b

The type TrafoE is used to introduce an existential quantifier into the definition of Trafo. It can be seen that a Trafo is a function taking as arguments: the input (a), a Ref-transformer (T env2 s) from the environment constructed in this step to the final environment, the environment (Env t s env1) where the current transformation starts and the "final environment" (FinalEnv t s) with the updates thus far applied. The function returns: the output (b), a Ref-transformer (T env1 s) from the initial environment of this step to the final environment, the environment (Env t s env2) constructed in this step and the final environment (FinalEnv t s) possibly updated.

Constructors

forall env2 . TrafoE (m env2) (a -> T env2 s -> Env t s env1 -> FinalEnv t s -> (b, T env1 s, Env t s env2, FinalEnv t s))

Instances

Functor (TrafoE m t s e a)

Create New References

newSRef :: Trafo Unit t s (t a s) (Ref a s)

The Trafo newSRef takes a typed term as input, adds it to the environment and yields a reference pointing to this value. No meta-information on the environment is recorded by newSRef; therefore we use the type Unit for the meta-data.

extEnv :: m (e, a) -> TrafoE m t s e (t a s) (Ref a s)

The function extEnv returns a TrafoE that extends the current environment.

castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s)

The function castSRef returns a TrafoE that casts the reference passed as parameter (in the constructed environment) to one in the final environment.

updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s)

The function updateSRef returns a TrafoE that updates the value pointed by the reference passed as parameter into the current environment.

State-like operations on the Final Environment

getFinalEnv :: Trafo m t s () (FinalEnv t s)

Return as output the final environment.

putFinalEnv :: Trafo m t s (FinalEnv t s) ()

Change the final environment by the one passed in the input.

updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) ()

The function updateFinalEnv returns a Trafo that updates the final environment using the input function (FinalEnv t s -> FinalEnv t s).

Run a Trafo

runTrafo :: (forall s. Trafo m t s a (b s)) -> m () -> a -> Result m t b

The function runTrafo takes as arguments the Trafo we want to run, meta-information for the empty environment, and an input value. The result of runTrafo (type Result) is the final environment (Env t s s) together with the resulting meta-data (m s), and the output value (b s). The rank-2 type for runTrafo ensures that transformation steps cannot make any assumptions about the type of final environment (s).

Other Combinators

sequenceA :: [Trafo m t s a b] -> Trafo m t s a [b]

The combinator sequenceA sequentially composes a list of Trafos into a Trafo that yields a list of outputs. Its use is analogous to the combinator sequence combinator for Monads.