{- - The Solver class, a generic interface for constraint solvers. - - Monadic Constraint Programming - http://www.cs.kuleuven.be/~toms/Haskell/ - Tom Schrijvers -} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} module Control.CP.Solver ( Solver, Constraint, Label, add, run, mark, markn, goto, Term, newvar, Help, help, ) where import Control.Monad.Writer import Data.Monoid class Monad solver => Solver solver where -- | the constraints type Constraint solver :: * -- | the labels type Label solver :: * -- | add a constraint to the current state, and -- return whether the resulting state is consistent add :: Constraint solver -> solver Bool -- | run a computation run :: solver a -> a -- | mark the current state, and return its label mark :: solver (Label solver) -- | mark the current state as discontinued, yet return a label that is usable n times markn :: Int -> solver (Label solver) -- | go to the state with given label goto :: Label solver -> solver () markn _ = mark class (Solver solver) => Term solver term where -- | produce a fresh constraint variable newvar :: solver term -- see note [Solver-Specific Term Operations] type Help solver term help :: solver () -> term -> Help solver term -- [Solver-Specific Term Operations] -- -- Terms of solvers in general only support the 'newvar' operation. -- However, for specific solvers, all terms may support additional -- operations. -- -- The 'Help'/'help' infrastructure allows accessing this solver-specific -- term operations. -- | 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 markn = lift . markn goto = lift . goto instance (Monoid w, Term s t) => Term (WriterT w s) t where newvar = lift newvar type Help (WriterT w s) t = () help _ _ = ()