SignCSP.hs revision e071fb22ea9923a2a4ff41184d80ca46b55ee932
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : CspCASL signatures
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : M.Roggenbach@swansea.ac.uk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskisignatures for CSP-CASL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- todo: implement isInclusion, computeExt
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Data.Map as Map
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskidata CSPAddSign = CSPAddSign { channelNames :: Map.Map Id SORT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , processNames :: Map.Map Id (Maybe SORT)}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Eq, Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype CSPSign = Sign () CSPAddSign
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederemptyCSPAddSign :: CSPAddSign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiemptyCSPAddSign = CSPAddSign { channelNames = Map.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , processNames = Map.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskidiffCSPAddSign :: CSPAddSign -> CSPAddSign -> CSPAddSign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskidiffCSPAddSign a b =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski a { channelNames = channelNames a `Map.difference` channelNames b,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski processNames = processNames a `Map.difference` processNames b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddCSPAddSign :: CSPAddSign -> CSPAddSign -> CSPAddSign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddCSPAddSign a b =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski a { channelNames = channelNames a `Map.union` channelNames b,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski processNames = processNames a `Map.union` processNames b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederemptyCSPSign :: CSPSign
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederemptyCSPSign = emptySign emptyCSPAddSign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisInclusion :: CSPAddSign -> CSPAddSign -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisInclusion _ _ = True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata CSPAddMorphism =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CSPAddMorphism { channelMap :: Map.Map Id Id
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , processMap :: Map.Map Id Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Eq, Show)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype CSPMorphism = Morphism () CSPAddSign CSPAddMorphism
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercomputeExt :: Ext () CSPAddSign CSPAddMorphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercomputeExt _ _ =
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski CSPAddMorphism { channelMap = Map.empty -- ???
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , processMap = Map.empty -- ???
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- dummy instances, need to be elaborated!
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty CSPAddSign where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty = text . show
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty CSPAddMorphism where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty = text . show