content: {-# 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)
  