{- |
Module      :  ./ExtModal/Parse_AS.hs
Description :  Parser for extended modal logic
Copyright   :  DFKI GmbH 2009
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

-}

module ExtModal.Parse_AS (ext_modal_reserved_words) where

import Text.ParserCombinators.Parsec

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

import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.OpItem
import CASL.Parse_AS_Basic

import ExtModal.AS_ExtModal
import ExtModal.Keywords

import Data.Maybe

-- | List of reserved words
ext_modal_reserved_words :: [String]
ext_modal_reserved_words :: [String]
ext_modal_reserved_words = (ModOp -> String) -> [ModOp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ModOp -> String
forall a. Show a => a -> String
show [ModOp
Intersection, ModOp
Union] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
untilS
  , String
sinceS
  , String
allPathsS
  , String
somePathsS
  , String
nextS
  , String
yesterdayS
  , String
generallyS
  , String
eventuallyS
  , String
atS
  , String
quMark
  , String
hereS
  , String
timeS
  , String
nominalS
  , String
nominalS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS
  , String
hithertoS
  , String
previouslyS
  , String
muS
  , String
nuS
  , String
diamondS
  , String
orElseS
  , String
oB
  , String
cB
  , String
termS
  , String
rigidS
  , String
flexibleS
  , String
modalityS
  , String
modalitiesS ]

boxParser :: AParser st (MODALITY, BoxOp, Range)
boxParser :: AParser st (MODALITY, BoxOp, Range)
boxParser = do
    let asESep :: String -> CharParser st Token
asESep = CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> CharParser st Token)
-> (String -> CharParser st String)
-> String
-> CharParser st Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> CharParser st String
forall st. String -> CharParser st String
tryString
    Token
open <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
asESep String
oB
    let isBox :: Bool
isBox = Token -> String
tokStr Token
open String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "["
    MODALITY
modal <- AParser st MODALITY
forall st. AParser st MODALITY
parseModality
    Token
close <- if Bool
isBox then CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT else String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
asESep String
cB
    (MODALITY, BoxOp, Range) -> AParser st (MODALITY, BoxOp, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY
modal, if Bool
isBox then BoxOp
Box else BoxOp
EBox, Token -> [Token] -> Token -> Range
toRange Token
open [] Token
close)

diamondParser :: AParser st (MODALITY, BoxOp, Range)
diamondParser :: AParser st (MODALITY, BoxOp, Range)
diamondParser = do
    Token
open <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lessS
    MODALITY
modal <- AParser st MODALITY
forall st. AParser st MODALITY
parseModality
    Token
close <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
greaterS
    (MODALITY, BoxOp, Range) -> AParser st (MODALITY, BoxOp, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY
modal, BoxOp
Diamond, Token -> [Token] -> Token -> Range
toRange Token
open [] Token
close)
  AParser st (MODALITY, BoxOp, Range)
-> AParser st (MODALITY, BoxOp, Range)
-> AParser st (MODALITY, BoxOp, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
d <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
diamondS
    let p :: Range
p = Token -> Range
tokPos Token
d
    (MODALITY, BoxOp, Range) -> AParser st (MODALITY, BoxOp, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> MODALITY
SimpleMod (Token -> MODALITY) -> Token -> MODALITY
forall a b. (a -> b) -> a -> b
$ String -> Range -> Token
Token String
emptyS Range
p, BoxOp
Diamond, Range
p)

rekPrimParser :: AParser st (FORMULA EM_FORMULA)
rekPrimParser :: AParser st (FORMULA EM_FORMULA)
rekPrimParser = AParser st EM_FORMULA
-> [String] -> AParser st (FORMULA EM_FORMULA)
forall f st.
TermParser f =>
AParser st f -> [String] -> AParser st (FORMULA f)
genPrimFormula AParser st EM_FORMULA
forall st. AParser st EM_FORMULA
modalPrimFormulaParser [String]
ext_modal_reserved_words

infixTok :: AParser st (Token, Bool)
infixTok :: AParser st (Token, Bool)
infixTok = ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Bool
-> AParser st (Token, Bool)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
untilS) (Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    AParser st (Token, Bool)
-> AParser st (Token, Bool) -> AParser st (Token, Bool)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Bool
-> AParser st (Token, Bool)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
sinceS) (Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

-- | Modal infix formula parser
modalFormulaParser :: AParser st EM_FORMULA
modalFormulaParser :: AParser st EM_FORMULA
modalFormulaParser = do
    EM_FORMULA
p1 <- AParser st EM_FORMULA
forall st. AParser st EM_FORMULA
modalPrimFormulaParser
    EM_FORMULA -> AParser st EM_FORMULA -> AParser st EM_FORMULA
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option EM_FORMULA
p1 (AParser st EM_FORMULA -> AParser st EM_FORMULA)
-> AParser st EM_FORMULA -> AParser st EM_FORMULA
forall a b. (a -> b) -> a -> b
$ do
      (t :: Token
t, b :: Bool
b) <- AParser st (Token, Bool)
forall st. AParser st (Token, Bool)
infixTok
      FORMULA EM_FORMULA
f2 <- AParser st (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
rekPrimParser
      EM_FORMULA -> AParser st EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> AParser st EM_FORMULA)
-> EM_FORMULA -> AParser st EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
b (EM_FORMULA -> FORMULA EM_FORMULA
forall f. f -> FORMULA f
ExtFORMULA EM_FORMULA
p1) FORMULA EM_FORMULA
f2 (Range -> EM_FORMULA) -> Range -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
  AParser st EM_FORMULA
-> AParser st EM_FORMULA -> AParser st EM_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (f1 :: FORMULA EM_FORMULA
f1, (t :: Token
t, b :: Bool
b)) <- GenParser Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
-> GenParser
     Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
 -> GenParser
      Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool)))
-> GenParser
     Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
-> GenParser
     Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
forall a b. (a -> b) -> a -> b
$ AParser st (FORMULA EM_FORMULA)
-> AParser st (Token, Bool)
-> GenParser
     Char (AnnoState st) (FORMULA EM_FORMULA, (Token, Bool))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair AParser st (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
rekPrimParser AParser st (Token, Bool)
forall st. AParser st (Token, Bool)
infixTok
    FORMULA EM_FORMULA
f2 <- AParser st (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
rekPrimParser
    EM_FORMULA -> AParser st EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> AParser st EM_FORMULA)
-> EM_FORMULA -> AParser st EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
b FORMULA EM_FORMULA
f1 FORMULA EM_FORMULA
f2 (Range -> EM_FORMULA) -> Range -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t

prefixModifier :: AParser st (FormPrefix, Range)
prefixModifier :: AParser st (FormPrefix, Range)
prefixModifier = let mkF :: a -> Token -> m (a, Range)
mkF f :: a
f r :: Token
r = (a, Range) -> m (a, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
f, Token -> Range
tokPos Token
r) in
      (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
allPathsS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> FormPrefix
PathQuantification Bool
True))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
somePathsS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> FormPrefix
PathQuantification Bool
False))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
nextS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> FormPrefix
NextY Bool
True))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
yesterdayS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> FormPrefix
NextY Bool
False))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
generallyS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Bool -> FormPrefix
StateQuantification Bool
True Bool
True))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
eventuallyS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Bool -> FormPrefix
StateQuantification Bool
True Bool
False))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
hithertoS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Bool -> FormPrefix
StateQuantification Bool
False Bool
True))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
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
previouslyS AParser st Token
-> (Token -> AParser st (FormPrefix, Range))
-> AParser st (FormPrefix, Range)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Bool -> FormPrefix
StateQuantification Bool
False Bool
False))
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Bool
mnb <- (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
muS AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
      ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
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
nuS AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
    Token
z <- [String] -> AParser st Token
forall st. [String] -> GenParser Char st Token
varId [String]
ext_modal_reserved_words
    AParser st Token
forall st. AParser st Token
dotT
    FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Token -> FormPrefix
FixedPoint Bool
mnb Token
z) Token
z
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Bool
ahb <- (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
atS AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
      ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
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
hereS AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
    Token
nom <- AParser st Token
forall st. CharParser st Token
simpleId
    FormPrefix -> Token -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> Token -> m (a, Range)
mkF (Bool -> Token -> FormPrefix
Hybrid Bool
ahb Token
nom) Token
nom
  AParser st (FormPrefix, Range)
-> AParser st (FormPrefix, Range) -> AParser st (FormPrefix, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (modal :: MODALITY
modal, b :: BoxOp
b, r :: Range
r) <- AParser st (MODALITY, BoxOp, Range)
forall st. AParser st (MODALITY, BoxOp, Range)
boxParser AParser st (MODALITY, BoxOp, Range)
-> AParser st (MODALITY, BoxOp, Range)
-> AParser st (MODALITY, BoxOp, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (MODALITY, BoxOp, Range)
forall st. AParser st (MODALITY, BoxOp, Range)
diamondParser
    (lgb :: Bool
lgb, val :: Int
val) <- (Bool, Int)
-> ParsecT String (AnnoState st) Identity (Bool, Int)
-> ParsecT String (AnnoState st) Identity (Bool, Int)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Bool
True, 1) (ParsecT String (AnnoState st) Identity (Bool, Int)
 -> ParsecT String (AnnoState st) Identity (Bool, Int))
-> ParsecT String (AnnoState st) Identity (Bool, Int)
-> ParsecT String (AnnoState st) Identity (Bool, Int)
forall a b. (a -> b) -> a -> b
$ do
       Bool
lgb <- Bool
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Bool
False (ParsecT String (AnnoState st) Identity Bool
 -> ParsecT String (AnnoState st) Identity Bool)
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall a b. (a -> b) -> a -> b
$ (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lessEq AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
         ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
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
greaterEq AParser st Token
-> ParsecT String (AnnoState st) Identity Bool
-> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ParsecT String (AnnoState st) Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
       String
number <- CharParser (AnnoState st) String
forall st. CharParser st String
getNumber CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. CharParser st ()
skipSmart
       (Bool, Int) -> ParsecT String (AnnoState st) Identity (Bool, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
lgb, Int -> String -> Int
value 10 String
number)
    (FormPrefix, Range) -> AParser st (FormPrefix, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
b MODALITY
modal Bool
lgb Int
val, Range
r)

-- | Modal formula parser
modalPrimFormulaParser :: AParser st EM_FORMULA
modalPrimFormulaParser :: AParser st EM_FORMULA
modalPrimFormulaParser = (ModDefn -> EM_FORMULA)
-> ParsecT String (AnnoState st) Identity ModDefn
-> AParser st EM_FORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModDefn -> EM_FORMULA
ModForm ParsecT String (AnnoState st) Identity ModDefn
forall st. AParser st ModDefn
modDefnParser AParser st EM_FORMULA
-> AParser st EM_FORMULA -> AParser st EM_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (f :: FormPrefix
f, r :: Range
r) <- AParser st (FormPrefix, Range)
forall st. AParser st (FormPrefix, Range)
prefixModifier
    FORMULA EM_FORMULA
em_formula <- AParser st (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
rekPrimParser
    EM_FORMULA -> AParser st EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> AParser st EM_FORMULA)
-> EM_FORMULA -> AParser st EM_FORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
PrefixForm FormPrefix
f FORMULA EM_FORMULA
em_formula Range
r

-- | Term modality parser
parsePrimModality :: AParser st MODALITY
parsePrimModality :: AParser st MODALITY
parsePrimModality =
  let fp :: AParser st (FORMULA EM_FORMULA)
fp = [String] -> AParser st (FORMULA EM_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula ([String] -> AParser st (FORMULA EM_FORMULA))
-> [String] -> AParser st (FORMULA EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ String
greaterS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ext_modal_reserved_words in do
          FORMULA EM_FORMULA
f <- GenParser Char (AnnoState st) (FORMULA EM_FORMULA)
-> GenParser Char (AnnoState st) (FORMULA EM_FORMULA)
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char (AnnoState st) (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
fp
          case FORMULA EM_FORMULA
f of
            Mixfix_formula t :: TERM EM_FORMULA
t -> 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 EM_FORMULA -> MODALITY
TermMod TERM EM_FORMULA
t
            _ -> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
asSeparator String
quMark CharParser (AnnoState st) Token
-> AParser st MODALITY -> AParser st MODALITY
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MODALITY -> AParser st MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA EM_FORMULA -> MODALITY
Guard FORMULA EM_FORMULA
f)
        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
<|> (CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT CharParser (AnnoState st) Token
-> AParser st MODALITY -> AParser st MODALITY
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st MODALITY
forall st. AParser st MODALITY
parseModality AParser st MODALITY
-> CharParser (AnnoState st) Token -> AParser st MODALITY
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT)
        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
<|> (FORMULA EM_FORMULA -> MODALITY)
-> GenParser Char (AnnoState st) (FORMULA EM_FORMULA)
-> AParser st MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FORMULA EM_FORMULA -> MODALITY
Guard GenParser Char (AnnoState st) (FORMULA EM_FORMULA)
forall st. AParser st (FORMULA EM_FORMULA)
fp -- fail if something was consumed in the first try
        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
<|> (Pos -> MODALITY)
-> ParsecT String (AnnoState st) Identity Pos
-> AParser st MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Token -> MODALITY
SimpleMod (Token -> MODALITY) -> (Pos -> Token) -> Pos -> MODALITY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Range -> Token
Token String
emptyS (Range -> Token) -> (Pos -> Range) -> Pos -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pos] -> Range
Range ([Pos] -> Range) -> (Pos -> [Pos]) -> Pos -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pos -> [Pos] -> [Pos]
forall a. a -> [a] -> [a]
: [])) ParsecT String (AnnoState st) Identity Pos
forall tok st. GenParser tok st Pos
getPos

parseTransClosModality :: AParser st MODALITY
parseTransClosModality :: AParser st MODALITY
parseTransClosModality = do
  MODALITY
t <- AParser st MODALITY
forall st. AParser st MODALITY
parsePrimModality
  [Token]
mt <- ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String (AnnoState st) Identity Token
 -> ParsecT String (AnnoState st) Identity [Token])
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity [Token]
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
tmTransClosS
  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
$ if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
mt then MODALITY
t else MODALITY -> MODALITY
TransClos MODALITY
t

parseCompModality :: AParser st MODALITY
parseCompModality :: AParser st MODALITY
parseCompModality = ModOp -> AParser st MODALITY -> AParser st MODALITY
forall st. ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality ModOp
Composition AParser st MODALITY
forall st. AParser st MODALITY
parseTransClosModality

parseInterModality :: AParser st MODALITY
parseInterModality :: AParser st MODALITY
parseInterModality = ModOp -> AParser st MODALITY -> AParser st MODALITY
forall st. ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality ModOp
Intersection AParser st MODALITY
forall st. AParser st MODALITY
parseCompModality

parseUnionModality :: AParser st MODALITY
parseUnionModality :: AParser st MODALITY
parseUnionModality = ModOp -> AParser st MODALITY -> AParser st MODALITY
forall st. ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality ModOp
Union AParser st MODALITY
forall st. AParser st MODALITY
parseInterModality

parseBinModality :: ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality :: ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality c :: ModOp
c p :: AParser st MODALITY
p = do
  MODALITY
t1 <- AParser st MODALITY
p
  MODALITY -> AParser st MODALITY -> AParser st MODALITY
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option MODALITY
t1 (AParser st MODALITY -> AParser st MODALITY)
-> AParser st MODALITY -> AParser st MODALITY
forall a b. (a -> b) -> a -> b
$ do
    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
$ ModOp -> String
forall a. Show a => a -> String
show ModOp
c
    MODALITY
t2 <- ModOp -> AParser st MODALITY -> AParser st MODALITY
forall st. ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality ModOp
c AParser st MODALITY
p
    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
$ ModOp -> MODALITY -> MODALITY -> MODALITY
ModOp ModOp
c MODALITY
t1 MODALITY
t2

-- | orElse binds weakest
parseModality :: AParser st MODALITY
parseModality :: AParser st MODALITY
parseModality = ModOp -> AParser st MODALITY -> AParser st MODALITY
forall st. ModOp -> AParser st MODALITY -> AParser st MODALITY
parseBinModality ModOp
OrElse AParser st MODALITY
forall st. AParser st MODALITY
parseUnionModality

instance TermParser EM_FORMULA where
    termParser :: Bool -> AParser st EM_FORMULA
termParser = AParser st EM_FORMULA -> Bool -> AParser st EM_FORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st EM_FORMULA
forall st. AParser st EM_FORMULA
modalFormulaParser

-- Signature parser

rigor :: AParser st Bool
rigor :: AParser st Bool
rigor = (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
rigidS AParser st Token -> AParser st Bool -> AParser st Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AParser st Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
        AParser st Bool -> AParser st Bool -> AParser st Bool
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 Bool -> AParser st Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AParser st Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

sigItemParser :: AParser st EM_SIG_ITEM
sigItemParser :: AParser st EM_SIG_ITEM
sigItemParser = do
  Bool
rig <- AParser st Bool
forall st. AParser st Bool
rigor
  [String]
-> String
-> ([String] -> AParser st (OP_ITEM EM_FORMULA))
-> ([Annoted (OP_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM)
-> AParser st EM_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ext_modal_reserved_words String
opS [String] -> AParser st (OP_ITEM EM_FORMULA)
forall f st. TermParser f => [String] -> AParser st (OP_ITEM f)
opItem (Bool -> [Annoted (OP_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM
Rigid_op_items Bool
rig)
    AParser st EM_SIG_ITEM
-> AParser st EM_SIG_ITEM -> AParser st EM_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 EM_FORMULA))
-> ([Annoted (PRED_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM)
-> AParser st EM_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ext_modal_reserved_words String
predS [String] -> AParser st (PRED_ITEM EM_FORMULA)
forall f st. TermParser f => [String] -> AParser st (PRED_ITEM f)
predItem (Bool -> [Annoted (PRED_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM
Rigid_pred_items Bool
rig)

instance AParsable EM_SIG_ITEM where
        aparser :: AParser st EM_SIG_ITEM
aparser = AParser st EM_SIG_ITEM
forall st. AParser st EM_SIG_ITEM
sigItemParser

-- Basic item parser

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

nKey :: AParser st Token
nKey :: AParser st Token
nKey = 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
nominalS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS)

modDefnParser :: AParser st ModDefn
modDefnParser :: AParser st ModDefn
modDefnParser = do
    Maybe Token
mtime <- ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
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 Token
 -> ParsecT String (AnnoState st) Identity (Maybe Token))
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
timeS
    Maybe Token
mterm <- ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
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 Token
 -> ParsecT String (AnnoState st) Identity (Maybe Token))
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
termS
    Token
k <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
mKey
    (ids :: [Annoted Id]
ids, ks :: [Token]
ks) <- GenParser Char (AnnoState st) (Annoted Id)
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) ([Annoted Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy
      (AParser st Id -> GenParser Char (AnnoState st) (Annoted Id)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st Id -> GenParser Char (AnnoState st) (Annoted Id))
-> AParser st Id -> GenParser Char (AnnoState st) (Annoted Id)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ext_modal_reserved_words) ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
anSemiOrComma
    ([Annoted FrameForm] -> Range -> ModDefn)
-> Range -> AParser st ModDefn
forall a st.
([Annoted FrameForm] -> Range -> a) -> Range -> AParser st a
parseAxioms (Bool
-> Bool -> [Annoted Id] -> [Annoted FrameForm] -> Range -> ModDefn
ModDefn (Maybe Token -> Bool
forall a. Maybe a -> Bool
isJust Maybe Token
mtime) (Maybe Token -> Bool
forall a. Maybe a -> Bool
isJust Maybe Token
mterm) [Annoted Id]
ids)
                           (Range -> AParser st ModDefn) -> Range -> AParser st ModDefn
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
k Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ks

basicItemParser :: AParser st EM_BASIC_ITEM
basicItemParser :: AParser st EM_BASIC_ITEM
basicItemParser = (ModDefn -> EM_BASIC_ITEM)
-> ParsecT String (AnnoState st) Identity ModDefn
-> AParser st EM_BASIC_ITEM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModDefn -> EM_BASIC_ITEM
ModItem ParsecT String (AnnoState st) Identity ModDefn
forall st. AParser st ModDefn
modDefnParser AParser st EM_BASIC_ITEM
-> AParser st EM_BASIC_ITEM -> AParser st EM_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
k <- AParser st Token
forall st. AParser st Token
nKey
    (annoId :: [Annoted Token]
annoId, ks :: [Token]
ks) <- GenParser Char (AnnoState st) (Annoted Token)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted Token], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (AParser st Token -> GenParser Char (AnnoState st) (Annoted Token)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser AParser st Token
forall st. CharParser st Token
simpleId) AParser st Token
forall st. AParser st Token
anSemiOrComma
    EM_BASIC_ITEM -> AParser st EM_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_BASIC_ITEM -> AParser st EM_BASIC_ITEM)
-> EM_BASIC_ITEM -> AParser st EM_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted Token] -> Range -> EM_BASIC_ITEM
Nominal_decl [Annoted Token]
annoId (Range -> EM_BASIC_ITEM) -> Range -> EM_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
k Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ks

parseAxioms :: ([Annoted FrameForm] -> Range -> a) -> Range -> AParser st a
parseAxioms :: ([Annoted FrameForm] -> Range -> a) -> Range -> AParser st a
parseAxioms mki :: [Annoted FrameForm] -> Range -> a
mki pos :: Range
pos =
         do Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT
            [Annoted FrameForm]
someAxioms <- AParser st FrameForm -> AParser st [Annoted FrameForm]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser AParser st FrameForm
forall st. AParser st FrameForm
parseFrames
            Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
            a -> AParser st a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> AParser st a) -> a -> AParser st a
forall a b. (a -> b) -> a -> b
$ [Annoted FrameForm] -> Range -> a
mki [Annoted FrameForm]
someAxioms
              (Range -> a) -> Range -> a
forall a b. (a -> b) -> a -> b
$ Range
pos Range -> Range -> Range
`appRange` Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c
         AParser st a -> AParser st a -> AParser st a
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> a -> AParser st a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted FrameForm] -> Range -> a
mki [] Range
pos)

parseFrames :: AParser st FrameForm
parseFrames :: AParser st FrameForm
parseFrames = do
    Token
v <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
varS
    (vs :: [VAR_DECL]
vs, ps :: [Token]
ps) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varItems [String]
ext_modal_reserved_words
    FrameForm -> AParser st FrameForm
forall (m :: * -> *) a. Monad m => a -> m a
return (FrameForm -> AParser st FrameForm)
-> FrameForm -> AParser st FrameForm
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs [] (Range -> FrameForm) -> Range -> FrameForm
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
v Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
  AParser st FrameForm
-> AParser st FrameForm -> AParser st FrameForm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
f <- CharParser (AnnoState st) Token
forall st. AParser st Token
forallT
    (vs :: [VAR_DECL]
vs, ps :: [Token]
ps) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varDecls [String]
ext_modal_reserved_words
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
forall st.
[Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
emDotFormulae [Annotation]
a [VAR_DECL]
vs (Range -> AParser st FrameForm) -> Range -> AParser st FrameForm
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
f Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
  AParser st FrameForm
-> AParser st FrameForm -> AParser st FrameForm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
forall st.
[Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
emDotFormulae [] [] Range
nullRange

axiomsToFrames :: [Annotation] -> [VAR_DECL] -> Range
  -> BASIC_ITEMS () () EM_FORMULA -> FrameForm
axiomsToFrames :: [Annotation]
-> [VAR_DECL] -> Range -> BASIC_ITEMS () () EM_FORMULA -> FrameForm
axiomsToFrames a :: [Annotation]
a vs :: [VAR_DECL]
vs posl :: Range
posl ais :: BASIC_ITEMS () () EM_FORMULA
ais = case BASIC_ITEMS () () EM_FORMULA
ais of
  Axiom_items (Annoted ft :: FORMULA EM_FORMULA
ft qs :: Range
qs as :: [Annotation]
as rs :: [Annotation]
rs : fs :: [Annoted (FORMULA EM_FORMULA)]
fs) ds :: Range
ds ->
         let aft :: Annoted (FORMULA EM_FORMULA)
aft = FORMULA EM_FORMULA
-> Range
-> [Annotation]
-> [Annotation]
-> Annoted (FORMULA EM_FORMULA)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FORMULA EM_FORMULA
ft Range
qs ([Annotation]
a [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
as) [Annotation]
rs
         in [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs (Annoted (FORMULA EM_FORMULA)
aft Annoted (FORMULA EM_FORMULA)
-> [Annoted (FORMULA EM_FORMULA)] -> [Annoted (FORMULA EM_FORMULA)]
forall a. a -> [a] -> [a]
: [Annoted (FORMULA EM_FORMULA)]
fs) (Range
posl Range -> Range -> Range
`appRange` Range
ds)
  _ -> String -> FrameForm
forall a. HasCallStack => String -> a
error "axiomsToFrames"

emDotFormulae :: [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
emDotFormulae :: [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm
emDotFormulae a :: [Annotation]
a v :: [VAR_DECL]
v p :: Range
p = (BASIC_ITEMS () () EM_FORMULA -> FrameForm)
-> ParsecT
     String (AnnoState st) Identity (BASIC_ITEMS () () EM_FORMULA)
-> AParser st FrameForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Annotation]
-> [VAR_DECL] -> Range -> BASIC_ITEMS () () EM_FORMULA -> FrameForm
axiomsToFrames [Annotation]
a [VAR_DECL]
v Range
p)
  (ParsecT
   String (AnnoState st) Identity (BASIC_ITEMS () () EM_FORMULA)
 -> AParser st FrameForm)
-> ParsecT
     String (AnnoState st) Identity (BASIC_ITEMS () () EM_FORMULA)
-> AParser st FrameForm
forall a b. (a -> b) -> a -> b
$ Bool
-> [String]
-> ParsecT
     String (AnnoState st) Identity (BASIC_ITEMS () () EM_FORMULA)
forall b s f st.
(AParsable b, AParsable s, TermParser f) =>
Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae Bool
False [String]
ext_modal_reserved_words

instance AParsable EM_BASIC_ITEM where
        aparser :: AParser st EM_BASIC_ITEM
aparser = AParser st EM_BASIC_ITEM
forall st. AParser st EM_BASIC_ITEM
basicItemParser