monadiccp-0.5.1: Control/CP/SearchTree.hs
{-# OPTIONS_GHC -fglasgow-exts #-}
{-
- The Tree data type, a generic modelling language for constraint solvers.
-
- Monadic Constraint Programming
- http://www.cs.kuleuven.be/~toms/Haskell/
- Tom Schrijvers
-}
module Control.CP.SearchTree where
import Monad
import Control.CP.Solver
-------------------------------------------------------------------------------
----------------------------------- Tree --------------------------------------
-------------------------------------------------------------------------------
data Tree s a where
Fail :: Tree s a -- failure
Return :: a -> Tree s a -- finished
Try :: Tree s a -> Tree s a -> Tree s a -- disjunction
Add :: Constraint s -> Tree s a -> Tree s a -- sequentially adding a constraint to a tree
NewVar :: Term s t => (t -> Tree s a) -> Tree s a -- add a new variable to a tree
Label :: s (Tree s a) -> Tree s a -- label with a strategy
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"
show (Label _) = "Label"
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
{- Monad laws:
-
- 1. return x >>= f == f x
-
- return a >>= f
- == Return a >>= f (return def)
- == f x (bind def)
-
- 2. m >>= return = m
-
- By induction
- case m of
- 1) Return x ->
- Return x >>= return
- == return x (bind def)
- == Return x (return def)
- 2) Fail ->
- Fail >>= return
- == Fail (bind def)
- 3) Try l r >>= return
- == Try (l >>= return) (r >>= return) (bind def)
- == Try l r (induction)
- 4) Add c m >>= return
- == Add c (m >>= return) (bind def)
- == Add c m (induction)
- 5) NewVar f >>= return
- == NewVar (\v -> f v >>= return) (bind def)
- == NewVar (\v -> f v) ((co)-induction?)
- == NewVar f (eta reduction)
- 6) Label sm >>= return
- == Label (sm >>= \m -> return (m >>= return)) (bind def)
- == Label (sm >>= \m -> return m) (co-induction)
- == Label (sm >>= return) (eta reduction)
- == Label sm (2nd monad law for Monad s)
-
- 3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)
-
- By induction
- case m of
- 1) (Return y >>= f) >>= g
- == f y >>= g (bind def)
- == (\x -> f x >>= g) y (beta expansion)
- == Return y >>= (\x -> f x >>= g) (bind def)
- 2) (Fail >>= f) >>= g
- == Fail >>= g (bind def)
- == Fail (bind def)
- == Fail >>= (\x -> f x >>= g) (bind def)
- 3) (Try l r >>= f) >>= g
- == Try (l >>= f) (r >>= f)) >>= g (bind def)
- == Try ((l >>= f) >>= g) ((r >>= f) >>= g) (bind def)
- == Try (l >>= (\x -> f x >>= g)) (r >>= (\x -> f x >>= g)) (induction)
- == Try l r >>= (\x -> f x >>= g) (bind def)
- 4) (NewVar m >>= f) >>= g
- == NewVar (\v -> m v >>= f) >>= g (bind def)
- == NewVar (\w -> (\v -> m v >>= f) w >>= g) (bind def)
- == NewVar (\w -> (m w >>= f) >>= g) (beta reduction)
- == NewVar (\w -> m w >>= (\x -> f x >>= g)) (co-induction)
- == NewVar m >>= (\x -> f x >>= g) (bind def)
- 5) (Label sm >>= f) >>= g
- == Label (sm >>= \m -> return (m >>= f)) >>= g (bind def)
- == Label ((sm >>= \m -> return (m >>= f)) >>= \m' -> return (m' >>= g))
- == Label (sm >>= (\m -> return (m >>= f) >>= \m' -> return (m' >>= g)))
- == Label (sm >>= \m -> return ((m >>= f) >>= g))
- == Label (sm >>= \m -> return (m >>= (\x -> f x >>= g)))
- == Label sm >>= (\x -> f x >>= g)
-
-}
-------------------------------------------------------------------------------
----------------------------------- Monad Subclass ----------------------------
-------------------------------------------------------------------------------
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
-------------------------------------------------------------------------------
----------------------------------- Sugar -------------------------------------
-------------------------------------------------------------------------------
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 (n-1) (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