TTTAS 0.4.2 → 0.6.0

raw patch · 7 files changed

+794/−758 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• TTTAS.cabal +4/−2
• examples/CSE.hs +0/−196
• examples/CSE1.hs +202/−0
• examples/CSE2.hs +165/−244
• src/Language/AbstractSyntax/TTTAS.hs +55/−316
• src/Language/AbstractSyntax/TTTAS/Common.hs +122/−0
• src/Language/AbstractSyntax/TTTAS2.hs +246/−0

@@ -1,7 +1,8 @@ cabal-version:      >=1.2.3 build-type:         Simple name:               TTTAS-version:            0.4.2++version:            0.6.0 license:            LGPL license-file:       COPYRIGHT maintainer:         Marcos Viera <mviera@fing.edu.uy>@@ -13,7 +14,8 @@ extra-source-files: README, LICENSE-LGPL, TTTAS.bib library         build-depends:      base >= 4 && < 5-        exposed-modules:    Language.AbstractSyntax.TTTAS       +        exposed-modules:    Language.AbstractSyntax.TTTAS, Language.AbstractSyntax.TTTAS2,+                            Language.AbstractSyntax.TTTAS.Common                extensions:         Arrows, KindSignatures, RankNTypes, GADTs, CPP         hs-source-dirs:     src         ghc-options:        -Wall

@@ -1,196 +0,0 @@-{-# OPTIONS -fglasgow-exts -XGADTs -XArrows #-}--module CSE where--import Language.AbstractSyntax.TTTAS-import Prelude hiding (lookup)-import Control.Arrow--data Expr  a env where-     Var       ::  Ref a env      -> Expr a env-     IntVal    ::  Int            -> Expr Int env-     BoolVal   ::  Bool           -> Expr Bool env -     Cons      ::  Expr a env     -> Expr [a]  env -               ->  Expr [a] env-     Nil       ::  Expr [a] env-     Add       ::  Expr Int env   -> Expr Int env         -               ->  Expr Int env-     LessThan  ::  Expr Int env   -> Expr Int env                 -               ->  Expr Bool env -     If        ::  Expr Bool env  -> Expr a env          -               ->  Expr a env     ->  Expr a env--eval    :: Expr  a env   -> env ->  a-eval (Var r)         e   =  lookup r e-eval (IntVal i)      _   =  i-eval (BoolVal b)     _   =  b-eval (Add x y)       e   =  eval x e + eval y e-eval (Cons x y)      e   =  eval x e : eval y e-eval Nil             _   =  []-eval (LessThan x y)  e   =  eval x e < eval y e-eval (If x y z)      e   =  if    eval x e -                            then  eval y e-                            else  eval z e--type Decls env  = Env Expr env env--data TDecls env = forall env' . TDecls  (Decls env') -                                        (T env env')--a = Suc Zero-b = Zero-exampledecls :: Decls (((),Int),Int)-exampledecls = - Empty  `Ext` (IntVal 4) -        `Ext` (Add  (Add (Var a) (IntVal 4)) -                    (Add (Var a) (IntVal 4)))--resdecls :: TDecls (((),Int),Int)-resdecls = cse exampledecls--evalDecls   :: Decls env -> env-evalVar     :: Ref a env -> TDecls env -> a-evalVar var (TDecls ds (T tt))- = lookup (tt var) (evalDecls ds)--value_a = evalVar a resdecls-value_b = evalVar b resdecls--evalDecls (ds :: Decls env) = -            let result :: env-                result = evalD ds-                evalD :: Env Expr env def -> def-                evalD Empty = ()-                evalD (Ext ds e) = (evalD ds,eval e result)-            in result--resdecls2 :: TDecls (((),Int),Int)  -resdecls2 =  --  TDecls-  (  Empty  `Ext` (IntVal 4) -            `Ext` (Add  (Var (Suc (Suc Zero))) -                        (Var (Suc (Suc Zero))))-            `Ext` (Add  (Var (Suc Zero)) -                        (Var (Suc Zero)))-  )-  (  T (\ref -> case ref of  -                  Zero      -> Zero -                  Suc Zero  -> Suc (Suc Zero))-     ::  T (((), Int), Int) ((((), Int), Int), Int))--instance Show (Ref a env) where-    show x = "#" ++ (show $ refint x) -refint :: Ref a env -> Int-refint Zero = 0-refint (Suc x) = 1 + refint x-instance Show (Expr a env) where-    show (Var r) = "v" ++ (show $ refint r)-    show (IntVal i) = show i-    show (BoolVal i) = show i-    show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"-    show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"-    show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z--equals  ::  Expr a env -> Expr b env ->  Maybe (Equal a b)-equals (Var r1) (Var r2)          = match r1 r2-equals (IntVal i1) (IntVal i2) -                        | i1==i2  = Just Eq-equals (LessThan x1 y1) (LessThan x2 y2) -       = do  Eq <- equals x1 x2 -             Eq <- equals y1 y2 -             return Eq --equals (BoolVal b1) (BoolVal b2) -                        | b1==b2  = Just Eq-equals (Add x1 y1) (Add x2 y2) = do-                                      Eq <- equals x1 x2-                                      Eq <- equals y1 y2 -                                      return Eq -equals (If x1 y1 z1) (If x2 y2 z2)  -                                  = do-                                      Eq <- equals x1 x2-                                      Eq <- equals y1 y2 -                                      Eq <- equals z1 z2 -                                      return Eq -equals _ _ = Nothing--newtype Memo env env'-  =  Memo -     ( forall x  .   Expr x env -                 ->  Maybe (Ref x env')-     )--emptyMemo  ::  Memo env ()-emptyMemo  =   Memo (const Nothing)--type TrafoCSE env = Trafo (Memo env) Expr--insertIfNew  ::  forall s a env . Expr a env -             ->  TrafoCSE env s (Expr a s) (Ref a s)-insertIfNew e =   -  Trafo-  (\(Memo m :: Memo env env') -> case m e of-     Nothing -> extEnv  (extMemo e (Memo m)) -     Just r  -> castSRef (Memo m) r -  )- -extMemo  :: Expr a env -> Memo env env' -         -> Memo env (env',a)-extMemo e (Memo m) -         = Memo  (\s -> case equals e s of-                                           Just Eq -> Just Zero-                                           Nothing -> fmap Suc (m s)-                 ) --app_cse  ::  Expr a env -         ->  TrafoCSE env s (T env s) (Ref a s) -app_cse (Var r)       = proc (T tenv_s) -> -                           returnA -< tenv_s r--app_cse e@(IntVal i)  = proc _ -> -                           insertIfNew e -< IntVal i --app_cse e@(LessThan x y) -                      = proc tt -> -                          do  l <- app_cse x -< tt-                              r <- app_cse y -< tt-                              insertIfNew e -< LessThan (Var l) (Var r)-app_cse e@(BoolVal b) = proc _ -> -                           insertIfNew e -< BoolVal b   -app_cse e@(Add x y)   = proc tt -> -                          do  l <- app_cse x -< tt-                              r <- app_cse y -< tt-                              insertIfNew e -< Add (Var l) (Var r)-                             -app_cse e@(If x y z)  = proc tt -> -                          do  b <- app_cse x -< tt-                              l <- app_cse y -< tt-                              r <- app_cse z -< tt-                              insertIfNew e -< If (Var b) (Var l) (Var r)- -cse_env  ::  Env Expr env env'-         ->  TrafoCSE env s-                    (T env s) -                    (Env Ref s env')--cse_env Empty       = proc _ -> returnA -< Empty -cse_env (Ext es e) = proc tt ->-                       do  renv  <- cse_env es  -< tt-                           r     <- app_cse e   -< tt-                           returnA -< Ext renv r --refTransformer :: Env Ref s env -> T env s-refTransformer refs = T (\r -> lookupEnv r refs)--trafo :: Decls env -> TrafoCSE env s () (T env s)-trafo decls =  proc _ -> -                      do  rec  let tt = refTransformer refs-                               refs <- cse_env decls -< tt-                          returnA -< tt--cse :: forall env . Decls env -> TDecls env-cse decls-   = case  runTrafo (trafo decls) emptyMemo () of-           Result _ t env -> TDecls env t-

@@ -0,0 +1,202 @@+{-# LANGUAGE ExistentialQuantification, ScopedTypeVariables, RankNTypes, GADTs, Arrows #-}+++module CSE where++import Language.AbstractSyntax.TTTAS+import Prelude hiding (lookup)+import Control.Arrow++ifThenElse c t e = case c of+                   True -> t+                   False -> e+data Expr  a env where+     Var       ::  Ref a env      -> Expr a env+     IntVal    ::  Int            -> Expr Int env+     BoolVal   ::  Bool           -> Expr Bool env +     Cons      ::  Expr a env     -> Expr [a]  env +               ->  Expr [a] env+     Nil       ::  Expr [a] env+     Add       ::  Expr Int env   -> Expr Int env         +               ->  Expr Int env+     LessThan  ::  Expr Int env   -> Expr Int env                 +               ->  Expr Bool env +     If        ::  Expr Bool env  -> Expr a env          +               ->  Expr a env     ->  Expr a env++eval    :: Expr  a env   -> env ->  a+eval (Var r)         e   =  lookup r e+eval (IntVal i)      _   =  i+eval (BoolVal b)     _   =  b+eval (Add x y)       e   =  eval x e + eval y e+eval (Cons x y)      e   =  eval x e : eval y e+eval Nil             _   =  []+eval (LessThan x y)  e   =  eval x e < eval y e+eval (If x y z)      e   =  if    eval x e +                            then  eval y e+                            else  eval z e++type Decls env  = Env Expr env env++data TDecls env = forall env' . TDecls  (Decls env') +                                        (T env env')++a = Suc Zero+b = Zero+exampledecls :: Decls (((),Int),Int)+exampledecls = + Empty  `Ext` (IntVal 4) +        `Ext` (Add  (Add (Var a) (IntVal 4)) +                    (Add (Var a) (IntVal 4)))++resdecls :: TDecls (((),Int),Int)+resdecls = cse exampledecls++evalDecls   :: Decls env -> env+evalVar     :: Ref a env -> TDecls env -> a+evalVar var (TDecls ds (T tt))+ = lookup (tt var) (evalDecls ds)++value_a = evalVar a resdecls+value_b = evalVar b resdecls++evalDecls (ds :: Decls env) = +            let result :: env+                result = evalD ds+                evalD :: Env Expr env def -> def+                evalD Empty = ()+                evalD (Ext ds e) = (evalD ds,eval e result)+            in result++resdecls2 :: TDecls (((),Int),Int)  +resdecls2 =  ++  TDecls+  (  Empty  `Ext` (IntVal 4) +            `Ext` (Add  (Var (Suc (Suc Zero))) +                        (Var (Suc (Suc Zero))))+            `Ext` (Add  (Var (Suc Zero)) +                        (Var (Suc Zero)))+  )+  (  T (\ref -> case ref of  +                  Zero      -> Zero +                  Suc Zero  -> Suc (Suc Zero))+     ::  T (((), Int), Int) ((((), Int), Int), Int))++instance Show (Ref a env) where+    show x = "#" ++ (show $ refint x) +refint :: Ref a env -> Int+refint Zero = 0+refint (Suc x) = 1 + refint x+instance Show (Expr a env) where+    show (Var r) = "v" ++ (show $ refint r)+    show (IntVal i) = show i+    show (BoolVal i) = show i+    show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"+    show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"+    show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z++equals  ::  Expr a env -> Expr b env ->  Maybe (Equal a b)+equals (Var r1) (Var r2)          = match r1 r2+equals (IntVal i1) (IntVal i2) +                        | i1==i2  = Just Eq+equals (LessThan x1 y1) (LessThan x2 y2) +       = do  Eq <- equals x1 x2 +             Eq <- equals y1 y2 +             return Eq ++equals (BoolVal b1) (BoolVal b2) +                        | b1==b2  = Just Eq+equals (Add x1 y1) (Add x2 y2) = do+                                      Eq <- equals x1 x2+                                      Eq <- equals y1 y2 +                                      return Eq +equals (If x1 y1 z1) (If x2 y2 z2)  +                                  = do+                                      Eq <- equals x1 x2+                                      Eq <- equals y1 y2 +                                      Eq <- equals z1 z2 +                                      return Eq +equals _ _ = Nothing++newtype Memo env env'+  =  Memo +     ( forall x  .   Expr x env +                 ->  Maybe (Ref x env')+     )++emptyMemo  ::  Memo env ()+emptyMemo  =   Memo (const Nothing)++type TrafoCSE env = Trafo (Memo env) Expr++insertIfNew  ::  forall s a env . Expr a env +                 ->  TrafoCSE env s (Expr a s) (Ref a s)+insertIfNew e =   +  Trafo+  (\(Memo m :: Memo env env') -> case m e of+     Nothing -> extEnv  (extMemo e (Memo m)) +     Just r  -> castSRef (Memo m) r +  )+ +extMemo  :: Expr a env -> Memo env env' +         -> Memo env (env',a)+extMemo e (Memo m) +         = Memo  (\s -> case equals e s of+                                           Just Eq -> Just Zero+                                           Nothing -> fmap Suc (m s)+                 ) ++app_cse  ::  Expr a env +         ->  TrafoCSE env s (T env s) (Ref a s) +app_cse (Var r)       = proc (T tenv_s) -> +                           returnA -< tenv_s r++app_cse e@(IntVal i)  = proc _ -> +                           insertIfNew e -< IntVal i ++app_cse e@(LessThan x y) +                      = proc tt -> +                          do  l <- app_cse x -< tt+                              r <- app_cse y -< tt+                              insertIfNew e -< LessThan (Var l) (Var r)+app_cse e@(BoolVal b) = proc _ -> +                           insertIfNew e -< BoolVal b   +app_cse e@(Add x y)   = proc tt -> +                          do  l <- app_cse x -< tt+                              r <- app_cse y -< tt+                              insertIfNew e -< Add (Var l) (Var r)+                             +app_cse e@(If x y z)  = proc tt -> +                          do  b <- app_cse x -< tt+                              l <- app_cse y -< tt+                              r <- app_cse z -< tt+                              insertIfNew e -< If (Var b) (Var l) (Var r)+ +cse_env  ::  Env Expr env env'+         ->  TrafoCSE env s +                    (T env s) +                    (Env Ref s env')++cse_env Empty       = proc _ -> returnA -< Empty +cse_env (Ext es e) = proc tt ->+                       do  renv  <- cse_env es  -< tt+                           r     <- app_cse e   -< tt+                           returnA -< Ext renv r ++refTransformer :: Env Ref s env -> T env s+refTransformer refs = T (\r -> lookupEnv r refs)++data EmptyEnv s = EmptyEnv++trafo :: Decls env -> TrafoCSE env s () (T env s)+trafo decls =  proc _ -> +                      do  rec  let tt = refTransformer refs+                               refs <- cse_env decls -< tt+                          returnA -< tt++cse :: forall env . Decls env -> TDecls env+cse decls+   = case  runTrafo (trafo decls) emptyMemo () of+           Result _ t env -> TDecls env t+

@@ -1,285 +1,206 @@-{-# OPTIONS -fglasgow-exts -XGADTs  #-}-module CSE2 where+{-# LANGUAGE ExistentialQuantification, ScopedTypeVariables, RankNTypes, GADTs, Arrows  #-} -  import Language.AbstractSyntax.TTTAS+-- We can't use arrow notation because RebindableSyntax +-- doesn't work well with Arrows (yet) +module CSE where -  data Expr1 a where-       IntVal1    :: Int                               -> Expr1 Int-       BoolVal1   :: Bool                              -> Expr1 Bool-       Add1       :: Expr1 Int -> Expr1 Int            -> Expr1 Int-       LessThan1  :: Expr1 Int -> Expr1 Int            -> Expr1 Bool-       If1        :: Expr1 Bool -> Expr1 a -> Expr1 a  -> Expr1 a  +import Language.AbstractSyntax.TTTAS2+import Prelude hiding (lookup)+-- import Control.Arrow +ifThenElse c t e = case c of+                   True -> t+                   False -> e+data Expr  a env where+     Var       ::  Ref a env      -> Expr a env+     IntVal    ::  Int            -> Expr Int env+     BoolVal   ::  Bool           -> Expr Bool env +     Cons      ::  Expr a env     -> Expr [a]  env +               ->  Expr [a] env+     Nil       ::  Expr [a] env+     Add       ::  Expr Int env   -> Expr Int env         +               ->  Expr Int env+     LessThan  ::  Expr Int env   -> Expr Int env                 +               ->  Expr Bool env +     If        ::  Expr Bool env  -> Expr a env          +               ->  Expr a env     ->  Expr a env -  data Expr a env where-       Var       ::  Ref a env      -> Expr a env-       IntVal    ::  Int            -> Expr Int env-       BoolVal   ::  Bool           -> Expr Bool env -       Add       ::  Expr Int env   -> Expr Int env  -                                    -> Expr Int env-       LessThan  ::  Expr Int env   -> Expr Int env-                                    -> Expr Bool env -       If        ::  Expr Bool env  -> Expr a env  -                     -> Expr a env  -> Expr a env+eval    :: Expr  a env   -> env ->  a+eval (Var r)         e   =  lookup r e+eval (IntVal i)      _   =  i+eval (BoolVal b)     _   =  b+eval (Add x y)       e   =  eval x e + eval y e+eval (Cons x y)      e   =  eval x e : eval y e+eval Nil             _   =  []+eval (LessThan x y)  e   =  eval x e < eval y e+eval (If x y z)      e   =  if    eval x e +                            then  eval y e+                            else  eval z e -  -----------------------------EASY VERSION (Expr1 -> Env)-  -  newtype MapExpr1 env2-    =  MapExpr1 -       ( forall x  .   Expr1 x -                   ->  Maybe (Ref x env2)-       )-  -  emptyExpr1  ::  MapExpr1 env2 -  emptyExpr1  =   MapExpr1 (const Nothing)+type Decls env  = Env Expr env env -  type TrafoCSE1 inp out = Trafo2 MapExpr1 Expr inp out+data TDecls env = forall env' . TDecls  (Decls env') +                                        (T env env') -  data FinalExprs = forall env. FinalExprs (Env Expr env env)+a = Suc Zero+b = Zero+exampledecls :: Decls (((),Int),Int)+exampledecls = + Empty  `Ext` (IntVal 4) +        `Ext` (Add  (Add (Var a) (IntVal 4)) +                    (Add (Var a) (IntVal 4))) -  cse1 :: Expr1 t -> FinalExprs-  cse1 e-     = let result = runTrafo2 (app_cse1 e) emptyExpr1 undefined-       in case result of -         Result _ _ envs -> FinalExprs envs+resdecls :: TDecls (((),Int),Int)+resdecls = cse exampledecls  -  app_cse1 :: Expr1 a -> TrafoCSE1 t (Ref a) -  app_cse1 e@(IntVal1 i)  = arr2 (const (IntVal i)) -                        >>>> insertExpr1 e    -  app_cse1 e@(BoolVal1 b) = arr2 (const (BoolVal b)) -                        >>>> insertExpr1 e    -  app_cse1 e@(Add1 x y)   = (app_cse1 x &&&& app_cse1 y) -                        >>>> arr2 (\(P (l,r)) -> Add (Var l) (Var r)) -                        >>>> insertExpr1 e-  app_cse1 e@(LessThan1 x y) -                          = (app_cse1 x &&&& app_cse1 y) -                        >>>> arr2 (\(P (l,r)) -> LessThan (Var l) (Var r))-                        >>>> insertExpr1 e-  app_cse1 e@(If1 x y z)  = (app_cse1 x &&&& app_cse1 y &&&& app_cse1 z) -                        >>>> arr2 (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) -                        >>>> insertExpr1 e+evalDecls   :: Decls env -> env+evalVar     :: Ref a env -> TDecls env -> a+evalVar var (TDecls ds (T tt))+ = lookup (tt var) (evalDecls ds) -  insertExpr1 :: Expr1 a -> TrafoCSE1 (Expr a) (Ref a)-  insertExpr1 e =   -    Trafo2-    (\(MapExpr1 m) -> case m e of-       Nothing  ->  -         case newERef1 e-         of Trafo2 step -> step (MapExpr1 m)-       Just r   -> TrafoE2 (MapExpr1 m) -                        (\e (T t) env1 upds ->  (t r, T t, env1, upds))-    )+value_a = evalVar a resdecls+value_b = evalVar b resdecls -  newERef1 ::  Expr1 a -           ->  TrafoCSE1 (Expr a) (Ref a)-  newERef1 e =-    Trafo2 -    (\(MapExpr1 m :: MapExpr1 env1) ->-       let m2 = MapExpr1  (\s -> aux1 (matchExpr1 e s) m s)-       in TrafoE2  m2 -                 (\e (T t) env1 upds ->  (  t Zero-                                         ,  T (t . Suc) -                                         ,  Ext env1 e-                                         ,  upds-    )            )                       )+evalDecls (ds :: Decls env) = +            let result :: env+                result = evalD ds+                evalD :: Env Expr env def -> def+                evalD Empty = ()+                evalD (Ext ds e) = (evalD ds,eval e result)+            in result -  aux1 :: Maybe (Equal a x) -> (Expr1 x -> Maybe (Ref x env1)) -       -> Expr1 x -> Maybe (Ref x (env1,a))-  aux1 (Just Eq) _ _  = Just Zero-  aux1 Nothing   m s  = fmap Suc (m s)+resdecls2 :: TDecls (((),Int),Int)  +resdecls2 =   -  matchExpr1  ::  Expr1 a -> Expr1 b -              ->  Maybe (Equal a b)-  matchExpr1 (IntVal1 i1) (IntVal1 i2) -                          | i1==i2  = Just Eq-  matchExpr1 (BoolVal1 b1) (BoolVal1 b2) -                          | b1==b2  = Just Eq-  matchExpr1 (Add1 x1 y1) (Add1 x2 y2) -                                    = do-                                        Eq <- matchExpr1 x1 x2-                                        Eq <- matchExpr1 y1 y2 -                                        return Eq -  matchExpr1 (LessThan1 x1 y1) (LessThan1 x2 y2) -                                    = do-                                        Eq <- matchExpr1 x1 x2-                                        Eq <- matchExpr1 y1 y2 -                                        return Eq -  matchExpr1 (If1 x1 y1 z1) (If1 x2 y2 z2)  -                                    = do-                                        Eq <- matchExpr1 x1 x2-                                        Eq <- matchExpr1 y1 y2 -                                        Eq <- matchExpr1 z1 z2 -                                        return Eq -  matchExpr1 _ _ = Nothing+  TDecls+  (  Empty  `Ext` (IntVal 4) +            `Ext` (Add  (Var (Suc (Suc Zero))) +                        (Var (Suc (Suc Zero))))+            `Ext` (Add  (Var (Suc Zero)) +                        (Var (Suc Zero)))+  )+  (  T (\ref -> case ref of  +                  Zero      -> Zero +                  Suc Zero  -> Suc (Suc Zero))+     ::  T (((), Int), Int) ((((), Int), Int), Int)) -  --- little test1-  n1 x = IntVal1 x-  env1 = Add1 (Add1 (n1 2) (n1 3)) (Add1 (n1 4) (Add1 (n1 2) (n1 3)))+instance Show (Ref a env) where+    show x = "#" ++ (show $ refint x) +refint :: Ref a env -> Int+refint Zero = 0+refint (Suc x) = 1 + refint x+instance Show (Expr a env) where+    show (Var r) = "v" ++ (show $ refint r)+    show (IntVal i) = show i+    show (BoolVal i) = show i+    show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"+    show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"+    show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z -  res1 = show $ cse1 env1+equals  ::  Expr a env -> Expr b env ->  Maybe (Equal a b)+equals (Var r1) (Var r2)          = match r1 r2+equals (IntVal i1) (IntVal i2) +                        | i1==i2  = Just Eq+equals (LessThan x1 y1) (LessThan x2 y2) +       = do  Eq <- equals x1 x2 +             Eq <- equals y1 y2 +             return Eq  +equals (BoolVal b1) (BoolVal b2) +                        | b1==b2  = Just Eq+equals (Add x1 y1) (Add x2 y2) = do+                                      Eq <- equals x1 x2+                                      Eq <- equals y1 y2 +                                      return Eq +equals (If x1 y1 z1) (If x2 y2 z2)  +                                  = do+                                      Eq <- equals x1 x2+                                      Eq <- equals y1 y2 +                                      Eq <- equals z1 z2 +                                      return Eq +equals _ _ = Nothing -  ----------------------------MORE COMPLICATED VERSION (Env -> Env)+newtype Memo env env'+  =  Memo +     ( forall x  .   Expr x env +                 ->  Maybe (Ref x env')+     ) +emptyMemo  ::  Memo env ()+emptyMemo  =   Memo (const Nothing) +type TrafoCSE2 env = Trafo (Memo env) Expr -  newtype MapExpr env env2-    =  MapExpr -       ( forall x  .   Expr x env -                   ->  Maybe (Ref x env2)-       )+insertIfNew  ::  forall s a env . Expr a env +                 ->  TrafoCSE2 env  (Expr a ) (Ref a )+insertIfNew e =   +  Trafo+  (\(Memo m :: Memo env env') -> case m e of+     Nothing -> extEnv  (extMemo e (Memo m)) +     Just r  -> castSRef (Memo m) r +  )+ +extMemo  :: Expr a env -> Memo env env' +         -> Memo env (env',a)+extMemo e (Memo m) +         = Memo  (\s -> case equals e s of+                                           Just Eq -> Just Zero+                                           Nothing -> fmap Suc (m s)+                 )  -  emptyExpr  ::  MapExpr env env2 -  emptyExpr  =   MapExpr (const Nothing)+app_cse  ::  Expr a env +         ->  TrafoCSE2 env  (T env) (Ref a)  -  initExpr  :: TrafoCSE env a b -            ->  Trafo2 Unit Expr a b-  initExpr (Trafo2 st)-    = Trafo2  (\_ ->  case st emptyExpr of-                      TrafoE2 _  f -> TrafoE2 Unit f-            )+app_cse (Var r)       = arr (\(T tenv_s) -> tenv_s r)+app_cse e@(IntVal i)  = arr (const (IntVal i)) +                      >>> insertIfNew e    +app_cse e@(BoolVal b) = arr (const (BoolVal b)) +                      >>> insertIfNew e    +app_cse e@(Add x y)   = (app_cse x &&& app_cse y) +                      >>> arr (\(P (l,r)) -> Add (Var l) (Var r)) +                      >>> insertIfNew e -  type TrafoCSE env inp out = Trafo2 (MapExpr env) Expr inp out+app_cse e@(LessThan x y) +                       = (app_cse x &&& app_cse y) +                      >>> arr (\(P (l,r)) -> LessThan (Var l) (Var r))+                      >>> insertIfNew e  -  newtype Mapping old new -           = Mapping (Env Ref new old) --  map2trans :: Mapping env s -> T env s-  map2trans (Mapping env) -     = T (\r -> (lookupEnv r env))-+app_cse e@(If x y z)  = (app_cse x &&& app_cse y &&& app_cse z) +                      >>> arr (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) +                      >>> insertIfNew e + +newtype EEnv r e1 e2 = EEnv (Env r e2 e1) -  cse :: Env Expr env env -> FinalExprs-  cse e-     = let result = runTrafo2  -                    ( loop2 $ second2 $-                      arr2 (\menv_s -> map2trans menv_s) >>>> cse_env e -                    )-                    Unit       -- meta-data-                    undefined  -- input-       in case result of -         Result _ _ env -> FinalExprs env+cse_env  ::  Env Expr env env'+         ->  TrafoCSE2 env +                    (T env ) +                    (EEnv Ref  env')  -  cse_env  ::  Env Expr env env'-           ->  Trafo2  Unit -                      Expr-                      (T env) -                      (Mapping env')+cse_env Empty      = arr (const (EEnv Empty))   -  cse_env (Ext es e) = (initExpr (app_cse e) &&&& cse_env es) -                    >>>> arr2  (\(P (r, (Mapping  renv)))-                                -> Mapping (Ext renv r)+cse_env (Ext es e) = (app_cse e &&& cse_env es) +                    >>> arr  (\(P (r, (EEnv  renv)))+                                -> EEnv (Ext renv r)                              )-  cse_env Empty       = arr2 (const (Mapping Empty))    -  app_cse :: Expr a env -> TrafoCSE env (T env) (Ref a) -  app_cse (Var r)       = arr2 (\(T tenv_s) -> tenv_s r)-  app_cse e@(IntVal i)  = arr2 (const (IntVal i)) -                      >>>> insertExpr e    -  app_cse e@(BoolVal b) = arr2 (const (BoolVal b)) -                      >>>> insertExpr e    -  app_cse e@(Add x y)   = (app_cse x &&&& app_cse y) -                      >>>> arr2 (\(P (l,r)) -> Add (Var l) (Var r)) -                      >>>> insertExpr e-  app_cse e@(LessThan x y) -                        = (app_cse x &&&& app_cse y) -                      >>>> arr2 (\(P (l,r)) -> LessThan (Var l) (Var r))-                      >>>> insertExpr e-  app_cse e@(If x y z)  = (app_cse x &&&& app_cse y &&&& app_cse z) -                      >>>> arr2 (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) -                      >>>> insertExpr e--  insertExpr :: Expr a env -> TrafoCSE env (Expr a) (Ref a)-  insertExpr e =   -    Trafo2-    (\(MapExpr m) -> case m e of-       Nothing  ->  -         case newERef e-         of Trafo2 step -> step (MapExpr m)-       Just r   -> TrafoE2 (MapExpr m) -                        (\e (T t) env1 upds ->  (t r, T t, env1, upds))-    )--  newERef ::  Expr a env-          ->  TrafoCSE env (Expr a) (Ref a)-  newERef e =-    Trafo2 -    (\(MapExpr m :: MapExpr env env1) ->-       let m2 = MapExpr (\s -> aux (matchExpr e s) m s)-       in TrafoE2  m2 -                 (\e (T t) env1 upds ->  (  t Zero-                                         ,  T (t . Suc) -                                         ,  Ext env1 e-                                         ,  upds-    )            )                       )--  aux :: Maybe (Equal a x) -> (Expr x env -> Maybe (Ref x env1)) -      -> Expr x env -> Maybe (Ref x (env1,a))-  aux (Just Eq) _ _  = Just Zero-  aux Nothing   m s  = fmap Suc (m s)+refTransformer :: Env Ref s env -> T env s+refTransformer refs = T (\r -> lookupEnv r refs)  -  matchExpr  ::  Expr a env -> Expr b env -             ->  Maybe (Equal a b)-  matchExpr (Var r1) (Var r2)       = match r1 r2-  matchExpr (IntVal i1) (IntVal i2) -                          | i1==i2  = Just Eq-  matchExpr (BoolVal b1) (BoolVal b2) -                          | b1==b2  = Just Eq-  matchExpr (Add x1 y1) (Add x2 y2) = do-                                        Eq <- matchExpr x1 x2-                                        Eq <- matchExpr y1 y2 -                                        return Eq -  matchExpr (LessThan x1 y1) (LessThan x2 y2) -                                    = do-                                        Eq <- matchExpr x1 x2-                                        Eq <- matchExpr y1 y2 -                                        return Eq -  matchExpr (If x1 y1 z1) (If x2 y2 z2)  -                                    = do-                                        Eq <- matchExpr x1 x2-                                        Eq <- matchExpr y1 y2 -                                        Eq <- matchExpr z1 z2 -                                        return Eq -  matchExpr _ _ = Nothing-+data EmptyEnv s = EmptyEnv -  --- little test2-  vx = Var Zero-  n x = IntVal x-  env2 =  Empty `Ext` (n 2)-                `Ext` (Add (Add vx (n 3)) (Add (n 4) (Add vx (n 3))))- -  res2 = show $ cse env2+trafo :: Decls env -> TrafoCSE2 env EmptyEnv (T env )+trafo decls = loop $ arr (\(P (_,EEnv refs)) -> refTransformer refs) >>> (arr id &&& cse_env decls)    -  ------------------------- SHOW--  instance Show (Ref a env) where-    show x = "#" ++ (show $ refint x)-  -  refint :: Ref a env -> Int-  refint Zero = 0-  refint (Suc x) = 1 + refint x--  instance Show (Expr a env) where-    show (Var r) = show r-    show (IntVal i) = show i-    show (BoolVal i) = show i-    show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"-    show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"-    show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z--  instance Show (Env Expr env1 env2) where-    show (Ext es e) = (show e) ++ "|" ++ show es-    show Empty = ""--  instance Show FinalExprs where-    show (FinalExprs env) = show env+cse :: forall env . Decls env -> TDecls env+cse decls+   = case  runTrafo (trafo decls) emptyMemo EmptyEnv of+           Result _ t env -> TDecls env t 

@@ -1,6 +1,6 @@-{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs #-}
-{-# LANGUAGE CPP #-}
+{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs  #-}
 
+
 {-| 
     Library for Typed Transformations of Typed Abstract Syntax.
 
@@ -10,18 +10,15 @@ 
     For more documentation see the TTTAS webpage: 
     <http://www.cs.uu.nl/wiki/bin/view/Center/TTTAS>.
+
+    For an example see examples/CSE1.hs 
+
 -}
 
 module Language.AbstractSyntax.TTTAS (
                -- * Typed References and Environments
-
-               -- ** Typed References
-               Ref(..), Equal(..), 
-               match, lookup, update,
-
-               -- ** Declarations
-               Env(..), FinalEnv, T(..),
-               lookupEnv, updateEnv,
+               module Language.AbstractSyntax.TTTAS.Common,
+               
 
                -- * Transformation Library
                
@@ -29,136 +26,34 @@                Trafo(..), TrafoE(..),
 
                -- ** Create New References
-               Unit(..),
                newSRef, extEnv, castSRef, updateSRef,
 
-               -- ** Update the Final Environment
-               updateFinalEnv,
+               -- ** State-like operations on the Final Environment               
+               getFinalEnv, putFinalEnv, updateFinalEnv,
  
                -- ** Run a Trafo
-               Result(..), 
                runTrafo,
 
                -- ** Other Combinators
-               sequenceA,
+              sequenceA,
 
-               -- * Alternative Transformation Library
-               
-               -- ** Trafo2
-               Trafo2(..), TrafoE2(..),
 
-               -- ** Create New References
-               newSRef2,
-
-               -- ** Update the Final Environment
-               UpdFinalEnv(..), updateFinalEnv2,
-
-               -- ** Run a Trafo2 
-               runTrafo2,
-
-               -- ** Arrow-style Combinators
-               Pair(..), Arrow2(..), ArrowLoop2(..),
-               (>>>>),
-               List(..), sequenceA2
-
              ) where
  
-import Unsafe.Coerce ( unsafeCoerce )
-import qualified Prelude as P
 
-#if __GLASGOW_HASKELL__ >= 609 
-import Control.Category 
+#if __GLASGOW_HASKELL__ >= 710
+import Prelude hiding (lookup,(.), id, sequenceA) 
+#else
 import Prelude hiding (lookup,(.), id) 
-#endif   
+#endif
 
+import Unsafe.Coerce ( unsafeCoerce )
+import Control.Category
 import Control.Arrow 
-#if __GLASGOW_HASKELL__ < 609 
-  hiding (pure) 
-import Prelude hiding (lookup)
-#endif
+import Language.AbstractSyntax.TTTAS.Common
 
 
--- | 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 where
- Zero  ::                      Ref a (env',a)
- Suc   ::  Ref a      env' ->  Ref a (env',b)
 
--- | The 'Equal' type encodes type equality. 
-data Equal :: * -> * -> * where 
- 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)
-match  Zero     Zero        =  Just Eq
-match  (Suc x)  (Suc y)     =  match x y
-match  _        _           =  Nothing
-
--- | 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
-lookup  Zero     (_,a)  =  a
-lookup  (Suc r)  (e,_)  =  lookup r e
-
--- | 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  
-update f  Zero     (e,a)   =  (e,f a)
-update f  (Suc r)  (e,x)   =  (update f r e,x)
-
-
--- | 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 where
-  Empty  ::  Env t use  ()
-  Ext    ::  Env t use def' ->  t a use  
-         ->  Env t use  (def',a)
-
-
-lookupEnv  :: Ref a env -> Env t s env -> t a s
-lookupEnv  Zero     (Ext _ t)   =  t
-lookupEnv  (Suc r)  (Ext ts _)  =  lookupEnv r ts
-lookupEnv  _        _           =  error "Error: The impossible happened!"
-
-updateEnv  ::  (t a s -> t a s) -> Ref a env 
-           ->  Env t s env ->  Env t s env
-updateEnv  f  Zero     (Ext ts t)  
-              =        Ext ts (f t) 
-updateEnv  f  (Suc r)  (Ext ts t)  
-              =        Ext (updateEnv f r ts)  t
-updateEnv  _  _        _ 
-              =  error "Error: The impossible happened!"
-
-
--- | 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 {unT :: forall x . Ref x e -> Ref x s}
-
 -- | 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 
@@ -167,6 +62,10 @@ --   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)
 
@@ -175,22 +74,20 @@ --   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@), 
+--   transformation starts and the "final environment" (@FinalEnv t s@) 
+--   with the updates thus far applied. 
+--   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'.
+--   environment, the environment (@Env t s env2@) constructed in this step and the final environment
+--   (@FinalEnv t s@) possibly updated.
 data  TrafoE m t s env1 a b = 
  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))
+                        (       a  ->  T env2 s ->  Env t s env1 ->  FinalEnv t s
+                          -> (  b,     T env1 s,    Env t s env2,    FinalEnv t s)
                         )
 
-data Unit s         = Unit
 
+
 -- |  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';
@@ -200,20 +97,33 @@  =  Trafo  (\ _->  extEnv Unit)
 
 
--- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function
---   (@FinalEnv t s -> FinalEnv t s@) to update the final environment.
+
+-- | Change the final environment by the one passed in the input.
+putFinalEnv ::  Trafo m t s (FinalEnv t s) ()
+putFinalEnv = Trafo $ \m -> (TrafoE m (\fe t e _ -> ((), t, e, fe)))
+
+-- | Return as output the final environment.
+getFinalEnv ::  Trafo m t s () (FinalEnv t s)
+getFinalEnv = Trafo $ \m -> (TrafoE m (\_ t e fe -> (fe, t, e, fe)))
+
+-- | The function 'updateFinalEnv' returns a 'Trafo' that updates the
+--   final environment using the input function 
+--   (@FinalEnv t s -> FinalEnv t s@).
 updateFinalEnv ::  Trafo m t s (FinalEnv t s -> FinalEnv t s) ()
-updateFinalEnv = Trafo $ \m -> (TrafoE m (\f' t e f -> ((), t, e, f' . f)))
+updateFinalEnv = proc f ->
+                  do fe  <- getFinalEnv -< ()
+                     putFinalEnv -< f fe
+ -- Trafo $ \m -> (TrafoE m (\f t e fe -> ((), t, e, f fe)))
 
 
 -- | 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)
-extEnv m = TrafoE m $ \ta  (T tr) env  f ->  (tr Zero,  T (tr P.. Suc),  Ext env ta, f )
+extEnv m = TrafoE m $ \ta  (T tr) env  fe ->  (tr Zero,  T (tr . Suc),  Ext env ta, fe )
 
 -- | 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)
-castSRef m r = TrafoE m $ (\   _ (T t) decls f ->  (t r, T t, decls, f))
+castSRef m r = TrafoE m $ (\   _ (T t) decls fe ->  (t r, T t, decls, fe))
 
 -- | The function 'updateSRef' returns a 'TrafoE' that updates the value pointed
 --   by the reference passed as parameter into the current environment.
@@ -222,14 +132,11 @@ 
 
 instance Functor (TrafoE m t s e a) where
- fmap f (TrafoE m step) = TrafoE m $ \i t e fs -> case step i t e fs of
-                                                  (i',t',e',fs') -> (f i',t',e',fs')
+ fmap f (TrafoE m step) = TrafoE m $ \i t e fe -> case step i t e fe of
+                                                  (i',t',e',fe') -> (f i',t',e',fe')
 
--- | 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   
-   =  forall s . Result  (m s) (b s) (FinalEnv t s)
 
+
 -- | 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 
@@ -240,15 +147,14 @@            ->  Result m t b
 runTrafo trafo m a = case trafo of
   Trafo trf -> case trf m of
-                   TrafoE m2 f -> 
-                     case  f a (T unsafeCoerce) Empty P.id of  -- the function could also be passed as argument
-                       (rb, _, env2, fenvs) -> 
-                         Result  (unsafeCoerce m2)  
+                   TrafoE m2 f ->
+                     let (rb, _, env2, fenv) =  f a (T unsafeCoerce) Empty (unsafeCoerce env2) 
+                     in  Result  (unsafeCoerce m2)  
                                  rb 
-                                 (fenvs $ unsafeCoerce env2) 
+                                 (unsafeCoerce fenv) 
 
-#if __GLASGOW_HASKELL__ >= 609
 
+
 instance Category (Trafo m t s) where
  -- |(.) :: Trafo m t s b c  ->  Trafo m t s a b ->  Trafo m t s a c|
  Trafo t2 . Trafo t1 = 
@@ -268,32 +174,12 @@  -- |id :: Trafo m t s a a|
  id =  Trafo  (\m -> TrafoE m (\a t e f -> (a, t, e, f)) )
 
-#endif
-
-
 instance Arrow (Trafo m t s) where
 
  -- |arr :: (a  -> b) -> Trafo m t s a b|
  arr f =  Trafo  (\m -> TrafoE m (\a t e fs -> (f a, t, e, fs)) )
 
-#if __GLASGOW_HASKELL__ < 609 
 
- Trafo t1 >>> Trafo t2 = 
-  Trafo 
-  (\m1 -> case t1 m1 of
-                                      TrafoE m2 f1 -> case t2 m2 of
-                                       TrafoE m3 f2 ->
-                                        TrafoE 
-                                        m3 
-                                        (\a  tt env1 fs ->
-                                             let  (b,tt1, env2, fs')   = f1 a tt2 env1 fs
-                                                  (c,tt2, env3, fs'')  = f2 b tt env2 fs'
-                                             in   (c,tt1, env3, fs'')                                                                    
-                                        )
-  )
-
-#endif 
-
  -- |first :: Trafo m t s a b -> Trafo m t s (a, c) (b, c)|
  first (Trafo tr) 
   = Trafo (\m1 -> case tr m1 of
@@ -331,151 +217,4 @@            bs <- sequenceA xs -< a
            returnA -< (b:bs)  
 
-
-
-
--- | 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)
-data  TrafoE2 m t env1 a b = 
-  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)
-                 )
-
-newtype UpdFinalEnv t s = Upd (FinalEnv t s -> FinalEnv t s)
-
--- | 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
-runTrafo2 trafo m a = 
- case trafo of
-  Trafo2 trf -> case trf m of
-                   TrafoE2 m2 f -> 
-                      let  (rb, _, env2, Upd upds) =  f a (T P.id) Empty (Upd P.id)
-                      in   Result m2  rb (upds env2)
-
-
--- |  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)
-newSRef2 
-    =  Trafo2  
-       (\Unit ->  TrafoE2  
-                  Unit
-                  (\ta (T tr) env upds ->
-                      ( tr Zero
-                      , T (tr P.. Suc)
-                      , Ext env ta
-                      , upds
-       )          )   )
-
-
--- | The function 'updateFinalEnv2' returns a 'Trafo2' that introduces a function
---   (@(UpdFinalEnv t)@) to update the final environment.
-updateFinalEnv2 ::  Trafo2 m t (UpdFinalEnv t) Unit
-updateFinalEnv2 = Trafo2 $ \m -> (TrafoE2 m (\(Upd u') t e (Upd u) -> (Unit, t, e, (Upd $ u' P.. u))))
-
-
-newtype Pair a b s = P (a s, b s)
-
-class Category2 (cat :: (* -> *) -> (* -> *) -> *) where
-  id2     :: cat a a
-  (.:.)   :: cat b c -> cat a b -> cat a c
-
-class Category2 arr => Arrow2 (arr :: (* -> *) -> (* -> *) -> *) where
-  arr2    :: (forall s . a s -> b s) -> arr a b
-  first2  :: arr a b -> arr (Pair a c) (Pair b c)
-  second2 :: arr a b -> arr (Pair c a) (Pair c b)
-  (****)  :: arr a b -> arr a' b'
-          -> arr (Pair a a') (Pair b b')
-  (&&&&)  :: arr a b -> arr a b' -> arr a (Pair b b')
-
-class Arrow2 arr => ArrowLoop2 arr where
-  loop2   :: arr (Pair a c) (Pair b c) -> arr a b
-
-
-instance Category2 (Trafo2 m t) where
-  id2   =  Trafo2  (\m -> TrafoE2 m (\a t e u -> (a, t, e, u)))
-
-  (.:.) (Trafo2 sb) (Trafo2 sa) = 
-    Trafo2 
-    (\m1 ->
-       case sa m1 of 
-        TrafoE2 m2 f1 -> case sb m2 of 
-         TrafoE2 m3 f2 -> 
-           TrafoE2  
-           m3 
-           (\a t3s e1 u1 -> let  (b, t1s, e2, u2) = f1 a t2s e1 u1
-                                 (c, t2s, e3, u3) = f2 b t3s e2 u2
-                            in   (c, t1s, e3, u3)
-           ))
-
-
-(>>>>) :: Category2 cat => cat a b -> cat b c -> cat a c
-f >>>> g = g .:. f
-
- 
-instance Arrow2 (Trafo2 m t) where
-  arr2 f 
-    =  Trafo2  (\m -> TrafoE2 m (\a t e u -> (f a, t, e, u)) )
-
-  
-  first2 (Trafo2 s) 
-    =  Trafo2
-       (\m1 -> case s m1 of
-          TrafoE2 m2 f -> 
-             TrafoE2  m2
-                    (\(P (a, c)) t2s e1 u1 -> 
-                                      let (b,t12,e2,u2) = f a t2s e1 u1 
-                                      in  (P (b, c),t12,e2,u2)
-                    )              
-       ) 
-
-  second2 f = arr2 swap >>>> first2 f >>>> arr2 swap
-              where   swap :: Pair c a s -> Pair a c s
-                      swap ~(P (x, y)) = P (y, x)
-             
-  f **** g =  first2 f >>>> second2 g  
- 
-  f &&&& g = arr2 (\b -> P (b, b)) >>>> (f **** g)      
-
-
-instance ArrowLoop2 (Trafo2 m t) where
-  loop2 (Trafo2 st) =
-    Trafo2 
-    (\m -> case st m of
-            TrafoE2 m1 f1 ->
-             TrafoE2  m1
-             (\a t e u -> 
-               let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u                                                                            
-               in (b,t1,e1,u1)
-             ) 
-    )
-
-
-newtype List a s = List [a s]
-
--- | The combinator 'sequenceA2' sequentially composes a list
---   of 'Trafo2's into a 'Trafo2' that yields a 'List' of outputs.
---   Its use is analogous to the combinator 'sequence' combinator
---   for 'Monad's.
-sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b)
-sequenceA2 [] = arr2 (const (List []))
-sequenceA2 (x:xs) 
-       =  (x &&&& sequenceA2 xs) >>>> 
-          arr2 (\(P (a,List as)) -> List (a:as))
 

@@ -0,0 +1,122 @@+{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs  #-}
+
+
+{-| 
+    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.Common (
+               -- * Typed References and Environments
+
+               -- ** Typed References
+               Ref(..), Equal(..), 
+               match, lookup, update,
+
+               -- ** Declarations
+               Env(..), FinalEnv, T(..),
+               lookupEnv, updateEnv,
+               Unit(..),
+               Result(..), 
+
+             ) where
+ 
+import Prelude hiding (lookup)
+
+
+-- | 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 where
+ Zero  ::                      Ref a (env',a)
+ Suc   ::  Ref a      env' ->  Ref a (env',b)
+
+-- | The 'Equal' type encodes type equality. 
+data Equal :: * -> * -> * where 
+ 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)
+match  Zero     Zero        =  Just Eq
+match  (Suc x)  (Suc y)     =  match x y
+match  _        _           =  Nothing
+
+-- | 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
+lookup  Zero     (_,a)  =  a
+lookup  (Suc r)  (e,_)  =  lookup r e
+
+-- | 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  
+update f  Zero     (e,a)   =  (e,f a)
+update f  (Suc r)  (e,x)   =  (update f r e,x)
+
+
+-- | 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 where
+  Empty  ::  Env t use  ()
+  Ext    ::  Env t use def' ->  t a use  
+         ->  Env t use  (def',a)
+
+
+data Unit s         = Unit
+
+lookupEnv  :: Ref a env -> Env t s env -> t a s
+lookupEnv  Zero     (Ext _ t)   =  t
+lookupEnv  (Suc r)  (Ext ts _)  =  lookupEnv r ts
+lookupEnv  _        _           =  error "Error: The impossible happened!"
+
+updateEnv  ::  (t a s -> t a s) -> Ref a env 
+           ->  Env t s env ->  Env t s env
+updateEnv  f  Zero     (Ext ts t)  
+              =        Ext ts (f t) 
+updateEnv  f  (Suc r)  (Ext ts t)  
+              =        Ext (updateEnv f r ts)  t
+updateEnv  _  _        _ 
+              =  error "Error: The impossible happened!"
+
+
+-- | 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 '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   
+   =  forall s . Result  (m s) (b s) (FinalEnv t s)
+
+
+
+-- | 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 {unT :: forall x . Ref x e -> Ref x s}
+

@@ -0,0 +1,246 @@+{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs  #-}
+
+
+{-| 
+    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.TTTAS2 (
+               -- * Typed References and Environments
+               module Language.AbstractSyntax.TTTAS.Common,
+
+               -- * Transformation Library
+               
+               -- ** Trafo
+               Trafo(..), TrafoE(..),
+
+               -- ** Create New References
+               newSRef, 
+               extEnv, 
+               castSRef,
+               updateSRef,
+
+               -- ** State-like operations on the Final Environment
+               getFinalEnv, putFinalEnv, updateFinalEnv,
+ 
+               -- ** Run a Trafo
+               runTrafo,
+               
+               -- ** Arrow-style Combinators
+               Pair(..), Arrow2(..), ArrowLoop2(..),
+               (>>>),
+               List(..), sequenceA, returnA
+
+             ) where
+ 
+#if __GLASGOW_HASKELL__ >= 710
+import Prelude hiding (lookup, sequenceA) 
+#else
+import Prelude hiding (lookup) 
+#endif
+
+import Language.AbstractSyntax.TTTAS.Common
+
+
+
+
+-- | 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  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)
+                 )
+
+
+-- | 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'.
+runTrafo   ::  Trafo m t a b -> m () -> (forall s . a s) 
+           ->  Result m t b
+runTrafo trafo m a = 
+ case trafo of
+  Trafo trf -> case trf m of
+                   TrafoE m2 f -> 
+                      let  (rb, _, env2, fenv) =  f a (T id) Empty env2
+                      in   Result m2  rb fenv
+
+
+-- |  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.  
+newSRef :: Trafo Unit t (t a) (Ref a)
+newSRef 
+    =  Trafo 
+       (\Unit ->  TrafoE  
+                  Unit
+                  (\ta (T tr) env fenv ->
+                      ( tr Zero
+                      , T (tr . Suc)
+                      , Ext env ta
+                      , fenv
+       )          )   )
+
+
+-- | The function 'extEnv' returns a 'TrafoE' that extends the current environment.
+extEnv :: m (e,a) -> TrafoE m t  e (t a ) (Ref a )
+extEnv m = TrafoE m $ \ta  (T tr) env  fe ->  (tr Zero,  T (tr . Suc),  Ext env ta, fe )
+
+-- | 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  e x (Ref a)
+castSRef m r = TrafoE m $ (\   _ (T t) decls fe ->  (t r, T t, decls, fe))
+
+data FUpd i t a  = FUpd (forall s. i -> t a s -> t a s)
+newtype SI i s = SI i 
+
+-- | 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 -> FUpd i t a -> TrafoE m t e (SI i) (Ref a)
+updateSRef m r (FUpd f) = TrafoE m $ \(SI i) (T t) decls fs -> (t r, T t, updateEnv (f i) r decls, fs)
+
+
+newtype UpdFinalEnv t s = Upd (FinalEnv t s -> FinalEnv t s)
+
+newtype FinalEnv2 t s = Final (FinalEnv t s)
+
+-- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function
+--   (@(UpdFinalEnv t)@) to update the final environment.
+updateFinalEnv ::  Trafo m t (UpdFinalEnv t) Unit
+updateFinalEnv = Trafo $ \m -> (TrafoE m (\(Upd u) t e fe -> (Unit, t, e, u fe)))
+
+-- | Change the final environment by the one passed in the input.
+putFinalEnv ::  Trafo m t (FinalEnv2 t) Unit
+putFinalEnv =   Trafo $ \m -> (TrafoE m (\(Final fe) t e _ -> (Unit, t, e, fe)))
+
+-- | Return as output the final environment.
+getFinalEnv ::  Trafo m t Unit (FinalEnv2 t)
+getFinalEnv = Trafo $ \m -> (TrafoE m (\_ t e fe -> ((Final fe), t, e, fe)))
+
+{-
+-- | 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) ()
+updateFinalEnv = proc f ->
+                  do fe  <- getFinalEnv -< ()
+                     putFinalEnv -< f fe
+ -- Trafo $ \m -> (TrafoE m (\f t e fe -> ((), t, e, f fe)))
+-}
+
+newtype Pair a b s = P (a s, b s)
+
+class Category2 (cat :: (* -> *) -> (* -> *) -> *) where
+  id2     :: cat a a
+  (.:.)   :: cat b c -> cat a b -> cat a c
+
+class Category2 arr => Arrow2 (arr :: (* -> *) -> (* -> *) -> *) where
+  arr    :: (forall s . a s -> b s) -> arr a b
+  first  :: arr a b -> arr (Pair a c) (Pair b c)
+  second :: arr a b -> arr (Pair c a) (Pair c b)
+  (***)  :: arr a b -> arr a' b'
+          -> arr (Pair a a') (Pair b b')
+  (&&&)  :: arr a b -> arr a b' -> arr a (Pair b b')
+
+class Arrow2 arr => ArrowLoop2 arr where
+  loop   :: arr (Pair a c) (Pair b c) -> arr a b
+
+
+instance Category2 (Trafo m t) where
+  id2   =  Trafo  (\m -> TrafoE m (\a t e u -> (a, t, e, u)))
+
+  (.:.) (Trafo sb) (Trafo sa) = 
+    Trafo 
+    (\m1 ->
+       case sa m1 of 
+        TrafoE m2 f1 -> case sb m2 of 
+         TrafoE m3 f2 -> 
+           TrafoE  
+           m3 
+           (\a t3s e1 u1 -> let  (b, t1s, e2, u2) = f1 a t2s e1 u1
+                                 (c, t2s, e3, u3) = f2 b t3s e2 u2
+                            in   (c, t1s, e3, u3)
+           ))
+
+
+(>>>) :: Category2 cat => cat a b -> cat b c -> cat a c
+f >>> g = g .:. f
+
+ 
+instance Arrow2 (Trafo m t) where
+  arr  f 
+    =  Trafo  (\m -> TrafoE m (\a t e u -> (f a, t, e, u)) )
+
+  
+  first  (Trafo s) 
+    =  Trafo
+       (\m1 -> case s m1 of
+          TrafoE m2 f -> 
+             TrafoE  m2
+                    (\(P (a, c)) t2s e1 u1 -> 
+                                      let (b,t12,e2,u2) = f a t2s e1 u1 
+                                      in  (P (b, c),t12,e2,u2)
+                    )              
+       ) 
+
+  second  f = arr swap >>> first f >>> arr swap
+              where   swap :: Pair c a s -> Pair a c s
+                      swap ~(P (x, y)) = P (y, x)
+             
+  f ***  g =  first f >>> second g  
+ 
+  f &&&  g = arr (\b -> P (b, b)) >>> (f *** g)      
+
+
+instance ArrowLoop2 (Trafo m t) where
+  loop (Trafo st) =
+    Trafo 
+    (\m -> case st m of
+            TrafoE m1 f1 ->
+             TrafoE  m1
+             (\a t e u -> 
+               let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u                                           
+               in (b,t1,e1,u1)
+             ) 
+    )
+
+
+newtype List a s = List [a s]
+
+-- | The combinator 'sequenceA2' sequentially composes a list
+--   of 'Trafo2's into a 'Trafo2' that yields a 'List' of outputs.
+--   Its use is analogous to the combinator 'sequence' combinator
+--   for 'Monad's.
+sequenceA :: [Trafo m t a b] -> Trafo m t a (List b)
+sequenceA [] = arr (const (List []))
+sequenceA (x:xs) 
+       =  (x &&& sequenceA xs) >>> 
+          arr (\(P (a,List as)) -> List (a:as))
+
+returnA :: Arrow2 arr => arr a a
+returnA = arr id
+
+