Parse_AS.hs

{- |
Module      :  $Header$
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