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 s a = HerbrandT { unHT :: StateT (HState t (HerbrandT t s)) s a }
instance Monad s => Monad (HerbrandT t s) where
return = HerbrandT . return
m >>= f = HerbrandT $ unHT m >>= unHT . f
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
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 (HerbrandT t s), 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
type Help (HerbrandT t s) (L t) = ()
help _ _ = ()
instance (HTerm t, Solver s, Term s st) => Term (HerbrandT t s) (R st) where
newvar = lift newvar >>= return . R
type Help (HerbrandT t s) (R st) = ()
help _ _ = ()