{- |
Module      :  ./Hybrid/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 Hybrid.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 Hybrid.AS_Hybrid
import Hybrid.Keywords
import Text.ParserCombinators.Parsec

hybrid_reserved_words :: [String]
hybrid_reserved_words :: [String]
hybrid_reserved_words = [
        String
diamondS,
        String
termS,
        String
rigidS,
        String
flexibleS,
        String
modalityS,
        String
modalitiesS,
        String
nominalS,
        String
nominalsS]

hybridFormula :: AParser st H_FORMULA
hybridFormula :: AParser st H_FORMULA
hybridFormula =
        do
        Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
hereP
        NOMINAL
n <- AParser st NOMINAL
forall st. AParser st NOMINAL
nominal
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> Range -> H_FORMULA
Here NOMINAL
n (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
a [] Token
a)
        AParser st H_FORMULA
-> AParser st H_FORMULA -> AParser st H_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
asP
        NOMINAL
n <- AParser st NOMINAL
forall st. AParser st NOMINAL
nominal
        FORMULA H_FORMULA
f <- [String] -> AParser st (FORMULA H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
hybrid_reserved_words
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
n FORMULA H_FORMULA
f (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
a [] Token
a)
        AParser st H_FORMULA
-> AParser st H_FORMULA -> AParser st H_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
exMark
        NOMINAL
n <- AParser st NOMINAL
forall st. AParser st NOMINAL
nominal
        FORMULA H_FORMULA
f <- [String] -> AParser st (FORMULA H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
hybrid_reserved_words
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
n FORMULA H_FORMULA
f (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
a [] Token
a)
        AParser st H_FORMULA
-> AParser st H_FORMULA -> AParser st H_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "?"
        NOMINAL
n <- AParser st NOMINAL
forall st. AParser st NOMINAL
nominal
        FORMULA H_FORMULA
f <- [String] -> AParser st (FORMULA H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
hybrid_reserved_words
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
n FORMULA H_FORMULA
f (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
a [] Token
a)
        AParser st H_FORMULA
-> AParser st H_FORMULA -> AParser st H_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        Token
o <- AParser st Token
forall st. CharParser st Token
oBracketT
        MODALITY
m <- [String] -> AParser st MODALITY
forall st. [String] -> AParser st MODALITY
modality []
        Token
c <- AParser st Token
forall st. CharParser st Token
cBracketT
        FORMULA H_FORMULA
f <- [String] -> AParser st (FORMULA H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
hybrid_reserved_words
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
True MODALITY
m FORMULA H_FORMULA
f (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)
        AParser st H_FORMULA
-> AParser st H_FORMULA -> AParser st H_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 -> AParser 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 -> AParser st Token
forall st. String -> AParser st Token
asKey String
greaterS
        FORMULA H_FORMULA
f <- [String] -> AParser st (FORMULA H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
hybrid_reserved_words
        H_FORMULA -> AParser st H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
False MODALITY
m FORMULA H_FORMULA
f (Range -> H_FORMULA) -> Range -> H_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)

nominal :: AParser st NOMINAL
nominal :: AParser st NOMINAL
nominal =
        do
        Token
n <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
simpleId
        NOMINAL -> AParser st NOMINAL
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> NOMINAL
Simple_nom Token
n)

modality :: [String] -> AParser st MODALITY
modality :: [String] -> AParser st MODALITY
modality ks :: [String]
ks =
    do TERM H_FORMULA
t <- [String] -> AParser st (TERM H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term ([String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
hybrid_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 H_FORMULA -> MODALITY
Term_mod TERM H_FORMULA
t


instance TermParser H_FORMULA where
    termParser :: Bool -> AParser st H_FORMULA
termParser = AParser st H_FORMULA -> Bool -> AParser st H_FORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st H_FORMULA
forall st. AParser st H_FORMULA
hybridFormula

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 H_SIG_ITEM
rigidSigItems :: AParser st H_SIG_ITEM
rigidSigItems =
    do RIGOR
r <- AParser st RIGOR
forall st. AParser st RIGOR
rigor
       [String]
-> String
-> ([String] -> AParser st (OP_ITEM H_FORMULA))
-> ([Annoted (OP_ITEM H_FORMULA)] -> Range -> H_SIG_ITEM)
-> AParser st H_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
hybrid_reserved_words String
opS [String] -> AParser st (OP_ITEM H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (OP_ITEM f)
opItem (RIGOR -> [Annoted (OP_ITEM H_FORMULA)] -> Range -> H_SIG_ITEM
Rigid_op_items RIGOR
r)
         AParser st H_SIG_ITEM
-> AParser st H_SIG_ITEM -> AParser st H_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 H_FORMULA))
-> ([Annoted (PRED_ITEM H_FORMULA)] -> Range -> H_SIG_ITEM)
-> AParser st H_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
hybrid_reserved_words String
predS [String] -> AParser st (PRED_ITEM H_FORMULA)
forall f st. TermParser f => [String] -> AParser st (PRED_ITEM f)
predItem (RIGOR -> [Annoted (PRED_ITEM H_FORMULA)] -> Range -> H_SIG_ITEM
Rigid_pred_items RIGOR
r)

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

hKey :: AParser st Token
hKey :: AParser st Token
hKey = 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

hKey' :: AParser st Token
hKey' :: AParser st Token
hKey' = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
nominalS 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
nominalsS

hBasic :: AParser st H_BASIC_ITEM
hBasic :: AParser st H_BASIC_ITEM
hBasic =
    do (as :: [Annoted Token]
as, fs :: [AnHybFORM]
fs, ps :: Range
ps) <- AParser st Token
-> AParser st Token
-> AParser st ([Annoted Token], [AnHybFORM], Range)
forall st a.
AParser st Token
-> AParser st a -> AParser st ([Annoted a], [AnHybFORM], Range)
hItem'' AParser st Token
forall st. AParser st Token
hKey AParser st Token
forall st. CharParser st Token
simpleId
       H_BASIC_ITEM -> AParser st H_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted Token] -> [AnHybFORM] -> Range -> H_BASIC_ITEM
Simple_mod_decl [Annoted Token]
as [AnHybFORM]
fs Range
ps)
    AParser st H_BASIC_ITEM
-> AParser st H_BASIC_ITEM -> AParser st H_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do (as :: [Annoted Token]
as, fs :: [AnHybFORM]
fs, ps :: Range
ps) <- AParser st Token
-> AParser st Token
-> AParser st ([Annoted Token], [AnHybFORM], Range)
forall st a.
AParser st Token
-> AParser st a -> AParser st ([Annoted a], [AnHybFORM], Range)
hItem'' AParser st Token
forall st. AParser st Token
hKey' AParser st Token
forall st. CharParser st Token
simpleId
       H_BASIC_ITEM -> AParser st H_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted Token] -> [AnHybFORM] -> Range -> H_BASIC_ITEM
Simple_nom_decl [Annoted Token]
as [AnHybFORM]
fs Range
ps)

hItem'' :: AParser st Token -> AParser st a ->
           AParser st ([Annoted a], [AnHybFORM], Range)
hItem'' :: AParser st Token
-> AParser st a -> AParser st ([Annoted a], [AnHybFORM], Range)
hItem'' k :: AParser st Token
k pr :: AParser st a
pr = do
        Token
c <- AParser st Token
k
        (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
        ([Annoted a], [AnHybFORM], Range)
-> AParser st ([Annoted a], [AnHybFORM], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted a]
as, [], Range
ps)

instance AParsable H_BASIC_ITEM where
  aparser :: AParser st H_BASIC_ITEM
aparser = AParser st H_BASIC_ITEM
forall st. AParser st H_BASIC_ITEM
hBasic