module CASL_DL.Parse_AS where
import Common.AnnoState
import Common.Id
import Common.Lexer
import Common.Parsec
import Common.Token
import CASL_DL.AS_CASL_DL
import CASL.Formula
import CASL.AS_Basic_CASL
import Text.ParserCombinators.Parsec
dlFormula :: AParser st DL_FORMULA
dlFormula :: AParser st DL_FORMULA
dlFormula = do
(ct :: CardType
ct, ctp :: Range
ctp) <- AParser st (CardType, Range)
forall st. AParser st (CardType, Range)
cardKeyword
Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
PRED_SYMB
p <- AParser st PRED_SYMB
forall st. AParser st PRED_SYMB
parsePredSymb
Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
Token
op <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT
TERM DL_FORMULA
t1 <- [String] -> AParser st (TERM DL_FORMULA)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
casl_DL_reserved_words
Token
co <- CharParser (AnnoState st) Token
forall st. AParser st Token
anComma
TERM DL_FORMULA
t2 <- [String] -> AParser st (TERM DL_FORMULA)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
casl_DL_reserved_words
Maybe (FORMULA DL_FORMULA)
t3 <- ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
-> ParsecT
String (AnnoState st) Identity (Maybe (FORMULA DL_FORMULA))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
-> ParsecT
String (AnnoState st) Identity (Maybe (FORMULA DL_FORMULA)))
-> ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
-> ParsecT
String (AnnoState st) Identity (Maybe (FORMULA DL_FORMULA))
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) Token
forall st. AParser st Token
anComma CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
-> ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String]
-> ParsecT String (AnnoState st) Identity (FORMULA DL_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
casl_DL_reserved_words
Token
cp <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT
DL_FORMULA -> AParser st DL_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (DL_FORMULA -> AParser st DL_FORMULA)
-> DL_FORMULA -> AParser st DL_FORMULA
forall a b. (a -> b) -> a -> b
$ CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
p TERM DL_FORMULA
t1 TERM DL_FORMULA
t2 Maybe (FORMULA DL_FORMULA)
t3
(Range -> DL_FORMULA) -> Range -> DL_FORMULA
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
ctp (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ (Token -> Range) -> [Token] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange Token -> Range
tokPos [Token
o, Token
c, Token
op, Token
co, Token
cp]
parsePredSymb :: AParser st PRED_SYMB
parsePredSymb :: AParser st PRED_SYMB
parsePredSymb = (PRED_NAME -> PRED_SYMB)
-> ParsecT String (AnnoState st) Identity PRED_NAME
-> AParser st PRED_SYMB
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PRED_NAME -> PRED_SYMB
Pred_name ([String] -> ParsecT String (AnnoState st) Identity PRED_NAME
forall st. [String] -> GenParser Char st PRED_NAME
parseId [String]
casl_DL_reserved_words)
AParser st PRED_SYMB
-> AParser st PRED_SYMB -> AParser st PRED_SYMB
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
Mixfix_qual_pred qpred :: PRED_SYMB
qpred <- [String] -> Token -> AParser st (TERM Any)
forall st f. [String] -> Token -> AParser st (TERM f)
qualPredName [String]
casl_DL_reserved_words Token
o
PRED_SYMB -> AParser st PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return PRED_SYMB
qpred
AParser st PRED_SYMB -> String -> AParser st PRED_SYMB
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "a PRED_SYMB"
cardKeyword :: AParser st (CardType, Range)
cardKeyword :: AParser st (CardType, Range)
cardKeyword = [AParser st (CardType, Range)] -> AParser st (CardType, Range)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st (CardType, Range)] -> AParser st (CardType, Range))
-> [AParser st (CardType, Range)] -> AParser st (CardType, Range)
forall a b. (a -> b) -> a -> b
$ (CardType -> AParser st (CardType, Range))
-> [CardType] -> [AParser st (CardType, Range)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ v :: CardType
v -> do
Token
kw <- String -> AParser st Token
forall st. String -> AParser st Token
asKey (String -> AParser st Token) -> String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ CardType -> String
forall a. Show a => a -> String
show CardType
v
(CardType, Range) -> AParser st (CardType, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (CardType
v, Token -> Range
tokPos Token
kw)) [CardType]
caslDLCardTypes
instance TermParser DL_FORMULA where
termParser :: Bool -> AParser st DL_FORMULA
termParser = AParser st DL_FORMULA -> Bool -> AParser st DL_FORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st DL_FORMULA
forall st. AParser st DL_FORMULA
dlFormula