{- |
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 :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result
     (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
basicAnalysisCspCASL inp :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
inp@(_, insig :: CspCASLSign
insig, _) = do
  (bs :: CspBasicSpec
bs, ExtSign sig :: CspCASLSign
sig syms :: Set Symbol
syms, sens :: [Named CspCASLSen]
sens) <- (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result
     (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
basicAnaAux (CspBasicSpec, CspCASLSign, GlobalAnnos)
inp
  -- check for local top elements in the subsort relation
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [Diagnosis]
LocalTop.checkLocalTops (Rel SORT -> [Diagnosis]) -> Rel SORT -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CspCASLSign
sig
  let ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
  (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
-> Result
     (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
forall (m :: * -> *) a. Monad m => a -> m a
return (CspBasicSpec
bs, CspCASLSign -> Set CspSymbol -> ExtSign CspCASLSign CspSymbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign CspCASLSign
sig (Set CspSymbol -> ExtSign CspCASLSign CspSymbol)
-> Set CspSymbol -> ExtSign CspCASLSign CspSymbol
forall a b. (a -> b) -> a -> b
$ [Set CspSymbol] -> Set CspSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
             ([Set CspSymbol] -> Set CspSymbol)
-> [Set CspSymbol] -> Set CspSymbol
forall a b. (a -> b) -> a -> b
$ (Symbol -> CspSymbol) -> Set Symbol -> Set CspSymbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> CspSymbol
caslToCspSymbol Set Symbol
syms
             Set CspSymbol -> [Set CspSymbol] -> [Set CspSymbol]
forall a. a -> [a] -> [a]
: CspSign -> [Set CspSymbol]
toSymbolSet (CspSign -> CspSign -> CspSign
diffCspSig CspSign
ext (CspSign -> CspSign) -> CspSign -> CspSign
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
insig), [Named CspCASLSen]
sens)

basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
  -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result
     (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
basicAnaAux =
  Min CspSen CspSign
-> Ana CspBasicExt CspBasicExt () CspSen CspSign
-> Ana () CspBasicExt () CspSen CspSign
-> Mix CspBasicExt () CspSen CspSign
-> (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result
     (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis ((CspSen -> Result CspSen) -> Min CspSen CspSign
forall a b. a -> b -> a
const CspSen -> Result CspSen
forall (m :: * -> *) a. Monad m => a -> m a
return) Ana CspBasicExt CspBasicExt () CspSen CspSign
ana_BASIC_CSP ((() -> State CspCASLSign ())
-> Ana () CspBasicExt () CspSen CspSign
forall a b. a -> b -> a
const () -> State CspCASLSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix CspBasicExt () CspSen CspSign
forall b s f e. Mix b s f e
emptyMix

ana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign
ana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign
ana_BASIC_CSP mix :: Mix CspBasicExt () CspSen CspSign
mix bs :: CspBasicExt
bs = do
  let caslMix :: Mix b s f e
caslMix = Mix b s f e
forall b s f e. Mix b s f e
emptyMix
        { mixRules :: (TokRules, Rules)
mixRules = Mix CspBasicExt () CspSen CspSign -> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix CspBasicExt () CspSen CspSign
mix }
  case CspBasicExt
bs of
    Channels cs :: [Annoted CHANNEL_DECL]
cs _ -> (Annoted CHANNEL_DECL -> State CspCASLSign ())
-> [Annoted CHANNEL_DECL] -> State CspCASLSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (CHANNEL_DECL -> State CspCASLSign ()
anaChanDecl (CHANNEL_DECL -> State CspCASLSign ())
-> (Annoted CHANNEL_DECL -> CHANNEL_DECL)
-> Annoted CHANNEL_DECL
-> State CspCASLSign ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CHANNEL_DECL -> CHANNEL_DECL
forall a. Annoted a -> a
item) [Annoted CHANNEL_DECL]
cs
    ProcItems ps :: [Annoted PROC_ITEM]
ps _ -> (Annoted PROC_ITEM -> State CspCASLSign ())
-> [Annoted PROC_ITEM] -> State CspCASLSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Mix Any Any () () -> Annoted PROC_ITEM -> State CspCASLSign ()
forall b s.
Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
anaProcItem Mix Any Any () ()
forall b s f e. Mix b s f e
caslMix) [Annoted PROC_ITEM]
ps
  CspBasicExt -> State CspCASLSign CspBasicExt
forall (m :: * -> *) a. Monad m => a -> m a
return CspBasicExt
bs

-- Static analysis of channel declarations

-- | Statically analyse a CspCASL channel declaration.
anaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
anaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
anaChanDecl (ChannelDecl chanNames :: [SORT]
chanNames chanSort :: SORT
chanSort) = do
    [SORT] -> State CspCASLSign ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT
chanSort] -- check channel sort is known
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    let ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
        oldChanMap :: ChanNameMap
oldChanMap = CspSign -> ChanNameMap
chans CspSign
ext
    ChanNameMap
newChanMap <- (ChanNameMap -> SORT -> State CspCASLSign ChanNameMap)
-> ChanNameMap -> [SORT] -> State CspCASLSign ChanNameMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (SORT -> ChanNameMap -> SORT -> State CspCASLSign ChanNameMap
anaChannelName SORT
chanSort) ChanNameMap
oldChanMap [SORT]
chanNames
    CspCASLSign
sig2 <- State CspCASLSign CspCASLSign
forall s. State s s
get
    CspCASLSign -> State CspCASLSign ()
forall s. s -> State s ()
put CspCASLSign
sig2 { extendedInfo :: CspSign
extendedInfo = CspSign
ext { chans :: ChanNameMap
chans = ChanNameMap
newChanMap }}

-- | Statically analyse a CspCASL channel name.
anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME
  -> State CspCASLSign ChanNameMap
anaChannelName :: SORT -> ChanNameMap -> SORT -> State CspCASLSign ChanNameMap
anaChannelName s :: SORT
s m :: ChanNameMap
m chanName :: SORT
chanName = do
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
chanName (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CspCASLSign
sig)
      then do
        let err :: [Char]
err = "channel name already in use as a sort name"
        [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error [Char]
err SORT
chanName]
        ChanNameMap -> State CspCASLSign ChanNameMap
forall (m :: * -> *) a. Monad m => a -> m a
return ChanNameMap
m
      else do
        Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SORT -> SORT -> ChanNameMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member SORT
chanName SORT
s ChanNameMap
m) (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$
          [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "redeclared channel" SORT
chanName]
        ChanNameMap -> State CspCASLSign ChanNameMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ChanNameMap -> State CspCASLSign ChanNameMap)
-> ChanNameMap -> State CspCASLSign ChanNameMap
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> ChanNameMap -> ChanNameMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
chanName SORT
s ChanNameMap
m

-- Static analysis of process items

-- | Statically analyse a CspCASL process item.
anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
anaProcItem mix :: Mix b s () ()
mix annotedProcItem :: Annoted PROC_ITEM
annotedProcItem = case Annoted PROC_ITEM -> PROC_ITEM
forall a. Annoted a -> a
item Annoted PROC_ITEM
annotedProcItem of
    Proc_Decl name :: SORT
name argSorts :: [SORT]
argSorts alpha :: PROC_ALPHABET
alpha -> SORT -> [SORT] -> PROC_ALPHABET -> State CspCASLSign ()
anaProcDecl SORT
name [SORT]
argSorts PROC_ALPHABET
alpha
    Proc_Defn name :: SORT
name args :: [VAR_DECL]
args alpha :: PROC_ALPHABET
alpha procTerm :: PROCESS
procTerm -> do
      let vs :: [(VAR, SORT)]
vs = [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
args
          argSorts :: [SORT]
argSorts = ((VAR, SORT) -> SORT) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd [(VAR, SORT)]
vs
          alpha' :: Set CommType
alpha' = case PROC_ALPHABET
alpha of
            ProcAlphabet alpha'' :: [CommType]
alpha'' -> [CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
alpha''
          procProfile :: ProcProfile
procProfile = [SORT] -> Set CommType -> ProcProfile
ProcProfile [SORT]
argSorts Set CommType
alpha'
          pn :: PARM_PROCNAME
pn = FQ_PROCESS_NAME -> [VAR] -> PARM_PROCNAME
ParmProcname (SORT -> ProcProfile -> FQ_PROCESS_NAME
FQ_PROCESS_NAME SORT
name ProcProfile
procProfile) ([VAR] -> PARM_PROCNAME) -> [VAR] -> PARM_PROCNAME
forall a b. (a -> b) -> a -> b
$ ((VAR, SORT) -> VAR) -> [(VAR, SORT)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> VAR
forall a b. (a, b) -> a
fst [(VAR, SORT)]
vs
      SORT -> [SORT] -> PROC_ALPHABET -> State CspCASLSign ()
anaProcDecl SORT
name [SORT]
argSorts PROC_ALPHABET
alpha
      Mix b s () ()
-> Annoted PROC_ITEM
-> PARM_PROCNAME
-> PROCESS
-> State CspCASLSign ()
forall b s a.
Mix b s () ()
-> Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
anaProcEq Mix b s () ()
mix Annoted PROC_ITEM
annotedProcItem PARM_PROCNAME
pn PROCESS
procTerm
    Proc_Eq parmProcName :: PARM_PROCNAME
parmProcName procTerm :: PROCESS
procTerm ->
      Mix b s () ()
-> Annoted PROC_ITEM
-> PARM_PROCNAME
-> PROCESS
-> State CspCASLSign ()
forall b s a.
Mix b s () ()
-> Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
anaProcEq Mix b s () ()
mix Annoted PROC_ITEM
annotedProcItem PARM_PROCNAME
parmProcName PROCESS
procTerm

-- Static analysis of process declarations

-- | Statically analyse a CspCASL process declaration.
anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
            -> State CspCASLSign ()
anaProcDecl :: SORT -> [SORT] -> PROC_ALPHABET -> State CspCASLSign ()
anaProcDecl name :: SORT
name argSorts :: [SORT]
argSorts comms :: PROC_ALPHABET
comms = do
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    let ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
        oldProcDecls :: ProcNameMap
oldProcDecls = CspSign -> ProcNameMap
procSet CspSign
ext
    ProcNameMap
newProcDecls <- do
      -- new process declation
      ProcProfile
profile <- [SORT] -> PROC_ALPHABET -> State CspCASLSign ProcProfile
anaProcAlphabet [SORT]
argSorts PROC_ALPHABET
comms
      -- we no longer add (channel and) proc symbols to the CASL signature
      if SORT -> ProcProfile -> ProcNameMap -> Bool
isNameInProcNameMap SORT
name ProcProfile
profile ProcNameMap
oldProcDecls
      -- Check the name (with profile) is new (for warning only)
         then -- name with profile already in signature
              do let warn :: [Char]
warn = "process name redeclared with same profile '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                            Doc -> [Char]
forall a. Show a => a -> [Char]
show (ProcProfile -> Doc
printProcProfile ProcProfile
profile) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "':"
                 [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning [Char]
warn SORT
name]
                 ProcNameMap -> State CspCASLSign ProcNameMap
forall (m :: * -> *) a. Monad m => a -> m a
return ProcNameMap
oldProcDecls
         else {- New name with profile - add the name to the signature in the
              state -}
              ProcNameMap -> State CspCASLSign ProcNameMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ProcNameMap -> State CspCASLSign ProcNameMap)
-> ProcNameMap -> State CspCASLSign ProcNameMap
forall a b. (a -> b) -> a -> b
$ SORT -> ProcProfile -> ProcNameMap -> ProcNameMap
addProcNameToProcNameMap SORT
name ProcProfile
profile ProcNameMap
oldProcDecls
    CspCASLSign
sig2 <- State CspCASLSign CspCASLSign
forall s. State s s
get
    CspCASLSign -> State CspCASLSign ()
forall s. s -> State s ()
put CspCASLSign
sig2 { extendedInfo :: CspSign
extendedInfo = CspSign
ext {procSet :: ProcNameMap
procSet = ProcNameMap
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 :: FQ_PROCESS_NAME
-> Int -> ProcNameMap -> State CspCASLSign (Maybe ProcProfile)
findProfileForProcName pn :: FQ_PROCESS_NAME
pn numParams :: Int
numParams procNameMap :: ProcNameMap
procNameMap =
  case FQ_PROCESS_NAME
pn of
    FQ_PROCESS_NAME pn' :: SORT
pn' (ProcProfile argSorts :: [SORT]
argSorts comms :: Set CommType
comms) -> do
      ProcProfile
procProfile <- [SORT] -> PROC_ALPHABET -> State CspCASLSign ProcProfile
anaProcAlphabet [SORT]
argSorts (PROC_ALPHABET -> State CspCASLSign ProcProfile)
-> PROC_ALPHABET -> State CspCASLSign ProcProfile
forall a b. (a -> b) -> a -> b
$ [CommType] -> PROC_ALPHABET
ProcAlphabet ([CommType] -> PROC_ALPHABET) -> [CommType] -> PROC_ALPHABET
forall a b. (a -> b) -> a -> b
$ Set CommType -> [CommType]
forall a. Set a -> [a]
Set.toList Set CommType
comms
      if SORT -> ProcProfile -> ProcNameMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member SORT
pn' ProcProfile
procProfile ProcNameMap
procNameMap
        then Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile))
-> Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall a b. (a -> b) -> a -> b
$ ProcProfile -> Maybe ProcProfile
forall a. a -> Maybe a
Just ProcProfile
procProfile
        else do
          [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> FQ_PROCESS_NAME -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error
                    "Fully qualified process name not in signature" FQ_PROCESS_NAME
pn]
          Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProcProfile
forall a. Maybe a
Nothing
    PROCESS_NAME pn' :: SORT
pn' ->
      let resProfile :: Result ProcProfile
resProfile = SORT -> Int -> ProcNameMap -> Result ProcProfile
getUniqueProfileInProcNameMap SORT
pn' Int
numParams ProcNameMap
procNameMap
      in case Result ProcProfile -> Maybe ProcProfile
forall a. Result a -> Maybe a
resultToMaybe Result ProcProfile
resProfile of
        Nothing ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State CspCASLSign ())
-> [Diagnosis] -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ Result ProcProfile -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags Result ProcProfile
resProfile
             Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProcProfile
forall a. Maybe a
Nothing
        Just profile' :: ProcProfile
profile' ->
          Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile))
-> Maybe ProcProfile -> State CspCASLSign (Maybe ProcProfile)
forall a b. (a -> b) -> a -> b
$ ProcProfile -> Maybe ProcProfile
forall a. a -> Maybe a
Just ProcProfile
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 :: FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
anaProcName pn :: FQ_PROCESS_NAME
pn numParams :: Int
numParams = do
  CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
  let ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
      procDecls :: ProcNameMap
procDecls = CspSign -> ProcNameMap
procSet CspSign
ext
      simpPn :: SORT
simpPn = FQ_PROCESS_NAME -> SORT
procNameToSimpProcName FQ_PROCESS_NAME
pn
  Maybe ProcProfile
maybeProf <- FQ_PROCESS_NAME
-> Int -> ProcNameMap -> State CspCASLSign (Maybe ProcProfile)
findProfileForProcName FQ_PROCESS_NAME
pn Int
numParams ProcNameMap
procDecls
  case Maybe ProcProfile
maybeProf of
    Nothing -> Maybe FQ_PROCESS_NAME -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FQ_PROCESS_NAME
forall a. Maybe a
Nothing
    Just procProfile :: ProcProfile
procProfile ->
      -- We now construct the real fully qualified process name
      Maybe FQ_PROCESS_NAME -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FQ_PROCESS_NAME
 -> State CspCASLSign (Maybe FQ_PROCESS_NAME))
-> Maybe FQ_PROCESS_NAME
-> State CspCASLSign (Maybe FQ_PROCESS_NAME)
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME -> Maybe FQ_PROCESS_NAME
forall a. a -> Maybe a
Just (FQ_PROCESS_NAME -> Maybe FQ_PROCESS_NAME)
-> FQ_PROCESS_NAME -> Maybe FQ_PROCESS_NAME
forall a b. (a -> b) -> a -> b
$ SORT -> ProcProfile -> FQ_PROCESS_NAME
FQ_PROCESS_NAME SORT
simpPn ProcProfile
procProfile

-- | Statically analyse a CspCASL process equation.
anaProcEq :: Mix b s () () -> Annoted a -> PARM_PROCNAME -> PROCESS
  -> State CspCASLSign ()
anaProcEq :: Mix b s () ()
-> Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
anaProcEq mix :: Mix b s () ()
mix a :: Annoted a
a (ParmProcname pn :: FQ_PROCESS_NAME
pn vs :: [VAR]
vs) proc :: PROCESS
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
    Maybe FQ_PROCESS_NAME
maybeFqPn <- FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
anaProcName FQ_PROCESS_NAME
pn ([VAR] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VAR]
vs)
    case Maybe FQ_PROCESS_NAME
maybeFqPn of
      -- Only analyse a process if its name and profile is known
      Nothing -> () -> State CspCASLSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just fqPn :: FQ_PROCESS_NAME
fqPn ->
        case FQ_PROCESS_NAME
fqPn of
          PROCESS_NAME _ ->
            [Char] -> State CspCASLSign ()
forall a. HasCallStack => [Char] -> a
error "CspCasl.StatAnaCSP.anaProcEq: Impossible case"
          FQ_PROCESS_NAME _ (ProcProfile argSorts :: [SORT]
argSorts commAlpha :: Set CommType
commAlpha) -> do
                [(VAR, SORT)]
gVars <- FQ_PROCESS_NAME
-> [SORT] -> [VAR] -> State CspCASLSign [(VAR, SORT)]
anaProcVars FQ_PROCESS_NAME
pn
                         [SORT]
argSorts [VAR]
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 :: (VAR, SORT) -> TERM f
mkFQProcVar (v :: VAR
v, s :: SORT
s) = VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
nullRange
                    fqGVars :: [TERM f]
fqGVars = ((VAR, SORT) -> TERM f) -> [(VAR, SORT)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> TERM f
forall f. (VAR, SORT) -> TERM f
mkFQProcVar [(VAR, SORT)]
gVars
                (termAlpha :: Set CommType
termAlpha, fqProc :: PROCESS
fqProc) <-
                  Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
proc ([(VAR, SORT)] -> ProcVarMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(VAR, SORT)]
gVars) ProcVarMap
forall k a. Map k a
Map.empty
                Set CommType
-> Set CommType -> PROCESS -> [Char] -> State CspCASLSign ()
checkCommAlphaSub Set CommType
termAlpha Set CommType
commAlpha PROCESS
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! -}
                [Named CspCASLSen] -> State CspCASLSign ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [Annoted CspCASLSen -> Named CspCASLSen
forall a. Annoted a -> Named a
makeNamedSen (Annoted CspCASLSen -> Named CspCASLSen)
-> Annoted CspCASLSen -> Named CspCASLSen
forall a b. (a -> b) -> a -> b
$
                              {- 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. -}
                               Annoted a
a {item :: CspCASLSen
item = CspSen -> CspCASLSen
forall f. f -> FORMULA f
ExtFORMULA
                                   (CspSen -> CspCASLSen) -> CspSen -> CspCASLSen
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME
-> FQProcVarList -> Set CommType -> PROCESS -> CspSen
ProcessEq FQ_PROCESS_NAME
fqPn FQProcVarList
forall f. [TERM f]
fqGVars Set CommType
commAlpha PROCESS
fqProc}]

-- | Statically analyse a CspCASL process equation's global variable names.
anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] ->
               State CspCASLSign ProcVarList
anaProcVars :: FQ_PROCESS_NAME
-> [SORT] -> [VAR] -> State CspCASLSign [(VAR, SORT)]
anaProcVars pn :: FQ_PROCESS_NAME
pn ss :: [SORT]
ss vs :: [VAR]
vs =
  let msg :: [Char] -> State (Sign f e) [a]
msg str :: [Char]
str = [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> FQ_PROCESS_NAME -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error ("process name applied to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
str) FQ_PROCESS_NAME
pn]
        State (Sign f e) () -> State (Sign f e) [a] -> State (Sign f e) [a]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> State (Sign f e) [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  in ([(VAR, SORT)] -> [(VAR, SORT)])
-> State CspCASLSign [(VAR, SORT)]
-> State CspCASLSign [(VAR, SORT)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(VAR, SORT)] -> [(VAR, SORT)]
forall a. [a] -> [a]
reverse (State CspCASLSign [(VAR, SORT)]
 -> State CspCASLSign [(VAR, SORT)])
-> State CspCASLSign [(VAR, SORT)]
-> State CspCASLSign [(VAR, SORT)]
forall a b. (a -> b) -> a -> b
$ case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
ss) (Int -> Ordering) -> Int -> Ordering
forall a b. (a -> b) -> a -> b
$ [VAR] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VAR]
vs of
    LT -> [Char] -> State CspCASLSign [(VAR, SORT)]
forall f e a. [Char] -> State (Sign f e) [a]
msg "too many arguments"
    GT -> [Char] -> State CspCASLSign [(VAR, SORT)]
forall f e a. [Char] -> State (Sign f e) [a]
msg "not enough arguments"
    EQ -> ([(VAR, SORT)] -> (VAR, SORT) -> State CspCASLSign [(VAR, SORT)])
-> [(VAR, SORT)]
-> [(VAR, SORT)]
-> State CspCASLSign [(VAR, SORT)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(VAR, SORT)] -> (VAR, SORT) -> State CspCASLSign [(VAR, SORT)]
anaProcVar [] ([VAR] -> [SORT] -> [(VAR, SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
vs [SORT]
ss)

-- | Statically analyse a CspCASL process-global variable name.
anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
anaProcVar :: [(VAR, SORT)] -> (VAR, SORT) -> State CspCASLSign [(VAR, SORT)]
anaProcVar old :: [(VAR, SORT)]
old (v :: VAR
v, s :: SORT
s) =
    if VAR
v VAR -> [VAR] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((VAR, SORT) -> VAR) -> [(VAR, SORT)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> VAR
forall a b. (a, b) -> a
fst [(VAR, SORT)]
old
       then do
         [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> VAR -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "Process argument declared more than once" VAR
v]
         [(VAR, SORT)] -> State CspCASLSign [(VAR, SORT)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(VAR, SORT)]
old
       else [(VAR, SORT)] -> State CspCASLSign [(VAR, SORT)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((VAR
v, SORT
s) (VAR, SORT) -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. a -> [a] -> [a]
: [(VAR, SORT)]
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 b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm mix :: Mix b s () ()
mix proc :: PROCESS
proc gVars :: ProcVarMap
gVars lVars :: ProcVarMap
lVars = case PROCESS
proc of
    NamedProcess name :: FQ_PROCESS_NAME
name args :: FQProcVarList
args r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Named process" PROCESS
proc]
           (fqName :: FQ_PROCESS_NAME
fqName, al :: Set CommType
al, fqArgs :: FQProcVarList
fqArgs) <-
             Mix b s () ()
-> PROCESS
-> FQ_PROCESS_NAME
-> FQProcVarList
-> ProcVarMap
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
forall b s.
Mix b s () ()
-> PROCESS
-> FQ_PROCESS_NAME
-> FQProcVarList
-> ProcVarMap
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
anaNamedProc Mix b s () ()
mix PROCESS
proc FQ_PROCESS_NAME
name FQProcVarList
args (ProcVarMap
lVars ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` ProcVarMap
gVars)
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (FQ_PROCESS_NAME -> FQProcVarList -> Range -> PROCESS
NamedProcess FQ_PROCESS_NAME
fqName FQProcVarList
fqArgs Range
r) Set CommType
al Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
al, PROCESS
fqProc)
    Skip r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Skip" PROCESS
proc]
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (Range -> PROCESS
Skip Range
r) Set CommType
forall a. Set a
Set.empty Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, PROCESS
fqProc)
    Stop r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Stop" PROCESS
proc]
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (Range -> PROCESS
Stop Range
r) Set CommType
forall a. Set a
Set.empty Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, PROCESS
fqProc)
    Div r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Div" PROCESS
proc]
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (Range -> PROCESS
Div Range
r) Set CommType
forall a. Set a
Set.empty Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, PROCESS
fqProc)
    Run es :: EVENT_SET
es r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Run" PROCESS
proc]
           (comms :: Set CommType
comms, fqEs :: EVENT_SET
fqEs) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
es
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (EVENT_SET -> Range -> PROCESS
Run EVENT_SET
fqEs Range
r) Set CommType
comms Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
comms, PROCESS
fqProc)
    Chaos es :: EVENT_SET
es r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Chaos" PROCESS
proc]
           (comms :: Set CommType
comms, fqEs :: EVENT_SET
fqEs) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
es
           let fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (EVENT_SET -> Range -> PROCESS
Chaos EVENT_SET
fqEs Range
r) Set CommType
comms Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
comms, PROCESS
fqProc)
    PrefixProcess e :: EVENT
e p :: PROCESS
p r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Prefix" PROCESS
proc]
           (evComms :: Set CommType
evComms, rcvMap :: ProcVarMap
rcvMap, fqEvent :: EVENT
fqEvent) <-
               Mix b s () ()
-> EVENT
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall b s.
Mix b s () ()
-> EVENT
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
anaEvent Mix b s () ()
mix EVENT
e (ProcVarMap
lVars ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` ProcVarMap
gVars)
           (comms :: Set CommType
comms, pFQTerm :: PROCESS
pFQTerm) <-
               Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars (ProcVarMap
rcvMap ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` ProcVarMap
lVars)
           let newAlpha :: Set CommType
newAlpha = Set CommType
comms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
evComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (EVENT -> PROCESS -> Range -> PROCESS
PrefixProcess EVENT
fqEvent PROCESS
pFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    Sequential p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Sequential" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
forall k a. Map k a
Map.empty
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS -> Range -> PROCESS
Sequential PROCESS
pFQTerm PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    InternalChoice p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "InternalChoice" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS -> Range -> PROCESS
InternalChoice PROCESS
pFQTerm PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    ExternalChoice p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "ExternalChoice" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS -> Range -> PROCESS
ExternalChoice PROCESS
pFQTerm PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    Interleaving p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Interleaving" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS -> Range -> PROCESS
Interleaving PROCESS
pFQTerm PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    SynchronousParallel p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Synchronous" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS -> Range -> PROCESS
SynchronousParallel PROCESS
pFQTerm
                                                       PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Generalised parallel" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (synComms :: Set CommType
synComms, fqEs :: EVENT_SET
fqEs) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
es
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           let newAlpha :: Set CommType
newAlpha = [Set CommType] -> Set CommType
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set CommType
pComms, Set CommType
qComms, Set CommType
synComms]
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> EVENT_SET -> PROCESS -> Range -> PROCESS
GeneralisedParallel PROCESS
pFQTerm EVENT_SET
fqEs PROCESS
qFQTerm Range
r)
                                         Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    AlphabetisedParallel p :: PROCESS
p esp :: EVENT_SET
esp esq :: EVENT_SET
esq q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Alphabetised parallel" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (pSynComms :: Set CommType
pSynComms, fqEsp :: EVENT_SET
fqEsp) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
esp
           Set CommType
-> Set CommType -> PROCESS -> [Char] -> State CspCASLSign ()
checkCommAlphaSub Set CommType
pSynComms Set CommType
pComms PROCESS
proc "alphabetised parallel, left"
           (qSynComms :: Set CommType
qSynComms, fqEsq :: EVENT_SET
fqEsq) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
esq
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           Set CommType
-> Set CommType -> PROCESS -> [Char] -> State CspCASLSign ()
checkCommAlphaSub Set CommType
qSynComms Set CommType
qComms PROCESS
proc
                                 "alphabetised parallel, right"
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
qComms
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> EVENT_SET -> EVENT_SET -> PROCESS -> Range -> PROCESS
AlphabetisedParallel PROCESS
pFQTerm EVENT_SET
fqEsp EVENT_SET
fqEsq
                                                        PROCESS
qFQTerm Range
r) Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    Hiding p :: PROCESS
p es :: EVENT_SET
es r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Hiding" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (hidComms :: Set CommType
hidComms, fqEs :: EVENT_SET
fqEs) <- EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet EVENT_SET
es
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
hidComms
                  , PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> EVENT_SET -> Range -> PROCESS
Hiding PROCESS
pFQTerm EVENT_SET
fqEs Range
r)
                                  (Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
hidComms) Range
r)
    RenamingProcess p :: PROCESS
p renaming :: RENAMING
renaming r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Renaming" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (renAlpha :: Set CommType
renAlpha, fqRenaming :: RENAMING
fqRenaming) <- RENAMING -> State CspCASLSign (Set CommType, RENAMING)
anaRenaming RENAMING
renaming
           let newAlpha :: Set CommType
newAlpha = Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
renAlpha
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (PROCESS -> RENAMING -> Range -> PROCESS
RenamingProcess PROCESS
pFQTerm RENAMING
fqRenaming Range
r)
                                         (Set CommType
pComms Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set CommType
renAlpha) Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    ConditionalProcess f :: FORMULA ()
f p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
        do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Conditional" PROCESS
proc]
           (pComms :: Set CommType
pComms, pFQTerm :: PROCESS
pFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
p ProcVarMap
gVars ProcVarMap
lVars
           (qComms :: Set CommType
qComms, qFQTerm :: PROCESS
qFQTerm) <- Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
forall b s.
Mix b s () ()
-> PROCESS
-> ProcVarMap
-> ProcVarMap
-> State CspCASLSign (Set CommType, PROCESS)
anaProcTerm Mix b s () ()
mix PROCESS
q ProcVarMap
gVars ProcVarMap
lVars
           -- mfs is the fully qualified formula version of f
           Maybe (FORMULA ())
mfs <- Mix b s () ()
-> ProcVarMap
-> FORMULA ()
-> State CspCASLSign (Maybe (FORMULA ()))
forall b s.
Mix b s () ()
-> ProcVarMap
-> FORMULA ()
-> State CspCASLSign (Maybe (FORMULA ()))
anaFormulaCspCASL Mix b s () ()
mix (ProcVarMap
gVars ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` ProcVarMap
lVars) FORMULA ()
f
           let fFQ :: FORMULA ()
fFQ = FORMULA () -> Maybe (FORMULA ()) -> FORMULA ()
forall a. a -> Maybe a -> a
fromMaybe FORMULA ()
f Maybe (FORMULA ())
mfs
               fComms :: Set CommType
fComms = Set CommType
-> (FORMULA () -> Set CommType)
-> Maybe (FORMULA ())
-> Set CommType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set CommType
forall a. Set a
Set.empty FORMULA () -> Set CommType
formulaComms Maybe (FORMULA ())
mfs
               newAlpha :: Set CommType
newAlpha = [Set CommType] -> Set CommType
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set CommType
pComms, Set CommType
qComms, Set CommType
fComms]
               fqProc :: PROCESS
fqProc = PROCESS -> Set CommType -> Range -> PROCESS
FQProcess (FORMULA () -> PROCESS -> PROCESS -> Range -> PROCESS
ConditionalProcess FORMULA ()
fFQ PROCESS
pFQTerm PROCESS
qFQTerm Range
r)
                        Set CommType
newAlpha Range
r
           (Set CommType, PROCESS)
-> State CspCASLSign (Set CommType, PROCESS)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
newAlpha, PROCESS
fqProc)
    FQProcess {} ->
        [Char] -> State CspCASLSign (Set CommType, PROCESS)
forall a. HasCallStack => [Char] -> a
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 b s () ()
-> PROCESS
-> FQ_PROCESS_NAME
-> FQProcVarList
-> ProcVarMap
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
anaNamedProc mix :: Mix b s () ()
mix proc :: PROCESS
proc pn :: FQ_PROCESS_NAME
pn terms :: FQProcVarList
terms procVars :: ProcVarMap
procVars = do
  Maybe FQ_PROCESS_NAME
maybeFqPn <- FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
anaProcName FQ_PROCESS_NAME
pn (FQProcVarList -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FQProcVarList
terms)
  case Maybe FQ_PROCESS_NAME
maybeFqPn of
    Nothing ->
      {- Return the empty alphabet and the original
      terms. There is an error in the spec. -}
      (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
forall (m :: * -> *) a. Monad m => a -> m a
return (FQ_PROCESS_NAME
pn, Set CommType
forall a. Set a
Set.empty, FQProcVarList
terms)
    Just fqPn :: FQ_PROCESS_NAME
fqPn ->
      case FQ_PROCESS_NAME
fqPn of
        PROCESS_NAME _ ->
          [Char]
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
forall a. HasCallStack => [Char] -> a
error "CspCasl.StatAnaCSP.anaNamedProc: Impossible case"
        FQ_PROCESS_NAME _ (ProcProfile argSorts :: [SORT]
argSorts permAlpha :: Set CommType
permAlpha) ->
          if FQProcVarList -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FQProcVarList
terms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
argSorts
          then do
            FQProcVarList
fqTerms <-
                    ((TERM (), SORT) -> State CspCASLSign (TERM ()))
-> [(TERM (), SORT)] -> State CspCASLSign FQProcVarList
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Mix b s () ()
-> ProcVarMap -> (TERM (), SORT) -> State CspCASLSign (TERM ())
forall b s.
Mix b s () ()
-> ProcVarMap -> (TERM (), SORT) -> State CspCASLSign (TERM ())
anaNamedProcTerm Mix b s () ()
mix ProcVarMap
procVars) (FQProcVarList -> [SORT] -> [(TERM (), SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip FQProcVarList
terms [SORT]
argSorts)
                  {- Return the permitted alphabet of the process and
                  the fully qualifed terms -}
            (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
forall (m :: * -> *) a. Monad m => a -> m a
return (FQ_PROCESS_NAME
fqPn, Set CommType
permAlpha, FQProcVarList
fqTerms)
          else do
            let err :: [Char]
err = "Wrong number of arguments in named process"
            [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error [Char]
err PROCESS
proc]
                  {- Return the empty alphabet and the original
                  terms. There is an error in the spec. -}
            (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
-> State CspCASLSign (FQ_PROCESS_NAME, Set CommType, FQProcVarList)
forall (m :: * -> *) a. Monad m => a -> m a
return (FQ_PROCESS_NAME
pn, Set CommType
forall a. Set a
Set.empty, FQProcVarList
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 b s () ()
-> ProcVarMap -> (TERM (), SORT) -> State CspCASLSign (TERM ())
anaNamedProcTerm mix :: Mix b s () ()
mix pm :: ProcVarMap
pm (t :: TERM ()
t, expSort :: SORT
expSort) = do
    Maybe (TERM ())
mt <- Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
forall b s.
Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL Mix b s () ()
mix ProcVarMap
pm TERM ()
t
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    case Maybe (TERM ())
mt of
      Nothing -> TERM () -> State CspCASLSign (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return TERM ()
t {- CASL term analysis failed. Use old term
                          as the fully qualified term, there is a
                          error in the spec anyway. -}
      Just at :: TERM ()
at -> do
        let Result ds :: [Diagnosis]
ds at' :: Maybe (TERM ())
at' = TERM () -> SORT -> CspCASLSign -> Result (TERM ())
ccTermCast TERM ()
at SORT
expSort CspCASLSign
sig -- attempt cast;
        [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
        case Maybe (TERM ())
at' of
          Nothing -> {- Use old term as the fully
                     qualified term, there is a error
                     in the spec anyway. -}
                               TERM () -> State CspCASLSign (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return TERM ()
t
          Just at'' :: TERM ()
at'' -> TERM () -> State CspCASLSign (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return TERM ()
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 :: EVENT_SET -> State CspCASLSign (Set CommType, EVENT_SET)
anaEventSet eventSet :: EVENT_SET
eventSet =
    case EVENT_SET
eventSet of
      EventSet es :: [CommType]
es r :: Range
r ->
          do CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
             -- fqEsElems is built the reversed order for efficiency.
             (comms :: Set CommType
comms, fqEsElems :: [CommType]
fqEsElems) <- ((Set CommType, [CommType])
 -> CommType -> State CspCASLSign (Set CommType, [CommType]))
-> (Set CommType, [CommType])
-> [CommType]
-> State CspCASLSign (Set CommType, [CommType])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (CspCASLSign
-> (Set CommType, [CommType])
-> CommType
-> State CspCASLSign (Set CommType, [CommType])
anaCommType CspCASLSign
sig)
                                   (Set CommType
forall a. Set a
Set.empty, []) [CommType]
es
             [Diagnosis]
vds <- (CspCASLSign -> [Diagnosis]) -> State CspCASLSign [Diagnosis]
forall s a. (s -> a) -> State s a
gets CspCASLSign -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags
             CspCASLSign -> State CspCASLSign ()
forall s. s -> State s ()
put CspCASLSign
sig { envDiags :: [Diagnosis]
envDiags = [Diagnosis]
vds }
             -- reverse the list inside the event set
             (Set CommType, EVENT_SET)
-> State CspCASLSign (Set CommType, EVENT_SET)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
comms, [CommType] -> Range -> EVENT_SET
EventSet ([CommType] -> [CommType]
forall a. [a] -> [a]
reverse [CommType]
fqEsElems) Range
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 :: [SORT] -> PROC_ALPHABET -> State CspCASLSign ProcProfile
anaProcAlphabet argSorts :: [SORT]
argSorts (ProcAlphabet commTypes :: [CommType]
commTypes) = do
  CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
  [SORT] -> State CspCASLSign ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT]
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 :: Set CommType
alpha, _ ) <- ((Set CommType, [CommType])
 -> CommType -> State CspCASLSign (Set CommType, [CommType]))
-> (Set CommType, [CommType])
-> [CommType]
-> State CspCASLSign (Set CommType, [CommType])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (CspCASLSign
-> (Set CommType, [CommType])
-> CommType
-> State CspCASLSign (Set CommType, [CommType])
anaCommType CspCASLSign
sig) (Set CommType
forall a. Set a
Set.empty, []) [CommType]
commTypes
  let profile :: ProcProfile
profile = Rel SORT -> ProcProfile -> ProcProfile
reduceProcProfile (CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CspCASLSign
sig) ([SORT] -> Set CommType -> ProcProfile
ProcProfile [SORT]
argSorts Set CommType
alpha)
  ProcProfile -> State CspCASLSign ProcProfile
forall (m :: * -> *) a. Monad m => a -> m a
return ProcProfile
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 :: CspCASLSign
-> (Set CommType, [CommType])
-> CommType
-> State CspCASLSign (Set CommType, [CommType])
anaCommType sig :: CspCASLSign
sig (alpha :: Set CommType
alpha, fqEsElems :: [CommType]
fqEsElems) ct :: CommType
ct =
  let res :: State CspCASLSign (Set CommType, [CommType])
res = (Set CommType, [CommType])
-> State CspCASLSign (Set CommType, [CommType])
forall (m :: * -> *) a. Monad m => a -> m a
return (CommType -> Set CommType -> Set CommType
forall a. Ord a => a -> Set a -> Set a
Set.insert CommType
ct Set CommType
alpha, CommType
ct CommType -> [CommType] -> [CommType]
forall a. a -> [a] -> [a]
: [CommType]
fqEsElems)
      old :: State CspCASLSign (Set CommType, [CommType])
old = (Set CommType, [CommType])
-> State CspCASLSign (Set CommType, [CommType])
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, [CommType]
fqEsElems)
      getChSrts :: SORT -> [SORT]
getChSrts ch :: SORT
ch = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> ChanNameMap -> Set SORT
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
ch (ChanNameMap -> Set SORT) -> ChanNameMap -> Set SORT
forall a b. (a -> b) -> a -> b
$ CspSign -> ChanNameMap
chans
        (CspSign -> ChanNameMap) -> CspSign -> ChanNameMap
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
      chRes :: SORT -> [SORT] -> m (Set CommType, [CommType])
chRes ch :: SORT
ch rs :: [SORT]
rs = let tcs :: [CommType]
tcs = (SORT -> CommType) -> [SORT] -> [CommType]
forall a b. (a -> b) -> [a] -> [b]
map (TypedChanName -> CommType
CommTypeChan (TypedChanName -> CommType)
-> (SORT -> TypedChanName) -> SORT -> CommType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SORT -> TypedChanName
TypedChanName SORT
ch) [SORT]
rs
        in (Set CommType, [CommType]) -> m (Set CommType, [CommType])
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set CommType
alpha (Set CommType -> Set CommType) -> Set CommType -> Set CommType
forall a b. (a -> b) -> a -> b
$ [CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
tcs, [CommType]
tcs [CommType] -> [CommType] -> [CommType]
forall a. [a] -> [a] -> [a]
++ [CommType]
fqEsElems)
  in case CommType
ct of
  CommTypeSort sid :: SORT
sid -> if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
sid (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CspCASLSign
sig) then State CspCASLSign (Set CommType, [CommType])
res else
    case SORT -> [SORT]
getChSrts SORT
sid of
      [] -> do
        [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "unknown sort or channel" SORT
sid]
        State CspCASLSign (Set CommType, [CommType])
old
      cs :: [SORT]
cs -> SORT -> [SORT] -> State CspCASLSign (Set CommType, [CommType])
forall (m :: * -> *).
Monad m =>
SORT -> [SORT] -> m (Set CommType, [CommType])
chRes SORT
sid [SORT]
cs
  CommTypeChan (TypedChanName ch :: SORT
ch sid :: SORT
sid) ->
    if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
sid (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CspCASLSign
sig) then
    case SORT -> [SORT]
getChSrts SORT
ch of
      [] -> do
        [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "unknown channel" SORT
ch]
        State CspCASLSign (Set CommType, [CommType])
old
      ts :: [SORT]
ts -> case (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ s :: SORT
s -> SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sid Bool -> Bool -> Bool
|| SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
sid
              (SORT -> CspCASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
s CspCASLSign
sig) Bool -> Bool -> Bool
|| SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (SORT -> CspCASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
sid CspCASLSign
sig)) [SORT]
ts of
        [] -> do
          let mess :: [Char]
mess = "found no suitably sort '"
                [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows SORT
sid "' for channel"
          [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error [Char]
mess SORT
ch]
          State CspCASLSign (Set CommType, [CommType])
old
        rs :: [SORT]
rs -> SORT -> [SORT] -> State CspCASLSign (Set CommType, [CommType])
forall (m :: * -> *).
Monad m =>
SORT -> [SORT] -> m (Set CommType, [CommType])
chRes SORT
ch [SORT]
rs
    else do
      let mess :: [Char]
mess = "unknow sort '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows SORT
sid "' for channel"
      [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error [Char]
mess SORT
ch]
      State CspCASLSign (Set CommType, [CommType])
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 b s () ()
-> EVENT
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
anaEvent mix :: Mix b s () ()
mix e :: EVENT
e vars :: ProcVarMap
vars =
    case EVENT
e of
      TermEvent t :: TERM ()
t range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Term event" EVENT
e]
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, fqTerm :: TERM ()
fqTerm) <- Mix b s () ()
-> TERM ()
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
forall b s.
Mix b s () ()
-> TERM ()
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
anaTermEvent Mix b s () ()
mix TERM ()
t ProcVarMap
vars
             let fqEvent :: EVENT
fqEvent = TERM () -> Range -> EVENT
FQTermEvent TERM ()
fqTerm Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      InternalPrefixChoice v :: VAR
v s :: SORT
s range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Internal prefix event" EVENT
e]
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, fqVar :: TERM ()
fqVar) <- VAR
-> SORT -> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
anaPrefixChoice VAR
v SORT
s
             let fqEvent :: EVENT
fqEvent = TERM () -> Range -> EVENT
FQInternalPrefixChoice TERM ()
fqVar Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      ExternalPrefixChoice v :: VAR
v s :: SORT
s range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "External prefix event" EVENT
e]
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, fqVar :: TERM ()
fqVar) <- VAR
-> SORT -> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
anaPrefixChoice VAR
v SORT
s
             let fqEvent :: EVENT
fqEvent = TERM () -> Range -> EVENT
FQExternalPrefixChoice TERM ()
fqVar Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      ChanSend c :: SORT
c t :: TERM ()
t range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Channel send event" EVENT
e]
             {- mfqChan is a maybe fully qualified
             channel. It will be Nothing if
             annChanSend failed - i.e. we forget
             about the channel. -}
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, mfqChan :: (SORT, SORT)
mfqChan, fqTerm :: TERM ()
fqTerm) <- Mix b s () ()
-> SORT
-> TERM ()
-> ProcVarMap
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall b s.
Mix b s () ()
-> SORT
-> TERM ()
-> ProcVarMap
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
anaChanSend Mix b s () ()
mix SORT
c TERM ()
t ProcVarMap
vars
             let fqEvent :: EVENT
fqEvent = (SORT, SORT) -> TERM () -> Range -> EVENT
FQChanSend (SORT, SORT)
mfqChan TERM ()
fqTerm Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      ChanNonDetSend c :: SORT
c v :: VAR
v s :: SORT
s range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Channel nondeterministic send event" EVENT
e]
             {- mfqChan is the same as in chanSend case.
             fqVar is the fully qualfied version of the variable. -}
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, mfqChan :: (SORT, SORT)
mfqChan, fqVar :: TERM ()
fqVar) <- SORT
-> VAR
-> SORT
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
anaChanBinding SORT
c VAR
v SORT
s
             let fqEvent :: EVENT
fqEvent = (SORT, SORT) -> TERM () -> Range -> EVENT
FQChanNonDetSend (SORT, SORT)
mfqChan TERM ()
fqVar Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      ChanRecv c :: SORT
c v :: VAR
v s :: SORT
s range :: Range
range ->
          do [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> EVENT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "Channel receive event" EVENT
e]
             {- mfqChan is the same as in chanSend case.
             fqVar is the fully qualfied version of the variable. -}
             (alpha :: Set CommType
alpha, newVars :: ProcVarMap
newVars, mfqChan :: (SORT, SORT)
mfqChan, fqVar :: TERM ()
fqVar) <- SORT
-> VAR
-> SORT
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
anaChanBinding SORT
c VAR
v SORT
s
             let fqEvent :: EVENT
fqEvent = (SORT, SORT) -> TERM () -> Range -> EVENT
FQChanRecv (SORT, SORT)
mfqChan TERM ()
fqVar Range
range
             (Set CommType, ProcVarMap, EVENT)
-> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
newVars, EVENT
fqEvent)
      _ -> [Char] -> State CspCASLSign (Set CommType, ProcVarMap, EVENT)
forall a. HasCallStack => [Char] -> a
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 b s () ()
-> TERM ()
-> ProcVarMap
-> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
anaTermEvent mix :: Mix b s () ()
mix t :: TERM ()
t vars :: ProcVarMap
vars = do
  Maybe (TERM ())
mt <- Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
forall b s.
Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL Mix b s () ()
mix ProcVarMap
vars TERM ()
t
  let (alpha :: [CommType]
alpha, t' :: TERM ()
t') = case Maybe (TERM ())
mt of
                      -- return the alphabet and the fully qualified term
                      Just at :: TERM ()
at -> ([SORT -> CommType
CommTypeSort (TERM () -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM ()
at)], TERM ()
at)
                      -- return the empty alphabet and the original term
                      Nothing -> ([], TERM ()
t)
  (Set CommType, ProcVarMap, TERM ())
-> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
alpha, ProcVarMap
forall k a. Map k a
Map.empty, TERM ()
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 :: VAR
-> SORT -> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
anaPrefixChoice v :: VAR
v s :: SORT
s = do
  [SORT] -> State CspCASLSign ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT
s] -- check sort is known
  let alpha :: Set CommType
alpha = CommType -> Set CommType
forall a. a -> Set a
Set.singleton (CommType -> Set CommType) -> CommType -> Set CommType
forall a b. (a -> b) -> a -> b
$ SORT -> CommType
CommTypeSort SORT
s
  let binding :: ProcVarMap
binding = VAR -> SORT -> ProcVarMap
forall k a. k -> a -> Map k a
Map.singleton VAR
v SORT
s
  let fqVar :: TERM f
fqVar = VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
nullRange
  (Set CommType, ProcVarMap, TERM ())
-> State CspCASLSign (Set CommType, ProcVarMap, TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
alpha, ProcVarMap
binding, TERM ()
forall f. TERM f
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 b s () ()
-> SORT
-> TERM ()
-> ProcVarMap
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
anaChanSend mix :: Mix b s () ()
mix c :: SORT
c t :: TERM ()
t vars :: ProcVarMap
vars = do
  CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
  let ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
      msg :: [Char]
msg = "CspCASL.StatAnaCSP.anaChanSend: Channel Error"
  case Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> ChanNameMap -> Set SORT
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
c (ChanNameMap -> Set SORT) -> ChanNameMap -> Set SORT
forall a b. (a -> b) -> a -> b
$ CspSign -> ChanNameMap
chans CspSign
ext of
    [] -> do
      [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "unknown channel" SORT
c]
      {- Use old term as the fully qualified term and forget about the
      channel, there is an error in the spec -}
      (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, ProcVarMap
forall k a. Map k a
Map.empty, [Char] -> (SORT, SORT)
forall a. HasCallStack => [Char] -> a
error [Char]
msg, TERM ()
t)
    chanSorts :: [SORT]
chanSorts -> do
      Maybe (TERM ())
mt <- Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
forall b s.
Mix b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL Mix b s () ()
mix ProcVarMap
vars TERM ()
t
      case Maybe (TERM ())
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. -}
          (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, ProcVarMap
forall k a. Map k a
Map.empty, [Char] -> (SORT, SORT)
forall a. HasCallStack => [Char] -> a
error [Char]
msg, TERM ()
t)
        Just at :: TERM ()
at -> do
          let rs :: [Result (TERM ())]
rs = (SORT -> Result (TERM ())) -> [SORT] -> [Result (TERM ())]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: SORT
s -> TERM () -> SORT -> CspCASLSign -> Result (TERM ())
ccTermCast TERM ()
at SORT
s CspCASLSign
sig) [SORT]
chanSorts
          [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State CspCASLSign ())
-> [Diagnosis] -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ (Result (TERM ()) -> [Diagnosis])
-> [Result (TERM ())] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result (TERM ()) -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result (TERM ())]
rs
          case ((Result (TERM ()), SORT) -> Bool)
-> [(Result (TERM ()), SORT)] -> [(Result (TERM ()), SORT)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe (TERM ()) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (TERM ()) -> Bool)
-> ((Result (TERM ()), SORT) -> Maybe (TERM ()))
-> (Result (TERM ()), SORT)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result (TERM ()) -> Maybe (TERM ())
forall a. Result a -> Maybe a
maybeResult (Result (TERM ()) -> Maybe (TERM ()))
-> ((Result (TERM ()), SORT) -> Result (TERM ()))
-> (Result (TERM ()), SORT)
-> Maybe (TERM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Result (TERM ()), SORT) -> Result (TERM ())
forall a b. (a, b) -> a
fst) ([(Result (TERM ()), SORT)] -> [(Result (TERM ()), SORT)])
-> [(Result (TERM ()), SORT)] -> [(Result (TERM ()), SORT)]
forall a b. (a -> b) -> a -> b
$ [Result (TERM ())] -> [SORT] -> [(Result (TERM ()), SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Result (TERM ())]
rs [SORT]
chanSorts of
            [] ->
              {- cast failed. Use old term as the fully
              qualified term, and forget about the
              channel there is an error in the spec. -}
              (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, ProcVarMap
forall k a. Map k a
Map.empty, [Char] -> (SORT, SORT)
forall a. HasCallStack => [Char] -> a
error [Char]
msg, TERM ()
t)
            [(_, castSort :: SORT
castSort)] ->
              let alpha :: [CommType]
alpha = [ SORT -> CommType
CommTypeSort SORT
castSort
                          , TypedChanName -> CommType
CommTypeChan (TypedChanName -> CommType) -> TypedChanName -> CommType
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> TypedChanName
TypedChanName SORT
c SORT
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 (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
alpha, ProcVarMap
forall k a. Map k a
Map.empty, (SORT
c, SORT
castSort), TERM ()
at)
            cts :: [(Result (TERM ()), SORT)]
cts -> do -- fail due to an ambiguous chan sort
              [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> TERM () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error
                   ("ambiguous channel sorts " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SORT] -> [Char]
forall a. Show a => a -> [Char]
show (((Result (TERM ()), SORT) -> SORT)
-> [(Result (TERM ()), SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Result (TERM ()), SORT) -> SORT
forall a b. (a, b) -> b
snd [(Result (TERM ()), SORT)]
cts)) TERM ()
t]
              {- Use old term as the fully qualified term and forget about the
              channel, there is an error in the spec. -}
              (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, ProcVarMap
forall k a. Map k a
Map.empty, [Char] -> (SORT, SORT)
forall a. HasCallStack => [Char] -> a
error [Char]
msg, TERM ()
t)

getDeclaredChanSort :: (CHANNEL_NAME, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort :: (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (c :: SORT
c, s :: SORT
s) sig :: CspCASLSign
sig =
  let cm :: ChanNameMap
cm = CspSign -> ChanNameMap
chans (CspSign -> ChanNameMap) -> CspSign -> ChanNameMap
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
  in case Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> ChanNameMap -> Set SORT
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
c ChanNameMap
cm of
    [] -> [Char] -> SORT -> Result SORT
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError "unknown channel" SORT
c
    css :: [SORT]
css -> case (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ cs :: SORT
cs -> SORT
cs SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s Bool -> Bool -> Bool
|| SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (SORT -> CspCASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
cs CspCASLSign
sig))
                  [SORT]
css of
             [] -> [Char] -> SORT -> Result SORT
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError "sort not a subsort of channel's sort" SORT
s
             [cs :: SORT
cs] -> SORT -> Result SORT
forall (m :: * -> *) a. Monad m => a -> m a
return SORT
cs
             fcs :: [SORT]
fcs -> [Char] -> SORT -> Result SORT
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError ("ambiguous channel sorts " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SORT] -> [Char]
forall a. Show a => a -> [Char]
show [SORT]
fcs) SORT
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 :: SORT
-> VAR
-> SORT
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
anaChanBinding c :: SORT
c v :: VAR
v s :: SORT
s = do
  [SORT] -> State CspCASLSign ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts [SORT
s] -- check sort is known
  CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
  let qv :: TERM f
qv = VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
nullRange
      fqChan :: (SORT, SORT)
fqChan = (SORT
c, SORT
s)
      Result ds :: [Diagnosis]
ds ms :: Maybe SORT
ms = (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (SORT, SORT)
fqChan CspCASLSign
sig
  [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
  case Maybe SORT
ms of
    Nothing -> (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Set CommType
forall a. Set a
Set.empty, ProcVarMap
forall k a. Map k a
Map.empty, (SORT, SORT)
fqChan, TERM ()
forall f. TERM f
qv)
    Just _ ->
        let alpha :: [CommType]
alpha = [SORT -> CommType
CommTypeSort SORT
s, TypedChanName -> CommType
CommTypeChan (SORT -> SORT -> TypedChanName
TypedChanName SORT
c SORT
s)]
            binding :: [(VAR, SORT)]
binding = [(VAR
v, SORT
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 (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
-> State
     CspCASLSign (Set CommType, ProcVarMap, (SORT, SORT), TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
alpha, [(VAR, SORT)] -> ProcVarMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(VAR, SORT)]
binding, (SORT, SORT)
fqChan, TERM ()
forall f. TERM f
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 -> State CspCASLSign (Set CommType, RENAMING)
anaRenaming renaming :: RENAMING
renaming = case RENAMING
renaming of
  Renaming r :: [Rename]
r -> do
    [[Rename]]
fqRenamingTerms <- (Rename -> State CspCASLSign [Rename])
-> [Rename] -> State CspCASLSign [[Rename]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Rename -> State CspCASLSign [Rename]
anaRenamingItem [Rename]
r
    let rs :: [Rename]
rs = [[Rename]] -> [Rename]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Rename]]
fqRenamingTerms
    (Set CommType, RENAMING)
-> State CspCASLSign (Set CommType, RENAMING)
forall (m :: * -> *) a. Monad m => a -> m a
return ( (SORT -> CommType) -> Set SORT -> Set CommType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> CommType
CommTypeSort (Set SORT -> Set CommType) -> Set SORT -> Set CommType
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Rename -> Set SORT) -> [Rename] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map Rename -> Set SORT
alphaOfRename [Rename]
rs
           , [Rename] -> RENAMING
Renaming [Rename]
rs)

alphaOfRename :: Rename -> Set.Set SORT
alphaOfRename :: Rename -> Set SORT
alphaOfRename (Rename _ cm :: Maybe (RenameKind, Maybe (SORT, SORT))
cm) = case Maybe (RenameKind, Maybe (SORT, SORT))
cm of
  Just (_, Just (s1 :: SORT
s1, s2 :: SORT
s2)) -> [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT
s1, SORT
s2]
  _ -> Set SORT
forall a. Set a
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 :: Rename -> State CspCASLSign [Rename]
anaRenamingItem r :: Rename
r@(Rename ri :: SORT
ri cm :: Maybe (RenameKind, Maybe (SORT, SORT))
cm) = let
  predToRen :: (SORT, SORT) -> Rename
predToRen p :: (SORT, SORT)
p = SORT -> Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename
Rename SORT
ri (Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename)
-> Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename
forall a b. (a -> b) -> a -> b
$ (RenameKind, Maybe (SORT, SORT))
-> Maybe (RenameKind, Maybe (SORT, SORT))
forall a. a -> Maybe a
Just (RenameKind
BinPred, (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT, SORT)
p)
  opToRen :: (OpKind, (SORT, SORT)) -> Rename
opToRen (o :: OpKind
o, p :: (SORT, SORT)
p) = SORT -> Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename
Rename SORT
ri
    (Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename)
-> Maybe (RenameKind, Maybe (SORT, SORT)) -> Rename
forall a b. (a -> b) -> a -> b
$ (RenameKind, Maybe (SORT, SORT))
-> Maybe (RenameKind, Maybe (SORT, SORT))
forall a. a -> Maybe a
Just (if OpKind
o OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Total then RenameKind
TotOp else RenameKind
PartOp, (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT, SORT)
p)
  in case Maybe (RenameKind, Maybe (SORT, SORT))
cm of
  Just (k :: RenameKind
k, ms :: Maybe (SORT, SORT)
ms) -> case RenameKind
k of
    BinPred -> do
      [(SORT, SORT)]
ps <- SORT -> State CspCASLSign [(SORT, SORT)]
getBinPredsById SORT
ri
      let realPs :: [(SORT, SORT)]
realPs = case Maybe (SORT, SORT)
ms of
                     Nothing -> [(SORT, SORT)]
ps
                     Just p :: (SORT, SORT)
p -> ((SORT, SORT) -> Bool) -> [(SORT, SORT)] -> [(SORT, SORT)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SORT, SORT) -> (SORT, SORT) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, SORT)
p) [(SORT, SORT)]
ps
      Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(SORT, SORT)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SORT, SORT)]
realPs)
        (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Rename -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "renaming predicate not found" Rename
r]
      Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(SORT, SORT)] -> Bool
forall a. [a] -> Bool
isSingle [(SORT, SORT)]
realPs)
        (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Rename -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "multiple predicates found" Rename
r]
      [Rename] -> State CspCASLSign [Rename]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Rename] -> State CspCASLSign [Rename])
-> [Rename] -> State CspCASLSign [Rename]
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> Rename) -> [(SORT, SORT)] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> Rename
predToRen [(SORT, SORT)]
realPs
    _ -> do
      [(OpKind, (SORT, SORT))]
os <- SORT -> State CspCASLSign [(OpKind, (SORT, SORT))]
getUnaryOpsById SORT
ri
      -- we ignore the user given op kind here!
      let realOs :: [(OpKind, (SORT, SORT))]
realOs = case Maybe (SORT, SORT)
ms of
                     Nothing -> [(OpKind, (SORT, SORT))]
os
                     Just p :: (SORT, SORT)
p -> ((OpKind, (SORT, SORT)) -> Bool)
-> [(OpKind, (SORT, SORT))] -> [(OpKind, (SORT, SORT))]
forall a. (a -> Bool) -> [a] -> [a]
filter (((SORT, SORT) -> (SORT, SORT) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, SORT)
p) ((SORT, SORT) -> Bool)
-> ((OpKind, (SORT, SORT)) -> (SORT, SORT))
-> (OpKind, (SORT, SORT))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpKind, (SORT, SORT)) -> (SORT, SORT)
forall a b. (a, b) -> b
snd) [(OpKind, (SORT, SORT))]
os
      Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(OpKind, (SORT, SORT))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(OpKind, (SORT, SORT))]
realOs)
        (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Rename -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "renaming operation not found" Rename
r]
      Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(OpKind, (SORT, SORT))] -> Bool
forall a. [a] -> Bool
isSingle [(OpKind, (SORT, SORT))]
realOs)
        (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Rename -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "multiple operations found" Rename
r]
      Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (RenameKind
k RenameKind -> RenameKind -> Bool
forall a. Eq a => a -> a -> Bool
== RenameKind
TotOp) (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$
        ((OpKind, (SORT, SORT)) -> State CspCASLSign ())
-> [(OpKind, (SORT, SORT))] -> State CspCASLSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (o :: OpKind
o, (s1 :: SORT
s1, s2 :: SORT
s2)) -> Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OpKind
o OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Partial)
          (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Rename -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error
                     ("operation of type '"
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows SORT
s1 " -> "
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows SORT
s2 "' is not total") Rename
r]) [(OpKind, (SORT, SORT))]
realOs
      [Rename] -> State CspCASLSign [Rename]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Rename] -> State CspCASLSign [Rename])
-> [Rename] -> State CspCASLSign [Rename]
forall a b. (a -> b) -> a -> b
$ ((OpKind, (SORT, SORT)) -> Rename)
-> [(OpKind, (SORT, SORT))] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map (OpKind, (SORT, SORT)) -> Rename
opToRen [(OpKind, (SORT, SORT))]
realOs
  Nothing -> do
    [(SORT, SORT)]
ps <- SORT -> State CspCASLSign [(SORT, SORT)]
getBinPredsById SORT
ri
    [(OpKind, (SORT, SORT))]
os <- SORT -> State CspCASLSign [(OpKind, (SORT, SORT))]
getUnaryOpsById SORT
ri
    let rs :: [Rename]
rs = ((SORT, SORT) -> Rename) -> [(SORT, SORT)] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> Rename
predToRen [(SORT, SORT)]
ps [Rename] -> [Rename] -> [Rename]
forall a. [a] -> [a] -> [a]
++ ((OpKind, (SORT, SORT)) -> Rename)
-> [(OpKind, (SORT, SORT))] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map (OpKind, (SORT, SORT)) -> Rename
opToRen [(OpKind, (SORT, SORT))]
os
    Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Rename] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rename]
rs)
      (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "renaming predicate or operation not found" SORT
ri]
    Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Rename] -> Bool
forall a. [a] -> Bool
isSingle [Rename]
rs)
      (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "multiple renamings found" SORT
ri]
    [Rename] -> State CspCASLSign [Rename]
forall (m :: * -> *) a. Monad m => a -> m a
return [Rename]
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 :: SORT -> State CspCASLSign [(OpKind, (SORT, SORT))]
getUnaryOpsById ri :: SORT
ri = do
  OpMap
om <- (CspCASLSign -> OpMap) -> State CspCASLSign OpMap
forall s a. (s -> a) -> State s a
gets CspCASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap
  [(OpKind, (SORT, SORT))]
-> State CspCASLSign [(OpKind, (SORT, SORT))]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(OpKind, (SORT, SORT))]
 -> State CspCASLSign [(OpKind, (SORT, SORT))])
-> [(OpKind, (SORT, SORT))]
-> State CspCASLSign [(OpKind, (SORT, SORT))]
forall a b. (a -> b) -> a -> b
$ (OpType -> [(OpKind, (SORT, SORT))] -> [(OpKind, (SORT, SORT))])
-> [(OpKind, (SORT, SORT))]
-> Set OpType
-> [(OpKind, (SORT, SORT))]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ oty :: OpType
oty -> case OpType
oty of
     OpType k :: OpKind
k [s1 :: SORT
s1] s2 :: SORT
s2 -> ((OpKind
k, (SORT
s1, SORT
s2)) (OpKind, (SORT, SORT))
-> [(OpKind, (SORT, SORT))] -> [(OpKind, (SORT, SORT))]
forall a. a -> [a] -> [a]
:)
     _ -> [(OpKind, (SORT, SORT))] -> [(OpKind, (SORT, SORT))]
forall a. a -> a
id) [] (Set OpType -> [(OpKind, (SORT, SORT))])
-> Set OpType -> [(OpKind, (SORT, SORT))]
forall a b. (a -> b) -> a -> b
$ SORT -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
ri OpMap
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 :: SORT -> State CspCASLSign [(SORT, SORT)]
getBinPredsById ri :: SORT
ri = do
  PredMap
pm <- (CspCASLSign -> PredMap) -> State CspCASLSign PredMap
forall s a. (s -> a) -> State s a
gets CspCASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap
  [(SORT, SORT)] -> State CspCASLSign [(SORT, SORT)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(SORT, SORT)] -> State CspCASLSign [(SORT, SORT)])
-> [(SORT, SORT)] -> State CspCASLSign [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ (PredType -> [(SORT, SORT)] -> [(SORT, SORT)])
-> [(SORT, SORT)] -> Set PredType -> [(SORT, SORT)]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ pty :: PredType
pty -> case PredType
pty of
     PredType [s1 :: SORT
s1, s2 :: SORT
s2] -> ((SORT
s1, SORT
s2) (SORT, SORT) -> [(SORT, SORT)] -> [(SORT, SORT)]
forall a. a -> [a] -> [a]
:)
     _ -> [(SORT, SORT)] -> [(SORT, SORT)]
forall a. a -> a
id) [] (Set PredType -> [(SORT, SORT)]) -> Set PredType -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
ri PredMap
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 :: Set CommType
-> Set CommType -> PROCESS -> [Char] -> State CspCASLSign ()
checkCommAlphaSub sub :: Set CommType
sub super :: Set CommType
super proc :: PROCESS
proc context :: [Char]
context = do
  Rel SORT
sr <- (CspCASLSign -> Rel SORT) -> State CspCASLSign (Rel SORT)
forall s a. (s -> a) -> State s a
gets CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel
  let extras :: Set CommType
extras = Rel SORT -> Set CommType -> Set CommType
closeCspCommAlpha Rel SORT
sr Set CommType
sub
        Set CommType -> Set CommType -> Set CommType
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Rel SORT -> Set CommType -> Set CommType
closeCspCommAlpha Rel SORT
sr Set CommType
super
  Bool -> State CspCASLSign () -> State CspCASLSign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set CommType -> Bool
forall a. Set a -> Bool
Set.null Set CommType
extras) (State CspCASLSign () -> State CspCASLSign ())
-> State CspCASLSign () -> State CspCASLSign ()
forall a b. (a -> b) -> a -> b
$
            let err :: [Char]
err = "Communication alphabet subset violations (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                       [Char]
context [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ")" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Set CommType -> Doc
printCommAlpha Set CommType
extras)
            in [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> PROCESS -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error [Char]
err PROCESS
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 b s () ()
-> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL mix :: Mix b s () ()
mix pm :: ProcVarMap
pm t :: TERM ()
t = do
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    let newVars :: ProcVarMap
newVars = ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ProcVarMap
pm (CspCASLSign -> ProcVarMap
forall f e. Sign f e -> ProcVarMap
varMap CspCASLSign
sig)
        sigext :: CspCASLSign
sigext = CspCASLSign
sig { varMap :: ProcVarMap
varMap = ProcVarMap
newVars }
        Result ds :: [Diagnosis]
ds mt :: Maybe (TERM ())
mt = Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
forall b s.
Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
anaTermCspCASL' Mix b s () ()
mix CspCASLSign
sigext TERM ()
t
    [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
    Maybe (TERM ()) -> State CspCASLSign (Maybe (TERM ()))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TERM ())
mt

idSetOfSig :: CspCASLSign -> IdSets
idSetOfSig :: CspCASLSign -> IdSets
idSetOfSig sig :: CspCASLSign
sig =
  [IdSets] -> IdSets
unite [Set SORT -> Set SORT -> Set SORT -> IdSets
mkIdSets (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allConstIds CspCASLSign
sig) (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allOpIds CspCASLSign
sig) (Set SORT -> IdSets) -> Set SORT -> IdSets
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allPredIds CspCASLSign
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 b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
anaTermCspCASL' mix :: Mix b s () ()
mix sig :: CspCASLSign
sig trm :: TERM ()
trm = ((TERM (), TERM ()) -> TERM ())
-> Result (TERM (), TERM ()) -> Result (TERM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TERM (), TERM ()) -> TERM ()
forall a b. (a, b) -> b
snd (Result (TERM (), TERM ()) -> Result (TERM ()))
-> Result (TERM (), TERM ()) -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ Min () ()
-> Mix b s () ()
-> Sign () ()
-> Maybe SORT
-> Range
-> TERM ()
-> Result (TERM (), TERM ())
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
anaTerm ((() -> Result ()) -> Min () ()
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix b s () ()
mix
 (CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
sig) Maybe SORT
forall a. Maybe a
Nothing (TERM () -> Range
forall a. GetRange a => a -> Range
getRange TERM ()
trm) TERM ()
trm

-- | Attempt to cast a CASL term to a particular CASL sort.
ccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
ccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
ccTermCast t :: TERM ()
t cSort :: SORT
cSort sig :: CspCASLSign
sig = let
  pos :: Range
pos = TERM () -> Range
forall a. GetRange a => a -> Range
getRange TERM ()
t
  msg :: [Char] -> [Char]
msg = ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "cast term to sort " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
cSort)
  in case TERM () -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort TERM ()
t of
  Nothing -> [Char] -> TERM () -> Result (TERM ())
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError "term without type" TERM ()
t
  Just termSort :: SORT
termSort
    | SORT
termSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
cSort -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return TERM ()
t
    | SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
termSort (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> CspCASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
cSort CspCASLSign
sig ->
        TERM () -> [Char] -> Range -> Result (TERM ())
forall a. a -> [Char] -> Range -> Result a
hint (TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
t SORT
cSort Range
pos) ([Char] -> [Char]
msg "up") Range
pos
    | SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
termSort (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> CspCASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
cSort CspCASLSign
sig ->
        TERM () -> [Char] -> Range -> Result (TERM ())
forall a. a -> [Char] -> Range -> Result a
hint (TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Cast TERM ()
t SORT
cSort Range
pos) ([Char] -> [Char]
msg "down") Range
pos
    | Bool
otherwise -> [Char] -> Range -> Result (TERM ())
forall a. [Char] -> Range -> Result a
fatal_error ([Char] -> [Char]
msg "cannot ") Range
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 b s () ()
-> ProcVarMap
-> FORMULA ()
-> State CspCASLSign (Maybe (FORMULA ()))
anaFormulaCspCASL mix :: Mix b s () ()
mix pm :: ProcVarMap
pm f :: FORMULA ()
f = do
    [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> FORMULA () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Debug "anaFormulaCspCASL" FORMULA ()
f]
    CspCASLSign
sig <- State CspCASLSign CspCASLSign
forall s. State s s
get
    let newVars :: ProcVarMap
newVars = ProcVarMap -> ProcVarMap -> ProcVarMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ProcVarMap
pm (CspCASLSign -> ProcVarMap
forall f e. Sign f e -> ProcVarMap
varMap CspCASLSign
sig)
        sigext :: CspCASLSign
sigext = CspCASLSign
sig { varMap :: ProcVarMap
varMap = ProcVarMap
newVars }
        Result ds :: [Diagnosis]
ds mt :: Maybe (FORMULA ())
mt = Mix b s () () -> CspCASLSign -> FORMULA () -> Result (FORMULA ())
forall b s.
Mix b s () () -> CspCASLSign -> FORMULA () -> Result (FORMULA ())
anaFormulaCspCASL' Mix b s () ()
mix CspCASLSign
sigext FORMULA ()
f
    [Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
    Maybe (FORMULA ()) -> State CspCASLSign (Maybe (FORMULA ()))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (FORMULA ())
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 b s () () -> CspCASLSign -> FORMULA () -> Result (FORMULA ())
anaFormulaCspCASL' mix :: Mix b s () ()
mix sig :: CspCASLSign
sig =
  ((FORMULA (), FORMULA ()) -> FORMULA ())
-> Result (FORMULA (), FORMULA ()) -> Result (FORMULA ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FORMULA (), FORMULA ()) -> FORMULA ()
forall a b. (a, b) -> b
snd (Result (FORMULA (), FORMULA ()) -> Result (FORMULA ()))
-> (FORMULA () -> Result (FORMULA (), FORMULA ()))
-> FORMULA ()
-> Result (FORMULA ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Min () ()
-> Mix b s () ()
-> Sign () ()
-> FORMULA ()
-> Result (FORMULA (), FORMULA ())
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm ((() -> Result ()) -> Min () ()
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix b s () ()
mix (CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
sig)

{- | Compute the communication alphabet arising from a formula
occurring in a CspCASL process term. -}
formulaComms :: FORMULA () -> CommAlpha
formulaComms :: FORMULA () -> Set CommType
formulaComms = (SORT -> CommType) -> Set SORT -> Set CommType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> CommType
CommTypeSort (Set SORT -> Set CommType)
-> (FORMULA () -> Set SORT) -> FORMULA () -> Set CommType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record () (Set SORT) (Set SORT) -> FORMULA () -> Set SORT
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
  ((() -> Set SORT)
-> ([Set SORT] -> Set SORT)
-> Set SORT
-> Record () (Set SORT) (Set SORT)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (Set SORT -> () -> Set SORT
forall a b. a -> b -> a
const Set SORT
forall a. Set a
Set.empty) [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set SORT
forall a. Set a
Set.empty)
  { foldQuantification :: FORMULA ()
-> QUANTIFIER -> [VAR_DECL] -> Set SORT -> Range -> Set SORT
foldQuantification = \ _ _ varDecls :: [VAR_DECL]
varDecls f :: Set SORT
f _ ->
      let vdSort :: VAR_DECL -> SORT
vdSort (Var_decl _ s :: SORT
s _) = SORT
s in
      Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SORT
f (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ((VAR_DECL -> SORT) -> [VAR_DECL] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> SORT
vdSort [VAR_DECL]
varDecls)
  , foldQual_var :: TERM () -> VAR -> SORT -> Range -> Set SORT
foldQual_var = \ _ _ s :: SORT
s _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
s
  , foldApplication :: TERM () -> OP_SYMB -> [Set SORT] -> Range -> Set SORT
foldApplication = \ _ o :: OP_SYMB
o _ _ -> case OP_SYMB
o of
       Op_name _ -> Set SORT
forall a. Set a
Set.empty
       Qual_op_name _ ty :: OP_TYPE
ty _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton (SORT -> Set SORT) -> SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ty
  , foldSorted_term :: TERM () -> Set SORT -> SORT -> Range -> Set SORT
foldSorted_term = \ _ _ s :: SORT
s _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
s
  , foldCast :: TERM () -> Set SORT -> SORT -> Range -> Set SORT
foldCast = \ _ _ s :: SORT
s _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
s }