SignCSP.hs revision f284db6f4dffd7bf60b82319648efb7bcb9378c9
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{-# LANGUAGE TypeSynonymInstances #-}
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceDescription : CspCASL signatures
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
5d801400993c9671010d244646936d8fd435638cChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : provisional
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancePortability : portable
5d801400993c9671010d244646936d8fd435638cChristian Maedersignatures for CSP-CASL
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederimport qualified CspCASL.LocalTop as LocalTop
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceimport Common.Lib.Rel (Rel, predecessors)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Map as Map
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Set as Set
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancetype ChanNameMap = Map.Map CHANNEL_NAME (Set.Set SORT)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancetype ProcNameMap = Map.Map PROCESS_NAME (Set.Set ProcProfile)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancetype ProcVarMap = Map.Map SIMPLE_ID SORT
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mancetype ProcVarList = [(SIMPLE_ID, SORT)]
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder-- | Add a process name and its profile to a process name map. exist.
968930c7674ae3b63d308bf4fa651400aa263054Christian MaederaddProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile ->
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ProcNameMap -> ProcNameMap
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceaddProcNameToProcNameMap name profile pm =
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance let l = Map.findWithDefault Set.empty name pm
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance in Map.insert name (Set.insert profile l) pm
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- | Test if a simple process name with a profile is in the process name map.
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisNameInProcNameMap name profile pm =
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance let l = Map.findWithDefault Set.empty name pm
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder{- | Given a simple process name and a required number of parameters, find a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceunqiue profile with that many parameters if possible. If this is not possible
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance(i.e., name does not exist, or no profile with the required number of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancearguments or not unique profile for the required number of arguments), then
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancethe functions returns a failed result with a helpful error message. failure. -}
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancegetUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Result ProcProfile
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancegetUniqueProfileInProcNameMap name numParams pm =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let profiles = Map.findWithDefault Set.empty name pm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance isMatch (ProcProfile argSorts _) =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance length argSorts == numParams
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance matchedProfiles = Set.filter isMatch profiles
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance in case Set.toList matchedProfiles of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [] -> mkError ("Process name not in signature with "
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance ++ show numParams ++ " parameters:") name
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [p] -> return p
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance _ -> mkError ("Process name not unique in signature with "
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance ++ show numParams ++ " parameters:") name
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel MancecloseProcs :: Rel SORT -> CspSign -> CspSign
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel MancecloseProcs r s = s { procSet = closeProcNameMapSortRel r $ procSet s }
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder{- | Close a proc name map under a sub-sort relation. Assumes all the proc
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceprofile's comms are in the sub sort relation and simply makes the comms
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedownward closed under the sub-sort relation. -}
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecloseProcNameMapSortRel :: Rel SORT -> ProcNameMap -> ProcNameMap
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecloseProcNameMapSortRel sig =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Map.map (Set.map $ closeProcProfileSortRel sig)
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder{- | Close a profile under a sub-sort relation. Assumes the proc profile's
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maedercomms are in the sub sort relation and simply makes the comms downward closed
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maederunder the sub-sort relation. -}
ea3f858eb531d981df3ed00beeadd99cf025adecChristian MaedercloseProcProfileSortRel :: Rel SORT -> ProcProfile -> ProcProfile
ea3f858eb531d981df3ed00beeadd99cf025adecChristian MaedercloseProcProfileSortRel sig (ProcProfile argSorts comms) =
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance ProcProfile argSorts (closeCspCommAlpha sig comms)
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance-- Close a communication alphabet under CASL subsort
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecloseCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecloseCspCommAlpha sr =
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Set.unions . Set.toList . Set.map (closeOneCspComm sr)
4c684d7a2343be7350eba088f8be42888f86a495Felix Gabriel Mance-- Close one CommType under CASL subsort
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel MancecloseOneCspComm :: Rel SORT -> CommType -> CommAlpha
5a3ae0a9224276de25e709ef8788c1b9716cd206Christian MaedercloseOneCspComm sr x = let
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance mkTypedChan c s = CommTypeChan $ TypedChanName c s
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Set.singleton s' `Set.union` predecessors sr s'
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance CommTypeSort s ->
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Set.map CommTypeSort (subsorts s)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance CommTypeChan (TypedChanName c s) ->
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Set.map CommTypeSort (subsorts s)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance `Set.union` Set.map (mkTypedChan c) (subsorts s)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance{- Will probably be useful, but doesn't appear to be right now.
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance-- Extract the sorts from a process alphabet
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel ManceprocAlphaSorts :: CommAlpha -> Set.Set SORT
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceprocAlphaSorts a = stripMaybe $ Set.map justSort a
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance where justSort n = case n of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (CommTypeSort s) -> Just s
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- Extract the typed channel names from a process alphabet
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceprocAlphaChans a = stripMaybe $ Set.map justChan a
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance where justChan n = case n of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (CommTypeChan c) -> Just c
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance-- Given a set of Maybes, filter to keep only the Justs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancestripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancestripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- Close a set of sorts under a subsort relation
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancecspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancecspSubsortCloseSorts sig sorts =
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance where subsort_sets =
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Set.toList $ Set.map (cspSubsortPreds sig) sorts
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | CSP process signature.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mancedata CspSign = CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance { chans :: ChanNameMap
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance , procSet :: ProcNameMap
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance } deriving (Eq, Ord, Show)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- | plain union
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecspSignUnion :: CspSign -> CspSign -> CspSign
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecspSignUnion sign1 sign2 = emptyCspSign
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance { chans = addMapSet (chans sign1) (chans sign2)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , procSet = addMapSet (procSet sign1) (procSet sign2) }
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance{- | A CspCASL signature is a CASL signature with a CSP process
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mancesignature in the extendedInfo part. -}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mancetype CspCASLSign = Sign CspSen CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceccSig2CASLSign :: CspCASLSign -> CASLSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Projection from CspCASL signature to Csp signature
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceccSig2CspSign :: CspCASLSign -> CspSign
968930c7674ae3b63d308bf4fa651400aa263054Christian MaederccSig2CspSign = extendedInfo
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Empty CspCASL signature.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceemptyCspCASLSign :: CspCASLSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceemptyCspCASLSign = emptySign emptyCspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Empty CSP process signature.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceemptyCspSign :: CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceemptyCspSign = CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Compute union of two CSP CASL signatures.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceunionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceunionCspCASLSign s1 s2 = do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- Compute the unioned data signature ignoring the csp signatures
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -- Check that the new data signature has local top elements
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance rel = sortRel newDataSig
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -- Compute the unioned csp signature with respect to the new data signature
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance {- Only error will be added if there are any probelms. If there are no
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance problems no errors will be added and hets will continue as normal. -}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance appendDiags diags'
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- put both the new data signature and the csp signature back together
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance return $ newDataSig {extendedInfo = newCspSign}
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance{- | Compute union of two CSP signatures assuming the new already computed data
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceunionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceunionCspSign sr a b = cspSignUnion (closeProcs sr a) (closeProcs sr b)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Compute difference of two CSP process signatures.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancediffCspSig :: CspSign -> CspSign -> CspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancediffCspSig a b = emptyCspSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance { chans = diffMapSet (chans a) $ chans b
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance , procSet = diffMapSet (procSet a) $ procSet b
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | Is one CspCASL Signature a sub signature of another
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisCspCASLSubSig =
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- Normal casl subsignature and our extended csp part
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance isSubSig isCspSubSign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance {- Also the sorts and sub-sort rels should be equal. If they are not then we
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance cannot just add the processes in as their profiles need to be donward closed
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance under the new sort-rels, but we do not check this here. -}
083b2687afdb676237f926bdb643b24027291d05Felix Gabriel Mance{- | Is one Csp Signature a sub signature of another assuming the same data
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mancesignature for now. -}
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel ManceisCspSubSign :: CspSign -> CspSign -> Bool
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceisCspSubSign a b =
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance isSubMapSet (chans a) (chans b) &&
0c3badd7ad83eb89f64ef5ed1122c4fa856fb45dFelix Gabriel Mance -- Check for each profile that the set of names are included.
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance isSubMapSet (procSet a) (procSet b)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance-- | Pretty printing for CspCASL signatures
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance Pretty CspSign where
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance pretty = printCspSign
0c3badd7ad83eb89f64ef5ed1122c4fa856fb45dFelix Gabriel MancemapSetToList :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> [(a, b)]
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel MancemapSetToList = concatMap (\ (c, ts) -> map (\ t -> (c, t)) $ Set.toList ts)
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel ManceprintCspSign :: CspSign -> Doc
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceprintCspSign sigma =
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel Mance case mapSetToList $ chans sigma of
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance s -> keyword (channelS ++ appendS s) <+> printChanList s
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance $+$ case mapSetToList $ procSet sigma of
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance ps -> keyword processS <+> printProcList ps
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance-- | Pretty printing for channels
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel ManceprintChanList :: [(CHANNEL_NAME, SORT)] -> Doc
0c3badd7ad83eb89f64ef5ed1122c4fa856fb45dFelix Gabriel ManceprintChanList l = let
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance gl = groupBy (\ (_, s1) (_, s2) -> s1 == s2) $ sortBy (comparing snd) l
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance printChan cl = case cl of
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder [] -> empty -- should not happen
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance (_, s) : _ -> fsep [ppWithCommas (map fst cl), colon <+> pretty s]
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance in sepBySemis $ map printChan gl
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance-- | Pretty printing for processes
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceprintProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceprintProcList =
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance sepBySemis . map printProc
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance where printProc (procName, procProfile) = pretty procName <+>
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance pretty procProfile
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance{- | FQProcVarList should only contain fully qualified CASL variables which are
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian MaederTERMs i.e. constructed via the TERM constructor Qual_var. -}
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mancetype FQProcVarList = [TERM ()]
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance{- | A CspCASl senetence is either a CASL formula or a Procsses equation. A
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceprocess equation has on the LHS a process name, a list of parameters which
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceare qualified variables (which are terms), a constituent( or is it permitted
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance?) communication alphabet and finally on the RHS a fully qualified process. -}
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mancedata CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance deriving (Show, Eq, Ord)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mancetype CspCASLSen = FORMULA CspSen
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance GetRange CspSen
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance Pretty CspSen where
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance pretty (ProcessEq pn varList _commAlpha proc) =
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance let varDoc = if null varList
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance else parens $ ppWithCommas varList
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel Mance in fsep [pretty pn, varDoc, equals <+> pretty proc]
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance FormExtension CspSen where
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance prefixExt (ProcessEq pn _ _ _) = case pn of
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance PROCESS_NAME _ -> (keyword processS <+>)
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance FQ_PROCESS_NAME {} -> id
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance TermExtension CspSen
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Manceinstance TermParser CspSen
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceisProcessEq :: CspCASLSen -> Bool
0c3badd7ad83eb89f64ef5ed1122c4fa856fb45dFelix Gabriel ManceisProcessEq f = case f of
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance ExtFORMULA _ -> True