content: {- | Module     : ./GMP/Parser.hs
   -  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 ()
  