Newer
Older
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
module Control.RTree (
-- # RTree
RTree (..),
extract,
reduce,
-- # IRTree
IRTree,
iextract,
ireduce,
ireduceExp,
IRTreeT (..),
iextractT,
ireduceT,
ireduceExpT,
ReState (..),
-- # Valuation
Valuation,
) where
import qualified Data.Valuation as Val
type Valuation = Val.Valuation
extract :: (Ord l) => Valuation l -> RTree l i -> i
extract v = \case
SplitWith ml lhs rhs -> case ml >>= Val.condition v of
Just v' -> extract v' rhs
_ -> extract v lhs
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 #-}
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
pure (a, ReState as (Val.withTruth v (if a then l else Val.not l)))
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
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@)
-> Valuation l
-> IRTreeT l m i
-> t i
ireduceT lift_ p v (IRTreeT m) = go []
-- 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)
-> 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@)
-> 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
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