Language.AbstractSyntax.TTTAS.Common

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

data Unit s

Constructors

Unit

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)