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
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
[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
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]
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 }}
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
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
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
ProcProfile
profile <- [SORT] -> PROC_ALPHABET -> State CspCASLSign ProcProfile
anaProcAlphabet [SORT]
argSorts PROC_ALPHABET
comms
if SORT -> ProcProfile -> ProcNameMap -> Bool
isNameInProcNameMap SORT
name ProcProfile
profile ProcNameMap
oldProcDecls
then
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
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 }}
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'
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 ->
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
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 =
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
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
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"
[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
$
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}]
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)
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)
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
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"
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 ->
(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)
(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]
(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)
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
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
[Diagnosis] -> State CspCASLSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
case Maybe (TERM ())
at' of
Nothing ->
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''
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
(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 }
(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)
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
(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
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
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]
(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]
(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]
(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"
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
Just at :: TERM ()
at -> ([SORT -> CommType
CommTypeSort (TERM () -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM ()
at)], TERM ()
at)
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')
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]
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)
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]
(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 ->
(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
[] ->
(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]
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
[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]
(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
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]
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)]
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)
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
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
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
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
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
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]
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]
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
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
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
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)
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 }