SignCSP.hs revision cdf1545bdcd39a9d53c00761ffa42e7b1174b91e
eb483f2216949400bfef8f6deb5320f071445626Christian MaederDescription : CspCASL signatures
eb483f2216949400bfef8f6deb5320f071445626Christian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
eb483f2216949400bfef8f6deb5320f071445626Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eb483f2216949400bfef8f6deb5320f071445626Christian MaederMaintainer : M.Roggenbach@swansea.ac.uk
eb483f2216949400bfef8f6deb5320f071445626Christian MaederStability : provisional
eb483f2216949400bfef8f6deb5320f071445626Christian MaederPortability : portable
eb483f2216949400bfef8f6deb5320f071445626Christian Maedersignatures for CSP-CASL
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- todo: implement isInclusion, computeExt
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Map as Map
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Set as S
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport CASL.Sign (emptySign, Sign, extendedInfo, sortRel)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport CASL.Morphism (Morphism)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Common.Doc as Doc
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Common.DocUtils as DocUtils
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Id (Id, SIMPLE_ID)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Lib.Rel (predecessors)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | A process has zero or more parameter sorts, and a communication
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata ProcProfile = ProcProfile [SORT] CommAlpha
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder deriving (Eq, Show)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | A process communication alphabet consists of a set of sort names
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- and typed channel names.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata TypedChanName = TypedChanName CHANNEL_NAME SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder deriving (Eq, Ord, Show)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata CommType = CommTypeSort SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | CommTypeChan TypedChanName
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder deriving (Eq, Ord)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Show CommType where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder show (CommTypeSort s) = show s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder show (CommTypeChan (TypedChanName c s)) = show (c, s)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype CommAlpha = S.Set CommType
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype ChanNameMap = Map.Map CHANNEL_NAME SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- Close a communication alphabet under CASL subsort
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercloseCspCommAlpha sig alpha =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder S.unions $ S.toList $ S.map (closeOneCspComm sig) alpha
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- Close one CommType under CASL subsort
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercloseOneCspComm sig x =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (CommTypeSort s) -> S.map CommTypeSort (subsorts s)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (CommTypeChan (TypedChanName c s)) -> (S.map CommTypeSort (subsorts s))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (S.map (mkTypedChan c) (subsorts s))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder where mkTypedChan c s = CommTypeChan $ TypedChanName c s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder subsorts s' = (S.singleton s') `S.union` predecessors (sortRel sig) s'
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder{- Will probably be useful, but doesn't appear to be right now.
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder-- Extract the sorts from a process alphabet
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprocAlphaSorts :: CommAlpha -> S.Set SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprocAlphaSorts a = stripMaybe $ S.map justSort a
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder where justSort n = case n of
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (CommTypeSort s) -> Just s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- Extract the typed channel names from a process alphabet
eb483f2216949400bfef8f6deb5320f071445626Christian MaederprocAlphaChans :: CommAlpha -> S.Set TypedChanName
eb483f2216949400bfef8f6deb5320f071445626Christian MaederprocAlphaChans a = stripMaybe $ S.map justChan a
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder where justChan n = case n of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (CommTypeChan c) -> Just c
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- Given a set of Maybes, filter to keep only the Justs
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederstripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a
eb483f2216949400bfef8f6deb5320f071445626Christian MaederstripMaybe x = S.fromList $ Maybe.catMaybes $ S.toList x
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- Close a set of sorts under a subsort relation
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercspSubsortCloseSorts :: CspCASLSign -> S.Set SORT -> S.Set SORT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercspSubsortCloseSorts sig sorts =
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski where subsort_sets = S.toList $ S.map (cspSubsortPreds sig) sorts
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski-- | CSP process signature.
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskidata CspSign = CspSign
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski { chans :: ChanNameMap
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski , procSet :: ProcNameMap
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski } deriving (Eq, Show)
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski-- | A CspCASL signature is a CASL signature with a CSP process
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- signature in the extendedInfo part.
eb483f2216949400bfef8f6deb5320f071445626Christian Maedertype CspCASLSign = Sign () CspSign
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till MossakowskiccSig2CASLSign :: CspCASLSign -> Sign () ()
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederccSig2CASLSign sigma = sigma { extendedInfo = () }
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | Empty CspCASL signature.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederemptyCspCASLSign :: CspCASLSign
eb483f2216949400bfef8f6deb5320f071445626Christian MaederemptyCspCASLSign = emptySign emptyCspSign
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | Empty CSP process signature.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederemptyCspSign :: CspSign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederemptyCspSign = CspSign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | Compute union of two CSP process signatures.
eb483f2216949400bfef8f6deb5320f071445626Christian MaederaddCspProcSig :: CspSign -> CspSign -> CspSign
eb483f2216949400bfef8f6deb5320f071445626Christian MaederaddCspProcSig a b =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder a { chans = chans a `Map.union` chans b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , procSet = procSet a `Map.union` procSet b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- XXX looks incomplete!
eb483f2216949400bfef8f6deb5320f071445626Christian MaederisInclusion :: CspSign -> CspSign -> Bool
eb483f2216949400bfef8f6deb5320f071445626Christian MaederisInclusion _ _ = True
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- XXX morphisms between CSP process signatures?
afbd86903151121381e4e9d22862136817d7f0f0Christian Maederdata CspAddMorphism = CspAddMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { channelMap :: Map.Map Id Id
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder , processMap :: Map.Map Id Id
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder } deriving (Eq, Show)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype CspMorphism = Morphism () CspSign CspAddMorphism
eb483f2216949400bfef8f6deb5320f071445626Christian MaederemptyCspAddMorphism :: CspAddMorphism
eb483f2216949400bfef8f6deb5320f071445626Christian MaederemptyCspAddMorphism = CspAddMorphism
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder { channelMap = Map.empty -- ???
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- dummy instances, need to be elaborated!
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance DocUtils.Pretty CspSign where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty = Doc.text . show
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance DocUtils.Pretty CspAddMorphism where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder pretty = Doc.text . show