-- Analysis of local top elements
-- | Check a CspCASL signature for local top elements in its subsort
checkLocalTops :: State CspCASLSign ()
addDiags (map lteError obs)
-- | Add diagnostic error message for every unmet local top element
lteError :: Obligation SORT -> Diagnosis
lteError (Obligation x y z) = mkDiag Error msg ()
where msg = ("local top element obligation ("
++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
-- 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 <-
Monad.foldM (anaChannelName chanSort) oldChanMap chanNames
put sig { extendedInfo = ext { chans = newChanMap }
-- | Statically analyse a CspCASL channel name.
anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
State CspCASLSign ChanNameMap
anaChannelName s m chanName = do
then do let err = "channel name already in use as a sort name"
addDiags [mkDiag Error err chanName]
-- Add the channel name as a symbol to the list of
-- newly defined symbols - which is stored in the CASL
do addSymbol (makeChannelNameSymbol chanName)
then do let warn = "channel redeclared with same sort"
addDiags [mkDiag Warning warn chanName]
return m -- already declared with this sort.
else do let err = "channel declared with multiple sorts"
addDiags [mkDiag Error err chanName]
-- Static analysis of process items
-- | Statically analyse a CspCASL process item.
anaProcItem :: PROC_ITEM -> State CspCASLSign ()
(Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha
(Proc_Eq parmProcName procTerm) -> anaProcEq parmProcName procTerm
-- Static analysis of process declarations
-- | Statically analyse a CspCASL process declaration.
anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
anaProcDecl name argSorts (ProcAlphabet commTypes _) = do
let ext = extendedInfo sig
oldProcDecls = procSet ext
then do -- duplicate process declaration
let err = "process name declared more than once"
addDiags [mkDiag Error err name]
else do -- new process declation
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)
let profile = (ProcProfile argSorts alpha)
-- Add the process name as a symbol to the list of
-- newly defined symbols - which is stored in the CASL
addSymbol (makeProcNameSymbol name)
put sig { extendedInfo = ext {procSet = newProcDecls }
-- Static analysis of process equations
-- | Statically analyse a CspCASL process equation.
anaProcEq :: PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
anaProcEq (ParmProcname pn vs) proc = do
let ext = extendedInfo sig
-- Only analyse a process if its name (and thus profile) is known
Just (ProcProfile procArgs procAlpha) ->
do gVars <- anaProcVars pn procArgs 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
let fqGVars = map mkFQProcVar gVars
checkCommAlphaSub termAlpha procAlpha proc "process equation"
-- Save the diags from the checkCommAlphaSub
-- put CspCASL Sentences back in to the state with new sentence
put sig {envDiags = vds, extendedInfo =
-- BUG - What should the constituent
-- alphabet be for this process?
-- probably the same as the inner one!
do addDiags [mkDiag Error
"process equation for unknown process" pn]
-- | Statically analyse a CspCASL process equation's global variable
anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList
case (compare (length ss) (length vs)) of
LT -> do addDiags [mkDiag Error "too many process arguments" pn]
GT -> do addDiags [mkDiag Error "not enough process arguments" pn]
-- | Statically analyse a CspCASL process-global variable name.
anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
anaProcVar old (v, s) = do
if v `elem` (map fst old)
then do addDiags [mkDiag Error
"process argument declared more than once" v]
else return ((v,s) : old)
-- Static analysis of process terms
-- not returing FQProcesses
-- | Statically analyse a CspCASL process term.
-- The process that is returned is a fully qualified process.
anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap ->
State CspCASLSign (CommAlpha, PROCESS)
anaProcTerm proc gVars lVars = case proc of
NamedProcess name args range ->
do addDiags [mkDiag Debug "Named process" proc]
(al, fqArgs) <- anaNamedProc proc name args (lVars `
Map.union` gVars)
let fqProc = FQProcess (NamedProcess name fqArgs range) al range
do addDiags [mkDiag Debug "Skip" proc]
let fqProc = FQProcess (Skip range)
S.empty range
do addDiags [mkDiag Debug "Stop" proc]
let fqProc = FQProcess (Stop range)
S.empty range
do addDiags [mkDiag Debug "Div" proc]
let fqProc = FQProcess (Div range)
S.empty range
do addDiags [mkDiag Debug "Run" proc]
(comms, fqEs) <- anaEventSet es
let fqProc = FQProcess (Run fqEs range) comms range
do addDiags [mkDiag Debug "Chaos" proc]
(comms, fqEs) <- anaEventSet es
let fqProc = FQProcess (Chaos fqEs range) comms range
PrefixProcess e p range ->
do addDiags [mkDiag Debug "Prefix" proc]
(evComms, rcvMap, fqEvent) <- anaEvent e (lVars `
Map.union` gVars)
(comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `
Map.union` lVars)
let newAlpha = comms `
S.union` evComms
let fqProc = FQProcess (PrefixProcess fqEvent pFQTerm range) newAlpha range
return (newAlpha, fqProc)
InternalPrefixProcess v s p range ->
-- BUG - Not returning a complete fully qualified process
do addDiags [mkDiag Debug "Internal prefix" proc]
checkSorts [s] -- check sort is known
(comms, pFQTerm) <- anaProcTerm p gVars (
Map.insert v s lVars)
let newAlpha =
S.insert (CommTypeSort s) comms
let fqProc = FQProcess (InternalPrefixProcess v s pFQTerm range) newAlpha range
return (newAlpha, fqProc)
ExternalPrefixProcess v s p range ->
-- BUG - Not returning a complete fully qualified process
do addDiags [mkDiag Debug "External prefix" proc]
checkSorts [s] -- check sort is known
(comms, pFQTerm) <- anaProcTerm p gVars (
Map.insert v s lVars)
let newAlpha =
S.insert (CommTypeSort s) comms
let fqProc = FQProcess (ExternalPrefixProcess v s pFQTerm range) newAlpha range
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "Sequential" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars
Map.empty let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (Sequential pFQTerm qFQTerm range) newAlpha range
return (newAlpha, fqProc)
InternalChoice p q range ->
do addDiags [mkDiag Debug "InternalChoice" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (InternalChoice pFQTerm qFQTerm range) newAlpha range
return (newAlpha, fqProc)
ExternalChoice p q range ->
do addDiags [mkDiag Debug "ExternalChoice" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm range) newAlpha range
return (newAlpha, fqProc)
Interleaving p q range ->
do addDiags [mkDiag Debug "Interleaving" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (Interleaving pFQTerm qFQTerm range) newAlpha range
return (newAlpha, fqProc)
SynchronousParallel p q range ->
do addDiags [mkDiag Debug "Synchronous" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (SynchronousParallel pFQTerm qFQTerm range) newAlpha range
return (newAlpha, fqProc)
GeneralisedParallel p es q range ->
do addDiags [mkDiag Debug "Generalised parallel" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(synComms, fqEs) <- anaEventSet es
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
let newAlpha =
S.unions [pComms, qComms, synComms]
let fqProc = FQProcess (GeneralisedParallel pFQTerm fqEs qFQTerm range) newAlpha range
return (newAlpha, fqProc)
AlphabetisedParallel p esp esq q range ->
do addDiags [mkDiag Debug "Alphabetised parallel" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(pSynComms, fqEsp) <- anaEventSet esp
checkCommAlphaSub pSynComms pComms proc
"alphabetised parallel, left"
(qSynComms, fqEsq) <- anaEventSet esq
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
checkCommAlphaSub qSynComms qComms proc
"alphabetised parallel, right"
let newAlpha = pComms `
S.union` qComms
let fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq qFQTerm range) newAlpha range
return (newAlpha, fqProc)
do addDiags [mkDiag Debug "Hiding" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(hidComms, fqEs) <- anaEventSet es
FQProcess (Hiding pFQTerm fqEs range) (pComms `
S.union` hidComms) range)
RenamingProcess p renaming range ->
do addDiags [mkDiag Debug "Renaming" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(renAlpha, fqRenaming) <- anaRenaming renaming
let newAlpha = pComms `
S.union` renAlpha
let fqProc = FQProcess (RenamingProcess pFQTerm fqRenaming range) (pComms `
S.union` renAlpha) range
return (newAlpha, fqProc)
ConditionalProcess f p q range ->
do addDiags [mkDiag Debug "Conditional" proc]
(pComms, pFQTerm) <- anaProcTerm p gVars lVars
(qComms, qFQTerm) <- anaProcTerm q gVars lVars
-- mfs is the fully qualified formula version of f
mfs <- anaFormulaCspCASL (gVars `
Map.union` lVars) f
Nothing -> f -- use old formula as the fully
-- qualified version - there is a
-- error in the spec anyway as the
-- formula could not be fully
Just fs -> fs -- use the real fully qualified formula
Just fs -> formulaComms fs
let newAlpha =
S.unions [pComms, qComms, fComms]
let fqProc = FQProcess (ConditionalProcess
(fFQ) pFQTerm qFQTerm range)
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.
anaNamedProc :: PROCESS -> PROCESS_NAME -> [TERM ()] -> ProcVarMap ->
State CspCASLSign (CommAlpha, [TERM ()])
anaNamedProc proc pn terms procVars = do
let ext = extendedInfo sig
Just (ProcProfile varSorts permAlpha) ->
if (length terms) == (length varSorts)
then do fqTerms <- mapM (anaNamedProcTerm procVars) (zip terms varSorts)
-- Return the permitted alphabet of the process and
-- the fully qualifed terms
return (permAlpha, fqTerms)
else do 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.
do addDiags [mkDiag Error "unknown process name" 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 :: ProcVarMap -> ((TERM ()), SORT) -> State CspCASLSign (TERM ())
anaNamedProcTerm pm (t, expSort) = do
mt <- anaTermCspCASL 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.
(Just at) -> do at' <- ccTermCast at expSort -- 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.
put sig { envDiags = vds }
-- reverse the list inside the event set
return (comms, FQEventSet (reverse fqEsElems) r)
-- | 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]) -> COMM_TYPE ->
State CspCASLSign (CommAlpha, [CommType])
anaCommType sig (alpha, fqEsElems) ct =
then -- ct is a sort name; insert sort into alpha and add a sort
-- to the fully qualified event set elements.
do let newAlpha =
S.insert (CommTypeSort ctSort) alpha
let newFqEsElems = (CommTypeSort ctSort) : fqEsElems
return (newAlpha, newFqEsElems)
else -- ct not a sort name, so should be a channel name
Just s -> -- ct is a channel name; insert typed chan name
-- into alpha and add typed channel to the fully
-- qualified event set elemenets.
let newAlpha =
S.insert (mkTypedChan ct s) alpha
newFqEsElems = (mkTypedChan ct s) : fqEsElems
in return (newAlpha, newFqEsElems)
Nothing -> do let err = "not a sort or channel name"
addDiags [mkDiag Error err ct]
-- failed, thus error in spec, return the
-- unmodified alphabet and the unmodifled
-- fully qualified event set elements.
return (alpha, fqEsElems)
where ctSort = simpleIdToId ct
mkTypedChan c s = CommTypeChan $ TypedChanName c s
-- 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 :: EVENT -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
do (alpha, newVars, fqTerm) <- anaTermEvent t vars
let fqEvent = FQEvent e Nothing fqTerm r
return (alpha, newVars, fqEvent)
do -- mfqChan is a maybe fully qualified
-- channel. It will ne Nothing if
-- annChanSend failed -
i.e. we forget
(alpha, newVars, mfqChan, fqTerm) <- anaChanSend c t vars
let fqEvent = FQEvent e mfqChan fqTerm r
return (alpha, newVars, fqEvent)
ChanNonDetSend c v s r ->
-- mfqChan is the same as in chanSend case.
-- fqVar is the fully qualfied version of the variable.
do (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
let fqEvent = FQEvent e mfqChan fqVar r
return (alpha, newVars, fqEvent)
-- mfqChan is the same as in chanSend case.
-- fqVar is the fully qualfied version of the variable.
do (alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s
let fqEvent = FQEvent e mfqChan fqVar r
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 :: (TERM ()) -> ProcVarMap ->
State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
mt <- anaTermCspCASL 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 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 :: CHANNEL_NAME -> (TERM ()) -> ProcVarMap ->
State CspCASLSign (CommAlpha, ProcVarMap,
(Maybe (CHANNEL_NAME, SORT)), TERM ())
anaChanSend 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 vars t
Nothing -> -- CASL analysis failed. Use old term as the fully
-- qualified term and forget about the channel,
-- there is an error in the spec.
do mc <- ccTermCast at chanSort
Nothing -> -- cast failed. Use old term as the fully
-- qualified term, and forget about the
-- channel there is an error in the spec.
do let castSort = sortOfTerm ct
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
-- | 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 ->
State CspCASLSign (CommAlpha, ProcVarMap, (Maybe (CHANNEL_NAME, SORT)), TERM ())
anaChanBinding c v s = do
checkSorts [s] -- check sort is known
let ext = extendedInfo sig
addDiags [mkDiag Error "unknown channel" c]
-- No fully qualified channel, use Nothing - there is a error in
-- the spec anyway. Use the real fully qualified variable
-- version with a nullRange.
then do let alpha = [CommTypeSort s
,CommTypeChan (TypedChanName c s)]
-- Return the alphabet, var mapping, the
-- fully qualfied channel and fully
(Just (c,chanSort)), (Qual_var v s nullRange))
else do let err = "sort not a subsort of channel's sort"
addDiags [mkDiag Error err s]
-- There is a error in the spec, but return
-- the alphabet, var mapping, the fully
-- qualfied channel and fully qualfied
(Qual_var v s nullRange))
-- 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
-- | Statically analyse a CspCASL renaming item. Return the alphabet
-- | and the fully qualified list of renaming functions and predicates.
anaRenamingItem :: (CommAlpha, [Maybe (TERM ())]) -> Id ->
State CspCASLSign (CommAlpha, [Maybe (TERM ())])
anaRenamingItem (inAl, fqRenamingTerms) ri = do
-- BUG -- too many nothings - should only be one
totOps <- getUnaryOpsById ri Total
then return (inAl `
S.union` totOps, fqRenamingTerms)
parOps <- getUnaryOpsById ri Partial
then return (inAl `
S.union` parOps, fqRenamingTerms)
preds <- getBinPredsById ri
then return (inAl `
S.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 with out any modification - there is an error
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 (
S.Set CommType)
getUnaryOpsById ri kind = do
binOpsKind =
S.filter (isBin kind) opsWithId
where isBin k ot = (k == opKind ot) && (1 == (length (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 (
S.Set CommType)
where isBin ot = (2 == (length (predArgs ot)))
-- | 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
(closeCspCommAlpha sig super))
else do let err = ("Communication alphabet subset violations (" ++
context ++ "): " ++ (show $
S.toList extras))
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 :: ProcVarMap -> (TERM ()) ->
State CspCASLSign (Maybe (TERM ()))
sigext = sig { varMap = newVars }
Result ds mt = anaTermCspCASL' sigext t
-- | Statically analyse a CASL term in the context of a CspCASL
-- signature. If successful, returns a fully-qualified term.
anaTermCspCASL' :: CspCASLSign -> TERM () -> Result (TERM ())
anaTermCspCASL' sig trm = do
let allIds = unite [mkIdSets (allOpIds sig) $ allPredIds sig]
mix = emptyMix { mixRules = makeRules ga allIds }
resT <- resolveMixfix (putParen mix) (mixResolve mix)
oneExpTerm (const return) sig resT
-- | Attempt to cast a CASL term to a particular CASL sort.
ccTermCast :: (TERM ()) -> SORT -> State CspCASLSign (Maybe (TERM ()))
then do let err = "upcast term to " ++ (show cSort)
addDiags [mkDiag Debug err t]
return (Just (Sorted_term t cSort (getRange t)))
then do let err = "downcast term to " ++ (show cSort)
addDiags [mkDiag Debug err t]
return (Just (Cast t cSort (getRange t)))
else do let err = "can't cast term to sort " ++
addDiags [mkDiag Error err t]
where termSort = (sortOfTerm t)
-- 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 :: ProcVarMap -> (FORMULA ()) ->
State CspCASLSign (Maybe (FORMULA ()))
anaFormulaCspCASL pm f = do
addDiags [mkDiag Debug "anaFormulaCspCASL" f]
sigext = sig { varMap = newVars }
Result ds mt = anaFormulaCspCASL' sigext f
-- | Statically analyse a CASL formula in the context of a CspCASL
-- signature. If successful, returns a fully-qualified formula.
anaFormulaCspCASL' :: CspCASLSign -> FORMULA () -> Result (FORMULA ())
anaFormulaCspCASL' sig frm = do
let allIds = unite [mkIdSets (allOpIds sig) $ allPredIds sig]
mix = emptyMix { mixRules = makeRules ga allIds }
resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm
minExpFORMULA (const return) sig resF
-- | Compute the communication alphabet arising from a formula
-- occurring in a CspCASL process term.
formulaComms :: (FORMULA ()) -> CommAlpha
formulaComms f = case f of
Quantification _ varDecls f' _ ->
where vdSorts = (map (CommTypeSort . vdSort) varDecls)
vdSort (Var_decl _ s _) = s
Conjunction fs _ ->
S.unions (map formulaComms fs)
Disjunction fs _ ->
S.unions (map formulaComms fs)
Implication f1 f2 _ _ -> (formulaComms f1) `
S.union` (formulaComms f2)
Equivalence f1 f2 _ -> (formulaComms f1) `
S.union` (formulaComms f2)
Negation f' _ -> formulaComms f'
Definedness t _ ->
S.singleton (CommTypeSort (sortOfTerm t))
Existl_equation t1 t2 _ ->
S.fromList [CommTypeSort (sortOfTerm t1),
CommTypeSort (sortOfTerm t2)]
Strong_equation t1 t2 _ ->
S.fromList [CommTypeSort (sortOfTerm t1),
CommTypeSort (sortOfTerm t2)]
Membership t s _ ->
S.fromList [CommTypeSort (sortOfTerm t),
Mixfix_formula t ->
S.singleton (CommTypeSort (sortOfTerm t))