{-
 - 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 _ _ = ()