4632N/A{- |

4632N/AModule : $Header$

4632N/ACopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004

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

4632N/A

4632N/AMaintainer : luettich@tzi.de

4632N/AStability : provisional

4632N/APortability : portable

4632N/A

4632N/AAbstract syntax for modal logic extension of CASL

4632N/A Only the added syntax is specified

4632N/A-}

4632N/A

4632N/Amodule Modal.AS_Modal where

4632N/A

4632N/Aimport Common.Id

4632N/Aimport Common.AS_Annotation

4632N/Aimport CASL.AS_Basic_CASL

4632N/A

4632N/A-- DrIFT command

4632N/A{-! global: UpPos !-}

4632N/A

4632N/Atype M_BASIC_SPEC = BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA

4632N/A

type AnModFORM = Annoted (FORMULA M_FORMULA)

data M_BASIC_ITEM = Simple_mod_decl [Annoted SIMPLE_ID] [AnModFORM] [Pos]

| Term_mod_decl [Annoted SORT] [AnModFORM] [Pos]

deriving (Eq, Show)

data RIGOR = Rigid | Flexible deriving (Eq, Show)

data M_SIG_ITEM =

Rigid_op_items RIGOR [Annoted (OP_ITEM M_FORMULA)] [Pos]

-- pos: op, semi colons

| Rigid_pred_items RIGOR [Annoted (PRED_ITEM M_FORMULA)] [Pos]

-- pos: pred, semi colons

deriving (Eq, Show)

data MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM M_FORMULA)

deriving (Eq, Ord, Show)

data M_FORMULA = BoxOrDiamond Bool MODALITY (FORMULA M_FORMULA) [Pos]

-- The identifier and the term specify the kind of the modality

-- pos: "[]" or "<>", True if Box, False if Diamond

deriving (Eq, Ord, Show)

modalityS, modalitiesS, flexibleS, rigidS, termS, emptyS, diamondS, greaterS

:: String

modalityS = "modality"

modalitiesS = init modalityS ++ "ies"

flexibleS = "flexible"

rigidS = "rigid"

termS = "term"

emptyS = "empty"

diamondS = "<>"

greaterS = ">"

modal_reserved_words :: [String]

modal_reserved_words = diamondS:termS:rigidS:flexibleS:modalityS:[modalitiesS]