From f683bc09b40239f202be210ebef63611e2ada024 Mon Sep 17 00:00:00 2001
From: Christian Gram Kalhauge <chrg@dtu.dk>
Date: Thu, 15 Feb 2024 10:08:09 +0100
Subject: [PATCH] Work in progress

---
 flake.nix                                 |   1 +
 .ghci => rtree/.ghci                      |   2 +-
 rtree/.gitignore                          |   1 +
 rtree/hie.yml                             |   6 +
 rtree/package.yaml                        |  13 +
 rtree/rtree.cabal                         |  28 ++
 rtree/src/Control/Monad/RTree.hs          |  75 +++-
 rtree/src/Control/Monad/Reduce.hs         |  32 +-
 rtree/src/Control/RTree.hs                | 429 +++++++++++-----------
 rtree/test/expected/rexpr.txt/golden      |  49 +++
 rtree/test/src/Control/Monad/RTreeSpec.hs | 156 ++++++++
 rtree/test/src/Main.hs                    |   4 +
 rtree/test/src/Spec.hs                    |   1 +
 13 files changed, 562 insertions(+), 235 deletions(-)
 rename .ghci => rtree/.ghci (70%)
 create mode 100644 rtree/.gitignore
 create mode 100644 rtree/hie.yml
 create mode 100644 rtree/test/expected/rexpr.txt/golden
 create mode 100644 rtree/test/src/Control/Monad/RTreeSpec.hs
 create mode 100644 rtree/test/src/Main.hs
 create mode 100644 rtree/test/src/Spec.hs

diff --git a/flake.nix b/flake.nix
index 6b6cab8..c5ac7d3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -58,6 +58,7 @@
           haskell-language-server
           hpack
           fourmolu
+          hspec-golden
         ];
         withHoogle = true;
       in {
diff --git a/.ghci b/rtree/.ghci
similarity index 70%
rename from .ghci
rename to rtree/.ghci
index bb358d0..bdbdd4c 100644
--- a/.ghci
+++ b/rtree/.ghci
@@ -1,4 +1,4 @@
 :set -fwarn-unused-binds -fwarn-unused-imports
-:set -isrc -ibin/rtree-c
+:set -isrc -itest/src
 :load Main
 
diff --git a/rtree/.gitignore b/rtree/.gitignore
new file mode 100644
index 0000000..508061b
--- /dev/null
+++ b/rtree/.gitignore
@@ -0,0 +1 @@
+actual
diff --git a/rtree/hie.yml b/rtree/hie.yml
new file mode 100644
index 0000000..8d5eb2b
--- /dev/null
+++ b/rtree/hie.yml
@@ -0,0 +1,6 @@
+cradle:
+  cabal:
+    - path: "./src"
+      component: "lib:rtree"
+    - path: "./test/src"
+      component: "test:rtree-test"
diff --git a/rtree/package.yaml b/rtree/package.yaml
index 0330af8..ec871b1 100644
--- a/rtree/package.yaml
+++ b/rtree/package.yaml
@@ -11,6 +11,7 @@ dependencies:
   - base >= 4.9 && < 5
   - transformers
   - vector
+  - indexed-traversable
   - mtl
   - containers
   - text
@@ -18,3 +19,15 @@ dependencies:
 library:
   source-dirs: src
 
+tests:
+  rtree-test:
+    source-dirs: test/src
+    main: Main.hs
+    dependencies:
+      - rtree
+      - hedgehog
+      - hspec
+      - hspec-discover
+      - hspec-expectations-pretty-diff
+      - hspec-hedgehog
+      - hspec-golden
diff --git a/rtree/rtree.cabal b/rtree/rtree.cabal
index 99d96be..d567a57 100644
--- a/rtree/rtree.cabal
+++ b/rtree/rtree.cabal
@@ -22,8 +22,36 @@ library
   build-depends:
       base >=4.9 && <5
     , containers
+    , indexed-traversable
     , mtl
     , text
     , transformers
     , vector
   default-language: Haskell2010
+
+test-suite rtree-test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Control.Monad.RTreeSpec
+      Spec
+      Paths_rtree
+  hs-source-dirs:
+      test/src
+  ghc-options: -Wall -fno-warn-incomplete-uni-patterns
+  build-depends:
+      base >=4.9 && <5
+    , containers
+    , hedgehog
+    , hspec
+    , hspec-discover
+    , hspec-expectations-pretty-diff
+    , hspec-golden
+    , hspec-hedgehog
+    , indexed-traversable
+    , mtl
+    , rtree
+    , text
+    , transformers
+    , vector
+  default-language: Haskell2010
diff --git a/rtree/src/Control/Monad/RTree.hs b/rtree/src/Control/Monad/RTree.hs
index c904799..5210cf1 100644
--- a/rtree/src/Control/Monad/RTree.hs
+++ b/rtree/src/Control/Monad/RTree.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -14,14 +15,17 @@ module Control.Monad.RTree (
   RTree,
   extract,
   inputs,
+  iinputs,
   reduce,
+  drawRTree,
 
   -- * RTreeT and RTreeN
   RTreeT (..),
   extractT,
   reduceT,
   RTreeN (..),
-  extractN,
+  unStateT,
+  flattenT,
 
   -- * Re-exports
   module Control.Monad.Reduce,
@@ -29,9 +33,13 @@ module Control.Monad.RTree (
 
 import Control.Applicative
 import Control.Monad
+import Control.Monad.Identity
 import Control.Monad.Reduce
 import Control.Monad.State
-import qualified Data.Foldable as Foldable
+import Data.Foldable
+import Data.Foldable.WithIndex
+import Data.Function ((&))
+import Data.Tree
 
 -- | The simple RTree
 data RTree i
@@ -51,6 +59,12 @@ instance Monad RTree where
 instance MonadReduce RTree where
   split = Split
 
+instance FoldableWithIndex RPath RTree where
+  ifoldMap f =
+    [] & fix \rec rs -> \case
+      Done i -> f (fromChoiceList (reverse rs)) i
+      Split lhs rhs -> rec (False : rs) lhs <> rec (True : rs) rhs
+
 -- | Extract the top value from the RTree.
 extract :: RTree i -> i
 extract = \case
@@ -58,9 +72,21 @@ extract = \case
   Done i -> i
 {-# INLINE extract #-}
 
--- | A simple wrapper around @toList@
+-- | A list of inputs, A simple wrapper around @toList@
 inputs :: RTree i -> [i]
-inputs = Foldable.toList
+inputs = toList
+
+-- | A list of indexed inputs, A simple wrapper around @itoList@
+iinputs :: RTree i -> [(RPath, i)]
+iinputs = itoList
+
+-- | For debugging purposes
+drawRTree :: (i -> String) -> RTree i -> String
+drawRTree pp rt = drawTree (go rt)
+ where
+  go = \case
+    Done i -> Node (pp i) []
+    Split lhs rhs -> Node "<|" [go rhs, go lhs]
 
 -- | Reduce the tree
 reduce :: (MonadPlus m) => (i -> m Bool) -> RTree i -> m i
@@ -77,7 +103,7 @@ reduce p = checkgo
 -- | An RTreeT Node
 data RTreeN m i
   = DoneN !i
-  | SplitN !(RTreeT m i) !(RTreeN m i)
+  | SplitN !(RTreeT m i) !(RTreeT m i)
   deriving (Functor, Foldable)
 
 newtype RTreeT m i = RTreeT {unRTreeT :: m (RTreeN m i)}
@@ -89,26 +115,39 @@ instance (Monad m) => Applicative (RTreeT m) where
 
 instance (Monad m) => Monad (RTreeT m) where
   RTreeT ma >>= f = RTreeT $ do
-    ma >>= go
-   where
-    go = \case
+    ma >>= \case
       DoneN i -> unRTreeT (f i)
-      SplitN lhs rhs -> SplitN (lhs >>= f) <$> go rhs
+      SplitN lhs rhs -> pure $ SplitN (lhs >>= f) (rhs >>= f)
+
+instance (Monad m) => MonadReduce (RTreeT m) where
+  split lhs rhs = RTreeT (pure $ SplitN lhs rhs)
 
 instance (MonadState s m) => MonadState s (RTreeT m) where
   state f = RTreeT (DoneN <$> state f)
 
 -- | Extract a value from an @RTreeT@
-extractT :: (Functor m) => RTreeT m b -> m b
-extractT (RTreeT m) = extractN <$> m
+extractT :: (Monad m) => RTreeT m b -> m b
+extractT (RTreeT m) = m >>= extractN
 {-# INLINE extractT #-}
 
-extractN :: RTreeN m i -> i
+extractN :: (Monad m) => RTreeN m b -> m b
 extractN = \case
-  DoneN i -> i
-  SplitN _ rhs -> extractN rhs
+  DoneN i -> pure i
+  SplitN _ rhs -> extractT rhs
 {-# INLINE extractN #-}
 
+unStateT :: (Monad m) => RTreeT (StateT s m) i -> s -> RTreeT m (i, s)
+unStateT (RTreeT (StateT sf)) s = RTreeT do
+  (t, s') <- sf s
+  case t of
+    DoneN i -> pure $ DoneN (i, s')
+    SplitN lhs rhs -> pure $ SplitN (unStateT lhs s') (unStateT rhs s')
+
+flattenT :: RTreeT Identity i -> RTree i
+flattenT (RTreeT (Identity t)) = case t of
+  DoneN i -> Done i
+  SplitN lhs rhs -> Split (flattenT lhs) (flattenT rhs)
+
 -- | Reduction in @RTreeT@
 reduceT
   :: forall i m n
@@ -120,12 +159,12 @@ reduceT
   -> n i
 reduceT lift_ p = checkgo
  where
-  checkgo r = do
-    r' <- lift_ (unRTreeT r)
-    t <- p (extractN r')
+  checkgo (RTreeT r) = do
+    r' <- lift_ r
+    t <- p =<< lift_ (extractN r')
     unless t mzero
     go r'
   go = \case
     DoneN i -> pure i
-    SplitN lhs rhs -> checkgo lhs <|> go rhs
+    SplitN lhs rhs -> checkgo lhs <|> (lift_ (unRTreeT rhs) >>= go)
 {-# INLINE reduceT #-}
diff --git a/rtree/src/Control/Monad/Reduce.hs b/rtree/src/Control/Monad/Reduce.hs
index 1b45e8a..e498663 100644
--- a/rtree/src/Control/Monad/Reduce.hs
+++ b/rtree/src/Control/Monad/Reduce.hs
@@ -20,12 +20,17 @@ module Control.Monad.Reduce (
 
   -- * Combinators
   collect,
-  collectNonEmpty,
-  collectNonEmpty',
 
   -- * MonadReducePlus
   MonadReducePlus,
   given,
+  collectNonEmpty,
+  collectNonEmpty',
+
+  -- * RPath
+  RPath,
+  fromChoiceList,
+  toChoiceList,
 
   -- * Helpers
   onBoth,
@@ -36,8 +41,11 @@ module Control.Monad.Reduce (
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Trans.Maybe
+import Data.Bool
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe
+import Data.String
+import qualified Data.Vector.Unboxed as VU
 
 -- {- | A reducer should extract itself
 -- @
@@ -119,3 +127,23 @@ liftMaybeT m = runMaybeT m >>= liftMaybe
 onBoth :: (MonadPlus m) => m a -> m a -> (a -> a -> m a) -> m a
 onBoth mlhs mrhs fn =
   join $ (fn <$> mlhs <*> mrhs) <|> fmap pure mrhs <|> fmap pure mlhs
+
+{- | A reduction path, can be used as an index into reduction tree.
+Is isomorphic to a list of choices.
+-}
+newtype RPath = RPath {rPathAsVector :: VU.Vector Bool}
+  deriving (Eq, Ord)
+
+-- | Create a reduction path from a list of choices
+fromChoiceList :: [Bool] -> RPath
+fromChoiceList = RPath . VU.fromList
+
+-- | Get a list of choices from a reduction path.
+toChoiceList :: RPath -> [Bool]
+toChoiceList = VU.toList . rPathAsVector
+
+instance Show RPath where
+  show = show . map (bool '0' '1') . toChoiceList
+
+instance IsString RPath where
+  fromString = fromChoiceList . map (== '1')
diff --git a/rtree/src/Control/RTree.hs b/rtree/src/Control/RTree.hs
index 32caea3..7290fb6 100644
--- a/rtree/src/Control/RTree.hs
+++ b/rtree/src/Control/RTree.hs
@@ -15,219 +15,220 @@
 Module: Control.RTree
 -}
 module Control.RTree (
-  -- # RTree
-  RTree (..),
-  extract,
-  reduce,
-  reduceMaybe,
-  -- # IRTree
-  IRTree,
-  iextract,
-  ireduce,
-  ireduceExp,
-  IRTreeT (..),
-  iextractT,
-  ireduceT,
-  ireduceExpT,
-  ReState (..),
-  -- # Valuation
-  Valuation,
-) where
-
-import Control.Applicative
-import Control.Monad.Reader
-import Control.Monad.State.Strict
-import Data.Functor.Identity
-
-import qualified Data.Vector as V
-
-import Control.Monad.Reduce
-import Control.Monad.Trans.Maybe
-import Data.Bits
-import Data.Maybe
-import qualified Data.Valuation as Val
-
-type Valuation = Val.Valuation
-type Truth = Val.Truth
-
-data RTree l i
-  = Bottom
-  | Done i
-  | SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
-  deriving (Functor)
-
-extract :: (Ord l) => Valuation l -> RTree l i -> Maybe i
-extract v = \case
-  Bottom -> Nothing
-  SplitWith ml lhs rhs -> case ml >>= Val.condition v of
-    Just v' -> extract v' rhs
-    _ -> extract v lhs
-  Done i -> Just i
-
-instance Applicative (RTree l) where
-  pure = Done
-  (<*>) = ap
-
-instance Monad (RTree l) where
-  ma >>= f = case ma of
-    Bottom -> Bottom
-    Done i -> f i
-    SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
-
-instance MonadReduce l (RTree l) where
-  splitWith = SplitWith
-  bottom = Bottom
-
-reduce
-  :: forall m l i
-   . (Alternative m, Ord l)
-  => (Valuation l -> i -> m ())
-  -> Valuation l
-  -> RTree l i
-  -> m i
-reduce p = checkgo
- where
-  checkgo v r =
-    case extract v r of
-      Nothing -> empty
-      Just e -> p v e *> go v r
-  go v = \case
-    Bottom -> empty
-    Done i -> pure i
-    SplitWith (Just l) lhs rhs -> case Val.truthValue v (Val.label l) of
-      Just t
-        | t == Val.truth l -> checkgo v rhs
-        | otherwise -> checkgo v lhs
-      Nothing -> checkgo (Val.withTruth v $ Val.not l) lhs <|> go (Val.withTruth v l) rhs
-    SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
-{-# INLINE reduce #-}
-
-reduceMaybe
-  :: forall m l i
-   . (Monad m, Ord l)
-  => (Valuation l -> i -> m Bool)
-  -> Valuation l
-  -> RTree l i
-  -> m (Maybe i)
-reduceMaybe p v rt =
-  runMaybeT
-    $ reduce
-      ( \v' i -> do
-          t <- lift (p v' i)
-          unless t empty
-      )
-      v
-      rt
+-- -- # RTree
+-- RTree (..),
+-- extract,
+-- reduce,
+-- reduceMaybe,
+-- -- # IRTree
+-- IRTree,
+-- iextract,
+-- ireduce,
+-- ireduceExp,
+-- IRTreeT (..),
+-- iextractT,
+-- ireduceT,
+-- ireduceExpT,
+-- ReState (..),
+-- -- # Valuation
+-- Valuation,
 
-data ReState l = ReState
-  { choices :: V.Vector Bool
-  , progress :: Int
-  , valuation :: !(Valuation l)
-  }
-
-type IRTree l = IRTreeT l Identity
-
-newtype IRTreeT l m i = IRTreeT {runIRTreeT :: MaybeT (StateT (ReState l) m) i}
-  deriving (Functor, Applicative, Alternative, Monad, MonadPlus) via (MaybeT (StateT (ReState l) m))
-
-instance MonadTrans (IRTreeT l) where
-  lift m = IRTreeT (lift (lift m))
-
-instance (MonadState s m) => MonadState s (IRTreeT l m) where
-  state s = lift (state s)
-
-instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
-  bottom = mzero
-  checkWith =
-    IRTreeT . MaybeT . StateT . \case
-      Nothing -> \case
-        ReState ch i v ->
-          pure (Just (fromMaybe True (ch V.!? i)), ReState ch (i + 1) v)
-      Just l -> \case
-        ReState ch i v@((`Val.truthValue` Val.label l) -> Just t) ->
-          pure (Just (t == Val.truth l), ReState ch i v)
-        ReState ch i v ->
-          let a = fromMaybe True (ch V.!? i)
-           in pure (Just a, ReState ch (i + 1) (Val.withTruth v (if a then l else Val.not l)))
-  {-# INLINE checkWith #-}
-
-iextract :: (Ord l) => Valuation l -> IRTree l a -> Maybe a
-iextract v t = runIdentity $ iextractT v t
-{-# INLINE iextract #-}
-
-iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m (Maybe i)
-iextractT v (IRTreeT m) = evalStateT (runMaybeT m) (ReState V.empty 0 v)
-{-# INLINE iextractT #-}
-
-ireduce
-  :: forall m l i
-   . (Monad m, Ord l)
-  => (ReState l -> Maybe i -> m Bool)
-  -> Valuation l
-  -> IRTree l i
-  -> m (Maybe i)
-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@)
-  -> (ReState l -> Maybe i -> t Bool)
-  -> Valuation l
-  -> IRTreeT l m i
-  -> t (Maybe i)
-ireduceT lift_ p v (IRTreeT m) = go V.empty
- where
-  go pth = do
-    -- Try to run the false branch.
-    let pth' = pth <> V.singleton False
-    result <- lift_ (runStateT (runMaybeT m) (ReState pth' 0 v))
-    case result of
-      (mi, ReState _ i v') | i >= V.length pth' -> do
-        t <- p (ReState pth' i v') mi
-        -- if the predicate is true, we can reduce to the false branch.
-        go (pth <> V.singleton (not t))
-
-      -- if we no more choices are needed, stop.
-      (mi, _) -> pure mi
-{-# INLINE ireduceT #-}
-
-ireduceExp
-  :: forall m l i
-   . (Monad m, Ord l)
-  => (ReState l -> Maybe i -> m Bool)
-  -> Valuation l
-  -> IRTree l i
-  -> m (Maybe i)
-ireduceExp = ireduceExpT (pure . runIdentity)
-{-# INLINE ireduceExp #-}
+) where
 
--- | 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@)
-  -> (ReState l -> Maybe i -> t Bool)
-  -> Valuation l
-  -> IRTreeT l m i
-  -> t (Maybe i)
-ireduceExpT lift_ p v (IRTreeT m) = go 0 V.empty
- where
-  -- here n is the number of explorative elements
-  go n pth = do
-    let depth = shiftL 1 n
-    let pth' = pth <> V.replicate depth False
-    result <- lift_ (runStateT (runMaybeT m) $ ReState pth' 0 v)
-    case result of
-      (mi, ReState _ i v') | i >= length pth' - depth + 1 -> do
-        t <- p (ReState pth' i v') mi
-        if t
-          then go (n + 1) pth'
-          else case n of
-            0 -> go 0 (pth <> V.singleton True)
-            n' -> go (n' - 1) pth
-      (mi, _) -> pure mi
+-- import Control.Applicative
+-- import Control.Monad.Reader
+-- import Control.Monad.State.Strict
+-- import Data.Functor.Identity
+--
+-- import qualified Data.Vector as V
+--
+-- import Control.Monad.Reduce
+-- import Control.Monad.Trans.Maybe
+-- import Data.Bits
+-- import Data.Maybe
+-- import qualified Data.Valuation as Val
+--
+-- type Valuation = Val.Valuation
+-- type Truth = Val.Truth
+--
+-- data RTree l i
+--   = Bottom
+--   | Done i
+--   | SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
+--   deriving (Functor)
+--
+-- extract :: (Ord l) => Valuation l -> RTree l i -> Maybe i
+-- extract v = \case
+--   Bottom -> Nothing
+--   SplitWith ml lhs rhs -> case ml >>= Val.condition v of
+--     Just v' -> extract v' rhs
+--     _ -> extract v lhs
+--   Done i -> Just i
+--
+-- instance Applicative (RTree l) where
+--   pure = Done
+--   (<*>) = ap
+--
+-- instance Monad (RTree l) where
+--   ma >>= f = case ma of
+--     Bottom -> Bottom
+--     Done i -> f i
+--     SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
+--
+-- instance MonadReduce l (RTree l) where
+--   splitWith = SplitWith
+--   bottom = Bottom
+--
+-- reduce
+--   :: forall m l i
+--    . (Alternative m, Ord l)
+--   => (Valuation l -> i -> m ())
+--   -> Valuation l
+--   -> RTree l i
+--   -> m i
+-- reduce p = checkgo
+--  where
+--   checkgo v r =
+--     case extract v r of
+--       Nothing -> empty
+--       Just e -> p v e *> go v r
+--   go v = \case
+--     Bottom -> empty
+--     Done i -> pure i
+--     SplitWith (Just l) lhs rhs -> case Val.truthValue v (Val.label l) of
+--       Just t
+--         | t == Val.truth l -> checkgo v rhs
+--         | otherwise -> checkgo v lhs
+--       Nothing -> checkgo (Val.withTruth v $ Val.not l) lhs <|> go (Val.withTruth v l) rhs
+--     SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
+-- {-# INLINE reduce #-}
+--
+-- reduceMaybe
+--   :: forall m l i
+--    . (Monad m, Ord l)
+--   => (Valuation l -> i -> m Bool)
+--   -> Valuation l
+--   -> RTree l i
+--   -> m (Maybe i)
+-- reduceMaybe p v rt =
+--   runMaybeT
+--     $ reduce
+--       ( \v' i -> do
+--           t <- lift (p v' i)
+--           unless t empty
+--       )
+--       v
+--       rt
+--
+-- data ReState l = ReState
+--   { choices :: V.Vector Bool
+--   , progress :: Int
+--   , valuation :: !(Valuation l)
+--   }
+--
+-- type IRTree l = IRTreeT l Identity
+--
+-- newtype IRTreeT l m i = IRTreeT {runIRTreeT :: MaybeT (StateT (ReState l) m) i}
+--   deriving (Functor, Applicative, Alternative, Monad, MonadPlus) via (MaybeT (StateT (ReState l) m))
+--
+-- instance MonadTrans (IRTreeT l) where
+--   lift m = IRTreeT (lift (lift m))
+--
+-- instance (MonadState s m) => MonadState s (IRTreeT l m) where
+--   state s = lift (state s)
+--
+-- instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
+--   bottom = mzero
+--   checkWith =
+--     IRTreeT . MaybeT . StateT . \case
+--       Nothing -> \case
+--         ReState ch i v ->
+--           pure (Just (fromMaybe True (ch V.!? i)), ReState ch (i + 1) v)
+--       Just l -> \case
+--         ReState ch i v@((`Val.truthValue` Val.label l) -> Just t) ->
+--           pure (Just (t == Val.truth l), ReState ch i v)
+--         ReState ch i v ->
+--           let a = fromMaybe True (ch V.!? i)
+--            in pure (Just a, ReState ch (i + 1) (Val.withTruth v (if a then l else Val.not l)))
+--   {-# INLINE checkWith #-}
+--
+-- iextract :: (Ord l) => Valuation l -> IRTree l a -> Maybe a
+-- iextract v t = runIdentity $ iextractT v t
+-- {-# INLINE iextract #-}
+--
+-- iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m (Maybe i)
+-- iextractT v (IRTreeT m) = evalStateT (runMaybeT m) (ReState V.empty 0 v)
+-- {-# INLINE iextractT #-}
+--
+-- ireduce
+--   :: forall m l i
+--    . (Monad m, Ord l)
+--   => (ReState l -> Maybe i -> m Bool)
+--   -> Valuation l
+--   -> IRTree l i
+--   -> m (Maybe i)
+-- 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@)
+--   -> (ReState l -> Maybe i -> t Bool)
+--   -> Valuation l
+--   -> IRTreeT l m i
+--   -> t (Maybe i)
+-- ireduceT lift_ p v (IRTreeT m) = go V.empty
+--  where
+--   go pth = do
+--     -- Try to run the false branch.
+--     let pth' = pth <> V.singleton False
+--     result <- lift_ (runStateT (runMaybeT m) (ReState pth' 0 v))
+--     case result of
+--       (mi, ReState _ i v') | i >= V.length pth' -> do
+--         t <- p (ReState pth' i v') mi
+--         -- if the predicate is true, we can reduce to the false branch.
+--         go (pth <> V.singleton (not t))
+--
+--       -- if we no more choices are needed, stop.
+--       (mi, _) -> pure mi
+-- {-# INLINE ireduceT #-}
+--
+-- ireduceExp
+--   :: forall m l i
+--    . (Monad m, Ord l)
+--   => (ReState l -> Maybe i -> m Bool)
+--   -> Valuation l
+--   -> IRTree l i
+--   -> m (Maybe 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@)
+--   -> (ReState l -> Maybe i -> t Bool)
+--   -> Valuation l
+--   -> IRTreeT l m i
+--   -> t (Maybe i)
+-- ireduceExpT lift_ p v (IRTreeT m) = go 0 V.empty
+--  where
+--   -- here n is the number of explorative elements
+--   go n pth = do
+--     let depth = shiftL 1 n
+--     let pth' = pth <> V.replicate depth False
+--     result <- lift_ (runStateT (runMaybeT m) $ ReState pth' 0 v)
+--     case result of
+--       (mi, ReState _ i v') | i >= length pth' - depth + 1 -> do
+--         t <- p (ReState pth' i v') mi
+--         if t
+--           then go (n + 1) pth'
+--           else case n of
+--             0 -> go 0 (pth <> V.singleton True)
+--             n' -> go (n' - 1) pth
+--       (mi, _) -> pure mi
diff --git a/rtree/test/expected/rexpr.txt/golden b/rtree/test/expected/rexpr.txt/golden
new file mode 100644
index 0000000..af56d7a
--- /dev/null
+++ b/rtree/test/expected/rexpr.txt/golden
@@ -0,0 +1,49 @@
+<|
+|
++- <|
+|  |
+|  +- <|
+|  |  |
+|  |  +- x := 0; 1 + x with context 
+|  |  |
+|  |  `- x := 0; x with context 
+|  |
+|  `- ⊥ with context 
+|
+`- <|
+   |
+   +- <|
+   |  |
+   |  +- 1 + x with context x = 0, 
+   |  |
+   |  `- <|
+   |     |
+   |     +- 1 + 0 with context x = 0, 
+   |     |
+   |     `- <|
+   |        |
+   |        +- x with context x = 0, 
+   |        |
+   |        `- <|
+   |           |
+   |           +- 0 with context x = 0, 
+   |           |
+   |           `- <|
+   |              |
+   |              +- 1 with context x = 0, 
+   |              |
+   |              `- ⊥ with context x = 0, 
+   |
+   `- <|
+      |
+      +- x with context x = 0, 
+      |
+      `- <|
+         |
+         +- 0 with context x = 0, 
+         |
+         `- <|
+            |
+            +- 1 with context x = 0, 
+            |
+            `- ⊥ with context x = 0, 
diff --git a/rtree/test/src/Control/Monad/RTreeSpec.hs b/rtree/test/src/Control/Monad/RTreeSpec.hs
new file mode 100644
index 0000000..d3cab50
--- /dev/null
+++ b/rtree/test/src/Control/Monad/RTreeSpec.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Control.Monad.RTreeSpec where
+
+import Control.Monad.Identity (Identity (runIdentity))
+import Control.Monad.RTree
+import Control.Monad.State
+import Control.Monad.Trans.Maybe
+import Data.Foldable
+import Data.Functor
+import qualified Data.Map.Strict as Map
+import Test.Hspec
+import qualified Test.Hspec.Expectations.Pretty as Pretty
+import Test.Hspec.Golden
+
+shouldBeString :: String -> String -> Pretty.Expectation
+shouldBeString = Pretty.shouldBe
+
+golden :: FilePath -> String -> Golden String
+golden fp str =
+  Golden
+    { writeToFile = writeFile
+    , readFromFile = readFile
+    , goldenFile = "test/expected/" ++ fp ++ "/golden"
+    , failFirstTime = False
+    , encodePretty = id
+    , actualFile = Just ("test/expected/" ++ fp ++ "/actual")
+    , output = str
+    }
+
+rBool :: (MonadReduce m) => m Bool
+rBool = split (pure False) (pure True)
+
+rList :: (MonadReduce m) => [a] -> m [a]
+rList = collect (given $>)
+
+data Expr
+  = Var String
+  | Cnt Int
+  | Opr Expr Expr
+  | Let String Expr Expr
+  deriving (Show, Eq)
+
+ex1 :: Expr
+ex1 =
+  Let "x" (Cnt 0) (Opr (Cnt 1) (Var "x"))
+
+rExpr :: (MonadReducePlus m, MonadState (Map.Map String Expr) m) => Expr -> m Expr
+rExpr e = case e of
+  Cnt i -> do
+    given $> Cnt i
+  Var k -> do
+    v <- gets (Map.lookup k)
+    case v of
+      Nothing -> pure e
+      Just x -> rExpr x <| pure e
+  Opr e1 e2 -> onBoth (rExpr e1) (rExpr e2) \e1' e2' ->
+    pure $ Opr e1' e2'
+  Let k e1 e2 ->
+    split
+      do
+        modify' (Map.insert k e1)
+        rExpr e2
+      do
+        e1' <- rExpr e1
+        e2' <- rExpr e2
+        pure $ Let k e1' e2'
+
+prettyExprS :: Int -> Expr -> String -> String
+prettyExprS p = \case
+  Var x -> showString x
+  Opr l r -> prettyExprS p l . showString " + " . prettyExprS p r
+  Cnt i -> showsPrec p i
+  Let x e1 e2 ->
+    showString x
+      . showString " := "
+      . prettyExprS p e1
+      . showString "; "
+      . prettyExprS p e2
+
+spec :: Spec
+spec = do
+  rtreeSpec
+  rtreeTSpec
+
+rtreeTSpec :: Spec
+rtreeTSpec = describe "RTreeT" do
+  describe "equivalence" do
+    it "should extract like RTree" do
+      equiv (rList [1, 2, 3 :: Int]) extract (runIdentity . extractT)
+
+    it "should input like RTree" do
+      equiv (rList [1, 2, 3 :: Int]) inputs (toList :: RTreeT Identity [Int] -> [[Int]])
+
+  describe "rExpr" do
+    let mrExpr = runMaybeT $ rExpr ex1
+    it "should extract expr" do
+      runState (extractT mrExpr) Map.empty
+        `shouldBe` (Just ex1, Map.empty)
+    it "should inputs expr" do
+      golden
+        "rexpr.txt"
+        ( drawRTree
+            ( \(e, m) ->
+                maybe "⊥" (flip (prettyExprS 0) "") e
+                  <> " with context "
+                  <> foldMap
+                    (\(k, v) -> showString k . showString " = " . prettyExprS 0 v . showString ", ")
+                    (Map.toList m)
+                    ""
+            )
+            (flattenT (unStateT mrExpr Map.empty))
+        )
+
+equiv
+  :: (Show b, MonadReduce x, MonadReduce y, Eq b)
+  => (forall m. (MonadReduce m) => m a)
+  -> (x a -> b)
+  -> (y a -> b)
+  -> IO ()
+equiv tree fn1 fn2 =
+  fn1 tree `shouldBe` fn2 tree
+
+rtreeSpec :: Spec
+rtreeSpec = describe "RTree" do
+  describe "extract" do
+    it "should extract rlist" do
+      extract (rList [1, 2, 3]) `shouldBe` [1, 2, 3 :: Int]
+
+    it "should extract rBool" do
+      extract rBool `shouldBe` True
+
+  describe "inputs" do
+    it "should get all inputs from rBool" do
+      inputs rBool `shouldBe` [False, True]
+
+    it "should get all inputs from rList" do
+      inputs (rList [1, 2, 3 :: Int])
+        `shouldBe` [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]
+
+  describe "iinputs" do
+    it "should get all inputs from rList" do
+      iinputs (rList [1, 2, 3 :: Int])
+        `shouldBe` [ ("000", [])
+                   , ("001", [3])
+                   , ("010", [2])
+                   , ("011", [2, 3])
+                   , ("100", [1])
+                   , ("101", [1, 3])
+                   , ("110", [1, 2])
+                   , ("111", [1, 2, 3])
+                   ]
diff --git a/rtree/test/src/Main.hs b/rtree/test/src/Main.hs
new file mode 100644
index 0000000..87de4f4
--- /dev/null
+++ b/rtree/test/src/Main.hs
@@ -0,0 +1,4 @@
+import qualified Spec
+
+main :: IO ()
+main = Spec.main
diff --git a/rtree/test/src/Spec.hs b/rtree/test/src/Spec.hs
new file mode 100644
index 0000000..5416ef6
--- /dev/null
+++ b/rtree/test/src/Spec.hs
@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover -optF --module-name=Spec #-}
-- 
GitLab