content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CoCASL/CoCASLSign.hs
  Description :  Signatures for CoCASL, as extension of CASL signatures
  Copyright   :  (c) Till Mossakowski, Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  hausmann@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Signatures for CoCASL, as extension of CASL signatures.
  -}
  
  module CoCASL.CoCASLSign where
  
  import CASL.Sign
  import CASL.AS_Basic_CASL (SORT)
  
  import qualified Common.Lib.Rel as Rel
  import qualified Common.Lib.MapSet as MapSet
  
  import Data.Data
  
  data CoCASLSign = CoCASLSign
    { sees :: Rel.Rel SORT
    , constructs :: Rel.Rel SORT
    , constructors :: OpMap
    } deriving (Show, Eq, Ord, Typeable, Data)
  
  emptyCoCASLSign :: CoCASLSign
  emptyCoCASLSign = CoCASLSign Rel.empty Rel.empty MapSet.empty
  
  closeConsRel :: CoCASLSign -> CoCASLSign
  closeConsRel s =
    s { constructs = Rel.transClosure $ constructs s
      , sees = Rel.transClosure $ sees s }
  
  addCoCASLSign :: CoCASLSign -> CoCASLSign -> CoCASLSign
  addCoCASLSign a b = closeConsRel a
    { sees = Rel.union (sees a) $ sees b
    , constructs = Rel.union (constructs a) $ constructs b
    , constructors = addOpMapSet (constructors a) $ constructors b }
  
  interCoCASLSign :: CoCASLSign -> CoCASLSign -> CoCASLSign
  interCoCASLSign a b = closeConsRel a
    { sees = interRel (sees a) $ sees b
    , constructs = interRel (constructs a) $ constructs b
    , constructors = interOpMapSet (constructors a) $ constructors b }
  
  diffCoCASLSign :: CoCASLSign -> CoCASLSign -> CoCASLSign
  diffCoCASLSign a b = closeConsRel a
    { sees = Rel.difference (sees a) $ sees b
    , constructs = Rel.difference (constructs a) $ constructs b
    , constructors = diffOpMapSet (constructors a) $ constructors b }
  
  isSubCoCASLSign :: CoCASLSign -> CoCASLSign -> Bool
  isSubCoCASLSign a b =
      Rel.isSubrelOf (sees a) (sees b)
      && Rel.isSubrelOf (constructs a) (constructs b)
      && isSubOpMap (constructors a) (constructors b)
  