TTTAS-0.6.0: Typed Transformations of Typed Abstract Syntax

Safe HaskellSafe-Inferred




Library for Typed Transformations of Typed Abstract Syntax.

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

Bibtex entry:;filename=TTTAS.bib

For more documentation see the TTTAS webpage:

For an example see examples/CSE2.hs

IMPORTANT: We would like to be able to use RebinadbleSyntax to use Arrow's Syntax in this variant of TTTAS, but this extension still doesn't work well with Arrows.


Typed References and Environments

Transformation Library


data Trafo m t a b Source

Alternative version of Trafo where the universal quantification over |s| is moved inside the quantification over |env2|. Note that the type variables |a| and |b| are now labelled with |s|, and hence have kind |(* -> *)|.


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


ArrowLoop2 (Trafo m t) 
Arrow2 (Trafo m t) 

data TrafoE m t env1 a b Source


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

Create New References

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

The Trafo2 newSRef2 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 newSRef2; therefore we use the type Unit for the meta-data.

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

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

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

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 -> FUpd i t a -> TrafoE m t e (SI i) (Ref a) Source

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 Unit (FinalEnv2 t) Source

Return as output the final environment.

putFinalEnv :: Trafo m t (FinalEnv2 t) Unit Source

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

updateFinalEnv :: Trafo m t (UpdFinalEnv t) Unit Source

The function updateFinalEnv returns a Trafo that introduces a function ((UpdFinalEnv t)) to update the final environment.

Run a Trafo

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

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 runTrafo2 ensures that transformation steps cannot make any assumptions about the type of final environment (s). It is an alternative version of runTrafo which does not use unsafeCoerce.

Arrow-style Combinators

newtype Pair a b s Source


P (a s, b s) 

class Category2 arr => Arrow2 arr where Source


arr :: (forall s. a s -> b s) -> arr a b Source

first :: arr a b -> arr (Pair a c) (Pair b c) Source

second :: arr a b -> arr (Pair c a) (Pair c b) Source

(***) :: arr a b -> arr a' b' -> arr (Pair a a') (Pair b b') Source

(&&&) :: arr a b -> arr a b' -> arr a (Pair b b') Source


Arrow2 (Trafo m t) 

class Arrow2 arr => ArrowLoop2 arr where Source


loop :: arr (Pair a c) (Pair b c) -> arr a b Source


(>>>) :: Category2 cat => cat a b -> cat b c -> cat a c Source

newtype List a s Source


List [a s] 

sequenceA :: [Trafo m t a b] -> Trafo m t a (List b) Source

The combinator sequenceA2 sequentially composes a list of Trafo2s into a Trafo2 that yields a List of outputs. Its use is analogous to the combinator sequence combinator for Monads.

returnA :: Arrow2 arr => arr a a Source