StatAnaCSP.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : Static analysis of CspCASL
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Andy Gimblett, Liam O'Reilly Markus Roggenbach,
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Swansea University 2008
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : GPLv2 or higher
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : a.m.gimblett@swansea.ac.uk
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStatic analysis of CSP-CASL specifications, following "Tool Support
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederfor CSP-CASL", MPhil thesis by Andy Gimblett, 2008.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Control.Monad as Monad
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Data.Map as Map
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Data.Set as S
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini VAR_DECL(..))
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport CASL.Overload (minExpFORMULA, oneExpTerm)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport CASL.StaticAna (allConstIds, allOpIds, allPredIds)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport qualified Common.Lib.Rel as Rel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport Common.Id (getRange, Id, nullRange, simpleIdToId, tokStr)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport CspCASL.LocalTop (Obligation(..), unmetObs)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport CspCASL.Morphism(makeChannelNameSymbol, makeProcNameSymbol)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | The first element of the returned pair (CspBasicSpec) is the same
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- as the inputted version just with some very minor optimisations -
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- none in our case, but for CASL - brackets are otimized. This all
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- that happens, the mixfixed terms are still mixed fixed terms in
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- the returned version.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibasicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [Named CspCASLSen])
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibasicAnalysisCspCASL (cc, sigma, ga) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> sigma
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just nga -> sigma { globAnnos = nga }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ds = reverse $ envDiags accSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Extract process equations only.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ext = extendedInfo accSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ccsents = reverse $ ccSentences ext
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Clean signature here
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cleanSig = accSig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini { extendedInfo = ext { ccSentences = []}}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in Result (es ++ ds) $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just (cc, ExtSign cleanSig $ declaredSymbols accSig, ccsents)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniana_BASIC_CSP cc = do checkLocalTops
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mapM anaChanDecl (channels cc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mapM anaProcItem (proc_items cc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Analysis of local top elements
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Check a CspCASL signature for local top elements in its subsort
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicheckLocalTops :: State CspCASLSign ()
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedercheckLocalTops = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sortRel sig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags (map lteError obs)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Add diagnostic error message for every unmet local top element
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- obligation.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilteError :: Obligation SORT -> Diagnosis
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilteError (Obligation x y z) = mkDiag Error msg ()
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly where msg = ("local top element obligation ("
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly ++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly ++ ") unfulfilled")
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly-- Static analysis of channel declarations
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Statically analyse a CspCASL channel declaration.
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyanaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyanaChanDecl (ChannelDecl chanNames chanSort) = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly checkSorts [chanSort] -- check channel sort is known
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly let ext = extendedInfo sig
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly oldChanMap = chans ext
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly newChanMap <- Monad.foldM (anaChannelName chanSort) oldChanMap chanNames
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly put sig2 { extendedInfo = ext { chans = newChanMap }}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL channel name.
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder State CspCASLSign ChanNameMap
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaChannelName s m chanName = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini if (show chanName) `S.member` (S.map show (sortSet sig))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then do let err = "channel name already in use as a sort name"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags [mkDiag Error err chanName]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else case Map.lookup chanName m of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Add the channel name as a symbol to the list of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- newly defined symbols - which is stored in the CASL
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addSymbol (makeChannelNameSymbol chanName)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (Map.insert chanName s m) -- insert new.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then do let warn = "channel redeclared with same sort"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags [mkDiag Warning warn chanName]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return m -- already declared with this sort.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else do let err = "channel declared with multiple sorts"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags [mkDiag Error err chanName]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Static analysis of process items
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL process item.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcItem :: PROC_ITEM -> State CspCASLSign ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcItem procItem =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini case procItem of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (Proc_Eq parmProcName procTerm) -> anaProcEq parmProcName procTerm
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Static analysis of process declarations
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL process declaration.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> State CspCASLSign ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcDecl name argSorts (ProcAlphabet commTypes _) = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let ext = extendedInfo sig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini oldProcDecls = procSet ext
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini newProcDecls <-
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini if name `Map.member` oldProcDecls
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then do -- duplicate process declaration
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let err = "process name declared more than once"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags [mkDiag Error err name]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return oldProcDecls
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder else do -- new process declation
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder checkSorts argSorts -- check argument sorts are known
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- build alphabet: set of CommType values. We do not
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- need the fully qualfied commTypes that are returned
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- (these area used for analysing Event Sets)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, _ ) <-
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Monad.foldM (anaCommType sig) (S.empty, []) commTypes
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let profile = (ProcProfile argSorts alpha)
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini -- Add the process name as a symbol to the list of
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini -- newly defined symbols - which is stored in the CASL
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addSymbol (makeProcNameSymbol name)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (Map.insert name profile oldProcDecls)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini put sig2 { extendedInfo = ext {procSet = newProcDecls }}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Static analysis of process equations
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL process equation.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinianaProcEq :: PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcEq (ParmProcname pn vs) proc = do
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder let ext = extendedInfo sig
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ccsens = ccSentences ext
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini procDecls = procSet ext
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini prof = pn `Map.lookup` procDecls
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- Only analyse a process if its name (and thus profile) is known
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini Just (ProcProfile procArgs procAlpha) ->
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini do gVars <- anaProcVars pn procArgs vs -- compute global
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- vars Change a procVarList to a FQProcVarList We do
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- not care about the range as we are building fully
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- qualified variables and they have already been
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- checked to be ok.
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini let mkFQProcVar (v,s) = Qual_var v s nullRange
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqGVars = map mkFQProcVar gVars
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (termAlpha, fqProc) <-
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini anaProcTerm proc (Map.fromList gVars) Map.empty
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini checkCommAlphaSub termAlpha procAlpha proc "process equation"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- Save the diags from the checkCommAlphaSub
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini vds <- gets envDiags
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- put CspCASL Sentences back in to the state with new sentence
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini put sig {envDiags = vds, extendedInfo =
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ext { ccSentences =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- BUG - What should the constituent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- alphabet be for this process?
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- probably the same as the inner one!
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (makeNamed ("Proc_" ++ tokStr pn)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (ProcessEq pn fqGVars
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini fqProc)):ccsens
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini do addDiags [mkDiag Error
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini "process equation for unknown process" pn]
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- | Statically analyse a CspCASL process equation's global variable
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcVars pn ss vs =
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini case (compare (length ss) (length vs)) of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini LT -> do addDiags [mkDiag Error "too many process arguments" pn]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini GT -> do addDiags [mkDiag Error "not enough process arguments" pn]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini EQ -> Monad.foldM anaProcVar [] (zip vs ss)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return $ reverse $ vars
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Statically analyse a CspCASL process-global variable name.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcVar old (v, s) = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini if v `elem` (map fst old)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then do addDiags [mkDiag Error
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "process argument declared more than once" v]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else return ((v,s) : old)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Static analysis of process terms
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- BUG in fucntion below
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- not returing FQProcesses
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- | Statically analyse a CspCASL process term.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- The process that is returned is a fully qualified process.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap ->
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder State CspCASLSign (CommAlpha, PROCESS)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederanaProcTerm proc gVars lVars = case proc of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NamedProcess name args r ->
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder do addDiags [mkDiag Debug "Named process" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (al, fqArgs) <- anaNamedProc proc name args (lVars `Map.union` gVars)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (NamedProcess name fqArgs r) al r
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder return (al, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Skip" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (Skip r) S.empty r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (S.empty, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Stop" proc]
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder let fqProc = FQProcess (Stop r) S.empty r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (S.empty, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Div" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let fqProc = FQProcess (Div r) S.empty r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (S.empty, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Run" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (comms, fqEs) <- anaEventSet es
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let fqProc = FQProcess (Run fqEs r) comms r
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (comms, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Chaos es r ->
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Chaos" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (comms, fqEs) <- anaEventSet es
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (Chaos fqEs r) comms r
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (comms, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder PrefixProcess e p r ->
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Prefix" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (evComms, rcvMap, fqEvent) <- anaEvent e (lVars `Map.union` gVars)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let newAlpha = comms `S.union` evComms
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let fqProc = FQProcess (PrefixProcess fqEvent pFQTerm r) newAlpha r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (newAlpha, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Sequential p q r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Sequential" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pComms, pFQTerm) <- anaProcTerm p gVars lVars
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars Map.empty
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let newAlpha = pComms `S.union` qComms
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (Sequential pFQTerm qFQTerm r) newAlpha r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (newAlpha, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder InternalChoice p q r ->
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder do addDiags [mkDiag Debug "InternalChoice" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (pComms, pFQTerm) <- anaProcTerm p gVars lVars
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = pComms `S.union` qComms
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let fqProc = FQProcess (InternalChoice pFQTerm qFQTerm r) newAlpha r
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (newAlpha, fqProc)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ExternalChoice p q r ->
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "ExternalChoice" proc]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (pComms, pFQTerm) <- anaProcTerm p gVars lVars
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = pComms `S.union` qComms
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm r) newAlpha r
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (newAlpha, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Interleaving p q r ->
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder do addDiags [mkDiag Debug "Interleaving" proc]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (pComms, pFQTerm) <- anaProcTerm p gVars lVars
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars lVars
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder let newAlpha = pComms `S.union` qComms
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder let fqProc = FQProcess (Interleaving pFQTerm qFQTerm r) newAlpha r
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (newAlpha, fqProc)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder SynchronousParallel p q r ->
a2e8cca8a8217b158b0b7a760e8234c03186456dChristian Maeder do addDiags [mkDiag Debug "Synchronous" proc]
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder (pComms, pFQTerm) <- anaProcTerm p gVars lVars
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars lVars
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder let newAlpha = pComms `S.union` qComms
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder let fqProc = FQProcess (SynchronousParallel pFQTerm
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder qFQTerm r) newAlpha r
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (newAlpha, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini GeneralisedParallel p es q r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Generalised parallel" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pComms, pFQTerm) <- anaProcTerm p gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (synComms, fqEs) <- anaEventSet es
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (qComms, qFQTerm) <- anaProcTerm q gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = S.unions [pComms, qComms, synComms]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (GeneralisedParallel pFQTerm fqEs qFQTerm r)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (newAlpha, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini AlphabetisedParallel p esp esq q r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Alphabetised parallel" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pComms, pFQTerm) <- anaProcTerm p gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pSynComms, fqEsp) <- anaEventSet esp
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (qSynComms, fqEsq) <- anaEventSet esq
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (qComms, qFQTerm) <- anaProcTerm q gVars lVars
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder checkCommAlphaSub qSynComms qComms proc
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini "alphabetised parallel, right"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = pComms `S.union` qComms
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini qFQTerm r) newAlpha r
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return (newAlpha, fqProc)
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder Hiding p es r ->
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder do addDiags [mkDiag Debug "Hiding" proc]
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maeder (pComms, pFQTerm) <- anaProcTerm p gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (hidComms, fqEs) <- anaEventSet es
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (pComms `S.union` hidComms, FQProcess (Hiding pFQTerm fqEs r)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (pComms `S.union` hidComms) r)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini RenamingProcess p renaming r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Renaming" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pComms, pFQTerm) <- anaProcTerm p gVars lVars
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (renAlpha, fqRenaming) <- anaRenaming renaming
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = pComms `S.union` renAlpha
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqProc = FQProcess (RenamingProcess pFQTerm fqRenaming r)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (pComms `S.union` renAlpha) r
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ConditionalProcess f p q r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Conditional" proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (pComms, pFQTerm) <- anaProcTerm p gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (qComms, qFQTerm) <- anaProcTerm q gVars lVars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- mfs is the fully qualified formula version of f
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let fFQ = case mfs of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly Nothing -> f -- use old formula as the fully
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- qualified version - there is a
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -- error in the spec anyway as the
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -- formula could not be fully
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -- qualified.
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Just fs -> fs -- use the real fully qualified formula
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder let fComms = case mfs of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just fs -> formulaComms fs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let newAlpha = S.unions [pComms, qComms, fComms]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder let fqProc = FQProcess (ConditionalProcess
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder (fFQ) pFQTerm qFQTerm r)
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder return (newAlpha, fqProc)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FQProcess _ _ _ ->
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder error "CspCASL.StatAnaCSP.anaProcTerm: Unexpected FQProcess"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL "named process" term. Return the
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder-- permitted alphabet of the process and also a list of the fully qualified
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- version of the inputted terms.
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederanaNamedProc :: PROCESS -> PROCESS_NAME -> [TERM ()] -> ProcVarMap ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini State CspCASLSign (CommAlpha, [TERM ()])
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaNamedProc proc pn terms procVars = do
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let ext = extendedInfo sig
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder procDecls = procSet ext
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder prof = pn `Map.lookup` procDecls
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just (ProcProfile varSorts permAlpha) ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini if (length terms) == (length varSorts)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder then do fqTerms <-
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder mapM (anaNamedProcTerm procVars) (zip terms varSorts)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Return the permitted alphabet of the process and
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- the fully qualifed terms
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (permAlpha, fqTerms)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini else do let err = "wrong number of arguments in named process"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini addDiags [mkDiag Error err proc]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Return the empty alphabet and the original
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- terms. There is an error in the spec.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (S.empty, terms)
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder do addDiags [mkDiag Error "unknown process name" proc]
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder -- Return the empty alphabet and the original
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- terms. There is an error in the spec.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (S.empty, terms)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Statically analysis a CASL term occurring in a CspCASL "named
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- process" term.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaNamedProcTerm :: ProcVarMap -> ((TERM ()), SORT) ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini State CspCASLSign (TERM ())
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaNamedProcTerm pm (t, expSort) = do
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini mt <- anaTermCspCASL pm t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> return t -- CASL term analysis failed. Use old term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- as the fully qualified term, there is a
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- error in the spec anyway.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (Just at) -> do at' <- ccTermCast at expSort -- attempt cast;
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini Nothing -> -- Use old term as the fully
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- qualified term, there is a error
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- in the spec anyway.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (Just at'') -> return at'' -- Use the fully
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- (possibly cast)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Static analysis of event sets and communication types
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Statically analyse a CspCASL event set. Returns the alphabet of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- the event set and a fully qualified version of the event set.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinianaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinianaEventSet eventSet =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini case eventSet of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini EventSet es r ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do sig <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- fqEsElems is built the reversed order for efficiency.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (comms, fqEsElems) <- Monad.foldM (anaCommType sig)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini vds <- gets envDiags
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini put sig { envDiags = vds }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- reverse the list inside the event set
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (comms, FQEventSet (reverse fqEsElems) r)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder FQEventSet _ _ ->
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini error "CspCASL.StatAnaCSP.anaEventSet: Unexpected FQEventSet"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Statically analyse a CspCASL communication type. Returns the
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- extended alphabet and the extended list of fully qualified event
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- set elements - [CommType].
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederanaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> COMM_TYPE ->
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini State CspCASLSign (CommAlpha, [CommType])
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinianaCommType sig (alpha, fqEsElems) ct =
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder if ctSort `S.member` (sortSet sig)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini then -- ct is a sort name; insert sort into alpha and add a sort
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini -- to the fully qualified event set elements.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini do let newAlpha = S.insert (CommTypeSort ctSort) alpha
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let newFqEsElems = (CommTypeSort ctSort) : fqEsElems
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (newAlpha, newFqEsElems)
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else -- ct not a sort name, so should be a channel name
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini case Map.lookup ct (chans $ extendedInfo sig) of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini Just s -> -- ct is a channel name; insert typed chan name
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- into alpha and add typed channel to the fully
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- qualified event set elemenets.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let newAlpha = S.insert (mkTypedChan ct s) alpha
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder newFqEsElems = (mkTypedChan ct s) : fqEsElems
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini in return (newAlpha, newFqEsElems)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini Nothing -> do let err = "not a sort or channel name"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini addDiags [mkDiag Error err ct]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- failed, thus error in spec, return the
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- unmodified alphabet and the unmodifled
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini -- fully qualified event set elements.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (alpha, fqEsElems)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini where ctSort = simpleIdToId ct
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini mkTypedChan c s = CommTypeChan $ TypedChanName c s
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- Static analysis of events
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Statically analyse a CspCASL event. Returns a constituent
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- communication alphabet of the event, mapping for any new
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- locally bound variables and a fully qualified version of the event.
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinianaEvent :: EVENT -> ProcVarMap ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinianaEvent e vars =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini TermEvent t range ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Term event" e]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, newVars, fqTerm) <- anaTermEvent t vars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqEvent = FQEvent e Nothing fqTerm range
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (alpha, newVars, fqEvent)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini InternalPrefixChoice v s range ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Internal prefix event" e]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, newVars, fqVar) <- anaPrefixChoice v s
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqEvent = FQEvent e Nothing fqVar range
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (alpha, newVars, fqEvent)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ExternalPrefixChoice v s range ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "External prefix event" e]
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini (alpha, newVars, fqVar) <- anaPrefixChoice v s
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder let fqEvent = FQEvent e Nothing fqVar range
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return (alpha, newVars, fqEvent)
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder ChanSend c t range ->
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder do addDiags [mkDiag Debug "Channel send event" e]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- mfqChan is a maybe fully qualified
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- channel. It will be Nothing if
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder -- annChanSend failed - i.e. we forget
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- about the channel.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, newVars, mfqChan, fqTerm) <- anaChanSend c t vars
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqEvent = FQEvent e mfqChan fqTerm range
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (alpha, newVars, fqEvent)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ChanNonDetSend c v s range ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini do addDiags [mkDiag Debug "Channel nondeterministic send event" e]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- mfqChan is the same as in chanSend case.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- fqVar is the fully qualfied version of the variable.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder let fqEvent = FQEvent e mfqChan fqVar range
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (alpha, newVars, fqEvent)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ChanRecv c v s range ->
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder do addDiags [mkDiag Debug "Channel receive event" e]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- mfqChan is the same as in chanSend case.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- fqVar is the fully qualfied version of the variable.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let fqEvent = FQEvent e mfqChan fqVar range
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (alpha, newVars, fqEvent)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder FQEvent _ _ _ _ ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini error "CspCASL.StatAnaCSP.anaEvent: Unexpected FQEvent"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder-- | Statically analyse a CspCASL term event. Returns a constituent
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian Maeder-- communication alphabet of the event and a mapping for any new
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder-- locally bound variables and the fully qualified version of the
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian MaederanaTermEvent :: (TERM ()) -> ProcVarMap ->
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederanaTermEvent t vars = do
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder mt <- anaTermCspCASL vars t
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let (alpha, t') = case mt of
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder -- return the alphabet and the fully qualified term
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian Maeder Just at -> ([(CommTypeSort (sortOfTerm at))], at)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder -- return the empty alphabet and the original term
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder Nothing -> ([], t)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder-- | Statically analyse a CspCASL internal or external prefix choice
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder-- event. Returns a constituent communication alphabet of the event
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini-- and a mapping for any new locally bound variables and the fully
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini-- qualified version of the variable.
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinianaPrefixChoice :: VAR -> SORT ->
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinianaPrefixChoice v s = do
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini checkSorts [s] -- check sort is known
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder let alpha = S.singleton $ CommTypeSort s
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let binding = Map.singleton v s
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let fqVar = Qual_var v s nullRange
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder return (alpha, binding, fqVar)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder-- | Statically analyse a CspCASL channel send event. Returns a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- constituent communication alphabet of the event, a mapping for
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- any new locally bound variables, a fully qualified channel (if
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- possible) and the fully qualified version of the term.
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederanaChanSend :: CHANNEL_NAME -> (TERM ()) -> ProcVarMap ->
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder State CspCASLSign (CommAlpha, ProcVarMap,
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder (Maybe (CHANNEL_NAME, SORT)), TERM ())
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyanaChanSend c t vars = do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder let ext = extendedInfo sig
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly case c `Map.lookup` (chans ext) of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly Nothing -> do
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly addDiags [mkDiag Error "unknown channel" c]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- Use old term as the fully qualified term and forget about the
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- channel, there is an error in the spec
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Just chanSort -> do
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly mt <- anaTermCspCASL vars t
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Nothing -> -- CASL analysis failed. Use old term as the fully
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -- qualified term and forget about the channel,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly -- there is an error in the spec.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder do mc <- ccTermCast at chanSort
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Nothing -> -- cast failed. Use old term as the fully
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- qualified term, and forget about the
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- channel there is an error in the spec.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder do let castSort = sortOfTerm ct
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder alpha = [CommTypeSort castSort
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ,CommTypeChan $ TypedChanName c castSort
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- Use the real fully qualified term. We do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- not want to use a cast term here. A cast
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- must be possible, but we do not want to
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just (c, chanSort), at)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Statically analyse a CspCASL "binding" channel event (which is
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- either a channel nondeterministic send event or a channel receive
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- event). Returns a constituent communication alphabet of the event,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- a mapping for any new locally bound variables, a fully qualified
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- channel (if possible) and the fully qualified version of the
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaChanBinding :: CHANNEL_NAME -> VAR -> SORT ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder State CspCASLSign( CommAlpha,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Maybe (CHANNEL_NAME, SORT)), TERM ()
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaChanBinding c v s = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder checkSorts [s] -- check sort is known
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let ext = extendedInfo sig
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder case c `Map.lookup` (chans ext) of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Nothing -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addDiags [mkDiag Error "unknown channel" c]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- No fully qualified channel, use Nothing - there is a error in
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- the spec anyway. Use the real fully qualified variable
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- version with a nullRange.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (S.empty, Map.empty, Nothing, (Qual_var v s nullRange))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just chanSort -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder if s `S.member` (chanSort `S.insert` (subsorts chanSort))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder then do let alpha = [CommTypeSort s
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ,CommTypeChan (TypedChanName c s)]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let binding = [(v, s)]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- Return the alphabet, var mapping, the fully
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- qualfied channel and fully qualfied
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- variable. Notice that the fully qualified
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- channel's sort should be the lowest sort we can
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- communicate in i.e. the sort of the variable.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (S.fromList alpha, Map.fromList binding,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Just (c,s)), (Qual_var v s nullRange))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder else do let err = "sort not a subsort of channel's sort"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addDiags [mkDiag Error err s]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- There is a error in the spec, but return
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- the alphabet, var mapping, the fully
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- qualfied channel and fully qualfied
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- variable - as we can.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Qual_var v s nullRange))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder where subsorts = Rel.predecessors (sortRel sig)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- Static analysis of renaming and renaming items
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Statically analyse a CspCASL renaming. Returns the alphabet and
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | the fully qualified renaming.
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaRenaming renaming = case renaming of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Renaming r -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (al, fqRenamingTermsMaybes) <- Monad.foldM anaRenamingItem (S.empty, []) r
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (al, FQRenaming fqRenamingTermsMaybes)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder FQRenaming _ ->
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder error "CspCASL.StatAnaCSP.anaRenaming: Unexpected FQRenaming"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder-- | Statically analyse a CspCASL renaming item. Return the alphabet
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder-- | and the fully qualified list of renaming functions and predicates.
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederanaRenamingItem :: (CommAlpha, [TERM ()]) -> Id ->
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder State CspCASLSign (CommAlpha, [TERM ()])
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaRenamingItem (inAl, fqRenamingTerms) ri = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- BUG -- too many nothings - should only be one
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder totOps <- getUnaryOpsById ri Total
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder if (not $ S.null totOps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder then return (inAl `S.union` totOps, fqRenamingTerms)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder parOps <- getUnaryOpsById ri Partial
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder if not (S.null parOps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder then return (inAl `S.union` parOps, fqRenamingTerms)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder preds <- getBinPredsById ri
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder if not (S.null preds)
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder then return (inAl `S.union` preds, fqRenamingTerms)
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder let err = "renaming item not a binary "
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ "operation or predicate name"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addDiags [mkDiag Error err ri]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- return the original alphabet and the original fully
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly -- qualified terms (renamings) with out any modification
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly -- as there is an error in the spec.
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly return (inAl, fqRenamingTerms)
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- | Given a CASL identifier and a `function kind' (total or partial),
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- find all unary operations of that kind with that name in the CASL
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- signature, and return a set of corresponding communication types
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- for those operations.
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillygetUnaryOpsById :: Id -> OpKind -> State CspCASLSign (S.Set CommType)
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillygetUnaryOpsById ri kind = do
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly let opsWithId = Map.findWithDefault S.empty ri (opMap sig)
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly binOpsKind = S.filter (isBin kind) opsWithId
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly cts = S.map CommTypeSort $ S.fold opSorts S.empty binOpsKind
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly where isBin k ot = (k == opKind ot) && (1 == (length (opArgs ot)))
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly opSorts o inS = inS `S.union` (S.fromList ((opArgs o) ++ [opRes o]))
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- | Given a CASL identifier find all binary predicates with that name
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- in the CASL signature, and return a set of corresponding
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'Reilly-- communication types for those predicates.
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillygetBinPredsById :: Id -> State CspCASLSign (S.Set CommType)
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillygetBinPredsById ri = do
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly let predsWithId = Map.findWithDefault S.empty ri (predMap sig)
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly binPreds = S.filter isBin predsWithId
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly cts = S.map CommTypeSort $ S.fold predSorts S.empty binPreds
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly where isBin ot = (2 == (length (predArgs ot)))
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly predSorts p inS = inS `S.union` (S.fromList (predArgs p))
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly-- | Given two CspCASL communication alphabets, check that the first's
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly-- subsort closure is a subset of the second's subsort closure.
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillycheckCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String ->
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly State CspCASLSign ()
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillycheckCommAlphaSub sub super proc context = do
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly let extras = ((closeCspCommAlpha sig sub) `S.difference`
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly (closeCspCommAlpha sig super))
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly then do return ()
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly else do let err = ("Communication alphabet subset violations (" ++
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly context ++ "): " ++ (show $ S.toList extras))
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly addDiags [mkDiag Error err proc]
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'Reilly-- Static analysis of CASL terms occurring in CspCASL process terms.
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder-- | Statically analyse a CASL term appearing in a CspCASL process;
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder-- any in-scope process variables are added to the signature before
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder-- performing the analysis.
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederanaTermCspCASL :: ProcVarMap -> (TERM ()) ->
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder State CspCASLSign (Maybe (TERM ()))
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederanaTermCspCASL pm t = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let newVars = Map.union pm (varMap sig)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder sigext = sig { varMap = newVars }
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Result ds mt = anaTermCspCASL' sigext t
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederidSetOfSig :: CspCASLSign -> IdSets
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian MaederidSetOfSig sig =
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian Maeder unite [mkIdSets (allConstIds sig) (allOpIds sig) $ allPredIds sig]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Statically analyse a CASL term in the context of a CspCASL
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder-- signature. If successful, returns a fully-qualified term.
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaTermCspCASL' :: CspCASLSign -> TERM () -> Result (TERM ())
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaTermCspCASL' sig trm = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let ga = globAnnos sig
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder mix = extendMix (Map.keysSet $ varMap sig)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder emptyMix { mixRules = makeRules ga $ idSetOfSig sig }
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder resT <- resolveMixfix (putParen mix) (mixResolve mix)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ga (mixRules mix) trm
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder oneExpTerm (const return) sig resT
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Attempt to cast a CASL term to a particular CASL sort.
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederccTermCast :: (TERM ()) -> SORT -> State CspCASLSign (Maybe (TERM ()))
a81140cdef15cb5de8256e310eae035f98a054bfChristian MaederccTermCast t cSort =
a81140cdef15cb5de8256e310eae035f98a054bfChristian Maeder if termSort == (cSort)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder then return (Just t)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder else do sig <- get
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian Maeder if Rel.member termSort cSort (sortRel sig)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder then do let err = "upcast term to " ++ (show cSort)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addDiags [mkDiag Debug err t]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (Just (Sorted_term t cSort (getRange t)))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder else if Rel.member cSort termSort (sortRel sig)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini then do let err = "downcast term to " ++ (show cSort)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini addDiags [mkDiag Debug err t]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (Just (Cast t cSort (getRange t)))
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini else do let err = "can't cast term to sort " ++
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder addDiags [mkDiag Error err t]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return Nothing
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder where termSort = (sortOfTerm t)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- Static analysis of CASL formulae occurring in CspCASL process
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | Statically analyse a CASL formula appearing in a CspCASL process;
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- any in-scope process variables are added to the signature before
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- performing the analysis.
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaFormulaCspCASL :: ProcVarMap -> (FORMULA ()) ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder State CspCASLSign (Maybe (FORMULA ()))
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederanaFormulaCspCASL pm f = do
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder addDiags [mkDiag Debug "anaFormulaCspCASL" f]
let newVars = Map.union pm (varMap sig)
mix = extendMix (Map.keysSet $ varMap sig)
Conjunction fs _ -> S.unions (map formulaComms fs)
Disjunction fs _ -> S.unions (map formulaComms fs)
Implication f1 f2 _ _ -> (formulaComms f1) `S.union` (formulaComms f2)
Equivalence f1 f2 _ -> (formulaComms f1) `S.union` (formulaComms f2)
Definedness t _ -> S.singleton (CommTypeSort (sortOfTerm t))
Existl_equation t1 t2 _ -> S.fromList [CommTypeSort (sortOfTerm t1),
Strong_equation t1 t2 _ -> S.fromList [CommTypeSort (sortOfTerm t1),
Membership t s _ -> S.fromList [CommTypeSort (sortOfTerm t),
Mixfix_formula t -> S.singleton (CommTypeSort (sortOfTerm t))
_ -> S.empty