for CSP-CASL", MPhil thesis by Andy Gimblett, 2008.
type CspBasicSpec = BASIC_SPEC CspBasicExt () CspSen
{- | The first element of the returned pair (CspBasicSpec) is the same
as the inputted version just with some very minor optimisations -
none in our case, but for CASL - brackets are otimized. This all
that happens, the mixfixed terms are still mixed fixed terms in
basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
basicAnalysisCspCASL inp@(_, insig, _) = do
(bs, ExtSign sig syms, sens) <- basicAnaAux inp
-- check for local top elements in the subsort relation
let ext = extendedInfo sig
: toSymbolSet (diffCspSig ext $ extendedInfo insig), sens)
basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
basicAnalysis (const return) ana_BASIC_CSP (const return) emptyMix
ana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign
ana_BASIC_CSP mix bs = do
{ mixRules = mixRules mix }
Channels cs _ -> mapM_ (anaChanDecl . item) cs
ProcItems ps _ -> mapM_ (anaProcItem caslMix) ps
-- Static analysis of channel declarations
-- | Statically analyse a CspCASL channel declaration.
anaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
anaChanDecl (ChannelDecl chanNames chanSort) = do
checkSorts [chanSort] -- check channel sort is known
let ext = extendedInfo sig
newChanMap <- foldM (anaChannelName chanSort) oldChanMap chanNames
put sig2 { extendedInfo = ext { chans = newChanMap }}
-- | Statically analyse a CspCASL channel name.
anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME
-> State CspCASLSign ChanNameMap
anaChannelName s m chanName = do
let err = "channel name already in use as a sort name"
addDiags [mkDiag Error err chanName]
addDiags [mkDiag Warning "redeclared channel" chanName]
-- Static analysis of process items
-- | Statically analyse a CspCASL process item.
anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
anaProcItem mix annotedProcItem = case item annotedProcItem of
Proc_Decl name argSorts alpha -> anaProcDecl name argSorts alpha
Proc_Defn name args alpha procTerm -> do
let vs = flatVAR_DECLs args
procProfile = ProcProfile argSorts alpha'
pn = ParmProcname (FQ_PROCESS_NAME name procProfile) $ map fst vs
anaProcDecl name argSorts alpha
anaProcEq mix annotedProcItem pn procTerm
Proc_Eq parmProcName procTerm ->
anaProcEq mix annotedProcItem parmProcName procTerm
-- Static analysis of process declarations
-- | Statically analyse a CspCASL process declaration.
anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
anaProcDecl name argSorts comms = do
let ext = extendedInfo sig
oldProcDecls = procSet ext
profile <- anaProcAlphabet argSorts comms
-- we no longer add (channel and) proc symbols to the CASL signature
if isNameInProcNameMap name profile oldProcDecls
-- Check the name (with profile) is new (for warning only)
then -- name with profile already in signature
do let warn = "process name redeclared with same profile '" ++
show (printProcProfile profile) ++ "':"
addDiags [mkDiag Warning warn name]
else {- New name with profile - add the name to the signature in the
return $ addProcNameToProcNameMap name profile oldProcDecls
put sig2 { extendedInfo = ext {procSet = newProcDecls }}
-- Static analysis of process equations
{- | Find a profile for a process name. Either the profile is given via a parsed
fully qualified process name, in which case we check everything is valid and
the process name with the profile is known. Or its a plain process name where
we must deduce a unique profile if possible. We also know how many variables
/ parameters the process name has. -}
findProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap ->
State CspCASLSign (Maybe ProcProfile)
findProfileForProcName pn numParams procNameMap =
FQ_PROCESS_NAME pn' (ProcProfile argSorts comms) -> do
procProfile <- anaProcAlphabet argSorts $ ProcAlphabet $
Set.toList comms
then return $ Just procProfile
"Fully qualified process name not in signature" pn]
let resProfile = getUniqueProfileInProcNameMap pn' numParams procNameMap
in case resultToMaybe resProfile of
do addDiags $ diags resProfile
{- | Analyse a process name an return a fully qualified one if possible. We also
know how many variables / parameters the process name has. -}
anaProcName :: FQ_PROCESS_NAME -> Int
-> State CspCASLSign (Maybe FQ_PROCESS_NAME)
anaProcName pn numParams = do
let ext = extendedInfo sig
simpPn = procNameToSimpProcName pn
maybeProf <- findProfileForProcName pn numParams procDecls
Nothing -> return Nothing
-- We now construct the real fully qualified process name
return $ Just $ FQ_PROCESS_NAME simpPn procProfile
-- | Statically analyse a CspCASL process equation.
anaProcEq :: Mix b s () () -> Annoted a -> PARM_PROCNAME -> PROCESS
anaProcEq mix a (ParmProcname pn vs) proc =
{- the 'annoted a' contains the annotation of the process equation. We do not
care what the underlying item is in the annotation (but it probably will be
maybeFqPn <- anaProcName pn (length vs)
-- Only analyse a process if its name and profile is known
FQ_PROCESS_NAME _ (ProcProfile argSorts commAlpha) -> do
argSorts vs {- compute global
vars Change a procVarList to a FQProcVarList We do
not care about the range as we are building fully
qualified variables and they have already been
let mkFQProcVar (v, s) = Qual_var v s nullRange
fqGVars = map mkFQProcVar gVars
checkCommAlphaSub termAlpha commAlpha proc "process equation"
{- put CspCASL Sentences back in to the state with new sentence
BUG - What should the constituent alphabet be for this
process? probably the same as the inner one! -}
addSentences [makeNamedSen $
{- We take the annotated item and replace the
inner item, thus preserving the annotations. We
then take this annotated sentence and make it a
named sentence in accordance to the (if
existing) name in the annotations. -}
$ ProcessEq fqPn fqGVars commAlpha fqProc}]
-- | Statically analyse a CspCASL process equation's global variable names.
anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] ->
State CspCASLSign ProcVarList
let msg str = addDiags [mkDiag Error ("process name applied to " ++ str) pn]
in fmap reverse $ case compare (length ss) $ length vs of
LT -> msg "too many arguments"
GT -> msg "not enough arguments"
EQ -> foldM anaProcVar [] (zip vs ss)
-- | Statically analyse a CspCASL process-global variable name.
anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
addDiags [mkDiag Error "Process argument declared more than once" v]
else return ((v, s) : old)
-- Static analysis of process terms
Statically analyse a CspCASL process term.
The process that is returned is a fully qualified process. -}
anaProcTerm :: Mix b s () () -> PROCESS -> ProcVarMap -> ProcVarMap
-> State CspCASLSign (CommAlpha, PROCESS)
anaProcTerm mix proc gVars lVars = case proc of
NamedProcess name args r ->
do addDiags [mkDiag Debug "Named process" proc]
anaNamedProc mix proc name args (lVars `
Map.union` gVars)
let fqProc = FQProcess (NamedProcess fqName fqArgs r) al r
do addDiags [mkDiag Debug "Skip" proc]
do addDiags [mkDiag Debug "Stop" proc]
do addDiags [mkDiag Debug "Div" proc]
do addDiags [mkDiag Debug "Run" proc]
(comms, fqEs) <- anaEventSet es
let fqProc = FQProcess (Run fqEs r) comms r
do addDiags [mkDiag Debug "Chaos" proc]
(comms, fqEs) <- anaEventSet es
let fqProc = FQProcess (Chaos fqEs r) comms r
do addDiags [mkDiag Debug "Prefix" proc]
(evComms, rcvMap, fqEvent) <-
anaProcTerm mix p gVars (rcvMap `
Map.union` lVars)
fqProc = FQProcess (PrefixProcess fqEvent pFQTerm r) newAlpha r
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "Sequential" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars
Map.empty fqProc = FQProcess (Sequential pFQTerm qFQTerm r) newAlpha r
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "InternalChoice" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
fqProc = FQProcess (InternalChoice pFQTerm qFQTerm r) newAlpha r
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "ExternalChoice" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm r) newAlpha r
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "Interleaving" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
fqProc = FQProcess (Interleaving pFQTerm qFQTerm r) newAlpha r
return (newAlpha, fqProc)
SynchronousParallel p q r ->
do addDiags [mkDiag Debug "Synchronous" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
fqProc = FQProcess (SynchronousParallel pFQTerm
return (newAlpha, fqProc)
GeneralisedParallel p es q r ->
do addDiags [mkDiag Debug "Generalised parallel" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(synComms, fqEs) <- anaEventSet es
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
let newAlpha =
Set.unions [pComms, qComms, synComms]
fqProc = FQProcess (GeneralisedParallel pFQTerm fqEs qFQTerm r)
return (newAlpha, fqProc)
AlphabetisedParallel p esp esq q r ->
do addDiags [mkDiag Debug "Alphabetised parallel" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(pSynComms, fqEsp) <- anaEventSet esp
checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
(qSynComms, fqEsq) <- anaEventSet esq
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
checkCommAlphaSub qSynComms qComms proc
"alphabetised parallel, right"
fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "Hiding" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(hidComms, fqEs) <- anaEventSet es
, FQProcess (Hiding pFQTerm fqEs r)
RenamingProcess p renaming r ->
do addDiags [mkDiag Debug "Renaming" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(renAlpha, _) <- anaRenaming renaming
fqProc = FQProcess (RenamingProcess pFQTerm renaming r)
return (newAlpha, fqProc)
ConditionalProcess f p q r ->
do addDiags [mkDiag Debug "Conditional" proc]
(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars
(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars
-- mfs is the fully qualified formula version of f
mfs <- anaFormulaCspCASL mix (gVars `
Map.union` lVars) f
let fFQ = fromMaybe f mfs
fqProc = FQProcess (ConditionalProcess fFQ pFQTerm qFQTerm r)
return (newAlpha, fqProc)
{- | Statically analyse a CspCASL "named process" term. Return the
permitted alphabet of the process and also a list of the fully qualified
version of the inputted terms.
BUG !!! the FQ_PROCESS_NAME may actually need to be a simple process name -}
anaNamedProc :: Mix b s () () -> PROCESS -> FQ_PROCESS_NAME -> [TERM ()]
-> ProcVarMap -> State CspCASLSign (FQ_PROCESS_NAME, CommAlpha, [TERM ()])
anaNamedProc mix proc pn terms procVars = do
maybeFqPn <- anaProcName pn (length terms)
{- Return the empty alphabet and the original
terms. There is an error in the spec. -}
FQ_PROCESS_NAME _ (ProcProfile argSorts permAlpha) ->
if length terms == length argSorts
mapM (anaNamedProcTerm mix procVars) (zip terms argSorts)
{- Return the permitted alphabet of the process and
the fully qualifed terms -}
return (fqPn, permAlpha, fqTerms)
let err = "Wrong number of arguments in named process"
addDiags [mkDiag Error err proc]
{- Return the empty alphabet and the original
terms. There is an error in the spec. -}
{- | Statically analysis a CASL term occurring in a CspCASL "named
anaNamedProcTerm :: Mix b s () () -> ProcVarMap -> (TERM (), SORT)
-> State CspCASLSign (TERM ())
anaNamedProcTerm mix pm (t, expSort) = do
mt <- anaTermCspCASL mix pm t
Nothing -> return t {- CASL term analysis failed. Use old term
as the fully qualified term, there is a
error in the spec anyway. -}
let Result ds at' = ccTermCast at expSort sig -- attempt cast;
Nothing -> {- Use old term as the fully
qualified term, there is a error
Just at'' -> return at'' {- Use the fully
-- Static analysis of event sets and communication types
{- | Statically analyse a CspCASL event set. Returns the alphabet of
the event set and a fully qualified version of the event set. -}
anaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)
-- fqEsElems is built the reversed order for efficiency.
(comms, fqEsElems) <- foldM (anaCommType sig)
put sig { envDiags = vds }
-- reverse the list inside the event set
return (comms, EventSet (reverse fqEsElems) r)
{- | Statically analyse a proc alphabet (
i.e., a list of channel and sort
identifiers) to yeild a list of sorts and typed channel names. We also check
the parameter sorts and actually construct a process profile. -}
anaProcAlphabet :: PROC_ARGS -> PROC_ALPHABET ->
State CspCASLSign ProcProfile
anaProcAlphabet argSorts (ProcAlphabet commTypes) = do
checkSorts argSorts {- check argument sorts are known build alphabet: set of
CommType values. We do not need the fully qualfied commTypes that are
returned (these area used for analysing Event Sets) -}
(alpha, _ ) <- foldM (anaCommType sig) (
Set.empty, []) commTypes
let profile = reduceProcProfile (sortRel sig) (ProcProfile argSorts alpha)
{- | Statically analyse a CspCASL communication type. Returns the
extended alphabet and the extended list of fully qualified event
set elements - [CommType]. -}
anaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> CommType ->
State CspCASLSign (CommAlpha, [CommType])
anaCommType sig (alpha, fqEsElems) ct =
let res = return (
Set.insert ct alpha, ct : fqEsElems)
old = return (alpha, fqEsElems)
chRes ch rs = let tcs = map (CommTypeChan . TypedChanName ch) rs
CommTypeSort sid -> if
Set.member sid (sortSet sig) then res else
addDiags [mkDiag Error "unknown sort or channel" sid]
CommTypeChan (TypedChanName ch sid) ->
addDiags [mkDiag Error "unknown channel" ch]
ts -> case filter (\ s -> s == sid ||
Set.member sid
(subsortsOf s sig) ||
Set.member s (subsortsOf sid sig)) ts of
let mess = "found no suitably sort '"
++ shows sid "' for channel"
addDiags [mkDiag Error mess ch]
let mess = "unknow sort '" ++ shows sid "' for channel"
addDiags [mkDiag Error mess ch]
-- Static analysis of events
{- | Statically analyse a CspCASL event. Returns a constituent
communication alphabet of the event, mapping for any new
locally bound variables and a fully qualified version of the event. -}
anaEvent :: Mix b s () () -> EVENT -> ProcVarMap
-> State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
do addDiags [mkDiag Debug "Term event" e]
(alpha, newVars, fqTerm) <- anaTermEvent mix t vars
let fqEvent = FQEvent e Nothing fqTerm range
return (alpha, newVars, fqEvent)
InternalPrefixChoice v s range ->
do addDiags [mkDiag Debug "Internal prefix event" e]
(alpha, newVars, fqVar) <- anaPrefixChoice v s
let fqEvent = FQEvent e Nothing fqVar range
return (alpha, newVars, fqEvent)
ExternalPrefixChoice v s range ->
do addDiags [mkDiag Debug "External prefix event" e]
(alpha, newVars, fqVar) <- anaPrefixChoice v s
let fqEvent = FQEvent e Nothing fqVar range
return (alpha, newVars, fqEvent)
do addDiags [mkDiag Debug "Channel send event" e]
{- mfqChan is a maybe fully qualified
channel. It will be Nothing if
annChanSend failed -
i.e. we forget
(alpha, newVars, mfqChan, fqTerm) <- anaChanSend mix c t vars
let fqEvent = FQEvent e mfqChan fqTerm range
return (alpha, newVars, fqEvent)
ChanNonDetSend c v s range ->
do addDiags [mkDiag Debug "Channel nondeterministic send event" e]
{- mfqChan is the same as in chanSend case.
fqVar is the fully qualfied version of the variable. -}
(alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
let fqEvent = FQEvent e mfqChan fqVar range
return (alpha, newVars, fqEvent)
do addDiags [mkDiag Debug "Channel receive event" e]
{- mfqChan is the same as in chanSend case.
fqVar is the fully qualfied version of the variable. -}
(alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
let fqEvent = FQEvent e mfqChan fqVar range
return (alpha, newVars, fqEvent)
{- | Statically analyse a CspCASL term event. Returns a constituent
communication alphabet of the event and a mapping for any new
locally bound variables and the fully qualified version of the
anaTermEvent :: Mix b s () () -> TERM () -> ProcVarMap
-> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
anaTermEvent mix t vars = do
mt <- anaTermCspCASL mix vars t
let (alpha, t') = case mt of
-- return the alphabet and the fully qualified term
Just at -> ([CommTypeSort (sortOfTerm at)], at)
-- return the empty alphabet and the original term
{- | Statically analyse a CspCASL internal or external prefix choice
event. Returns a constituent communication alphabet of the event
and a mapping for any new locally bound variables and the fully
qualified version of the variable. -}
anaPrefixChoice :: VAR -> SORT ->
State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
checkSorts [s] -- check sort is known
let fqVar = Qual_var v s nullRange
return (alpha, binding, fqVar)
{- | Statically analyse a CspCASL channel send event. Returns a
constituent communication alphabet of the event, a mapping for
any new locally bound variables, a fully qualified channel (if
possible) and the fully qualified version of the term. -}
anaChanSend :: Mix b s () () -> CHANNEL_NAME -> TERM () -> ProcVarMap
(CommAlpha, ProcVarMap, Maybe (CHANNEL_NAME, SORT), TERM ())
anaChanSend mix c t vars = do
let ext = extendedInfo sig
addDiags [mkDiag Error "unknown channel" c]
{- Use old term as the fully qualified term and forget about the
channel, there is an error in the spec -}
mt <- anaTermCspCASL mix vars t
{- CASL analysis failed. Use old term as the fully
qualified term and forget about the channel,
there is an error in the spec. -}
let rs = map (\ s -> ccTermCast at s sig) chanSorts
addDiags $ concatMap diags rs
case filter (isJust . maybeResult . fst) $ zip rs chanSorts of
{- cast failed. Use old term as the fully
qualified term, and forget about the
channel there is an error in the spec. -}
let alpha = [ CommTypeSort castSort
, CommTypeChan $ TypedChanName c castSort]
{- Use the real fully qualified term. We do
not want to use a cast term here. A cast
must be possible, but we do not want to
cts -> do -- fail due to an ambiguous chan sort
("ambiguous channel sorts " ++ show (map snd cts)) t]
getDeclaredChanSort :: Maybe (CHANNEL_NAME, SORT) -> CspCASLSign
getDeclaredChanSort mc sig = let cm = chans $ extendedInfo sig in case mc of
Nothing -> fail "no channel data"
[] -> mkError "unknown channel" c
css -> case filter (\ cs -> cs == s ||
Set.member s (subsortsOf cs sig))
[] -> mkError "sort not a subsort of channel's sort" s
fcs -> mkError ("ambiguous channel sorts " ++ show fcs) s
{- | Statically analyse a CspCASL "binding" channel event (which is
either a channel nondeterministic send event or a channel receive
event). Returns a constituent communication alphabet of the event,
a mapping for any new locally bound variables, a fully qualified
channel (if possible) and the fully qualified version of the
anaChanBinding :: CHANNEL_NAME -> VAR -> SORT
(CommAlpha, ProcVarMap, Maybe (CHANNEL_NAME, SORT), TERM ())
anaChanBinding c v s = do
checkSorts [s] -- check sort is known
let qv = Qual_var v s nullRange
Result ds ms = getDeclaredChanSort jcs sig
let alpha = [CommTypeSort s, CommTypeChan (TypedChanName c s)]
{- Return the alphabet, var mapping, the fully
qualfied channel and fully qualfied
variable. Notice that the fully qualified
channel's sort should be the lowest sort we can
communicate in
i.e. the sort of the variable. -}
-- Static analysis of renaming and renaming items
{- | Statically analyse a CspCASL renaming. Returns the alphabet and
the fully qualified renaming. -}
anaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)
anaRenaming renaming = case renaming of
(al, fqRenamingTermsMaybes) <- foldM anaRenamingItem (
Set.empty, []) r
return (al, FQRenaming fqRenamingTermsMaybes)
{- | Statically analyse a CspCASL renaming item. Return the alphabet
and the fully qualified list of renaming functions and predicates. -}
anaRenamingItem :: (CommAlpha, [TERM ()]) -> Id ->
State CspCASLSign (CommAlpha, [TERM ()])
anaRenamingItem (inAl, fqRenamingTerms) ri = do
-- BUG -- too many nothings - should only be one
totOps <- getUnaryOpsById ri Total
then return (inAl `
Set.union` totOps, fqRenamingTerms)
parOps <- getUnaryOpsById ri Partial
then return (inAl `
Set.union` parOps, fqRenamingTerms)
preds <- getBinPredsById ri
then return (inAl `
Set.union` preds, fqRenamingTerms)
let err = "renaming item not a binary "
++ "operation or predicate name"
addDiags [mkDiag Error err ri]
{- return the original alphabet and the original fully
qualified terms (renamings) with out any modification
as there is an error in the spec. -}
return (inAl, fqRenamingTerms)
{- | Given a CASL identifier and a `function kind' (total or partial),
find all unary operations of that kind with that name in the CASL
signature, and return a set of corresponding communication types
getUnaryOpsById :: Id -> OpKind -> State CspCASLSign (
Set.Set CommType)
getUnaryOpsById ri kind = do
where isBin k ot = k == opKind ot && isSingle (opArgs ot)
{- | Given a CASL identifier find all binary predicates with that name
in the CASL signature, and return a set of corresponding
communication types for those predicates. -}
getBinPredsById :: Id -> State CspCASLSign (
Set.Set CommType)
{- | Given two CspCASL communication alphabets, check that the first's
subsort closure is a subset of the second's subsort closure. -}
checkCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String
checkCommAlphaSub sub super proc context = do
let extras = closeCspCommAlpha sr sub
let err = "Communication alphabet subset violations (" ++
context ++ ")" ++ show (printCommAlpha extras)
in addDiags [mkDiag Error err proc]
-- Static analysis of CASL terms occurring in CspCASL process terms.
{- | Statically analyse a CASL term appearing in a CspCASL process;
any in-scope process variables are added to the signature before
performing the analysis. -}
anaTermCspCASL :: Mix b s () () -> ProcVarMap -> TERM ()
-> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL mix pm t = do
sigext = sig { varMap = newVars }
Result ds mt = anaTermCspCASL' mix sigext t
idSetOfSig :: CspCASLSign -> IdSets
unite [mkIdSets (allConstIds sig) (allOpIds sig) $ allPredIds sig]
{- | Statically analyse a CASL term in the context of a CspCASL
signature. If successful, returns a fully-qualified term. -}
anaTermCspCASL' :: Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
anaTermCspCASL' mix sig trm = fmap snd $ anaTerm (const return) mix
(ccSig2CASLSign sig) Nothing (getRange trm) trm
-- | Attempt to cast a CASL term to a particular CASL sort.
ccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
ccTermCast t cSort sig = let
msg = (++ "cast term to sort " ++ show cSort)
Nothing -> mkError "term without type" t
| termSort == cSort -> return t
hint (Sorted_term t cSort pos) (msg "up") pos
hint (Cast t cSort pos) (msg "down") pos
| otherwise -> fatal_error (msg "cannot ") pos
{- Static analysis of CASL formulae occurring in CspCASL process
{- | Statically analyse a CASL formula appearing in a CspCASL process;
any in-scope process variables are added to the signature before
performing the analysis. -}
anaFormulaCspCASL :: Mix b s () () -> ProcVarMap -> FORMULA ()
-> State CspCASLSign (Maybe (FORMULA ()))
anaFormulaCspCASL mix pm f = do
addDiags [mkDiag Debug "anaFormulaCspCASL" f]
sigext = sig { varMap = newVars }
Result ds mt = anaFormulaCspCASL' mix sigext f
{- | Statically analyse a CASL formula in the context of a CspCASL
signature. If successful, returns a fully-qualified formula. -}
anaFormulaCspCASL' :: Mix b s () () -> CspCASLSign -> FORMULA ()
anaFormulaCspCASL' mix sig =
fmap snd . anaForm (const return) mix (ccSig2CASLSign sig)
{- | Compute the communication alphabet arising from a formula
occurring in a CspCASL process term. -}
formulaComms :: FORMULA () -> CommAlpha
formulaComms =
Set.map CommTypeSort . foldFormula
{ foldQuantification = \ _ _ varDecls f _ ->
let vdSort (Var_decl _ s _) = s in
, foldApplication = \ _ o _ _ -> case o of