SignCSP.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
08ea5f703d2e034f347a7e30ee3cca8a127d9c0eChristian MaederModule : $Header$
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : CspCASL signatures
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedersignatures for CSP-CASL
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly ( addProcNameToProcNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , ccSig2CASLSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , ccSig2CspSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , ChanNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , closeCspCommAlpha
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , CspCASLSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , CspSen (..)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , CspSign (..)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , cspSignUnion
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , emptyCspCASLSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , emptyCspSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , FQProcVarList
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , getUniqueProfileInProcNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , isCspCASLSubSig
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , isCspSubSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , isNameInProcNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , isProcessEq
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , ProcNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , ProcVarList
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , reduceProcProfile
01008b4f7e0076702f9cd61cb41bc02142c34375Christian Maeder , commType2Sort
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , relatedSorts
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , relatedProcs
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly , unionCspCASLSign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified CspCASL.LocalTop as LocalTop
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyimport Common.Lib.Rel (Rel, predecessors, member)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyimport Common.Utils (keepMins)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Map as Map
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Set as Set
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maedertype ChanNameMap = MapSet.MapSet CHANNEL_NAME SORT
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maedertype ProcNameMap = MapSet.MapSet PROCESS_NAME ProcProfile
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimbletttype ProcVarMap = Map.Map SIMPLE_ID SORT
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillytype ProcVarList = [(SIMPLE_ID, SORT)]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Add a process name and its profile to a process name map. exist.
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian MaederaddProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder -> ProcNameMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederaddProcNameToProcNameMap = MapSet.insert
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Test if a simple process name with a profile is in the process name map.
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederisNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederisNameInProcNameMap = MapSet.member
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | Given a simple process name and a required number of parameters, find a
842ae753ab848a8508c4832ab64296b929167a97Christian Maederunqiue profile with that many parameters if possible. If this is not possible
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder(i.e., name does not exist, or no profile with the required number of
842ae753ab848a8508c4832ab64296b929167a97Christian Maederarguments or not unique profile for the required number of arguments), then
842ae753ab848a8508c4832ab64296b929167a97Christian Maederthe functions returns a failed result with a helpful error message. failure. -}
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedergetUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Result ProcProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetUniqueProfileInProcNameMap name numParams pm =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let profiles = MapSet.lookup name pm
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly isMatch (ProcProfile argSorts _) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder length argSorts == numParams
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly matchedProfiles = Set.filter isMatch profiles
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in case Set.toList matchedProfiles of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [] -> mkError ("Process name not in signature with "
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ show numParams ++ " parameters:") name
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [p] -> return p
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> mkError ("Process name not unique in signature with "
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ++ show numParams ++ " parameters:") name
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a communication alphabet under CASL subsort
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseCspCommAlpha sr =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Set.unions . Set.toList . Set.map (closeOneCspComm sr)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close one CommType under CASL subsort
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseOneCspComm :: Rel SORT -> CommType -> CommAlpha
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseOneCspComm sr x = let
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder subsorts s' = Set.insert s' $ predecessors sr s'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CommTypeSort s ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.map CommTypeSort (subsorts s)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CommTypeChan (TypedChanName c s) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.map CommTypeSort (subsorts s)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder `Set.union` Set.map (mkTypedChan c) (subsorts s)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly{- | Remove the implicit sorts from the proc name map under a sub-sort
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyrelation. Assumes all the proc profile's comms are in the sub sort relation and
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillysimply makes the comms contain only the minimal super sorts under the sub-sort
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcNamesInSig :: Rel SORT -> CspSign -> CspSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcNamesInSig sr cspSig =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly cspSig { procSet = reduceProcNameMap sr $ procSet cspSig }
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly{- | Remove the implicit sorts from a proc name map under a sub-sort
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillyrelation. Assumes all the proc profile's comms are in the sub sort relation and
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillysimply makes the comms contain only the minimal super sorts under the sub-sort
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcNameMap :: Rel SORT -> ProcNameMap -> ProcNameMap
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcNameMap sr =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly MapSet.map (reduceProcProfile sr)
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly{- | Remove the implicit sorts from a profile under a sub-sort relation. Assumes
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillyall the proc profile's comms are in the sub sort relation and simply makes the
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillycomms contain only the minimal super sorts under the sub-sort relation. -}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceProcProfile sr (ProcProfile argSorts comms) =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly ProcProfile argSorts (reduceCspCommAlpha sr comms)
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reilly{- | Remove the implicit sorts from a CommAlpha under a sub-sort
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillyrelation. Assumes all the proc profile's comms are in the sub sort relation and
baba0fc1bc5847a1b084c03b8895097649a25a46Liam O'Reillysimply makes the comms contain only the minimal super sorts under the sub-sort
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyreduceCspCommAlpha sr =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly concatMap (keepMins $ cmpCommType sr) . groupBy sameChan . Set.toList
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillycmpCommType :: Rel SORT -> CommType -> CommType -> Bool
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillycmpCommType rel t1 t2 = let
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly s1 = commType2Sort t1
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly s2 = commType2Sort t2
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly in s1 == s2 || member s2 s1 rel
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillycommType2Sort :: CommType -> SORT
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillycommType2Sort c = case c of
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly CommTypeSort s -> s
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly CommTypeChan (TypedChanName _ s) -> s
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillysameChan :: CommType -> CommType -> Bool
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillysameChan t1 t2 = case (t1, t2) of
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly (CommTypeSort _, CommTypeSort _) -> True
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly (CommTypeChan (TypedChanName c1 _), CommTypeChan (TypedChanName c2 _))
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettdata CspSign = CspSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet :: ProcNameMap
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder-- | plain union
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillycspSignUnion :: CspSign -> CspSign -> CspSign
67e234eb781dd16dfd269486befd2b5781075079Christian MaedercspSignUnion sign1 sign2 = emptyCspSign
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly { chans = chans sign1 `MapSet.union` chans sign2
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly , procSet = procSet sign1 `MapSet.union` procSet sign2 }
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | A CspCASL signature is a CASL signature with a CSP process
842ae753ab848a8508c4832ab64296b929167a97Christian Maedersignature in the extendedInfo part. -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maedertype CspCASLSign = Sign CspSen CspSign
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyccSig2CASLSign :: CspCASLSign -> CASLSign
bcd914850de931848b86d7728192a149f9c0108bChristian MaederccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Projection from CspCASL signature to Csp signature
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyccSig2CspSign :: CspCASLSign -> CspSign
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederccSig2CspSign = extendedInfo
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspCASLSign :: CspCASLSign
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspCASLSign = emptySign emptyCspSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspSign :: CspSign
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspSign = CspSign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Compute union of two CSP CASL signatures.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyunionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyunionCspCASLSign s1 s2 = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Compute the unioned data signature ignoring the csp signatures
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Check that the new data signature has local top elements
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder rel = sortRel newDataSig
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Compute the unioned csp signature with respect to the new data signature
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- Only error will be added if there are any probelms. If there are no
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder problems no errors will be added and hets will continue as normal. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder appendDiags diags'
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- put both the new data signature and the csp signature back together
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ newDataSig {extendedInfo = newCspSign}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | Compute union of two CSP signatures assuming the new already computed data
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyunionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyunionCspSign sr a b = reduceProcNamesInSig sr $ cspSignUnion a b
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly-- | Compute difference of two CSP process signatures.
7dc79552823b00bdd0dd75fcd2ab9af541c71650Christian MaederdiffCspSig :: CspSign -> CspSign -> CspSign
7dc79552823b00bdd0dd75fcd2ab9af541c71650Christian MaederdiffCspSig a b = emptyCspSign
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder { chans = MapSet.difference (chans a) $ chans b
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , procSet = MapSet.difference (procSet a) $ procSet b
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Is one CspCASL Signature a sub signature of another
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
842ae753ab848a8508c4832ab64296b929167a97Christian MaederisCspCASLSubSig =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Normal casl subsignature and our extended csp part
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder isSubSig isCspSubSign
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- Also the sorts and sub-sort rels should be equal. If they are not then we
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder cannot just add the processes in as their profiles need to be donward closed
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder under the new sort-rels, but we do not check this here. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | Is one Csp Signature a sub signature of another assuming the same data
842ae753ab848a8508c4832ab64296b929167a97Christian Maedersignature for now. -}
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillyisCspSubSign :: CspSign -> CspSign -> Bool
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillyisCspSubSign a b =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder MapSet.isSubmapOf (chans a) (chans b) &&
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Check for each profile that the set of names are included.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder MapSet.isSubmapOf (procSet a) (procSet b)
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for CspCASL signatures
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CspSign where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printCspSign
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintCspSign :: CspSign -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintCspSign sigma =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case mapSetToList $ chans sigma of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder s -> keyword (channelS ++ appendS s) <+> printChanList s
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder $+$ case mapSetToList $ procSet sigma of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ps -> keyword processS <+> printProcList ps
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Pretty printing for channels
842ae753ab848a8508c4832ab64296b929167a97Christian MaederprintChanList :: [(CHANNEL_NAME, SORT)] -> Doc
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian MaederprintChanList l = let
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder gl = groupBy (\ (_, s1) (_, s2) -> s1 == s2) $ sortBy (comparing snd) l
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder printChan cl = case cl of
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder [] -> empty -- should not happen
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder (_, s) : _ -> fsep [ppWithCommas (map fst cl), colon <+> pretty s]
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder in sepBySemis $ map printChan gl
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Pretty printing for processes
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederprintProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian MaederprintProcList = sepBySemis . map
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder (\ (procName, procProfile) -> pretty procName <+> pretty procProfile)
23b1275b6136c9dbec63d3ea87c697f2aa89a061Liam O'Reilly-- * overload relations: We do not have one of these yet in theory
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedSorts :: CspCASLSign -> SORT -> SORT -> Bool
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedSorts sig s1 s2 = haveCommonSupersorts True sig s1 s2
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder || haveCommonSupersorts False sig s1 s2
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedCommTypes :: CspCASLSign -> CommType -> CommType -> Bool
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedCommTypes sig ct1 ct2 = case (ct1, ct2) of
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder (CommTypeSort s1, CommTypeSort s2) -> relatedSorts sig s1 s2
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder (CommTypeChan (TypedChanName c1 s1), CommTypeChan (TypedChanName c2 s2))
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder -> c1 == c2 && relatedSorts sig s1 s2
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha -> Bool
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedCommAlpha sig al1 al2 = Set.null al1 || Set.null al2 ||
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder any (\ a -> any (relatedCommTypes sig a) $ Set.toList al1) (Set.toList al2)
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaederrelatedProcs sig (ProcProfile l1 al1) (ProcProfile l2 al2) =
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder length l1 == length l2 &&
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder and (zipWith (relatedSorts sig) l1 l2)
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder && relatedCommAlpha sig al1 al2
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder-- * Sentences
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | FQProcVarList should only contain fully qualified CASL variables which are
842ae753ab848a8508c4832ab64296b929167a97Christian MaederTERMs i.e. constructed via the TERM constructor Qual_var. -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillytype FQProcVarList = [TERM ()]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | A CspCASl senetence is either a CASL formula or a Procsses equation. A
842ae753ab848a8508c4832ab64296b929167a97Christian Maederprocess equation has on the LHS a process name, a list of parameters which
842ae753ab848a8508c4832ab64296b929167a97Christian Maederare qualified variables (which are terms), a constituent( or is it permitted
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder?) communication alphabet and finally on the RHS a fully qualified process. -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maederdata CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
bcd914850de931848b86d7728192a149f9c0108bChristian Maedertype CspCASLSen = FORMULA CspSen
bcd914850de931848b86d7728192a149f9c0108bChristian Maederinstance GetRange CspSen
bcd914850de931848b86d7728192a149f9c0108bChristian Maederinstance Pretty CspSen where
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder pretty (ProcessEq pn varList _commAlpha proc) =
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder let varDoc = if null varList
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder else parens $ ppWithCommas varList
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder in fsep [pretty pn, varDoc, equals <+> pretty proc]
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maederinstance FormExtension CspSen where
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder prefixExt (ProcessEq pn _ _ _) = case pn of
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder PROCESS_NAME _ -> (keyword processS <+>)
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder FQ_PROCESS_NAME {} -> id
bcd914850de931848b86d7728192a149f9c0108bChristian Maederinstance TermExtension CspSen
bcd914850de931848b86d7728192a149f9c0108bChristian Maederinstance TermParser CspSen
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq :: CspCASLSen -> Bool
bcd914850de931848b86d7728192a149f9c0108bChristian MaederisProcessEq f = case f of
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder ExtFORMULA _ -> True