-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Typed Transformations of Typed Abstract Syntax
--
-- Library for Typed Transformations of Typed Abstract Syntax
@package TTTAS
@version 0.4.2
-- | 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.
module Language.AbstractSyntax.TTTAS
-- | 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.
data Ref a env
Zero :: Ref a (env', a)
Suc :: Ref a env' -> Ref a (env', b)
-- | The Equal type encodes type equality.
data Equal :: * -> * -> *
Eq :: Equal a a
-- | 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.
match :: Ref a env -> Ref b env -> Maybe (Equal a b)
-- | The function lookup returns the element indexed in the
-- environment parameter by the Ref parameter. The types guarantee
-- that the lookup succeeds.
lookup :: Ref a env -> env -> a
-- | The function update takes an additional function as argument,
-- which is used to update the value the reference addresses.
update :: (a -> a) -> Ref a env -> env -> env
-- | 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.
data Env term use def
Empty :: Env t use ()
Ext :: Env t use def' -> t a use -> Env t use (def', a)
-- | 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.
type FinalEnv t usedef = Env t usedef usedef
-- | The type T encodes a Ref-transformer. It is usually used
-- to transform references from an actual environment to the final one.
newtype T e s
T :: (forall x. Ref x e -> Ref x s) -> T e s
unT :: T e s -> 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
-- | 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 Trafo m t s a b
Trafo :: (forall env1. m env1 -> TrafoE m t s env1 a b) -> Trafo m t s 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.
data TrafoE m t s env1 a b
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)) -> TrafoE m t s env1 a b
data Unit s
Unit :: Unit 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.
newSRef :: Trafo Unit t s (t a s) (Ref a s)
-- | The function extEnv returns a TrafoE that extends the
-- current environment.
extEnv :: m (e, a) -> TrafoE m t s e (t a s) (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.
castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s)
-- | The function updateSRef returns a TrafoE that updates
-- the value pointed by the reference passed as parameter into the
-- current 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 updateFinalEnv returns a Trafo that
-- introduces a function (FinalEnv t s -> FinalEnv t s) to
-- update the final environment.
updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) ()
-- | 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.
data Result m t b
Result :: (m s) -> (b s) -> (FinalEnv t s) -> 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).
runTrafo :: (forall s. Trafo m t s a (b s)) -> m () -> a -> Result m t 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.
sequenceA :: [Trafo m t s a b] -> Trafo m t s 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 |(* -> *)|.
data Trafo2 m t a b
Trafo2 :: (forall env1. m env1 -> TrafoE2 m t env1 a b) -> Trafo2 m t a b
data TrafoE2 m t env1 a b
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)) -> TrafoE2 m t env1 a b
-- | 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.
newSRef2 :: Trafo2 Unit t (t a) (Ref a)
newtype UpdFinalEnv t s
Upd :: (FinalEnv t s -> FinalEnv t s) -> UpdFinalEnv t s
-- | The function updateFinalEnv2 returns a Trafo2 that
-- introduces a function ((UpdFinalEnv t)) to update the final
-- environment.
updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) Unit
-- | 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.
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) -> Pair a b s
class Category2 arr => Arrow2 (arr :: (* -> *) -> (* -> *) -> *)
arr2 :: Arrow2 arr => (forall s. a s -> b s) -> arr a b
first2 :: Arrow2 arr => arr a b -> arr (Pair a c) (Pair b c)
second2 :: Arrow2 arr => arr a b -> arr (Pair c a) (Pair c b)
(****) :: Arrow2 arr => arr a b -> arr a' b' -> arr (Pair a a') (Pair b b')
(&&&&) :: Arrow2 arr => arr a b -> arr a b' -> arr a (Pair b b')
class Arrow2 arr => ArrowLoop2 arr
loop2 :: ArrowLoop2 arr => arr (Pair a c) (Pair b c) -> arr a b
(>>>>) :: Category2 cat => cat a b -> cat b c -> cat a c
newtype List a s
List :: [a s] -> List a s
-- | 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.
sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b)
instance ArrowLoop2 (Trafo2 m t)
instance Arrow2 (Trafo2 m t)
instance Category2 (Trafo2 m t)
instance ArrowLoop (Trafo m t s)
instance Arrow (Trafo m t s)
instance Category (Trafo m t s)
instance Functor (TrafoE m t s e a)