content: {- | Module     : ./GMP/GMP-CoLoSS/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 L formula datatype
   -}
  
  module GMP.Parser where
  import Text.ParserCombinators.Parsec
  
  import GMP.Logics.Generic
  
  -- import Debug.Trace
  
  {- ----------------------------------
  experiment 2 starting here:
  ---------------------------------- -}
  
  {- class (SigFeature a b (c d), SigFeature b c (e f)) => MyFeat a b c d e f where
  yoyo :: (a (b (c d))) -> (b (c (e f)))
  pGoOn3 :: (a (b (c d))) -> ModalOperator ->  GenParser Char st (Formula (b (c (e f)))) -}
  
  {- instance MyFeat K K K () K () where
  yoyo sig = K [Mod (K [Mod (K [])])]
  pGoOn3 sig flag = primFormula (yoyo sig) flag -}
  
  {- instance MyFeat KD KD KD () KD () where
  yoyo sig = KD [Mod (KD [Mod (KD [])])]
  pGoOn3 sig flag = primFormula (yoyo sig) flag -}
  
  {- instance MyFeat K KD K () KD () where
  yoyo sig = KD [Mod (K [Mod (KD [])])]
  pGoOn3 sig flag = primFormula (yoyo sig) flag -}
  
  {- instance MyFeat KD K KD () K () where
  yoyo sig = K [Mod (KD [Mod (K [])])]
  pGoOn3 sig flag = primFormula (yoyo sig) flag -}
  
  {- ----------------------------------
  experiment 1 starting here:
  ---------------------------------- -}
  
  {- class SigFeature a b c => ParseMe a b c where
  pGive :: (a (b c)) -> (b c)
  pGoOn2 :: (a (b c)) -> ModalOperator ->  GenParser Char st (Formula (b c)) -}
  
  {- instance (SigFeature K K (K d), ParseMe K K d) => ParseMe K K (K d) where
  pGive = genericPGive
  pGoOn2 = genericPGoOn2 -}
  
  {- instance SigFeature K K () => ParseMe K K () where
  pGive sig = trace ("finishing: " ++ sPretty sig) $ K []
  pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
  
  {- instance (SigFeature KD KD (KD d), ParseMe KD KD d) => ParseMe KD KD (KD d) where
  pGive = genericPGive
  pGoOn2 = genericPGoOn2 -}
  
  {- instance SigFeature KD KD () => ParseMe KD KD () where
  pGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
  pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
  
  {- instance (SigFeature KD K (KD d), ParseMe K KD d) => ParseMe KD K (KD d) where
  pGive = genericPGive
  pGoOn2 = genericPGoOn2 -}
  
  {- instance SigFeature K KD () => ParseMe K KD () where
  pGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
  pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
  
  {- instance (SigFeature K KD (K d), ParseMe KD K d) => ParseMe K KD (K d) where
  pGive = genericPGive
  pGoOn2 = genericPGoOn2 -}
  
  {- instance SigFeature KD K () => ParseMe KD K () where
  pGive sig = trace ("finishing: " ++ sPretty sig) $ K []
  pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
  
  {- genericPGive :: (SigFeature a b (c d), SigFeature b c d, ParseMe a b (c d), ParseMe b c d) => (a (b (c d))) -> (b (c d))
  genericPGive sig = ((sSecondFeat sig) [Mod ((sSecondFeat (sNextSig sig)) [])]) -}
  
  {- genericPGoOn2 :: (SigFeature a b (c d), SigFeature b c d, ParseMe a b (c d), ParseMe b c d) => (a (b (c d))) -> ModalOperator ->  GenParser Char st (Formula (b (c d)))
  genericPGoOn2 sig flag = return T
  genericPGoOn2 sig flag = primFormula (pGive sig) flag -}
  
  -- generic parsing stuff
  genericPGoOn :: (SigFeature a b (c d), SigFeature b c d) =>
                  a (b (c d)) -> ModalOperator -> Parser (Formula (b (c d)))
  genericPGoOn sig = primFormula (sNextSig sig)
  
  -- parser:
  
  -- Normalised negation.
  nneg :: Formula (a b) -> Formula (a b)
  nneg F = T
  nneg T = F
  nneg (Neg phi) = phi
  nneg phi = Neg phi
  
  -- | Main parser
  parser :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                  Parser (Formula (a (b c)) )
  parser = implFormula
  
  -- | Parser which translates all implications in disjunctions & conjunctions
  implFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                       Parser (Formula (a (b c)) )
  implFormula sig flag = do
      f <- orFormula sig flag
      option f (do string "->"
                   spaces
                   i <- implFormula sig flag
                   return $ Or (Neg f) i
            <|> do try (string "<->")
                   spaces
                   i <- implFormula sig flag
                   return $ And (Or (Neg f) i) (Or f (Neg i))
            <|> do string "<-"
                   spaces
                   i <- implFormula sig flag
                   return $ Or f (Neg i)
            <|> return f
            <?> "GMPParser.implFormula")
  
  -- | Parser for disjunction - used for handling binding order
  orFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                     Parser (Formula (a (b c)) )
  orFormula sig flag = do
      f <- andFormula sig flag
      option f $ do
        string "\\/"
        spaces
        g <- orFormula sig flag
        return $ Or f g
    <?> "GMPParser.orFormula"
  
  -- | Parser for conjunction - used for handling the binding order
  andFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                      Parser (Formula (a (b c)) )
  andFormula sig flag = do
      f <- primFormula sig flag
      option f $ do
        string "/\\"
        spaces
        g <- andFormula sig flag
        return $ And f g
    <?> "GMPParser.andFormula"
  
  {- | Parse a primitive formula: T, F, ~f, <i>f, [i]f, p*,
   -   where i stands for an index, f for a formula and
   -   * for a series of digits i.e. and integer -}
  primFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                       Parser (Formula (a (b c)) )
  primFormula sig flag =
                    do string "T"
                       spaces
                       return T
                <|> do string "F"
                       spaces
                       return F
                <|> parenFormula sig flag
                <|> do string "~"
                       spaces
                       f <- primFormula sig flag
                       return $ nneg f
                <|> do char '<'
                       spaces
                       i <- sParser sig
                       spaces
                       char '>'
                       spaces
                       f <- sepBy1 (pGoOn sig flag) (string (fSeparator sig))
                       -- restrict to the default modal operator
                       case flag of
                         Ang -> return $ Mod (i f)
                         Sqr -> return $ Neg (Mod (i (map nneg f)))
                         _ -> return $ Mod (i f)
                <|> do char '['
                       spaces
                       i <- sParser sig
                       spaces
                       char ']'
                       spaces
                       f <- sepBy1 (pGoOn sig flag) (string (fSeparator sig))
                       -- restrict to the default modal operator
                       case flag of
                         Sqr -> return $ Mod (i f)
                         Ang -> return $ Neg (Mod (i (map nneg f)))
                         _ -> return $ Mod (i f)
                <|> do char 'p'
                       i <- atomIndex
                       return $ Atom (fromInteger i)
                <?> "GMPParser.primFormula"
  
  -- | Parser for un-parenthesizing a formula
  parenFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
                                        Parser (Formula (a (b c)) )
  parenFormula sig flag =
                     do char '('
                        spaces
                        f <- parser sig flag
                        spaces
                        char ')'
                        spaces
                        return f
                 <?> "GMPParser.parenFormula"
  
  -- | Parse integer number
  natural :: GenParser Char st Integer
  natural = fmap read $ many1 digit
  
  -- | Parse the possible integer index of a variable
  atomIndex :: GenParser Char st Integer
  atomIndex =  do i <- try natural
                  spaces
                  return i
           <?> "GMPParser.atomIndex"
  