diff --git a/benchmark-macro/Benchmark.hs b/benchmark-macro/Benchmark.hs
deleted file mode 100644
--- a/benchmark-macro/Benchmark.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# 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/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.8.1.3
+Version:		0.9
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -69,23 +69,29 @@
      to families of mutually recursive data types and (more generally) GADTs.
      This extension resides in the module "Data.Comp.Multi".
   .
-  * Advanced recursion schemes derived from tree automata. These
-    recursion schemes allow for a higher degree of modularity and make
-    it possible to apply fusion. See /Modular Tree Automata/
-    (Mathematics of Program Construction, 263-299, 2012,
-    <http://dx.doi.org/10.1007/978-3-642-31113-0_14>) and 
-    /Programming Macro Tree Transducers/ (Workshop on Generic Programming, 61-72,
-    2013, <http://dx.doi.org/10.1145/2502488.2502489>).
-  .
 
   Examples of using (generalised) compositional data types are bundled
   with the package in the folder @examples@.
   .
-  Previous versions of this library contained a parametric variant of
-  compositional data types. This former part of the library has been
-  moved to a separate package: @compdata-param@
-  <https://hackage.haskell.org/package/compdata-param>
 
+  There are some supplementary packages, some of which were included
+  in previous versions of this package:
+  .
+  * @compdata-param@
+    <https://hackage.haskell.org/package/compdata-param>: a parametric
+    variant of compositional data types to deal with variable binders
+    in a systematic way.
+  .
+  * @compdata-automata@
+    <https://hackage.haskell.org/package/compdata-automata>: advanced
+    recursion schemes derived from tree automata that allow for a
+    higher degree of modularity and make it possible to apply fusion.
+  .
+  * @compdata-dags@
+    <https://hackage.haskell.org/package/compdata-dags>: recursion
+    schemes on directed acyclic graphs.
+
+
 Category:               Generics
 License:                BSD3
 License-file:           LICENSE
@@ -113,7 +119,6 @@
   benchmark/Multi/Functions/Comp/*.hs
   -- example files
   examples/Examples/*.hs
-  examples/Examples/Automata/*.hs
   examples/Examples/Multi/*.hs
 
 library
@@ -137,10 +142,7 @@
                         Data.Comp.Derive.Utils
                         Data.Comp.Matching
                         Data.Comp.Desugar
-                        Data.Comp.Automata
-                        Data.Comp.MacroAutomata
-                        Data.Comp.Automata.Product
-                        Data.Comp.Number
+                        Data.Comp.Mapping
                         Data.Comp.Thunk
                         Data.Comp.Ops
 
@@ -157,7 +159,7 @@
                         Data.Comp.Multi.Ordering
                         Data.Comp.Multi.Variables
                         Data.Comp.Multi.Ops
-                        Data.Comp.Multi.Number
+                        Data.Comp.Multi.Mapping
                         Data.Comp.Multi.Derive
                         Data.Comp.Multi.Generic
                         Data.Comp.Multi.Desugar
@@ -173,7 +175,6 @@
                         Data.Comp.Derive.Foldable
                         Data.Comp.Derive.Traversable
                         Data.Comp.Derive.HaskellStrict
-                        Data.Comp.Automata.Product.Derive
 
                         Data.Comp.Multi.Derive.HFunctor
                         Data.Comp.Multi.Derive.HFoldable
@@ -206,16 +207,6 @@
   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.
   cpp-options:          -DNO_RULES
   Build-Depends:        base >= 4.7, base < 5, 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
-  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive, 
-                        deepseq, criterion, random, uniplate, th-expand-syns, transformers
 
 
 source-repository head
diff --git a/examples/Examples/Automata.hs b/examples/Examples/Automata.hs
deleted file mode 100644
--- a/examples/Examples/Automata.hs
+++ /dev/null
@@ -1,147 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Automata
--- Copyright   :  (c) 2010-2011 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines tree automata based on compositional data types.
---
---------------------------------------------------------------------------------
-
-module Examples.Automata where
-
-import Data.Comp
-import Data.Maybe
-import Data.Traversable
-import Control.Monad
-
-
-{-| This type represents transition functions of deterministic
-bottom-up tree acceptors (DUTAs).  -}
-
-type DUTATrans f q = Alg f q
-
-{-| This data type represents deterministic bottom-up tree acceptors (DUTAs).
--}
-data DUTA f q = DUTA {
-      dutaTrans :: DUTATrans f q,
-      dutaAccept :: q -> Bool
-    }
-
-{-| This function runs the transition function of a DUTA on the given
-term. -}
-
-runDUTATrans :: Functor f => DUTATrans f q -> Term f -> q
-runDUTATrans = cata
-
-{-| This function checks whether a given DUTA accepts a term.  -}
-
-duta :: Functor f => DUTA f q -> Term f -> Bool
-duta DUTA{dutaTrans = trans, dutaAccept = accept} = accept . runDUTATrans trans
-
-
-
-{-| This type represents transition functions of non-deterministic
-bottom-up tree acceptors (NUTAs).  -}
-
-type NUTATrans f q = AlgM [] f q
-
-
-{-| This type represents non-deterministic bottom-up tree acceptors.
--}
-data NUTA f q = NUTA {
-      nutaTrans :: AlgM [] f q,
-      nutaAccept :: q -> Bool
-    }
-
-{-| This function runs the given transition function of a NUTA on the
-given term -}
-
-runNUTATrans :: Traversable f => NUTATrans f q -> Term f -> [q]
-runNUTATrans = cataM
-
-{-| This function checks whether a given NUTA accepts a term. -}
-
-nuta :: Traversable f => NUTA f q -> Term f -> Bool
-nuta NUTA{nutaTrans = trans, nutaAccept = accept} = any accept . runNUTATrans trans
-
-
-{-| This function determinises the given NUTA.  -}
-
-determNUTA :: (Traversable f) => NUTA f q -> DUTA f [q]
-determNUTA n = DUTA{
-               dutaTrans = algM $ nutaTrans n,
-               dutaAccept = any $ nutaAccept n}
-
-{-| This function represents transition functions of
-deterministic bottom-up tree transducers (DUTTs).  -}
-
-type DUTTTrans f g q = forall a. f (q,a) -> (q, Cxt Hole g a)
-
-{-| This function transforms a DUTT transition function into an
-algebra.  -}
-
-duttTransAlg :: (Functor f, Functor g)  => DUTTTrans f g q -> Alg f (q, Term g)
-duttTransAlg trans = fmap injectCxt . trans 
-
-{-| This function runs the given DUTT transition function on the given
-term.  -}
-
-runDUTTTrans :: (Functor f, Functor g)  => DUTTTrans f g q -> Term f -> (q, Term g)
-runDUTTTrans = cata . duttTransAlg
-
-{-| This data type represents deterministic bottom-up tree
-transducers. -}
-
-data DUTT f g q = DUTT {
-      duttTrans :: DUTTTrans f g q,
-      duttAccept :: q -> Bool
-    }
-
-{-| This function transforms the given term according to the given
-DUTT and returns the resulting term provided it is accepted by the
-DUTT. -}
-
-dutt :: (Functor f, Functor g) => DUTT f g q -> Term f -> Maybe (Term g)
-dutt DUTT{duttTrans = trans, duttAccept = accept} = accept' . runDUTTTrans trans
-    where accept' (q,res)
-              | accept q = Just res
-              | otherwise = Nothing
-
-{-| This type represents transition functions of non-deterministic
-bottom-up tree transducers (NUTTs).  -}
-
-type NUTTTrans f g q = forall a. f (q,a) -> [(q, Cxt Hole g a)]
-
-{-| This function transforms a NUTT transition function into a monadic
-algebra.  -}
-
-nuttTransAlg :: (Functor f, Functor g)  => NUTTTrans f g q -> AlgM [] f (q, Term g)
-nuttTransAlg trans = liftM (fmap injectCxt) . trans 
-
-{-| This function runs the given NUTT transition function on the given
-term.  -}
-
-runNUTTTrans :: (Traversable f, Functor g)  => NUTTTrans f g q -> Term f -> [(q, Term g)]
-runNUTTTrans = cataM . nuttTransAlg
-
-{-| This data type represents non-deterministic bottom-up tree
-transducers (NUTTs). -}
-
-data NUTT f g q = NUTT {
-      nuttTrans :: NUTTTrans f g q,
-      nuttAccept :: q -> Bool
-    }
-
-{-| This function transforms the given term according to the given
-NUTT and returns a list containing all accepted results. -}
-
-nutt :: (Traversable f, Functor g) => NUTT f g q -> Term f -> [Term g]
-nutt NUTT{nuttTrans = trans, nuttAccept = accept} = mapMaybe accept' . runNUTTTrans trans
-    where accept' (q,res)
-              | accept q = Just res
-              | otherwise = Nothing
diff --git a/examples/Examples/Automata/Compiler.hs b/examples/Examples/Automata/Compiler.hs
deleted file mode 100644
--- a/examples/Examples/Automata/Compiler.hs
+++ /dev/null
@@ -1,192 +0,0 @@
-{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,
-TypeOperators, FlexibleInstances, UndecidableInstances,
-ScopedTypeVariables, TypeSynonymInstances, GeneralizedNewtypeDeriving,
-OverlappingInstances, ConstraintKinds #-}
-
-module Examples.Automata.Compiler where
-
-import Data.Comp.Automata
-import Data.Comp.Derive
-import Data.Comp.Ops
-import Data.Comp hiding (height)
-import Data.Foldable
-import Prelude hiding (foldl)
-
-import Data.Set (Set, union, singleton, delete, member)
-import qualified Data.Set as Set
-
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-type Var = String
-
-data Val a = Const Int
-data Op a  = Plus a a
-           | Times a a
-type Core = Op :+: Val
-data Let a = Let Var a a
-           | Var Var
-
-type CoreLet = Let :+: Core
-
-data Sugar a = Neg a
-             | Minus a a
-
-$(derive [makeFunctor, makeFoldable, makeTraversable, smartConstructors, makeShowF]
-  [''Val, ''Op, ''Let, ''Sugar])
-
-
-class Eval f where
-    evalSt :: UpState f Int
-
-$(derive [liftSum] [''Eval])
-
-instance Eval Val where
-    evalSt (Const i) = i
-
-instance Eval Op where
-    evalSt (Plus x y) = x + y
-    evalSt (Times x y) = x * y
-
-type Addr = Int
-
-data Instr = Acc Int
-           | Load Addr
-           | Store Addr
-           | Add Int
-           | Sub Int
-           | Mul Int
-             deriving (Show)
-
-type Code = [Instr]
-
-data MState = MState {
-      mRam :: Map Addr Int,
-      mAcc :: Int }
-
-runCode :: Code -> MState -> MState
-runCode [] = id
-runCode (ins:c) = runCode c . step ins 
-    where step (Acc i) s = s{mAcc = i}
-          step (Load a) s = case Map.lookup a (mRam s) of
-              Nothing -> error $ "memory cell " ++ show a ++ " is not set"
-              Just n -> s {mAcc = n}
-          step (Store a) s = s {mRam = Map.insert a (mAcc s) (mRam s)}
-          step (Add a) s = exec (+) a s
-          step (Sub a) s = exec (-) a s
-          step (Mul a) s = exec (*) a s
-          exec op a s = case Map.lookup a (mRam s) of
-                        Nothing -> error $ "memory cell " ++ show a ++ " is not set"
-                        Just n -> s {mAcc = mAcc s `op` n}
-
-
-runCode' :: Code -> Int
-runCode' c = mAcc $ runCode c MState{mRam = Map.empty, mAcc = error "accumulator is not set"}
-
-
--- | Defines the height of an expression.
-heightSt :: Foldable f => UpState f Int
-heightSt t = foldl max 0 t + 1
-
-tmpAddrSt :: Foldable f => UpState f Int
-tmpAddrSt = (+1) . heightSt
-
-
-newtype VarAddr = VarAddr {varAddr :: Int} deriving (Eq, Show, Num)
-
-class VarAddrSt f where
-  varAddrSt :: DownState f VarAddr
-  
-instance (VarAddrSt f, VarAddrSt g) => VarAddrSt (f :+: g) where
-    varAddrSt (q,Inl x) = varAddrSt (q, x)
-    varAddrSt (q,Inr x) = varAddrSt (q, x)
-
-instance VarAddrSt Let where
-  varAddrSt (d, Let _ _ x) = x `Map.singleton` (d + 2)
-  varAddrSt _ = Map.empty
-  
-instance VarAddrSt f where
-  varAddrSt _ = Map.empty
-
-
-type Bind = Map Var Int
-
-bindSt :: (Let :<: f,VarAddr :< q) => DDownState f q Bind
-bindSt t = case proj t of
-             Just (Let v _ e) -> Map.singleton e q'
-                       where q' = Map.insert v (varAddr above) above
-             _ -> Map.empty
-
--- | Defines the code that an expression is compiled to. It depends on
--- an integer state that denotes the height of the current node.
-class CodeSt f q where
-    codeSt :: DUpState f q Code
-
-instance (CodeSt f q, CodeSt g q) => CodeSt (f :+: g) q where
-    codeSt (Inl x) = codeSt x
-    codeSt (Inr x) = codeSt x
-  
-
-instance CodeSt Val q where
-    codeSt (Const i) = [Acc i]
-
-instance (Int :< q) => CodeSt Op q where
-    codeSt (Plus x y) = below x ++ [Store i] ++ below y ++ [Add i]
-        where i = below y
-    codeSt (Times x y) = below x ++ [Store i] ++ below y ++ [Mul i]
-        where i = below y
-
-instance (VarAddr :< q, Bind :< q) => CodeSt Let q where
-    codeSt (Let _ b e) = below b ++ [Store i] ++ below e
-                    where i = varAddr above
-    codeSt (Var v) = case Map.lookup v above of
-                       Nothing -> error $ "unbound variable " ++ v
-                       Just i -> [Load i]
-
-compile' :: (CodeSt f (Code,Int), Foldable f, Functor f) => Term f -> Code
-compile' = fst . runDUpState (codeSt `prodDUpState` dUpState tmpAddrSt)
-
-
-exComp' = compile' (iConst 2 `iPlus` iConst 3 :: Term Core)
-
-
-
-compile :: (CodeSt f ((Code,Int),(Bind,VarAddr)), Traversable f, Functor f, Let :<: f, VarAddrSt f)
-           => Term f -> Code
-compile = fst . runDState 
-          (codeSt `prodDUpState` dUpState tmpAddrSt)
-          (bindSt `prodDDownState` dDownState varAddrSt)
-          (Map.empty, VarAddr 1)
-          
-
-exComp = compile (iLet "x" (iLet "x" (iConst 5) (iConst 10 `iPlus` iVar "x")) (iConst 2 `iPlus` iVar "x") :: Term CoreLet)
-
--- | Defines the set of free variables
-class VarsSt f where
-    varsSt :: UpState f (Set Var)
-
-$(derive [liftSum] [''VarsSt])
-
-instance VarsSt Val where
-    varsSt _ = Set.empty
-
-instance VarsSt Op where
-    varsSt (Plus x y) = x `union` y
-    varsSt (Times x y) = x `union` y
-
-instance VarsSt Let where
-    varsSt (Var v) = singleton v
-    varsSt (Let v x y) = (if v `member` y then x else Set.empty) `union` delete v y
-
--- | Stateful homomorphism that removes unnecessary let bindings.
-remLetHom :: (Set Var :< q, Let :<: f, Functor f) => QHom f q f
-remLetHom t = case proj t of
-                Just (Let v _ y) 
-                    | not (v `member` below y) -> Hole y
-                _ -> simpCxt t
-
--- | Removes unnecessary let bindings.
-remLet :: (Let :<: f, Functor f, VarsSt f) => Term f -> Term f
-remLet = runUpHom varsSt remLetHom
-
-exLet = remLet (iLet "x" (iConst 3) (iConst 2 `iPlus` iVar "y") :: Term CoreLet)
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
@@ -30,22 +30,13 @@
      liftA',
      stripA,
      propAnn,
-     propAnnQ,
-     propAnnUp,
-     propAnnDown,
-     propAnnMacro,
-     propAnnMacroLA,
      propAnnM,
      ann,
-     pathAnn,
      project'
     ) where
 
 import Control.Monad
 import Data.Comp.Algebra
-import Data.Comp.Automata
-import Data.Comp.MacroAutomata
-import Data.Comp.Number
 import Data.Comp.Ops
 import Data.Comp.Term
 
@@ -76,50 +67,6 @@
     where (f,p) = projectA f'
 
 
--- | Lift a stateful term homomorphism over signatures @f@ and @g@ to
--- a stateful term homomorphism over the same signatures, but extended with
--- annotations.
-propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g)
-        => QHom f q g -> QHom f' q g'
-propAnnQ hom f' = ann p (hom f)
-    where (f,p) = projectA f'
-
--- | Lift a bottom-up tree transducer over signatures @f@ and @g@ to a
--- bottom-up tree transducer over the same signatures, but extended
--- with annotations.
-propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g)
-        => UpTrans f q g -> UpTrans f' q g'
-propAnnUp trans f' = (q, ann p t)
-    where (f,p) = projectA f'
-          (q,t) = trans f
-
--- | Lift a top-down tree transducer over signatures @f@ and @g@ to a
--- top-down tree transducer over the same signatures, but extended
--- 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)
-    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) = (s . fmap (ann an), 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)
@@ -131,15 +78,6 @@
 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. -}
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
deleted file mode 100644
--- a/src/Data/Comp/Automata.hs
+++ /dev/null
@@ -1,521 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs            #-}
-{-# LANGUAGE ImplicitParams   #-}
-{-# LANGUAGE Rank2Types       #-}
-{-# LANGUAGE TypeOperators    #-}
-
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Automata
--- Copyright   :  (c) 2010-2012 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines stateful term homomorphisms. This (slightly
--- oxymoronic) notion extends per se stateless term homomorphisms with
--- a state that is maintained separately by a bottom-up or top-down
--- state transformation. Additionally, this module also provides
--- combinators to run state transformations themselves.
---
--- Like regular term homomorphisms also stateful homomorphisms (as
--- well as transducers) can be lifted to annotated signatures
--- (cf. "Data.Comp.Annotation").
---
--- The recursion schemes provided in this module are derived from tree
--- automata. They allow for a higher degree of modularity and make it
--- possible to apply fusion. The implementation is based on the paper
--- /Modular Tree Automata/ (Mathematics of Program Construction,
--- 263-299, 2012, <http://dx.doi.org/10.1007/978-3-642-31113-0_14>).
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Automata
-    (
-    -- * Stateful Term Homomorphisms
-      QHom
-    , below
-    , above
-    , pureHom
-    -- ** Bottom-Up State Propagation
-    , upTrans
-    , runUpHom
-    , runUpHomSt
-    -- ** Top-Down State Propagation
-    , downTrans
-    , runDownHom
-    -- ** Bidirectional State Propagation
-    , runQHom
-    -- * Deterministic Bottom-Up Tree Transducers
-    , UpTrans
-    , UpTrans'
-    , mkUpTrans
-    , runUpTrans
-    , compUpTrans
-    , compUpTransHom
-    , compHomUpTrans
-    , compUpTransSig
-    , compSigUpTrans
-    , compAlgUpTrans
-    -- * Deterministic Bottom-Up Tree State Transformations
-    -- ** Monolithic State
-    , UpState
-    , tagUpState
-    , runUpState
-    , prodUpState
-    -- ** Modular State
-    , DUpState
-    , dUpState
-    , upState
-    , runDUpState
-    , prodDUpState
-    , (|*|)
-    -- * Deterministic Top-Down Tree Transducers
-    , DownTrans
-    , DownTrans'
-    , mkDownTrans
-    , runDownTrans
-    , compDownTrans
-    , compDownTransSig
-    , compSigDownTrans
-    , compDownTransHom
-    , compHomDownTrans
-    -- * Deterministic Top-Down Tree State Transformations
-    -- ** Monolithic State
-    , DownState
-    , tagDownState
-    , prodDownState
-    -- ** Modular State
-    , DDownState
-    , dDownState
-    , downState
-    , prodDDownState
-    , (>*<)
-    -- * Bidirectional Tree State Transformations
-    , runDState
-    -- * Operators for Finite Mappings
-    , (&)
-    , (|->)
-    , o
-    -- * Product State Spaces
-    , module Data.Comp.Automata.Product
-    ) where
-
-import Data.Comp.Algebra
-import Data.Comp.Automata.Product
-import Data.Comp.Number
-import Data.Comp.Term
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-
-
--- The following are operators to specify finite mappings.
-
-
-infix 1 |->
-infixr 0 &
-
--- | left-biased union of two mappings.
-
-(&) :: Ord k => Map k v -> Map k v -> Map k v
-(&) = Map.union
-
--- | This operator constructs a singleton mapping.
-
-(|->) :: k -> a -> Map k a
-(|->) = Map.singleton
-
--- | This is the empty mapping.
-
-o :: Map k a
-o = Map.empty
-
--- | This function provides access to components of the states from
--- "below".
-
-below :: (?below :: a -> q, p :< q) => a -> p
-below = pr . ?below
-
--- | This function provides access to components of the state from
--- "above"
-
-above :: (?above :: q, p :< q) => p
-above = pr ?above
-
--- | Turns the explicit parameters @?above@ and @?below@ into explicit
--- ones.
-
-explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b
-explicit x ab be = x where ?above = ab; ?below = be
-
-
--- | This type represents stateful term homomorphisms. Stateful term
--- homomorphisms have access to a state that is provided (separately)
--- by a bottom-up or top-down state transformation function (or both).
-
-type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
-
-
--- | This function turns a stateful homomorphism with a fully
--- polymorphic state type into a (stateless) homomorphism.
-pureHom :: (forall q . QHom f q g) -> Hom f g
-pureHom phom t = let ?above = undefined
-                     ?below = const undefined
-                 in phom t
-
--- | 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 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 UTT on the given term.
-
-runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g
-runUpTrans trans = snd . runUpTransSt trans
-
--- | This function is a variant of 'runUpTrans' that additionally
--- returns the final state of the run.
-
-runUpTransSt :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g)
-runUpTransSt = cata . upAlg
-
--- | This function generalises 'runUpTrans' to contexts. Therefore,
--- additionally, a transition function for the holes is needed.
-
-runUpTrans' :: (Functor f, Functor g) => UpTrans f q g -> Context f (q,a) -> (q, Context g a)
-runUpTrans' trans = run where
-    run (Hole (q,a)) = (q, Hole a)
-    run (Term t) = fmap appCxt $ trans $ fmap run t
-
--- | 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
-compUpTrans t2 t1 x = ((q1,q2), c2) where
-    (q1, c1) = t1 $ fmap (\((q1,q2),a) -> (q1,(q2,a))) x
-    (q2, c2) = runUpTrans' t2 c1
-
-
--- | 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 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 UTT.
-
-compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h
-compUpTransSig trans sig = trans . sig
-
--- | 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 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 total, deterministic
--- bottom-up tree acceptors (UTAs).
-
-type UpState f q = Alg f q
-
--- | 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 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 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
-    p = sp $ fmap fst t
-    q = sq $ fmap snd t
-
-
--- | 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)
-    where q = st $ fmap fst t
-          c = fmap snd $ explicit f q fst t
-
--- | This function applies a given stateful term homomorphism with
--- 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
-
--- | This is a variant of 'runUpHom' that also returns the final state
--- of the run.
-
-runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)
-runUpHomSt alg h = runUpTransSt (upTrans alg h)
-
-
--- | This type represents transition functions of generalised
--- deterministic bottom-up tree acceptors (GUTAs) which have access
--- to an extended state space.
-
-type DUpState f p q = (q :< p) => DUpState' f p q
-type DUpState' f p q = forall a . (?below :: a -> p, ?above :: p) => f a -> q
-
--- | 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 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 GUTA on a term.
-
-runDUpState :: Functor f => DUpState f q q -> Term f -> q
-runDUpState = runUpState . upState
-
--- | 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)
-prodDUpState sp sq t = (sp t, sq t)
-
-(|*|) :: (p :< c, q :< c)
-             => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)
-(|*|) = prodDUpState
-
-
-
--- | This type represents transition functions of total deterministic
--- top-down tree transducers (DTTs).
-
-type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a
-
-
--- | 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 t q where
-    run (Term t) q = appCxt $ tr q $ fmap run t
-    run (Hole a) _ = Hole a
-
--- | This function runs the given DTT on the given tree.
-
-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 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 = runDownTrans' t2  p $ t1 q (fmap curry t)
-
-
-
--- | 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 q = appSigFun sig . trans q
-
--- | 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)
-
-
--- | 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 q = appHom hom . trans q
-
--- | 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)
-
-
--- | 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 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 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 DTAs.
-
-data ProdState p q = LState p
-                   | RState q
-                   | BState p q
--- | This function constructs the pointwise product of two maps each
--- with a default value.
-
-prodMap :: (Ord i) => p -> q -> Map i p -> Map i q -> Map i (p,q)
-prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs
-    where ps = Map.map LState mp
-          qs = Map.map RState mq
-          combine (LState p) (RState q) = BState p q
-          combine (RState q) (LState p) = BState p q
-          combine _ _                   = error "unexpected merging"
-          final (LState p) = (p, q)
-          final (RState q) = (p, q)
-          final (BState p q) = (p,q)
-
-
--- | Apply the given state mapping to the given functorial value by
--- adding the state to the corresponding index if it is in the map and
--- otherwise adding the provided default state.
-
-appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
-                       -> q -> f (q -> b) -> f (q,b)
-appMap qmap q s = fmap qfun s'
-    where s' = number s
-          qfun k@(Numbered (_,a)) = let q' = Map.findWithDefault q k (qmap s')
-                                    in (q', a q')
-
--- | This function constructs a DTT from a given stateful term--
--- homomorphism with the state propagated by the given DTA.
-
-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 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 (GDTAs) which have access
-
--- to an extended state space.
-type DDownState f p q = (q :< p) => DDownState' f p q
-
-type DDownState' f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p)
-                                => f i -> Map i q
-
--- | 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 GDTA with the smallest possible state
--- space into a DTA.
-
-downState :: DDownState f q q -> DownState f q
-downState f (q,s) = res
-    where res = explicit f q bel s
-          bel k = Map.findWithDefault q k res
-
-
--- | This combinator constructs the product of two dependant top-down
--- state transformations.
-
-prodDDownState :: (p :< c, q :< c)
-               => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
-prodDDownState sp sq t = prodMap above above (sp t) (sq t)
-
--- | This is a synonym for 'prodDDownState'.
-
-(>*<) :: (p :< c, q :< c, Functor f)
-         => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
-(>*<) = prodDDownState
-
-
--- | This combinator combines a bottom-up and a top-down state
--- transformations. Both state transformations can depend mutually
--- recursive on each other.
-
-runDState :: Traversable f => DUpState' f (u,d) u -> DDownState' f (u,d) d -> d -> Term f -> u
-runDState up down d (Term t) = u where
-        t' = fmap bel $ number t
-        bel (Numbered (i,s)) =
-            let d' = Map.findWithDefault d (Numbered (i,undefined)) m
-            in Numbered (i, (runDState up down d' s, d'))
-        m = explicit down (u,d) unNumbered t'
-        u = explicit up (u,d) unNumbered t'
-
--- | This combinator runs a stateful term homomorphisms with a state
--- space produced both on a bottom-up and a top-down state
--- transformation.
-
-runQHom :: (Traversable f, Functor g) =>
-           DUpState' f (u,d) u -> DDownState' f (u,d) d ->
-           QHom f (u,d) g ->
-           d -> Term f -> (u, Term g)
-runQHom up down trans d (Term t) = (u,t'') where
-        t' = fmap bel $ number t
-        bel (Numbered (i,s)) =
-            let d' = Map.findWithDefault d (Numbered (i,undefined)) m
-                (u', s') = runQHom up down trans d' s
-            in Numbered (i, ((u', d'),s'))
-        m = explicit down (u,d) (fst . unNumbered) t'
-        u = explicit up (u,d) (fst . unNumbered) t'
-        t'' = appCxt $ fmap (snd . unNumbered) $  explicit trans (u,d) (fst . unNumbered) t'
diff --git a/src/Data/Comp/Automata/Product.hs b/src/Data/Comp/Automata/Product.hs
deleted file mode 100644
--- a/src/Data/Comp/Automata/Product.hs
+++ /dev/null
@@ -1,62 +0,0 @@
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE UndecidableInstances  #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Automata.Product
--- Copyright   :  (c) 2014 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Automata.Product ((:<), pr) where
-
-
-
-data Pos = Here | Le Pos | Ri Pos
-
-data Res = NotFound | Ambiguous | Found Pos
-
-type family Ch (l :: Res) (r :: Res) :: Res where
-    Ch (Found x) (Found y) = Ambiguous
-    Ch Ambiguous y = Ambiguous
-    Ch x Ambiguous = Ambiguous
-    Ch (Found x) y = Found (Le x)
-    Ch x (Found y) = Found (Ri y)
-    Ch x y = NotFound
-
-type family Elem (e :: *) (p :: *) :: Res where
-    Elem e e = Found Here
-    Elem e (l,r) = Ch (Elem e l) (Elem e r)
-    Elem e p = NotFound
-
-data Proxy a = P
-
-class IsElem (res :: Res) e p where
-    pr' :: Proxy res -> p -> e
-
-instance IsElem (Found Here) e e where
-    pr' _ = id
-
-instance IsElem (Found pos) e p => IsElem (Found (Le pos)) e (p, p') where
-    pr' _ (x,_) = pr' (P :: Proxy (Found pos)) x
-
-instance IsElem (Found pos) e p => IsElem (Found (Ri pos)) e (p', p) where
-    pr' _ (_,y) = pr' (P :: Proxy (Found pos)) y
-
-
-type (e :< p) = IsElem (Elem e p) e p
-
-pr :: forall e p . (e :< p) => p -> e
-pr = pr' (P :: Proxy (Elem e p))
diff --git a/src/Data/Comp/Automata/Product/Derive.hs b/src/Data/Comp/Automata/Product/Derive.hs
deleted file mode 100644
--- a/src/Data/Comp/Automata/Product/Derive.hs
+++ /dev/null
@@ -1,75 +0,0 @@
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeOperators         #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Automata.Product.Derive
--- Copyright   :  (c) 2011 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Automata.Product.Derive where
-
-import Language.Haskell.TH
-
--- | An instance @a :< b@ means that @a@ is a component of @b@. @a@
--- can be extracted from @b@ via the method 'pr'.
-class a :< b where
-    pr :: b -> a
-
-data Dir = L | R
-         deriving Show
-
-genAllInsts :: Int -> Q [Dec]
-genAllInsts n = mapM genInst dirs
-    where dirs = map (L:) (genDirs n)
-
-genDirs :: Int -> [[Dir]]
-genDirs 0 = [[]]
-genDirs n = [] : map (L:) dirs ++ map (R:) dirs
-    where dirs = genDirs (n-1)
-
-genInst :: [Dir] -> Q Dec
-genInst dir = do
-  n <- newName "a"
-  ty <- genType n dir
-  ex <- genEx dir
-  return $ InstanceD [] (ConT (mkName ":<") `AppT` VarT n `AppT` ty) [ex]
-
-genType :: Name -> [Dir] -> Q Type
-genType n = gen
-    where gen [] = varT n
-          gen (L:dir) =  gen dir `pairT` (varT =<< newName "a")
-          gen (R:dir) =  (varT =<< newName "a") `pairT` gen dir
-
-genPat :: Name -> [Dir] -> PatQ
-genPat n = gen where
-    gen [] = varP n
-    gen (L:dir) = tupP [gen dir,wildP]
-    gen (R:dir) = tupP [wildP,gen dir]
-
-genEx :: [Dir] -> DecQ
-genEx dir = do
-  n <- newName "x"
-  p <- genPat n dir
-  return $ FunD (mkName "pr") [Clause [p] (NormalB (VarE n)) []]
-
-genPatExp :: Name -> [Dir] -> Q (Pat, Exp)
-genPatExp n = gen where
-    gen [] = return (WildP, VarE n)
-    gen (d:dir) = do
-      (p,e) <- gen dir
-      x <- newName "x"
-      return $ case d of
-        L -> (TupP [p,VarP x] , TupE [e,VarE x])
-        R -> (TupP [VarP x,p] , TupE [VarE x,e])
-
-
-
-pairT :: TypeQ -> TypeQ -> TypeQ
-pairT x = appT (appT (tupleT 2) x)
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
@@ -22,7 +22,6 @@
 
 import Control.Monad hiding (mapM)
 import Data.Comp.Algebra
-import Data.Comp.Automata
 import Data.Comp.Sum
 import Data.Comp.Term
 import Data.Foldable
@@ -43,18 +42,6 @@
     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
deleted file mode 100644
--- a/src/Data/Comp/MacroAutomata.hs
+++ /dev/null
@@ -1,199 +0,0 @@
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE Rank2Types          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE 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.Algebra
-import Data.Comp.Automata
-import Data.Comp.Multi.HFunctor (I (..))
-import Data.Comp.Ops
-import Data.Comp.Term
-
--- | 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/Mapping.hs b/src/Data/Comp/Mapping.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Mapping.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Mapping
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides functionality to construct mappings from
+-- positions in a functorial value.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Mapping
+    ( Numbered (..)
+    , unNumbered
+    , number
+    , Traversable ()
+    , Mapping (..)
+    , lookupNumMap) where
+
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Traversable
+
+import Control.Monad.State hiding (mapM)
+import Prelude hiding (mapM)
+
+
+-- | This type is used for numbering components of a functorial value.
+data Numbered a = Numbered Int a
+
+unNumbered :: Numbered a -> a
+unNumbered (Numbered _ x) = x
+
+
+-- | This function numbers the components of the given functorial
+-- value with consecutive integers starting at 0.
+number :: Traversable f => f a -> f (Numbered a)
+number x = evalState (mapM run x) 0 where
+  run b = do n <- get
+             put (n+1)
+             return $ Numbered n b
+
+
+infix 1 |->
+infixr 0 &
+
+
+class Functor m => Mapping m k | m -> k where
+    -- | left-biased union of two mappings.
+    (&) :: m v -> m v -> m v
+
+    -- | This operator constructs a singleton mapping.
+    (|->) :: k -> v -> m v
+
+    -- | This is the empty mapping.
+    empty :: m v
+
+    -- | This function constructs the pointwise product of two maps each
+    -- with a default value.
+    prodMap :: v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
+
+    -- | Returns the value at the given key or returns the given
+    -- default when the key is not an element of the map.
+    findWithDefault :: a -> k -> m a -> a
+
+
+
+newtype NumMap k v = NumMap (IntMap v) deriving Functor
+
+lookupNumMap :: a -> Int -> NumMap t a -> a
+lookupNumMap d k (NumMap m) = IntMap.findWithDefault d k m
+
+instance Mapping (NumMap k) (Numbered k) where
+    NumMap m1 & NumMap m2 = NumMap (IntMap.union m1 m2)
+    Numbered k _ |-> v = NumMap $ IntMap.singleton k v
+    empty = NumMap IntMap.empty
+
+    findWithDefault d (Numbered i _) m = lookupNumMap d i m
+
+    prodMap p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge 
+                                          (IntMap.map (,q)) (IntMap.map (p,)) mp mq
+      where merge _ p q = Just (p,q)
diff --git a/src/Data/Comp/Multi/Mapping.hs b/src/Data/Comp/Multi/Mapping.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Multi/Mapping.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Multi.Mapping
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides functionality to construct mappings from
+-- positions in a functorial value.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Multi.Mapping
+    ( Numbered (..)
+    , unNumbered
+    , number
+    , HTraversable ()
+    , Mapping (..)
+    , lookupNumMap) where
+
+import Data.Comp.Multi.HFunctor
+import Data.Comp.Multi.HTraversable
+
+import Control.Monad.State
+
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+
+
+-- | This type is used for numbering components of a functorial value.
+data Numbered a i = Numbered Int (a i)
+
+unNumbered :: Numbered a :-> a
+unNumbered (Numbered _ x) = x
+
+
+-- | This function numbers the components of the given functorial
+-- value with consecutive integers starting at 0.
+number :: HTraversable f => f a :-> f (Numbered a)
+number x = evalState (hmapM run x) 0 where
+  run b = do n <- get
+             put (n+1)
+             return $ Numbered n b
+
+
+
+infix 1 |->
+infixr 0 &
+
+
+class Mapping m (k :: * -> *) | m -> k where
+    -- | left-biased union of two mappings.
+    (&) :: m v -> m v -> m v
+
+    -- | This operator constructs a singleton mapping.
+    (|->) :: k i -> v -> m v
+
+    -- | This is the empty mapping.
+    empty :: m v
+
+    -- | This function constructs the pointwise product of two maps each
+    -- with a default value.
+    prodMap :: v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)
+
+    -- | Returns the value at the given key or returns the given
+    -- default when the key is not an element of the map.
+    findWithDefault :: a -> k i -> m a -> a
+
+
+newtype NumMap (k :: * -> *) v = NumMap (IntMap v) deriving Functor
+
+lookupNumMap :: a -> Int -> NumMap t a -> a
+lookupNumMap d k (NumMap m) = IntMap.findWithDefault d k m
+
+instance Mapping (NumMap k) (Numbered k) where
+    NumMap m1 & NumMap m2 = NumMap (IntMap.union m1 m2)
+    Numbered k _ |-> v = NumMap $ IntMap.singleton k v
+    empty = NumMap IntMap.empty
+
+    findWithDefault d (Numbered i _) m = lookupNumMap d i m
+
+    prodMap p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge 
+                                          (IntMap.map (,q)) (IntMap.map (p,)) mp mq
+      where merge _ p q = Just (p,q)
diff --git a/src/Data/Comp/Multi/Number.hs b/src/Data/Comp/Multi/Number.hs
deleted file mode 100644
--- a/src/Data/Comp/Multi/Number.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Multi.Number
--- Copyright   :  (c) 2012 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module provides functionality to number the components of a
--- functorial value with consecutive integers.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Multi.Number
-    ( Numbered (..)
-    , unNumbered
-    , number
-    , HTraversable ()) where
-
-import Data.Comp.Multi.Equality
-import Data.Comp.Multi.HFunctor
-import Data.Comp.Multi.HTraversable
-import Data.Comp.Multi.Ordering
-
-
-import Control.Monad.State
-
-
--- | This type is used for numbering components of a functorial value.
-newtype Numbered a i = Numbered (Int, a i)
-
-unNumbered :: Numbered a :-> a
-unNumbered (Numbered (_, x)) = x
-
-instance KEq (Numbered a) where
-  keq (Numbered (i,_))  (Numbered (j,_)) = i == j
-
-instance KOrd (Numbered a) where
-    kcompare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j
-
--- | This function numbers the components of the given functorial
--- value with consecutive integers starting at 0.
-number :: HTraversable f => f a :-> f (Numbered a)
-number x = evalState (hmapM run x) 0 where
-  run b = do n <- get
-             put (n+1)
-             return $ Numbered (n,b)
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -36,16 +36,19 @@
      variables',
      appSubst,
      compSubst,
-     getBoundVars
+     getBoundVars,
+    (&),
+    (|->),
+    empty
     ) where
 
 import Data.Comp.Multi.Algebra
 import Data.Comp.Multi.Derive
 import Data.Comp.Multi.HFoldable
 import Data.Comp.Multi.HFunctor
-import Data.Comp.Multi.Number
+import Data.Comp.Multi.Mapping
 import Data.Comp.Multi.Ops
-import Data.Comp.Multi.Ordering
+
 import Data.Comp.Multi.Term
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -81,20 +84,20 @@
     -- @
     -- data Let i e = Let Var (e i) (e i)
     -- instance HasVars Let Var where
-    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]
+    --   bindsVars (Let v x y) = y |-> Set.singleton v
     -- @
     -- If, instead, the let binding is recursive, the methods has to
     -- be implemented like this:
     -- @
-    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),
-    --                                         (y, (Set.singleton v))]
+    --   bindsVars (Let v x y) = x |-> Set.singleton v &
+    --                           y |-> Set.singleton v
     -- @
     -- This indicates that the scope of the bound variable also
     -- extends to the right-hand side of the variable binding.
     --
     -- The default implementation returns the empty map.
-    bindsVars :: KOrd a => f a :=> Map (E a) (Set v)
-    bindsVars _ = Map.empty
+    bindsVars :: Mapping m a => f a :=> m (Set v)
+    bindsVars _ = empty
 
 $(derive [liftSum] [''HasVars])
 
@@ -113,10 +116,9 @@
 getBoundVars :: forall f a v i . (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i
 getBoundVars t = let n :: f (Numbered a) i
                      n = number t
-                     m :: Map (E (Numbered a)) (Set v)
                      m = bindsVars n
                      trans :: Numbered a :-> (a :*: K (Set v))
-                     trans x = unNumbered x :*: K (Map.findWithDefault Set.empty (E x) m)
+                     trans (Numbered i x) = x :*: K (lookupNumMap Set.empty i m)
                  in hfmap trans n
 
 -- | This combinator combines 'getBoundVars' with the 'mfmap' function.
@@ -124,10 +126,9 @@
                   => (Set v -> a :-> b) -> f a i -> f b i
 hfmapBoundVars f t = let n :: f (Numbered a) i
                          n = number t
-                         m :: Map (E (Numbered a)) (Set v)
                          m = bindsVars n
                          trans :: Numbered a :-> b
-                         trans x = f (Map.findWithDefault Set.empty (E x) m) (unNumbered x)
+                         trans (Numbered i x) = f (lookupNumMap Set.empty i m) x
                      in hfmap trans n
 
 -- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.
@@ -135,10 +136,9 @@
                   => (b -> Set v ->  a :=> b) -> b -> f a i -> b
 hfoldlBoundVars f e t = let n :: f (Numbered a) i
                             n = number t
-                            m :: Map (E (Numbered a)) (Set v)
                             m = bindsVars n
                             trans :: b -> Numbered a :=> b
-                            trans x y = f x (Map.findWithDefault Set.empty (E y) m) (unNumbered y)
+                            trans x (Numbered i y) = f x (lookupNumMap Set.empty i m) y
                        in hfoldl trans e n
 
 
diff --git a/src/Data/Comp/Number.hs b/src/Data/Comp/Number.hs
deleted file mode 100644
--- a/src/Data/Comp/Number.hs
+++ /dev/null
@@ -1,45 +0,0 @@
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Number
--- Copyright   :  (c) 2012 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module provides functionality to number the components of a
--- functorial value with consecutive integers.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Number
-    ( Numbered (..)
-    , unNumbered
-    , number
-    , Traversable ()) where
-
-import Data.Traversable
-
-import Control.Monad.State hiding (mapM)
-import Prelude hiding (mapM)
-
-
--- | This type is used for numbering components of a functorial value.
-newtype Numbered a = Numbered (Int, a)
-
-unNumbered :: Numbered a -> a
-unNumbered (Numbered (_, x)) = x
-
-instance Eq (Numbered a) where
-    Numbered (i,_) == Numbered (j,_) = i == j
-
-instance Ord (Numbered a) where
-    compare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j
-
--- | This function numbers the components of the given functorial
--- value with consecutive integers starting at 0.
-number :: Traversable f => f a -> f (Numbered a)
-number x = evalState (mapM run x) 0 where
-  run b = do n <- get
-             put (n+1)
-             return $ Numbered (n,b)
diff --git a/src/Data/Comp/Thunk.hs b/src/Data/Comp/Thunk.hs
--- a/src/Data/Comp/Thunk.hs
+++ b/src/Data/Comp/Thunk.hs
@@ -42,13 +42,13 @@
 
 import Data.Comp.Algebra
 import Data.Comp.Equality
-import Data.Comp.Number
+import Data.Comp.Mapping
 import Data.Comp.Ops ((:+:) (..), fromInr)
 import Data.Comp.Sum
 import Data.Comp.Term
 import Data.Foldable hiding (and)
 
-import qualified Data.Set as Set
+import qualified Data.IntSet as IntSet
 
 import Control.Monad hiding (mapM, sequence)
 import Data.Traversable
@@ -160,7 +160,7 @@
 -- @f@. It is a function that extracts a number of components (of
 -- polymorphic type @a@) from a functorial value and puts it into a
 -- list.
-type Pos f = forall a . Ord a => f a -> [a]
+type Pos f = forall a . f a -> [a]
 
 -- | This combinator is a variant of 'strict' that only makes a subset
 -- of the arguments of a functor application strict. The first
@@ -169,7 +169,7 @@
 strictAt :: (f :<: g, Traversable f, Monad m) => Pos f ->  f (TermT m g) -> TermT m g
 strictAt p s = thunk $ liftM (inject_ (Inr . inj)) $ mapM run s'
     where s'  = number s
-          isStrict e = Set.member e $ Set.fromList $ p s'
+          isStrict (Numbered i _) = IntSet.member i $ IntSet.fromList $ map (\(Numbered i _) -> i) $ p s'
           run e | isStrict e = whnf' $ unNumbered e
                 | otherwise  = return $ unNumbered e
 
diff --git a/src/Data/Comp/Variables.hs b/src/Data/Comp/Variables.hs
--- a/src/Data/Comp/Variables.hs
+++ b/src/Data/Comp/Variables.hs
@@ -33,12 +33,15 @@
      substVars,
      appSubst,
      compSubst,
-     getBoundVars
+     getBoundVars,
+    (&),
+    (|->),
+    empty
     ) where
 
 import Data.Comp.Algebra
 import Data.Comp.Derive
-import Data.Comp.Number
+import Data.Comp.Mapping
 import Data.Comp.Term
 import Data.Foldable hiding (elem, notElem)
 import Data.Map (Map)
@@ -71,20 +74,20 @@
     -- @
     -- data Let e = Let Var e e
     -- instance HasVars Let Var where
-    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]
+    --   bindsVars (Let v x y) = y |-> Set.singleton v
     -- @
     -- If, instead, the let binding is recursive, the methods has to
     -- be implemented like this:
     -- @
-    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),
-    --                                         (y, (Set.singleton v))]
+    --   bindsVars (Let v x y) = x |-> Set.singleton v &
+    --                           y |-> Set.singleton v
     -- @
     -- This indicates that the scope of the bound variable also
     -- extends to the right-hand side of the variable binding.
     --
     -- The default implementation returns the empty map.
-    bindsVars :: Ord a => f a -> Map a (Set v)
-    bindsVars _ = Map.empty
+    bindsVars :: Mapping m a => f a -> m (Set v)
+    bindsVars _ = empty
 
 
 $(derive [liftSum] [''HasVars])
@@ -104,21 +107,21 @@
 getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)
 getBoundVars t = let n = number t
                      m = bindsVars n
-                     trans x = (Map.findWithDefault Set.empty x m, unNumbered x)
+                     trans (Numbered i x) = (lookupNumMap Set.empty i m, x)
                  in fmap trans n
 
 -- | This combinator combines 'getBoundVars' with the generic 'fmap' function.
 fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b
 fmapBoundVars f t = let n = number t
                         m = bindsVars n
-                        trans x = f (Map.findWithDefault Set.empty x m) (unNumbered x)
+                        trans (Numbered i x) = f (lookupNumMap Set.empty i m) x
                     in fmap trans n
 
 -- | This combinator combines 'getBoundVars' with the generic 'foldl' function.
 foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b
 foldlBoundVars f e t = let n = number t
                            m = bindsVars n
-                           trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y)
+                           trans x (Numbered i y) = f x (lookupNumMap Set.empty i m) y
                        in foldl trans e n
 
 -- | Convert variables to holes, except those that are bound.
diff --git a/testsuite/tests/Data/Comp/Multi/Variables_Test.hs b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
--- a/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
+++ b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
@@ -64,16 +64,16 @@
     isVar (Var v) = Just v
     isVar _       = Nothing
     
-    bindsVars (Abs v a) = Map.singleton (E a) (Set.singleton v)
-    bindsVars _         = Map.empty
+    bindsVars (Abs v a) = a |-> Set.singleton v
+    bindsVars _         = empty
 
 instance HasVars Op a where
 
 instance HasVars Let Var where
-    bindsVars (Let v _ a) = Map.singleton (E a) (Set.singleton v)
+    bindsVars (Let v _ a) = a |-> Set.singleton v
 
 instance HasVars LetRec Var where
-    bindsVars (LetRec v a b) = Map.fromList [(E a,vs),(E b,vs)]
+    bindsVars (LetRec v a b) = a |-> vs & b |-> vs
         where vs = Set.singleton v
 
 -- let x = x + 1 in (\y. y + x) z
diff --git a/testsuite/tests/Data/Comp/Variables_Test.hs b/testsuite/tests/Data/Comp/Variables_Test.hs
--- a/testsuite/tests/Data/Comp/Variables_Test.hs
+++ b/testsuite/tests/Data/Comp/Variables_Test.hs
@@ -10,9 +10,7 @@
 import Data.Comp.Term
 import Data.Comp.Show ()
 
-import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Set (Set)
 import qualified Data.Set as Set
 
 import Test.Framework
@@ -53,16 +51,16 @@
     isVar (Var v) = Just v
     isVar _       = Nothing
     
-    bindsVars (Abs v a) = Map.singleton a (Set.singleton v)
-    bindsVars _         = Map.empty
+    bindsVars (Abs v a) =  a |-> Set.singleton v
+    bindsVars _         = empty
 
 instance HasVars Op a where
 
 instance HasVars Let Var where
-    bindsVars (Let v _ a) = Map.singleton a (Set.singleton v)
+    bindsVars (Let v _ a) = a |-> Set.singleton v
 
 instance HasVars LetRec Var where
-    bindsVars (LetRec v a b) = Map.fromList [(a,vs),(b,vs)]
+    bindsVars (LetRec v a b) = a |-> vs & b |-> vs
         where vs = Set.singleton v
 
 -- let x = x + 1 in (\y. y + x) z