SignCSP.hs revision 9f6d67c9b0e2661e7967b435f17a27687929144f
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : CspCASL signatures
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedersignatures for CSP-CASL
fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder-- todo: implement isInclusion, computeExt
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport qualified Data.Set as S
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettimport CASL.AS_Basic_CASL (SORT, VAR)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport CASL.Sign (emptySign, Sign, sortRel)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.Morphism (Morphism)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.Doc as Doc
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.DocUtils as DocUtils
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Common.Lib.Rel (predecessors)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | A process has zero or more parameter sorts, and a communication
b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy Gimblettdata ProcProfile = ProcProfile
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { procArgs :: [SORT]
9f6d67c9b0e2661e7967b435f17a27687929144fAndy Gimblett , procAlphabet :: CommAlpha
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett } deriving (Eq, Show)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | A process communication alphabet consists of a set of sort names
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- and typed channel names.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata TypedChanName = TypedChanName CHANNEL_NAME SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett deriving (Eq, Ord, Show)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata CommType = CommTypeSort SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett | CommTypeChan TypedChanName
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett deriving (Eq, Ord, Show)
9f6d67c9b0e2661e7967b435f17a27687929144fAndy Gimbletttype CommAlpha = S.Set CommType
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype ChanNameMap = Map.Map CHANNEL_NAME SORT
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimbletttype ProcVarMap = Map.Map VAR SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a communication alphabet under CASL subsort
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettcloseCspCommAlpha :: CspSign -> CommAlpha -> CommAlpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcloseCspCommAlpha sig alpha =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett S.unions $ S.toList $ S.map (closeOneCspComm sig) alpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close one CommType under CASL subsort
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettcloseOneCspComm :: CspSign -> CommType -> CommAlpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcloseOneCspComm sig x =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeSort s) ->
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett S.map CommTypeSort (cspSubsortPreds sig s)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeChan (TypedChanName c s)) ->
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (S.map CommTypeSort (cspSubsortPreds sig s))
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (S.map (foo c) (cspSubsortPreds sig s))
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where foo c s = CommTypeChan $ TypedChanName c s
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Get the subsorts of a sort from a CspCASL signature
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortPreds :: CspSign -> SORT -> S.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortPreds sig s = S.union preds (S.singleton s)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where preds = predecessors (sortRel sig) s
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett{- Will probably be useful, but doesn't appear to be right now.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the sorts from a process alphabet
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettprocAlphaSorts :: CommAlpha -> S.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettprocAlphaSorts a = stripMaybe $ S.map justSort a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where justSort n = case n of
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeSort s) -> Just s
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the typed channel names from a process alphabet
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettprocAlphaChans :: CommAlpha -> S.Set TypedChanName
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettprocAlphaChans a = stripMaybe $ S.map justChan a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where justChan n = case n of
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeChan c) -> Just c
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Given a set of Maybes, filter to keep only the Justs
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettstripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettstripMaybe x = S.fromList $ Maybe.catMaybes $ S.toList x
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a set of sorts under a subsort relation
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts :: CspSign -> S.Set SORT -> S.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts sig sorts =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where subsort_sets = S.toList $ S.map (cspSubsortPreds sig) sorts
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata CspProcSign = CspProcSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , procs :: ProcNameMap
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett } deriving (Eq, Show)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CspCASL signature is a CASL signature with a CSP process
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- signature in the extendedInfo part.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspSign = Sign () CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign :: CspSign
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign = emptySign emptyCspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign :: CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign = CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Compute union of two CSP process signatures.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig :: CspProcSign -> CspProcSign -> CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig a b =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a { chans = chans a `Map.union` chans b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , procs = procs a `Map.union` procs b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX looks incomplete!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettisInclusion :: CspProcSign -> CspProcSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX morphisms between CSP process signatures?
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettdata CspAddMorphism = CspAddMorphism
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { channelMap :: Map.Map Id Id
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , processMap :: Map.Map Id Id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving (Eq, Show)
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspMorphism = Morphism () CspProcSign CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism :: CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism = CspAddMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { channelMap = Map.empty -- ???
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , processMap = Map.empty
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- dummy instances, need to be elaborated!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance DocUtils.Pretty CspProcSign where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettinstance DocUtils.Pretty CspAddMorphism where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show