{-# LANGUAGE Safe #-}

-- | Read a CNF file without haskell-platform
module SAT.Mios.Util.DIMACS.Reader
       (
         -- * Interface
         fromFile
       , clauseListFromFile
       )
       where
import Control.Applicative ((<$>), (<*>), (<*), (*>))
import Data.Char
import Text.ParserCombinators.ReadP

-- parser
# INLINE newline #
newline :: ReadP Char
newline = char '\n'

# INLINE digit #
digit :: ReadP Char
digit = satisfy isDigit

# INLINE spaces #
spaces :: ReadP String
spaces = munch (`elem` " \t")

# INLINE noneOf #
noneOf :: Foldable t => t Char -> ReadP Char
noneOf s = satisfy (`notElem` s)

-- |parse a non-signed integer
# INLINE pint #
pint :: ReadP Int
pint = do
  n <- munch isDigit
  return (read n :: Int)

# INLINE mint #
mint :: ReadP Int
mint = do
  char '-'
  n <- munch isDigit
  return (- (read n::Int))

-- |parse a (signed) integer
# INLINE int #
int :: ReadP Int
int = mint <++ pint

  |Parse something like : p FORMAT VARIABLES CLAUSES
# INLINE problemLine #
problemLine :: ReadP (Int, Int)
problemLine = do
  char 'p'
  skipSpaces
  (string "cnf" <++ string "CNF")
  skipSpaces
  vars <- pint
  skipSpaces
  clas <- pint
  spaces
  newline
  return (vars, clas)

-- |Parse something like: c This in an example of a comment line.
# INLINE commentLines #
commentLines :: ReadP ()
commentLines = do
  l <- look
  if (head l)  == 'c'
    then do
      munch ('\n' /=)
      newline
      commentLines
    else return ()

_commentLines :: ReadP ()
_commentLines = do
  char 'c'
  munch ('\n' /=)
  newline
  l <- look
  if (head l)  == 'c' then commentLines else return ()

-- |Parse the preamble part
{-# INLINE preambleCNF #-}
preambleCNF :: ReadP (Int, Int)
preambleCNF = do
  commentLines
  problemLine

  |return integer list that terminates at zero
# INLINE seqNums #
seqNums :: ReadP [Int]
seqNums = do
  skipSpaces
  x <- int
  skipSpaces
  if (x == 0) then return []  else (x :) <$> seqNums

  |Parse something like : 1 -2 0 4 0 -3 0
# INLINE parseClauses #
parseClauses :: Int -> ReadP [[Int]]
parseClauses n = count n seqNums

-- |top level interface for parsing CNF
# INLINE parseCNF #
parseCNF :: ReadP ((Int, Int), [[Int]])
parseCNF = do
  a <- preambleCNF
  b <- parseClauses (snd a)
  return (a, b)

-- |driver:: String -> Either ParseError Int
driver :: String -> [([[Int]], String)]
driver input = readP_to_S (parseClauses 1) input

  |read a CNF file and return :
-- ((numbefOfVariables, numberOfClauses), [Literal])
--
-- >>> fromFile "acnf"
  ( ( 3 , 4 ) , [ [ 1 , 2 ] , [ -2 , 3 ] , [ -1 , 2 , -3 ] , [ 3 ] ]
--
# INLINE fromFile #
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))
fromFile f = do
  c <- readFile f
  case readP_to_S parseCNF c of
    [(a, _)] -> return $ Just a
    _ -> return Nothing

-- | return clauses as [[Int]] from 'file'
--
-- >>> clauseListFromFile "a.cnf"
  [ [ 1 , 2 ] , [ -2 , 3 ] , [ -1 , 2 , -3 ] , [ 3 ] ]
--
clauseListFromFile :: FilePath -> IO [[Int]]
clauseListFromFile l = do
  res <- fromFile l
  case res of
    Just (_, l) -> return l
    _ -> return []

# LANGUAGE Safe #
 | Read a CNF file without haskell-platform
 * Interface
 parser
 |parse a non-signed integer
 |parse a (signed) integer
 |Parse something like: c This in an example of a comment line.
 |Parse the preamble part
# INLINE preambleCNF #
 |top level interface for parsing CNF
 |driver:: String -> Either ParseError Int
 ((numbefOfVariables, numberOfClauses), [Literal])

 >>> fromFile "acnf"

 | return clauses as [[Int]] from 'file'

 >>> clauseListFromFile "a.cnf"


module SAT.Mios.Util.DIMACS.Reader
       (
         fromFile
       , clauseListFromFile
       )
       where
import Control.Applicative ((<$>), (<*>), (<*), (*>))
import Data.Char
import Text.ParserCombinators.ReadP

# INLINE newline #
newline :: ReadP Char
newline = char '\n'

# INLINE digit #
digit :: ReadP Char
digit = satisfy isDigit

# INLINE spaces #
spaces :: ReadP String
spaces = munch (`elem` " \t")

# INLINE noneOf #
noneOf :: Foldable t => t Char -> ReadP Char
noneOf s = satisfy (`notElem` s)

# INLINE pint #
pint :: ReadP Int
pint = do
  n <- munch isDigit
  return (read n :: Int)

# INLINE mint #
mint :: ReadP Int
mint = do
  char '-'
  n <- munch isDigit
  return (- (read n::Int))

# INLINE int #
int :: ReadP Int
int = mint <++ pint

  |Parse something like : p FORMAT VARIABLES CLAUSES
# INLINE problemLine #
problemLine :: ReadP (Int, Int)
problemLine = do
  char 'p'
  skipSpaces
  (string "cnf" <++ string "CNF")
  skipSpaces
  vars <- pint
  skipSpaces
  clas <- pint
  spaces
  newline
  return (vars, clas)

# INLINE commentLines #
commentLines :: ReadP ()
commentLines = do
  l <- look
  if (head l)  == 'c'
    then do
      munch ('\n' /=)
      newline
      commentLines
    else return ()

_commentLines :: ReadP ()
_commentLines = do
  char 'c'
  munch ('\n' /=)
  newline
  l <- look
  if (head l)  == 'c' then commentLines else return ()

preambleCNF :: ReadP (Int, Int)
preambleCNF = do
  commentLines
  problemLine

  |return integer list that terminates at zero
# INLINE seqNums #
seqNums :: ReadP [Int]
seqNums = do
  skipSpaces
  x <- int
  skipSpaces
  if (x == 0) then return []  else (x :) <$> seqNums

  |Parse something like : 1 -2 0 4 0 -3 0
# INLINE parseClauses #
parseClauses :: Int -> ReadP [[Int]]
parseClauses n = count n seqNums

# INLINE parseCNF #
parseCNF :: ReadP ((Int, Int), [[Int]])
parseCNF = do
  a <- preambleCNF
  b <- parseClauses (snd a)
  return (a, b)

driver :: String -> [([[Int]], String)]
driver input = readP_to_S (parseClauses 1) input

  |read a CNF file and return :
  ( ( 3 , 4 ) , [ [ 1 , 2 ] , [ -2 , 3 ] , [ -1 , 2 , -3 ] , [ 3 ] ]
# INLINE fromFile #
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))
fromFile f = do
  c <- readFile f
  case readP_to_S parseCNF c of
    [(a, _)] -> return $ Just a
    _ -> return Nothing

  [ [ 1 , 2 ] , [ -2 , 3 ] , [ -1 , 2 , -3 ] , [ 3 ] ]
clauseListFromFile :: FilePath -> IO [[Int]]
clauseListFromFile l = do
  res <- fromFile l
  case res of
    Just (_, l) -> return l
    _ -> return []
