Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell98 |
Language.AbstractSyntax.TTTAS2
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.
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.
- module Language.AbstractSyntax.TTTAS.Common
- data Trafo m t a b = Trafo (forall env1. m env1 -> TrafoE m t env1 a b)
- data TrafoE m t env1 a b = 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))
- newSRef :: Trafo Unit t (t a) (Ref a)
- extEnv :: m (e, a) -> TrafoE m t e (t a) (Ref a)
- castSRef :: m e -> Ref a e -> TrafoE m t e x (Ref a)
- updateSRef :: m e -> Ref a e -> FUpd i t a -> TrafoE m t e (SI i) (Ref a)
- getFinalEnv :: Trafo m t Unit (FinalEnv2 t)
- putFinalEnv :: Trafo m t (FinalEnv2 t) Unit
- updateFinalEnv :: Trafo m t (UpdFinalEnv t) Unit
- runTrafo :: Trafo 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
- (>>>) :: Category2 cat => cat a b -> cat b c -> cat a c
- newtype List a s = List [a s]
- sequenceA :: [Trafo m t a b] -> Trafo m t a (List b)
- returnA :: Arrow2 arr => arr a a
Typed References and Environments
Transformation Library
Trafo
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 (Trafo m t) | |
Arrow2 (Trafo m t) |
Create New References
newSRef :: Trafo 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.
updateSRef :: m e -> Ref a e -> FUpd i t a -> TrafoE m t e (SI i) (Ref a) Source
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) Source
Return as output the final environment.
putFinalEnv :: Trafo m t (FinalEnv2 t) Unit Source
Change the final environment by the one passed in the input.
updateFinalEnv :: Trafo m t (UpdFinalEnv t) Unit Source
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 Source
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
class Arrow2 arr => ArrowLoop2 arr where Source
Instances
ArrowLoop2 (Trafo m t) |