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.

Typed References and Environments

Typed References

data Ref a env where

The Ref type for represents typed indices which are labeled with both the type of value to which they refer and the type of the environment (a nested Cartesian product, growing to the right) in which this value lives. The constructor Zero expresses that the first element of the environment has to be of type a. The constructor Suc does not care about the type of the first element in the environment, being polymorphic in the type b.

Constructors

Zero :: Ref a (env', a)

Suc :: Ref a env' -> Ref a (env', b)

data Equal where

The Equal type encodes type equality.

Constructors

Eq :: Equal a a

match :: Ref a env -> Ref b env -> Maybe (Equal a b)

The function match compares two references for equality. If they refer to the same element in the environment the value Just Eq is returned, expressing the fact that the types of the referred values are the same too.

lookup :: Ref a env -> env -> a

The function lookup returns the element indexed in the environment parameter by the Ref parameter. The types guarantee that the lookup succeeds.

update :: (a -> a) -> Ref a env -> env -> env

The function update takes an additional function as argument, which is used to update the value the reference addresses.

Declarations

data Env term use def where

The type Env term use def represents a sequence of instantiations of type forall a. term a use, where all the instances of a are stored in the type parameter def. The type use is a sequence containing the types to which may be referred from within terms of type term a use.

Constructors

Empty :: Env t use ()

Ext :: Env t use def' -> t a use -> Env t use (def', a)

type FinalEnv t usedef = Env t usedef usedef

When the types def and use of an Env coincide, we can be sure that the references in the terms do not point to values outside the environment but point to terms representing the right type. This kind of environment is the final environment of a transformation.

newtype T e s

The type T encodes a Ref-transformer. It is usually used to transform references from an actual environment to the final one.

Constructors

T

Fields

unT :: forall x. Ref x e -> Ref x s

lookupEnv :: Ref a env -> Env t s env -> t a s

updateEnv :: (t a s -> t a s) -> Ref a env -> Env t s env -> Env t s env

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

Arrow (Trafo m t s)

ArrowLoop (Trafo m t s)

Category (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 a function (FinalEnv t s -> FinalEnv t s) to update (modify) the final environment. 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 a function (FinalEnv t s -> FinalEnv t s) to update (modify) the final environment. NOTE: The function (FinalEnv t s -> FinalEnv t s) was introduced in version 0.3. It's carried throw the transformation steps and can be modified (composed to another function) using the function updateFinalEnv.

Constructors

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

Instances

Functor (TrafoE m t s e a)

Create New References

data Unit s

Constructors

Unit

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.

Update the Final Environment

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

The function updateFinalEnv returns a Trafo that introduces a function (FinalEnv t s -> FinalEnv t s) to update the final environment.

Run a Trafo

data Result m t b

The type Result is the type of the result of "running" a Trafo. Because s could be anything we have to hide it using existential quantification.

Constructors

forall s . Result (m s) (b s) (FinalEnv t s)

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.

Alternative Transformation Library

Trafo2

data Trafo2 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

Trafo2 (forall env1. m env1 -> TrafoE2 m t env1 a b)

Instances

ArrowLoop2 (Trafo2 m t)

Arrow2 (Trafo2 m t)

Category2 (Trafo2 m t)

data TrafoE2 m t env1 a b

Constructors

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

Create New References

newSRef2 :: Trafo2 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.

Update the Final Environment

newtype UpdFinalEnv t s

Constructors

Upd (FinalEnv t s -> FinalEnv t s)

updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) Unit

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

Run a Trafo2

runTrafo2 :: Trafo2 m t a b -> m () -> (forall s. a s) -> Result m t b

The function runTrafo2 takes as arguments the Trafo2 we want to run, meta-information for the empty environment, and an input value. The result of runTrafo2 (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

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

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

second2 :: 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 (Trafo2 m t)

class Arrow2 arr => ArrowLoop2 arr where

Methods

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

Instances

ArrowLoop2 (Trafo2 m t)

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

newtype List a s

Constructors

List [a s]

sequenceA2 :: [Trafo2 m t a b] -> Trafo2 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.