hets/Hybrid/AS_Hybrid.der.hs

	AS_Hybrid.der.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Hybrid/AS_Hybrid.der.hs
Copyright   :  (c) T.Mossakowski, W.Herding, C.Maeder, Uni Bremen 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt

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

Abstract syntax for hybrid logic extension of CASL
Only the added syntax is specified
-}

module Hybrid.AS_Hybrid where

import Common.Id
import Common.AS_Annotation

import CASL.AS_Basic_CASL

import Data.Data

-- DrIFT command
{-! global: GetRange !-}

type H_BASIC_SPEC = BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA

type AnHybFORM = Annoted (FORMULA H_FORMULA)

data H_BASIC_ITEM = Simple_mod_decl [Annoted SIMPLE_ID] [AnHybFORM] Range
                  | Term_mod_decl [Annoted SORT] [AnHybFORM] Range
                  | Simple_nom_decl [Annoted SIMPLE_ID] [AnHybFORM] Range
                    deriving (Show, Typeable, Data)

data RIGOR = Rigid | Flexible deriving (Show, Typeable, Data)

data H_SIG_ITEM =
          Rigid_op_items RIGOR [Annoted (OP_ITEM H_FORMULA)] Range
                 -- pos: op, semi colons
        | Rigid_pred_items RIGOR [Annoted (PRED_ITEM H_FORMULA)] Range
                 -- pos: pred, semi colons
             deriving (Show, Typeable, Data)

data MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM H_FORMULA)
             deriving (Show, Eq, Ord, Typeable, Data)

data NOMINAL = Simple_nom SIMPLE_ID
        deriving (Show, Eq, Ord, Typeable, Data)

data H_FORMULA = At NOMINAL (FORMULA H_FORMULA) Range
                | BoxOrDiamond Bool MODALITY (FORMULA H_FORMULA) Range
                | Here NOMINAL Range
                | Univ NOMINAL (FORMULA H_FORMULA) Range
                | Exist NOMINAL (FORMULA H_FORMULA) Range
             deriving (Show, Eq, Ord, Typeable, Data)