{- |
Module      :  ./Modal/Parse_AS.hs
Copyright   :  (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Parser for modal logic extension of CASL
-}

module Modal.Parse_AS where

import CASL.Formula
import CASL.OpItem

import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Token

import Modal.AS_Modal

import Text.ParserCombinators.Parsec

import Data.List

modal_reserved_words :: [String]
modal_reserved_words :: [String]
modal_reserved_words =
  String
diamondS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
termS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
rigidS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
flexibleS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
modalityS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
modalitiesS]

modalFormula :: AParser st M_FORMULA
modalFormula :: AParser st M_FORMULA
modalFormula =
    do Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
       MODALITY
m <- [String] -> AParser st MODALITY
forall st. [String] -> AParser st MODALITY
modality []
       Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
       FORMULA M_FORMULA
f <- [String] -> AParser st (FORMULA M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
modal_reserved_words
       M_FORMULA -> AParser st M_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
True MODALITY
m FORMULA M_FORMULA
f (Range -> M_FORMULA) -> Range -> M_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)
    AParser st M_FORMULA
-> AParser st M_FORMULA -> AParser st M_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Token
o <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
lessS
       MODALITY
m <- [String] -> AParser st MODALITY
forall st. [String] -> AParser st MODALITY
modality [String
greaterS] -- do not consume matching ">"!
       Token
c <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
greaterS
       FORMULA M_FORMULA
f <- [String] -> AParser st (FORMULA M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
modal_reserved_words
       M_FORMULA -> AParser st M_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
False MODALITY
m FORMULA M_FORMULA
f (Range -> M_FORMULA) -> Range -> M_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)
    AParser st M_FORMULA
-> AParser st M_FORMULA -> AParser st M_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Token
d <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
diamondS
       FORMULA M_FORMULA
f <- [String] -> AParser st (FORMULA M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
modal_reserved_words
       let p :: Range
p = Token -> Range
tokPos Token
d
       M_FORMULA -> AParser st M_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
False (Token -> MODALITY
Simple_mod (Token -> MODALITY) -> Token -> MODALITY
forall a b. (a -> b) -> a -> b
$ String -> Range -> Token
Token String
emptyS Range
p) FORMULA M_FORMULA
f Range
p)

modality :: [String] -> AParser st MODALITY
modality :: [String] -> AParser st MODALITY
modality ks :: [String]
ks =
    do TERM M_FORMULA
t <- [String] -> AParser st (TERM M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term ([String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
modal_reserved_words)
       MODALITY -> AParser st MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> AParser st MODALITY)
-> MODALITY -> AParser st MODALITY
forall a b. (a -> b) -> a -> b
$ TERM M_FORMULA -> MODALITY
Term_mod TERM M_FORMULA
t
   AParser st MODALITY -> AParser st MODALITY -> AParser st MODALITY
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> MODALITY -> AParser st MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> MODALITY
Simple_mod (Token -> MODALITY) -> Token -> MODALITY
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
emptyS)

instance TermParser M_FORMULA where
    termParser :: Bool -> AParser st M_FORMULA
termParser = AParser st M_FORMULA -> Bool -> AParser st M_FORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st M_FORMULA
forall st. AParser st M_FORMULA
modalFormula

rigor :: AParser st RIGOR
rigor :: AParser st RIGOR
rigor = (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
rigidS AParser st Token -> AParser st RIGOR -> AParser st RIGOR
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RIGOR -> AParser st RIGOR
forall (m :: * -> *) a. Monad m => a -> m a
return RIGOR
Rigid)
        AParser st RIGOR -> AParser st RIGOR -> AParser st RIGOR
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
flexibleS AParser st Token -> AParser st RIGOR -> AParser st RIGOR
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RIGOR -> AParser st RIGOR
forall (m :: * -> *) a. Monad m => a -> m a
return RIGOR
Flexible)

rigidSigItems :: AParser st M_SIG_ITEM
rigidSigItems :: AParser st M_SIG_ITEM
rigidSigItems =
    do RIGOR
r <- AParser st RIGOR
forall st. AParser st RIGOR
rigor
       [String]
-> String
-> ([String] -> AParser st (OP_ITEM M_FORMULA))
-> ([Annoted (OP_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM)
-> AParser st M_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
modal_reserved_words String
opS [String] -> AParser st (OP_ITEM M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (OP_ITEM f)
opItem (RIGOR -> [Annoted (OP_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM
Rigid_op_items RIGOR
r)
         AParser st M_SIG_ITEM
-> AParser st M_SIG_ITEM -> AParser st M_SIG_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> String
-> ([String] -> AParser st (PRED_ITEM M_FORMULA))
-> ([Annoted (PRED_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM)
-> AParser st M_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
modal_reserved_words String
predS [String] -> AParser st (PRED_ITEM M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (PRED_ITEM f)
predItem (RIGOR -> [Annoted (PRED_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM
Rigid_pred_items RIGOR
r)

instance AParsable M_SIG_ITEM where
  aparser :: AParser st M_SIG_ITEM
aparser = AParser st M_SIG_ITEM
forall st. AParser st M_SIG_ITEM
rigidSigItems

mKey :: AParser st Token
mKey :: AParser st Token
mKey = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
modalityS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
modalitiesS

mBasic :: AParser st M_BASIC_ITEM
mBasic :: AParser st M_BASIC_ITEM
mBasic =
    do (as :: [Annoted Token]
as, fs :: [AnModFORM]
fs, ps :: Range
ps) <- AParser st Token
-> AParser st ([Annoted Token], [AnModFORM], Range)
forall st a.
AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
mItem AParser st Token
forall st. CharParser st Token
simpleId
       M_BASIC_ITEM -> AParser st M_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted Token] -> [AnModFORM] -> Range -> M_BASIC_ITEM
Simple_mod_decl [Annoted Token]
as [AnModFORM]
fs Range
ps)
    AParser st M_BASIC_ITEM
-> AParser st M_BASIC_ITEM -> AParser st M_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
termS
       (as :: [Annoted Id]
as, fs :: [AnModFORM]
fs, ps :: Range
ps) <- AParser st Id -> AParser st ([Annoted Id], [AnModFORM], Range)
forall st a.
AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
mItem ([String] -> AParser st Id
forall st. [String] -> GenParser Char st Id
sortId [String]
modal_reserved_words)
       M_BASIC_ITEM -> AParser st M_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted Id] -> [AnModFORM] -> Range -> M_BASIC_ITEM
Term_mod_decl [Annoted Id]
as [AnModFORM]
fs (Token -> Range
tokPos Token
t Range -> Range -> Range
`appRange` Range
ps))

mItem :: AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
mItem :: AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
mItem pr :: AParser st a
pr = do
       Token
c <- AParser st Token
forall st. AParser st Token
mKey
       (as :: [Annoted a]
as, cs :: [Token]
cs) <- GenParser Char (AnnoState st) (Annoted a)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted a], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (AParser st a -> GenParser Char (AnnoState st) (Annoted a)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser AParser st a
pr) AParser st Token
forall st. AParser st Token
anSemiOrComma
       let ps :: Range
ps = [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs
       do Token
o <- AParser st Token
forall st. CharParser st Token
oBraceT
          (fs :: [AnModFORM]
fs, q :: Range
q) <- [String]
-> [Token]
-> AParser st (FORMULA M_FORMULA)
-> ([AnModFORM] -> Range -> ([AnModFORM], Range))
-> AParser st ([AnModFORM], Range)
forall st b a.
[String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList (String -> [String] -> [String]
forall a. Eq a => a -> [a] -> [a]
delete String
diamondS [String]
modal_reserved_words) []
                      ([String] -> AParser st (FORMULA M_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
modal_reserved_words) (,)
          Token
p <- AParser st Token
forall st. CharParser st Token
cBraceT
          ([Annoted a], [AnModFORM], Range)
-> AParser st ([Annoted a], [AnModFORM], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted a]
as, [AnModFORM]
fs, Range
ps Range -> Range -> Range
`appRange` Range
q Range -> Range -> Range
`appRange` Token -> [Token] -> Token -> Range
toRange Token
o [] Token
p)
        AParser st ([Annoted a], [AnModFORM], Range)
-> AParser st ([Annoted a], [AnModFORM], Range)
-> AParser st ([Annoted a], [AnModFORM], Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Annoted a], [AnModFORM], Range)
-> AParser st ([Annoted a], [AnModFORM], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted a]
as, [], Range
ps)

instance AParsable M_BASIC_ITEM where
  aparser :: AParser st M_BASIC_ITEM
aparser = AParser st M_BASIC_ITEM
forall st. AParser st M_BASIC_ITEM
mBasic