TTTAS-0.4.0: Typed Transformations of Typed Abstract Syntax

Language.AbstractSyntax.TTTAS

Contents

Description

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.

Synopsis

Typed References and Environments

Typed References

data Ref a env whereSource

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 whereSource

The Equal type encodes type equality.

Constructors

Eq :: Equal a a 

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

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

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

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 whereSource

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 usedefSource

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 Source

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 sSource

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

Transformation Library

Trafo

data Trafo m t s a b Source

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 Source

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 Source

Constructors

Unit 

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

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

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

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) ()Source

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 Source

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 bSource

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]Source

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

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 Source

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

Update the Final Environment

newtype UpdFinalEnv t s Source

Constructors

Upd (FinalEnv t s -> FinalEnv t s) 

updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) UnitSource

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 bSource

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 Source

Constructors

P (a s, b s) 

class Category2 arr => Arrow2 arr whereSource

Methods

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

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

second2 :: 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

Instances

Arrow2 (Trafo2 m t) 

class Arrow2 arr => ArrowLoop2 arr whereSource

Methods

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

Instances

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

newtype List a s Source

Constructors

List [a s] 

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