Let's try this

rtree-c/bench/Main.hs

@@ -2,6 +2,7 @@
 
 import Criterion.Main
 
+import Control.DeepSeq
 import qualified Language.C as C
 import qualified Language.C.System.GCC as C
 import ReduceC
@@ -17,6 +18,10 @@ main = do
          in bgroup
               "clang-26760"
               [ bench "extract" $ nf IRTree.extract r
-              , bench "probe 11" $ nf (`IRTree.probe` "11") r
+              , bench "probe 11" $ nf (\r -> let (i, _, _) = IRTree.probe r "11" in i) r
+              , bench "reduce true" $
+                  nfAppIO
+                    (IRTree.reduceAdaptive (\_ i -> i `deepseq` pure True))
+                    r
               ]
     ]

rtree-c/bin/Main.hs

@@ -53,7 +53,6 @@ process sev p ma = do
 data Mode
   = Lin
   | Exp
-  | Fib
   deriving (Show, Read, Eq, Ord, Enum)
 
 run :: (HasCallStack) => Parser (IO ())
@@ -62,8 +61,8 @@ run = do
     option auto $
       fold
         [ long "mode"
-        , help "search mode (Lin, Exp, Fib)"
-        , value Lin
+        , help "search mode (Lin, Exp)"
+        , value Exp
         ]
 
   checkmode <-
@@ -150,18 +149,18 @@ run = do
           liftIO exitFailure
 
         check' f l c = process D "Checking predictate" do
-          let xs = NE.nonEmpty (filter fst l)
+          let xs = NE.nonEmpty (filter ((RPath.Yes ==) . RPath.choice) l)
           logInfo
             ( "Checking D="
-                <> Text.pack (show (maybe 0 NE.length xs))
+                <> Text.pack (show (RPath.numberOfUndecided l) <> "/" <> show (length l))
                 <> ": "
-                <> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . snd . NE.last) xs)
+                <> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . RPath.label . NE.last) xs)
             )
           when debug do
             pPrint (void c)
           when pedandic do
             liftIO $ copyFile f (f <.> "last")
-          logDebug (Text.pack . show $ RPath.fromChoiceList $ map fst l)
+          -- logDebug (Text.pack . show $ RPath.fromChoiceList $ map fst l)
           output f c
           v <- validiate f
           res <-
@@ -220,24 +219,18 @@ run = do
 
       l <-
         c & fix \rec prevc -> do
-          mc' <-
+          c' <-
             ( case mode of
                 Lin -> IRTree.reduce
-                Exp -> IRTree.reduceExp
-                Fib -> IRTree.reduceFib
+                Exp -> IRTree.reduceAdaptive
               )
               (check' file)
               (ReduceC.defaultReduceC prevc)
-          case mc' of
-            Just c' ->
           if fixpoint && (c' $> ()) /= (prevc $> ())
             then do
               logInfo "Running again until fixpoint"
               rec c'
             else pure c'
-            Nothing -> do
-              logError "Was unable to produce any output"
-              cleanup file
 
       when pedandic do
         liftIO $ copyFile file (file <.> "last")

rtree-c/package.yaml

@@ -5,7 +5,7 @@ name: rtree-c
 # category: categories
 # extra-source-files: []
 
-ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto
+ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
 
 dependencies:
   - base >= 4.9 && < 5
@@ -83,3 +83,4 @@ benchmarks:
       - filepath
       - typed-process
       - text
+      - deepseq

rtree-c/rtree-c.cabal

@@ -15,7 +15,7 @@ library
       Paths_rtree_c
   hs-source-dirs:
       src
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
   build-depends:
       base >=4.9 && <5
     , containers
@@ -34,7 +34,7 @@ executable rtree-c
       Paths_rtree_c
   hs-source-dirs:
       bin/
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
   build-depends:
       base >=4.9 && <5
     , co-log
@@ -64,7 +64,7 @@ test-suite rtree-c-test
       Paths_rtree_c
   hs-source-dirs:
       test/src
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
   build-depends:
       base >=4.9 && <5
     , containers
@@ -93,7 +93,7 @@ benchmark rtree-c-bench
       Paths_rtree_c
   hs-source-dirs:
       bench/
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto -O2 -threaded
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late -O2 -threaded
   build-depends:
       base >=4.9 && <5
     , containers
@@ -119,11 +119,12 @@ benchmark rtree-c-profile
       Paths_rtree_c
   hs-source-dirs:
       bench/
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-auto -O -threaded -fprof-late "-with-rtsopts=-N -p -s -hc -i0.1 -L500"
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late -O -threaded -fprof-late "-with-rtsopts=-N -p -s -hc -i0.1 -L500"
   build-depends:
       base >=4.9 && <5
     , containers
     , criterion
+    , deepseq
     , directory
     , filepath
     , language-c

rtree/package.yaml

@@ -5,7 +5,7 @@ name: rtree
 # category: categories
 # extra-source-files: []
 
-ghc-options: -Wall -fno-warn-incomplete-uni-patterns 
+ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
 
 dependencies:
   - base >= 4.9 && < 5

rtree/rtree.cabal

@@ -19,7 +19,7 @@ library
       Paths_rtree
   hs-source-dirs:
       src
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
   build-depends:
       base >=4.9 && <5
     , containers
@@ -41,7 +41,7 @@ test-suite rtree-test
       Paths_rtree
   hs-source-dirs:
       test/src
-  ghc-options: -Wall -fno-warn-incomplete-uni-patterns
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns -fprof-late
   build-depends:
       base >=4.9 && <5
     , bytestring

rtree/src/Control/Monad/IRTree.hs

@@ -53,6 +53,7 @@ newtype IRTreeT l m i = IRTreeT (RWST RPath (Endo [l]) Int m i)
 instance (Monad m) => MonadReduce l (IRTreeT l m) where
   check l = IRTreeT . RWST $ \rp i -> do
     pure (indexChoice rp i, i + 1, Endo (l :))
+  {-# INLINE check #-}
 
 extract :: IRTree l i -> i
 extract t = runIdentity $ extractT t
@@ -77,7 +78,7 @@ probeT (IRTreeT m) pth =
 {-# INLINE probeT #-}
 
 reduce
-  :: (Monad m, m ~ IO, Show l)
+  :: (Monad m)
   => ([AnnotatedChoice l] -> i -> m Bool)
   -> IRTree l i
   -> m i
@@ -86,7 +87,7 @@ reduce = reduceT (pure . runIdentity)
 
 -- | Interpreted reduction with an m base monad
 reduceT
-  :: (Monad m, Functor t, m ~ IO, Show l)
+  :: (Monad m, Functor t)
   => (forall a. t a -> m a)
   -> ([AnnotatedChoice l] -> i -> m Bool)
   -> IRTreeT l t i
@@ -105,7 +106,7 @@ reduceT lift_ p rt = do
 {-# INLINE reduceT #-}
 
 reduceAdaptive
-  :: (Monad m, m ~ IO, Show i, Show l)
+  :: (Monad m)
   => ([AnnotatedChoice l] -> i -> m Bool)
   -> IRTree l i
   -> m i
@@ -114,7 +115,7 @@ reduceAdaptive = reduceAdaptiveT (pure . runIdentity)
 
 -- | Interpreted reduction with an m base monad, but using exponential search.
 reduceAdaptiveT
-  :: (Monad m, Functor t, IO ~ m, Show i, Show l)
+  :: (Monad m, Functor t)
   => (forall a. t a -> m a)
   -- ^ a lift of monad m into t (normally @id@ or @lift@)
   -> ([AnnotatedChoice l] -> i -> m Bool)

rtree/src/Control/Monad/Reduce.hs

@@ -100,6 +100,7 @@ type MonadReducePlus l m = (MonadReduce l m, MonadPlus m)
 
 instance (MonadReduce l m) => MonadReduce l (MaybeT m) where
   split l (MaybeT lhs) (MaybeT rhs) = MaybeT (split l lhs rhs)
+  {-# INLINE split #-}
 
 -- | Continues if the fact is true.
 given :: (MonadReducePlus l m) => l -> m ()