{- | Module     : $Header$
 -  Description : Implementation of logic formula parser
 -  Copyright   : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
 -  License     : GPLv2 or higher, see LICENSE.txt
 -  Maintainer  : g.calin@jacobs-university.de
 -  Stability   : provisional
 -  Portability : portable
 -
 -  Provides the implementation of the generic parser for the Boole datatype
 -}
module Parser where

import Text.ParserCombinators.Parsec

-- import GenericSequent
import ModalLogic
import CombLogic

data ModalOperator = Sqr | Ang | None deriving Eq

{- | Main parser
par5er :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
par5er = implFormula

{- | Parser which translates all implications in disjunctions & conjunctions
implFormula :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
implFormula flag logics = do
    f <- orFormula flag logics
    option f (do string "->"
                 spaces
                 i <- implFormula flag logics
                 return $ Not (And f (Not i))
          <|> do try (string "<->")
                 spaces
                 i <- implFormula flag logics
                 return $ And (Not (And f (Not i))) (Not (And (Not f) i))
          <|> do string "<-"
                 spaces
                 i <- implFormula flag logics
                 return $ And (Not f) i
          <|> return f
          <?> "GMPParser.implFormula")

{- | Parser for disjunction - used for handling binding order
orFormula :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
orFormula flag logics = do
    f <- andFormula flag logics
    option f $ do
      string "\\/"
      spaces
      g <- orFormula flag logics
      return $ Not (And (Not f) (Not g))
  <?> "GMPParser.orFormula"

{- | Parser for conjunction - used for handling the binding order
andFormula :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
andFormula flag logics = do
    f <- primFormula flag logics
    option f $ do
      string "/\\"
      spaces
      g <- andFormula flag logics
      return $ And f g
  <?> "GMPParser.andFormula"


{- | Parse a primitive formula: T, F, ~f, <i>f, [i]f,
 -   where i stands for an index, f for a formula/boolean expression
primFormula :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
primFormula flag logics =  do string "T"
                              spaces
                              return T
                       <|> do string "F"
                              spaces
                              return F
                       <|> parenFormula flag logics
                       <|> do string "~"
                              spaces
                              f <- primFormula flag logics
                              return $ Not f
                       <|> atomFormula flag logics
                       <?> "GMPParser.primFormula"


-- modalAtom :: ModalOperator -> [Int] -> GenParser Char st (Boole a)
atomFormula flag logics =  do char '<'
                              spaces
                              let h = head logics
                              let t = tail logics
                              case h of
                                1 -> do parseKindex
                                        spaces
                                        char '>'
                                        spaces
                                        f <- primFormula flag $ t ++ [h]
                                        case flag of
                                          -- FIXME: cannot construct the infinite type
                                          Ang -> return $ At (K f) -- M i f
                                          Sqr -> return $ Not (At (K (Not f)))
                                          _ -> return $ At (K f)
{-
                                2 -> do parseKDindex
                                        spaces
                                        char '>'
                                        spaces
                                        f <- primFormula flag $ t ++ [h]
                                        case flag of
                                          Ang -> return $ At (KD f)--M i f
                                          Sqr -> return $ Not (At (KD (Not f)))
                                          _   -> return $ At (KD f)
                                _ -> do aux <- parseGindex
                                        return aux
                       <|> do char '['
                              spaces
                              i <- head pa
                              spaces
                              char ']'
                              spaces
                              f <- primFormula flag $ tail pa ++ [head pa]
                              case flag of
                                Ang -> return $ Not (At (Not (Box i f)))
                                Sqr -> return $ At (Box i f)
                                _   -> return $ At (Box i f)
-}

{- | Parser for un-parenthesizing a formula
parenFormula :: ModalOperator -> [GenParser Char st a] -> GenParser Char st (Boole a) -}
parenFormula flag logics = do char '('
                              spaces
                              f <- par5er flag logics
                              spaces
                              char ')'
                              spaces
                              return f
                        <?> "GMPParser.parenFormula"


-- | Parse integer number
natural :: GenParser Char st Integer
natural = fmap read $ many1 digit

-- | Parser for Coalition Logic index
parseCindex :: Parser [Int]
parseCindex = do -- checks whether there are more numbers to be parsed
                  let stopParser =  do char ','
                                       return False
                                <|> do char '}'
                                       return True
                                <?> "Parser.parseCindex.stop"
                  -- checks whether the index is of the for x1,..,x&
                  let normalParser l =  do x <- natural
                                           let n = fromInteger x
                                           spaces
                                           q <- stopParser
                                           spaces
                                           if q then normalParser (n : l)
                                           else return (n : l)
                                    <?> "Parser.parseCindex.normal"
                  char '{'
                  try (normalParser [])
           <|> do -- checks whether the index is of the form "n..m"
                  let shortParser =  do x <- natural
                                        let n = fromInteger x
                                        spaces
                                        string ".."
                                        spaces
                                        y <- natural
                                        let m = fromInteger y
                                        return [n .. m]
                                 <?> "Parser.parseCindex.short"
                  try shortParser
           <?> "Parser.parseCindex"

-- | Parser for Graded Modal Logic index
parseGindex :: Parser Int
parseGindex =  do n <- natural
                  return $ fromInteger n
           <?> "Parser.parseGindex"

-- | Parser for Hennesy-Milner Modal Logic index
parseHMindex :: Parser Char
parseHMindex = letter
            <?> "Parser.parseHMindex"

-- | Parser for K Modal Logic index
parseKindex :: Parser ()
parseKindex = return ()

-- | Parser for KD Modal Logic index
parseKDindex :: Parser ()
parseKDindex = return ()

-- | Parser for Probability Logic index
parsePindex :: Parser Rational
parsePindex =
    do x <- natural
       let auxP n =  do char '/'
                        m <- natural
                        return $ toRational (fromInteger n / fromInteger m)
                 <|> do char '.'
                        m <- natural
                        let noDig n = let tmp = n < 10
                                      in if tmp then 1
                                         else 1 + noDig (div n 10)
                        let rat n = toRational (fromInteger n /
                                               fromInteger (10 ^ noDig n))
                        let res = toRational n + rat m
                        return res
                 <|> return (toRational n)
                 <?> "Parser.parsePindex.auxP"
       auxP x

-- | Parser for Monotonic Modal Logic index
parseMindex :: Parser ()
parseMindex = return ()
