bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : Static analysis of CspCASL
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : (c) Andy Gimblett, Liam O'Reilly, Markus Roggenbach,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Swansea University 2008, C. Maeder, DFKI 2011
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederMaintainer : Christian.Maeder@dfki.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStatic analysis of CSP-CASL specifications, following "Tool Support
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettfor CSP-CASL", MPhil thesis by Andy Gimblett, 2008.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified CspCASL.LocalTop as LocalTop
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified Data.Set as Set
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport qualified Data.Map as Map
bcd914850de931848b86d7728192a149f9c0108bChristian Maedertype CspBasicSpec = BASIC_SPEC CspBasicExt () CspSen
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | The first element of the returned pair (CspBasicSpec) is the same
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederas the inputted version just with some very minor optimisations -
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedernone in our case, but for CASL - brackets are otimized. This all
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthat happens, the mixfixed terms are still mixed fixed terms in
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthe returned version. -}
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettbasicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederbasicAnalysisCspCASL inp@(_, insig, _) = do
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder (bs, ExtSign sig syms, sens) <- basicAnaAux inp
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder -- check for local top elements in the subsort relation
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder appendDiags $ LocalTop.checkLocalTops $ sortRel sig
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder let ext = extendedInfo sig
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return (bs, ExtSign sig $ Set.unions
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder $ Set.map caslToCspSymbol syms
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder : toSymbolSet (diffCspSig ext $ extendedInfo insig), sens)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederbasicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder basicAnalysis (const return) ana_BASIC_CSP (const return) emptyMix
bcd914850de931848b86d7728192a149f9c0108bChristian Maederana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederana_BASIC_CSP mix bs = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder let caslMix = emptyMix
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder { mixRules = mixRules mix }
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder Channels cs _ -> mapM_ (anaChanDecl . item) cs
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ProcItems ps _ -> mapM_ (anaProcItem caslMix) ps
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of channel declarations
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL channel declaration.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyanaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy GimblettanaChanDecl (ChannelDecl chanNames chanSort) = do
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett checkSorts [chanSort] -- check channel sort is known
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let ext = extendedInfo sig
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett oldChanMap = chans ext
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder newChanMap <- foldM (anaChannelName chanSort) oldChanMap chanNames
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder put sig2 { extendedInfo = ext { chans = newChanMap }}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL channel name.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign ChanNameMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettanaChannelName s m chanName = do
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder if Set.member chanName (sortSet sig)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let err = "channel name already in use as a sort name"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder addDiags [mkDiag Error err chanName]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder when (MapSet.member chanName s m) $
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder addDiags [mkDiag Warning "redeclared channel" chanName]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder return $ MapSet.insert chanName s m
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of process items
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL process item.
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcItem mix annotedProcItem = case item annotedProcItem of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Proc_Decl name argSorts alpha -> anaProcDecl name argSorts alpha
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder Proc_Defn name args alpha procTerm -> do
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder let vs = flatVAR_DECLs args
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly argSorts = map snd vs
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly alpha' = case alpha of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly ProcAlphabet alpha'' -> Set.fromList alpha''
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly procProfile = ProcProfile argSorts alpha'
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly pn = ParmProcname (FQ_PROCESS_NAME name procProfile) $ map fst vs
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly anaProcDecl name argSorts alpha
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaProcEq mix annotedProcItem pn procTerm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Proc_Eq parmProcName procTerm ->
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaProcEq mix annotedProcItem parmProcName procTerm
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of process declarations
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL process declaration.
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederanaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -> State CspCASLSign ()
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaProcDecl name argSorts comms = do
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let ext = extendedInfo sig
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett oldProcDecls = procSet ext
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly newProcDecls <- do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- new process declation
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly profile <- anaProcAlphabet argSorts comms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- we no longer add (channel and) proc symbols to the CASL signature
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly if isNameInProcNameMap name profile oldProcDecls
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- Check the name (with profile) is new (for warning only)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then -- name with profile already in signature
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do let warn = "process name redeclared with same profile '" ++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (printProcProfile profile) ++ "':"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly addDiags [mkDiag Warning warn name]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return oldProcDecls
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else {- New name with profile - add the name to the signature in the
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ addProcNameToProcNameMap name profile oldProcDecls
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder put sig2 { extendedInfo = ext {procSet = newProcDecls }}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of process equations
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Find a profile for a process name. Either the profile is given via a parsed
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederfully qualified process name, in which case we check everything is valid and
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthe process name with the profile is known. Or its a plain process name where
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maederwe must deduce a unique profile if possible. We also know how many variables
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder/ parameters the process name has. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly State CspCASLSign (Maybe ProcProfile)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfindProfileForProcName pn numParams procNameMap =
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder FQ_PROCESS_NAME pn' (ProcProfile argSorts comms) -> do
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder procProfile <- anaProcAlphabet argSorts $ ProcAlphabet $ Set.toList comms
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder if MapSet.member pn' procProfile procNameMap
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly then return $ Just procProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly addDiags [mkDiag Error
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Fully qualified process name not in signature" pn]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PROCESS_NAME pn' ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let resProfile = getUniqueProfileInProcNameMap pn' numParams procNameMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in case resultToMaybe resProfile of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do addDiags $ diags resProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just profile' ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Just profile'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Analyse a process name an return a fully qualified one if possible. We also
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederknow how many variables / parameters the process name has. -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederanaProcName :: FQ_PROCESS_NAME -> Int
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederanaProcName pn numParams = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let ext = extendedInfo sig
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly procDecls = procSet ext
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly simpPn = procNameToSimpProcName pn
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly maybeProf <- findProfileForProcName pn numParams procDecls
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case maybeProf of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> return Nothing
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Just procProfile ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- We now construct the real fully qualified process name
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly return $ Just $ FQ_PROCESS_NAME simpPn procProfile
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL process equation.
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcEq :: Mix b s () () -> Annoted a -> PARM_PROCNAME -> PROCESS
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> State CspCASLSign ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcEq mix a (ParmProcname pn vs) proc =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- the 'annoted a' contains the annotation of the process equation. We do not
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder care what the underlying item is in the annotation (but it probably will be
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder the proc eq) -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly maybeFqPn <- anaProcName pn (length vs)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case maybeFqPn of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Only analyse a process if its name and profile is known
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> return ()
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PROCESS_NAME _ ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly error "CspCasl.StatAnaCSP.anaProcEq: Impossible case"
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FQ_PROCESS_NAME _ (ProcProfile argSorts commAlpha) -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly gVars <- anaProcVars pn
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly argSorts vs {- compute global
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder vars Change a procVarList to a FQProcVarList We do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder not care about the range as we are building fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder qualified variables and they have already been
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder checked to be ok. -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let mkFQProcVar (v, s) = Qual_var v s nullRange
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder fqGVars = map mkFQProcVar gVars
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (termAlpha, fqProc) <-
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaProcTerm mix proc (Map.fromList gVars) Map.empty
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly checkCommAlphaSub termAlpha commAlpha proc "process equation"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- put CspCASL Sentences back in to the state with new sentence
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder BUG - What should the constituent alphabet be for this
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder process? probably the same as the inner one! -}
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder addSentences [makeNamedSen $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- We take the annotated item and replace the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder inner item, thus preserving the annotations. We
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder then take this annotated sentence and make it a
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder named sentence in accordance to the (if
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder existing) name in the annotations. -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder a {item = ExtFORMULA
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly $ ProcessEq fqPn fqGVars commAlpha fqProc}]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Statically analyse a CspCASL process equation's global variable names.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly State CspCASLSign ProcVarList
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyanaProcVars pn ss vs =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let msg str = addDiags [mkDiag Error ("process name applied to " ++ str) pn]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in fmap reverse $ case compare (length ss) $ length vs of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder LT -> msg "too many arguments"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GT -> msg "not enough arguments"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder EQ -> foldM anaProcVar [] (zip vs ss)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Statically analyse a CspCASL process-global variable name.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyanaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederanaProcVar old (v, s) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if v `elem` map fst old
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder addDiags [mkDiag Error "Process argument declared more than once" v]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else return ((v, s) : old)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of process terms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- BUG in fucntion below
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedernot returing FQProcesses
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederStatically analyse a CspCASL process term.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederThe process that is returned is a fully qualified process. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcTerm :: Mix b s () () -> PROCESS -> ProcVarMap -> ProcVarMap
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> State CspCASLSign (CommAlpha, PROCESS)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaProcTerm mix proc gVars lVars = case proc of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly NamedProcess name args r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Named process" proc]
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly (fqName, al, fqArgs) <-
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaNamedProc mix proc name args (lVars `Map.union` gVars)
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly let fqProc = FQProcess (NamedProcess fqName fqArgs r) al r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (al, fqProc)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Skip" proc]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let fqProc = FQProcess (Skip r) Set.empty r
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (Set.empty, fqProc)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Stop" proc]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let fqProc = FQProcess (Stop r) Set.empty r
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (Set.empty, fqProc)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Div" proc]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let fqProc = FQProcess (Div r) Set.empty r
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (Set.empty, fqProc)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Run" proc]
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (comms, fqEs) <- anaEventSet es
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let fqProc = FQProcess (Run fqEs r) comms r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (comms, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Chaos es r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Chaos" proc]
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (comms, fqEs) <- anaEventSet es
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let fqProc = FQProcess (Chaos fqEs r) comms r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (comms, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly PrefixProcess e p r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Prefix" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (evComms, rcvMap, fqEvent) <-
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaEvent mix e (lVars `Map.union` gVars)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (comms, pFQTerm) <-
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder anaProcTerm mix p gVars (rcvMap `Map.union` lVars)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = comms `Set.union` evComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (PrefixProcess fqEvent pFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Sequential p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Sequential" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars Map.empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (Sequential pFQTerm qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly InternalChoice p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "InternalChoice" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (InternalChoice pFQTerm qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ExternalChoice p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "ExternalChoice" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Interleaving p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Interleaving" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (Interleaving pFQTerm qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly SynchronousParallel p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Synchronous" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (SynchronousParallel pFQTerm
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly GeneralisedParallel p es q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Generalised parallel" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (synComms, fqEs) <- anaEventSet es
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = Set.unions [pComms, qComms, synComms]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (GeneralisedParallel pFQTerm fqEs qFQTerm r)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly AlphabetisedParallel p esp esq q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Alphabetised parallel" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (pSynComms, fqEsp) <- anaEventSet esp
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (qSynComms, fqEsq) <- anaEventSet esq
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett checkCommAlphaSub qSynComms qComms proc
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett "alphabetised parallel, right"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` qComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly qFQTerm r) newAlpha r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Hiding p es r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Hiding" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (hidComms, fqEs) <- anaEventSet es
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (pComms `Set.union` hidComms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , FQProcess (Hiding pFQTerm fqEs r)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (pComms `Set.union` hidComms) r)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly RenamingProcess p renaming r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Renaming" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly (renAlpha, fqRenaming) <- anaRenaming renaming
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newAlpha = pComms `Set.union` renAlpha
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly fqProc = FQProcess (RenamingProcess pFQTerm fqRenaming r)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (pComms `Set.union` renAlpha) r
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return (newAlpha, fqProc)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ConditionalProcess f p q r ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do addDiags [mkDiag Debug "Conditional" proc]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- mfs is the fully qualified formula version of f
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder mfs <- anaFormulaCspCASL mix (gVars `Map.union` lVars) f
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let fFQ = fromMaybe f mfs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fComms = maybe Set.empty formulaComms mfs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder newAlpha = Set.unions [pComms, qComms, fComms]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqProc = FQProcess (ConditionalProcess fFQ pFQTerm qFQTerm r)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly return (newAlpha, fqProc)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FQProcess {} ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly error "CspCASL.StatAnaCSP.anaProcTerm: Unexpected FQProcess"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL "named process" term. Return the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederpermitted alphabet of the process and also a list of the fully qualified
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederversion of the inputted terms.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederBUG !!! the FQ_PROCESS_NAME may actually need to be a simple process name -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaNamedProc :: Mix b s () () -> PROCESS -> FQ_PROCESS_NAME -> [TERM ()]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> ProcVarMap -> State CspCASLSign (FQ_PROCESS_NAME, CommAlpha, [TERM ()])
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaNamedProc mix proc pn terms procVars = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly maybeFqPn <- anaProcName pn (length terms)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case maybeFqPn of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- Return the empty alphabet and the original
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder terms. There is an error in the spec. -}
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly return (pn, Set.empty, terms)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly PROCESS_NAME _ ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly error "CspCasl.StatAnaCSP.anaNamedProc: Impossible case"
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FQ_PROCESS_NAME _ (ProcProfile argSorts permAlpha) ->
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly if length terms == length argSorts
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly mapM (anaNamedProcTerm mix procVars) (zip terms argSorts)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- Return the permitted alphabet of the process and
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder the fully qualifed terms -}
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly return (fqPn, permAlpha, fqTerms)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let err = "Wrong number of arguments in named process"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder addDiags [mkDiag Error err proc]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- Return the empty alphabet and the original
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder terms. There is an error in the spec. -}
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly return (pn, Set.empty, terms)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analysis a CASL term occurring in a CspCASL "named
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederprocess" term. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaNamedProcTerm :: Mix b s () () -> ProcVarMap -> (TERM (), SORT)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> State CspCASLSign (TERM ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaNamedProcTerm mix pm (t, expSort) = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder mt <- anaTermCspCASL mix pm t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> return t {- CASL term analysis failed. Use old term
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder as the fully qualified term, there is a
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder error in the spec anyway. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just at -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let Result ds at' = ccTermCast at expSort sig -- attempt cast;
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> {- Use old term as the fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder qualified term, there is a error
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in the spec anyway. -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just at'' -> return at'' {- Use the fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (possibly cast)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of event sets and communication types
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL event set. Returns the alphabet of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthe event set and a fully qualified version of the event set. -}
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyanaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyanaEventSet eventSet =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case eventSet of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly EventSet es r ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly do sig <- get
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- fqEsElems is built the reversed order for efficiency.
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder (comms, fqEsElems) <- foldM (anaCommType sig)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly vds <- gets envDiags
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly put sig { envDiags = vds }
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- reverse the list inside the event set
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder return (comms, EventSet (reverse fqEsElems) r)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a proc alphabet (i.e., a list of channel and sort
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederidentifiers) to yeild a list of sorts and typed channel names. We also check
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthe parameter sorts and actually construct a process profile. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaProcAlphabet :: PROC_ARGS -> PROC_ALPHABET ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly State CspCASLSign ProcProfile
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederanaProcAlphabet argSorts (ProcAlphabet commTypes) = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder checkSorts argSorts {- check argument sorts are known build alphabet: set of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder CommType values. We do not need the fully qualfied commTypes that are
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder returned (these area used for analysing Event Sets) -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (alpha, _ ) <- foldM (anaCommType sig) (Set.empty, []) commTypes
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly let profile = reduceProcProfile (sortRel sig) (ProcProfile argSorts alpha)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return profile
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder{- | Statically analyse a CspCASL communication type. Returns the
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maederextended alphabet and the extended list of fully qualified event
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maederset elements - [CommType]. -}
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederanaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> CommType ->
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder State CspCASLSign (CommAlpha, [CommType])
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederanaCommType sig (alpha, fqEsElems) ct =
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder let res = return (Set.insert ct alpha, ct : fqEsElems)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder old = return (alpha, fqEsElems)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder getChSrts ch = Set.toList $ MapSet.lookup ch $ chans
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder $ extendedInfo sig
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder chRes ch rs = let tcs = map (CommTypeChan . TypedChanName ch) rs
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder in return (Set.union alpha $ Set.fromList tcs, tcs ++ fqEsElems)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder in case ct of
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder CommTypeSort sid -> if Set.member sid (sortSet sig) then res else
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder case getChSrts sid of
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder addDiags [mkDiag Error "unknown sort or channel" sid]
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder cs -> chRes sid cs
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder CommTypeChan (TypedChanName ch sid) ->
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder if Set.member sid (sortSet sig) then
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder case getChSrts ch of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder addDiags [mkDiag Error "unknown channel" ch]
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder ts -> case filter (\ s -> s == sid || Set.member sid
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder (subsortsOf s sig) || Set.member s (subsortsOf sid sig)) ts of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder let mess = "found no suitably sort '"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder ++ shows sid "' for channel"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder addDiags [mkDiag Error mess ch]
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder rs -> chRes ch rs
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder let mess = "unknow sort '" ++ shows sid "' for channel"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder addDiags [mkDiag Error mess ch]
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of events
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL event. Returns a constituent
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedercommunication alphabet of the event, mapping for any new
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederlocally bound variables and a fully qualified version of the event. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaEvent :: Mix b s () () -> EVENT -> ProcVarMap
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaEvent mix e vars =
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly TermEvent t range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "Term event" e]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (alpha, newVars, fqTerm) <- anaTermEvent mix t vars
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQTermEvent fqTerm range
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return (alpha, newVars, fqEvent)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly InternalPrefixChoice v s range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "Internal prefix event" e]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (alpha, newVars, fqVar) <- anaPrefixChoice v s
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQInternalPrefixChoice fqVar range
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return (alpha, newVars, fqEvent)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ExternalPrefixChoice v s range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "External prefix event" e]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (alpha, newVars, fqVar) <- anaPrefixChoice v s
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQExternalPrefixChoice fqVar range
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly return (alpha, newVars, fqEvent)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ChanSend c t range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "Channel send event" e]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- mfqChan is a maybe fully qualified
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder channel. It will be Nothing if
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder annChanSend failed - i.e. we forget
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder about the channel. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (alpha, newVars, mfqChan, fqTerm) <- anaChanSend mix c t vars
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQChanSend mfqChan fqTerm range
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly return (alpha, newVars, fqEvent)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ChanNonDetSend c v s range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "Channel nondeterministic send event" e]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- mfqChan is the same as in chanSend case.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqVar is the fully qualfied version of the variable. -}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQChanNonDetSend mfqChan fqVar range
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return (alpha, newVars, fqEvent)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ChanRecv c v s range ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly do addDiags [mkDiag Debug "Channel receive event" e]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- mfqChan is the same as in chanSend case.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fqVar is the fully qualfied version of the variable. -}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let fqEvent = FQChanRecv mfqChan fqVar range
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly return (alpha, newVars, fqEvent)
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly "CspCASL.StatAnaCSP.anaEvent: Unexpected Fully qualified event"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL term event. Returns a constituent
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedercommunication alphabet of the event and a mapping for any new
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederlocally bound variables and the fully qualified version of the
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermEvent :: Mix b s () () -> TERM () -> ProcVarMap
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermEvent mix t vars = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder mt <- anaTermCspCASL mix vars t
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly let (alpha, t') = case mt of
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly -- return the alphabet and the fully qualified term
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just at -> ([CommTypeSort (sortOfTerm at)], at)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly -- return the empty alphabet and the original term
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly Nothing -> ([], t)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL internal or external prefix choice
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederevent. Returns a constituent communication alphabet of the event
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederand a mapping for any new locally bound variables and the fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederqualified version of the variable. -}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyanaPrefixChoice :: VAR -> SORT ->
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyanaPrefixChoice v s = do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly checkSorts [s] -- check sort is known
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let alpha = Set.singleton $ CommTypeSort s
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let binding = Map.singleton v s
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let fqVar = Qual_var v s nullRange
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return (alpha, binding, fqVar)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL channel send event. Returns a
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederconstituent communication alphabet of the event, a mapping for
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederany new locally bound variables, a fully qualified channel (if
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederpossible) and the fully qualified version of the term. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaChanSend :: Mix b s () () -> CHANNEL_NAME -> TERM () -> ProcVarMap
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaChanSend mix c t vars = do
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett let ext = extendedInfo sig
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly msg = "CspCASL.StatAnaCSP.anaChanSend: Channel Error"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder case Set.toList $ MapSet.lookup c $ chans ext of
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett addDiags [mkDiag Error "unknown channel" c]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- Use old term as the fully qualified term and forget about the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder channel, there is an error in the spec -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder chanSorts -> do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder mt <- anaTermCspCASL mix vars t
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- CASL analysis failed. Use old term as the fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder qualified term and forget about the channel,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder there is an error in the spec. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just at -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let rs = map (\ s -> ccTermCast at s sig) chanSorts
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder addDiags $ concatMap diags rs
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case filter (isJust . maybeResult . fst) $ zip rs chanSorts of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- cast failed. Use old term as the fully
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder qualified term, and forget about the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder channel there is an error in the spec. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [(_, castSort)] ->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let alpha = [ CommTypeSort castSort
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , CommTypeChan $ TypedChanName c castSort]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- Use the real fully qualified term. We do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder not want to use a cast term here. A cast
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder must be possible, but we do not want to
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly in return (Set.fromList alpha, Map.empty, (c, castSort), at)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder cts -> do -- fail due to an ambiguous chan sort
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder addDiags [mkDiag Error
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ("ambiguous channel sorts " ++ show (map snd cts)) t]
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Use old term as the fully qualified term and forget about the
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly channel, there is an error in the spec. -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'ReillygetDeclaredChanSort :: (CHANNEL_NAME, SORT) -> CspCASLSign -> Result SORT
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'ReillygetDeclaredChanSort (c, s) sig =
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly let cm = chans $ extendedInfo sig
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [] -> mkError "unknown channel" c
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder css -> case filter (\ cs -> cs == s || Set.member s (subsortsOf cs sig))
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly [] -> mkError "sort not a subsort of channel's sort" s
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly [cs] -> return cs
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly fcs -> mkError ("ambiguous channel sorts " ++ show fcs) s
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL "binding" channel event (which is
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedereither a channel nondeterministic send event or a channel receive
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederevent). Returns a constituent communication alphabet of the event,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedera mapping for any new locally bound variables, a fully qualified
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reillychannel and the fully qualified version of the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederanaChanBinding :: CHANNEL_NAME -> VAR -> SORT
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
9582375827616730f146b77f9d5a4fd0cc78bc47Andy GimblettanaChanBinding c v s = do
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett checkSorts [s] -- check sort is known
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let qv = Qual_var v s nullRange
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly fqChan = (c, s)
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly Result ds ms = getDeclaredChanSort fqChan sig
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly Nothing -> return (Set.empty, Map.empty, fqChan, qv)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let alpha = [CommTypeSort s, CommTypeChan (TypedChanName c s)]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder binding = [(v, s)]
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Return the alphabet, var mapping, the fully qualfied channel and
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly fully qualfied variable. Notice that the fully qualified
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly channel's sort should be the lowest sort we can communicate in
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly i.e. the sort of the variable. -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly in return (Set.fromList alpha, Map.fromList binding, fqChan, qv)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Static analysis of renaming and renaming items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL renaming. Returns the alphabet and
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederthe fully qualified renaming. -}
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyanaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyanaRenaming renaming = case renaming of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Renaming r -> do
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder fqRenamingTerms <- mapM anaRenamingItem r
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder let rs = concat fqRenamingTerms
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder return ( Set.map CommTypeSort $ Set.unions $ map alphaOfRename rs
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder , Renaming rs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaederalphaOfRename :: Rename -> Set.Set SORT
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaederalphaOfRename (Rename _ cm) = case cm of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Just (_, Just (s1, s2)) -> Set.fromList [s1, s2]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CspCASL renaming item. Return the alphabet
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederand the fully qualified list of renaming functions and predicates. -}
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaederanaRenamingItem :: Rename -> State CspCASLSign [Rename]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaederanaRenamingItem r@(Rename ri cm) = let
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder predToRen p = Rename ri $ Just (BinPred, Just p)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder opToRen (o, p) = Rename ri
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ Just (if o == Total then TotOp else PartOp, Just p)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder in case cm of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Just (k, ms) -> case k of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder BinPred -> do
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder ps <- getBinPredsById ri
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder let realPs = case ms of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Nothing -> ps
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Just p -> filter (== p) ps
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder when (null realPs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Error "renaming predicate not found" r]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder unless (isSingle realPs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Warning "multiple predicates found" r]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder return $ map predToRen realPs
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder os <- getUnaryOpsById ri
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder -- we ignore the user given op kind here!
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder let realOs = case ms of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Nothing -> os
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Just p -> filter ((== p) . snd) os
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder when (null realOs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Error "renaming operation not found" r]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder unless (isSingle realOs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Warning "multiple operations found" r]
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder when (k == TotOp) $
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder mapM_ (\ (o, (s1, s2)) -> when (o == Partial)
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder $ addDiags [mkDiag Error
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder ("operation of type '"
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder ++ shows s1 " -> "
dca96ff121cbc516fa9633b6603f9a094dab0a52Christian Maeder ++ shows s2 "' is not total") r]) realOs
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder return $ map opToRen realOs
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder Nothing -> do
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder ps <- getBinPredsById ri
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder os <- getUnaryOpsById ri
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder let rs = map predToRen ps ++ map opToRen os
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder when (null rs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Error "renaming predicate or operation not found" ri]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder unless (isSingle rs)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder $ addDiags [mkDiag Warning "multiple renamings found" ri]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder{- | Given a CASL identifier, find all
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maederunary operations with that name in the CASL signature, and return a
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maederlist of corresponding profiles, i.e. kind, argument sort and result sort. -}
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaedergetUnaryOpsById :: Id -> State CspCASLSign [(OpKind, (SORT, SORT))]
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaedergetUnaryOpsById ri = do
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder om <- gets opMap
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder return $ Set.fold (\ oty -> case oty of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder OpType k [s1] s2 -> ((k, (s1, s2)) :)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder _ -> id) [] $ MapSet.lookup ri om
7dcf630aadcf1a72b4ed877698f745cd8d4d3511Liam O'Reilly{- | Given a CASL identifier find all binary predicates with that name in the
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaederCASL signature, and return a list of corresponding profiles. -}
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian MaedergetBinPredsById :: Id -> State CspCASLSign [(SORT, SORT)]
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettgetBinPredsById ri = do
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder pm <- gets predMap
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder return $ Set.fold (\ pty -> case pty of
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder PredType [s1, s2] -> ((s1, s2) :)
e113367135dc6dbaa56c0d29d4cadbc4e0cb5dd6Christian Maeder _ -> id) [] $ MapSet.lookup ri pm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Given two CspCASL communication alphabets, check that the first's
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedersubsort closure is a subset of the second's subsort closure. -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercheckCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign ()
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettcheckCommAlphaSub sub super proc context = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sr <- gets sortRel
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let extras = closeCspCommAlpha sr sub
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder `Set.difference` closeCspCommAlpha sr super
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder unless (Set.null extras) $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let err = "Communication alphabet subset violations (" ++
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder context ++ ")" ++ show (printCommAlpha extras)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in addDiags [mkDiag Error err proc]
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett-- Static analysis of CASL terms occurring in CspCASL process terms.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CASL term appearing in a CspCASL process;
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederany in-scope process variables are added to the signature before
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederperforming the analysis. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermCspCASL :: Mix b s () () -> ProcVarMap -> TERM ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> State CspCASLSign (Maybe (TERM ()))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermCspCASL mix pm t = do
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let newVars = Map.union pm (varMap sig)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sigext = sig { varMap = newVars }
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Result ds mt = anaTermCspCASL' mix sigext t
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederidSetOfSig :: CspCASLSign -> IdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederidSetOfSig sig =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder unite [mkIdSets (allConstIds sig) (allOpIds sig) $ allPredIds sig]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CASL term in the context of a CspCASL
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedersignature. If successful, returns a fully-qualified term. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermCspCASL' :: Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaTermCspCASL' mix sig trm = fmap snd $ anaTerm (const return) mix
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (ccSig2CASLSign sig) Nothing (getRange trm) trm
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Attempt to cast a CASL term to a particular CASL sort.
842ae753ab848a8508c4832ab64296b929167a97Christian MaederccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
842ae753ab848a8508c4832ab64296b929167a97Christian MaederccTermCast t cSort sig = let
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder pos = getRange t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder msg = (++ "cast term to sort " ++ show cSort)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in case optTermSort t of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> mkError "term without type" t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just termSort
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder | termSort == cSort -> return t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder | Set.member termSort $ subsortsOf cSort sig ->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder hint (Sorted_term t cSort pos) (msg "up") pos
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder | Set.member termSort $ supersortsOf cSort sig ->
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder hint (Cast t cSort pos) (msg "down") pos
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder | otherwise -> fatal_error (msg "cannot ") pos
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- Static analysis of CASL formulae occurring in CspCASL process
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CASL formula appearing in a CspCASL process;
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederany in-scope process variables are added to the signature before
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederperforming the analysis. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaFormulaCspCASL :: Mix b s () () -> ProcVarMap -> FORMULA ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> State CspCASLSign (Maybe (FORMULA ()))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaFormulaCspCASL mix pm f = do
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly addDiags [mkDiag Debug "anaFormulaCspCASL" f]
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let newVars = Map.union pm (varMap sig)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett sigext = sig { varMap = newVars }
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Result ds mt = anaFormulaCspCASL' mix sigext f
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Statically analyse a CASL formula in the context of a CspCASL
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedersignature. If successful, returns a fully-qualified formula. -}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaFormulaCspCASL' :: Mix b s () () -> CspCASLSign -> FORMULA ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> Result (FORMULA ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederanaFormulaCspCASL' mix sig =
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder fmap snd . anaForm (const return) mix (ccSig2CASLSign sig)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Compute the communication alphabet arising from a formula
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederoccurring in a CspCASL process term. -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederformulaComms :: FORMULA () -> CommAlpha
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederformulaComms = Set.map CommTypeSort . foldFormula
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (constRecord (const Set.empty) Set.unions Set.empty)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder { foldQuantification = \ _ _ varDecls f _ ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let vdSort (Var_decl _ s _) = s in
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Set.union f $ Set.fromList (map vdSort varDecls)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , foldQual_var = \ _ _ s _ -> Set.singleton s
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , foldApplication = \ _ o _ _ -> case o of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Qual_op_name _ ty _ -> Set.singleton $ res_OP_TYPE ty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , foldSorted_term = \ _ _ s _ -> Set.singleton s
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , foldCast = \ _ _ s _ -> Set.singleton s }