hets/Hybrid/AS_Hybrid.hs

	AS_Hybrid.hs revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a
{- |
Module      :  $Header$
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

-- 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

data RIGOR = Rigid | Flexible deriving Show

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

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

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

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 (Eq, Ord, Show)

-- Generated by DrIFT, look but don't touch!

instance GetRange H_BASIC_ITEM where
  getRange x = case x of
    Simple_mod_decl _ _ p -> p
    Term_mod_decl _ _ p -> p
    Simple_nom_decl _ _ p -> p
  rangeSpan x = case x of
    Simple_mod_decl a b c -> joinRanges [rangeSpan a, rangeSpan b,
                                         rangeSpan c]
    Term_mod_decl a b c -> joinRanges [rangeSpan a, rangeSpan b,
                                       rangeSpan c]
    Simple_nom_decl a b c -> joinRanges [rangeSpan a, rangeSpan b,
                                         rangeSpan c]

instance GetRange RIGOR where
  getRange = const nullRange
  rangeSpan x = case x of
    Rigid -> []
    Flexible -> []

instance GetRange H_SIG_ITEM where
  getRange x = case x of
    Rigid_op_items _ _ p -> p
    Rigid_pred_items _ _ p -> p
  rangeSpan x = case x of
    Rigid_op_items a b c -> joinRanges [rangeSpan a, rangeSpan b,
                                        rangeSpan c]
    Rigid_pred_items a b c -> joinRanges [rangeSpan a, rangeSpan b,
                                          rangeSpan c]

instance GetRange MODALITY where
  getRange = const nullRange
  rangeSpan x = case x of
    Simple_mod a -> joinRanges [rangeSpan a]
    Term_mod a -> joinRanges [rangeSpan a]

instance GetRange NOMINAL where
  getRange = const nullRange
  rangeSpan x = case x of
    Simple_nom a -> joinRanges [rangeSpan a]

instance GetRange H_FORMULA where
  getRange x = case x of
    At _ _ p -> p
    BoxOrDiamond _ _ _ p -> p
    Here _ p -> p
    Univ _ _ p -> p
    Exist _ _ p -> p
  rangeSpan x = case x of
    At a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c]
    BoxOrDiamond a b c d -> joinRanges [rangeSpan a, rangeSpan b,
                                        rangeSpan c, rangeSpan d]
    Here a b -> joinRanges [rangeSpan a, rangeSpan b]
    Univ a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c]
    Exist a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c]