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.
- data Ref a env where
- data Equal where
- match :: Ref a env -> Ref b env -> Maybe (Equal a b)
- lookup :: Ref a env -> env -> a
- update :: (a -> a) -> Ref a env -> env -> env
- data Env term use def where
- type FinalEnv t usedef = Env t usedef usedef
- newtype T e s = T {}
- 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 Trafo m t s a b = Trafo (forall env1. m env1 -> TrafoE m t s a b env1)
- data TrafoE m t s a b env1 = forall env2 . TrafoE (m env2) (a -> T env2 s -> Env t s env1 -> (b, T env1 s, Env t s env2))
- data Unit s = Unit
- newSRef :: Trafo Unit t s (t a s) (Ref a s)
- extEnv :: m (e, a) -> TrafoE m t s (t a s) (Ref a s) e
- castSRef :: m e -> Ref a e -> TrafoE m t s x (Ref a s) e
- updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s i (Ref a s) e
- data Result m t b = 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
- sequenceA :: [Trafo m t s a b] -> Trafo m t s a [b]
- data Trafo2 m t a b = Trafo2 (forall env1. m env1 -> TrafoE2 m t a b env1)
- data TrafoE2 m t a b env1 = forall env2 . TrafoE2 (m env2) (forall s. a s -> T env2 s -> Env t s env1 -> (b s, T env1 s, Env t s env2))
- newSRef2 :: Trafo2 Unit t (t a) (Ref a)
- runTrafo2 :: Trafo2 m t a b -> m () -> (forall s. a s) -> Result m t b
- newtype Pair a b s = P (a s, b s)
- class Category2 arr => Arrow2 arr where
- class Arrow2 arr => ArrowLoop2 arr where
- newtype List a s = List [a s]
- sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b)
Typed References and Environments
Typed References
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
.
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.
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
.
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.
Transformation Library
Trafo
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.
data TrafoE m t s a b env1 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 and the environment (Env t s env1
) where the
current transformation starts. The function returns: the output (b
), a
Ref
-transformer (T env1 s
) from the initial environment of this step to the final
environment and the environment (Env t s env2
) constructed in this step.
Create New References
updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s i (Ref a s) eSource
The function updateSRef
returns a TrafoE
that updates the value pointed
by the reference passed as parameter into the current environment.
Run a Trafo
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
Alternative Transformation Library
Trafo2
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 |(* -> *)|.
Instances
ArrowLoop2 (Trafo2 m t) | |
Arrow2 (Trafo2 m t) | |
Category2 (Trafo2 m t) |
Create New References
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
class Arrow2 arr => ArrowLoop2 arr whereSource
Instances
ArrowLoop2 (Trafo2 m t) |