# LANGUAGE TypeOperators , FlexibleContexts , FlexibleInstances , MultiParamTypeClasses #
module Carnap.Languages.ModalFirstOrder.Parser ( hardegreeMPLFormulaPreParser, hardegreeMPLFormulaParser) where

import Carnap.Core.Data.Types
import Carnap.Core.Data.Classes (Schematizable)
import Carnap.Languages.ClassicalSequent.Parser
import Carnap.Languages.PureFirstOrder.Syntax (foVar)
import Carnap.Languages.ModalPropositional.Syntax
import Carnap.Languages.ModalFirstOrder.Syntax
import Carnap.Languages.Util.LanguageClasses (BooleanLanguage, StandardVarLanguage, ModalLanguage, PrismModality, BooleanConstLanguage, IndexingLang(..), IndexConsLang(..), IndexedPropLanguage(..), QuantLanguage(..))
import Carnap.Languages.Util.GenericParsers
import Text.Parsec
import Text.Parsec.Expr
import Control.Monad.Identity

data ModalFirstOrderParserOptions lex u m = ModalFirstOrderParserOptions 
                                          { atomicSentenceParser :: ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                          , quantifiedSentenceParser' :: ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                          , freeVarParser  :: ParsecT String u m (FixLang lex (Term Int)) 
                                          , constantParser :: Maybe (ParsecT String u m (FixLang lex (Term Int)))
                                          , functionParser :: Maybe (ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Term Int)))
                                          , hasBooleanConstants :: Bool
                                          }

hardegreeMPLParserOptions :: ModalFirstOrderParserOptions IndexedModalFirstOrderLex u Identity
hardegreeMPLParserOptions = ModalFirstOrderParserOptions 
                         { atomicSentenceParser = \x -> parsePredicateSymbolNoParen "ABCDEFGHIJKLMNOPQRSTUVWXYZ" x
                         , quantifiedSentenceParser' = quantifiedSentenceParser
                         , freeVarParser = parseFreeVar "tuvwxyz"
                         , constantParser = Just (parseConstant "abcdefghijklmnopqrs")
                         , functionParser = Nothing
                         , hasBooleanConstants = True
                         }

coreSubformulaParser :: ( BoundVars lex
                        , BooleanLanguage (FixLang lex (Form (World -> Bool)))
                        , ModalLanguage (FixLang lex (Form (World -> Bool)))
                        , BooleanConstLanguage (FixLang lex (Form (World -> Bool)))
                        , QuantLanguage (FixLang lex (Form (World -> Bool))) (FixLang lex (Term Int))
                        ) =>
    Parsec String u (FixLang lex (Form (World -> Bool))) -> ModalFirstOrderParserOptions lex u Identity
        -> Parsec String u (FixLang lex (Form (World -> Bool)))
coreSubformulaParser fp opts = (parenParser fp <* spaces)
                             <|> try (unaryOpParser [parseNeg, parsePos, parseNec] (coreSubformulaParser fp opts))
                             <|> try ((quantifiedSentenceParser' opts) vparser (coreSubformulaParser fp opts) <* spaces)
                             <|> (atomicSentenceParser opts tparser <* spaces)
                             <|> if hasBooleanConstants opts then try (booleanConstParser <* spaces) else parserZero
    where cparser = case constantParser opts of Just c -> c
                                                Nothing -> mzero
          --Function symbols, if there are any
          fparser = case functionParser opts of Just f -> f
                                                Nothing -> const mzero
          --Free variables
          vparser = freeVarParser opts 
          --Terms
          tparser = try (fparser tparser) <|> cparser <|> vparser

parserFromOptions opts = buildExpressionParser opTable subformulaParser
    where subformulaParser = coreSubformulaParser (parserFromOptions opts) opts 

hardegreeMPLFormulaParser :: Parsec String u (IndexedModalFirstOrderLanguage (Form Bool))
hardegreeMPLFormulaParser = hardegreeMPLFormulaPreParser >>= indexIt
    where indexIt :: IndexedModalFirstOrderLanguage (Form (World -> Bool)) -> Parsec String u (IndexedModalFirstOrderLanguage (Form Bool))
          indexIt f = do char '/'
                         (w:ws)<- sepBy1 parseWorld (char '-')
                         let idx = foldl indexcons w ws
                         return (f `atWorld` idx)

hardegreeMPLFormulaPreParser :: Parsec String u (IndexedModalFirstOrderLanguage (Form (World -> Bool)))
hardegreeMPLFormulaPreParser = buildExpressionParser opTable subFormulaParser
          where subFormulaParser = coreSubformulaParser hardegreeMPLFormulaPreParser hardegreeMPLParserOptions

instance ParsableLex (Form (World -> Bool)) IndexedModalFirstOrderLex where
        langParser = hardegreeMPLFormulaPreParser

instance ParsableLex (Form Bool) IndexedModalFirstOrderLex where
        langParser = hardegreeMPLFormulaParser

parseFreeVar :: StandardVarLanguage ((ModalFirstOrderLanguageOverWith b a (Term Int))) => String -> Parsec String u (ModalFirstOrderLanguageOverWith b a (Term Int))
parseFreeVar s = choice [try $ do _ <- string "x_"
                                  dig <- many1 digit
                                  return $ foVar $ "x_" ++ dig
                        ,      do c <- oneOf s
                                  return $ foVar [c]
                        ]

opTable :: ( BooleanLanguage (ModalFirstOrderLanguageOverWith b a (Form (World -> Bool)))
           , PrismModality (ModalFirstOrderLexOverWith b a) (World -> Bool)
           , Monad m)
    => [[Operator String u m (ModalFirstOrderLanguageOverWith b a (Form (World -> Bool)))]]
opTable = [[ Prefix (try parseNeg), Prefix (try parseNec), Prefix (try parsePos)], 
          [Infix (try parseOr) AssocLeft, Infix (try parseAnd) AssocLeft],
          [Infix (try parseIf) AssocNone, Infix (try parseIff) AssocNone]]

parseWorld :: (IndexingLang lex (Term World) (Form c) (Form b), Monad m) => ParsecT String u m (FixLang lex (Term World))
parseWorld = do digits <- many1 digit
                return $ world (read digits)

Function symbols, if there are any
Free variables
Terms
# LANGUAGE TypeOperators , FlexibleContexts , FlexibleInstances , MultiParamTypeClasses #
module Carnap.Languages.ModalFirstOrder.Parser ( hardegreeMPLFormulaPreParser, hardegreeMPLFormulaParser) where

import Carnap.Core.Data.Types
import Carnap.Core.Data.Classes (Schematizable)
import Carnap.Languages.ClassicalSequent.Parser
import Carnap.Languages.PureFirstOrder.Syntax (foVar)
import Carnap.Languages.ModalPropositional.Syntax
import Carnap.Languages.ModalFirstOrder.Syntax
import Carnap.Languages.Util.LanguageClasses (BooleanLanguage, StandardVarLanguage, ModalLanguage, PrismModality, BooleanConstLanguage, IndexingLang(..), IndexConsLang(..), IndexedPropLanguage(..), QuantLanguage(..))
import Carnap.Languages.Util.GenericParsers
import Text.Parsec
import Text.Parsec.Expr
import Control.Monad.Identity

data ModalFirstOrderParserOptions lex u m = ModalFirstOrderParserOptions 
                                          { atomicSentenceParser :: ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                          , quantifiedSentenceParser' :: ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                             -> ParsecT String u m (FixLang lex (Form (World -> Bool)))
                                          , freeVarParser  :: ParsecT String u m (FixLang lex (Term Int)) 
                                          , constantParser :: Maybe (ParsecT String u m (FixLang lex (Term Int)))
                                          , functionParser :: Maybe (ParsecT String u m (FixLang lex (Term Int)) 
                                             -> ParsecT String u m (FixLang lex (Term Int)))
                                          , hasBooleanConstants :: Bool
                                          }

hardegreeMPLParserOptions :: ModalFirstOrderParserOptions IndexedModalFirstOrderLex u Identity
hardegreeMPLParserOptions = ModalFirstOrderParserOptions 
                         { atomicSentenceParser = \x -> parsePredicateSymbolNoParen "ABCDEFGHIJKLMNOPQRSTUVWXYZ" x
                         , quantifiedSentenceParser' = quantifiedSentenceParser
                         , freeVarParser = parseFreeVar "tuvwxyz"
                         , constantParser = Just (parseConstant "abcdefghijklmnopqrs")
                         , functionParser = Nothing
                         , hasBooleanConstants = True
                         }

coreSubformulaParser :: ( BoundVars lex
                        , BooleanLanguage (FixLang lex (Form (World -> Bool)))
                        , ModalLanguage (FixLang lex (Form (World -> Bool)))
                        , BooleanConstLanguage (FixLang lex (Form (World -> Bool)))
                        , QuantLanguage (FixLang lex (Form (World -> Bool))) (FixLang lex (Term Int))
                        ) =>
    Parsec String u (FixLang lex (Form (World -> Bool))) -> ModalFirstOrderParserOptions lex u Identity
        -> Parsec String u (FixLang lex (Form (World -> Bool)))
coreSubformulaParser fp opts = (parenParser fp <* spaces)
                             <|> try (unaryOpParser [parseNeg, parsePos, parseNec] (coreSubformulaParser fp opts))
                             <|> try ((quantifiedSentenceParser' opts) vparser (coreSubformulaParser fp opts) <* spaces)
                             <|> (atomicSentenceParser opts tparser <* spaces)
                             <|> if hasBooleanConstants opts then try (booleanConstParser <* spaces) else parserZero
    where cparser = case constantParser opts of Just c -> c
                                                Nothing -> mzero
          fparser = case functionParser opts of Just f -> f
                                                Nothing -> const mzero
          vparser = freeVarParser opts 
          tparser = try (fparser tparser) <|> cparser <|> vparser

parserFromOptions opts = buildExpressionParser opTable subformulaParser
    where subformulaParser = coreSubformulaParser (parserFromOptions opts) opts 

hardegreeMPLFormulaParser :: Parsec String u (IndexedModalFirstOrderLanguage (Form Bool))
hardegreeMPLFormulaParser = hardegreeMPLFormulaPreParser >>= indexIt
    where indexIt :: IndexedModalFirstOrderLanguage (Form (World -> Bool)) -> Parsec String u (IndexedModalFirstOrderLanguage (Form Bool))
          indexIt f = do char '/'
                         (w:ws)<- sepBy1 parseWorld (char '-')
                         let idx = foldl indexcons w ws
                         return (f `atWorld` idx)

hardegreeMPLFormulaPreParser :: Parsec String u (IndexedModalFirstOrderLanguage (Form (World -> Bool)))
hardegreeMPLFormulaPreParser = buildExpressionParser opTable subFormulaParser
          where subFormulaParser = coreSubformulaParser hardegreeMPLFormulaPreParser hardegreeMPLParserOptions

instance ParsableLex (Form (World -> Bool)) IndexedModalFirstOrderLex where
        langParser = hardegreeMPLFormulaPreParser

instance ParsableLex (Form Bool) IndexedModalFirstOrderLex where
        langParser = hardegreeMPLFormulaParser

parseFreeVar :: StandardVarLanguage ((ModalFirstOrderLanguageOverWith b a (Term Int))) => String -> Parsec String u (ModalFirstOrderLanguageOverWith b a (Term Int))
parseFreeVar s = choice [try $ do _ <- string "x_"
                                  dig <- many1 digit
                                  return $ foVar $ "x_" ++ dig
                        ,      do c <- oneOf s
                                  return $ foVar [c]
                        ]

opTable :: ( BooleanLanguage (ModalFirstOrderLanguageOverWith b a (Form (World -> Bool)))
           , PrismModality (ModalFirstOrderLexOverWith b a) (World -> Bool)
           , Monad m)
    => [[Operator String u m (ModalFirstOrderLanguageOverWith b a (Form (World -> Bool)))]]
opTable = [[ Prefix (try parseNeg), Prefix (try parseNec), Prefix (try parsePos)], 
          [Infix (try parseOr) AssocLeft, Infix (try parseAnd) AssocLeft],
          [Infix (try parseIf) AssocNone, Infix (try parseIff) AssocNone]]

parseWorld :: (IndexingLang lex (Term World) (Form c) (Form b), Monad m) => ParsecT String u m (FixLang lex (Term World))
parseWorld = do digits <- many1 digit
                return $ world (read digits)
