Language.AbstractSyntax.TTTAS2

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/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

module Language.AbstractSyntax.TTTAS.Common

Transformation Library

Trafo

data Trafo m t a b

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

Constructors

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

Instances

ArrowLoop2 (Trafo m t)

Arrow2 (Trafo m t)

data TrafoE m t env1 a b

Constructors

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)

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)

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

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

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)

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)

Return as output the final environment.

putFinalEnv :: Trafo m t (FinalEnv2 t) Unit

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

updateFinalEnv :: Trafo m t (UpdFinalEnv t) Unit

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

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

Constructors

P (a s, b s)

class Category2 arr => Arrow2 arr where

Methods

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

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

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

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

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

Instances

Arrow2 (Trafo m t)

class Arrow2 arr => ArrowLoop2 arr where

Methods

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

Instances

ArrowLoop2 (Trafo m t)

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

newtype List a s

Constructors

List [a s]

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

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