diff --git a/.gitignore b/.gitignore
index b15d36b9801de73621543eb91dddd8d21d273fe4..7ad9f184062db2370a7f7c8bfc86dd909e69e6a9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,5 +27,5 @@ cabal.project.local~
 result
 
 a.out
-rtree-c
+/rtree-c
 test.c
diff --git a/bin/rtree-c/Main.hs b/bin/rtree-c/Main.hs
index 19314eb8d98c866999bd4ae86cad2259c9f81941..629be3f15d5d96d4454a5c3450d1f8aee2d496b5 100644
--- a/bin/rtree-c/Main.hs
+++ b/bin/rtree-c/Main.hs
@@ -6,28 +6,24 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-import Control.Monad.Reduce
 import Control.RTree
 
+import ReduceC
+
 import Colog
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Trans
-import Control.Monad.Trans.Maybe
 import Data.Foldable
 import Data.Functor
-import Data.Maybe
+import Data.Map.Strict qualified as Map
+import Data.Text qualified as Text
+import GHC.Stack
 import Language.C qualified as C
 import Options.Applicative
 import System.Directory
 import System.Exit
 import System.FilePath
-
-import Data.Text qualified as Text
-
-import Data.Map.Strict qualified as Map
-import GHC.Stack
-import Language.C (CInitializer (CInitExpr))
 import System.IO
 import System.Process.Typed
 import Text.Pretty.Simple
@@ -63,6 +59,13 @@ run = do
         , help "check for validity, throw error if command fails"
         ]
 
+  expmode <-
+    flag False True
+      $ fold
+        [ long "exp"
+        , help "run in exponential mode"
+        ]
+
   pure
     $ usingLoggerT (cmap fmtMessage logTextStdout)
     $ do
@@ -76,7 +79,7 @@ run = do
           let x = P.render (C.pretty (c $> C.undefNode))
           liftIO $ writeFile f x
 
-        check' f _ c = do
+        check' f c = do
           when validity do
             liftIO $ copyFile file (file <.> "last")
           output f c
@@ -119,10 +122,10 @@ run = do
           liftIO exitFailure
 
       l <-
-        reduceI
+        (if expmode then ireduceExp else ireduce)
           (check' file)
           (Map.singleton (C.internalIdent "main") True)
-          (reduceC c)
+          (ReduceC.reduceC c)
 
       output file l
  where
@@ -133,180 +136,3 @@ run = do
       Left err -> do
         logError (Text.pack (show err))
         liftIO exitFailure
-
-type Lab = C.Ident
-
-reduceC :: (MonadReduce Lab m) => C.CTranslUnit -> m C.CTranslUnit
-reduceC (C.CTranslUnit es ni) = do
-  es' <- collect mrCExternalDeclaration es
-  pure $ C.CTranslUnit es' ni
-
-mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo)
-mrCExternalDeclaration = \case
-  C.CFDefExt fun -> do
-    givenWith (funName fun)
-    C.CFDefExt <$> rCFunctionDef fun
-  C.CDeclExt decl ->
-    C.CDeclExt <$> mrCDeclaration decl
-  a -> error (show a)
- where
-  funName (C.CFunDef _ (C.CDeclr x _ _ _ _) _ _ _) =
-    x
-
-mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo)
-mrCDeclarationItem = \case
-  C.CDeclarationItem d@(C.CDeclr x _ _ _ _) i e -> do
-    givenWith x
-    i' <- mtry $ munder i mrCInitializer
-    e' <- mtry $ munder e mrCExpression
-    pure (C.CDeclarationItem d i' e')
-  a -> error (show a)
-
-mrCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m (C.CInitializer C.NodeInfo)
-mrCInitializer = \case
-  C.CInitExpr e ni -> mrCExpression e <&> \e' -> CInitExpr e' ni
-  C.CInitList (C.CInitializerList items) ni -> do
-    collectNonEmpty' rmCInitializerListItem items <&> \items' ->
-      C.CInitList (C.CInitializerList items') ni
- where
-  rmCInitializerListItem (pds, is) = do
-    pds' <- lift $ collect rmCPartDesignator pds
-    is' <- mrCInitializer is
-    pure (pds', is')
-
-  rmCPartDesignator :: (MonadReduce Lab m) => C.CPartDesignator C.NodeInfo -> m (C.CPartDesignator C.NodeInfo)
-  rmCPartDesignator = \case
-    a -> error (show a)
-
-mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo)
-mrCDeclaration = \case
-  C.CDecl spc decl ni -> do
-    decl' <- lift $ collect mrCDeclarationItem decl
-    case decl' of
-      [] -> empty
-      decl'' -> pure $ C.CDecl spc decl'' ni
-  a -> error (show a)
-
-rCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> m (C.CFunctionDef C.NodeInfo)
-rCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
-  smt' <- rCStatement smt
-  pure $ C.CFunDef spc dec cdecls smt' ni
-
-rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
-rCStatement = \case
-  C.CCompound is cbi ni -> do
-    cbi' <- collect mrCCompoundBlockItem cbi
-    pure $ C.CCompound is cbi' ni
-  C.CExpr e ni -> do
-    e' <- runMaybeT $ munder e mrCExpression
-    pure $ C.CExpr e' ni
-  C.CIf e s els ni -> do
-    e' <- runMaybeT $ mrCExpression e
-    s' <- rCStatement s
-    els' <- case els of
-      Just els' -> do
-        pure Nothing <| Just <$> rCStatement els'
-      Nothing -> pure Nothing
-    case (e', els') of
-      (Nothing, Nothing) -> pure s'
-      (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
-      (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
-      (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
-  C.CFor e1 e2 e3 s ni -> do
-    rCStatement s <| do
-      e1' <- rCForInit e1
-      e2' <- runMaybeT $ munder e2 mrCExpression
-      e3' <- runMaybeT $ munder e3 mrCExpression
-      s' <- rCStatement s
-      pure $ C.CFor e1' e2' e3' s' ni
-  C.CReturn e ni -> do
-    e' <- case e of
-      Nothing -> pure Nothing
-      Just e' -> Just <$> zrCExpression e'
-    pure $ C.CReturn e' ni
-  C.CBreak ni -> pure (C.CBreak ni)
-  C.CCont ni -> pure (C.CCont ni)
-  C.CLabel i s [] ni ->
-    -- todo fix attrs
-    splitOn i (rCStatement s) do
-      s' <- rCStatement s
-      pure $ C.CLabel i s' [] ni
-  C.CGoto i ni ->
-    -- todo fix attrs
-    splitOn i (pure $ C.CExpr Nothing ni) do
-      pure $ C.CGoto i ni
-  a -> error (show a)
- where
-  rCForInit = \case
-    C.CForDecl decl -> do
-      m <- runMaybeT $ mrCDeclaration decl
-      pure $ case m of
-        Nothing -> C.CForInitializing Nothing
-        Just d' -> C.CForDecl d'
-    C.CForInitializing n -> do
-      C.CForInitializing <$> runMaybeT (munder n mrCExpression)
-
-orZero :: Maybe (C.CExpression C.NodeInfo) -> C.CExpression C.NodeInfo
-orZero = fromMaybe zeroExp
-
-zeroExp :: C.CExpression C.NodeInfo
-zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
-
-zrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> m (C.CExpression C.NodeInfo)
-zrCExpression e = orZero <$> runMaybeT (mrCExpression e)
-
-mrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m (C.CExpression C.NodeInfo)
-mrCExpression = \case
-  C.CVar i ni -> do
-    givenThat i
-    pure $ C.CVar i ni
-  C.CCall e es ni -> do
-    e' <- mrCExpression e
-    es' <- lift $ traverse zrCExpression es
-    pure $ C.CCall e' es' ni
-  C.CCond ec et ef ni -> do
-    ec' <- mrCExpression ec
-    ef' <- mrCExpression ef
-    et' <- mtry $ munder et mrCExpression
-    pure $ C.CCond ec' et' ef' ni
-  C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
-    pure $ C.CBinary o lhs rhs ni
-  C.CUnary o elhs ni -> do
-    lhs <- mrCExpression elhs
-    pure $ C.CUnary o lhs ni
-  C.CConst c -> do
-    -- TODO fix
-    pure $ C.CConst c
-  C.CCast cd e ni -> do
-    -- TODO fix
-    cd' <- mrCDeclaration cd
-    e' <- mrCExpression e
-    pure $ C.CCast cd' e' ni
-  C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
-    pure $ C.CAssign op e1' e2' ni
-  C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
-    pure $ C.CIndex e1' e2' ni
-  C.CMember e i b ni -> do
-    givenThat i
-    e' <- mrCExpression e
-    pure $ C.CMember e' i b ni
-  C.CComma items ni -> do
-    C.CComma <$> collectNonEmpty' mrCExpression items <*> pure ni
-  e -> error (show e)
- where
-  onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs)
-
-mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
-mtry (MaybeT mt) = MaybeT (Just <$> mt)
-
-mlift :: (Applicative m) => Maybe a -> MaybeT m a
-mlift a = MaybeT (pure a)
-
-munder :: (Monad m) => Maybe a -> (a -> MaybeT m b) -> MaybeT m b
-munder a mf = mlift a >>= mf
-
-mrCCompoundBlockItem :: (MonadReduce Lab m) => C.CCompoundBlockItem C.NodeInfo -> MaybeT m (C.CCompoundBlockItem C.NodeInfo)
-mrCCompoundBlockItem = \case
-  C.CBlockStmt s -> empty <| lift (C.CBlockStmt <$> rCStatement s)
-  C.CBlockDecl d -> C.CBlockDecl <$> mrCDeclaration d
-  a -> error (show a)
diff --git a/bin/rtree-c/ReduceC.hs b/bin/rtree-c/ReduceC.hs
new file mode 100644
index 0000000000000000000000000000000000000000..0a4fea667561bb1165f6a3c19e764cfb27a8ea2c
--- /dev/null
+++ b/bin/rtree-c/ReduceC.hs
@@ -0,0 +1,197 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module ReduceC where
+
+import Control.Monad.Reduce
+
+import Control.Applicative
+import Control.Monad.Trans
+import Control.Monad.Trans.Maybe
+import Data.Functor
+import Data.Maybe
+import qualified Language.C as C
+
+type Lab = C.Ident
+
+reduceC :: (MonadReduce Lab m) => C.CTranslUnit -> m C.CTranslUnit
+reduceC (C.CTranslUnit es ni) = do
+  es' <- collect mrCExternalDeclaration es
+  pure $ C.CTranslUnit es' ni
+
+mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo)
+mrCExternalDeclaration = \case
+  C.CFDefExt fun -> do
+    givenWith (funName fun)
+    C.CFDefExt <$> rCFunctionDef fun
+  C.CDeclExt decl ->
+    C.CDeclExt <$> mrCDeclaration decl
+  a -> error (show a)
+ where
+  funName (C.CFunDef _ (C.CDeclr x _ _ _ _) _ _ _) =
+    x
+
+mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo)
+mrCDeclarationItem = \case
+  C.CDeclarationItem d@(C.CDeclr x _ _ _ _) i e -> do
+    givenWith x
+    i' <- mtry $ munder i mrCInitializer
+    e' <- mtry $ munder e mrCExpression
+    pure (C.CDeclarationItem d i' e')
+  a -> error (show a)
+
+mrCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m (C.CInitializer C.NodeInfo)
+mrCInitializer = \case
+  C.CInitExpr e ni -> mrCExpression e <&> \e' -> C.CInitExpr e' ni
+  C.CInitList (C.CInitializerList items) ni -> do
+    collectNonEmpty' rmCInitializerListItem items <&> \items' ->
+      C.CInitList (C.CInitializerList items') ni
+ where
+  rmCInitializerListItem (pds, is) = do
+    pds' <- lift $ collect rmCPartDesignator pds
+    is' <- mrCInitializer is
+    pure (pds', is')
+
+  rmCPartDesignator :: (MonadReduce Lab m) => C.CPartDesignator C.NodeInfo -> m (C.CPartDesignator C.NodeInfo)
+  rmCPartDesignator = \case
+    a -> error (show a)
+
+mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo)
+mrCDeclaration = \case
+  C.CDecl spc decl ni -> do
+    decl' <- lift $ collect mrCDeclarationItem decl
+    case decl' of
+      [] -> empty
+      decl'' -> pure $ C.CDecl spc decl'' ni
+  a -> error (show a)
+
+rCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> m (C.CFunctionDef C.NodeInfo)
+rCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
+  smt' <- rCStatement smt
+  pure $ C.CFunDef spc dec cdecls smt' ni
+
+rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
+rCStatement = \case
+  C.CCompound is cbi ni -> do
+    cbi' <- collect mrCCompoundBlockItem cbi
+    pure $ C.CCompound is cbi' ni
+  C.CExpr e ni -> do
+    e' <- runMaybeT $ munder e mrCExpression
+    pure $ C.CExpr e' ni
+  C.CIf e s els ni -> do
+    e' <- runMaybeT $ mrCExpression e
+    s' <- rCStatement s
+    els' <- case els of
+      Just els' -> do
+        pure Nothing <| Just <$> rCStatement els'
+      Nothing -> pure Nothing
+    case (e', els') of
+      (Nothing, Nothing) -> pure s'
+      (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
+      (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
+      (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
+  C.CFor e1 e2 e3 s ni -> do
+    rCStatement s <| do
+      e1' <- rCForInit e1
+      e2' <- runMaybeT $ munder e2 mrCExpression
+      e3' <- runMaybeT $ munder e3 mrCExpression
+      s' <- rCStatement s
+      pure $ C.CFor e1' e2' e3' s' ni
+  C.CReturn e ni -> do
+    e' <- case e of
+      Nothing -> pure Nothing
+      Just e' -> Just <$> zrCExpression e'
+    pure $ C.CReturn e' ni
+  C.CBreak ni -> pure (C.CBreak ni)
+  C.CCont ni -> pure (C.CCont ni)
+  C.CLabel i s [] ni ->
+    -- todo fix attrs
+    splitOn i (rCStatement s) do
+      s' <- rCStatement s
+      pure $ C.CLabel i s' [] ni
+  C.CGoto i ni ->
+    -- todo fix attrs
+    splitOn i (pure $ C.CExpr Nothing ni) do
+      pure $ C.CGoto i ni
+  a -> error (show a)
+ where
+  rCForInit = \case
+    C.CForDecl decl -> do
+      m <- runMaybeT $ mrCDeclaration decl
+      pure $ case m of
+        Nothing -> C.CForInitializing Nothing
+        Just d' -> C.CForDecl d'
+    C.CForInitializing n -> do
+      C.CForInitializing <$> runMaybeT (munder n mrCExpression)
+
+orZero :: Maybe (C.CExpression C.NodeInfo) -> C.CExpression C.NodeInfo
+orZero = fromMaybe zeroExp
+
+zeroExp :: C.CExpression C.NodeInfo
+zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
+
+zrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> m (C.CExpression C.NodeInfo)
+zrCExpression e = orZero <$> runMaybeT (mrCExpression e)
+
+mrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m (C.CExpression C.NodeInfo)
+mrCExpression = \case
+  C.CVar i ni -> do
+    givenThat i
+    pure $ C.CVar i ni
+  C.CCall e es ni -> do
+    e' <- mrCExpression e
+    es' <- lift $ traverse zrCExpression es
+    pure $ C.CCall e' es' ni
+  C.CCond ec et ef ni -> do
+    ec' <- mrCExpression ec
+    ef' <- mrCExpression ef
+    et' <- mtry $ munder et mrCExpression
+    pure $ C.CCond ec' et' ef' ni
+  C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
+    pure $ C.CBinary o lhs rhs ni
+  C.CUnary o elhs ni -> do
+    lhs <- mrCExpression elhs
+    pure $ C.CUnary o lhs ni
+  C.CConst c -> do
+    -- TODO fix
+    pure $ C.CConst c
+  C.CCast cd e ni -> do
+    -- TODO fix
+    cd' <- mrCDeclaration cd
+    e' <- mrCExpression e
+    pure $ C.CCast cd' e' ni
+  C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
+    pure $ C.CAssign op e1' e2' ni
+  C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
+    pure $ C.CIndex e1' e2' ni
+  C.CMember e i b ni -> do
+    givenThat i
+    e' <- mrCExpression e
+    pure $ C.CMember e' i b ni
+  C.CComma items ni -> do
+    C.CComma <$> collectNonEmpty' mrCExpression items <*> pure ni
+  e -> error (show e)
+ where
+  onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs)
+
+mrCCompoundBlockItem
+  :: (MonadReduce Lab m)
+  => C.CCompoundBlockItem C.NodeInfo
+  -> MaybeT m (C.CCompoundBlockItem C.NodeInfo)
+mrCCompoundBlockItem = \case
+  C.CBlockStmt s -> empty <| lift (C.CBlockStmt <$> rCStatement s)
+  C.CBlockDecl d -> C.CBlockDecl <$> mrCDeclaration d
+  a -> error (show a)
+
+mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
+mtry (MaybeT mt) = MaybeT (Just <$> mt)
+
+mlift :: (Applicative m) => Maybe a -> MaybeT m a
+mlift a = MaybeT (pure a)
+
+munder :: (Monad m) => Maybe a -> (a -> MaybeT m b) -> MaybeT m b
+munder a mf = mlift a >>= mf
diff --git a/rtree.cabal b/rtree.cabal
index 3e72b7322f19cf256a4237e25bbbda26ef90cb7d..6c39356775e59a0a78b060263e6cf1c816f8f252 100644
--- a/rtree.cabal
+++ b/rtree.cabal
@@ -32,6 +32,7 @@ library
 executable rtree-c
   main-is: Main.hs
   other-modules:
+      ReduceC
       Paths_rtree
   hs-source-dirs:
       bin/rtree-c
diff --git a/src/Control/Monad/Reduce.hs b/src/Control/Monad/Reduce.hs
index de3096689b1c7f0fbed64360af5d8a23a5cfb090..5627b5141f59ec682cc17a42693834452a2a36e3 100644
--- a/src/Control/Monad/Reduce.hs
+++ b/src/Control/Monad/Reduce.hs
@@ -15,7 +15,8 @@ Module: Control.Monad.Reduce
 -}
 module Control.Monad.Reduce (
   MonadReduce (..),
-  -- # Constructors
+
+  -- * Constructors
   (<|),
   (|>),
   splitOn,
@@ -24,17 +25,20 @@ module Control.Monad.Reduce (
   givenWith,
   check,
   checkThat,
-  -- # Combinators
+
+  -- * Combinators
   collect,
   collectNonEmpty,
   collectNonEmpty',
-  -- # Algorithms
+
+  -- * Algorithms
   ddmin,
   linearSearch,
   linearSearch',
   binarySearch,
   exponentialSearch,
-  -- # Helpers
+
+  -- * Helpers
   onBoth,
 ) where
 
@@ -53,33 +57,43 @@ import Data.Maybe
 
 -- | The Monad Reduce class.
 class (Monad m) => MonadReduce l m | m -> l where
-  -- | Split the world into the a reduced world (left) without an ellement and a world
+  {-# MINIMAL splitWith | checkWith #-}
+
+  -- | Split the world into the a reduced world (left) without an element and a world
   -- with that element (right). Optionally, labeled with l.
   splitWith :: Maybe l -> m i -> m i -> m i
   splitWith l r1 r2 =
     checkWith l >>= \case
-      True -> r1
-      False -> r2
+      False -> r1
+      True -> r2
   {-# INLINE splitWith #-}
 
+  -- | Check with returns a boolean, that can be used to split the input into a world where
+  -- an optional label is true and where it is false.
   checkWith :: Maybe l -> m Bool
   checkWith l = splitWith l (pure False) (pure True)
   {-# INLINE checkWith #-}
 
+-- | Split with no label.
 split :: (MonadReduce l m) => m i -> m i -> m i
 split = splitWith Nothing
 {-# INLINE split #-}
 
+-- | Infix split.
 (<|) :: (MonadReduce l m) => m i -> m i -> m i
 (<|) = split
 {-# INLINE (<|) #-}
+
 infixr 3 <|
 
+-- | Infix split, to the right.
 (|>) :: (MonadReduce l m) => m i -> m i -> m i
 r1 |> r2 = r2 <| r1
 {-# INLINE (|>) #-}
+
 infixl 3 |>
 
+-- | Split on a label.
 splitOn :: (MonadReduce l m) => l -> m i -> m i -> m i
 splitOn l = splitWith (Just l)
 {-# INLINE splitOn #-}
@@ -94,9 +108,6 @@ checkThat :: (MonadReduce l m) => l -> m Bool
 checkThat l = checkWith (Just l)
 {-# INLINE checkThat #-}
 
-instance (MonadReduce l m) => MonadReduce l (MaybeT m) where
-  splitWith m (MaybeT lhs) (MaybeT rhs) = MaybeT (splitWith m lhs rhs)
-
 -- | Continues if the fact is true.
 given :: (MonadReduce l m) => MaybeT m ()
 given = givenWith Nothing
@@ -130,6 +141,19 @@ collectNonEmpty fn as = do
   MaybeT . pure $ NE.nonEmpty as'
 {-# INLINE collectNonEmpty #-}
 
+instance (MonadReduce l m) => MonadReduce l (MaybeT m) where
+  splitWith m (MaybeT lhs) (MaybeT rhs) = MaybeT (splitWith m lhs rhs)
+
+-- | Returns either of the maybes or combines them if both have values.
+onBoth :: (Monad m) => MaybeT m a -> MaybeT m a -> (a -> a -> MaybeT m a) -> MaybeT m a
+onBoth mlhs mrhs fn = MaybeT do
+  runMaybeT mlhs >>= \case
+    Nothing -> runMaybeT mrhs
+    Just l ->
+      runMaybeT mrhs >>= \case
+        Nothing -> pure (Just l)
+        Just r -> runMaybeT (fn l r)
+
 {- | Given a list of ordered options, choose the first that statisfy the constraints,
 returning the last element if nothing else matches.
 -}
@@ -189,13 +213,3 @@ exponentialSearch = go 1
       | otherwise -> go (n * 2) l <| binarySearch f
      where
       (NE.fromList -> f, NE.fromList -> l) = NE.splitAt n d
-
--- | Returns either of the maybes or combines them if both have values.
-onBoth :: (Monad m) => MaybeT m a -> MaybeT m a -> (a -> a -> MaybeT m a) -> MaybeT m a
-onBoth mlhs mrhs fn = MaybeT do
-  runMaybeT mlhs >>= \case
-    Nothing -> runMaybeT mrhs
-    Just l ->
-      runMaybeT mrhs >>= \case
-        Nothing -> pure (Just l)
-        Just r -> runMaybeT (fn l r)
diff --git a/src/Control/RTree.hs b/src/Control/RTree.hs
index 165b2fb2fdb0a622b6caa57badac11b32640c976..5403a5cffb7d511826fd9686a963ac1fe2a1847d 100644
--- a/src/Control/RTree.hs
+++ b/src/Control/RTree.hs
@@ -14,30 +14,46 @@
 {- |
 Module: Control.RTree
 -}
-module Control.RTree where
+module Control.RTree (
+  -- # RTree
+  RTree (..),
+  extract,
+  reduce,
+  -- # IRTree
+  IRTree,
+  iextract,
+  ireduce,
+  ireduceExp,
+  IRTreeT (..),
+  iextractT,
+  ireduceT,
+  ireduceExpT,
+  ReState (..),
+  -- # Valuation
+  Valuation,
+) where
 
 import Control.Applicative
 import Control.Monad.Reader
-import Control.Monad.Trans.Maybe
 import Data.Functor.Identity
 import qualified Data.Map.Strict as Map
-import Data.Maybe
-import GHC.IORef
 
 import Control.Monad.Reduce
 import Control.Monad.State.Strict
 
 data RTree l i
-  = Split (RTree l i) !(RTree l i)
-  | SplitOn !l (RTree l i) !(RTree l i)
+  = SplitWith (Maybe l) (RTree l i) !(RTree l i)
   | Done i
   deriving (Functor)
 
-extract :: RTree l i -> i
-extract = \case
-  Split _ rhs -> extract rhs
-  SplitOn _ _ rhs -> extract rhs
-  Done v -> v
+type Valuation l = Map.Map l Bool
+
+extract :: (Ord l) => Valuation l -> RTree l i -> i
+extract v = \case
+  SplitWith ml lhs rhs -> case ml >>= (`Map.lookup` v) of
+    Just False -> extract v lhs
+    _ -> extract v rhs
+  Done i -> i
 
 instance Applicative (RTree l) where
   pure = Done
@@ -46,89 +62,134 @@ instance Applicative (RTree l) where
 instance Monad (RTree l) where
   ma >>= f = case ma of
     Done i -> f i
-    Split lhs rhs ->
-      Split (lhs >>= f) (rhs >>= f)
-    SplitOn l lhs rhs ->
-      SplitOn l (lhs >>= f) (rhs >>= f)
+    SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
 
 instance MonadReduce l (RTree l) where
-  splitWith = \case
-    Just n -> SplitOn n
-    Nothing -> Split
+  splitWith = SplitWith
 
 reduce
-  :: forall m l i
-   . (Alternative m)
-  => (i -> m ())
-  -> RTree l i
-  -> m i
-reduce p = checkgo
- where
-  go = \case
-    (Done i) -> pure i
-    (Split lhs rhs) -> (checkgo lhs <|> go rhs)
-    (SplitOn _ lhs rhs) -> (checkgo lhs <|> go rhs)
-  checkgo rt = p (extract rt) *> go rt
-{-# SPECIALIZE reduce :: (i -> MaybeT IO ()) -> RTree l i -> MaybeT IO i #-}
-
-type Valuation l = Map.Map l Bool
-
-extractL :: (Ord l) => Valuation l -> RTree l i -> i
-extractL v = \case
-  Split _ rhs -> extractL v rhs
-  SplitOn l lhs rhs -> case Map.lookup l v of
-    Just False -> extractL v lhs
-    _ -> extractL v rhs
-  Done i -> i
-
-reduceL
   :: forall m l i
    . (Alternative m, Ord l)
-  => (Valuation l -> i -> m ())
+  => (i -> m ())
   -> Valuation l
   -> RTree l i
   -> m i
-reduceL p = checkgo
+reduce p = checkgo
  where
-  checkgo v r = p v (extractL v r) *> go v r
+  checkgo v r = p (extract v r) *> go v r
   go v = \case
     Done i -> pure i
-    SplitOn l lhs rhs -> case Map.lookup l v of
+    SplitWith (Just l) lhs rhs -> case Map.lookup l v of
       Just True -> checkgo v rhs
       Just False -> checkgo v lhs
       Nothing -> checkgo (Map.insert l False v) lhs <|> go (Map.insert l True v) rhs
-    Split lhs rhs -> (checkgo v lhs <|> go v rhs)
-{-# INLINE reduceL #-}
-
-data ReState l = ReState ![Bool] !(Valuation l)
-
-newtype IRTree l i = IRTree {runIRTree :: ReState l -> (i, ReState l)}
-  deriving (Functor, Applicative, Monad) via (State (ReState l))
-
-instance (Ord l) => MonadReduce l (IRTree l) where
-  checkWith = \case
-    Nothing ->
-      IRTree \case
-        ReState (a : as) v -> (a, ReState as v)
-        ReState [] v -> (False, ReState [] v)
-    Just l -> IRTree \case
-      ReState as v@(Map.lookup l -> Just x) -> (not x, ReState as v)
-      ReState (a : as) v -> (a, ReState as (Map.insert l (not a) v))
-      ReState [] v -> (False, ReState [] (Map.insert l True v))
-
-reduceI
+    SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
+{-# INLINE reduce #-}
+
+data ReState l = ReState
+  { choices :: [Bool]
+  , valuation :: !(Valuation l)
+  }
+
+type IRTree l = IRTreeT l Identity
+
+newtype IRTreeT l m i = IRTreeT {runIRTreeT :: StateT (ReState l) m i}
+  deriving (Functor, Applicative, Monad) via (StateT (ReState l) m)
+  deriving (MonadTrans) via (StateT (ReState l))
+
+instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
+  checkWith =
+    IRTreeT . StateT . \case
+      Nothing -> \case
+        ReState (uncons -> (a, as)) v ->
+          pure (a, ReState as v)
+      Just l -> \case
+        ReState as v@(Map.lookup l -> Just x) ->
+          pure (x, ReState as v)
+        ReState (uncons -> (a, as)) v ->
+          pure (a, ReState as (Map.insert l a v))
+   where
+    uncons [] = (True, [])
+    uncons (a : as) = (a, as)
+  {-# INLINE checkWith #-}
+
+iextract :: (Ord l) => Valuation l -> IRTree l a -> a
+iextract v t = runIdentity $ iextractT v t
+{-# INLINE iextract #-}
+
+iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m i
+iextractT v (IRTreeT m) = evalStateT m (ReState [] v)
+{-# INLINE iextractT #-}
+
+ireduce
   :: forall m l i
    . (Monad m, Ord l)
-  => (Valuation l -> i -> m Bool)
+  => (i -> m Bool)
   -> Valuation l
   -> IRTree l i
   -> m i
-reduceI p v (IRTree m) = go []
+ireduce = ireduceT (pure . runIdentity)
+{-# INLINE ireduce #-}
+
+-- | Interpreted reduction with an m base monad
+ireduceT
+  :: forall t m l i
+   . (Monad m, Monad t, Ord l)
+  => (forall a. m a -> t a)
+  -- ^ a lift of monad m into t (normally @id@ or @lift@)
+  -> (i -> t Bool)
+  -> Valuation l
+  -> IRTreeT l m i
+  -> t i
+ireduceT lift_ p v (IRTreeT m) = go []
  where
   go pth =
-    case m (ReState pth v) of
-      (i, ReState [] v') -> do
-        t <- p v' i
-        go (pth <> [t])
+    lift_ (runStateT m (ReState pth v)) >>= \case
+      (i, ReState [] _) -> do
+        t <- p i
+        -- if the predicate is true, we can reduce to the false branch.
+        go (pth <> [not t])
+      (i, _) -> pure i
+{-# INLINE ireduceT #-}
+
+ireduceExp
+  :: forall m l i
+   . (Monad m, Ord l)
+  => (i -> m Bool)
+  -> Valuation l
+  -> IRTree l i
+  -> m i
+ireduceExp = ireduceExpT (pure . runIdentity)
+{-# INLINE ireduceExp #-}
+
+-- | Interpreted reduction with an m base monad, and running in expoential mode.
+ireduceExpT
+  :: forall t m l i
+   . (Monad m, Monad t, Ord l)
+  => (forall a. m a -> t a)
+  -- ^ a lift of monad m into t (normally @id@ or @lift@)
+  -> (i -> t Bool)
+  -> Valuation l
+  -> IRTreeT l m i
+  -> t i
+ireduceExpT lift_ p v (IRTreeT (StateT m)) = go 0 []
+ where
+  -- here n is the number of explorative elements
+  go n pth =
+    lift_ (m $ ReState pth v) >>= \case
+      (i, ReState [] _) -> do
+        p i >>= \case
+          True -> do
+            let n' = next n
+            go n' (pth <> replicate n' False)
+          False -> do
+            case n of
+              0 -> go 0 (pth <> [True])
+              n' -> go n' $ take (length pth - prev n') pth
       (i, _) -> pure i
-{-# INLINE reduceI #-}
+
+  next 0 = 1
+  next n = n * 2
+
+  prev 1 = 0
+  prev n = n `quot` 2