3853N/A{- |

3853N/AModule : $Header$

3853N/ADescription : Parser for extended modal logic

3853N/ACopyright : DFKI GmbH 2009

3853N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3853N/A

3853N/AMaintainer : Christian.Maeder@dfki.de

3853N/AStability : experimental

3853N/APortability : portable

3853N/A

3853N/A-}

3853N/A

3853N/Amodule ExtModal.Parse_AS (ext_modal_reserved_words) where

3853N/A

3853N/Aimport Text.ParserCombinators.Parsec

3853N/A

3853N/Aimport Common.AS_Annotation

3853N/Aimport Common.Id

3853N/Aimport Common.Parsec

3853N/Aimport Common.Token

3853N/Aimport Common.Lexer

3853N/Aimport Common.AnnoState

3853N/Aimport Common.Keywords

3853N/A

5035N/Aimport CASL.AS_Basic_CASL

3853N/Aimport CASL.Formula

3853N/Aimport CASL.OpItem

3853N/Aimport CASL.Parse_AS_Basic

3853N/A

3853N/Aimport ExtModal.AS_ExtModal

4803N/Aimport ExtModal.Keywords

3853N/A

3853N/Aimport Data.Maybe

3853N/A

4141N/A-- | List of reserved words

3853N/Aext_modal_reserved_words :: [String]

3853N/Aext_modal_reserved_words = map show [Intersection, Union] ++

3853N/A [ untilS

3853N/A , sinceS

3853N/A , allPathsS

4141N/A , somePathsS

3898N/A , nextS

3898N/A , yesterdayS

4920N/A , generallyS

4518N/A , eventuallyS

3853N/A , atS

3853N/A , quMark

3853N/A , hereS

3853N/A , timeS

4803N/A , nominalS

3853N/A , nominalS ++ sS

3853N/A , hithertoS

3853N/A , previouslyS

3853N/A , muS

3853N/A , nuS

3853N/A , diamondS

3853N/A , termS

3853N/A , rigidS

3853N/A , flexibleS

3853N/A , modalityS

3853N/A , modalitiesS ]

3853N/A

3853N/AboxParser :: AParser st (MODALITY, Bool, Range)

3853N/AboxParser = do

3853N/A open <- oBracketT

4803N/A modal <- parseModality

4803N/A close <- cBracketT

3853N/A return (modal, True, toRange open [] close)

3853N/A

3853N/AdiamondParser :: AParser st (MODALITY, Bool, Range)

3853N/AdiamondParser = do

3853N/A open <- asKey lessS

3853N/A modal <- parseModality

3853N/A close <- asKey greaterS

3853N/A return (modal, False, toRange open [] close)

4141N/A <|> do

4141N/A d <- asKey diamondS

4141N/A let p = tokPos d

4141N/A return (SimpleMod $ Token emptyS p, False, p)

4141N/A

4141N/ArekPrimParser :: AParser st (FORMULA EM_FORMULA)

4141N/ArekPrimParser = genPrimFormula modalPrimFormulaParser ext_modal_reserved_words

4141N/A

4141N/AinfixTok :: AParser st (Token, Bool)

4141N/AinfixTok = pair (asKey untilS) (return True)

4518N/A <|> pair (asKey sinceS) (return False)

4518N/A

4141N/A-- | Modal infix formula parser

4141N/AmodalFormulaParser :: AParser st EM_FORMULA

3853N/AmodalFormulaParser = do

3853N/A p1 <- modalPrimFormulaParser

4920N/A option p1 $ do

3853N/A (t, b) <- infixTok

4500N/A f2 <- rekPrimParser

4500N/A return $ UntilSince b (ExtFORMULA p1) f2 $ tokPos t

4500N/A <|> do

4500N/A (f1, (t, b)) <- try $ pair rekPrimParser infixTok

3853N/A f2 <- rekPrimParser

3853N/A return $ UntilSince b f1 f2 $ tokPos t

3853N/A

3853N/AprefixModifier :: AParser st (FORMULA EM_FORMULA -> EM_FORMULA)

3853N/AprefixModifier = let mkF f r = return $ flip f $ tokPos r in

3853N/A (asKey allPathsS >>= mkF (PathQuantification True))

3853N/A <|> (asKey somePathsS >>= mkF (PathQuantification False))

3853N/A <|> (asKey nextS >>= mkF (NextY True))

3853N/A <|> (asKey yesterdayS >>= mkF (NextY False))

3853N/A <|> (asKey generallyS >>= mkF (StateQuantification True True))

3853N/A <|> (asKey eventuallyS >>= mkF (StateQuantification True False))

3853N/A <|> (asKey hithertoS >>= mkF (StateQuantification False True))

3853N/A <|> (asKey previouslyS >>= mkF (StateQuantification False False))

3853N/A <|> do

3853N/A mnb <- (asKey muS >> return True)

3853N/A <|> (asKey nuS >> return False)

3853N/A z <- varId ext_modal_reserved_words

3853N/A dotT

3853N/A mkF (FixedPoint mnb z) z

3853N/A <|> do

3853N/A ahb <- (asKey atS >> return True)

3853N/A <|> (asKey hereS >> return False)

3853N/A nom <- simpleId

4500N/A mkF (Hybrid ahb nom) nom

4500N/A

4500N/A-- | Modal formula parser

4500N/AmodalPrimFormulaParser :: AParser st EM_FORMULA

3853N/AmodalPrimFormulaParser = fmap ModForm modDefnParser <|> do

3853N/A (modal, b, r) <- boxParser <|> diamondParser

3853N/A (lgb, val) <- option (False, 1) $ do

3853N/A lgb <- option False $ (asKey lessEq >> return True)

3853N/A <|> (asKey greaterEq >> return False)

3853N/A number <- getNumber << skipSmart

3853N/A return (lgb, value 10 number)

3853N/A em_formula <- rekPrimParser

3853N/A return $ BoxOrDiamond b modal lgb val em_formula r

3853N/A <|> do

3853N/A f <- prefixModifier

3853N/A em_formula <- rekPrimParser

3853N/A return $ f em_formula

3853N/A

3853N/A-- | Term modality parser

3853N/AparsePrimModality :: AParser st MODALITY

3853N/AparsePrimModality = do

3853N/A oParenT

3858N/A t <- parseModality

3853N/A cParenT

3853N/A return t

3853N/A <|> do

3853N/A f <- formula $ greaterS : ext_modal_reserved_words

3853N/A case f of

3853N/A Mixfix_formula t -> return $ TermMod t

3853N/A _ -> asSeparator quMark >> return (Guard f)

3853N/A <|> fmap (SimpleMod . Token emptyS . Range . (: [])) getPos

3858N/A

3853N/AparseTransClosModality :: AParser st MODALITY

3853N/AparseTransClosModality = do

3853N/A t <- parsePrimModality

3853N/A mt <- many $ asKey tmTransClosS

3853N/A return $ if null mt then t else TransClos t

3853N/A

3853N/AparseCompModality :: AParser st MODALITY

3853N/AparseCompModality = parseBinModality Composition parseTransClosModality

3853N/A

3853N/AparseInterModality :: AParser st MODALITY

3853N/AparseInterModality = parseBinModality Intersection parseCompModality

3853N/A

3853N/AparseBinModality :: ModOp -> AParser st MODALITY -> AParser st MODALITY

3853N/AparseBinModality c p = do

3853N/A t1 <- p

3853N/A option t1 $ do

3853N/A asKey $ show c

3853N/A t2 <- parseBinModality c p

3853N/A return $ ModOp c t1 t2

3853N/A

3853N/AparseModality :: AParser st MODALITY

3853N/AparseModality = parseBinModality Union parseInterModality

3853N/A

4060N/Ainstance TermParser EM_FORMULA where

4060N/A termParser = aToTermParser modalFormulaParser

4060N/A

4060N/A-- Signature parser

4060N/A

4803N/Arigor :: AParser st Bool

4060N/Arigor = (asKey rigidS >> return True)

4060N/A <|> (asKey flexibleS >> return False)

4060N/A

4060N/AsigItemParser :: AParser st EM_SIG_ITEM

4060N/AsigItemParser = do

4060N/A rig <- rigor

4060N/A itemList ext_modal_reserved_words opS opItem (Rigid_op_items rig)

4060N/A <|> itemList ext_modal_reserved_words predS predItem (Rigid_pred_items rig)

4060N/A

4060N/Ainstance AParsable EM_SIG_ITEM where

4803N/A aparser = sigItemParser

4060N/A

4060N/A-- Basic item parser

4060N/A

4060N/AmKey :: AParser st Token

4060N/AmKey = asKey modalityS <|> asKey modalitiesS

3853N/A

3853N/AnKey :: AParser st Token

3853N/AnKey = asKey nominalS <|> asKey (nominalS ++ sS)

4803N/A

3853N/AmodDefnParser :: AParser st ModDefn

3853N/AmodDefnParser = do

3853N/A mtime <- optionMaybe $ asKey timeS

3853N/A mterm <- optionMaybe $ asKey termS

3853N/A k <- mKey

3853N/A (ids, ks) <- separatedBy

3853N/A (annoParser $ sortId ext_modal_reserved_words) anSemiOrComma

3853N/A parseAxioms (ModDefn (isJust mtime) (isJust mterm) ids)

4803N/A $ catRange $ k : ks

3853N/A

3853N/AbasicItemParser :: AParser st EM_BASIC_ITEM

3853N/AbasicItemParser = fmap ModItem modDefnParser <|> do

3853N/A k <- nKey

3853N/A (annoId, ks) <- separatedBy (annoParser simpleId) anSemiOrComma

4803N/A return $ Nominal_decl annoId $ catRange $ k : ks

4803N/A

4803N/AparseAxioms :: ([FrameForm] -> Range -> a) -> Range -> AParser st a

4803N/AparseAxioms mki pos =

4803N/A do o <- oBraceT

4803N/A someAxioms <- many parseFrames

4803N/A c <- cBraceT

4803N/A return $ mki someAxioms

4803N/A $ pos `appRange` toRange o [] c

4803N/A <|> return (mki [] pos)

4803N/A

4803N/AparseFrames :: AParser st FrameForm

4803N/AparseFrames = do

4803N/A v <- pluralKeyword varS

4803N/A (vs, ps) <- varItems ext_modal_reserved_words

4803N/A return $ FrameForm vs [] $ catRange $ v : ps

4803N/A <|> do

4803N/A f <- forallT

4803N/A (vs, ps) <- varDecls ext_modal_reserved_words

4803N/A a <- annos

4803N/A emDotFormulae a vs $ catRange $ f : ps

4803N/A <|> emDotFormulae [] [] nullRange

4803N/A

4803N/AaxiomsToFrames :: [Annotation] -> [VAR_DECL] -> Range

4803N/A -> BASIC_ITEMS () () EM_FORMULA -> FrameForm

4803N/AaxiomsToFrames a vs posl ais = case ais of

4803N/A Axiom_items (Annoted ft qs as rs : fs) ds ->

4803N/A let aft = Annoted ft qs (a ++ as) rs

4803N/A in FrameForm vs (aft : fs) (posl `appRange` ds)

4803N/A _ -> error "axiomsToFrames"

4803N/A

4803N/AemDotFormulae :: [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm

4803N/AemDotFormulae a v p = fmap (axiomsToFrames a v p)

4803N/A $ dotFormulae ext_modal_reserved_words

4803N/A

4803N/Ainstance AParsable EM_BASIC_ITEM where

4803N/A aparser = basicItemParser

3853N/A