{- |

Module : $Header$

Description : Static analysis of CspCASL

Copyright : (c) Andy Gimblett, Liam O'Reilly, Markus Roggenbach,

Swansea University 2008, C. Maeder, DFKI 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

Static analysis of CSP-CASL specifications, following "Tool Support

for CSP-CASL", MPhil thesis by Andy Gimblett, 2008.

<http://www.cs.swan.ac.uk/~csandy/mphil/>

-}

module CspCASL.StatAnaCSP where

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.MixfixParser

import CASL.Quantification

import CASL.Sign

import CASL.StaticAna

import CASL.ToDoc ()

import Common.AS_Annotation

import Common.Result

import Common.GlobalAnnotations

import Common.Id

import Common.Lib.State

import Common.ExtSign

import qualified Common.Lib.MapSet as MapSet

import CspCASL.AS_CspCASL

import CspCASL.AS_CspCASL_Process

import qualified CspCASL.LocalTop as LocalTop

import CspCASL.Print_CspCASL

import CspCASL.SignCSP

import CspCASL.Symbol

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.Maybe

import Control.Monad

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

the returned version. -}

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

appendDiags $ LocalTop.checkLocalTops $ sortRel sig

let ext = extendedInfo sig

return (bs, ExtSign sig $ Set.unions

$ Set.map caslToCspSymbol syms

: toSymbolSet (diffCspSig ext $ extendedInfo insig), sens)

basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos)

-> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])

basicAnaAux =

basicAnalysis (const return) ana_BASIC_CSP (const return) emptyMix

ana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign

ana_BASIC_CSP mix bs = do

let caslMix = emptyMix

{ mixRules = mixRules mix }

case bs of

Channels cs _ -> mapM_ (anaChanDecl . item) cs

ProcItems ps _ -> mapM_ (anaProcItem caslMix) ps

return bs

-- 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

sig <- get

let ext = extendedInfo sig

oldChanMap = chans ext

newChanMap <- foldM (anaChannelName chanSort) oldChanMap chanNames

sig2 <- get

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

sig <- get

if Set.member chanName (sortSet sig)

then do

let err = "channel name already in use as a sort name"

addDiags [mkDiag Error err chanName]

return m

else do

when (MapSet.member chanName s m) $

addDiags [mkDiag Warning "redeclared channel" chanName]

return $ MapSet.insert chanName s m

-- 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

argSorts = map snd vs

alpha' = case alpha of

ProcAlphabet alpha'' -> Set.fromList alpha''

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

-> State CspCASLSign ()

anaProcDecl name argSorts comms = do

sig <- get

let ext = extendedInfo sig

oldProcDecls = procSet ext

newProcDecls <- do

-- new process declation

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]

return oldProcDecls

else {- New name with profile - add the name to the signature in the

state -}

return $ addProcNameToProcNameMap name profile oldProcDecls

sig2 <- get

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 =

case pn of

FQ_PROCESS_NAME pn' (ProcProfile argSorts comms) -> do

procProfile <- anaProcAlphabet argSorts $ ProcAlphabet $ Set.toList comms

if MapSet.member pn' procProfile procNameMap

then return $ Just procProfile

else do

addDiags [mkDiag Error

"Fully qualified process name not in signature" pn]

return Nothing

PROCESS_NAME pn' ->

let resProfile = getUniqueProfileInProcNameMap pn' numParams procNameMap

in case resultToMaybe resProfile of

Nothing ->

do addDiags $ diags resProfile

return Nothing

Just profile' ->

return $ Just profile'

{- | 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

sig <- get

let ext = extendedInfo sig

procDecls = procSet ext

simpPn = procNameToSimpProcName pn

maybeProf <- findProfileForProcName pn numParams procDecls

case maybeProf of

Nothing -> return Nothing

Just procProfile ->

-- 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

-> State CspCASLSign ()

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

the proc eq) -}

do

maybeFqPn <- anaProcName pn (length vs)

case maybeFqPn of

-- Only analyse a process if its name and profile is known

Nothing -> return ()

Just fqPn ->

case fqPn of

PROCESS_NAME _ ->

error "CspCasl.StatAnaCSP.anaProcEq: Impossible case"

FQ_PROCESS_NAME _ (ProcProfile argSorts commAlpha) -> do

gVars <- anaProcVars pn

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

checked to be ok. -}

let mkFQProcVar (v, s) = Qual_var v s nullRange

fqGVars = map mkFQProcVar gVars

(termAlpha, fqProc) <-

anaProcTerm mix proc (Map.fromList gVars) Map.empty

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. -}

a {item = ExtFORMULA

$ ProcessEq fqPn fqGVars commAlpha fqProc}]

-- | Statically analyse a CspCASL process equation's global variable names.

anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] ->

State CspCASLSign ProcVarList

anaProcVars pn ss vs =

let msg str = addDiags [mkDiag Error ("process name applied to " ++ str) pn]

>> return []

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

anaProcVar old (v, s) =

if v `elem` map fst old

then do

addDiags [mkDiag Error "Process argument declared more than once" v]

return old

else return ((v, s) : old)

-- Static analysis of process terms

{- BUG in fucntion below

not returing FQProcesses

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]

(fqName, al, fqArgs) <-

anaNamedProc mix proc name args (lVars `Map.union` gVars)

let fqProc = FQProcess (NamedProcess fqName fqArgs r) al r

return (al, fqProc)

Skip r ->

do addDiags [mkDiag Debug "Skip" proc]

let fqProc = FQProcess (Skip r) Set.empty r

return (Set.empty, fqProc)

Stop r ->

do addDiags [mkDiag Debug "Stop" proc]

let fqProc = FQProcess (Stop r) Set.empty r

return (Set.empty, fqProc)

Div r ->

do addDiags [mkDiag Debug "Div" proc]

let fqProc = FQProcess (Div r) Set.empty r

return (Set.empty, fqProc)

Run es r ->

do addDiags [mkDiag Debug "Run" proc]

(comms, fqEs) <- anaEventSet es

let fqProc = FQProcess (Run fqEs r) comms r

return (comms, fqProc)

Chaos es r ->

do addDiags [mkDiag Debug "Chaos" proc]

(comms, fqEs) <- anaEventSet es

let fqProc = FQProcess (Chaos fqEs r) comms r

return (comms, fqProc)

PrefixProcess e p r ->

do addDiags [mkDiag Debug "Prefix" proc]

(evComms, rcvMap, fqEvent) <-

anaEvent mix e (lVars `Map.union` gVars)

(comms, pFQTerm) <-

anaProcTerm mix p gVars (rcvMap `Map.union` lVars)

let newAlpha = comms `Set.union` evComms

fqProc = FQProcess (PrefixProcess fqEvent pFQTerm r) newAlpha r

return (newAlpha, fqProc)

Sequential p q r ->

do addDiags [mkDiag Debug "Sequential" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(qComms, qFQTerm) <- anaProcTerm mix q gVars Map.empty

let newAlpha = pComms `Set.union` qComms

fqProc = FQProcess (Sequential pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

InternalChoice p q r ->

do addDiags [mkDiag Debug "InternalChoice" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars

let newAlpha = pComms `Set.union` qComms

fqProc = FQProcess (InternalChoice pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

ExternalChoice p q r ->

do addDiags [mkDiag Debug "ExternalChoice" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars

let newAlpha = pComms `Set.union` qComms

fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

Interleaving p q r ->

do addDiags [mkDiag Debug "Interleaving" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(qComms, qFQTerm) <- anaProcTerm mix q gVars lVars

let newAlpha = pComms `Set.union` qComms

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

let newAlpha = pComms `Set.union` qComms

fqProc = FQProcess (SynchronousParallel pFQTerm

qFQTerm r) newAlpha r

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)

newAlpha 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"

let newAlpha = pComms `Set.union` qComms

fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq

qFQTerm r) newAlpha r

return (newAlpha, fqProc)

Hiding p es r ->

do addDiags [mkDiag Debug "Hiding" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(hidComms, fqEs) <- anaEventSet es

return (pComms `Set.union` hidComms

, FQProcess (Hiding pFQTerm fqEs r)

(pComms `Set.union` hidComms) r)

RenamingProcess p renaming r ->

do addDiags [mkDiag Debug "Renaming" proc]

(pComms, pFQTerm) <- anaProcTerm mix p gVars lVars

(renAlpha, fqRenaming) <- anaRenaming renaming

let newAlpha = pComms `Set.union` renAlpha

fqProc = FQProcess (RenamingProcess pFQTerm fqRenaming r)

(pComms `Set.union` renAlpha) 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

fComms = maybe Set.empty formulaComms mfs

newAlpha = Set.unions [pComms, qComms, fComms]

fqProc = FQProcess (ConditionalProcess fFQ pFQTerm qFQTerm r)

newAlpha r

return (newAlpha, fqProc)

FQProcess {} ->

error "CspCASL.StatAnaCSP.anaProcTerm: Unexpected FQProcess"

{- | 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)

case maybeFqPn of

Nothing ->

{- Return the empty alphabet and the original

terms. There is an error in the spec. -}

return (pn, Set.empty, terms)

Just fqPn ->

case fqPn of

PROCESS_NAME _ ->

error "CspCasl.StatAnaCSP.anaNamedProc: Impossible case"

FQ_PROCESS_NAME _ (ProcProfile argSorts permAlpha) ->

if length terms == length argSorts

then do

fqTerms <-

mapM (anaNamedProcTerm mix procVars) (zip terms argSorts)

{- Return the permitted alphabet of the process and

the fully qualifed terms -}

return (fqPn, 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. -}

return (pn, Set.empty, terms)

{- | Statically analysis a CASL term occurring in a CspCASL "named

process" term. -}

anaNamedProcTerm :: Mix b s () () -> ProcVarMap -> (TERM (), SORT)

-> State CspCASLSign (TERM ())

anaNamedProcTerm mix pm (t, expSort) = do

mt <- anaTermCspCASL mix pm t

sig <- get

case mt of

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

let Result ds at' = ccTermCast at expSort sig -- attempt cast;

addDiags ds

case at' of

Nothing -> {- Use old term as the fully

qualified term, there is a error

in the spec anyway. -}

return t

Just at'' -> return at'' {- Use the fully

qualified

(possibly cast)

term -}

-- 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)

anaEventSet eventSet =

case eventSet of

EventSet es r ->

do sig <- get

-- fqEsElems is built the reversed order for efficiency.

(comms, fqEsElems) <- foldM (anaCommType sig)

(Set.empty, []) es

vds <- gets envDiags

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

sig <- get

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)

return profile

{- | 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)

getChSrts ch = Set.toList $ MapSet.lookup ch $ chans

$ extendedInfo sig

chRes ch rs = let tcs = map (CommTypeChan . TypedChanName ch) rs

in return (Set.union alpha $ Set.fromList tcs, tcs ++ fqEsElems)

in case ct of

CommTypeSort sid -> if Set.member sid (sortSet sig) then res else

case getChSrts sid of

[] -> do

addDiags [mkDiag Error "unknown sort or channel" sid]

old

cs -> chRes sid cs

CommTypeChan (TypedChanName ch sid) ->

if Set.member sid (sortSet sig) then

case getChSrts ch of

[] -> do

addDiags [mkDiag Error "unknown channel" ch]

old

ts -> case filter (\ s -> s == sid || Set.member sid

(subsortsOf s sig) || Set.member s (subsortsOf sid sig)) ts of

[] -> do

let mess = "found no suitably sort '"

++ shows sid "' for channel"

addDiags [mkDiag Error mess ch]

old

rs -> chRes ch rs

else do

let mess = "unknow sort '" ++ shows sid "' for channel"

addDiags [mkDiag Error mess ch]

old

-- 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)

anaEvent mix e vars =

case e of

TermEvent t range ->

do addDiags [mkDiag Debug "Term event" e]

(alpha, newVars, fqTerm) <- anaTermEvent mix t vars

let fqEvent = FQTermEvent 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 = FQInternalPrefixChoice 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 = FQExternalPrefixChoice fqVar range

return (alpha, newVars, fqEvent)

ChanSend c t range ->

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

about the channel. -}

(alpha, newVars, mfqChan, fqTerm) <- anaChanSend mix c t vars

let fqEvent = FQChanSend 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 = FQChanNonDetSend mfqChan fqVar range

return (alpha, newVars, fqEvent)

ChanRecv c v s range ->

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 = FQChanRecv mfqChan fqVar range

return (alpha, newVars, fqEvent)

_ -> error

"CspCASL.StatAnaCSP.anaEvent: Unexpected Fully qualified event"

{- | 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

term. -}

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

Nothing -> ([], t)

return (Set.fromList alpha, Map.empty, t')

{- | 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 ())

anaPrefixChoice v s = do

checkSorts [s] -- check sort is known

let alpha = Set.singleton $ CommTypeSort s

let binding = Map.singleton v s

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

-> State CspCASLSign

(CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())

anaChanSend mix c t vars = do

sig <- get

let ext = extendedInfo sig

msg = "CspCASL.StatAnaCSP.anaChanSend: Channel Error"

case Set.toList $ MapSet.lookup c $ chans ext of

[] -> do

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 -}

return (Set.empty, Map.empty, error msg, t)

chanSorts -> do

mt <- anaTermCspCASL mix vars t

case mt of

Nothing ->

{- CASL analysis failed. Use old term as the fully

qualified term and forget about the channel,

there is an error in the spec. -}

return (Set.empty, Map.empty, error msg, t)

Just at -> do

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. -}

return (Set.empty, Map.empty, error msg, t)

[(_, castSort)] ->

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

force it! -}

in return (Set.fromList alpha, Map.empty, (c, castSort), at)

cts -> do -- fail due to an ambiguous chan sort

addDiags [mkDiag Error

("ambiguous channel sorts " ++ show (map snd cts)) t]

{- Use old term as the fully qualified term and forget about the

channel, there is an error in the spec. -}

return (Set.empty, Map.empty, error msg, t)

getDeclaredChanSort :: (CHANNEL_NAME, SORT) -> CspCASLSign -> Result SORT

getDeclaredChanSort (c, s) sig =

let cm = chans $ extendedInfo sig

in case Set.toList $ MapSet.lookup c cm of

[] -> mkError "unknown channel" c

css -> case filter (\ cs -> cs == s || Set.member s (subsortsOf cs sig))

css of

[] -> mkError "sort not a subsort of channel's sort" s

[cs] -> return cs

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 and the fully qualified version of the

variable. -}

anaChanBinding :: CHANNEL_NAME -> VAR -> SORT

-> State CspCASLSign

(CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())

anaChanBinding c v s = do

checkSorts [s] -- check sort is known

sig <- get

let qv = Qual_var v s nullRange

fqChan = (c, s)

Result ds ms = getDeclaredChanSort fqChan sig

addDiags ds

case ms of

Nothing -> return (Set.empty, Map.empty, fqChan, qv)

Just _ ->

let alpha = [CommTypeSort s, CommTypeChan (TypedChanName c s)]

binding = [(v, 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. -}

in return (Set.fromList alpha, Map.fromList binding, fqChan, qv)

-- 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

Renaming r -> do

fqRenamingTerms <- mapM anaRenamingItem r

let rs = concat fqRenamingTerms

return ( Set.map CommTypeSort $ Set.unions $ map alphaOfRename rs

, Renaming rs)

alphaOfRename :: Rename -> Set.Set SORT

alphaOfRename (Rename _ cm) = case cm of

Just (_, Just (s1, s2)) -> Set.fromList [s1, s2]

_ -> Set.empty

{- | Statically analyse a CspCASL renaming item. Return the alphabet

and the fully qualified list of renaming functions and predicates. -}

anaRenamingItem :: Rename -> State CspCASLSign [Rename]

anaRenamingItem r@(Rename ri cm) = let

predToRen p = Rename ri $ Just (BinPred, Just p)

opToRen (o, p) = Rename ri

$ Just (if o == Total then TotOp else PartOp, Just p)

in case cm of

Just (k, ms) -> case k of

BinPred -> do

ps <- getBinPredsById ri

let realPs = case ms of

Nothing -> ps

Just p -> filter (== p) ps

when (null realPs)

$ addDiags [mkDiag Error "renaming predicate not found" r]

unless (isSingle realPs)

$ addDiags [mkDiag Warning "multiple predicates found" r]

return $ map predToRen realPs

_ -> do

os <- getUnaryOpsById ri

-- we ignore the user given op kind here!

let realOs = case ms of

Nothing -> os

Just p -> filter ((== p) . snd) os

when (null realOs)

$ addDiags [mkDiag Error "renaming operation not found" r]

unless (isSingle realOs)

$ addDiags [mkDiag Warning "multiple operations found" r]

when (k == TotOp) $

mapM_ (\ (o, (s1, s2)) -> when (o == Partial)

$ addDiags [mkDiag Error

("operation of type '"

++ shows s1 " -> "

++ shows s2 "' is not total") r]) realOs

return $ map opToRen realOs

Nothing -> do

ps <- getBinPredsById ri

os <- getUnaryOpsById ri

let rs = map predToRen ps ++ map opToRen os

when (null rs)

$ addDiags [mkDiag Error "renaming predicate or operation not found" ri]

unless (isSingle rs)

$ addDiags [mkDiag Warning "multiple renamings found" ri]

return rs

{- | Given a CASL identifier, find all

unary operations with that name in the CASL signature, and return a

list of corresponding profiles, i.e. kind, argument sort and result sort. -}

getUnaryOpsById :: Id -> State CspCASLSign [(OpKind, (SORT, SORT))]

getUnaryOpsById ri = do

om <- gets opMap

return $ Set.fold (\ oty -> case oty of

OpType k [s1] s2 -> ((k, (s1, s2)) :)

_ -> id) [] $ MapSet.lookup ri om

{- | Given a CASL identifier find all binary predicates with that name in the

CASL signature, and return a list of corresponding profiles. -}

getBinPredsById :: Id -> State CspCASLSign [(SORT, SORT)]

getBinPredsById ri = do

pm <- gets predMap

return $ Set.fold (\ pty -> case pty of

PredType [s1, s2] -> ((s1, s2) :)

_ -> id) [] $ MapSet.lookup ri pm

{- | 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

-> State CspCASLSign ()

checkCommAlphaSub sub super proc context = do

sr <- gets sortRel

let extras = closeCspCommAlpha sr sub

`Set.difference` closeCspCommAlpha sr super

unless (Set.null extras) $

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

sig <- get

let newVars = Map.union pm (varMap sig)

sigext = sig { varMap = newVars }

Result ds mt = anaTermCspCASL' mix sigext t

addDiags ds

return mt

idSetOfSig :: CspCASLSign -> IdSets

idSetOfSig sig =

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

pos = getRange t

msg = (++ "cast term to sort " ++ show cSort)

in case optTermSort t of

Nothing -> mkError "term without type" t

Just termSort

| termSort == cSort -> return t

| Set.member termSort $ subsortsOf cSort sig ->

hint (Sorted_term t cSort pos) (msg "up") pos

| Set.member termSort $ supersortsOf cSort sig ->

hint (Cast t cSort pos) (msg "down") pos

| otherwise -> fatal_error (msg "cannot ") pos

{- Static analysis of CASL formulae occurring in CspCASL process

terms. -}

{- | 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]

sig <- get

let newVars = Map.union pm (varMap sig)

sigext = sig { varMap = newVars }

Result ds mt = anaFormulaCspCASL' mix sigext f

addDiags ds

return mt

{- | 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 ()

-> Result (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

(constRecord (const Set.empty) Set.unions Set.empty)

{ foldQuantification = \ _ _ varDecls f _ ->

let vdSort (Var_decl _ s _) = s in

Set.union f $ Set.fromList (map vdSort varDecls)

, foldQual_var = \ _ _ s _ -> Set.singleton s

, foldApplication = \ _ o _ _ -> case o of

Op_name _ -> Set.empty

Qual_op_name _ ty _ -> Set.singleton $ res_OP_TYPE ty

, foldSorted_term = \ _ _ s _ -> Set.singleton s

, foldCast = \ _ _ s _ -> Set.singleton s }