diff --git a/benchmark-macro/Benchmark.hs b/benchmark-macro/Benchmark.hs
new file mode 100644
--- /dev/null
+++ b/benchmark-macro/Benchmark.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TypeOperators, DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell, GADTs #-}
+
+module Main where
+
+import Criterion.Main
+import Data.Comp.Derive
+import Data.Comp.DeepSeq ()
+import Data.Comp.Arbitrary ()
+import Data.Comp.Show ()
+import Data.Comp
+
+import qualified Functions.Mono as M
+import qualified DataTypes.Mono as M
+
+
+
+benchmarks :: String -> Term M.ArithLet -> String -> Term M.ArithExc -> Benchmark
+benchmarks n t n' t' = rnf t `seq` rnf t' `seq` getBench
+    where getBench = bgroup "" [letBench, excBench]
+          letBench = bgroup n
+                     [ inlineAnnBench
+                     , annInlineBench
+                     ]
+          excBench = bgroup n' 
+                     [ compAnnBench
+                     , annCompBench]
+          inlineAnnBench = bgroup "inlineAnn" 
+                           [ bench "fused" (nf M.inlineAnnFuse t) 
+                           , bench "seq" (nf M.inlineAnnSeq t)
+                           , bench "implicit, fused" (nf M.inlineAnnImpFuse t) 
+                           , bench "implicit, seq" (nf M.inlineAnnImpSeq t) ]
+          annInlineBench = bgroup "annInline" 
+                           [ bench "fused" (nf M.annInlineFuse t) 
+                           , bench "seq" (nf M.annInlineSeq t)
+                           , bench "implicit, fused)" (nf M.annInlineImpFuse t) 
+                           , bench "implicit, seq" (nf M.annInlineImpSeq t) ]
+          compAnnBench = bgroup "compAnn"
+                         [ bench "fused" (nf M.compAnnFuse t')
+                         , bench "seq" (nf M.compAnnSeq t')]
+          annCompBench = bgroup "annComp"
+                         [ bench "fused" (nf M.annCompFuse t')
+                         , bench "seq" (nf M.annCompSeq t')]
+
+genExpr :: Int -> IO Benchmark
+genExpr s = do
+  let t = M.exprAL s
+  let t' = M.exprAE s
+  putStr "size of the term: "
+  let termsize = size t
+  let termsize' = size t'
+  print termsize
+  putStr "size of the other term: "
+  print termsize'
+  return $ benchmarks ("term size="++ show termsize) t ("term size="++ show termsize') t'
+
+main = do b0 <- genExpr 11
+          b1 <- genExpr 8
+          b2 <- genExpr 4
+          defaultMain [b0, b1,b2]
diff --git a/benchmark/Benchmark.hs b/benchmark/Benchmark.hs
--- a/benchmark/Benchmark.hs
+++ b/benchmark/Benchmark.hs
@@ -138,7 +138,7 @@
 
 randStdBenchmarks :: Int -> IO Benchmark
 randStdBenchmarks s = do
-  rand <- getStdGen
+  rand <- newStdGen
   let ty = unGen arbitrary rand s
   putStr "size of the type term: "
   print $ size ty
diff --git a/benchmark/Functions/Comp/Desugar.hs b/benchmark/Functions/Comp/Desugar.hs
--- a/benchmark/Functions/Comp/Desugar.hs
+++ b/benchmark/Functions/Comp/Desugar.hs
@@ -60,7 +60,8 @@
 desug2 :: (Functor f, Desug2 f g) => Term f -> Term g
 desug2 = cata desugAlg2
 
-$(derive [liftSum] [''Desug2])
+instance (Desug2 f1 g, Desug2 f2 g) => Desug2 (f1 :+: f2) g where
+    desugAlg2 = caseF desugAlg2 desugAlg2
 
 instance (Value :<: v) => Desug2 Value v where
     desugAlg2 = inject
diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.6.1.4
+Version:		0.7
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -172,6 +172,7 @@
                         Data.Comp.Matching,
                         Data.Comp.Desugar,
                         Data.Comp.Automata,
+                        Data.Comp.MacroAutomata,
                         Data.Comp.Automata.Product,
                         Data.Comp.Number,
                         Data.Comp.Thunk,
@@ -286,6 +287,15 @@
   Type:                 exitcode-stdio-1.0
   Main-is:		Benchmark.hs
   hs-source-dirs:	src benchmark
+  ghc-options:          -W -O2
+  -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.
+  cpp-options:          -DNO_RULES
+  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers
+
+Benchmark macro
+  Type:                 exitcode-stdio-1.0
+  Main-is:		Benchmark.hs
+  hs-source-dirs:	src benchmark-macro
   ghc-options:          -W -O2
   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.
   cpp-options:          -DNO_RULES
diff --git a/src/Data/Comp/Annotation.hs b/src/Data/Comp/Annotation.hs
--- a/src/Data/Comp/Annotation.hs
+++ b/src/Data/Comp/Annotation.hs
@@ -3,7 +3,7 @@
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Annotation
--- Copyright   :  (c) 2010-2011 Patrick Bahr
+-- Copyright   :  (c) 2010-2013 Patrick Bahr
 -- License     :  BSD3
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
@@ -26,8 +26,11 @@
      propAnnQ,
      propAnnUp,
      propAnnDown,
+     propAnnMacro,
+     propAnnMacroLA,
      propAnnM,
      ann,
+     pathAnn,
      project'
     ) where
 
@@ -36,8 +39,12 @@
 import Data.Comp.Ops
 import Data.Comp.Algebra
 import Data.Comp.Automata
+import Data.Comp.MacroAutomata
 import Control.Monad
+import Data.Traversable
+import Data.Comp.Number
 
+
 {-| Transform a function with a domain constructed from a functor to a function
  with a domain constructed with the same functor, but with an additional
  annotation. -}
@@ -86,9 +93,28 @@
 -- with annotations.
 propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) 
         => DownTrans f q g -> DownTrans f' q g'
-propAnnDown trans (q, f') = ann p (trans (q, f))
+propAnnDown trans q f' = ann p (trans q f)
     where (f,p) = projectA f'
 
+-- | Lift a macro tree transducer over signatures @f@ and @g@ to a
+-- macro tree transducer over the same signatures, but extended
+-- with annotations.
+propAnnMacro :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) 
+        => MacroTrans f q g -> MacroTrans f' q g'
+propAnnMacro trans q f' = ann p (trans q (fmap ann' f))
+    where (f,p) = projectA f'
+          ann' s q' = s (fmap (ann p) q')
+
+-- | Lift a macro tree transducer with regular look-ahead over
+-- signatures @f@ and @g@ to a macro tree transducer with regular
+-- look-ahead over the same signatures, but extended with annotations.
+propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) 
+                => MacroTransLA f q p g -> MacroTransLA f' q p g'
+propAnnMacroLA trans q p f' = ann an (trans q p (fmap ann' f))
+    where (f,an) = projectA f'
+          ann' (s,p) = (\q' -> s (fmap (ann an) q'), p)
+
+
 {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic
   term homomorphism over the same signatures, but extended with annotations. -}
 propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m) 
@@ -100,9 +126,17 @@
 ann :: (DistAnn f p g, Functor f) => p -> CxtFun f g
 ann c = appSigFun (injectA c)
 
+
+-- | This function adds unique annotations to a term/context. Each
+-- node in the term/context is annotated with its path from the root,
+-- which is represented as an integer list. It is implemented as a
+-- DTT.
+pathAnn :: forall g. (Traversable g) => CxtFun g (g :&: [Int])
+pathAnn = runDownTrans trans [] where
+    trans :: DownTrans g [Int] (g :&: [Int])
+    trans q t = simpCxt (fmap (\ (Numbered (n,s)) -> s (n:q)) (number t) :&: q)
+
 {-| This function is similar to 'project' but applies to signatures
 with an annotation which is then ignored. -}
--- bug in type checker? below is the inferred type, however, the type checker
--- rejects it.
 project' :: forall f g f1 a h . (RemA f g, f :<: f1) => Cxt h f1 a -> Maybe (g (Cxt h f1 a))
 project' v = liftM remA (project v :: Maybe (f (Cxt h f1 a)))
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -45,6 +45,8 @@
     , runQHom
     -- * Deterministic Bottom-Up Tree Transducers
     , UpTrans
+    , UpTrans'
+    , mkUpTrans
     , runUpTrans
     , compUpTrans
     , compUpTransHom
@@ -67,6 +69,8 @@
     , (<*>)
     -- * Deterministic Top-Down Tree Transducers
     , DownTrans
+    , DownTrans'
+    , mkDownTrans
     , runDownTrans
     , compDownTrans
     , compDownTransSig
@@ -157,18 +161,31 @@
                      ?below = const undefined
                  in phom t
 
--- | This type represents transition functions of deterministic
--- bottom-up tree transducers (DUTTs).
+-- | This type represents transition functions of total, deterministic
+-- bottom-up tree transducers (UTTs).
 
 type UpTrans f q g = forall a. f (q,a) -> (q, Context g a)
 
--- | This function transforms a DUTT transition function into an
+
+-- | This is a variant of the 'UpTrans' type that makes it easier to
+-- define UTTs as it avoids the explicit use of 'Hole' to inject
+-- placeholders into the result.
+
+type UpTrans' f q g = forall a. f (q,Context g a) -> (q, Context g a)
+
+-- | This function turns a UTT defined using the type 'UpTrans'' in
+-- to the canonical form of type 'UpTrans'.
+
+mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g
+mkUpTrans tr t = tr $ fmap (\(q,a) -> (q, Hole a)) t
+
+-- | This function transforms a UTT transition function into an
 -- algebra.
 
 upAlg :: (Functor g)  => UpTrans f q g -> Alg f (q, Term g)
 upAlg trans = fmap appCxt . trans 
 
--- | This function runs the given DUTT on the given term.
+-- | This function runs the given UTT on the given term.
 
 runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g
 runUpTrans trans = snd . runUpTransSt trans
@@ -187,7 +204,7 @@
     run (Hole (q,a)) = (q, Hole a)
     run (Term t) = fmap appCxt $ trans $ fmap run t
 
--- | This function composes two DUTTs. (see TATA, Theorem 6.4.5)
+-- | This function composes two UTTs. (see TATA, Theorem 6.4.5)
     
 compUpTrans :: (Functor f, Functor g, Functor h)
                => UpTrans g p h -> UpTrans f q g -> UpTrans f (q,p) h
@@ -196,52 +213,52 @@
     (q2, c2) = runUpTrans' t2 c1
 
 
--- | This function composes a DUTT with an algebra.
+-- | This function composes a UTT with an algebra.
     
 compAlgUpTrans :: (Functor g)
                => Alg g a -> UpTrans f q g -> Alg f (q,a)
 compAlgUpTrans alg trans = fmap (cata' alg) . trans
 
 
--- | This combinator composes a DUTT followed by a signature function.
+-- | This combinator composes a UTT followed by a signature function.
 
 compSigUpTrans :: (Functor g) => SigFun g h -> UpTrans f q g -> UpTrans f q h
 compSigUpTrans sig trans x = (q, appSigFun sig x') where
     (q, x') = trans x
 
--- | This combinator composes a signature function followed by a DUTT.
+-- | This combinator composes a signature function followed by a UTT.
     
 compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h
 compUpTransSig trans sig = trans . sig
 
--- | This combinator composes a DUTT followed by a homomorphism.
+-- | This combinator composes a UTT followed by a homomorphism.
 
 compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h
 compHomUpTrans hom trans x = (q, appHom hom x') where
     (q, x') = trans x
 
--- | This combinator composes a homomorphism followed by a DUTT.
+-- | This combinator composes a homomorphism followed by a UTT.
     
 compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h
 compUpTransHom trans hom x  = runUpTrans' trans . hom $ x
 
--- | This type represents transition functions of deterministic
--- bottom-up tree acceptors (DUTAs).
+-- | This type represents transition functions of total, deterministic
+-- bottom-up tree acceptors (UTAs).
 
 type UpState f q = Alg f q
 
--- | Changes the state space of the DUTA using the given isomorphism.
+-- | Changes the state space of the UTA using the given isomorphism.
 
 tagUpState :: (Functor f) => (q -> p) -> (p -> q) -> UpState f q -> UpState f p
 tagUpState i o s = i . s . fmap o
 
--- | This combinator runs the given DUTA on a term returning the final
+-- | This combinator runs the given UTA on a term returning the final
 -- state of the run.
 
 runUpState :: (Functor f) => UpState f q -> Term f -> q
 runUpState = cata
 
--- | This function combines the product DUTA of the two given DUTAs.
+-- | This function combines the product UTA of the two given UTAs.
 
 prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p,q)
 prodUpState sp sq t = (p,q) where
@@ -249,8 +266,8 @@
     q = sq $ fmap snd t
 
 
--- | This function constructs a DUTT from a given stateful term
--- homomorphism with the state propagated by the given DUTA.
+-- | This function constructs a UTT from a given stateful term
+-- homomorphism with the state propagated by the given UTA.
     
 upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g
 upTrans st f t = (q, c)
@@ -258,7 +275,7 @@
           c = fmap snd $ explicit f q fst t
 
 -- | This function applies a given stateful term homomorphism with
--- a state space propagated by the given DUTA to a term.
+-- a state space propagated by the given UTA to a term.
           
 runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g
 runUpHom st hom = snd . runUpHomSt st hom
@@ -271,28 +288,28 @@
 
 
 -- | This type represents transition functions of generalised
--- deterministic bottom-up tree acceptors (GDUTAs) which have access
+-- deterministic bottom-up tree acceptors (GUTAs) which have access
 -- to an extended state space.
 
 type DUpState f p q = forall a . (?below :: a -> p, ?above :: p, q :< p) => f a -> q
 
--- | This combinator turns an arbitrary DUTA into a GDUTA.
+-- | This combinator turns an arbitrary UTA into a GUTA.
 
 dUpState :: Functor f => UpState f q -> DUpState f p q
 dUpState f = f . fmap below
 
--- | This combinator turns a GDUTA with the smallest possible state
--- space into a DUTA.
+-- | This combinator turns a GUTA with the smallest possible state
+-- space into a UTA.
 
 upState :: DUpState f q q -> UpState f q
 upState f s = res where res = explicit f res id s
 
--- | This combinator runs a GDUTA on a term.
+-- | This combinator runs a GUTA on a term.
                         
 runDUpState :: Functor f => DUpState f q q -> Term f -> q
 runDUpState = runUpState . upState
 
--- | This combinator constructs the product of two GDUTA.
+-- | This combinator constructs the product of two GUTA.
 
 prodDUpState :: (p :< c, q :< c)
              => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)
@@ -304,75 +321,88 @@
 
 
 
--- | This type represents transition functions of deterministic
--- top-down tree transducers (DDTTs).
+-- | This type represents transition functions of total deterministic
+-- top-down tree transducers (DTTs).
 
-type DownTrans f q g = forall a. (q, f a) -> Context g (q,a)
+type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a
 
--- | Thsis function runs the given DDTT on the given tree.
 
+-- | This is a variant of the 'DownTrans' type that makes it easier to
+-- define DTTs as it avoids the explicit use of 'Hole' to inject
+-- placeholders into the result.
+
+type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a
+
+-- | This function turns a DTT defined using the type 'DownTrans'' in
+-- to the canonical form of type 'DownTrans'.
+mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g
+mkDownTrans tr q t = tr q (fmap (Hole .) t)
+
+-- | Thsis function runs the given DTT on the given tree.
+
 runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a
-runDownTrans tr q t = run (q,t) where
-    run (q,Term t) = appCxt $ fmap run $  tr (q, t)
-    run (_,Hole a)      = Hole a
+runDownTrans tr q t = run t q where
+    run (Term t) q = appCxt $ tr q $ fmap run t
+    run (Hole a) _ = Hole a
 
--- | This function runs the given DDTT on the given tree.
+-- | This function runs the given DTT on the given tree.
     
-runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g (q,a)
-runDownTrans' tr q t = run (q,t) where
-    run (q,Term t) = appCxt $ fmap run $  tr (q, t)
-    run (q,Hole a)      = Hole (q,a)
+runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f (q -> a) -> Cxt h g a
+runDownTrans' tr q t = run t q where
+    run (Term t) q = appCxt $ tr q $ fmap run $ t
+    run (Hole a) q = Hole (a q)
 
--- | This function composes two DDTTs. (see Z. Fulop, H. Vogler
--- /Syntax-Directed Semantics/, Theorem 3.39)
+-- | This function composes two DTTs. (see W.C. Rounds /Mappings and
+-- grammars on trees/, Theorem 2.)
     
 compDownTrans :: (Functor f, Functor g, Functor h)
               => DownTrans g p h -> DownTrans f q g -> DownTrans f (q,p) h
-compDownTrans t2 t1 ((q,p), t) = fmap (\(p, (q, a)) -> ((q,p),a)) $ runDownTrans' t2 p (t1 (q, t))
+compDownTrans t2 t1 (q,p) t = runDownTrans' t2  p $ t1 q (fmap curry t)
 
 
--- | This function composes a signature function after a DDTT.
 
+-- | This function composes a signature function after a DTT.
+
 compSigDownTrans :: (Functor g) => SigFun g h -> DownTrans f q g -> DownTrans f q h
-compSigDownTrans sig trans = appSigFun sig . trans
+compSigDownTrans sig trans q = appSigFun sig . trans q
 
--- | This function composes a DDTT after a function.
+-- | This function composes a DTT after a function.
 
 compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h
-compDownTransSig trans hom (q,t) = trans (q, hom t)
+compDownTransSig trans hom q t = trans q (hom t)
 
 
--- | This function composes a homomorphism after a DDTT.
+-- | This function composes a homomorphism after a DTT.
 
 compHomDownTrans :: (Functor g, Functor h)
               => Hom g h -> DownTrans f q g -> DownTrans f q h
-compHomDownTrans hom trans = appHom hom . trans
+compHomDownTrans hom trans q = appHom hom . trans q
 
--- | This function composes a DDTT after a homomorphism.
+-- | This function composes a DTT after a homomorphism.
 
 compDownTransHom :: (Functor g, Functor h)
               => DownTrans g q h -> Hom f g -> DownTrans f q h
-compDownTransHom trans hom (q,t) = runDownTrans' trans q (hom t)
+compDownTransHom trans hom q t = runDownTrans' trans q (hom t)
 
 
--- | This type represents transition functions of deterministic
--- top-down tree acceptors (DDTAs).
+-- | This type represents transition functions of total, deterministic
+-- top-down tree acceptors (DTAs).
 
 type DownState f q = forall a. Ord a => (q, f a) -> Map a q
 
 
--- | Changes the state space of the DDTA using the given isomorphism.
+-- | Changes the state space of the DTA using the given isomorphism.
 
 tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p
 tagDownState i o t (q,s) = fmap i $ t (o q,s)
 
--- | This function constructs the product DDTA of the given two DDTAs.
+-- | This function constructs the product DTA of the given two DTAs.
 
 prodDownState :: DownState f p -> DownState f q -> DownState f (p,q)
 prodDownState sp sq ((p,q),t) = prodMap p q (sp (p, t)) (sq (q, t))
 
 
--- | This type is needed to construct the product of two DDTAs.
+-- | This type is needed to construct the product of two DTAs.
 
 data ProdState p q = LState p
                    | RState q
@@ -397,39 +427,40 @@
 -- otherwise adding the provided default state.
           
 appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
-                       -> q -> f b -> f (q,b)
+                       -> q -> f (q -> b) -> f (q,b)
 appMap qmap q s = fmap qfun s'
     where s' = number s
-          qfun k@(Numbered (_,a)) = (Map.findWithDefault q k (qmap s') ,a)
+          qfun k@(Numbered (_,a)) = let q' = Map.findWithDefault q k (qmap s')
+                                    in (q', a q') 
 
--- | This function constructs a DDTT from a given stateful term--
--- homomorphism with the state propagated by the given DDTA.
+-- | This function constructs a DTT from a given stateful term--
+-- homomorphism with the state propagated by the given DTA.
           
-downTrans :: Traversable f => DownState f q -> QHom f q g -> DownTrans f q g
-downTrans st f (q, s) = explicit f q fst (appMap (curry st q) q s)
+downTrans :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> DownTrans f q g
+downTrans st f q s = fmap snd $ explicit f q fst (appMap (curry st q) q s)
 
 
 -- | This function applies a given stateful term homomorphism with a
--- state space propagated by the given DDTA to a term.
+-- state space propagated by the given DTA to a term.
 
 runDownHom :: (Traversable f, Functor g)
             => DownState f q -> QHom f q g -> q -> Term f -> Term g
 runDownHom st h = runDownTrans (downTrans st h)
 
 -- | This type represents transition functions of generalised
--- deterministic top-down tree acceptors (GDDTAs) which have access
+-- deterministic top-down tree acceptors (GDTAs) which have access
 
 -- to an extended state space.
 type DDownState f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p, q :< p)
                                 => f i -> Map i q
 
--- | This combinator turns an arbitrary DDTA into a GDDTA.
+-- | This combinator turns an arbitrary DTA into a GDTA.
 
 dDownState :: DownState f q -> DDownState f p q
 dDownState f t = f (above,t)
 
--- | This combinator turns a GDDTA with the smallest possible state
--- space into a DDTA.
+-- | This combinator turns a GDTA with the smallest possible state
+-- space into a DTA.
 
 downState :: DDownState f q q -> DownState f q
 downState f (q,s) = res
diff --git a/src/Data/Comp/DeepSeq.hs b/src/Data/Comp/DeepSeq.hs
--- a/src/Data/Comp/DeepSeq.hs
+++ b/src/Data/Comp/DeepSeq.hs
@@ -16,24 +16,23 @@
 
 module Data.Comp.DeepSeq
     (
-     NFDataF(..),
-     rnfF'
+     NFDataF(..)
     )
     where
 
 import Data.Comp.Term
 import Control.DeepSeq
 import Data.Comp.Derive
-import Data.Foldable
-import Prelude hiding (foldr)
+import Data.Comp.Annotation
 
-{-| Fully evaluate a value over a foldable signature. -}
-rnfF' :: (Foldable f, NFDataF f, NFData a) => f a -> ()
-rnfF' x = foldr seq (rnfF x) x
 
 instance (NFDataF f, NFData a) => NFData (Cxt h f a) where
     rnf (Hole x) = rnf x
     rnf (Term x) = rnfF x
+
+instance (NFDataF f, NFData a) => NFDataF (f :&: a) where
+    rnfF (f :&: a) = rnfF f `seq` rnf a
+
 
 $(derive [liftSum] [''NFDataF])
 $(derive [makeNFDataF] [''Maybe, ''[], ''(,)])
diff --git a/src/Data/Comp/Derive/DeepSeq.hs b/src/Data/Comp/Derive/DeepSeq.hs
--- a/src/Data/Comp/Derive/DeepSeq.hs
+++ b/src/Data/Comp/Derive/DeepSeq.hs
@@ -22,7 +22,6 @@
 import Control.DeepSeq
 import Data.Comp.Derive.Utils
 import Language.Haskell.TH
-import Data.Maybe
 
 {-| Signature normal form. An instance @NFDataF f@ gives rise to an instance
   @NFData (Term f)@. -}
@@ -43,16 +42,11 @@
   rnfFDecl <- funD 'rnfF (rnfFClauses fArg constrs')
   return [InstanceD preCond classType [rnfFDecl]]
       where rnfFClauses fArg = map (genRnfFClause fArg)
-            filterFarg excl x
-                | excl = Nothing
-                | otherwise = Just $ varE x
-            mkPat True _ = WildP
-            mkPat False x = VarP x
             genRnfFClause fArg (constr, args) = do 
               let isFargs = map (==fArg) args
                   n = length args
               varNs <- newNames n "x"
-              let pat = ConP constr $ zipWith mkPat isFargs varNs
-                  allVars = catMaybes $ zipWith filterFarg isFargs varNs
+              let pat = ConP constr $ map VarP varNs
+                  allVars = map varE varNs 
               body <- foldr (\ x y -> [|rnf $x `seq` $y|]) [| () |] allVars
               return $ Clause [pat] (NormalB body) []
diff --git a/src/Data/Comp/Generic.hs b/src/Data/Comp/Generic.hs
--- a/src/Data/Comp/Generic.hs
+++ b/src/Data/Comp/Generic.hs
@@ -18,12 +18,39 @@
 
 import Data.Comp.Term
 import Data.Comp.Sum
+import Data.Comp.Algebra
+import Data.Comp.Automata
 import Data.Foldable
 import Data.Maybe
 import Data.Traversable
 import GHC.Exts
 import Control.Monad hiding (mapM)
 import Prelude hiding (foldl,mapM)
+
+
+-- | This function returns the subterm of a given term at the position
+-- specified by the given path or @Nothing@ if the input term has no
+-- such subterm
+
+getSubterm :: (Functor g, Foldable g) => [Int] -> Term g -> Maybe (Term g)
+getSubterm path t = cata alg t path where
+    alg :: (Functor g, Foldable g) => Alg g ([Int] -> Maybe (Cxt h g a))
+    alg t [] = Just $ Term $ fmap ((fromJust) . ($[])) t
+    alg t (i:is) = case drop i (toList t) of
+                     [] -> Nothing
+                     x : _ -> x is
+
+-- | This function returns the subterm of a given term at the position
+-- specified by the given path. This function is a variant of
+-- 'getSubterm' which fails if there is no subterm at the given
+-- position.
+
+getSubterm' :: (Functor g, Foldable g) => [Int] -> Term g -> Term g
+getSubterm' path t = runDownTrans trans path t where
+    trans :: (Functor g, Foldable g) => DownTrans g [Int] g
+    trans [] t = simpCxt $ fmap ($[]) t
+    trans (i : is) t = Hole $ (toList t !! i) is
+
 
 -- | This function returns a list of all subterms of the given
 -- term. This function is similar to Uniplate's @universe@ function.
diff --git a/src/Data/Comp/MacroAutomata.hs b/src/Data/Comp/MacroAutomata.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/MacroAutomata.hs
@@ -0,0 +1,196 @@
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.MacroAutomata
+-- Copyright   :  (c) 2013 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+-- 
+-- This module defines macro tree transducers (MTTs). It provides
+-- functions to run MTTs and to compose them with top down tree
+-- transducers. It also defines MTTs with regular look-ahead which
+-- combines MTTs with bottom-up tree acceptors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.MacroAutomata
+    (
+     -- * Macro Tree Transducers
+      MacroTrans
+    , MacroTrans'
+    , mkMacroTrans
+    , runMacroTrans
+    , compMacroDown
+    , compDownMacro
+    -- * Macro Tree Transducers with Singleton State Space
+    , MacroTransId
+    , MacroTransId'
+    , fromMacroTransId
+    , fromMacroTransId'
+    -- * Macro Tree Transducers with Regular Look-Ahead
+    , MacroTransLA
+    , MacroTransLA'
+    , mkMacroTransLA
+    , runMacroTransLA
+    , compDownMacroLA
+    -- * Macro Tree Transducers with Regular Look-Ahead
+    , (:^:) (..)
+    , I (..)
+    )
+    where
+
+import Data.Comp.Term
+import Data.Comp.Algebra
+import Data.Comp.Automata
+import Data.Comp.Ops
+import Data.Comp.Multi.HFunctor (I (..))
+
+-- | This type represents total deterministic macro tree transducers
+-- (MTTs).
+
+type MacroTrans f q g = forall a. q a -> f (q (Context g a) -> a) -> Context g a
+
+-- | This is a variant of the type 'MacroTrans' that makes it easier
+-- to define MTTs as it avoids the explicit use of 'Hole' when using
+-- placeholders in the result.
+
+type MacroTrans' f q g = forall a . q (Context g a) -> f (q (Context g a) -> Context g a)
+                       -> Context g a
+
+-- | This function turns an MTT defined using the more convenient type
+-- 'MacroTrans'' into its canonical form of type 'MacroTrans'.
+
+mkMacroTrans :: (Functor f, Functor q) => MacroTrans' f q g -> MacroTrans f q g
+mkMacroTrans tr q t = tr (fmap Hole q) (fmap (Hole .) t)
+
+-- | This function defines the semantics of MTTs. It applies a given
+-- MTT to an input with and an initial state.
+
+runMacroTrans :: (Functor g, Functor f, Functor q) => 
+                 MacroTrans f q g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a
+runMacroTrans tr q t = run t q where
+    run (Term t) q = appCxt (tr q (fmap run' t))
+    run (Hole a) _ = Hole a
+    run' t q = run t (fmap appCxt q)
+    
+
+-- This function is a variant of 'runMacroTrans' that is used to
+-- define composition. Restricted to 'Term's, both functions coincide.
+
+runMacroTrans' :: forall g f q h a. 
+                  (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a) 
+               -> Cxt h f (q (Cxt h g a) -> a) -> Cxt h g a
+runMacroTrans' tr q t = run t q where
+    run :: Cxt h f (q (Cxt h g a) -> a) -> q (Cxt h g a) -> Cxt h g a
+    run (Term t) q = appCxt (tr q (fmap run' t))
+    run (Hole a) q = Hole (a q)
+
+    run' :: Cxt h f (q (Cxt h g a) -> a) -> q (Context g (Cxt h g a)) -> Cxt h g a
+    run' t q = run t (fmap appCxt q)
+
+
+-- | This function composes a DTT followed by an MTT. The resulting
+-- MTT's semantics is equivalent to the function composition of the
+-- semantics of the original MTT and DTT.
+
+compMacroDown :: (Functor f, Functor g, Functor h, Functor p)
+              => MacroTrans g p h -> DownTrans f q g -> MacroTrans f (p :&: q) h
+compMacroDown t2 t1 (p :&: q) t = runMacroTrans' t2 (fmap Hole p) (t1 q (fmap curryF t))
+    where curryF :: ((p :&: q) a -> b) -> q -> p a -> b
+          curryF f q p = f (p :&: q)
+
+-- | This function is a variant of 'runDownTrans' that is used to
+-- define composition, similarly to the function 'runMacroTrans''.
+
+runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f (q -> a) -> Cxt h g a
+runDownTrans' tr q (Term t) = appCxt $ tr q $ fmap (\s q -> runDownTrans' tr q s) t
+runDownTrans' _ q (Hole a) = Hole (a q)
+
+-- | This type constructor is used to define the state space of an MTT
+-- that is obtained by composing an MTT followed by a DTT.
+
+data (q :^: p) a = q (p -> a) :^: p
+
+instance Functor q => Functor (q :^: p) where
+    fmap f (q :^: p) = fmap (f .) q :^: p
+
+-- | This function composes an MTT followed by a DTT. The resulting
+-- MTT's semantics is equivalent to first running the original MTT and
+-- then the DTT.
+
+compDownMacro :: forall f g h q p . (Functor f, Functor g, Functor h, Functor q)
+              => DownTrans g p h -> MacroTrans f q g -> MacroTrans f (q :^: p) h
+compDownMacro t2 t1 (q :^: p) t = runDownTrans' t2 p (t1 (fmap (\a p' -> a p') q) (fmap reshape t))
+    where reshape :: ((q :^: p) (Context h a) -> a) -> (q (Context g (p -> a)) -> p -> a)
+          reshape f q' p' = f (fmap (\s p'' -> runDownTrans' t2 p'' s) q' :^: p')
+
+
+-- | This type is an instantiation of the 'MacroTrans' type to a state
+-- space with only a single state with a single accumulation parameter
+-- (i.e. the state space is the identity functor).
+
+type MacroTransId  f g = forall a. a           -> f (Context g a -> a)           -> Context g a
+
+-- | This type is a variant of the 'MacroTransId' which is more
+-- convenient to work with as it avoids the explicit use of 'Hole' to
+-- embed placeholders into the result.
+type MacroTransId' f g = forall a. Context g a -> f (Context g a -> Context g a) -> Context g a
+
+
+-- | This function transforms an MTT of type |MacroTransId| into the
+-- canonical type such that it can be run.
+
+fromMacroTransId :: Functor f => MacroTransId f g -> MacroTrans f I g
+fromMacroTransId tr (I a) t = tr a (fmap (. I) t)
+
+
+-- | This function transforms an MTT of type |MacroTransId'| into the
+-- canonical type such that it can be run.
+
+fromMacroTransId' :: Functor f => MacroTransId' f g -> MacroTrans f I g
+fromMacroTransId' tr (I a) t = tr (Hole a) (fmap (\f -> Hole . f . I) t)
+
+-- | This type represents MTTs with regular look-ahead, i.e. MTTs that
+-- have access to information that is generated by a separate UTA.
+
+type MacroTransLA  f q p g = forall a. q a -> p -> f (q (Context g a) -> a, p) -> Context g a
+
+-- | This type is a more convenient variant of 'MacroTransLA' with
+-- which one can avoid using 'Hole' explicitly when injecting
+-- placeholders in the result.
+type MacroTransLA' f q p g = forall a. q (Context g a) -> p -> 
+                             f (q (Context g a) -> Context g a, p) -> Context g a
+
+
+-- | This function turns an MTT with regular look-ahead defined using
+-- the more convenient type |MacroTransLA'| into its canonical form of
+-- type |MacroTransLA|.
+mkMacroTransLA :: (Functor q, Functor f) => MacroTransLA' f q p g -> MacroTransLA f q p g
+mkMacroTransLA tr q p t = tr (fmap Hole q) p (fmap (\ (f, p) -> (Hole . f,p)) t)
+
+
+-- | This function defines the semantics of MTTs with regular
+-- look-ahead. It applies a given MTT with regular look-ahead
+-- (including an accompanying bottom-up state transition function) to
+-- an input with and an initial state.
+runMacroTransLA :: forall g f q p. (Functor g, Functor f, Functor q) => 
+                   UpState f p -> MacroTransLA f q p g -> q (Term g) -> Term f -> Term g
+runMacroTransLA st tr q t = fst (run t) q where
+    run :: Term f -> (q (Term g) -> Term g, p)
+    run (Term t) = let p = st $ fmap snd t'
+                       t' = fmap run' t
+                   in (\ q -> appCxt (tr q p t'), p)
+    run' :: Term f -> (q (Context g (Term g)) -> (Term g), p)
+    run' t = let (res, p) = run t
+             in  (res . fmap appCxt, p)
+
+-- | This function composes an MTT with regular look-ahead followed by
+-- a DTT.
+
+compDownMacroLA :: forall f g h q1 q2 p . (Functor f, Functor g, Functor h, Functor q1) =>
+                 DownTrans g q2 h -> MacroTransLA f q1 p g -> MacroTransLA f (q1 :^: q2) p h
+compDownMacroLA t2 t1 (q1 :^: q2) p t = runDownTrans' t2 q2 (t1 (fmap (\a q2' -> a q2') q1) p (fmap reshape t))
+    where reshape :: ((q1 :^: q2) (Context h a) -> a,p) -> (q1 (Context g (q2 -> a)) -> q2 -> a,p)
+          reshape (f,p) = (\q1' q2' -> f (fmap (\s q2'' -> runDownTrans' t2 q2'' s) q1' :^: q2'),p)
diff --git a/src/Data/Comp/Multi/HFunctor.hs b/src/Data/Comp/Multi/HFunctor.hs
--- a/src/Data/Comp/Multi/HFunctor.hs
+++ b/src/Data/Comp/Multi/HFunctor.hs
@@ -31,6 +31,9 @@
 -- | The identity Functor.
 newtype I a = I {unI :: a}
 
+instance Functor I where
+    fmap f (I x) = I (f x)
+
 -- | The parametrised constant functor.
 newtype K a i = K {unK :: a}