{- |
Module      :  $Header$
Copyright   :  (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Parser for modal logic extension of CASL
-}

module Hybrid.Parse_AS where

import CASL.Formula
import CASL.OpItem

import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Token
import Hybrid.AS_Hybrid
import Hybrid.Keywords
import Text.ParserCombinators.Parsec

hybrid_reserved_words :: [String]
hybrid_reserved_words = [
        diamondS,
        termS,
        rigidS,
        flexibleS,
        modalityS,
        modalitiesS,
        nominalS,
        nominalsS]

hybridFormula :: AParser st H_FORMULA
hybridFormula =
        do
        a <- asKey hereP
        n <- nominal
        return (Here n $ toRange a [] a)
        <|>
        do
        a <- asKey asP
        n <- nominal
        f <- primFormula hybrid_reserved_words
        return (At n f $ toRange a [] a)
        <|>
        do
        a <- asKey exMark
        n <- nominal
        f <- primFormula hybrid_reserved_words
        return (Univ n f $ toRange a [] a)
        <|>
        do
        a <- asKey "?"
        n <- nominal
        f <- primFormula hybrid_reserved_words
        return (Exist n f $ toRange a [] a)
        <|>
        do
        o <- oBracketT
        m <- modality []
        c <- cBracketT
        f <- primFormula hybrid_reserved_words
        return (BoxOrDiamond True m f $ toRange o [] c)
        <|>
        do
        o <- asKey lessS
        m <- modality [greaterS] -- do not consume matching ">"!
        c <- asKey greaterS
        f <- primFormula hybrid_reserved_words
        return (BoxOrDiamond False m f $ toRange o [] c)

nominal :: AParser st NOMINAL
nominal =
        do
        n <- simpleId
        return (Simple_nom n)

modality :: [String] -> AParser st MODALITY
modality ks =
    do t <- term (ks ++ hybrid_reserved_words)
       return $ Term_mod t


instance TermParser H_FORMULA where
    termParser = aToTermParser hybridFormula

rigor :: AParser st RIGOR
rigor = (asKey rigidS >> return Rigid)
        <|> (asKey flexibleS >> return Flexible)

rigidSigItems :: AParser st H_SIG_ITEM
rigidSigItems =
    do r <- rigor
       itemList hybrid_reserved_words opS opItem (Rigid_op_items r)
         <|> itemList hybrid_reserved_words predS predItem (Rigid_pred_items r)

instance AParsable H_SIG_ITEM where
  aparser = rigidSigItems

hKey :: AParser st Token
hKey = asKey modalityS <|> asKey modalitiesS

hKey' :: AParser st Token
hKey' = asKey nominalS <|> asKey nominalsS

hBasic :: AParser st H_BASIC_ITEM
hBasic =
    do (as, fs, ps) <- hItem'' hKey simpleId
       return (Simple_mod_decl as fs ps)
    <|>
    do (as, fs, ps) <- hItem'' hKey' simpleId
       return (Simple_nom_decl as fs ps)

hItem'' :: AParser st Token -> AParser st a ->
           AParser st ([Annoted a], [AnHybFORM], Range)
hItem'' k pr = do
        c <- k
        (as, cs) <- separatedBy (annoParser pr) anSemiOrComma
        let ps = catRange $ c : cs
        return (as, [], ps)

instance AParsable H_BASIC_ITEM where
  aparser = hBasic
