{- |

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 = map show [Intersection, Union] ++

[ untilS

, sinceS

, allPathsS

, somePathsS

, nextS

, yesterdayS

, generallyS

, eventuallyS

, atS

, quMark

, hereS

, timeS

, nominalS

, nominalS ++ sS

, hithertoS

, previouslyS

, muS

, nuS

, diamondS

, orElseS

, oB

, cB

, termS

, rigidS

, flexibleS

, modalityS

, modalitiesS ]

boxParser :: AParser st (MODALITY, BoxOp, Range)

boxParser = do

let asESep = pToken . tryString

open <- oBracketT <|> asESep oB

let isBox = tokStr open == "["

modal <- parseModality

close <- if isBox then cBracketT else asESep cB

return (modal, if isBox then Box else EBox, toRange open [] close)

diamondParser :: AParser st (MODALITY, BoxOp, Range)

diamondParser = do

open <- asKey lessS

modal <- parseModality

close <- asKey greaterS

return (modal, Diamond, toRange open [] close)

<|> do

d <- asKey diamondS

let p = tokPos d

return (SimpleMod $ Token emptyS p, Diamond, p)

rekPrimParser :: AParser st (FORMULA EM_FORMULA)

rekPrimParser = genPrimFormula modalPrimFormulaParser ext_modal_reserved_words

infixTok :: AParser st (Token, Bool)

infixTok = pair (asKey untilS) (return True)

<|> pair (asKey sinceS) (return False)

-- | Modal infix formula parser

modalFormulaParser :: AParser st EM_FORMULA

modalFormulaParser = do

p1 <- modalPrimFormulaParser

option p1 $ do

(t, b) <- infixTok

f2 <- rekPrimParser

return $ UntilSince b (ExtFORMULA p1) f2 $ tokPos t

<|> do

(f1, (t, b)) <- try $ pair rekPrimParser infixTok

f2 <- rekPrimParser

return $ UntilSince b f1 f2 $ tokPos t

prefixModifier :: AParser st (FormPrefix, Range)

prefixModifier = let mkF f r = return (f, tokPos r) in

(asKey allPathsS >>= mkF (PathQuantification True))

<|> (asKey somePathsS >>= mkF (PathQuantification False))

<|> (asKey nextS >>= mkF (NextY True))

<|> (asKey yesterdayS >>= mkF (NextY False))

<|> (asKey generallyS >>= mkF (StateQuantification True True))

<|> (asKey eventuallyS >>= mkF (StateQuantification True False))

<|> (asKey hithertoS >>= mkF (StateQuantification False True))

<|> (asKey previouslyS >>= mkF (StateQuantification False False))

<|> do

mnb <- (asKey muS >> return True)

<|> (asKey nuS >> return False)

z <- varId ext_modal_reserved_words

dotT

mkF (FixedPoint mnb z) z

<|> do

ahb <- (asKey atS >> return True)

<|> (asKey hereS >> return False)

nom <- simpleId

mkF (Hybrid ahb nom) nom

<|> do

(modal, b, r) <- boxParser <|> diamondParser

(lgb, val) <- option (True, 1) $ do

lgb <- option False $ (asKey lessEq >> return False)

<|> (asKey greaterEq >> return True)

number <- getNumber << skipSmart

return (lgb, value 10 number)

return (BoxOrDiamond b modal lgb val, r)

-- | Modal formula parser

modalPrimFormulaParser :: AParser st EM_FORMULA

modalPrimFormulaParser = fmap ModForm modDefnParser <|> do

(f, r) <- prefixModifier

em_formula <- rekPrimParser

return $ PrefixForm f em_formula r

-- | Term modality parser

parsePrimModality :: AParser st MODALITY

parsePrimModality =

let fp = formula $ greaterS : ext_modal_reserved_words in do

f <- try fp

case f of

Mixfix_formula t -> return $ TermMod t

_ -> asSeparator quMark >> return (Guard f)

<|> (oParenT >> parseModality << cParenT)

<|> fmap Guard fp -- fail if something was consumed in the first try

<|> fmap (SimpleMod . Token emptyS . Range . (: [])) getPos

parseTransClosModality :: AParser st MODALITY

parseTransClosModality = do

t <- parsePrimModality

mt <- many $ asKey tmTransClosS

return $ if null mt then t else TransClos t

parseCompModality :: AParser st MODALITY

parseCompModality = parseBinModality Composition parseTransClosModality

parseInterModality :: AParser st MODALITY

parseInterModality = parseBinModality Intersection parseCompModality

parseUnionModality :: AParser st MODALITY

parseUnionModality = parseBinModality Union parseInterModality

parseBinModality :: ModOp -> AParser st MODALITY -> AParser st MODALITY

parseBinModality c p = do

t1 <- p

option t1 $ do

asKey $ show c

t2 <- parseBinModality c p

return $ ModOp c t1 t2

-- | orElse binds weakest

parseModality :: AParser st MODALITY

parseModality = parseBinModality OrElse parseUnionModality

instance TermParser EM_FORMULA where

termParser = aToTermParser modalFormulaParser

-- Signature parser

rigor :: AParser st Bool

rigor = (asKey rigidS >> return True)

<|> (asKey flexibleS >> return False)

sigItemParser :: AParser st EM_SIG_ITEM

sigItemParser = do

rig <- rigor

itemList ext_modal_reserved_words opS opItem (Rigid_op_items rig)

<|> itemList ext_modal_reserved_words predS predItem (Rigid_pred_items rig)

instance AParsable EM_SIG_ITEM where

aparser = sigItemParser

-- Basic item parser

mKey :: AParser st Token

mKey = asKey modalityS <|> asKey modalitiesS

nKey :: AParser st Token

nKey = asKey nominalS <|> asKey (nominalS ++ sS)

modDefnParser :: AParser st ModDefn

modDefnParser = do

mtime <- optionMaybe $ asKey timeS

mterm <- optionMaybe $ asKey termS

k <- mKey

(ids, ks) <- separatedBy

(annoParser $ sortId ext_modal_reserved_words) anSemiOrComma

parseAxioms (ModDefn (isJust mtime) (isJust mterm) ids)

$ catRange $ k : ks

basicItemParser :: AParser st EM_BASIC_ITEM

basicItemParser = fmap ModItem modDefnParser <|> do

k <- nKey

(annoId, ks) <- separatedBy (annoParser simpleId) anSemiOrComma

return $ Nominal_decl annoId $ catRange $ k : ks

parseAxioms :: ([Annoted FrameForm] -> Range -> a) -> Range -> AParser st a

parseAxioms mki pos =

do o <- oBraceT

someAxioms <- annosParser parseFrames

c <- cBraceT

return $ mki someAxioms

$ pos `appRange` toRange o [] c

<|> return (mki [] pos)

parseFrames :: AParser st FrameForm

parseFrames = do

v <- pluralKeyword varS

(vs, ps) <- varItems ext_modal_reserved_words

return $ FrameForm vs [] $ catRange $ v : ps

<|> do

f <- forallT

(vs, ps) <- varDecls ext_modal_reserved_words

a <- annos

emDotFormulae a vs $ catRange $ f : ps

<|> emDotFormulae [] [] nullRange

axiomsToFrames :: [Annotation] -> [VAR_DECL] -> Range

-> BASIC_ITEMS () () EM_FORMULA -> FrameForm

axiomsToFrames a vs posl ais = case ais of

Axiom_items (Annoted ft qs as rs : fs) ds ->

let aft = Annoted ft qs (a ++ as) rs

in FrameForm vs (aft : fs) (posl `appRange` ds)

_ -> error "axiomsToFrames"

emDotFormulae :: [Annotation] -> [VAR_DECL] -> Range -> AParser st FrameForm

emDotFormulae a v p = fmap (axiomsToFrames a v p)

$ dotFormulae False ext_modal_reserved_words

instance AParsable EM_BASIC_ITEM where

aparser = basicItemParser