module Control.CP.SearchTree where
import Control.CP.Solver
import Control.Monad
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State
import Data.Monoid
data Tree s a where
Fail :: Tree s a
Return :: a -> Tree s a
Try :: Tree s a -> Tree s a -> Tree s a
Add :: Constraint s -> Tree s a -> Tree s a
NewVar :: Term s t => (t -> Tree s a) -> Tree s a
Label :: s (Tree s a) -> Tree s a
instance Show (Tree s a) where
show Fail = "Fail"
show (Return _) = "Return"
show (Try l r) = "Try (" ++ show l ++ ") (" ++ show r ++ ")"
show (Add _ t) = "Add (" ++ show t ++ ")"
show (NewVar _) = "NewVar <function>"
show (Label _) = "Label <monadic value>"
instance Solver s => Functor (Tree s) where
fmap = liftM
instance Solver s => Monad (Tree s) where
return = Return
(>>=) = bindTree
bindTree :: Solver s => Tree s a -> (a -> Tree s b) -> Tree s b
Fail `bindTree` k = Fail
(Return x) `bindTree` k = k x
(Try m n) `bindTree` k = Try (m `bindTree` k) (n `bindTree` k)
(Add c m) `bindTree` k = Add c (m `bindTree` k)
(NewVar f) `bindTree` k = NewVar (\x -> f x `bindTree` k)
(Label m) `bindTree` k = Label (m >>= \t -> return (t `bindTree` k))
insertTree :: Solver s => Tree s a -> Tree s () -> Tree s a
(NewVar f) `insertTree` t = NewVar (\x -> f x `insertTree` t)
(Add c o) `insertTree` t = Add c (o `insertTree` t)
other `insertTree` t = t /\ other
infixl 2 \/
class (Monad m, Solver (TreeSolver m)) => MonadTree m where
type TreeSolver m :: * -> *
addTo :: Constraint (TreeSolver m) -> m a -> m a
false :: m a
(\/) :: m a -> m a -> m a
exists :: Term (TreeSolver m) t => (t -> m a) -> m a
label :: (TreeSolver m) (m a) -> m a
instance Solver solver => MonadTree (Tree solver) where
type TreeSolver (Tree solver) = solver
addTo = Add
false = Fail
(\/) = Try
exists = NewVar
label = Label
infixr 3 /\
(/\) :: MonadTree tree => tree a -> tree b -> tree b
(/\) = (>>)
true :: MonadTree tree => tree ()
true = return ()
disj :: MonadTree tree => [tree a] -> tree a
disj = foldr (\/) false
conj :: MonadTree tree => [tree ()] -> tree ()
conj = foldr (/\) true
disj2 :: Solver s => [Tree s a] -> Tree s a
disj2 (x: []) = x
disj2 l = let (xs,ys) = split l
split [] = ([],[])
split (a:as) = let (bs,cs) = split as
in (a:cs,bs)
in Try (disj2 xs) (disj2 ys)
exist :: (MonadTree tree, Term (TreeSolver tree) t) => Int -> ([t] -> tree a) -> tree a
exist n ftree = f n []
where f 0 acc = ftree acc
f n acc = exists $ \v -> f (n1) (v:acc)
forall :: (Solver s, Term s t) => [t] -> (t -> Tree s ()) -> Tree s ()
forall list ftree = conj $ map ftree list
prim :: MonadTree tree => TreeSolver tree a -> tree a
prim action = label (action >>= return . return)
add :: MonadTree tree => Constraint (TreeSolver tree) -> tree ()
add c = c `addTo` true
instance MonadTree t => MonadTree (ReaderT env t) where
type TreeSolver (ReaderT env t) = TreeSolver t
addTo constraint tree = ReaderT $ \env -> addTo constraint (runReaderT tree env)
false = lift false
l \/ r = ReaderT $ \env -> runReaderT l env \/ runReaderT r env
exists f = ReaderT $ \env -> exists (\var -> runReaderT (f var) env)
label p = ReaderT $ \env -> label (p >>= \m -> return $ runReaderT m env)
instance (Monoid w, MonadTree t) => MonadTree (WriterT w t) where
type TreeSolver (WriterT w t) = TreeSolver t
addTo constraint tree = WriterT $ addTo constraint (runWriterT tree)
false = lift false
l \/ r = WriterT $ runWriterT l \/ runWriterT r
exists f = WriterT $ exists (\var -> runWriterT (f var))
label p = WriterT $ label (p >>= \m -> return $ runWriterT m)
instance MonadTree t => MonadTree (StateT s t) where
type TreeSolver (StateT s t) = TreeSolver t
addTo constraint tree = StateT $ \s -> addTo constraint (runStateT tree s)
false = lift false
l \/ r = StateT $ \s -> runStateT l s \/ runStateT r s
exists f = StateT $ \s -> exists (\var -> runStateT (f var) s)
label p = StateT $ \s -> label (p >>= \m -> return $ runStateT m s)