content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CoCASL/AS_CoCASL.der.hs
  Description :  Abstract syntax for CoCASL
  Copyright   :  (c) T.Mossakowski, C.Maeder, Uni Bremen 2004-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  hausmann@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Abstract syntax for CoCASL, the coalgebraic extension of CASL
    Only the added syntax is specified
  -}
  
  module CoCASL.AS_CoCASL where
  
  import Common.Id
  import Common.AS_Annotation
  
  import CASL.AS_Basic_CASL
  
  import Data.Data
  
  -- DrIFT command
  {-! global: GetRange !-}
  
  type C_BASIC_SPEC = BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA
  
  type AnModFORM = Annoted (FORMULA C_FORMULA)
  
  data C_BASIC_ITEM = CoFree_datatype [Annoted CODATATYPE_DECL] Range
                     -- pos: free, type, semi colons
                    | CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] Range
                     -- pos: generated, opt. braces
                    deriving (Show, Typeable, Data)
  
  data C_SIG_ITEM = CoDatatype_items [Annoted CODATATYPE_DECL] Range
                   -- type, semi colons
                    deriving (Show, Typeable, Data)
  
  data CODATATYPE_DECL = CoDatatype_decl SORT [Annoted COALTERNATIVE] Range
                       -- pos: "::=", "|"s
                         deriving (Show, Typeable, Data)
  
  data COALTERNATIVE = Co_construct OpKind (Maybe OP_NAME) [COCOMPONENTS] Range
                     -- True if Total, pos: "(", semi colons, ")"
                   | CoSubsorts [SORT] Range
                     -- pos: sort, commas
                    deriving (Show, Typeable, Data)
  
  data COCOMPONENTS = CoSelect [OP_NAME] OP_TYPE Range
                    -- pos: commas, colon
                    deriving (Show, Typeable, Data)
  
  data MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM C_FORMULA)
               deriving (Show, Eq, Ord, Typeable, Data)
  
  data C_FORMULA = BoxOrDiamond Bool MODALITY (FORMULA C_FORMULA) Range
                 {- The identifier and the term specify the kind of the modality
                 pos: "[]" or  "<>", True if Box, False if Diamond -}
                 | CoSort_gen_ax [SORT] [OP_SYMB] Bool
                 -- flag: belongs to a cofree type and hence is cofreeness axiom?
               deriving (Show, Eq, Ord, Typeable, Data)
  