StatAnaCSP.hs revision 7ed9dd4cb1efebf38025cff55e9a28d0c274ef69
5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : static analysis for CspCASL
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Markus Roggenbach, Till Mossakowski, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStatic analysis for CSP-CASL
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport qualified Control.Monad as Monad
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Map as Map
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Data.Maybe as Maybe
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport qualified Data.Set as S
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport CASL.AS_Basic_CASL (FunKind(..), SORT, TERM(..), VAR)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.MixfixParser (emptyMix, Mix(..), makeRules, mkIdSets,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder resolveMixfix, unite)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport CASL.Overload (oneExpTerm)
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport CASL.StaticAna (allOpIds, allPredIds)
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Rel as Rel
af621d0066770895fd79562728e93099c8c52060Christian Maederimport Common.Id (Id, simpleIdToId)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport CspCASL.LocalTop (Obligation(..), unmetObs)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederbasicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -> Result (CspBasicSpec, ExtSign CspCASLSign (), [Named ()])
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederbasicAnalysisCspCASL (cc, sigma, _ga) = do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let (_, accSig) = runState (ana_BASIC_CSP cc) sigma
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let ds = reverse $ envDiags accSig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Result ds (Just ()) -- insert diagnostics
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return (cc, mkExtSign accSig, [])
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederana_BASIC_CSP cc = do checkLocalTops
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder mapM anaChanDecl (channels cc)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder mapM anaProcItem (proc_items cc)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- Analysis of local top elements
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Check CspCASL signature for local top elements in subsorts.
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedercheckLocalTops :: State CspCASLSign ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedercheckLocalTops = do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sortRel sig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder addDiags (map lteError obs)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Add diagnostic error for every unmet local top element obligation.
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederlteError :: Obligation SORT -> Diagnosis
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederlteError (Obligation x y z) = mkDiag Error msg ()
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder where msg = ("local top element obligation ("
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ++ ") unfulfilled")
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- Analysis of channel declarations
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaChanDecl (ChannelDecl chanNames chanSort) = do
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder checkSorts [chanSort] -- check channel sort is known
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let ext = extendedInfo sig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder oldChanMap = chans ext
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder newChanMap <- Monad.foldM (anaChannelName chanSort) oldChanMap chanNames
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder vds <- gets envDiags
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder put sig { extendedInfo = ext { chans = newChanMap }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , envDiags = vds
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return (ChannelDecl chanNames chanSort)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder State CspCASLSign ChanNameMap
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaederanaChannelName s m chanName = do
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder if (show chanName) `S.member` (S.map show (sortSet sig))
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder then do let err = "channel name already in use as a sort name"
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder addDiags [mkDiag Error err chanName]
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder else case Map.lookup chanName m of
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Nothing -> return (Map.insert chanName s m) -- insert new.
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder then do let warn = "channel redeclared with same sort"
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder addDiags [mkDiag Warning warn chanName]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return m -- already declared with this sort.
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder else do let err = "channel declared with multiple sorts"
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder addDiags [mkDiag Error err chanName]
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder-- Analysis of process items
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederanaProcItem :: PROC_ITEM -> State CspCASLSign ()
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian MaederanaProcItem procItem =
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder case procItem of
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (Proc_Eq parmProcName procTerm) -> anaProcEq parmProcName procTerm
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- Analysis of process declarations
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederanaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder -> State CspCASLSign ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaProcDecl name argSorts (ProcAlphabet commTypes _) = do
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let ext = extendedInfo sig
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder oldProcDecls = procSet ext
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder newProcDecls <-
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder if name `Map.member` oldProcDecls
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder then do -- duplicate process declaration
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let err = "process name declared more than once"
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder addDiags [mkDiag Error err name]
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder return oldProcDecls
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder else do -- new process declation
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder checkSorts argSorts -- check argument sorts are known
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -- build alphabet: set of CommType values
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder alpha <- Monad.foldM (anaCommType sig) S.empty commTypes
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let profile = (ProcProfile argSorts alpha)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return (Map.insert name profile oldProcDecls)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder vds <- gets envDiags
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder put sig { extendedInfo = ext {procSet = newProcDecls }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , envDiags = vds
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder-- Analysis of process equations
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederanaProcEq :: PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederanaProcEq (ParmProcname pn vs) proc = do
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let ext = extendedInfo sig
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder procDecls = procSet ext
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder prof = pn `Map.lookup` procDecls
8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder -- Only analyse a process if its name (and thus profile) is known
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Just (ProcProfile procArgs procAlpha) ->
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder do gVars <- anaProcVars pn procArgs vs -- compute global vars
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder termAlpha <- anaProcTerm proc gVars Map.empty
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder checkCommAlphaSub termAlpha procAlpha proc "process equation"
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder do addDiags [mkDiag Error "process equation for unknown process" pn]
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder vds <- gets envDiags
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder put sig { envDiags = vds }
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- Analysis of process variable names.
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederanaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarMap
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaProcVars pn ss vs = do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case (compare (length ss) (length vs)) of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder LT -> do addDiags [mkDiag Error "too many process arguments" pn]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GT -> do addDiags [mkDiag Error "not enough process arguments" pn]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspCASLSign ProcVarMap
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaProcVar old (v, s) = do
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder then do addDiags [mkDiag Error "process arg declared more than once" v]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else return (Map.insert v s old)
f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder-- Analysis of process terms
fce77b2785912d1abbcc3680088b235f534bdeffChristian MaederanaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> State CspCASLSign CommAlpha
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaProcTerm proc gVars lVars = case proc of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder NamedProcess name args _ ->
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder do addDiags [mkDiag Debug "Named process" proc]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder al <- anaNamedProc proc name args (lVars `Map.union` gVars)
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder do addDiags [mkDiag Debug "Skip" proc]
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder do addDiags [mkDiag Debug "Stop" proc]
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder do addDiags [mkDiag Debug "Div" proc]
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder do addDiags [mkDiag Debug "Run" proc]
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder comms <- anaEventSet es
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Chaos es _ ->
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder do addDiags [mkDiag Debug "Chaos" proc]
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder comms <- anaEventSet es
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder PrefixProcess e p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Prefix" proc]
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (comms `S.union` evComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder InternalPrefixProcess v s p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Internal prefix" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder checkSorts [s] -- check sort is known
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (Map.insert v s lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (S.insert (CommTypeSort s) comms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ExternalPrefixProcess v s p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "External prefix" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder checkSorts [s] -- check sort is known
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (Map.insert v s lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (S.insert (CommTypeSort s) comms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Sequential p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Sequential" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder qComms <- anaProcTerm q gVars Map.empty
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder InternalChoice p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "InternalChoice" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder qComms <- anaProcTerm q gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ExternalChoice p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "ExternalChoice" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder qComms <- anaProcTerm q gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Interleaving p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Interleaving" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder qComms <- anaProcTerm q gVars lVars
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder return (pComms `S.union` qComms)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder SynchronousParallel p q _ ->
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder do addDiags [mkDiag Debug "Synchronous" proc]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder pComms <- anaProcTerm p gVars lVars
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder qComms <- anaProcTerm q gVars lVars
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return (pComms `S.union` qComms)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GeneralisedParallel p es q _ ->
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder do addDiags [mkDiag Debug "Generalised parallel" proc]
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder pComms <- anaProcTerm p gVars lVars
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder synComms <- anaEventSet es
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder qComms <- anaProcTerm q gVars lVars
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return (S.unions [pComms, qComms, synComms])
bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder AlphabetisedParallel p esp esq q _ ->
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder do addDiags [mkDiag Debug "Alphabetised parallel" proc]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder pComms <- anaProcTerm p gVars lVars
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder pSynComms <- anaEventSet esp
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder qSynComms <- anaEventSet esq
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder qComms <- anaProcTerm q gVars lVars
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder checkCommAlphaSub qSynComms qComms proc "alphabetised parallel, right"
return (pComms `S.union` qComms)
return (pComms `S.union` hidComms)
return (pComms `S.union` renAlpha)
let fComms = S.empty -- XXX get formula sorts here
return (S.unions [pComms, qComms, fComms])
prof = pn `Map.lookup` procDecls
return S.empty
if ctSort `S.member` (sortSet sig)
do return (S.insert (CommTypeSort ctSort) alpha)
case Map.lookup ct (chans $ extendedInfo sig) of
return (S.insert (mkTypedChan ct s) alpha)
case c `Map.lookup` (chans ext) of
case c `Map.lookup` (chans ext) of
if s `S.member` (subsorts chanSort)
where subsorts = Rel.predecessors (sortRel sig)
if (not $ S.null totOps)
then return (inAl `S.union` totOps)
if (not $ S.null parOps)
then return (inAl `S.union` parOps)
if (not $ S.null preds)
then return (inAl `S.union` preds)
getBinOpsById :: Id -> FunKind -> State CspCASLSign (S.Set CommType)
binOpsKind = S.filter (isBin kind) opsWithId
getBinPredsById :: Id -> State CspCASLSign (S.Set CommType)
binPreds = S.filter isBin predsWithId
let extras = ((closeCspCommAlpha sig sub) `S.difference`
if S.null extras
context ++ "): " ++ (show $ S.toList extras))
let newVars = Map.union pm (varMap sig)