diff --git a/ADP/Fusion/Base/Classes.hs b/ADP/Fusion/Base/Classes.hs
--- a/ADP/Fusion/Base/Classes.hs
+++ b/ADP/Fusion/Base/Classes.hs
@@ -35,11 +35,13 @@
 -- show up in CORE.
 
 class Element x i where
-  data Elm x i :: *
-  type Arg x :: *
+  data Elm    x i :: *
+  type RecElm x i :: *
+  type Arg    x   :: *
   getArg :: Elm x i -> Arg x
   getIdx :: Elm x i -> i
   getOmx :: Elm x i -> i
+  getElm :: Elm x i -> RecElm x i
 
 -- | @mkStream@ creates the actual stream of elements (@Elm@) that will be fed
 -- to functions on the left of the @(<<<)@ operator. Streams work over all
diff --git a/ADP/Fusion/Base/Subword.hs b/ADP/Fusion/Base/Subword.hs
--- a/ADP/Fusion/Base/Subword.hs
+++ b/ADP/Fusion/Base/Subword.hs
@@ -73,3 +73,30 @@
           {-# Inline [0] go #-}
   {-# Inline mkStream #-}
 
+
+
+instance
+  ( Monad m
+  , MkStream m S is
+  , Context (is:.Subword) ~ (Context is:.(InsideContext ()))
+  ) => MkStream m S (is:.Subword) where
+  mkStream S (vs:.IStatic ()) (lus:.Subword (_:.h)) (ixs:.Subword(i:.j))
+    = staticCheck (i>=0 && i==j && j<=h)
+    . map (\(ElmS zi zo) -> ElmS (zi:.subword i i) (zo:.subword 0 0))
+    $ mkStream S vs lus ixs
+  mkStream S (vs:.IVariable ()) (lus:.Subword (_:.h)) (ixs:.Subword (i:.j))
+    = map (\(ElmS zi zo) -> ElmS (zi:.subword i i) (zo:.subword 0 0))
+    . filter (const $ 0<=i && i<=j && j<=h)
+    $ mkStream S vs lus ixs
+  {-# Inline mkStream #-}
+
+instance TableStaticVar Subword where
+  tableStaticVar (IStatic   d) _ = IVariable d
+  tableStaticVar (IVariable d) _ = IVariable d
+  tableStreamIndex c _ (Subword (i:.j))
+    | c==EmptyOk  = subword i j
+    | c==NonEmpty = subword i (j-1)
+    | c==NonEmpty = error "A.F.B.Subword ???"
+  {-# INLINE [0] tableStaticVar   #-}
+  {-# INLINE [0] tableStreamIndex #-}
+
diff --git a/ADP/Fusion/QuickCheck/Point.hs b/ADP/Fusion/QuickCheck/Point.hs
--- a/ADP/Fusion/QuickCheck/Point.hs
+++ b/ADP/Fusion/QuickCheck/Point.hs
@@ -278,9 +278,10 @@
   zzz :: IO (MutArr IO (Unboxed (Z:.PointL:.PointL) Int))
   zzz = fromListM (Z:.PointL 0:.PointL 0) (Z:.maxPL:.maxPL) [0 ..]
 
-maxPL = PointL 100
+maxI = 100
+maxPL = PointL maxI
 
-xs = VU.fromList [0 .. 99 :: Int]
+xs = VU.fromList [0 .. maxI - 1 :: Int]
 
 -- * general quickcheck stuff
 
diff --git a/ADP/Fusion/QuickCheck/Subword.hs b/ADP/Fusion/QuickCheck/Subword.hs
--- a/ADP/Fusion/QuickCheck/Subword.hs
+++ b/ADP/Fusion/QuickCheck/Subword.hs
@@ -1,6 +1,11 @@
 
 {-# Options_GHC -O0 #-}
 
+-- |
+--
+-- TODO need to carefully check all props against boundary errors!
+-- Especially the 2-dim cases!
+
 module ADP.Fusion.QuickCheck.Subword where
 
 import           Test.QuickCheck
@@ -148,17 +153,66 @@
   ls = [ () | i==0 && j==highest ]
 
 
+-- ** Multi-tape cases
 
-highest = 2
+prop_2dimIt ix@(Z:.Subword (i:.j):.Subword (k:.l)) = zs == ls where
+  t = ITbl 0 0 (Z:.EmptyOk:.EmptyOk) xsSS (\ _ _ -> Id ((1,1),(1,1)))
+  zs = (id <<< t ... S.toList) (Z:.subword 0 highest:.subword 0 highest) ix
+  ls = [ ( unsafeIndex xsSS ix ) | j<=highest && l<=highest ]
 
+{-
+xprop_2dimItIt ix@(Z:.Subword (i:.j):.Subword (k:.l)) = zs == ls where
+  t = ITbl 0 0 (Z:.EmptyOk:.EmptyOk) xsSS (\ _ _ -> Id (1,1))
+  zs = ((,) <<< t % t ... S.toList) (Z:.subword 0 highest:.subword 0 highest) ix
+  ls = [ ( unsafeIndex xsSS (Z:.subword i m:.subword k n)
+         , unsafeIndex xsSS (Z:.subword m j:.subword n l) )
+       | j<=highest && l<=highest
+       , m <- [i..j]
+       , n <- [k..l]
+       ]
+-}
+
+prop_2dimcIt ix@(Z:.Subword(i:.j):.Subword(k:.l)) = {- traceShow (zs,ls) $ -} zs == ls where
+  t = ITbl 0 0 (Z:.EmptyOk:.EmptyOk) xsSS (\ _ _ -> Id ((1,1),(1,1)))
+  zs = ((,) <<< (M:|chr csS:|chr csS) % t ... S.toList) (Z:.subword 0 highest:.subword 0 highest) ix
+  ls = [ ( Z :. (csS VU.! i) :. (csS VU.! k)
+         , unsafeIndex xsSS (Z :. subword (i+1) j :. subword (k+1) l) )
+       | j<=highest && l<=highest
+       , i+1<=j && k+1<=l ]
+
+prop_2dimItc ix@(Z:.Subword(i:.j):.Subword(k:.l)) = {- traceShow (zs,ls) $ -} zs == ls where
+  t = ITbl 0 0 (Z:.EmptyOk:.EmptyOk) xsSS (\ _ _ -> Id ((1,1),(1,1)))
+  zs = ((,) <<< t % (M:|chr csS:|chr csS)  ... S.toList) (Z:.subword 0 highest:.subword 0 highest) ix
+  ls = [ ( unsafeIndex xsSS (Z :. subword i (j-1) :. subword k (l-1))
+         , Z :. (csS VU.! (j-1)) :. (csS VU.! (l-1)) )
+       | j<=highest && l<=highest
+       , i+1<=j && k+1<=l ]
+
+prop_2dimcItc ix@(Z:.Subword(i:.j):.Subword(k:.l)) = {- traceShow (zs,ls) $ -} zs == ls where
+  t = ITbl 0 0 (Z:.EmptyOk:.EmptyOk) xsSS (\ _ _ -> Id ((1,1),(1,1)))
+  zs = ((,,) <<< (M:|chr csS:|chr csS) % t % (M:|chr csS:| chr csS) ... S.toList) (Z:.subword 0 highest:.subword 0 highest) ix
+  ls = [ ( Z :. (csS VU.! i) :. (csS VU.! k)
+         , unsafeIndex xsSS (Z :. subword (i+1) (j-1) :. subword (k+1) (l-1))
+         , Z :. (csS VU.! (j-1)) :. (csS VU.! (l-1)) )
+       | j<=highest && l<=highest
+       , i+2<=j && k+2<=l ]
+
+
+
+highest = 10
+
 csS :: VU.Vector (Int,Int)
-csS = VU.fromList [ (i,i+1) | i <- [0 .. highest] ] -- this should be @highest -1@, we should die if we see @(highest,highest+1)@
+csS = VU.fromList [ (i,i+1) | i <- [0 .. highest-1] ] -- this should be @highest -1@, we should die if we see @(highest,highest+1)@
 
 xsS :: Unboxed Subword (Int,Int)
 xsS = fromList (subword 0 0) (subword 0 highest) [ (i,j) | i <- [ 0 .. highest ] , j <- [ i .. highest ] ]
 
 xoS :: Unboxed (Outside Subword) (Int,Int)
 xoS = fromList (O $ subword 0 0) (O $ subword 0 highest) [ (i,j) | i <- [ 0 .. highest ] , j <- [ i .. highest ] ]
+
+xsSS :: Unboxed (Z:.Subword:.Subword) ( (Int,Int) , (Int,Int) )
+xsSS = fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 highest:.subword 0 highest) ((-1,-1),(-1,-1))
+        $ Prelude.map (\((i,j),(k,l)) -> (Z:.subword i j:.subword k l, ((i,j),(k,l)) )) [ ((i,j) , (k,l)) | i <- [0 .. highest], j <-[i .. highest], k <- [0 .. highest], l <- [0 .. highest] ]
 
 -- * general quickcheck stuff
 
diff --git a/ADP/Fusion/SynVar.hs b/ADP/Fusion/SynVar.hs
--- a/ADP/Fusion/SynVar.hs
+++ b/ADP/Fusion/SynVar.hs
@@ -7,6 +7,7 @@
   , module ADP.Fusion.SynVar.Backtrack
   , module ADP.Fusion.SynVar.Fill
   , module ADP.Fusion.SynVar.Recursive
+  , module ADP.Fusion.SynVar.Split
   ) where
 
 import ADP.Fusion.SynVar.Array
@@ -14,4 +15,5 @@
 import ADP.Fusion.SynVar.Backtrack
 import ADP.Fusion.SynVar.Fill
 import ADP.Fusion.SynVar.Recursive
+import ADP.Fusion.SynVar.Split
 
diff --git a/ADP/Fusion/SynVar/Array.hs b/ADP/Fusion/SynVar/Array.hs
--- a/ADP/Fusion/SynVar/Array.hs
+++ b/ADP/Fusion/SynVar/Array.hs
@@ -9,6 +9,7 @@
 import ADP.Fusion.SynVar.Array.Point
 import ADP.Fusion.SynVar.Array.Set
 import ADP.Fusion.SynVar.Array.Subword
+import ADP.Fusion.SynVar.Array.TermSymbol
 import ADP.Fusion.SynVar.Array.Type
 
 {-
diff --git a/ADP/Fusion/SynVar/Array/Subword.hs b/ADP/Fusion/SynVar/Array/Subword.hs
--- a/ADP/Fusion/SynVar/Array/Subword.hs
+++ b/ADP/Fusion/SynVar/Array/Subword.hs
@@ -1,4 +1,6 @@
 
+{-# Language MagicHash #-}
+
 module ADP.Fusion.SynVar.Array.Subword where
 
 import Data.Strict.Tuple
@@ -14,9 +16,12 @@
 import ADP.Fusion.SynVar.Array.Type
 import ADP.Fusion.SynVar.Backtrack
 
+-- TODO think about what we are about to do
+import GHC.Prim (reallyUnsafePtrEquality#)
 
 
 
+
 -- TODO delay inline @(subword i $ j - minSize c)@ or face fusion-breakage.
 -- Can we just have @Inline [0] subword@ to fix this?
 
@@ -171,4 +176,143 @@
   toEmpty    (BtITbl _ arr bt) = BtITbl EmptyOk  arr bt
   {-# Inline toNonEmpty #-}
   {-# Inline toEmpty #-}
+
+
+
+instance
+  ( Monad m
+  , Element ls Subword -- (Z:.Subword:.Subword)
+  , FirstSecond ls (arr (Z:.Subword:.Subword) x)
+  , FirstSecondIdx ls (arr (Z:.Subword:.Subword) x) Subword
+  , PrimArrayOps arr (Z:.Subword:.Subword) x
+  , MkStream m ls Subword
+  , Show x
+  ) => MkStream m (ls :!: ITbl m arr (Z:.Subword:.Subword) x) Subword where
+  mkStream (ls :!: ITbl _ _ c t elm) (IStatic ()) hh (Subword (i:.j))
+    = map (\s -> let (Subword (_:.l)) = getIdx s
+                     ab               = if greenLight ls t
+                                          then greenIdx ls (undefined :: Subword) t s
+                                          else subword 0 0
+                 in  -- traceShow ("13",ab,subword l j,t!(Z:.ab:.subword l j)) $
+                     ElmITbl (t ! (Z:.ab:.subword l j)) (subword l j) (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - 0))
+  mkStream (ls :!: ITbl _ _ c t elm) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - 0))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l - 0)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                        ab             = if greenLight ls t
+                                                           then greenIdx ls (undefined :: Subword) t s
+                                                           else subword 0 0
+                                    --traceShow ("02",ab,subword k l,t!(Z:.ab:.subword k l)) $
+                                    return $ Yield (ElmITbl (t ! (Z:.ab:.kl)) kl (subword 0 0) s) (s:.z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
+instance
+  ( Monad mB
+  , FirstSecond ls (arr (Z:.Subword:.Subword) x)
+  , FirstSecondIdx ls (arr (Z:.Subword:.Subword) x) Subword
+  , PrimArrayOps arr (Z:.Subword:.Subword) x
+  , Element ls Subword
+  , MkStream mB ls Subword
+  , Show r
+  ) => MkStream mB (ls :!: Backtrack (ITbl mF arr (Z:.Subword:.Subword) x) mF mB r) Subword where
+  mkStream (ls :!: BtITbl c t bt) (IStatic ()) hh (Subword (i:.j))
+    = mapM (\s -> let (Subword (_:.l)) = getIdx s
+                      lj               = subword l j
+                      light            = greenLight ls t
+                      ab               = if light
+                                           then greenIdx ls (undefined :: Subword) t s
+                                           else lj -- subword 0 0
+                      ablj             = if light
+                                           then Z:.ab:.lj
+                                           else Z:.subword 0 0:.subword 0 0 -- Z:.lj:.lj
+                  in bt (Prelude.snd $ bounds t) ablj >>= \ ~bb -> {- traceShow (ab,lj,bb) $ -} return $ ElmBtITbl (t ! ablj) bb lj (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - 0))
+  mkStream (ls :!: BtITbl c t bt) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - 0))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l - 0)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                        light          = greenLight ls t
+                                        ab             = if light
+                                                           then greenIdx ls (undefined :: Subword) t s
+                                                           else kl -- subword 0 0
+                                        abkl           = if light
+                                                           then Z:.ab:.kl
+                                                           else Z:.subword 0 0:.subword 0 0 -- Z:.kl:.kl
+                                    bt (Prelude.snd $ bounds t) abkl >>= \ ~bb -> {- traceShow (ab,kl,bb) $ -} return $ Yield (ElmBtITbl (t!abkl) bb kl (subword 0 0) s) (s:.z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
+-- | Get the previous index; this should really be made generic!
+--
+-- TODO This is probably a REALLY STUPID IDEA ;-)
+
+class FirstSecond x k where
+  greenLight :: x -> k -> Bool
+
+class FirstSecondIdx x k i where
+  greenIdx :: x -> i -> k -> Elm x i -> Subword
+
+instance FirstSecond S k where
+  greenLight S _ = False
+  {-# Inline greenLight #-}
+
+
+
+instance
+  ( FirstSecond ls (arr (Z:.Subword:.Subword) x)
+  ) => FirstSecond (ls :!: ITbl m arr (Z:.Subword:.Subword) x) (arr (Z:.Subword:.Subword) x) where
+  greenLight (ls :!: ITbl _ _ _ t _) t' =
+    case reallyUnsafePtrEquality# t t' of
+      -- TODO speaking of stupid ideas!
+      1# -> True
+      _  -> greenLight ls t'
+  {-# Inline greenLight #-}
+
+instance
+  ( FirstSecond ls (arr (Z:.Subword:.Subword) x)
+  ) => FirstSecond (ls :!: Backtrack (ITbl mF arr (Z:.Subword:.Subword) x) mF mB r) (arr (Z:.Subword:.Subword) x) where
+  greenLight (ls :!: BtITbl _ t _) t' =
+    case reallyUnsafePtrEquality# t t' of
+      -- TODO speaking of stupid ideas!
+      1# -> True
+      _  -> greenLight ls t'
+  {-# Inline greenLight #-}
+
+
+
+instance FirstSecondIdx S k i where
+  greenIdx S _ _ _ = error "shouldn't arrive here!"
+  {-# Inline greenIdx #-}
+
+instance
+  ( FirstSecondIdx ls (arr (Z:.Subword:.Subword) x) Subword
+  , Elm ls Subword ~ RecElm (ls :!: ITbl m arr (Z:.Subword:.Subword) x) Subword
+  , Element ls Subword
+  ) => FirstSecondIdx (ls :!: ITbl m arr (Z:.Subword:.Subword) x) (arr (Z:.Subword:.Subword) x) Subword where
+  greenIdx (ls :!: ITbl _ _ _ t _) _ t' e =
+    case reallyUnsafePtrEquality# t t' of
+      1# -> let ab = getIdx e in ab
+      _  -> let g = getElm e in greenIdx ls (undefined :: Subword) t' g
+  {-# Inline greenIdx   #-}
+
+instance
+  ( FirstSecondIdx ls (arr (Z:.Subword:.Subword) x) Subword
+  , Elm ls Subword ~ RecElm (ls :!: Backtrack (ITbl mF arr (Z:.Subword:.Subword) x) mF mB r) Subword
+  , Element ls Subword
+  ) => FirstSecondIdx (ls :!: Backtrack (ITbl mF arr (Z:.Subword:.Subword) x) mF mB r) (arr (Z:.Subword:.Subword) x) Subword where
+  greenIdx (ls :!: BtITbl _ t _) _ t' e =
+    case reallyUnsafePtrEquality# t t' of
+      1# -> let ab = getIdx e in ab
+      _  -> let g = getElm e in greenIdx ls (undefined :: Subword) t' g
+  {-# Inline greenIdx   #-}
 
diff --git a/ADP/Fusion/SynVar/Array/TermSymbol.hs b/ADP/Fusion/SynVar/Array/TermSymbol.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/SynVar/Array/TermSymbol.hs
@@ -0,0 +1,110 @@
+
+-- | TODO migrate instances to correct modules
+
+module ADP.Fusion.SynVar.Array.TermSymbol where
+
+import Data.Strict.Tuple hiding (snd)
+import Data.Vector.Fusion.Stream.Size
+import Data.Vector.Fusion.Util (delay_inline)
+import Data.Vector.Fusion.Stream.Monadic
+import Debug.Trace
+import Prelude hiding (map,mapM)
+
+import Data.PrimitiveArray hiding (map)
+
+import ADP.Fusion.Base
+import ADP.Fusion.SynVar.Array.Type
+import ADP.Fusion.SynVar.Backtrack
+
+
+
+-- | TODO need to deal with @minSize@
+
+instance
+  ( Monad m
+  , TerminalStream m a is
+  , PrimArrayOps arr Subword x
+  , Show x
+  ) => TerminalStream m (TermSymbol a (ITbl m arr Subword x)) (is:.Subword) where
+  terminalStream (a :| ITbl _ _ c t _) (sv:.IStatic _) (is:.ix@(Subword (i:.j)))
+    = map (\ (S6 s (zi:.(Subword (_:.l))) (zo:._) is os e) ->
+              let lj = subword l j
+              in  S6 s zi zo (is:.lj) (os:.subword 0 0) (e:.(t!lj)) )
+    . iPackTerminalStream a sv (is:.ix)
+  terminalStream (a :| ITbl _ _ c t _) (sv:.IVariable _) (is:.ix@(Subword (i:.j)))
+    = flatten mk step Unknown . iPackTerminalStream a sv (is:.ix)
+    where mk (S6 s (zi:.(Subword (_:.l))) (zo:._) is os e) = return (S6 s zi zo is os e :. l :. j - l) -- TODO minsize c !
+          step (s6:.k:.z) | z >= 0 = do let S6 s zi zo is os e = s6
+                                            l                  = j - z
+                                            kl                 = subword k l
+                                        return $ Yield (S6 s zi zo (is:.kl) (os:.subword 0 0) (e:.(t!kl))) (s6 :. k :. z-1)
+                          | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline terminalStream #-}
+
+instance
+  ( Monad mB
+  , TerminalStream mB a is
+  , PrimArrayOps arr Subword x
+  ) => TerminalStream mB (TermSymbol a (Backtrack (ITbl mF arr Subword x) mF mB r)) (is:.Subword) where
+  terminalStream (a :| BtITbl c t bt) (sv:.IStatic _) (is:.ix@(Subword (i:.j)))
+    = mapM (\ (S6 s (zi:.(Subword (_:.l))) (zo:._) is os e) ->
+              let lj = subword l j
+                  hh = snd $ bounds t
+              in  bt hh lj >>= \ ~bb -> return $ S6 s zi zo (is:.lj) (os:.subword 0 0) (e:.(t!lj, bb)) )
+    . iPackTerminalStream a sv (is:.ix)
+  terminalStream (a :| BtITbl c t bt) (sv:.IVariable _) (is:.ix@(Subword (i:.j)))
+    = flatten mk step Unknown . iPackTerminalStream a sv (is:.ix)
+    where mk (S6 s (zi:.(Subword (_:.l))) (zo:._) is os e) = return (S6 s zi zo is os e :. l :. j - l) -- TODO minsize c !
+          step (s6:.k:.z) | z >= 0 = do let S6 s zi zo is os e = s6
+                                            l                  = j - z
+                                            kl                 = subword k l
+                                            hh                 = snd $ bounds t
+                                        bt hh kl >>= \ ~bb -> return $ Yield (S6 s zi zo (is:.kl) (os:.subword 0 0) (e:.(t!kl,bb))) (s6 :. k :. z-1)
+                          | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline terminalStream #-}
+
+
+instance TermStaticVar (ITbl m arr Subword x) Subword where
+  termStaticVar _ (IStatic   d) _ = IVariable d
+  termStaticVar _ (IVariable d) _ = IVariable d
+  termStreamIndex (ITbl _ _ _ _ _) (IStatic   d) (Subword (i:.j)) = subword i j -- TODO minSize handling !
+  termStreamIndex (ITbl _ _ _ _ _) (IVariable d) (Subword (i:.j)) = subword i j -- TODO minsize handling
+  {-# Inline [0] termStaticVar   #-}
+  {-# Inline [0] termStreamIndex #-}
+
+instance TermStaticVar (Backtrack (ITbl mF arr Subword x) mF mB r) Subword where
+  termStaticVar _ (IStatic   d) _ = IVariable d
+  termStaticVar _ (IVariable d) _ = IVariable d
+  termStreamIndex (BtITbl _ _ _) (IStatic   d) (Subword (i:.j)) = subword i j -- TODO minSize handling !
+  termStreamIndex (BtITbl _ _ _) (IVariable d) (Subword (i:.j)) = subword i j -- TODO minsize handling
+  {-# Inline [0] termStaticVar   #-}
+  {-# Inline [0] termStreamIndex #-}
+
+
+{-
+  mkStream (ls :!: ITbl _ _ c t _) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - minSize c))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l - minSize c)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                    return $ Yield (ElmITbl (t ! kl) kl (subword 0 0) s) (s:. z-1)
+                      | otherwise = return $ Done
+
+  terminalStream (a:|Chr f v) (sv:.IVariable _) (is:.ix@(Subword (i:.j)))
+    = S.map (\(S6 s (zi:.Subword (_:.l)) (zo:._) is os e) -> S6 s zi zo (is:.subword l (l+1)) (os:.subword 0 0) (e:.f v l))
+    . iPackTerminalStream a sv (is:.ix)
+  {-# Inline terminalStream #-}
+
+instance TermStaticVar (Chr r x) Subword where
+  termStaticVar _ sv _ = sv
+  termStreamIndex _ _ (Subword (i:.j)) = subword i (j-1)
+  {-# Inline [0] termStaticVar   #-}
+  {-# Inline [0] termStreamIndex #-}
+
+-}
+
diff --git a/ADP/Fusion/SynVar/Array/Type.hs b/ADP/Fusion/SynVar/Array/Type.hs
--- a/ADP/Fusion/SynVar/Array/Type.hs
+++ b/ADP/Fusion/SynVar/Array/Type.hs
@@ -27,12 +27,16 @@
 
 instance Build (ITbl m arr i x)
 
+type instance TermArg (TermSymbol a (ITbl m arr i x)) = TermArg a :. x
+
 instance GenBacktrackTable (ITbl mF arr i x) mF mB r where
   data Backtrack (ITbl mF arr i x) mF mB r = BtITbl !(TblConstraint i) !(arr i x) (i -> i -> mB [r])
   type BacktrackIndex (ITbl mF arr i x) = i
   toBacktrack (ITbl _ _ c arr _) _ bt = BtITbl c arr bt
   {-# Inline toBacktrack #-}
 
+type instance TermArg (TermSymbol a (Backtrack (ITbl mF arr i x) mF mB r)) = TermArg a :. (x,[r])
+
 instance
   ( Monad m
   , PrimArrayOps arr i x
@@ -56,26 +60,32 @@
   {-# Inline axiom #-}
 
 instance Element ls i => Element (ls :!: ITbl m arr j x) i where
-  data Elm (ls :!: ITbl m arr j x) i = ElmITbl !x !i !i !(Elm ls i)
-  type Arg (ls :!: ITbl m arr j x)   = Arg ls :. x
+  data Elm    (ls :!: ITbl m arr j x) i = ElmITbl !x !i !i !(Elm ls i)
+  type Arg    (ls :!: ITbl m arr j x)   = Arg ls :. x
+  type RecElm (ls :!: ITbl m arr j x) i = Elm ls i
   getArg (ElmITbl x _ _ ls) = getArg ls :. x
   getIdx (ElmITbl _ i _ _ ) = i
   getOmx (ElmITbl _ _ o _ ) = o
+  getElm (ElmITbl _ _ _ ls) = ls
   {-# Inline getArg #-}
   {-# Inline getIdx #-}
   {-# Inline getOmx #-}
+  {-# Inline getElm #-}
 
 deriving instance (Show i, Show (Elm ls i), Show x) => Show (Elm (ls :!: ITbl m arr j x) i)
 
-instance Element ls i => Element (ls :!: (Backtrack (ITbl mF arr i x) mF mB r)) i where
-  data Elm (ls :!: (Backtrack (ITbl mF arr i x) mF mB r)) i = ElmBtITbl !x [r] !i !i !(Elm ls i)
-  type Arg (ls :!: (Backtrack (ITbl mF arr i x) mF mB r))   = Arg ls :. (x, [r])
+instance Element ls i => Element (ls :!: (Backtrack (ITbl mF arr j x) mF mB r)) i where
+  data Elm    (ls :!: (Backtrack (ITbl mF arr j x) mF mB r)) i = ElmBtITbl !x [r] !i !i !(Elm ls i)
+  type Arg    (ls :!: (Backtrack (ITbl mF arr j x) mF mB r))   = Arg ls :. (x, [r])
+  type RecElm (ls :!: (Backtrack (ITbl mF arr j x) mF mB r)) i = Elm ls i
   getArg (ElmBtITbl x s _ _ ls) = getArg ls :. (x,s)
   getIdx (ElmBtITbl _ _ i _ _ ) = i
   getOmx (ElmBtITbl _ _ _ o _ ) = o
+  getElm (ElmBtITbl _ _ _ _ ls) = ls
   {-# Inline getArg #-}
   {-# Inline getIdx #-}
   {-# Inline getOmx #-}
+  {-# Inline getElm #-}
 
 instance (Show x, Show i, Show (Elm ls i)) => Show (Elm (ls :!: (Backtrack (ITbl mF arr i x) mF mB r)) i) where
   show (ElmBtITbl x _ i o s) = show (x,i,o) ++ " " ++ show s
diff --git a/ADP/Fusion/SynVar/Fill.hs b/ADP/Fusion/SynVar/Fill.hs
--- a/ADP/Fusion/SynVar/Fill.hs
+++ b/ADP/Fusion/SynVar/Fill.hs
@@ -12,6 +12,7 @@
 import           Control.Monad (when,forM_)
 import           Data.List (nub,sort)
 import qualified Data.Vector.Unboxed as VU
+import           Data.Proxy
 
 import           Data.PrimitiveArray
 
@@ -54,20 +55,17 @@
     {-# INLINE expose #-}
     {-# INLINE onlyTables #-}
 
--- Thanks to the table being a gadt we now the internal types
---
--- TODO move to Table/Array.hs
 
---instance (ExposeTables ts) => ExposeTables (ts:.(MTbl m arr i x)) where
---    type TableFun   (ts:. MTbl m arr i x) = TableFun   ts :. (PA.MutArr m (arr i x), i -> m x)
---    type OnlyTables (ts:. MTbl m arr i x) = OnlyTables ts :. (PA.MutArr m (arr i x))
---    expose     (ts:.MTbl _ t f) = expose ts :. (t,f)
---    onlyTables (ts:.MTbl _ t _) = onlyTables ts :. t
---    {-# INLINE expose #-}
---    {-# INLINE onlyTables #-}
 
+-- | A vanilla context-free grammar
 
+data CFG
 
+-- | This grammar is a multi-cfg in a monotone setting
+
+data MonotoneMCFG
+
+
 -- * Unsafely mutate 'ITbls' and similar tables in the forward phase.
 
 -- | Mutate a cell in a stack of syntactic variables.
@@ -78,13 +76,13 @@
 -- /not/ want to have this state influence forward results, unless that can
 -- be made deterministic, or we'll break Bellman)
 
-class MutateCell (s :: *) (im :: * -> *) (om :: * -> *) i where
-  mutateCell :: Int -> Int -> (forall a . im a -> om a) -> s -> i -> i -> om ()
+class MutateCell (h :: *) (s :: *) (im :: * -> *) (om :: * -> *) i where
+  mutateCell :: Proxy h -> Int -> Int -> (forall a . im a -> om a) -> s -> i -> i -> om ()
 
 -- |
 
-class MutateTables (s :: *) (im :: * -> *) (om :: * -> *) where
-  mutateTables :: (forall a . im a -> om a) -> s -> om s
+class MutateTables (h :: *) (s :: *) (im :: * -> *) (om :: * -> *) where
+  mutateTables :: Proxy h -> (forall a . im a -> om a) -> s -> om s
 
 class TableOrder (s :: *) where
   tableLittleOrder :: s -> [Int]
@@ -107,39 +105,64 @@
 instance
   ( PrimArrayOps  arr i x
   , MPrimArrayOps arr i x
-  , MutateCell ts im om i
+  , MutateCell CFG ts im om i
   , PrimMonad om
   , Show x, Show i
-  ) => MutateCell (ts:.ITbl im arr i x) im om i where
-  mutateCell bo lo mrph (ts:.ITbl tbo tlo c arr f) lu i = do
-    mutateCell bo lo mrph ts lu i
+  ) => MutateCell CFG (ts:.ITbl im arr i x) im om i where
+  mutateCell h bo lo mrph (ts:.ITbl tbo tlo c arr f) lu i = do
+    mutateCell h bo lo mrph ts lu i
     when (bo==tbo && lo==tlo) $ do
       marr <- unsafeThaw arr
       z <- (inline mrph) $ f lu i
       writeM marr i z
   {-# INLINE mutateCell #-}
 
-{-
+type ZS2 = Z:.Subword:.Subword
+
 instance
-  ( MutateCell ts im om i
-  ) => MutateCell (ts:.IRec im i x) im om i where
-  mutateCell mrph (ts:.IRec (!c) _ _ f) lu i = do
-    mutateCell mrph ts lu i
+  ( PrimArrayOps  arr ZS2 x
+  , MPrimArrayOps arr ZS2 x
+  , MutateCell MonotoneMCFG ts im om ZS2
+  , PrimMonad om
+  ) => MutateCell MonotoneMCFG (ts:.ITbl im arr ZS2 x) im om ZS2 where
+  mutateCell h bo lo mrph (ts:.ITbl tbo tlo c arr f) lu iklj@(Z:.Subword (i:.k):.Subword(l:.j)) = do
+    mutateCell h bo lo mrph ts lu iklj
+    when (bo==tbo && lo==tlo && k<=l) $ do
+      marr <- unsafeThaw arr
+      z <- (inline mrph) $ f lu iklj
+      writeM marr iklj z
   {-# INLINE mutateCell #-}
--}
 
+instance
+  ( PrimArrayOps arr Subword x
+  , MPrimArrayOps arr Subword x
+  , MutateCell h ts im om (Z:.Subword:.Subword)
+  , PrimMonad om
+  ) => MutateCell h (ts:.ITbl im arr Subword x) im om (Z:.Subword:.Subword) where
+  mutateCell h bo lo mrph (ts:.ITbl tbo tlo c arr f) lu@(Z:.Subword (l:._):.Subword(_:.u)) ix@(Z:.Subword (i1:.j1):.Subword (i2:.j2)) = do
+    mutateCell h bo lo mrph ts lu ix
+    when (bo==tbo && lo==tlo && i1==i2 && j1==j2) $ do
+      let i = i1
+      let j = j1
+      marr <- unsafeThaw arr
+      z <- (inline mrph) $ f (subword l u) (subword i j)
+      writeM marr (subword i j) z
+  {-# Inline mutateCell #-}
+
+
+
 -- ** individual instances for filling a complete table and extracting the
 -- bounds
 
 instance
   ( Monad om
-  , MutateCell (ts:.ITbl im arr i x) im om i
+  , MutateCell h (ts:.ITbl im arr i x) im om i
   , PrimArrayOps arr i x
   , Show i
   , IndexStream i
   , TableOrder (ts:.ITbl im arr i x)
-  ) => MutateTables (ts:.ITbl im arr i x) im om where
-  mutateTables mrph tt@(_:.ITbl _ _ _ arr _) = do
+  ) => MutateTables h (ts:.ITbl im arr i x) im om where
+  mutateTables h mrph tt@(_:.ITbl _ _ _ arr _) = do
     let (from,to) = bounds arr
     -- TODO (1) find the set of orders for the synvars
     let !tbos = VU.fromList . nub . sort $ tableBigOrder tt
@@ -147,34 +170,28 @@
     VU.forM_ tbos $ \bo ->
       flip SM.mapM_ (streamUp from to) $ \k ->
         VU.forM_ tlos $ \lo ->
-          mutateCell bo lo (inline mrph) tt to k
+          --traceShow (bo,k,lo) $
+          mutateCell h bo lo (inline mrph) tt to k
     return tt
   {-# INLINE mutateTables #-}
 
-{-
 instance
   ( Monad om
-  , MutateCell (ts:.IRec im i x) im om i
-  , IndexStream i
-  ) => MutateTables (ts:.IRec im i x) im om where
-  mutateTables mrph tt@(_:.IRec _ from to _) = do
-    -- SM.mapM_ (mutateCell (inline mrph) tt to) $ PA.rangeStream from to
-    SM.mapM_ (mutateCell (inline mrph) tt to) $ PA.streamUp from to
-    return tt
-  {-# INLINE mutateTables #-}
--}
-
-instance
-  ( Monad om
-  ) => MutateCell Z im om i where
-  mutateCell _ _ _ Z _ _ = return ()
+  ) => MutateCell p Z im om i where
+  mutateCell _ _ _ _ Z _ _ = return ()
   {-# INLINE mutateCell #-}
 
 -- | Default table filling, assuming that the forward monad is just @IO@.
 --
 -- TODO generalize to @MonadIO@ or @MonadPrim@.
 
-mutateTablesDefault :: MutateTables t Id IO => t -> t
-mutateTablesDefault t = unsafePerformIO $ mutateTables (return . unId) t
+mutateTablesDefault :: MutateTables CFG t Id IO => t -> t
+mutateTablesDefault t = unsafePerformIO $ mutateTables (Proxy :: Proxy CFG) (return . unId) t
 {-# INLINE mutateTablesDefault #-}
+
+-- | Mutate tables, but observe certain hints. We use this for monotone
+-- mcfgs for now.
+
+mutateTablesWithHints :: MutateTables h t Id IO => Proxy h -> t -> t
+mutateTablesWithHints h t = unsafePerformIO $ mutateTables h (return . unId) t
 
diff --git a/ADP/Fusion/SynVar/Indices.hs b/ADP/Fusion/SynVar/Indices.hs
--- a/ADP/Fusion/SynVar/Indices.hs
+++ b/ADP/Fusion/SynVar/Indices.hs
@@ -26,8 +26,29 @@
   tableIndices _ _ _ = id
   {-# INLINE tableIndices #-}
 
-{-
 instance TableIndices is => TableIndices (is:.Subword) where
+  tableIndices (cs:._) (vs:.IStatic _) (ixs:.Subword (i:.j))
+    = map (\(S5 s (zi:.Subword (_:.l)) (zo:._) is os) -> S5 s zi zo (is:.subword l j) (os:.subword 0 0))
+    . tableIndices cs vs ixs
+    . map (\(S5 s zi zo (is:.i) (os:.o)) -> S5 s (zi:.i) (zo:.o) is os)
+  -- TODO ? using the defns in TermSymbol.hs for Array syns?
+  tableIndices (cs:._) (vs:.IVariable _) (ixs:.Subword (i:.j))
+    = map (\(S5 s (zi:.Subword (_:.l)) (zo:._) is os) -> S5 s zi zo (is:.subword l j) (os:.subword 0 0))
+    . tableIndices cs vs ixs
+    . map (\(S5 s zi zo (is:.i) (os:.o)) -> S5 s (zi:.i) (zo:.o) is os)
+  -- TODO minsize handling ? constraint handling?
+  {-
+  tableIndices (cs:._) (vs:.IVariable _) (ixs:.Subword (i:.j))
+    = flatten mk step Unknown
+    . tableIndices cs vs ixs
+    . map (\(S5 s zi zo (is:.i) (os:.o)) -> S5 s (zi:.i) (zo:.o) is os)
+    where mk (S5 s (zi:.Subword (_:.l)) (zo:._) is os) = return ( (S5 s zi zo (is:.
+          step = error "step"
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+          -}
+  {-# Inline tableIndices #-}
+{-
   tableIndices (cs:.c) (vs:.Static) (is:.Subword (i:.j))
     = S.map (\(Tr s (x:.Subword (_:.l)) ys) -> Tr s x (is:.subword l j)) -- constraint handled: tableStreamIndex
     . tableIndices cs vs is
diff --git a/ADP/Fusion/SynVar/Split.hs b/ADP/Fusion/SynVar/Split.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/SynVar/Split.hs
@@ -0,0 +1,11 @@
+
+-- | Split syntactic variables for multi-cfg dynamic programs.
+
+module ADP.Fusion.SynVar.Split
+  ( module ADP.Fusion.SynVar.Split.Type
+  , module ADP.Fusion.SynVar.Split.Subword
+  ) where
+
+import ADP.Fusion.SynVar.Split.Subword
+import ADP.Fusion.SynVar.Split.Type
+
diff --git a/ADP/Fusion/SynVar/Split/Subword.hs b/ADP/Fusion/SynVar/Split/Subword.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/SynVar/Split/Subword.hs
@@ -0,0 +1,125 @@
+
+module ADP.Fusion.SynVar.Split.Subword where
+
+import Data.Strict.Tuple
+import Data.Proxy
+import Data.Vector.Fusion.Stream.Monadic
+import Data.Vector.Fusion.Stream.Size
+import Data.Vector.Fusion.Util (delay_inline)
+import Debug.Trace
+import GHC.TypeLits
+import Prelude hiding (map,mapM)
+import Data.Type.Equality
+
+import Data.PrimitiveArray hiding (map)
+
+import ADP.Fusion.Base
+import ADP.Fusion.SynVar.Array.Type
+import ADP.Fusion.SynVar.Backtrack
+import ADP.Fusion.SynVar.Split.Type
+
+
+
+-- * 'Fragment' and 'Final' instances for 'Split' / 'ITbl'.
+
+instance
+  ( Monad m
+  , Element ls Subword
+  , MkStream m ls Subword
+  ) => MkStream m (ls :!: Split uId Fragment (ITbl m arr j x)) Subword where
+  mkStream (ls :!: Split _) (IStatic ()) hh (Subword (i:.j))
+    = map (\s -> let (Subword (_:.l)) = getIdx s
+                 in  ElmSplitITbl Proxy () (subword l j) (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see TODO in @Split@) - minSize c))
+  mkStream (ls :!: Split _) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see above) - minSize c))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l) -- TODO - minSize c)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                    return $ Yield (ElmSplitITbl Proxy () kl (subword 0 0) s) (s:. z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
+instance
+  ( Monad m
+  , Element ls Subword
+  , MkStream m ls Subword
+  , SplitIxCol uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)
+  , (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword) :. Subword) ~ mix
+  ,  (PrimArrayOps arr (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword) :. Subword) x)
+  ) => MkStream m (ls :!: Split uId Final (ITbl m arr mix x)) Subword where
+  mkStream (ls :!: Split (ITbl _ _ c t elm)) (IStatic ()) hh (Subword (i:.j))
+    = map (\s -> let (Subword (_:.l)) = getIdx s
+                     fmbkm :: mix = collectIx (Proxy :: Proxy uId) s :. subword l j
+                 in  ElmSplitITbl Proxy (t ! fmbkm) (subword l j) (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see TODO in @Split@) - minSize c))
+  mkStream (ls :!: Split (ITbl _ _ c t _)) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO - minSize c))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l) -- TODO - minSize c)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                        fmbkm :: mix   = collectIx (Proxy :: Proxy uId) s :. kl
+                                    return $ Yield (ElmSplitITbl Proxy (t ! fmbkm) kl (subword 0 0) s) (s:. z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
+
+
+-- * 'Fragment' and 'Final' instances for 'Split' / @Backtrack@ 'ITbl'.
+
+instance
+  ( Monad mB
+  , Element ls Subword
+  , MkStream mB ls Subword
+  ) => MkStream mB (ls :!: Split uId Fragment (Backtrack (ITbl mF arr j x) mF mB r)) Subword where
+  mkStream (ls :!: Split _) (IStatic ()) hh (Subword (i:.j))
+    = map (\s -> let (Subword (_:.l)) = getIdx s
+                 in  ElmSplitBtITbl Proxy () (subword l j) (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see TODO in @Split@) - minSize c))
+  mkStream (ls :!: Split _) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see above) - minSize c))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l) -- TODO - minSize c)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                    return $ Yield (ElmSplitBtITbl Proxy () kl (subword 0 0) s) (s:. z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
+instance
+  ( Monad mB
+  , Element ls Subword
+  , MkStream mB ls Subword
+  , SplitIxCol uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)
+  , (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword) :. Subword) ~ mix
+  , (PrimArrayOps arr (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword) :. Subword) x)
+  ) => MkStream mB (ls :!: Split uId Final (Backtrack (ITbl mF arr mix x) mF mB r)) Subword where
+  mkStream (ls :!: Split (BtITbl c t bt)) (IStatic ()) hh (Subword (i:.j))
+    = mapM (\s -> let (Subword (_:.l)) = getIdx s
+                      lj               = subword l j
+                      fmbkm :: mix     = collectIx (Proxy :: Proxy uId) s :. lj
+                      (_,hhhh)         = bounds t -- This is an ugly hack, but we need a notation of higher bound from somewhere
+                  in  bt hhhh fmbkm >>= \ ~bb -> return $ ElmSplitBtITbl Proxy (t ! fmbkm,bb) lj (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO (see TODO in @Split@) - minSize c))
+  mkStream (ls :!: Split (BtITbl c t bt)) (IVariable ()) hh (Subword (i:.j))
+    = flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j)) -- TODO - minSize c))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l) -- TODO - minSize c)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                        fmbkm :: mix   = collectIx (Proxy :: Proxy uId) s :. kl
+                                        (_,hhhh)       = bounds t -- same ugly hack
+                                    bt hhhh fmbkm >>= \ ~bb -> return $ Yield (ElmSplitBtITbl Proxy (t ! fmbkm,bb) kl (subword 0 0) s) (s:. z-1)
+                      | otherwise = return $ Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
diff --git a/ADP/Fusion/SynVar/Split/Type.hs b/ADP/Fusion/SynVar/Split/Type.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/SynVar/Split/Type.hs
@@ -0,0 +1,186 @@
+
+-- |
+--
+-- NOTE /highly experimental/
+
+module ADP.Fusion.SynVar.Split.Type
+  ( module ADP.Fusion.SynVar.Split.Type
+  , Proxy (..)
+  ) where
+
+import Data.Proxy
+import Data.Strict.Tuple
+import Data.Vector.Fusion.Stream.Monadic
+import Data.Vector.Fusion.Stream.Size
+import Data.Vector.Fusion.Util (delay_inline)
+import Debug.Trace
+import GHC.TypeLits
+import Prelude hiding (map,mapM)
+import Data.Type.Equality
+
+import Data.PrimitiveArray hiding (map)
+
+import ADP.Fusion.Base
+import ADP.Fusion.SynVar.Array.Type
+import ADP.Fusion.SynVar.Backtrack
+
+
+
+data SplitType = Fragment | Final
+
+-- | The @Arg synVar@ means that we probably need to rewrite the internal
+-- type resolution now!
+
+type family CalcSplitType splitType varTy where
+  CalcSplitType Fragment varTy = ()
+  CalcSplitType Final    varTy = varTy
+
+-- | Should never fail?
+
+type family ArgTy argTy where
+--  ArgTy Z = Z
+  ArgTy (z:.x) = x
+
+-- | Wraps a normal non-terminal and attaches a type-level unique identier
+-- and z-ordering (with the unused @Z@ at @0@).
+--
+-- TODO attach empty/non-empty stuff (or get from non-splitted synvar?)
+--
+-- TODO re-introduce z-ordering later (once we have a sort fun)
+
+newtype Split (uId :: Symbol) {- (zOrder :: Nat) -} (splitType :: SplitType) synVar = Split { getSplit :: synVar }
+
+split :: Proxy (uId::Symbol) -> {- Proxy (zOrder::Nat) -> -} Proxy (splitType::SplitType) -> synVar -> Split uId splitType synVar
+split _ _ = Split
+{-# Inline split #-}
+
+--type Spl uId zOrder splitType = forall synVar . Split uId zOrder splitType synVar
+
+instance Build (Split uId splitType synVar)
+
+instance
+  ( Element ls i
+  ) => Element (ls :!: Split uId splitType (ITbl m arr j x)) i where
+  data Elm     (ls :!: Split uId splitType (ITbl m arr j x)) i = ElmSplitITbl !(Proxy uId) !(CalcSplitType splitType x) !i !i !(Elm ls i)
+  type Arg     (ls :!: Split uId splitType (ITbl m arr j x))   = Arg ls :. (CalcSplitType splitType x)
+  type RecElm  (ls :!: Split uId splitType (ITbl m arr j x)) i = Elm ls i
+  getArg (ElmSplitITbl _ x _ _ ls) = getArg ls :. x
+  getIdx (ElmSplitITbl _ _ i _ _ ) = i
+  getOmx (ElmSplitITbl _ _ _ o _ ) = o
+  getElm (ElmSplitITbl _ _ _ _ ls) = ls
+  {-# Inline getArg #-}
+  {-# Inline getIdx #-}
+  {-# Inline getOmx #-}
+  {-# Inline getElm #-}
+
+instance
+  ( Element ls i
+  ) => Element (ls :!: Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r)) i where
+  data Elm     (ls :!: Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r)) i = ElmSplitBtITbl !(Proxy uId) !(CalcSplitType splitType (x, [r])) !i !i !(Elm ls i)
+  type Arg     (ls :!: Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r))   = Arg ls :. (CalcSplitType splitType (x,[r]))
+  type RecElm  (ls :!: Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r)) i = Elm ls i
+  getArg (ElmSplitBtITbl _ xs _ _ ls) = getArg ls :. xs
+  getIdx (ElmSplitBtITbl _ _ i _ _ ) = i
+  getOmx (ElmSplitBtITbl _ _ _ o _ ) = o
+  getElm (ElmSplitBtITbl _ _ _ _ ls) = ls
+  {-# Inline getArg #-}
+  {-# Inline getIdx #-}
+  {-# Inline getOmx #-}
+  {-# Inline getElm #-}
+
+
+
+-- | 'collectIx' gobbles up indices that are tagged with the same symbolic
+-- identifier.
+
+collectIx
+  :: forall uId ls i .
+     ( SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i)
+     )
+  => Proxy uId -> Elm ls i -> SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)
+collectIx p e = splitIxCol p (Proxy :: Proxy (SameSid uId (Elm ls i))) e
+
+-- | Closed type family that gives us a (type) function for type symbol
+-- equality.
+
+type family SameSid uId elm :: Bool where
+  SameSid uId (Elm (ls :!: Split sId splitType synVar) i) = uId == sId
+  SameSid uId (Elm (ls :!: TermSymbol a b            ) i) = SameSid uId (TermSymbol a b)
+  SameSid uId M                                           = False
+  SameSid uId (TermSymbol a (Split sId splitType synVar)) = OR (uId == sId) (SameSid uId a)
+  SameSid uId (Elm (ls :!: l                         ) i) = False
+
+-- | Type-level @(||)@
+
+type family OR a b where
+  OR False False = False
+  OR a     b     = True
+
+-- | @x ++ y@ but for inductive tuples.
+--
+-- TODO move to PrimitiveArray
+
+class Zconcat x y where
+  type Zpp x y :: *
+  zconcat :: x -> y -> Zpp x y
+
+instance Zconcat x Z where
+  type Zpp x Z = x
+  zconcat x Z = x
+  {-# Inline zconcat #-}
+
+instance 
+  ( Zconcat x z
+  ) => Zconcat x (z:.y) where
+  type Zpp x (z:.y) = Zpp x z :. y
+  zconcat x (z:.y) = zconcat x z :. y
+  {-# Inline zconcat #-}
+
+-- WORKS
+
+-- | Actually collect split indices based on if we managed to find the
+-- right @Split@ synvar (based on the right symbol).
+
+class SplitIxCol (uId::Symbol) (b::Bool) e where
+  type SplitIxTy uId b e :: *
+  splitIxCol :: Proxy uId -> Proxy b -> e -> SplitIxTy uId b e
+
+
+
+instance SplitIxCol uId b (Elm S i) where
+  type SplitIxTy uId b (Elm S i) = Z
+  splitIxCol p b (ElmS _ _) = Z
+  {-# Inline splitIxCol #-}
+
+
+instance
+  ( SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i)
+  , Element (ls :!: l) i
+  , RecElm (ls :!: l) i ~ Elm ls i
+  ) => SplitIxCol uId False (Elm (ls :!: l) i) where
+  type SplitIxTy uId False (Elm (ls :!: l) i) = SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)
+  splitIxCol p b e = collectIx p (getElm e)
+  {-# Inline splitIxCol #-}
+
+instance
+  ( SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i)
+  ) => SplitIxCol   uId True (Elm (ls :!: Split sId splitType (ITbl m arr j x)) i) where
+  type SplitIxTy uId True (Elm (ls :!: Split sId splitType (ITbl m arr j x)) i) = SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i) :. i
+  splitIxCol p b (ElmSplitITbl _ _ i _ e) = collectIx p e :. i
+  {-# Inline splitIxCol #-}
+
+instance
+  ( SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i)
+  ) => SplitIxCol   uId True (Elm (ls :!: Split sId splitType (Backtrack (ITbl mF arr j x) mF mB r)) i) where
+  type SplitIxTy uId True (Elm (ls :!: Split sId splitType (Backtrack (ITbl mF arr j x) mF mB r)) i) = SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i) :. i
+  splitIxCol p b (ElmSplitBtITbl _ _ i _ e) = collectIx p e :. i
+  {-# Inline splitIxCol #-}
+
+instance
+  ( SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i)
+  , Zconcat (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) (SplitIxTy uId (SameSid uId (TermSymbol a b)) (TermSymbol a b))
+  ) => SplitIxCol uId True (Elm (ls :!: TermSymbol a b) i) where
+  type SplitIxTy uId True (Elm (ls :!: TermSymbol a b) i) = Zpp (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) (SplitIxTy uId (SameSid uId (TermSymbol a b)) (TermSymbol a b))
+  splitIxCol p b (ElmTS t i _ e) = collectIx p e `zconcat` (undefined p t :: SplitIxTy uId (SameSid uId (TermSymbol a b)) (TermSymbol a b))
+  {-# Inline splitIxCol #-}
+
diff --git a/ADP/Fusion/TH.hs b/ADP/Fusion/TH.hs
--- a/ADP/Fusion/TH.hs
+++ b/ADP/Fusion/TH.hs
@@ -14,6 +14,7 @@
 module ADP.Fusion.TH
   ( makeAlgebraProduct
   , (<||)
+  , (***)
   ) where
 
 import           Data.List
@@ -22,12 +23,12 @@
 import           Language.Haskell.TH.Syntax
 import qualified Data.Vector.Fusion.Stream.Monadic as SM
 
-import           ADP.Fusion.TH.Backtrack (makeBacktrackingProductInstance,(<||))
+import           ADP.Fusion.TH.Backtrack -- (makeBacktrackingProductInstance,(<||))
 import           ADP.Fusion.TH.Common (getRuleResultType)
 
 
 
-makeAlgebraProduct = makeBacktrackingProductInstance
+makeAlgebraProduct = makeProductInstances
 
 {-
 -- | Create the algebra product function from a signature type constructor.
diff --git a/ADP/Fusion/TH/Backtrack.hs b/ADP/Fusion/TH/Backtrack.hs
--- a/ADP/Fusion/TH/Backtrack.hs
+++ b/ADP/Fusion/TH/Backtrack.hs
@@ -6,33 +6,48 @@
 
 module ADP.Fusion.TH.Backtrack where
 
+import           Control.Applicative ( (<$>) )
+import           Control.Monad
+import           Control.Monad.Primitive (PrimState, PrimMonad)
 import           Data.List
 import           Data.Tuple.Select
+import           Data.Vector.Fusion.Stream.Monadic (Stream(..))
+import           Debug.Trace
 import           Language.Haskell.TH
+import           Language.Haskell.TH.Instances
 import           Language.Haskell.TH.Syntax
-import qualified Data.Vector.Fusion.Stream.Monadic as SM
-import qualified Data.Vector.Mutable as VM
-import qualified Data.Vector.Generic.Mutable as VGM
+import qualified Data.Map.Strict as M
 import qualified Data.Vector as V
+import qualified Data.Vector.Fusion.Stream.Monadic as SM
 import qualified Data.Vector.Generic as VG
-import           Control.Monad.Primitive (PrimState, PrimMonad)
-import           Data.Vector.Fusion.Stream.Monadic (Stream(..))
-import           Debug.Trace
+import qualified Data.Vector.Generic.Mutable as VGM
+import qualified Data.Vector.Mutable as VM
 
+import           Data.PrimitiveArray ( (:.)(..) , Z(..) )
+
 import           ADP.Fusion.TH.Common
 
 
 
--- | The type class of algebra products. We have the forward signature
--- @sigF@ and the backtracking signature @sigB@. Combined via @(<||)@ we
--- have a new signature @SigR@.
+-- | @Backtracking@ products of @f@ and @b@. Choice in @f@ needs to be
+-- reduced to a scalar value. It is then compared to the @fst@ values
+-- in @b@. From those, @choice b@ selects.
 
-class BacktrackingProduct sigF sigB where
-  type SigR sigF sigB :: *
-  (<||) :: sigF -> sigB -> SigR sigF sigB
+class ProductBacktracking sigF sigB where
+  type SigBacktracking sigF sigB :: *
+  (<||) :: sigF -> sigB -> SigBacktracking sigF sigB
 
-makeBacktrackingProductInstance :: Name -> Q [Dec]
-makeBacktrackingProductInstance tyconName = do
+-- | The ADP-established product operation. Returns a vector of results,
+-- along the lines of what the ADP @f *** b@ provides.
+
+class ProductCombining sigF sigB where
+  type SigCombining sigF sigB :: *
+  (***) :: sigF -> sigB -> SigCombining sigF sigB
+
+-- | Creates instances for all products given a signature data type.
+
+makeProductInstances :: Name -> Q [Dec]
+makeProductInstances tyconName = do
   t <- reify tyconName
   case t of
     TyConI (DataD ctx tyConName args cs d) -> do
@@ -42,20 +57,37 @@
           let Just (h,m',x,r) = getObjectiveNames funs
           mL <- newName "mL"
           xL <- newName "xL"
+          rL <- newName "rL"
           mR <- newName "mR"
           xR <- newName "xR"
           rR <- newName "rR"
-          let lType    = buildLeftType  tyconName (m', x, r) (mL, xL)        args
+--          let lType    = buildLeftType  tyconName (m', x, r) (mL, xL)        args
+          let lType    = buildRightType tyconName (m', x, r) (mL, xL, rL)    args
           let rType    = buildRightType tyconName (m', x, r) (mR, xR, rR)    args
-          let sigRType = buildSigRType  tyconName (m', x, r) xL (mR, xR, rR) args
           let (fs,hs) = partition ((`notElem` [h]) . sel1) funs
-          Clause ps (NormalB b) ds <- genClauseBacktrack dataconName funs fs hs
-          i <- [d| instance (Monad $(varT mL), Monad $(varT mR), Eq $(varT xL), $(varT mL) ~ $(varT mR)) => BacktrackingProduct $(return lType) $(return rType) where
-                     type SigR $(return lType) $(return rType) = $(return sigRType)
-                     (<||) = $(return $ LamE ps $ LetE ds b)
-                     {-# Inline (<||) #-}
-               |]
-          return i
+          let sigBType = buildSigBacktrackingType  tyconName (m', x, r) xL (mR, xR, rR) args
+          Clause psB (NormalB bB) dsB <- genAlgProdFunctions buildBacktrackingChoice dataconName funs fs hs
+          iB <- [d| instance (Monad $(varT mL), Monad $(varT mR), Eq $(varT xL), $(varT mL) ~ $(varT mR), $(varT xL) ~ $(varT rL))
+                      => ProductBacktracking $(return lType) $(return rType) where
+                          type SigBacktracking $(return lType) $(return rType) = $(return sigBType)
+                          (<||) = $(return $ LamE psB $ LetE dsB bB)
+                          {-# Inline (<||) #-}
+                |]
+          -- TODO might well be that this doesn't work because we re-use
+          -- type names ...
+          vG <- newName "vG"
+          sigPType <- buildSigCombiningType tyconName vG (m', x, r) (mL, xL, rL) (mR, xR, rR) args
+          Clause psC (NormalB bC) dsC <- genAlgProdFunctions buildCombiningChoice    dataconName funs fs hs
+          iC <- [d| instance (Monad $(varT mL), Monad $(varT mR), Eq $(varT xL), $(varT mL) ~ $(varT mR) {- , VG.Vector $(varT vG) ($(varT rL),$(varT rR)) -} )
+                      => ProductCombining $(return lType) $(return rType) where
+                          type SigCombining $(return lType) $(return rType) = $(return sigPType)
+                          (***) = undefined
+                          {-
+                           - (***) = $(return $ LamE psC $ LetE dsC bC)
+                           - -}
+                          {-# Inline (***) #-}
+                |]
+          return $ iB -- ++ iC
 
 -- | Returns the 'Name' of the monad variable.
 
@@ -76,6 +108,13 @@
           | otherwise             = go xs
         go ( _ : xs) = go xs
 
+
+
+-- * Constructions for the different algebra types.
+
+-- | The left algebra type. Assumes that in @choice :: Stream m x -> m r@
+-- we have that @x ~ r@.
+
 buildLeftType :: Name -> (Name, Name, Name) -> (Name, Name) -> [TyVarBndr] -> Type
 buildLeftType tycon (m, x, r) (mL, xL) = foldl AppT (ConT tycon) . map (VarT . go)
   where go (PlainTV z)
@@ -84,19 +123,24 @@
           | z == r        = xL  -- stream and return type are the same
           | otherwise     = z   -- everything else can stay as is
         go (KindedTV z _) = go (PlainTV z)
---        go s              = error $ "buildLeftType: " ++ show s
 
+-- | Here, we do not set any restrictions on the types @m@ and @r@.
+
 buildRightType :: Name -> (Name, Name, Name) -> (Name, Name, Name) -> [TyVarBndr] -> Type
 buildRightType tycon (m, x, r) (mR, xR, rR) = foldl AppT (ConT tycon) . map (VarT . go)
   where go (PlainTV z)
-          | z == m    = mR
-          | z == x    = xR
-          | z == r    = rR
-          | otherwise = z
+          | z == m    = mR  -- have discovered a monadic type
+          | z == x    = xR  -- have discovered a type that is equal to the stream type (and hence we have a synvar type)
+          | z == r    = rR  -- have discovered a type that is equal to the result type (for @<||@) equal to the stream type, hence synvar
+          | otherwise = z   -- this is a terminal or a terminal stack (we don't care)
         go (KindedTV z _) = go (PlainTV z)
 
-buildSigRType :: Name -> (Name, Name, Name) -> (Name) -> (Name, Name, Name) -> [TyVarBndr] -> Type
-buildSigRType tycon (m, x, r) (xL) (mR, xR, rR) = foldl AppT (ConT tycon) . map go
+-- | Build up the type for backtracking. We want laziness in the right
+-- return type. Hence, we have @AppT ListT (VarT xR)@ ; i.e. we want to
+-- return results in a list.
+
+buildSigBacktrackingType :: Name -> (Name, Name, Name) -> (Name) -> (Name, Name, Name) -> [TyVarBndr] -> Type
+buildSigBacktrackingType tycon (m, x, r) (xL) (mR, xR, rR) = foldl AppT (ConT tycon) . map go
   where go (PlainTV z)
           | z == m    = VarT mR
           | z == x    = (AppT (AppT (TupleT 2) (VarT xL)) (AppT ListT (VarT xR)))
@@ -104,21 +148,38 @@
           | otherwise = VarT z
         go (KindedTV z _) = go (PlainTV z)
 
--- |
+-- | Build up the type for backtracking. We want laziness in the right
+-- return type. Hence, we have @AppT ListT (VarT xR)@.
 
-genClauseBacktrack
-  :: Name
+buildSigCombiningType :: Name -> Name -> (Name, Name, Name) -> (Name, Name, Name) -> (Name, Name, Name) -> [TyVarBndr] -> TypeQ
+buildSigCombiningType tycon vG (m, x, r) (mL, xL, rL) (mR, xR, rR) = foldl appT (conT tycon) . map go
+  where go (PlainTV z)
+          | z == m    = varT mR
+          | z == x    = [t| ($(varT xL) , $(varT xR)) |]
+          | z == r    = [t| V.Vector ($(varT rL) , $(varT rR)) |]
+          | otherwise = varT z
+        go (KindedTV z _) = go (PlainTV z)
+
+
+
+-- *
+
+-- | Build up attribute and choice function. Here, we actually bind the
+-- left and right algebra to @l@ and @r@.
+
+genAlgProdFunctions
+  :: Choice
+  -> Name
   -> [VarStrictType]
   -> [VarStrictType]
   -> [VarStrictType]
   -> Q Clause
-genClauseBacktrack conName allFunNames evalFunNames choiceFunNames = do
+genAlgProdFunctions choice conName allFunNames evalFunNames choiceFunNames = do
   let nonTermNames = nub . map getRuleResultType $ evalFunNames
   -- bind the l'eft and r'ight variable of the two algebras we want to join,
   -- also create unique names for the function names we shall bind later.
   nameL <- newName "l"
   varL  <- varP nameL
-  -- TODO automate discovery of choice functions?
   fnmsL <- sequence $ replicate (length allFunNames) (newName "fnamL")
   nameR <- newName "r"
   varR  <- varP nameR
@@ -127,26 +188,29 @@
   whereL <- valD (conP conName (map varP fnmsL)) (normalB $ varE nameL) []
   whereR <- valD (conP conName (map varP fnmsR)) (normalB $ varE nameR) []
   rce <- recConE conName
-          $  zipWith3 (genChoiceFunction) (drop (length evalFunNames) fnmsL) (drop (length evalFunNames) fnmsR) choiceFunNames
+          $  zipWith3 (genChoiceFunction choice) (drop (length evalFunNames) fnmsL) (drop (length evalFunNames) fnmsR) choiceFunNames
           ++ zipWith3 (genAttributeFunction nonTermNames) fnmsL fnmsR evalFunNames
   -- build the function pairs
   -- to keep our sanity, lets print this stuff
   let cls = Clause [varL, varR] (NormalB rce) [whereL,whereR]
   return cls
 
--- |
+-- | Simple wrapper for creating the choice fun expression.
 
 genChoiceFunction
-  :: Name
+  :: Choice
   -> Name
+  -> Name
   -> VarStrictType
   -> Q (Name,Exp)
-genChoiceFunction hL hR (name,_,t) = do
-  exp <- buildBacktrackingChoice hL hR
+genChoiceFunction choice hL hR (name,_,t) = do
+  exp <- choice hL hR
   return (name,exp)
 
 
--- |
+-- | We take the left and right function name for one attribute and build
+-- up the combined attribute function. Mostly a wrapper around
+-- 'recBuildLampat' which does the main work.
 --
 -- TODO need fun names from @l@ and @r@
 
@@ -157,24 +221,84 @@
   -> VarStrictType
   -> Q (Name,Exp)
 genAttributeFunction nts fL fR (name,_,t) = do
-  (lamPat,funL,funR) <-recBuildLamPat nts fL fR (init $ getRuleSynVarNames t) -- @init@ since we don't want the result as a parameter
+  (lamPat,funL,funR) <-recBuildLamPat nts fL fR (init $ getRuleSynVarNames nts t) -- @init@ since we don't want the result as a parameter
   let exp = LamE lamPat $ TupE [funL,funR]
   return (name,exp)
 
--- |
+-- | Now things become trickly. We are given all non-terminal names (to
+-- differentiate between a terminal (stack) and a syntactic variable; the
+-- left and right function; and the arguments to this attribute function
+-- (except the result parameter). We are given the latter as a result to an
+-- earlier call to 'getRuleSynVarNames'.
+--
+-- We now look at each argument and determine wether it is a syntactic
+-- variable. If so, then we actually have a tuple arguments @(x,ys)@ where
+-- @x@ has to optimized value and @ys@ the backtracking list. The left
+-- function receives just @x@ in this case. For the right function, things
+-- are more complicated, since we have to flatten lists. See 'buildRns'.
+--
+-- Terminals are always given "as is" since we do not have a need for
+-- tupled-up information as we have for syntactic variables.
 
-recBuildLamPat :: [Name] -> Name -> Name -> [Name] -> Q ([Pat], Exp, Exp)
+recBuildLamPat
+  :: [Name]   -- ^ all non-terminal names
+  -> Name     -- ^ left attribute function
+  -> Name     -- ^ right attribute function
+  -> [ArgTy Name]  -- ^ all arguments to the attribute function
+  -> Q ([Pat], Exp, Exp)
 recBuildLamPat nts fL' fR' ts = do
   -- here we just run through all arguments, either creating an @x@ and
   -- a @ys@ for a non-term or a @t@ for a term.
-  ps <- sequence [ if t `elem` nts then tupP [newName "x" >>= varP, newName "ys" >>= varP] else (newName "t" >>= varP) | t<-ts]
-  let buildLfun f (TupP [VarP v,_]) = appE f (varE v)
-      buildLfun f (VarP v         ) = appE f (varE v)
-  lfun <- foldl buildLfun (varE fL') ps
+  -- ps <- sequence [ if t `elem` nts then tupP [newName "x" >>= varP, newName "ys" >>= varP] else (newName "t" >>= varP) | t<-ts]
+  ps <- mapM argTyArgs ts
+  {-
+  let buildLfun f (SynVar (TupP [VarP v,_])) = appE f (varE v)
+      buildLfun f (Term   (VarP v         )) = appE f (varE v)
+      buildLfun f (StackedVars vs) =
+        let
+        in  error "buildLfun: WRITE ME" -- appE f (varE $ mkName "foo")
+  -}
+  lamPat <- buildLamPat ps
+  lfun <- buildLns (VarE fL') ps -- foldl buildLfun (varE fL') ps
   rfun <- buildRns (VarE fR') ps
-  return (ps, lfun, rfun)
+  return (lamPat, lfun, rfun)
 
+buildLamPat :: [ArgTy Pat] -> Q [Pat]
+buildLamPat = mapM go where
+  go (SynVar      p ) = return p
+  go (Term        p ) = return p
+  go (StackedVars ps) = build ps
+  build :: [ArgTy Pat] -> Q Pat
+  build = foldl (\s v -> [p| $(s) :. $(return v) |]) [p|Z|] . map get
+  get :: ArgTy Pat -> Pat
+  get (SynVar p) = p
+  get (Term   p) = p
 
+-- | Look at the argument type and build the capturing variables. In
+-- particular captures synvar arguments with a 2-tuple @(x,ys)@.
+
+argTyArgs :: ArgTy Name -> Q (ArgTy Pat)
+argTyArgs (SynVar n) = SynVar <$> tupP [newName "x" >>= varP , newName "ys" >>= varP]
+argTyArgs (Term n)          = Term <$> (newName "t" >>= varP)
+argTyArgs (StackedTerms _)  = Term <$> (newName "t" >>= varP) -- !!!
+argTyArgs (StackedVars vs)  = StackedVars <$> mapM argTyArgs vs
+argTyArgs NilVar            = Term <$> (newName "t" >>= varP)
+argTyArgs (Result _)        = error "argTyArgs: should not receive @Result@"
+
+buildLns
+  :: Exp
+  -> [ArgTy Pat]
+  -> ExpQ
+buildLns f' ps = foldl go (return f') ps
+  where go :: ExpQ -> ArgTy Pat -> ExpQ
+        go f (SynVar      (TupP [VarP v,_])) = appE f (varE v)
+        go f (Term        (VarP v         )) = appE f (varE v)
+        go f (StackedVars vs               ) = appE f (build vs)
+        build :: [ArgTy Pat] -> ExpQ
+        build = foldl (\s v -> [| $(s) :. $(varE v) |]) [|Z|] . map get
+        get (SynVar (TupP [VarP v,_])) = v
+        get (Term   (VarP t)         ) = t
+
 -- |
 --
 -- NOTE
@@ -187,8 +311,40 @@
 buildRns
   :: Exp
 --  -> [Name]
-  -> [Pat]
+  -> [ArgTy Pat]
   -> ExpQ
+buildRns f' ps = do
+  -- get all synvars, shallow or deep and create a new name to bind
+  -- individual parts to.
+  sy :: M.Map Pat Name <- M.fromList <$> (mapM (\s -> newName "y" >>= \y -> return (s,y)) $ concatMap flattenSynVars ps)
+  -- bind them for the right part of the list expression (even though they
+  -- are left in @CompE@. We don't use @sy@ directly to keep the order in
+  -- which the comprehensions run.
+  let rs = map (\k@(TupP [_,VarP v]) -> BindS (VarP $ sy M.! k) (VarE v)) $ concatMap flattenSynVars ps
+  let go :: ExpQ -> ArgTy Pat -> ExpQ
+      go f (SynVar      k       ) = appE f (varE $ sy M.! k) -- needed like this, because we need the @y@ in @y <- ys@
+      go f (Term        (VarP v)) = appE f (varE v)
+      go f (StackedVars vs      ) = appE f (foldl build [|Z|] vs)
+      build :: ExpQ -> ArgTy Pat -> ExpQ
+      build s (SynVar k       ) = [| $(s) :. $(varE $ sy M.! k) |]
+      build s (Term   (VarP v)) = [| $(s) :. $(varE v)          |]
+  funApp <- foldl go (return f') ps
+  return . CompE $ rs ++ [NoBindS funApp]
+
+{-
+  -- helper function for the argument build-up
+  let go :: [ArgTy Pat] -> [Name]
+      go [] = []
+      go ((SynVar      k       ):ks) = sy M.! k  : go ks
+      go ((Term        (VarP v)):ks) = v         : go ks -- should also cover StackedTerms, NilVar ! (because we build this earlier in @argTypArgs@)
+      go ((StackedVars ls      ):ks) = (error "here") : go ks -- need to work more
+  -- more verbose build-up of the arguments for @funApp@.
+  let xs = go ps
+  -- function application
+  funApp <- noBindS $ foldl (\g z -> appE g (varE z)) (return f) xs
+  return . CompE $ rs ++ [funApp]
+-}
+{-
 buildRns f ps = do
   ys <- sequence [ newName "y" | TupP [_,VarP v] <- ps ]
   let vs = zipWith (\y v -> (BindS (VarP y) (VarE v))) ys [ v | TupP [_,VarP v] <- ps ]
@@ -199,7 +355,14 @@
         go (VarP v : gs) ys     = v : go gs ys  -- keep terminal binders
         go (TupP _ : gs) (v:ys) = v : go gs ys  -- insert new binders
         go as bs = error $ show ("not done?", as, bs)
+-}
 
+-- | Type for backtracking functions.
+--
+-- Not too interesting, mostly to keep track of @choice@.
+
+type Choice = Name -> Name -> Q Exp
+
 -- | Build up the backtracking choice function. This choice function will
 -- backtrack based on the first result, then return only the second.
 --
@@ -213,7 +376,7 @@
 --
 -- This means strict optimization AND lazy backtracking
 
-buildBacktrackingChoice :: Name -> Name -> Q Exp
+buildBacktrackingChoice :: Choice
 buildBacktrackingChoice hL' hR' =
   [| \xs -> do        -- first, create a boxed, mutable vector from the results
                ysM <- streamToVector xs -- VGM.unstream xs :: m (VM.MVector s (t1,[t2]))
@@ -222,10 +385,40 @@
                      -- second choice on snd elements, then concat'ed up
                      -- TODO good candidate for rewriting into flatten
                      -- operation!
-               $(varE hR') $ SM.concatMap (SM.fromList . snd) $ SM.filter ((hFres==) . fst) $ vectorToStream ysM
+               {-
+                - $(varE hR') $ SM.concatMap (SM.fromList . snd) $ SM.filter ((hFres==) . fst) $ vectorToStream ysM
+                -}
+               $(varE hR') $ SM.fromList $ concatMap snd $ filter ((hFres==) . fst) $ V.toList ysM
   |]
 
+buildCombiningChoice :: Choice
+buildCombiningChoice hL' hR' =
+  [| \xs -> do       -- first, create a boxed, mutable vector from the results
+               --ys <- streamToVector xs
+               --      -- apply first choice
+               --fs <- $(varE hL') $ SM.map fst $ vectorToStream ys
+               --      -- generate a vector of vectors, one for each
+               --      -- surviving @f@
+               --vs <- V.forM fs $ \f -> do
+               --        -- keep only those @ys@ that have @f@
+               --        let as = V.filter ((f==) . fst) ys
+               --        -- apply @hR'@ to those, but only to the @snd@
+               --        -- elements
+               --        bs <- streamToVector =<< $(varE hR') $ SM.map snd $ vectorToStream $ as
+               --        -- return the combined result, with @f@ attached.
+               --        return $ V.map (\z -> (f,z)) bs
+               undefined
+               {-
+                - $ V.concat $ V.toList vs
+                -}
+               -- TODO we should return a @newtype Many x = forall (G.Vector v x) => Many { v x }
+               -- Together with a closed type family, this gives us a good
+               -- way to encode that we have classified DP
+  |]
+
 -- | Transform a monadic stream monadically into a vector.
+--
+-- TODO Improve code!
 
 streamToVector :: (Monad m) => SM.Stream m x -> m (V.Vector x)
 streamToVector xs = do
@@ -235,6 +428,8 @@
 {-# Inline streamToVector #-}
 
 -- | Transform a vector into a monadic stream.
+--
+-- TODO improve code!
 
 vectorToStream :: (Monad m) => V.Vector x -> SM.Stream m x
 vectorToStream = SM.fromList . V.toList
@@ -254,12 +449,76 @@
 -- AppT (AppT ArrowT (AppT (AppT (ConT Data.Array.Repa.Index.:.) (AppT (AppT (ConT Data.Array.Repa.Index.:.) (ConT Data.Array.Repa.Index.Z)) (VarT c_1627675270))) (VarT c_1627675270))) (VarT x_1627675265)
 -- @
 
-getRuleSynVarNames :: Type -> [Name]
-getRuleSynVarNames t' = go t' where
+getRuleSynVarNames :: [Name]-> Type -> [ArgTy Name] -- [Name]
+getRuleSynVarNames nts t' = go t' where
   go t
+    | VarT x <- t                          = [Result x]
+    | AppT (AppT ArrowT (VarT x)  ) y <- t = (if x `elem` nts then SynVar x else Term x) : go y
+    | AppT (AppT ArrowT (TupleT 0)) y <- t = NilVar : go y
+    | AppT (AppT ArrowT s         ) y <- t = stacked s : go y
+    | otherwise                            = error $ "getRuleSynVarNames error: " ++ show t ++ "    in:    " ++ show t'
+  stacked s = if null [ () | SynVar _ <- xs ] then StackedTerms xs else StackedVars xs
+    where xs = reverse $ stckd s
+          stckd (ConT z) | z == ''Z = []
+          stckd (AppT a (TupleT 0)) = NilVar : stckd a
+          stckd (AppT a (VarT x)  ) = (if x `elem` nts then SynVar x else Term x) : stckd a
+          stckd (AppT (ConT c) a  ) | c == ''(:.) = stckd a
+          stckd err = error $ "stckd" ++ show err
+
+{-
+(AppT (AppT (ConT Data.PrimitiveArray.Index.Class.:.)
+            (AppT (AppT (ConT Data.PrimitiveArray.Index.Class.:.)
+                        (ConT Data.PrimitiveArray.Index.Class.Z)
+                  )
+                  (VarT x_1627774371)
+            )
+      )
+      (TupleT 0)
+)
+-}
+
+{-
+getRuleSynVarNames nts t' = undefined where -- go t' where
+  go t
     | VarT x <- t = [x]
-    | AppT (AppT ArrowT (VarT x  )) y <- t = x : go y   -- this is a syntactic variable, return the name that the incoming data is bound to
+    | AppT (AppT ArrowT (VarT x  )) y <- t = x : go y   -- this is a single-dim variable, return the name that the incoming data is bound to (not necessarily syntactic)
     | AppT (AppT ArrowT (AppT _ _)) y <- t = mkName "[]" : go y   -- this captures that we have a multi-dim terminal.
     | AppT (AppT ArrowT (TupleT 0)) y <- t = mkName "()" : go y   -- this case captures things like @nil :: () -> x@ for rules like @nil <<< Epsilon@.
     | otherwise            = error $ "getRuleSynVarNames error: " ++ show t ++ "    in:    " ++ show t'
+-}
+
+data ArgTy x
+  -- | This @SynVar@ spans the full column of tapes; i.e. it is a normal
+  -- syntactic variable.
+  = SynVar { synVarName :: x }
+  -- | We have just a single-tape grammar and as such just
+  -- a single-dimensional terminal. We call this term, because
+  -- @StackedTerms@ will be rewritten to just @Term@!
+  | Term { termName :: x }
+  -- | We have a multi-tape grammar with a stack of just terminals. We
+  -- normally can ignore the contents in the functions above, but keep them
+  -- anyway.
+  | StackedTerms { stackedTerms :: [ArgTy x] }
+  -- | We have a multi-tape grammar, but the stack contains a mixture of
+  -- @ArgTy@s.
+  | StackedVars { stackedVars :: [ArgTy x] }
+  -- | A single-dim @()@ case
+  | NilVar
+  -- | The result type name
+  | Result { result :: x }
+  deriving (Show,Eq)
+
+unpackArgTy :: Show x => ArgTy x -> x
+unpackArgTy = go
+  where go (SynVar x) = x
+        go (Term   x) = x
+        go (Result x) = x
+        go err        = error $ "unpackArgTy " ++ show err
+
+-- | Get all synvars, even if deep in a stack
+
+flattenSynVars :: ArgTy x -> [x]
+flattenSynVars (SynVar x)       = [x]
+flattenSynVars (StackedVars xs) = concatMap flattenSynVars xs
+flattenSynVars _                = []
 
diff --git a/ADP/Fusion/Term/Chr/Point.hs b/ADP/Fusion/Term/Chr/Point.hs
--- a/ADP/Fusion/Term/Chr/Point.hs
+++ b/ADP/Fusion/Term/Chr/Point.hs
@@ -61,7 +61,7 @@
     . S.map (\(S5 s zi zo (is:.i) (os:.o)) -> S5 s (zi:.i) (zo:.o) is os)
     -}
   terminalStream (a:|Chr f (!v)) (sv:._) (is:.i@(PointL _))
-    = S.map (\(S6 s (zi:.PointL k) (zo:.PointL l) is os e) -> S6 s zi zo (is:.PointL (k+1)) (os:.PointL 0) (e:.f v (l-1)))
+    = S.map (\(S6 s (zi:.PointL k) (zo:.PointL l) is os e) -> S6 s zi zo (is:.PointL (k+1)) (os:.PointL 0) (e:.f v (l-1))) -- TODO is the @l-1@ even right? is this part even called?
     . iPackTerminalStream a sv (is:.i)
     {-
     . terminalStream a sv is
diff --git a/ADP/Fusion/Term/Chr/Subword.hs b/ADP/Fusion/Term/Chr/Subword.hs
--- a/ADP/Fusion/Term/Chr/Subword.hs
+++ b/ADP/Fusion/Term/Chr/Subword.hs
@@ -30,8 +30,6 @@
     $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j-1))
   {-# Inline mkStream #-}
 
-
-
 instance
   ( Monad m
   , Element ls (Outside Subword)
@@ -58,4 +56,26 @@
                  in  ElmChr (f xs k) (O $ subword k (k+1)) (getOmx s) s)
     $ mkStream ls (OLeftOf (di+1:.dj)) u ij
   {-# Inline mkStream #-}
+
+
+
+instance
+  ( Monad m
+  , TerminalStream m a is
+  ) => TerminalStream m (TermSymbol a (Chr r x)) (is:.Subword) where
+  terminalStream (a:|Chr f v) (sv:.IStatic _) (is:.ix@(Subword (i:.j)))
+    -- TODO check if 'staticCheck' breaks fusion!!!
+    = staticCheck (i>=0 && i<j && j<=VG.length v)
+    . S.map (\(S6 s (zi:._) (zo:._) is os e) -> S6 s zi zo (is:.subword (j-1) j) (os:.subword 0 0) (e:.f v (j-1)))
+    . iPackTerminalStream a sv (is:.ix)
+  terminalStream (a:|Chr f v) (sv:.IVariable _) (is:.ix@(Subword (i:.j)))
+    = S.map (\(S6 s (zi:.Subword (_:.l)) (zo:._) is os e) -> S6 s zi zo (is:.subword l (l+1)) (os:.subword 0 0) (e:.f v l))
+    . iPackTerminalStream a sv (is:.ix)
+  {-# Inline terminalStream #-}
+
+instance TermStaticVar (Chr r x) Subword where
+  termStaticVar _ sv _ = sv
+  termStreamIndex _ _ (Subword (i:.j)) = subword i (j-1)
+  {-# Inline [0] termStaticVar   #-}
+  {-# Inline [0] termStreamIndex #-}
 
diff --git a/ADP/Fusion/Term/Chr/Type.hs b/ADP/Fusion/Term/Chr/Type.hs
--- a/ADP/Fusion/Term/Chr/Type.hs
+++ b/ADP/Fusion/Term/Chr/Type.hs
@@ -17,15 +17,14 @@
 
 data Chr r x where
   Chr :: VG.Vector v x
-      => !(v x -> Int -> r)
-      -> !(v x)
+      => (v x -> Int -> r)
+      -> (v x)
       -> Chr r x
 
 -- | smart constructor for regular 1-character parsers
 
---chr xs = Chr VG.unsafeIndex xs
-chr xs = Chr (VG.unsafeIndex) xs
---chr xs = Chr (VG.!) xs
+chr :: VG.Vector v x => v x -> Chr x x
+chr = Chr VG.unsafeIndex
 {-# Inline chr #-}
 
 -- | Smart constructor for Maybe Peeking, followed by a character.
diff --git a/ADP/Fusion/Term/Deletion.hs b/ADP/Fusion/Term/Deletion.hs
--- a/ADP/Fusion/Term/Deletion.hs
+++ b/ADP/Fusion/Term/Deletion.hs
@@ -2,9 +2,11 @@
 module ADP.Fusion.Term.Deletion
   ( module ADP.Fusion.Term.Deletion.Type
   , module ADP.Fusion.Term.Deletion.Point
+  , module ADP.Fusion.Term.Deletion.Subword
   ) where
 
 import ADP.Fusion.Term.Deletion.Point
+import ADP.Fusion.Term.Deletion.Subword
 import ADP.Fusion.Term.Deletion.Type
 
 
diff --git a/ADP/Fusion/Term/Deletion/Subword.hs b/ADP/Fusion/Term/Deletion/Subword.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/Term/Deletion/Subword.hs
@@ -0,0 +1,32 @@
+
+module ADP.Fusion.Term.Deletion.Subword where
+
+import Data.Strict.Tuple
+import Data.Vector.Fusion.Stream.Monadic as S
+import Prelude hiding (map)
+
+import Data.PrimitiveArray hiding (map)
+
+import ADP.Fusion.Base
+import ADP.Fusion.Term.Deletion.Type
+
+
+
+instance
+  ( Monad m
+  , TerminalStream m a is
+  ) => TerminalStream m (TermSymbol a Deletion) (is:.Subword) where
+  terminalStream (a:|Deletion) (sv:.IStatic _) (is:.ij@(Subword (i:.j)))
+    = S.map (\(S6 s (zi:._) (zo:._) is os e) -> S6 s zi zo (is:.subword j j) (os:.subword 0 0) (e:.()))
+    . iPackTerminalStream a sv (is:.ij)
+  terminalStream (a:|Deletion) (sv:.IVariable _) (is:.ij@(Subword (i:.j)))
+    = S.map (\(S6 s (zi:.Subword (_:.l)) (zo:._) is os e) -> S6 s zi zo (is:.subword l l) (os:.subword 0 0) (e:.()))
+    . iPackTerminalStream a sv (is:.ij)
+  {-# Inline terminalStream #-}
+
+instance TermStaticVar Deletion Subword where
+  termStaticVar _ sv _ = sv
+  termStreamIndex _ _ ij = ij
+  {-# Inline termStaticVar   #-}
+  {-# Inline termStreamIndex #-}
+
diff --git a/ADP/Fusion/Term/Epsilon/Subword.hs b/ADP/Fusion/Term/Epsilon/Subword.hs
--- a/ADP/Fusion/Term/Epsilon/Subword.hs
+++ b/ADP/Fusion/Term/Epsilon/Subword.hs
@@ -24,8 +24,6 @@
     $ mkStream ls (IStatic ()) hh ij
   {-# Inline mkStream #-}
 
-
-
 instance
   ( Monad m
   , MkStream m ls (Outside Subword)
@@ -34,4 +32,22 @@
     = map (ElmEpsilon (O $ subword i j) (O $ subword i j))
     $ mkStream ls (OStatic d) u ij
   {-# Inline mkStream #-}
+
+
+
+instance
+  ( Monad m
+  , TerminalStream m a is
+  ) => TerminalStream m (TermSymbol a Epsilon) (is:.Subword) where
+  terminalStream (a:|Epsilon) (sv:.IStatic _) (is:.ij@(Subword (i:.j)))
+    = S.map (\(S6 s (zi:._) (zo:._) is os e) -> S6 s zi zo (is:.subword i j) (os:.subword 0 0) (e:.()))
+    . iPackTerminalStream a sv (is:.ij)
+  {-# Inline terminalStream #-}
+
+instance TermStaticVar Epsilon Subword where
+  termStaticVar _ sv _ = sv
+  termStreamIndex _ _ ij = ij
+  {-# Inline termStaticVar #-}
+  {-# Inline termStreamIndex #-}
+
 
diff --git a/ADP/Fusion/Term/Strng.hs b/ADP/Fusion/Term/Strng.hs
--- a/ADP/Fusion/Term/Strng.hs
+++ b/ADP/Fusion/Term/Strng.hs
@@ -4,8 +4,10 @@
 module ADP.Fusion.Term.Strng
   ( module ADP.Fusion.Term.Strng.Type
   , module ADP.Fusion.Term.Strng.Point
+  , module ADP.Fusion.Term.Strng.Subword
   ) where
 
 import ADP.Fusion.Term.Strng.Point
+import ADP.Fusion.Term.Strng.Subword
 import ADP.Fusion.Term.Strng.Type
 
diff --git a/ADP/Fusion/Term/Strng/Subword.hs b/ADP/Fusion/Term/Strng/Subword.hs
new file mode 100644
--- /dev/null
+++ b/ADP/Fusion/Term/Strng/Subword.hs
@@ -0,0 +1,44 @@
+
+module ADP.Fusion.Term.Strng.Subword where
+
+
+import           Data.Strict.Tuple
+import           Data.Vector.Fusion.Stream.Size
+import           Data.Vector.Fusion.Util (delay_inline)
+import           Debug.Trace
+import           Prelude hiding (map)
+import qualified Data.Vector.Fusion.Stream.Monadic as S
+import qualified Data.Vector.Generic as VG
+
+import           Data.PrimitiveArray
+
+import           ADP.Fusion.Base
+import           ADP.Fusion.Term.Strng.Type
+
+
+
+-- | TODO If we use (IVariable mx) we might be able to request @exactly@
+-- the range we need!
+
+instance
+  ( Monad m
+  , Element ls Subword
+  , MkStream m ls Subword
+  ) => MkStream m (ls :!: Strng v x) Subword where
+  mkStream (ls :!: Strng slice mn mx v) (IStatic ()) hh (Subword (i:.j))
+    = S.filter (\s -> let Subword (k:.l) = getIdx s in l-k <= mx)
+    . S.map (\s -> let (Subword (_:.l)) = getIdx s
+                   in  ElmStrng (slice l (j-l) v) (subword l j) (subword 0 0) s)
+    $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - mn))
+  mkStream (ls :!: Strng slice mn mx v) (IVariable ()) hh (Subword (i:.j))
+    = S.flatten mk step Unknown $ mkStream ls (IVariable ()) hh (delay_inline Subword (i:.j - mn))
+    where mk s = let Subword (_:.l) = getIdx s in return (s :. j - l - mn)
+          step (s:.z) | z >= 0 = do let Subword (_:.k) = getIdx s
+                                        l              = j - z
+                                        kl             = subword k l
+                                    return $ S.Yield (ElmStrng (slice k (l-k) v) kl (subword 0 0) s) (s:.z-1)
+                      | otherwise = return $ S.Done
+          {-# Inline [0] mk   #-}
+          {-# Inline [0] step #-}
+  {-# Inline mkStream #-}
+
diff --git a/ADP/Fusion/Term/Strng/Type.hs b/ADP/Fusion/Term/Strng/Type.hs
--- a/ADP/Fusion/Term/Strng/Type.hs
+++ b/ADP/Fusion/Term/Strng/Type.hs
@@ -18,10 +18,10 @@
 
 data Strng v x where
   Strng :: VG.Vector v x
-        => !(Int -> Int -> v x -> v x)  -- @slice@ function
-        -> !Int                         -- minimal size
-        -> !Int                         -- maximal size (just use s.th. big if you don't want a limit)
-        -> !(v x)                       -- the actual vector
+        => (Int -> Int -> v x -> v x)  -- @slice@ function
+        -> Int                         -- minimal size
+        -> Int                         -- maximal size (just use s.th. big if you don't want a limit)
+        -> (v x)                       -- the actual vector
         -> Strng v x
 
 manyS :: VG.Vector v x => v x -> Strng v x
diff --git a/ADPfusion.cabal b/ADPfusion.cabal
--- a/ADPfusion.cabal
+++ b/ADPfusion.cabal
@@ -1,8 +1,9 @@
 name:           ADPfusion
-version:        0.4.0.2
+version:        0.4.1.0
 author:         Christian Hoener zu Siederdissen, 2011-2015
 copyright:      Christian Hoener zu Siederdissen, 2011-2015
-homepage:       http://www.bioinf.uni-leipzig.de/Software/gADP/
+homepage:       https://github.com/choener/ADPfusion
+bug-reports:    https://github.com/choener/ADPfusion/issues
 maintainer:     choener@bioinf.uni-leipzig.de
 category:       Algorithms, Data Structures, Bioinformatics, Formal Languages
 license:        BSD3
@@ -13,12 +14,14 @@
 tested-with:    GHC == 7.8.4, GHC == 7.10.1
 synopsis:       Efficient, high-level dynamic programming.
 description:
+                <http://www.bioinf.uni-leipzig.de/Software/gADP/ generalized Algebraic Dynamic Programming>
+                .
                 ADPfusion combines stream-fusion (using the stream interface
                 provided by the vector library) and type-level programming to
                 provide highly efficient dynamic programming combinators.
                 .
                 ADPfusion allows writing dynamic programs for single- and
-                multi-tape problems. Inputs can be sequences, or sets. And new
+                multi-tape problems. Inputs can be sequences, or sets. New
                 input types can be defined, without having to rewrite this
                 library thanks to the open-world assumption of ADPfusion.
                 .
@@ -26,37 +29,16 @@
                 algorithms as well. Ensemble algorithms combine Inside and
                 Outside calculations.
                 .
+                Starting with version 0.4.1 we support writing multiple
+                context-free grammars (interleaved syntactic variables). Such
+                grammars have applications in bioinformatics and linguistics.
+                .
                 The homepage provides a number of tutorial-style examples, with
                 linear and context-free grammars over sequence and set inputs.
                 .
-                Ideas implemented here are described in a couple of papers:
-                .
-                @
-                Christian Hoener zu Siederdissen
-                Sneaking Around ConcatMap: Efficient Combinators for Dynamic Programming
-                2012. Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
-                <http://doi.acm.org/10.1145/2364527.2364559> preprint: <http://www.tbi.univie.ac.at/newpapers/pdfs/TBI-p-2012-2.pdf>
-                @
-                .
-                @
-                Andrew Farmer, Christian Höner zu Siederdissen, and Andy Gill.
-                The HERMIT in the stream: fusing stream fusion’s concatMap.
-                2014. Proceedings of the ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation.
-                <http://dl.acm.org/citation.cfm?doid=2543728.2543736>
-                @
-                .
-                @
-                Christian Höner zu Siederdissen, Ivo L. Hofacker, and Peter F. Stadler.
-                Product Grammars for Alignment and Folding.
-                2014. IEEE/ACM Transactions on Computational Biology and Bioinformatics. 99.
-                <http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6819790>
-                @
-                .
-                @
-                Christian Höner zu Siederdissen, Sonja J. Prohaska, and Peter F. Stadler.
-                Algebraic Dynamic Programming over General Data Structures.
-                2015. submitted.
-                @
+                The formal background for generalized algebraic dynamic
+                progrmaming and ADPfusion is described in a number of papers.
+                These can be found on the gADP homepage and in the README.
                 .
 
 
@@ -72,11 +54,6 @@
   default:      False
   manual:       True
 
-flag llvm
-  description:  build using LLVM
-  default:      False
-  manual:       True
-
 flag debug
   description:  dump intermediate Core files
   default:      False
@@ -85,21 +62,24 @@
 
 
 library
-
+-- ghc-prim: for reallyUnsafePtrEquality#
   build-depends: base               >= 4.7      && < 4.9
-               , bits               == 0.4.*
-               , mmorph             == 1.0.*
-               , monad-primitive    == 0.1
-               , mtl                == 2.*
-               , OrderedBits        == 0.0.0.*
+               , bits               >= 0.4      && < 0.5
+               , containers
+               , ghc-prim
+               , mmorph             >= 1.0      && < 1.1
+               , monad-primitive    >= 0.1      && < 0.2
+               , mtl                >= 2.0      && < 2.3
+               , OrderedBits        >= 0.0.0.1  && < 0.0.1
                , primitive          >= 0.5.4    && < 0.7
-               , PrimitiveArray     == 0.6.0.*
+               , PrimitiveArray     >= 0.6.1    && < 0.6.2
                , QuickCheck         >= 2.7      && < 2.9
-               , strict             == 0.3.*
-               , template-haskell   == 2.*
+               , strict             >= 0.3      && < 0.4
+               , template-haskell   >= 2.0      && < 3.0
+               , th-orphans         >= 0.12     && < 0.13
                , transformers       >= 0.3      && < 0.5
-               , tuple              == 0.3.*
-               , vector             == 0.10.*
+               , tuple              >= 0.3      && < 0.4
+               , vector             >= 0.10     && < 0.11
 
   exposed-modules:
     ADP.Fusion
@@ -110,11 +90,37 @@
     ADP.Fusion.Base.Point
     ADP.Fusion.Base.Set
     ADP.Fusion.Base.Subword
+    ADP.Fusion.QuickCheck.Common
+    ADP.Fusion.QuickCheck.Point
+    ADP.Fusion.QuickCheck.Set
+    ADP.Fusion.QuickCheck.Subword
+    ADP.Fusion.SynVar
+    ADP.Fusion.SynVar.Array
+    ADP.Fusion.SynVar.Array.Point
+    ADP.Fusion.SynVar.Array.Set
+    ADP.Fusion.SynVar.Array.Subword
+    ADP.Fusion.SynVar.Array.TermSymbol
+    ADP.Fusion.SynVar.Array.Type
+    ADP.Fusion.SynVar.Axiom
+    ADP.Fusion.SynVar.Backtrack
+    ADP.Fusion.SynVar.Fill
+    ADP.Fusion.SynVar.Indices
+    ADP.Fusion.SynVar.Recursive
+    ADP.Fusion.SynVar.Recursive.Point
+    ADP.Fusion.SynVar.Recursive.Subword
+    ADP.Fusion.SynVar.Recursive.Type
+    ADP.Fusion.SynVar.Split
+    ADP.Fusion.SynVar.Split.Subword
+    ADP.Fusion.SynVar.Split.Type
     ADP.Fusion.Term
     ADP.Fusion.Term.Chr
     ADP.Fusion.Term.Chr.Point
     ADP.Fusion.Term.Chr.Subword
     ADP.Fusion.Term.Chr.Type
+    ADP.Fusion.Term.Deletion
+    ADP.Fusion.Term.Deletion.Point
+    ADP.Fusion.Term.Deletion.Subword
+    ADP.Fusion.Term.Deletion.Type
     ADP.Fusion.Term.Edge
     ADP.Fusion.Term.Edge.Set
     ADP.Fusion.Term.Edge.Type
@@ -122,44 +128,28 @@
     ADP.Fusion.Term.Epsilon.Point
     ADP.Fusion.Term.Epsilon.Subword
     ADP.Fusion.Term.Epsilon.Type
-    ADP.Fusion.Term.Deletion
-    ADP.Fusion.Term.Deletion.Point
-    ADP.Fusion.Term.Deletion.Type
     ADP.Fusion.Term.PeekIndex
     ADP.Fusion.Term.PeekIndex.Subword
     ADP.Fusion.Term.PeekIndex.Type
     ADP.Fusion.Term.Strng
     ADP.Fusion.Term.Strng.Point
+    ADP.Fusion.Term.Strng.Subword
     ADP.Fusion.Term.Strng.Type
-    ADP.Fusion.SynVar
-    ADP.Fusion.SynVar.Array
-    ADP.Fusion.SynVar.Array.Point
-    ADP.Fusion.SynVar.Array.Set
-    ADP.Fusion.SynVar.Array.Subword
-    ADP.Fusion.SynVar.Array.Type
-    ADP.Fusion.SynVar.Axiom
-    ADP.Fusion.SynVar.Backtrack
-    ADP.Fusion.SynVar.Fill
-    ADP.Fusion.SynVar.Indices
-    ADP.Fusion.SynVar.Recursive
-    ADP.Fusion.SynVar.Recursive.Point
-    ADP.Fusion.SynVar.Recursive.Subword
-    ADP.Fusion.SynVar.Recursive.Type
     ADP.Fusion.TH
     ADP.Fusion.TH.Backtrack
     ADP.Fusion.TH.Common
-    ADP.Fusion.QuickCheck.Common
-    ADP.Fusion.QuickCheck.Point
-    ADP.Fusion.QuickCheck.Set
-    ADP.Fusion.QuickCheck.Subword
 
   default-extensions: BangPatterns
+                    , DataKinds
                     , DefaultSignatures
                     , FlexibleContexts
                     , FlexibleInstances
                     , GADTs
+                    , KindSignatures
                     , MultiParamTypeClasses
                     , RankNTypes
+                    , RecordWildCards
+                    , ScopedTypeVariables
                     , StandaloneDeriving
                     , TemplateHaskell
                     , TypeFamilies
@@ -189,7 +179,6 @@
   else
     buildable:
       False
-
   hs-source-dirs:
     src
   main-is:
@@ -209,11 +198,6 @@
     -funbox-strict-fields
     -funfolding-use-threshold1000
     -funfolding-keeness-factor1000
-  if flag(llvm)
-    ghc-options:
-      -fllvm
-      -optlo-O3 -optlo-std-compile-opts
-      -fllvm-tbaa
   if flag(debug)
     ghc-options:
       -ddump-to-file
@@ -237,7 +221,6 @@
   else
     buildable:
       False
-
   hs-source-dirs:
     src
   main-is:
@@ -252,16 +235,12 @@
                     , TemplateHaskell
                     , TypeFamilies
                     , TypeOperators
+                    , UndecidableInstances
   ghc-options:
     -O2
     -funbox-strict-fields
     -funfolding-use-threshold1000
     -funfolding-keeness-factor1000
-  if flag(llvm)
-    ghc-options:
-      -fllvm
-      -optlo-O3 -optlo-std-compile-opts
-      -fllvm-tbaa
   if flag(debug)
     ghc-options:
       -ddump-to-file
@@ -286,7 +265,6 @@
   else
     buildable:
       False
-
   hs-source-dirs:
     src
   main-is:
@@ -306,11 +284,6 @@
     -funbox-strict-fields
     -funfolding-use-threshold1000
     -funfolding-keeness-factor1000
-  if flag(llvm)
-    ghc-options:
-      -fllvm
-      -optlo-O3 -optlo-std-compile-opts
-      -fllvm-tbaa
   if flag(debug)
     ghc-options:
       -ddump-to-file
@@ -320,7 +293,6 @@
 
 
 executable Durbin
-
   if flag(examples)
     buildable:
       True
@@ -332,7 +304,6 @@
   else
     buildable:
       False
-
   hs-source-dirs:
     src
   main-is:
@@ -353,11 +324,46 @@
     -funbox-strict-fields
     -funfolding-use-threshold1000
     -funfolding-keeness-factor1000
-  if flag(llvm)
+  if flag(debug)
     ghc-options:
-      -fllvm
-      -optlo-O3 -optlo-std-compile-opts
-      -fllvm-tbaa
+      -ddump-to-file
+      -ddump-simpl
+      -dsuppress-all
+
+
+
+executable Pseudoknot
+  if flag(examples)
+    buildable:
+      True
+    build-depends:  base
+                 ,  ADPfusion
+                 ,  PrimitiveArray
+                 ,  template-haskell
+                 ,  vector
+  else
+    buildable:
+      False
+  hs-source-dirs:
+    src
+  main-is:
+    Pseudoknot.hs
+  default-language:
+    Haskell2010
+  default-extensions: BangPatterns
+                    , DataKinds
+                    , FlexibleContexts
+                    , FlexibleInstances
+                    , MultiParamTypeClasses
+                    , RecordWildCards
+                    , TemplateHaskell
+                    , TypeFamilies
+                    , TypeOperators
+  ghc-options:
+    -O2
+    -funbox-strict-fields
+    -funfolding-use-threshold1000
+    -funfolding-keeness-factor1000
   if flag(debug)
     ghc-options:
       -ddump-to-file
@@ -366,6 +372,84 @@
 
 
 
+executable OverlappingPalindromes
+  if flag(examples)
+    buildable:
+      True
+    build-depends:  base
+                 ,  ADPfusion
+                 ,  PrimitiveArray
+                 ,  template-haskell
+                 ,  vector
+  else
+    buildable:
+      False
+  hs-source-dirs:
+    src
+  main-is:
+    OverlappingPalindromes.hs
+  default-language:
+    Haskell2010
+  default-extensions: BangPatterns
+                    , FlexibleContexts
+                    , FlexibleInstances
+                    , MultiParamTypeClasses
+                    , RecordWildCards
+                    , TemplateHaskell
+                    , TypeFamilies
+                    , TypeOperators
+  ghc-options:
+    -O2
+    -funbox-strict-fields
+    -funfolding-use-threshold1000
+    -funfolding-keeness-factor1000
+  if flag(debug)
+    ghc-options:
+      -ddump-to-file
+      -ddump-simpl
+      -dsuppress-all
+
+
+
+executable SplitTests
+  if flag(examples)
+    buildable:
+      True
+    build-depends:  base
+                 ,  ADPfusion
+                 ,  PrimitiveArray
+                 ,  template-haskell
+                 ,  vector
+  else
+    buildable:
+      False
+  hs-source-dirs:
+    src
+  main-is:
+    SplitTests.hs
+  default-language:
+    Haskell2010
+  default-extensions: BangPatterns
+                    , FlexibleContexts
+                    , FlexibleInstances
+                    , MultiParamTypeClasses
+                    , RecordWildCards
+                    , TemplateHaskell
+                    , TypeFamilies
+                    , TypeOperators
+  ghc-options:
+    -O2
+    -funbox-strict-fields
+    -funfolding-use-threshold1000
+    -funfolding-keeness-factor1000
+  if flag(debug)
+    ghc-options:
+      -ddump-to-file
+      -ddump-simpl
+      -dsuppress-all
+
+
+
 test-suite properties
   type:
     exitcode-stdio-1.0
@@ -384,6 +468,42 @@
                , test-framework               >= 0.8  && < 0.9
                , test-framework-quickcheck2   >= 0.3  && < 0.4
                , test-framework-th            >= 0.2  && < 0.3
+
+
+
+benchmark performance
+  type:
+    exitcode-stdio-1.0
+  main-is:
+    performance.hs
+  ghc-options:
+    -rtsopts -with-rtsopts=-N -with-rtsopts=-T
+    -O2
+    -funbox-strict-fields
+    -funfolding-use-threshold1000
+    -funfolding-keeness-factor1000
+  if flag(debug)
+    ghc-options:
+      -ddump-to-file
+      -ddump-simpl
+      -dsuppress-all
+  hs-source-dirs:
+    tests
+  default-language:
+    Haskell2010
+  default-extensions: BangPatterns
+                    , FlexibleContexts
+                    , TemplateHaskell
+                    , RecordWildCards
+                    , TypeFamilies
+                    , TypeOperators
+                    , StandaloneDeriving
+                    , DeriveGeneric
+  build-depends: base
+               , ADPfusion
+               , BenchmarkHistory   >= 0.0.0  && < 0.0.1
+               , PrimitiveArray
+               , vector
 
 
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,11 +1,36 @@
-# ADPfusion
-
 [![Build Status](https://travis-ci.org/choener/ADPfusion.svg?branch=master)](https://travis-ci.org/choener/ADPfusion)
 
+# ADPfusion
+
 [*generalized ADPfusion Homepage*](http://www.bioinf.uni-leipzig.de/Software/gADP/)
 
+Ideas implemented here are described in a couple of papers:
 
 
+
+1.  Christian Hoener zu Siederdissen  
+    *Sneaking Around ConcatMap: Efficient Combinators for Dynamic Programming*  
+    2012, Proceedings of the 17th ACM SIGPLAN international conference on Functional programming  
+    [paper](http://doi.acm.org/10.1145/2364527.2364559) [preprint](http://www.tbi.univie.ac.at/newpapers/pdfs/TBI-p-2012-2.pdf)  
+1.  Andrew Farmer, Christian Höner zu Siederdissen, and Andy Gill.  
+    *The HERMIT in the stream: fusing stream fusion’s concatMap*  
+    2014, Proceedings of the ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation.  
+    [paper](http://dl.acm.org/citation.cfm?doid=2543728.2543736)  
+1.  Christian Höner zu Siederdissen, Ivo L. Hofacker, and Peter F. Stadler.  
+    *Product Grammars for Alignment and Folding*  
+    2014, IEEE/ACM Transactions on Computational Biology and Bioinformatics. 99  
+    [paper](http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6819790)  
+1.  Christian Höner zu Siederdissen, Sonja J. Prohaska, and Peter F. Stadler  
+    *Algebraic Dynamic Programming over General Data Structures*  
+    2015, BMC Bioinformatics  
+    [preprint](http://www.bioinf.uni-leipzig.de/Software/gADP/preprints/hoe-pro-2015.pdf)  
+1.  Maik Riechert, Christian Höner zu Siederdissen, and Peter F. Stadler  
+    *Algebraic dynamic programming for multiple context-free languages*  
+    2015, submitted  
+    [preprint](http://www.bioinf.uni-leipzig.de/Software/gADP/preprints/rie-hoe-2015.pdf)  
+
+
+
 # Introduction
 
 ADPfusion combines stream-fusion (using the stream interface provided by the
@@ -32,55 +57,16 @@
 combinators. This facilitates writing code that performs backtracking, or
 samples structures stochastically, among others things.
 
-This version is still highly experimental and makes use of multiple recent
-improvements in GHC. This is particularly true for the monadic interface.
 
-Long term goals: Outer indices with more than two dimensions, specialized table
-design, a combinator library, a library for computational biology.
 
-Two algorithms from the realm of computational biology are provided as examples
-on how to write dynamic programming algorithms using this library:
-<http://hackage.haskell.org/package/Nussinov78> and
-<http://hackage.haskell.org/package/RNAfold>.
 
-
-
 # Installation
 
-If GHC-7.2.2/GHC-7.4, LLVM and cabal-install are available, you should be all
-set. I recommend using cabal-dev as it provides a very nice sandbox (replace
-cabal-dev with cabal otherwise).
-
-If you go with cabal-dev, no explicit installation is necessary and ADPfusion
-will be installed in the sandbox together with the example algorithms or your
-own.
-
-For a more global installation, "cabal install ADPfusion" should do the trick.
-
-To run the Quickcheck tests, do an additional "cabal-dev install QuickCheck",
-then "cabal-dev ghci", ":l ADP/Fusion/QuickCheck.hs", and "allProps". Loading
-the quickcheck module should take a bit due to compilation. "allProps" tests
-all properties and should yield no errors.
-
-
-
-# Notes
-
-If you have problems, find bugs, or want to use this library to write your own
-DP algorithms, please send me a mail. I'm very interested in hearing what is
-missing.
-
-One of the things I'll be integrating is an extension to higher dimensions
-(more than two).
-
-Right now, I am not quite happy with the construction and destruction of the
-"Box" representations. These will change soon. In addition, an analysis of the
-actual combinators should remove the need for nested applications of objective
-functions in many cases.
+Follow the [gADP examples](http://www.bioinf.uni-leipzig.de/Software/gADP/index.html).
 
 
 
-# Implementors Notes
+# Implementors Notes (if you want to extend ADPfusion)
 
 
 - The general inlining scheme is: (i) mkStream is {-# INLINE mkStream #-},
@@ -94,11 +80,18 @@
   constaints), you have to delay_inline this (until inliner phase 0). Otherwise
   you will break fusion for mkStream.
 
+- Terminals that capture both, say indexing functions, and data should have no
+  strictness annotations for the indexing function. This allows the code to be
+  duplicated, then inlined. This improves performance a lot, because otherwise
+  a function is created that performs these lookups, which has serious (50%
+  slower or so) performance implications.
 
 
+
 #### Contact
 
-Christian Hoener zu Siederdissen
-choener@bioinf.uni-leipzig.de
-Leipzig University, Leipzig, Germany
+Christian Hoener zu Siederdissen  
+Leipzig University, Leipzig, Germany  
+choener@bioinf.uni-leipzig.de  
+<http://www.bioinf.uni-leipzig.de/~choener/>  
 
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,17 @@
+0.4.1.0
+-------
+
+- initial support for multi-context free grammars
+- mcfgs allow for interleaved syntactic variables
+- applications include: natural language modelling and pseudoknotted structures in RNA
+- the simplest formal language that requires this is: a^i b^j a^i b^j
+- the [GenussFold](http://hackage.haskell.org/package/GenussFold) library gives a simple example grammar
+
+0.4.0.2
+-------
+
+- bugfixes
+
 0.4.0.0
 -------
 
diff --git a/src/Nussinov.hs b/src/Nussinov.hs
--- a/src/Nussinov.hs
+++ b/src/Nussinov.hs
@@ -100,7 +100,7 @@
 {-# INLINE grammar #-}
 
 runNussinov :: Int -> String -> (Int,[String])
-runNussinov k inp = (d, take k bs) where -- . {- . S.toList . -} unId $ axiom b) where
+runNussinov k inp = (d, take k bs) where
   i = VU.fromList . Prelude.map toUpper $ inp
   n = VU.length i
   !(Z:.t) = runInsideForward i
diff --git a/src/OverlappingPalindromes.hs b/src/OverlappingPalindromes.hs
new file mode 100644
--- /dev/null
+++ b/src/OverlappingPalindromes.hs
@@ -0,0 +1,156 @@
+
+{-# Language DataKinds #-}
+{-# Language KindSignatures #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language DataKinds               #-}
+{-# Language DefaultSignatures       #-}
+{-# Language FlexibleContexts        #-}
+{-# Language FlexibleInstances       #-}
+{-# Language GADTs                   #-}
+{-# Language KindSignatures          #-}
+{-# Language MultiParamTypeClasses   #-}
+{-# Language RankNTypes              #-}
+{-# Language StandaloneDeriving      #-}
+{-# Language TemplateHaskell         #-}
+{-# Language TypeFamilies            #-}
+{-# Language TypeOperators           #-}
+{-# Language TypeSynonymInstances    #-}
+{-# Language UndecidableInstances    #-}
+
+module Main where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Vector.Fusion.Stream.Monadic (Stream (..))
+import           Data.Vector.Fusion.Util
+import           Debug.Trace
+import qualified Control.Arrow as A
+import qualified Data.Vector as V
+import qualified Data.Vector.Fusion.Stream as S
+import qualified Data.Vector.Fusion.Stream.Monadic as SM
+import qualified Data.Vector.Unboxed as VU
+import           System.Environment (getArgs)
+import           System.IO.Unsafe (unsafePerformIO)
+import           Text.Printf
+
+import           Data.PrimitiveArray as PA hiding (map)
+
+import           ADP.Fusion
+
+
+
+data Signature m x r c = Signature
+  { ovrlap :: () -> () -> x -> x -> () -> x -- TODO !!!
+  , brckts :: (Z:.c:.()) -> x -> (Z:.():.c) -> x
+  , braces :: (Z:.c:.()) -> x -> (Z:.():.c) -> x
+  , nilnil :: (Z:.():.()) -> x
+  , h :: Stream m x -> m r
+  }
+
+makeAlgebraProduct ''Signature
+
+
+
+-- |
+--
+-- @
+-- 012345678
+-- [[((]]))
+-- @
+
+grammar Signature{..} x' a' b' i =
+  let x = x'  ( ovrlap <<< (split (Proxy :: Proxy "a") (Proxy :: Proxy Fragment) a)
+                        %  (split (Proxy :: Proxy "b") (Proxy :: Proxy Fragment) b)
+                        %  (split (Proxy :: Proxy "a") (Proxy :: Proxy Final   ) a)
+                        %  (split (Proxy :: Proxy "b") (Proxy :: Proxy Final   ) b) -- ... h
+                        %  (split (Proxy :: Proxy "c") (Proxy :: Proxy Fragment) b) ... h
+              )
+      a = a'  ( nilnil <<< (M:|Epsilon:|Epsilon)                           |||
+                brckts <<< (M:|chr i:|Deletion) % a % (M:|Deletion:|chr i) ... h
+              )
+      b = b'  ( nilnil <<< (M:|Epsilon:|Epsilon)                           |||
+                braces <<< (M:|chr i:|Deletion) % b % (M:|Deletion:|chr i) ... h
+              )
+  in Z:.x:.a:.b
+{-# Inline grammar #-}
+
+
+
+score :: Monad m => Signature m Int Int Char
+score = Signature
+  { ovrlap = \ a' b' a b _ -> {- if a>0 || b>0 then traceShow ("oo",a',b',a,b) $ a + b else -} a+b -- TODO !!!
+  , brckts = \ (Z:.l:.()) a (Z:.():.r) -> {- traceShow ("[]",l,a,r) $ -} if l=='[' && r==']' then a+1 else -999999
+  , braces = \ (Z:.l:.()) b (Z:.():.r) -> {- traceShow ("()",l,b,r) $ -} if l=='(' && r==')' then b+1 else -999999
+  , nilnil = \ _ -> 0
+  , h = SM.foldl' max (-999999)
+  }
+{-# Inline score #-}
+
+
+
+-- |
+--
+-- TODO pretty shows in @ovrlap@ that we might want to introduce a second
+-- @h@ together with @Stream m y -> m s@?
+
+pretty :: Monad m => Signature m [String] [[String]] Char
+pretty = Signature
+  { ovrlap = \ () () [a,a'] [b,b'] () -> [a ++ b ++ a' ++ b'] -- TODO !!!
+  , brckts = \ (Z:.l:.()) [a,a'] (Z:.():.r) -> ["a"++a , a'++"A"]
+  , braces = \ (Z:.l:.()) [b,b'] (Z:.():.r) -> ["b"++b , b'++"B"]
+  , nilnil = \ _ -> ["",""]
+  , h = SM.toList
+  }
+{-# Inline pretty #-}
+
+
+
+overlappingPalindromes :: String -> (Int,[[String]])
+overlappingPalindromes inp = (d,bs) where
+  i  = VU.fromList inp
+  n  = VU.length i
+  d  = unId $ axiom x
+  bs = unId $ axiom x'
+  x :: X
+  a :: T
+  b :: T
+  (Z:.x:.a:.b) = opForward i
+  {-
+  (Z:.x:.a:.b) = mutateTablesDefault $
+                   grammar score
+                   (ITbl 1 0 EmptyOk (PA.fromAssocs (subword 0 0) (subword 0 n) (-999999) []))
+                   (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-999999) []))
+                   (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-999999) []))
+                   i
+                   -}
+  (Z:.x':.a':.b') = grammar (score <|| pretty)
+                      (toBacktrack x (undefined :: Id a -> Id a))
+                      (toBacktrack a (undefined :: Id a -> Id a))
+                      (toBacktrack b (undefined :: Id a -> Id a))
+                      i
+{-# NoInline overlappingPalindromes #-}
+
+opForward :: VU.Vector Char -> Z:.X:.T:.T
+opForward i =
+  let n = VU.length i
+  in  mutateTablesDefault $
+        grammar score
+        (ITbl 1 0 EmptyOk (PA.fromAssocs (subword 0 0) (subword 0 n) (-999999) []))
+        (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-999999) []))
+        (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-999999) []))
+        i
+{-# NoInline opForward #-}
+
+type X = ITbl Id Unboxed Subword Int
+type T = ITbl Id Unboxed (Z:.Subword:.Subword) Int
+
+
+main :: IO ()
+main = do
+  xs <- fmap lines $ getContents
+  forM_ xs $ \x -> do
+    let (d,bs) = overlappingPalindromes x
+    putStrLn x
+    print d
+--    putStrLn $ head $ head bs
+
diff --git a/src/Pseudoknot.hs b/src/Pseudoknot.hs
new file mode 100644
--- /dev/null
+++ b/src/Pseudoknot.hs
@@ -0,0 +1,141 @@
+
+module Main where
+
+import           Control.Applicative
+import           Control.Monad
+import           Control.Monad.ST
+import           Data.Char (toUpper,toLower)
+import           Data.List as L
+import           Data.Vector.Fusion.Util
+import           Debug.Trace
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Syntax
+import qualified Data.Vector.Fusion.Stream as S
+import qualified Data.Vector.Fusion.Stream.Monadic as SM
+import qualified Data.Vector.Unboxed as VU
+import           System.Environment (getArgs)
+import           Text.Printf
+
+import           Data.PrimitiveArray as PA
+
+import           ADP.Fusion
+
+
+
+data Nussinov m x r c = Nussinov
+  { unp :: x -> c -> x
+  , jux :: x -> c -> x -> c -> x
+  , pse :: () -> () -> x -> x -> x
+  , nil :: () -> x
+  , pk1 :: (Z:.x:.()) -> (Z:.c:.()) -> x -> (Z:.():.x) -> (Z:.():.c) -> x
+  , pk2 :: (Z:.x:.()) -> (Z:.c:.()) -> x -> (Z:.():.x) -> (Z:.():.c) -> x
+  , nll :: (Z:.():.()) -> x
+  , h   :: SM.Stream m x -> m r
+  }
+
+makeAlgebraProduct ''Nussinov
+
+
+bpmax :: Monad m => Nussinov m Int Int Char
+bpmax = Nussinov
+  { unp = \ x c     -> x
+  , jux = \ x c y d -> if c `pairs` d then x + y + 1 else -999999
+  , pse = \ () () x y -> x + y
+  , nil = \ ()      -> 0
+  , pk1 = \ (Z:.x:.()) (Z:.a:.()) y (Z:.():.z) (Z:.():.b) -> if a `pairs` b then x + y + z + 1 else -888888
+  , pk2 = \ (Z:.x:.()) (Z:.a:.()) y (Z:.():.z) (Z:.():.b) -> if a `pairs` b then x + y + z + 1 else -888888
+  , nll = \ (Z:.():.()) -> 0
+  , h   = SM.foldl' max (-999999)
+  }
+{-# INLINE bpmax #-}
+
+-- |
+
+pairs !c !d
+  =  c=='A' && d=='U'
+  || c=='C' && d=='G'
+  || c=='G' && d=='C'
+  || c=='G' && d=='U'
+  || c=='U' && d=='A'
+  || c=='U' && d=='G'
+{-# INLINE pairs #-}
+
+-- |
+--
+-- TODO It could be beneficial to introduce
+-- @type Splitted = Either String (String,String)@
+-- or something isomorphic. While [String] works, it allows for too many
+-- possibilities here! ([] ist lightweight, on the other hand ...)
+
+pretty :: Monad m => Nussinov m [String] [[String]] Char
+pretty = Nussinov
+  { unp = \ [x] c     -> [x ++ "."]
+  , jux = \ [x] c [y] d -> [x ++ "(" ++ y ++ ")"]
+  , pse = \ () () [x1,x2] [y1,y2] -> [x1 ++ y1 ++ x2 ++ y2]
+  , nil = \ ()      -> [""]
+  , pk1 = \ (Z:.[x]:.()) (Z:.a:.()) [y1,y2] (Z:.():.[z]) (Z:.():.b) -> [x ++ "[" ++ y1 , y2 ++ z ++ "]"]
+  , pk2 = \ (Z:.[x]:.()) (Z:.a:.()) [y1,y2] (Z:.():.[z]) (Z:.():.b) -> [x ++ "{" ++ y1 , y2 ++ z ++ "}"]
+  , nll = \ (Z:.():.()) -> ["",""]
+  , h   = SM.toList
+  }
+{-# INLINE pretty #-}
+
+grammar Nussinov{..} t' u' v' c =
+  let t = t'  ( unp <<< t % c               |||
+                jux <<< t % c % t % c   |||
+                nil <<< Epsilon                 |||
+                pse <<< (split (Proxy :: Proxy "U") (Proxy :: Proxy Fragment) u)
+                     %  (split (Proxy :: Proxy "V") (Proxy :: Proxy Fragment) v)
+                     %  (split (Proxy :: Proxy "U") (Proxy :: Proxy Final)    u)
+                     %  (split (Proxy :: Proxy "V") (Proxy :: Proxy Final)    v)  ... h
+              )
+      u = u'  ( pk1 <<< (M:|t:|Deletion) % (M:|c:|Deletion) % u % (M:|Deletion:|t) % (M:|Deletion:|c) |||
+                nll <<< (M:|Epsilon:|Epsilon)                                                                 ... h
+              )
+      v = v'  ( pk2 <<< (M:|t:|Deletion) % (M:|c:|Deletion) % v % (M:|Deletion:|t) % (M:|Deletion:|c) |||
+                nll <<< (M:|Epsilon:|Epsilon)                                                                 ... h
+              )
+  in Z:.t:.u:.v
+{-# INLINE grammar #-}
+
+runPseudoknot :: Int -> String -> (Int,[[String]])
+runPseudoknot k inp = (d, take k bs) where
+  i = VU.fromList . Prelude.map toUpper $ inp
+  n = VU.length i
+  !(Z:.t:.u:.v) = runInsideForward i
+  d = unId $ axiom t
+  bs = runInsideBacktrack i (Z:.t:.u:.v)
+{-# NOINLINE runPseudoknot #-}
+
+type X = ITbl Id Unboxed Subword Int
+type T = ITbl Id Unboxed (Z:.Subword:.Subword) Int
+
+runInsideForward :: VU.Vector Char -> Z:.X:.T:.T
+runInsideForward i = mutateTablesWithHints (Proxy :: Proxy MonotoneMCFG)
+                   $ grammar bpmax
+                        (ITbl 0 0 EmptyOk (PA.fromAssocs (subword 0 0) (subword 0 n) (-666999) []))
+                        (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-777999) []))
+                        (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-888999) []))
+                        (chr i)
+  where n = VU.length i
+{-# NoInline runInsideForward #-}
+
+runInsideBacktrack :: VU.Vector Char -> Z:.X:.T:.T -> [[String]]
+runInsideBacktrack i (Z:.t:.u:.v) = unId $ axiom b
+  where !(Z:.b:._:._) = grammar (bpmax <|| pretty)
+                          (toBacktrack t (undefined :: Id a -> Id a))
+                          (toBacktrack u (undefined :: Id a -> Id a))
+                          (toBacktrack v (undefined :: Id a -> Id a))
+                          (chr i)
+{-# NoInline runInsideBacktrack #-}
+
+main = do
+  as <- getArgs
+  let k = if null as then 1 else read $ head as
+  ls <- lines <$> getContents
+  forM_ ls $ \l -> do
+    putStrLn l
+    let (s,xs) = runPseudoknot k l
+    print s
+    mapM_ (\[x] -> printf "%s %5d\n" x s) xs
+
diff --git a/src/SplitTests.hs b/src/SplitTests.hs
new file mode 100644
--- /dev/null
+++ b/src/SplitTests.hs
@@ -0,0 +1,136 @@
+
+{-# Language DataKinds #-}
+{-# Language KindSignatures #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language DataKinds               #-}
+{-# Language DefaultSignatures       #-}
+{-# Language FlexibleContexts        #-}
+{-# Language FlexibleInstances       #-}
+{-# Language GADTs                   #-}
+{-# Language KindSignatures          #-}
+{-# Language MultiParamTypeClasses   #-}
+{-# Language RankNTypes              #-}
+{-# Language StandaloneDeriving      #-}
+{-# Language TemplateHaskell         #-}
+{-# Language TypeFamilies            #-}
+{-# Language TypeOperators           #-}
+{-# Language TypeSynonymInstances    #-}
+{-# Language UndecidableInstances    #-}
+
+module Main where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Vector.Fusion.Stream.Monadic (Stream (..))
+import           Data.Vector.Fusion.Util
+import           Debug.Trace
+import qualified Control.Arrow as A
+import qualified Data.Vector as V
+import qualified Data.Vector.Fusion.Stream as S
+import qualified Data.Vector.Fusion.Stream.Monadic as SM
+import qualified Data.Vector.Unboxed as VU
+import           System.Environment (getArgs)
+import           System.IO.Unsafe (unsafePerformIO)
+import           Text.Printf
+
+import           Data.PrimitiveArray as PA hiding (map)
+
+import           ADP.Fusion
+
+
+
+data Signature m x r c = Signature
+  { ovrlap :: () -> x -> x
+  , brckts :: (Z:.c:.()) -> x -> (Z:.():.c) -> x
+  , nilnil :: (Z:.():.()) -> x
+  , h :: Stream m x -> m r
+  }
+
+makeAlgebraProduct ''Signature
+
+
+
+-- |
+--
+-- @
+-- 012345678
+-- [[((]]))
+-- @
+
+grammar Signature{..} x' a' i =
+  let x = x'  ( ovrlap <<< (split (Proxy :: Proxy "a") (Proxy :: Proxy Fragment) a)
+                        %  (split (Proxy :: Proxy "a") (Proxy :: Proxy Final   ) a) ... h
+              )
+      a = a'  ( nilnil <<< (M:|Epsilon:|Epsilon)                           |||
+                brckts <<< (M:|chr i:|Deletion) % a % (M:|Deletion:|chr i) ... h
+              )
+  in Z:.x:.a
+{-# Inline grammar #-}
+
+
+
+score :: Monad m => Signature m Int Int Char
+score = Signature
+  { ovrlap = \ a' a -> a + 4711
+  , brckts = \ (Z:.l:.()) a (Z:.():.r) -> {- traceShow ("[]",l,a,r) $ -} if l=='[' && r==']' then a+1 else -999999
+  , nilnil = \ _ -> 0
+  , h = SM.foldl' max (-999999)
+  }
+{-# Inline score #-}
+
+
+
+-- |
+--
+-- TODO pretty shows in @ovrlap@ that we might want to introduce a second
+-- @h@ together with @Stream m y -> m s@?
+
+pretty :: Monad m => Signature m [String] [[String]] Char
+pretty = Signature
+  { ovrlap = \ () [a,a'] -> [a ++ a']
+  , brckts = \ (Z:.l:.()) [a,a'] (Z:.():.r) -> ["a"++a , a'++"A"]
+  , nilnil = \ _ -> ["",""]
+  , h = SM.toList
+  }
+{-# Inline pretty #-}
+
+
+
+overlappingPalindromes :: String -> (Int,[[String]])
+overlappingPalindromes inp = (d,bs) where
+  i  = VU.fromList inp
+  n  = VU.length i
+  d  = unId $ axiom x
+  bs = unId $ axiom x'
+  x :: X
+  a :: T
+  (Z:.x:.a) = opForward i
+  (Z:.x':.a') = grammar (score <|| pretty)
+                  (toBacktrack x (undefined :: Id a -> Id a))
+                  (toBacktrack a (undefined :: Id a -> Id a))
+                  i
+{-# NoInline overlappingPalindromes #-}
+
+opForward :: VU.Vector Char -> Z:.X:.T
+opForward i =
+  let n = VU.length i
+  in  mutateTablesDefault $
+        grammar score
+        (ITbl 1 0 EmptyOk (PA.fromAssocs (subword 0 0) (subword 0 n) (-999999) []))
+        (ITbl 0 0 (Z:.EmptyOk:.EmptyOk) (PA.fromAssocs (Z:.subword 0 0:.subword 0 0) (Z:.subword 0 n:.subword 0 n) (-999999) []))
+        i
+{-# NoInline opForward #-}
+
+type X = ITbl Id Unboxed Subword Int
+type T = ITbl Id Unboxed (Z:.Subword:.Subword) Int
+
+
+main :: IO ()
+main = do
+  xs <- fmap lines $ getContents
+  forM_ xs $ \x -> do
+    let (d,bs) = overlappingPalindromes x
+    putStrLn x
+    print d
+--    putStrLn $ head $ head bs
+
diff --git a/tests/performance.hs b/tests/performance.hs
new file mode 100644
--- /dev/null
+++ b/tests/performance.hs
@@ -0,0 +1,89 @@
+
+module Main where
+
+import           Data.Vector.Fusion.Util
+import           GHC.Stats
+import qualified Data.Vector.Fusion.Stream.Monadic as SM
+import qualified Data.Vector.Unboxed as VU
+import           System.Mem
+import           System.Environment
+import           GHC.Conc (pseq)
+import           GHC.Generics
+import qualified Data.Vector as V
+import           Control.Arrow (second)
+import           Data.Int(Int64)
+import           System.Exit
+
+import           ADP.Fusion hiding (Split)
+import           Data.PrimitiveArray hiding (map)
+import           BenchmarkHistory
+
+
+
+-- | All grammars require a signature.
+
+data Split m x r = Split
+  { nil :: ()  -> x
+  , lef :: Int -> x -> x
+  , spl :: x   -> x -> x
+  , h   :: SM.Stream m x -> m r
+  }
+
+-- makeAlgebraProduct ''Split
+
+algMax :: Monad m => Split m Int Int
+algMax = Split
+  { nil = \ () -> 0
+  , lef = \k x -> k+x
+  , spl = \ x y   -> x+y
+  , h   = SM.foldl' max 0
+  }
+{-# Inline algMax #-}
+
+gLeft Split{..} c t' =
+  let t = t'  ( lef <<< chr c % t   |||
+                spl <<< t % t       |||
+                nil <<< Epsilon     ... h
+              )
+  in Z:.t
+{-# Inline gLeft #-}
+
+mkArrs :: Int -> (VU.Vector Int, Unboxed Subword Int)
+mkArrs n = ( VU.enumFromTo 1 n
+           , fromAssocs (subword 0 0) (subword 0 n) (-999999) []
+           )
+{-# NoInline mkArrs #-}
+
+-- | WARNING: Multiple runs of @runLeft@ make use of the same @arr@. This
+-- is, of course, dangerous. Unless you know what you are doing.
+
+runLeft :: (VU.Vector Int, Unboxed Subword Int) -> Int -> Int
+runLeft (!i, !arr) k = seq k d where
+--  i   = VU.enumFromTo 1 k
+  n   = VU.length i
+--  arr = fromAssocs (subword 0 0) (subword 0 n) (-999999) []
+  (Z:.t) = runLeftForward i arr
+  d = unId $ axiom t
+{-# NoInline runLeft #-}
+
+runLeftForward :: VU.Vector Int -> Unboxed Subword Int -> Z:.ITbl Id Unboxed Subword Int
+runLeftForward !i !arr = mutateTablesDefault
+               $ gLeft algMax
+                   i
+                   (ITbl 0 0 EmptyOk arr)
+{-# NoInline runLeftForward #-}
+
+
+
+main :: IO ()
+main = do
+  es <- sequence
+    [ benchmark 10000 ("bench-0100.csv") mkArrs runLeft  100
+    , benchmark    10 ("bench-1000.csv") mkArrs runLeft 1000
+    , benchmark     1 ("bench-2000.csv") mkArrs runLeft 2000
+    ]
+  let ok = all (== ExitSuccess) es
+  if ok
+    then exitSuccess
+    else exitFailure
+