SignCSP.hs revision d297a45fc73aa6c4a1f9d073c3170611415f324b
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannDescription : CspCASL signatures
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannMaintainer : M.Roggenbach@swansea.ac.uk
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannStability : provisional
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannPortability : portable
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannsignatures for CSP-CASL
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- todo: implement isInclusion, computeExt
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Data.Map as Map
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Data.Set as S
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport CASL.AS_Basic_CASL (SORT, VAR)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport CASL.Sign (emptySign, Sign, sortRel)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport CASL.Morphism (Morphism)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Common.Doc as Doc
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Common.DocUtils as DocUtils
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport Common.Lib.Rel (predecessors)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | A process has zero or more parameter sorts, and a communication
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata ProcProfile = ProcProfile
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { procArgs :: [SORT]
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , procAlphabet :: CommAlpha
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann } deriving (Eq, Show)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | A process communication alphabet consists of a set of sort names
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- and typed channel names.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata TypedChanName = TypedChanName CHANNEL_NAME SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann deriving (Eq, Ord, Show)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata CommType = CommTypeSort SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann | CommTypeChan TypedChanName
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann deriving (Eq, Ord, Show)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype CommAlpha = S.Set CommType
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype ChanNameMap = Map.Map CHANNEL_NAME SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype ProcVarMap = Map.Map VAR SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Close a communication alphabet under CASL subsort
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncloseCspCommAlpha :: CspSign -> CommAlpha -> CommAlpha
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncloseCspCommAlpha sig alpha =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann S.unions $ S.toList $ S.map (closeOneCspComm sig) alpha
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Close one CommType under CASL subsort
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncloseOneCspComm :: CspSign -> CommType -> CommAlpha
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncloseOneCspComm sig x =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (CommTypeSort s) -> S.map CommTypeSort (subsorts s)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (CommTypeChan (TypedChanName c s)) -> (S.map CommTypeSort (subsorts s))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (S.map (mkTypedChan c) (subsorts s))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann where mkTypedChan c s = CommTypeChan $ TypedChanName c s
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann subsorts = predecessors (sortRel sig)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann{- Will probably be useful, but doesn't appear to be right now.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Extract the sorts from a process alphabet
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprocAlphaSorts :: CommAlpha -> S.Set SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprocAlphaSorts a = stripMaybe $ S.map justSort a
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann where justSort n = case n of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (CommTypeSort s) -> Just s
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Extract the typed channel names from a process alphabet
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprocAlphaChans :: CommAlpha -> S.Set TypedChanName
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprocAlphaChans a = stripMaybe $ S.map justChan a
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann where justChan n = case n of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (CommTypeChan c) -> Just c
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Given a set of Maybes, filter to keep only the Justs
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannstripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannstripMaybe x = S.fromList $ Maybe.catMaybes $ S.toList x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- Close a set of sorts under a subsort relation
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncspSubsortCloseSorts :: CspSign -> S.Set SORT -> S.Set SORT
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncspSubsortCloseSorts sig sorts =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann where subsort_sets = S.toList $ S.map (cspSubsortPreds sig) sorts
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | CSP process signature.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata CspProcSign = CspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { chans :: ChanNameMap
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , procSet :: ProcNameMap
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann } deriving (Eq, Show)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | A CspCASL signature is a CASL signature with a CSP process
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- signature in the extendedInfo part.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype CspSign = Sign () CspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Empty CspCASL signature.
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspSign :: CspSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspSign = emptySign emptyCspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Empty CSP process signature.
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspProcSign :: CspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspProcSign = CspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Compute union of two CSP process signatures.
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannaddCspProcSig :: CspProcSign -> CspProcSign -> CspProcSign
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannaddCspProcSig a b =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann a { chans = chans a `Map.union` chans b
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , procSet = procSet a `Map.union` procSet b
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- XXX looks incomplete!
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisInclusion :: CspProcSign -> CspProcSign -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisInclusion _ _ = True
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- XXX morphisms between CSP process signatures?
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata CspAddMorphism = CspAddMorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { channelMap :: Map.Map Id Id
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , processMap :: Map.Map Id Id
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann } deriving (Eq, Show)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanntype CspMorphism = Morphism () CspProcSign CspAddMorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspAddMorphism :: CspAddMorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannemptyCspAddMorphism = CspAddMorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { channelMap = Map.empty -- ???
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , processMap = Map.empty
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- dummy instances, need to be elaborated!
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance DocUtils.Pretty CspProcSign where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann pretty = Doc.text . show
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance DocUtils.Pretty CspAddMorphism where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann pretty = Doc.text . show