addfile ./Control/CP/Herbrand/HerbrandT.hs
hunk ./Control/CP/Herbrand/HerbrandT.hs 1
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+-- |This module provides a Herbrand solver as a monad transformer.
+--
+--  The constraints offered are "Either (Unify t) (Constraint m)"
+--  where "m" is the transformed solver. Hence, both unification
+--  and the underlying solver's constraints are available.
+--
+--  The terms offered are "L t1" where "t1" is the Herbrand solver's
+--  terms and "R t2" where "t2" are the underlying solver's types.
+--  
+module Control.CP.Herbrand.HerbrandT where
+
+import Control.Monad.Trans
+import Control.Monad.State.Lazy
+
+import Control.CP.Solver
+import Control.CP.Herbrand.Herbrand (HState, Unify, HTerm,initState,addH,newvarH)
+
+newtype HerbrandT t m a = HerbrandT { unHT :: StateT (HState t) m a }
+  deriving (MonadTrans, Monad, MonadState (HState t))
+
+instance (Solver s, HTerm t) => Solver (HerbrandT t s) where
+  type Constraint (HerbrandT t s)  = Either (Unify t) (Constraint s)
+  type Label      (HerbrandT t s)  = (HState t, Label s)
+  add (Left  c)  = addH c
+  add (Right c)  = lift $ add c
+  mark           = do l <- get
+                      r <- lift $ mark
+                      return (l,r)
+  goto (l,r)     = put l >> (lift $ goto r)
+  run            = run . flip evalStateT initState . unHT
+
+data L a = L a
+data R a = R a
+
+instance (HTerm t, Solver s) => Term (HerbrandT t s) (L t) where
+  newvar  = newvarH >>= return . L 
+
+instance (HTerm t, Solver s, Term s st) => Term (HerbrandT t s) (R st) where
+  newvar  = lift newvar >>= return . R
hunk ./Control/CP/Herbrand/Herbrand.hs 7
+-- |This module provides a Herbrand solver.
+--
+--  The type of terms is parameterized by the "HTerm" type class.
hunk ./Control/CP/Herbrand/Herbrand.hs 19
--- Herbrand terms
+-- |Herbrand terms
hunk ./Control/CP/Herbrand/Herbrand.hs 28
-        :: (MonadState (HState t) m) => t -> t -> m Bool
+        :: (MonadState (HState t m) m) => t -> t -> m Bool
hunk ./Control/CP/Herbrand/Herbrand.hs 30
--- Herbrand monad
+-- |Herbrand monad
hunk ./Control/CP/Herbrand/Herbrand.hs 32
-newtype Herbrand t a = Herbrand { unH :: State (HState t) a }
-  deriving (Monad, MonadState (HState t))
+data Herbrand t a = Herbrand { unH :: State (HState t (Herbrand t)) a }
+
+instance Monad (Herbrand t) where
+  return x  = Herbrand $ return x
+  m >>=  f  = Herbrand $ unH m >>= unH . f
+
+instance MonadState (HState t (Herbrand t)) (Herbrand t) where
+  get  = Herbrand $ get
+  put  = Herbrand . put
hunk ./Control/CP/Herbrand/Herbrand.hs 45
-
hunk ./Control/CP/Herbrand/Herbrand.hs 51
-type Subst t = Map VarId t
+-- |State
+
+type Heap t m   = Map VarId (Binding t m)
hunk ./Control/CP/Herbrand/Herbrand.hs 55
-data HState t = HState {var_supply :: VarId
-                       ,subst      :: Subst t
-                       }
+data Binding t m 
+  = VAR VarId 		-- | indirection to other variable
+  | NONVAR t 		-- | bound to term
+  | ACTION (m Bool)	-- | attributed variable, with given action
hunk ./Control/CP/Herbrand/Herbrand.hs 60
-updateState :: (HTerm t, MonadState (HState t) m) => (HState t -> HState t) -> m ()
+data HState t m = HState {var_supply :: VarId
+                         ,heap       :: Heap t m
+                         }
+
+updateState :: (HTerm t, MonadState (HState t m) m) => (HState t m -> HState t m) -> m ()
hunk ./Control/CP/Herbrand/Herbrand.hs 67
--- Solver instance 
+-- |Solver instance 
hunk ./Control/CP/Herbrand/Herbrand.hs 71
-  type Label      (Herbrand t)  = HState t
+  type Label      (Herbrand t)  = HState t (Herbrand t)
hunk ./Control/CP/Herbrand/Herbrand.hs 85
-newvarH :: (HTerm t,MonadState (HState t) m) => m t
+newvarH :: (HTerm t,MonadState (HState t m) m) => m t
hunk ./Control/CP/Herbrand/Herbrand.hs 91
+{- Representatin of variables
+   --------------------------
+
+   Each variable is represented by
+   * a VarId
+   * a possible Binding on the Heap
+       - if there is a binding, then the variable's meaning 
+         is that of the binding
+       - if there is no binding, then variable's meaning is 
+         that of an unbound variable
+
+-}
+
hunk ./Control/CP/Herbrand/Herbrand.hs 108
-addH :: (HTerm t, MonadState (HState t) m) => Unify t -> m Bool
+addH :: (HTerm t, MonadState (HState t m) m) => Unify t -> m Bool
hunk ./Control/CP/Herbrand/Herbrand.hs 111
-unify :: (HTerm t, MonadState (HState t) m) => t -> t -> m Bool
+-- | unify two arbitrary terms
+unify :: (HTerm t, MonadState (HState t m) m) => t -> t -> m Bool
hunk ./Control/CP/Herbrand/Herbrand.hs 119
-       (Just v1, _      ) -> bind v1 nt2 >> success
-       (_      , Just v2) -> bind v2 nt1 >> success
-       (_      , _      ) -> nonvar_unify nt1 nt2
+	  | otherwise     -> bindv v1 v2
+       (Just v1, Nothing) -> bindt v1 nt2
+       (Nothing, Just v2) -> bindt v2 nt1
+       (Nothing, Nothing) -> nonvar_unify nt1 nt2
hunk ./Control/CP/Herbrand/Herbrand.hs 127
+m1 `andM` m2  = m1 >>= \b -> if b then m2 else return b 
hunk ./Control/CP/Herbrand/Herbrand.hs 129
-bind :: (HTerm t, MonadState (HState t) m) => VarId -> t -> m ()
-bind v t  = updateState $ \state -> state{subst = insert v t (subst state)}
+-- | bind a variable to a term
+bindt :: (HTerm t, MonadState (HState t m) m) => VarId -> t -> m Bool
+bindt v t  = do r <- lookupVar v
+                updater v (NONVAR t)
+                case r of
+		  Just (ACTION action) -> action
+                  Nothing              -> success
+
+-- | alias one variable to another
+bindv :: (HTerm t, MonadState (HState t m) m) => VarId -> VarId -> m Bool
+bindv v1 v2  = do r1 <- lookupVar v1
+                  r2 <- lookupVar v2
+                  case (r1,r2) of
+                    (Just (ACTION a1), Just (ACTION a2)) 
+				      -> let r3 = noACTION
+                                         in do updater v1 r3
+                                               updater v2 r3
+				               a1 `andM` a2
+                    (Just _, Nothing) -> updater v1 (VAR v2) >> success
+                    (Nothing, Just _) -> updater v2 (VAR v1) >> success
+                    (Nothing,Nothing) -> updater v1 (VAR v2) >> success
+
+             where noACTION = ACTION success
+
+updater v  r  = updateState $ \state -> state{heap = insert v r (heap state)}
+
+lookupVar v  = do state <- get
+                  return $ Data.Map.lookup v (heap state)
+
+-- Actions
+
+registerAction :: (HTerm t, MonadState (HState t m) m) => t -> m Bool -> m ()
+registerAction t action  =
+  do nt <- shallow_normalize t
+     case isVar nt of
+       Just v  ->
+         do r <- lookupVar v
+            case r of
+              Nothing          -> updater v (ACTION action)
+              Just (ACTION a1) -> updater v (ACTION (a1 `andM` action))
+       Nothing -> return ()
+
+-- TODO: unregister action?
hunk ./Control/CP/Herbrand/Herbrand.hs 175
-shallow_normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
-shallow_normalize t
-  | Just v <- isVar t    
-     = do state <- get
-          case Data.Map.lookup v (subst state) of
-            Just t' -> shallow_normalize t'
-            Nothing -> return t 
-  | otherwise  
-     = return t
+shallow_normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t
+shallow_normalize t  = gnormalize return t
+
+normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t
+normalize t          = gnormalize nvnormalize t
+  where nvnormalize t  =  let (ts,mkt)  = children t
+                          in mapM normalize ts >>= return . mkt
hunk ./Control/CP/Herbrand/Herbrand.hs 183
-normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
-normalize t
-  | Just v <- isVar t  = do state <- get
-                            case Data.Map.lookup v (subst state) of
-                              Just t' -> normalize t'
-                              Nothing -> return t
-  | otherwise          = let (ts,mkt)  = children t
-                         in mapM normalize ts >>= return . mkt
+gnormalize nvnormalize t
+  | Just v <- isVar t  = vnormalize v
+  | otherwise          = nvnormalize t
+  where vnormalize v   = do state <- get
+                            case Data.Map.lookup v (heap state) of
+                              Just (VAR v')   -> vnormalize v'
+                              Just (NONVAR t) -> nvnormalize t
+                              _               -> return $ mkVar v
hunk ./Control/CP/Herbrand/PrologTerm.hs 1
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
hunk ./Control/CP/Herbrand/PrologTerm.hs 9
+
hunk ./Control/CP/Herbrand/PrologTerm.hs 13
+     deriving Eq
hunk ./Control/CP/Herbrand/PrologTerm.hs 35
-
hunk ./Control/CP/SearchTree.hs 125
+-------------------------------------------------------------------------------
+----------------------------------- 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
+
hunk ./Control/CP/SearchTree.hs 152
-(/\) :: Solver s => Tree s a -> Tree s b -> Tree s b
+(/\) :: MonadTree tree => tree a -> tree b -> tree b
hunk ./Control/CP/SearchTree.hs 155
-infixl 2 \/
-(\/) :: Solver s => Tree s a -> Tree s a -> Tree s a
-(\/) = Try
-
-false :: Tree s a
-false = Fail
- 
-true :: Tree s ()
-true = Return ()
+true :: MonadTree tree  => tree ()
+true = return ()
hunk ./Control/CP/SearchTree.hs 158
-disj :: Solver s => [Tree s a] -> Tree s a
+disj :: MonadTree tree => [tree a] -> tree a
hunk ./Control/CP/SearchTree.hs 161
-conj :: Solver s => [Tree s ()] -> Tree s ()
+conj :: MonadTree tree => [tree ()] -> tree ()
hunk ./Control/CP/SearchTree.hs 172
-exists :: Term s t => (t -> Tree s a) -> Tree s a
-exists f = NewVar f
-
-exist :: (Solver s, Term s t) => Int -> ([t] -> Tree s a) -> Tree s a
+exist :: (MonadTree tree, Term (TreeSolver tree) t) => Int -> ([t] -> tree a) -> tree a
hunk ./Control/CP/SearchTree.hs 180
-label :: Solver s => s (Tree s a) -> Tree s a
-label = Label
-
-prim :: Solver s => (s a) -> Tree s a
-prim action = Label (action >>= return . return)
+prim :: MonadTree tree => TreeSolver tree a -> tree a
+prim action = label (action >>= return . return)
hunk ./Control/CP/SearchTree.hs 183
-add :: Solver s => Constraint s -> Tree s ()
-add c = Add c true
+add :: MonadTree tree => Constraint (TreeSolver tree) -> tree ()
+add c = c `addTo` true
hunk ./Control/CP/Solver.hs 11
+import Control.Monad.Writer
+import Data.Monoid
+
hunk ./Control/CP/Solver.hs 15
-	-- the constraints
+	-- | the constraints
hunk ./Control/CP/Solver.hs 17
- 	-- the labels
+ 	-- | the labels
hunk ./Control/CP/Solver.hs 19
-	-- add a constraint to the current state, and
-	-- return whethe the resulting state is consistent
+	-- | add a constraint to the current state, and
+	--   return whethe the resulting state is consistent
hunk ./Control/CP/Solver.hs 22
-	-- run a computation
+	-- | run a computation
hunk ./Control/CP/Solver.hs 24
-	-- mark the current state, and return its label
+	-- | mark the current state, and return its label
hunk ./Control/CP/Solver.hs 26
-	-- go to the state with given label
+	-- | go to the state with given label
hunk ./Control/CP/Solver.hs 30
-	-- produce a fresh constraint variable
+	-- | produce a fresh constraint variable
hunk ./Control/CP/Solver.hs 33
+-- | WriterT decoration of a solver
+--   useful for producing statistics during solving
+instance (Monoid w, Solver s) => Solver (WriterT w s) where
+  type Constraint (WriterT w s)  = Constraint s
+  type Label (WriterT w s)       = Label s
+  add  = lift . add
+  run  = fst . run . runWriterT
+  mark = lift mark
+  goto = lift . goto 
hunk ./Control/CP/Solver.hs 43
+instance (Monoid w, Term s t) => Term (WriterT w s) t where
+  newvar  = lift newvar
hunk ./monadiccp.cabal 10
-Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.HerbrandT
+Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog
hunk ./monadiccp.cabal 13
-Synopsis:	     Package for Constraint Programming
+Synopsis:	     Constraint Programming
hunk ./monadiccp.cabal 15
+bug-reports:         http://trac.haskell.org/monadiccp/
hunk ./Control/CP/Herbrand/HerbrandT.hs 4
+{-# LANGUAGE FlexibleInstances #-}
hunk ./Control/CP/Herbrand/HerbrandT.hs 23
-newtype HerbrandT t m a = HerbrandT { unHT :: StateT (HState t) m a }
-  deriving (MonadTrans, Monad, MonadState (HState t))
+newtype HerbrandT t s a = HerbrandT { unHT :: StateT (HState t (HerbrandT t s)) s a }
+  deriving Monad
+
+instance MonadTrans (HerbrandT t) where
+  lift = HerbrandT . lift
+
+instance Solver s =>MonadState (HState t (HerbrandT t s)) (HerbrandT t s)  where
+  get = HerbrandT get
+  put = HerbrandT . put
hunk ./Control/CP/Herbrand/HerbrandT.hs 35
-  type Label      (HerbrandT t s)  = (HState t, Label s)
+  type Label      (HerbrandT t s)  = (HState t (HerbrandT t s), Label s)
hunk ./monadiccp.cabal 10
-Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog
+Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog Control.CP.Herbrand.HerbrandT