{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}


#if (__GLASGOW_HASKELL__ >= 708)
{-# LANGUAGE AllowAmbiguousTypes #-}
#endif

module Satchmo.MonadSAT

( MonadSAT(..), Weight
, Header (..)                
)

where

import Satchmo.Data
import Satchmo.Code

import Control.Applicative
import Control.Monad.Trans (lift)
import Control.Monad.Cont  (ContT)
import Control.Monad.List  (ListT)
import Control.Monad.Reader (ReaderT)
import Control.Monad.Fix ( MonadFix )
import qualified Control.Monad.State  as Lazy (StateT)
import qualified Control.Monad.Writer as Lazy (WriterT)
import qualified Control.Monad.RWS    as Lazy (RWST)
import qualified Control.Monad.State.Strict  as Strict (StateT)
import qualified Control.Monad.Writer.Strict as Strict (WriterT)
import qualified Control.Monad.RWS.Strict    as Strict (RWST)
import Data.Monoid

type Weight = Int

class ( -- MonadFix m,
        Applicative m, Monad m) => MonadSAT m where
  fresh, fresh_forall :: m  Literal

  emit  :: Clause  -> m ()
  -- emitW :: Weight -> Clause (Literal m) -> m ()

  -- | emit some note (could be printed by the backend)
  note :: String -> m ()

  type Decoder m :: * -> * 
  decode_variable :: Variable -> Decoder m Bool


type NumClauses = Integer
type NumVars    = Integer

data Header = 
     Header { Header -> Int
numClauses, Header -> Int
numVars :: !Int
            , Header -> [Int]
universals :: ![Int]
                     }
     deriving Int -> Header -> ShowS
[Header] -> ShowS
Header -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Header] -> ShowS
$cshowList :: [Header] -> ShowS
show :: Header -> String
$cshow :: Header -> String
showsPrec :: Int -> Header -> ShowS
$cshowsPrec :: Int -> Header -> ShowS
Show

-- -------------------------------------------------------
-- MonadSAT liftings for standard monad transformers
-- -------------------------------------------------------

instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where
  fresh :: ListT m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: ListT m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> ListT m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> ListT m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where
  fresh :: ReaderT r m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: ReaderT r m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> ReaderT r m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> ReaderT r m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where
  fresh :: StateT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: StateT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> StateT s m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> StateT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where
  fresh :: RWST r w s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: RWST r w s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> RWST r w s m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> RWST r w s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where
  fresh :: WriterT w m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: WriterT w m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> WriterT w m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> WriterT w m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where
  fresh :: StateT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: StateT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> StateT s m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> StateT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where
  fresh :: RWST r w s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: RWST r w s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> RWST r w s m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> RWST r w s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where
  fresh :: WriterT w m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: WriterT w m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> WriterT w m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> WriterT w m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note

instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where
  fresh :: ContT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
  fresh_forall :: ContT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
  emit :: Clause -> ContT s m ()
emit  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
  -- emitW = (lift.) . emitW
  note :: String -> ContT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note