Add fibonacci mode

rtree-c/bin/Main.hs

@@ -49,13 +49,20 @@ process sev p ma = do
   s = withFrozenCallStack callStack
   msg t = Colog.logMsg (Msg sev s (t <> p))
 
+data Mode
+  = Lin
+  | Exp
+  | Fib
+  deriving (Show, Read, Eq, Ord, Enum)
+
 run :: (HasCallStack) => Parser (IO ())
 run = do
-  expmode <-
-    flag False True $
+  mode <-
+    option auto $
       fold
-        [ long "exp"
-        , help "run in exponential mode"
+        [ long "mode"
+        , help "search mode (Lin, Exp, Fib)"
+        , value "Lin"
         ]
 
   checkmode <-
@@ -206,12 +213,16 @@ run = do
       l <-
         c & fix \rec prevc -> do
           mc' <-
-            (if expmode then IRTree.reduceExp else IRTree.reduce)
+            ( case mode of
+                Lin -> IRTree.reduce
+                Exp -> IRTree.reduceExp
+                Fib -> IRTree.reduceFib
+              )
               (check' file)
               (ReduceC.defaultReduceC prevc)
           case mc' of
             Just c' ->
-              if fixpoint && c' /= c
+              if fixpoint && (c' $> ()) /= (prevc $> ())
                 then do
                   logInfo "Running again until fixpoint"
                   rec c'

rtree/src/Control/Monad/IRTree.hs

@@ -12,12 +12,14 @@ module Control.Monad.IRTree (
   probe,
   reduce,
   reduceExp,
+  reduceFib,
 
   -- * IRTreeT
   IRTreeT,
   probeT,
   extractT,
   reduceT,
+  reduceFibT,
   reduceExpT,
 
   -- * Re-exports
@@ -105,6 +107,14 @@ reduceExp
 reduceExp = reduceExpT (pure . runIdentity)
 {-# INLINE reduceExp #-}
 
+reduceFib
+  :: (Monad m)
+  => ([(Bool, l)] -> i -> m Bool)
+  -> IRTree l i
+  -> m (Maybe i)
+reduceFib = reduceFibT (pure . runIdentity)
+{-# INLINE reduceFib #-}
+
 -- | Interpreted reduction with an m base monad, and running in expoential mode.
 reduceExpT
   :: (Monad m, Functor t)
@@ -135,3 +145,34 @@ reduceExpT lift_ p rt = do
             n' -> go (n' - 1) sq
       else pure i
 {-# INLINE reduceExpT #-}
+
+-- | Interpreted reduction with an m base monad, and running in fibonacci mode.
+reduceFibT
+  :: (Monad m, Functor t)
+  => (forall a. t a -> m a)
+  -- ^ a lift of monad m into t (normally @id@ or @lift@)
+  -> ([(Bool, l)] -> i -> m Bool)
+  -> IRTreeT l t i
+  -> m (Maybe i)
+reduceFibT lift_ p rt = do
+  (i, l) <- lift_ (probeT rt "")
+  t <- p l i
+  if t
+    then Just <$> go 1 1 Seq.empty
+    else pure Nothing
+ where
+  go n m sq = do
+    let depth = m
+    let sq' = sq <> Seq.replicate depth True
+    let pth' = fromChoiceList (toList sq')
+    (i, l) <- lift_ (probeT rt pth')
+    if length l >= numberOfChoices pth' - depth + 1
+      then do
+        t <- p l i
+        if t
+          then go m (n + m) sq'
+          else case m of
+            1 -> go 1 1 (sq Seq.|> False)
+            m' -> go (m' - n) n sq
+      else pure i
+{-# INLINE reduceFibT #-}

rtree/test/src/Control/Monad/IRTreeSpec.hs

@@ -35,11 +35,11 @@ spec = describe "examples" do
 
     let re = runReaderT (Expr.rExpr e) Map.empty
 
-    -- let
-    --   predicate :: Expr -> IO Bool
-    --   predicate = pure . contains isOpr
+    let
+      predicate :: Expr -> IO Bool
+      predicate = pure . contains isOpr
 
-    -- rex <- runIO $ RTree.reduce predicate re
+    rex <- runIO $ RTree.reduce predicate re
 
     -- onGlitterWith
     --   ("test/expected/" <> str <> "-red")
@@ -52,10 +52,13 @@ spec = describe "examples" do
     --     it "should produce the same results as the RTree" \mex -> do
     --       rex `shouldBe` mex
 
-    -- it "should find an opr exponentially" do
-    --   (mex, result) <- runWriterT (IRTree.reduceExp (debugPredicate showString (prettyExprS 0) predicate) me)
-    --   rex `shouldBe` mex
-    --   pure $ glitter ("test/expected/" <> str <> "-red-exp") (appEndo result "")
+    it "should find an opr exponentially" do
+      (mex, _) <- runWriterT (IRTree.reduceExp (debugPredicate showString (prettyExprS 0) predicate) me)
+      rex `shouldBe` mex
+
+    it "should find an opr fibonacci" do
+      (mex, _) <- runWriterT (IRTree.reduceFib (debugPredicate showString (prettyExprS 0) predicate) me)
+      rex `shouldBe` mex
 
     it "should reduce like iinputs" do
       forM_ (RTree.iinputs re) \(ii, e') -> do