diff --git a/rtree-c/bin/Main.hs b/rtree-c/bin/Main.hs index aad22c6db5ad89a53241a7f0eb5a8a2ed92fac6b..5cffc1276b459114f0677f6261f5cbfb1ed9eeb4 100644 --- a/rtree-c/bin/Main.hs +++ b/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' diff --git a/rtree/src/Control/Monad/IRTree.hs b/rtree/src/Control/Monad/IRTree.hs index 3464d5fa27530996971f49994653c53f55d91e3d..517b8c276e11e73d305461ad82ee116cb06ad720 100644 --- a/rtree/src/Control/Monad/IRTree.hs +++ b/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 #-} diff --git a/rtree/test/src/Control/Monad/IRTreeSpec.hs b/rtree/test/src/Control/Monad/IRTreeSpec.hs index 4b2731f13226e38a6d98e7395b862c5a9523c13e..2d312562fa35e257c0d575dab7a3944820ae1b5e 100644 --- a/rtree/test/src/Control/Monad/IRTreeSpec.hs +++ b/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