{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./COL/COLSign.hs
Description :  Signatures of COL as extension of CASL signatures
Copyright   :  (c) Till Mossakowski, C. Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

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

Signatures of COL as extension of CASL signatures.
-}

module COL.COLSign where

import Data.Data
import qualified Data.Set as Set
import qualified Data.Map as Map

import Common.Id

data COLSign = COLSign { COLSign -> Set Id
constructors :: Set.Set Id
                       , COLSign -> Map Id Int
observers :: Map.Map Id Int
                       } deriving (Int -> COLSign -> ShowS
[COLSign] -> ShowS
COLSign -> String
(Int -> COLSign -> ShowS)
-> (COLSign -> String) -> ([COLSign] -> ShowS) -> Show COLSign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [COLSign] -> ShowS
$cshowList :: [COLSign] -> ShowS
show :: COLSign -> String
$cshow :: COLSign -> String
showsPrec :: Int -> COLSign -> ShowS
$cshowsPrec :: Int -> COLSign -> ShowS
Show, COLSign -> COLSign -> Bool
(COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> Bool) -> Eq COLSign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: COLSign -> COLSign -> Bool
$c/= :: COLSign -> COLSign -> Bool
== :: COLSign -> COLSign -> Bool
$c== :: COLSign -> COLSign -> Bool
Eq, Eq COLSign
Eq COLSign =>
(COLSign -> COLSign -> Ordering)
-> (COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> COLSign)
-> (COLSign -> COLSign -> COLSign)
-> Ord COLSign
COLSign -> COLSign -> Bool
COLSign -> COLSign -> Ordering
COLSign -> COLSign -> COLSign
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: COLSign -> COLSign -> COLSign
$cmin :: COLSign -> COLSign -> COLSign
max :: COLSign -> COLSign -> COLSign
$cmax :: COLSign -> COLSign -> COLSign
>= :: COLSign -> COLSign -> Bool
$c>= :: COLSign -> COLSign -> Bool
> :: COLSign -> COLSign -> Bool
$c> :: COLSign -> COLSign -> Bool
<= :: COLSign -> COLSign -> Bool
$c<= :: COLSign -> COLSign -> Bool
< :: COLSign -> COLSign -> Bool
$c< :: COLSign -> COLSign -> Bool
compare :: COLSign -> COLSign -> Ordering
$ccompare :: COLSign -> COLSign -> Ordering
$cp1Ord :: Eq COLSign
Ord, Typeable, Typeable COLSign
Constr
DataType
Typeable COLSign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> COLSign -> c COLSign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c COLSign)
-> (COLSign -> Constr)
-> (COLSign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c COLSign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COLSign))
-> ((forall b. Data b => b -> b) -> COLSign -> COLSign)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> COLSign -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> COLSign -> r)
-> (forall u. (forall d. Data d => d -> u) -> COLSign -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> COLSign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> COLSign -> m COLSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> COLSign -> m COLSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> COLSign -> m COLSign)
-> Data COLSign
COLSign -> Constr
COLSign -> DataType
(forall b. Data b => b -> b) -> COLSign -> COLSign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> COLSign -> c COLSign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c COLSign
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> COLSign -> u
forall u. (forall d. Data d => d -> u) -> COLSign -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> COLSign -> m COLSign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> COLSign -> m COLSign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c COLSign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> COLSign -> c COLSign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c COLSign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COLSign)
$cCOLSign :: Constr
$tCOLSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> COLSign -> m COLSign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> COLSign -> m COLSign
gmapMp :: (forall d. Data d => d -> m d) -> COLSign -> m COLSign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> COLSign -> m COLSign
gmapM :: (forall d. Data d => d -> m d) -> COLSign -> m COLSign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> COLSign -> m COLSign
gmapQi :: Int -> (forall d. Data d => d -> u) -> COLSign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> COLSign -> u
gmapQ :: (forall d. Data d => d -> u) -> COLSign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> COLSign -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> COLSign -> r
gmapT :: (forall b. Data b => b -> b) -> COLSign -> COLSign
$cgmapT :: (forall b. Data b => b -> b) -> COLSign -> COLSign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COLSign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COLSign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c COLSign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c COLSign)
dataTypeOf :: COLSign -> DataType
$cdataTypeOf :: COLSign -> DataType
toConstr :: COLSign -> Constr
$ctoConstr :: COLSign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c COLSign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c COLSign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> COLSign -> c COLSign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> COLSign -> c COLSign
$cp1Data :: Typeable COLSign
Data)

emptyCOLSign :: COLSign
emptyCOLSign :: COLSign
emptyCOLSign = Set Id -> Map Id Int -> COLSign
COLSign Set Id
forall a. Set a
Set.empty Map Id Int
forall k a. Map k a
Map.empty

addCOLSign :: COLSign -> COLSign -> COLSign
addCOLSign :: COLSign -> COLSign -> COLSign
addCOLSign s1 :: COLSign
s1 s2 :: COLSign
s2 =
    COLSign
s1 { constructors :: Set Id
constructors = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (COLSign -> Set Id
constructors COLSign
s1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ COLSign -> Set Id
constructors COLSign
s2
       , observers :: Map Id Int
observers = Map Id Int -> Map Id Int -> Map Id Int
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (COLSign -> Map Id Int
observers COLSign
s1) (Map Id Int -> Map Id Int) -> Map Id Int -> Map Id Int
forall a b. (a -> b) -> a -> b
$ COLSign -> Map Id Int
observers COLSign
s2 }

diffCOLSign :: COLSign -> COLSign -> COLSign
diffCOLSign :: COLSign -> COLSign -> COLSign
diffCOLSign s1 :: COLSign
s1 s2 :: COLSign
s2 =
    COLSign
s1 { constructors :: Set Id
constructors = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (COLSign -> Set Id
constructors COLSign
s1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ COLSign -> Set Id
constructors COLSign
s2
       , observers :: Map Id Int
observers = Map Id Int -> Map Id Int -> Map Id Int
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (COLSign -> Map Id Int
observers COLSign
s1) (Map Id Int -> Map Id Int) -> Map Id Int -> Map Id Int
forall a b. (a -> b) -> a -> b
$ COLSign -> Map Id Int
observers COLSign
s2 }

isSubCOLSign :: COLSign -> COLSign -> Bool
isSubCOLSign :: COLSign -> COLSign -> Bool
isSubCOLSign s1 :: COLSign
s1 s2 :: COLSign
s2 =
    Set Id -> Bool
forall a. Set a -> Bool
Set.null (COLSign -> Set Id
constructors COLSign
s2 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ COLSign -> Set Id
constructors COLSign
s1)
    Bool -> Bool -> Bool
&& Map Id Int -> Bool
forall k a. Map k a -> Bool
Map.null (COLSign -> Map Id Int
observers COLSign
s2 Map Id Int -> Map Id Int -> Map Id Int
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ COLSign -> Map Id Int
observers COLSign
s1)