SignCSP.hs revision 7dc79552823b00bdd0dd75fcd2ab9af541c71650
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE TypeSynonymInstances #-}
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
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport CASL.AS_Basic_CASL (CASLFORMULA, SORT, TERM)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (CHANNEL_NAME, SIMPLE_PROCESS_NAME, FQ_PROCESS_NAME, PROCESS (..),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder CommAlpha, CommType (..), TypedChanName (..), ProcProfile (..))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified CspCASL.LocalTop as LocalTop
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport Common.Lib.Rel (Rel, predecessors)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Map as Map
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Set as Set
842ae753ab848a8508c4832ab64296b929167a97Christian Maedertype ChanNameMap = Map.Map CHANNEL_NAME (Set.Set SORT)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillytype ProcNameMap = Map.Map SIMPLE_PROCESS_NAME (Set.Set 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.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyaddProcNameToProcNameMap :: SIMPLE_PROCESS_NAME -> ProcProfile ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ProcNameMap -> ProcNameMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyaddProcNameToProcNameMap name profile pm =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Test if a simple process name with a profile is in the process name map.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisNameInProcNameMap :: SIMPLE_PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisNameInProcNameMap name profile pm =
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. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetUniqueProfileInProcNameMap :: SIMPLE_PROCESS_NAME -> Int -> ProcNameMap ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Result ProcProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetUniqueProfileInProcNameMap name numParams pm =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let profiles = Map.findWithDefault Set.empty 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
67e234eb781dd16dfd269486befd2b5781075079Christian MaedercloseProcs :: Rel SORT -> CspSign -> CspSign
67e234eb781dd16dfd269486befd2b5781075079Christian MaedercloseProcs r s = s { procSet = closeProcNameMapSortRel r $ procSet s }
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | Close a proc name map under a sub-sort relation. Assumes all the proc
842ae753ab848a8508c4832ab64296b929167a97Christian Maederprofile's comms are in the sub sort relation and simply makes the comms
842ae753ab848a8508c4832ab64296b929167a97Christian Maederdownward closed under the sub-sort relation. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseProcNameMapSortRel :: Rel SORT -> ProcNameMap -> ProcNameMap
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercloseProcNameMapSortRel sig =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Map.map (Set.map $ closeProcProfileSortRel sig)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | Close a profile under a sub-sort relation. Assumes the proc profile's
842ae753ab848a8508c4832ab64296b929167a97Christian Maedercomms are in the sub sort relation and simply makes the comms downward closed
842ae753ab848a8508c4832ab64296b929167a97Christian Maederunder the sub-sort relation. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseProcProfileSortRel :: Rel SORT -> ProcProfile -> ProcProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycloseProcProfileSortRel sig (ProcProfile argSorts comms) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ProcProfile argSorts (closeCspCommAlpha sig comms)
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
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly subsorts s' =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Set.singleton s' `Set.union` 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)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett{- Will probably be useful, but doesn't appear to be right now.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the sorts from a process alphabet
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaSorts :: CommAlpha -> Set.Set SORT
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaSorts a = stripMaybe $ Set.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
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaChans a = stripMaybe $ Set.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
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a set of sorts under a subsort relation
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedercspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts sig sorts =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly where subsort_sets =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.toList $ Set.map (cspSubsortPreds sig) sorts
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettdata CspSign = CspSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet :: ProcNameMap
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- | Added for uniformity to the CASL static analysis. After
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder static analysis this is the empty list. -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , ccSentences :: [Named CspCASLSen]
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder } deriving (Eq, Ord, Show)
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder-- | plain union
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillycspSignUnion :: CspSign -> CspSign -> CspSign
67e234eb781dd16dfd269486befd2b5781075079Christian MaedercspSignUnion sign1 sign2 = emptyCspSign
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder { chans = addMapSet (chans sign1) (chans sign2)
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder , procSet = addMapSet (procSet sign1) (procSet sign2) }
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- | A CspCASL signature is a CASL signature with a CSP process
842ae753ab848a8508c4832ab64296b929167a97Christian Maedersignature in the extendedInfo part. -}
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimbletttype CspCASLSign = Sign () CspSign
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyccSig2CASLSign :: CspCASLSign -> CASLSign
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'ReillyccSig2CASLSign sigma = sigma { extendedInfo = () }
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
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder , ccSentences = []
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
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let newDataSig = uniteCASLSign (ccSig2CASLSign s1) (ccSig2CASLSign 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
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder 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
67e234eb781dd16dfd269486befd2b5781075079Christian MaederunionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
67e234eb781dd16dfd269486befd2b5781075079Christian MaederunionCspSign sr a b = cspSignUnion (closeProcs sr a) (closeProcs sr b)
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly-- | Compute difference of two CSP process signatures.
7dc79552823b00bdd0dd75fcd2ab9af541c71650Christian MaederdiffCspSig :: CspSign -> CspSign -> CspSign
7dc79552823b00bdd0dd75fcd2ab9af541c71650Christian MaederdiffCspSig a b = emptyCspSign
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder { chans = diffMapSet (chans a) $ chans b
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , procSet = diffMapSet (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 =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder isSubMapSet (chans a) (chans b) &&
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Check for each profile that the set of names are included.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder isSubMapSet (procSet a) (procSet b)
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for CspCASL signatures
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CspSign where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printCspSign
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermapSetToList :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> [(a, b)]
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermapSetToList = concatMap (\ (c, ts) -> map (\ t -> (c, t)) $ Set.toList ts)
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
842ae753ab848a8508c4832ab64296b929167a97Christian MaederprintChanList =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder vcat . punctuate semi . map printChan
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly where printChan (chanName, sort) =
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder pretty chanName <+> colon <+> pretty sort
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Pretty printing for processes
842ae753ab848a8508c4832ab64296b929167a97Christian MaederprintProcList :: [(SIMPLE_PROCESS_NAME, ProcProfile)] -> Doc
842ae753ab848a8508c4832ab64296b929167a97Christian MaederprintProcList =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder vcat . punctuate semi . map printProc
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder where printProc (procName, procProfile) = pretty procName <+>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder pretty procProfile
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. -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata CspCASLSen
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly = CASLSen (CASLFORMULA)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly deriving (Show, Eq, Ord)
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maederinstance GetRange CspCASLSen
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CspCASLSen where
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder pretty (CASLSen f) = pretty f
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder pretty (ProcessEq pn varList _commAlpha proc) =
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder let varDoc = if null varList
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder else parens $ ppWithCommas varList
042fd01d46834d3fecb5ac109ff905c5eb034376Liam O'Reilly in pretty pn <+> varDoc <+> equals <+> pretty proc
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Test if a CspCASL sentence is a CASL sentence
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisCASLSen :: CspCASLSen -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisCASLSen (CASLSen _) = True
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillyisCASLSen _ = False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Test if a CspCASL sentence is a Process Equation.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq :: CspCASLSen -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq (ProcessEq _ _ _ _) = True
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq _ = False