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 Control.Monad.Reduce
import Control.Monad.State.Strict
type Valuation l = Map.Map l Bool
extract :: (Ord l) => Valuation l -> RTree l i -> i
extract v = \case
SplitWith ml lhs rhs -> case ml >>= (`Map.lookup` v) of
Just False -> extract v lhs
_ -> extract v rhs
Done i -> i
Just True -> checkgo v rhs
Just False -> checkgo v lhs
Nothing -> checkgo (Map.insert l False v) lhs <|> go (Map.insert l True v) rhs
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
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
ReState as v@(Map.lookup l -> Just x) ->
pure (x, ReState as v)
ReState (uncons -> (a, as)) v ->
pure (a, ReState as (Map.insert l a v))
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@)
-> (i -> t Bool)
-> Valuation l
-> IRTreeT l m i
-> t i
ireduceT lift_ p v (IRTreeT m) = go []
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
lift_ (runStateT m (ReState pth v)) >>= \case
(i, ReState [] _) -> do
t <- p i
-- 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)
=> (i -> m Bool)
-> 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@)
-> (i -> t Bool)
-> 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
(i, ReState [] _) -> do
p i >>= \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