{- |
Module      :  ./CspCASL/StatAnaCSP.hs
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 }
