{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CspCASL/SignCSP.hs
Description :  CspCASL signatures
Copyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  M.Roggenbach@swansea.ac.uk
Stability   :  provisional
Portability :  portable

signatures for CSP-CASL
-}

module CspCASL.SignCSP
  ( addProcNameToProcNameMap
  , ccSig2CASLSign
  , ccSig2CspSign
  , ChanNameMap
  , closeCspCommAlpha
  , CspCASLSign
  , CspCASLSen
  , CspSen (..)
  , CspSign (..)
  , cspSignUnion
  , diffCspSig
  , emptyCspCASLSign
  , emptyCspSign
  , FQProcVarList
  , getUniqueProfileInProcNameMap
  , isCspCASLSubSig
  , isCspSubSign
  , isNameInProcNameMap
  , isProcessEq
  , ProcNameMap
  , ProcVarList
  , ProcVarMap
  , reduceProcProfile
  , commType2Sort
  , relatedSorts
  , relatedProcs
  , unionCspCASLSign
  ) where

import CASL.AS_Basic_CASL
import CASL.Overload
import CASL.Sign
import CASL.ToDoc

import CspCASL.AS_CspCASL_Process
import CspCASL.AS_CspCASL ()
import CspCASL.CspCASL_Keywords
import qualified CspCASL.LocalTop as LocalTop
import CspCASL.Print_CspCASL ()

import Common.AnnoState
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Lib.Rel (Rel, predecessors, member)
import qualified Common.Lib.MapSet as MapSet
import Common.Utils (keepMins)

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Data
import Data.List
import Data.Ord

type ChanNameMap = MapSet.MapSet CHANNEL_NAME SORT
type ProcNameMap = MapSet.MapSet PROCESS_NAME ProcProfile
type ProcVarMap = Map.Map SIMPLE_ID SORT
type ProcVarList = [(SIMPLE_ID, SORT)]

-- | Add a process name and its profile to a process name map.  exist.
addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap
  -> ProcNameMap
addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap
addProcNameToProcNameMap = PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert

-- | Test if a simple process name with a profile is in the process name map.
isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
isNameInProcNameMap = PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member

{- | Given a simple process name and a required number of parameters, find a
unqiue profile with that many parameters if possible. If this is not possible
(i.e., name does not exist, or no profile with the required number of
arguments or not unique profile for the required number of arguments), then
the functions returns a failed result with a helpful error message.  failure. -}
getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
                                 Result ProcProfile
getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap -> Result ProcProfile
getUniqueProfileInProcNameMap name :: PROCESS_NAME
name numParams :: Int
numParams pm :: ProcNameMap
pm =
  let profiles :: Set ProcProfile
profiles = PROCESS_NAME -> ProcNameMap -> Set ProcProfile
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup PROCESS_NAME
name ProcNameMap
pm
      isMatch :: ProcProfile -> Bool
isMatch (ProcProfile argSorts :: PROC_ARGS
argSorts _) =
        PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
argSorts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
numParams
      matchedProfiles :: Set ProcProfile
matchedProfiles = (ProcProfile -> Bool) -> Set ProcProfile -> Set ProcProfile
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ProcProfile -> Bool
isMatch Set ProcProfile
profiles
  in case Set ProcProfile -> [ProcProfile]
forall a. Set a -> [a]
Set.toList Set ProcProfile
matchedProfiles of
       [] -> String -> PROCESS_NAME -> Result ProcProfile
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("Process name not in signature with "
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numParams String -> String -> String
forall a. [a] -> [a] -> [a]
++ " parameters:") PROCESS_NAME
name
       [p :: ProcProfile
p] -> ProcProfile -> Result ProcProfile
forall (m :: * -> *) a. Monad m => a -> m a
return ProcProfile
p
       _ -> String -> PROCESS_NAME -> Result ProcProfile
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("Process name not unique in signature with "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numParams String -> String -> String
forall a. [a] -> [a] -> [a]
++ " parameters:") PROCESS_NAME
name

-- Close a communication alphabet under CASL subsort
closeCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
closeCspCommAlpha :: Rel PROCESS_NAME -> CommAlpha -> CommAlpha
closeCspCommAlpha sr :: Rel PROCESS_NAME
sr =
    [CommAlpha] -> CommAlpha
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([CommAlpha] -> CommAlpha)
-> (CommAlpha -> [CommAlpha]) -> CommAlpha -> CommAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set CommAlpha -> [CommAlpha]
forall a. Set a -> [a]
Set.toList (Set CommAlpha -> [CommAlpha])
-> (CommAlpha -> Set CommAlpha) -> CommAlpha -> [CommAlpha]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CommType -> CommAlpha) -> CommAlpha -> Set CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Rel PROCESS_NAME -> CommType -> CommAlpha
closeOneCspComm Rel PROCESS_NAME
sr)

-- Close one CommType under CASL subsort
closeOneCspComm :: Rel SORT -> CommType -> CommAlpha
closeOneCspComm :: Rel PROCESS_NAME -> CommType -> CommAlpha
closeOneCspComm sr :: Rel PROCESS_NAME
sr x :: CommType
x = let
  mkTypedChan :: PROCESS_NAME -> PROCESS_NAME -> CommType
mkTypedChan c :: PROCESS_NAME
c s :: PROCESS_NAME
s = TypedChanName -> CommType
CommTypeChan (TypedChanName -> CommType) -> TypedChanName -> CommType
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME -> PROCESS_NAME -> TypedChanName
TypedChanName PROCESS_NAME
c PROCESS_NAME
s
  subsorts :: PROCESS_NAME -> Set PROCESS_NAME
subsorts s' :: PROCESS_NAME
s' = PROCESS_NAME -> Set PROCESS_NAME -> Set PROCESS_NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert PROCESS_NAME
s' (Set PROCESS_NAME -> Set PROCESS_NAME)
-> Set PROCESS_NAME -> Set PROCESS_NAME
forall a b. (a -> b) -> a -> b
$ Rel PROCESS_NAME -> PROCESS_NAME -> Set PROCESS_NAME
forall a. Ord a => Rel a -> a -> Set a
predecessors Rel PROCESS_NAME
sr PROCESS_NAME
s'
  in case CommType
x of
    CommTypeSort s :: PROCESS_NAME
s ->
        (PROCESS_NAME -> CommType) -> Set PROCESS_NAME -> CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map PROCESS_NAME -> CommType
CommTypeSort (PROCESS_NAME -> Set PROCESS_NAME
subsorts PROCESS_NAME
s)
    CommTypeChan (TypedChanName c :: PROCESS_NAME
c s :: PROCESS_NAME
s) ->
        (PROCESS_NAME -> CommType) -> Set PROCESS_NAME -> CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map PROCESS_NAME -> CommType
CommTypeSort (PROCESS_NAME -> Set PROCESS_NAME
subsorts PROCESS_NAME
s)
      CommAlpha -> CommAlpha -> CommAlpha
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (PROCESS_NAME -> CommType) -> Set PROCESS_NAME -> CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (PROCESS_NAME -> PROCESS_NAME -> CommType
mkTypedChan PROCESS_NAME
c) (PROCESS_NAME -> Set PROCESS_NAME
subsorts PROCESS_NAME
s)

{- | Remove the implicit sorts from the proc name map under a sub-sort
relation. Assumes all the proc profile's comms are in the sub sort relation and
simply makes the comms contain only the minimal super sorts under the sub-sort
relation. -}
reduceProcNamesInSig :: Rel SORT -> CspSign -> CspSign
reduceProcNamesInSig :: Rel PROCESS_NAME -> CspSign -> CspSign
reduceProcNamesInSig sr :: Rel PROCESS_NAME
sr cspSig :: CspSign
cspSig =
  CspSign
cspSig { procSet :: ProcNameMap
procSet = Rel PROCESS_NAME -> ProcNameMap -> ProcNameMap
reduceProcNameMap Rel PROCESS_NAME
sr (ProcNameMap -> ProcNameMap) -> ProcNameMap -> ProcNameMap
forall a b. (a -> b) -> a -> b
$ CspSign -> ProcNameMap
procSet CspSign
cspSig }

{- | Remove the implicit sorts from a proc name map under a sub-sort
relation. Assumes all the proc profile's comms are in the sub sort relation and
simply makes the comms contain only the minimal super sorts under the sub-sort
relation. -}
reduceProcNameMap :: Rel SORT -> ProcNameMap -> ProcNameMap
reduceProcNameMap :: Rel PROCESS_NAME -> ProcNameMap -> ProcNameMap
reduceProcNameMap sr :: Rel PROCESS_NAME
sr =
  (ProcProfile -> ProcProfile) -> ProcNameMap -> ProcNameMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map (Rel PROCESS_NAME -> ProcProfile -> ProcProfile
reduceProcProfile Rel PROCESS_NAME
sr)

{- | Remove the implicit sorts from a profile under a sub-sort relation. Assumes
all the proc profile's comms are in the sub sort relation and simply makes the
comms contain only the minimal super sorts under the sub-sort relation. -}
reduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile
reduceProcProfile :: Rel PROCESS_NAME -> ProcProfile -> ProcProfile
reduceProcProfile sr :: Rel PROCESS_NAME
sr (ProcProfile argSorts :: PROC_ARGS
argSorts comms :: CommAlpha
comms) =
  PROC_ARGS -> CommAlpha -> ProcProfile
ProcProfile PROC_ARGS
argSorts (Rel PROCESS_NAME -> CommAlpha -> CommAlpha
reduceCspCommAlpha Rel PROCESS_NAME
sr CommAlpha
comms)

{- | Remove the implicit sorts from a CommAlpha under a sub-sort
relation. Assumes all the proc profile's comms are in the sub sort relation and
simply makes the comms contain only the minimal super sorts under the sub-sort
relation. -}
reduceCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
reduceCspCommAlpha :: Rel PROCESS_NAME -> CommAlpha -> CommAlpha
reduceCspCommAlpha sr :: Rel PROCESS_NAME
sr =
  [CommType] -> CommAlpha
forall a. Ord a => [a] -> Set a
Set.fromList ([CommType] -> CommAlpha)
-> (CommAlpha -> [CommType]) -> CommAlpha -> CommAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ([CommType] -> [CommType]) -> [[CommType]] -> [CommType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CommType -> CommType -> Bool) -> [CommType] -> [CommType]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins ((CommType -> CommType -> Bool) -> [CommType] -> [CommType])
-> (CommType -> CommType -> Bool) -> [CommType] -> [CommType]
forall a b. (a -> b) -> a -> b
$ Rel PROCESS_NAME -> CommType -> CommType -> Bool
cmpCommType Rel PROCESS_NAME
sr) ([[CommType]] -> [CommType])
-> (CommAlpha -> [[CommType]]) -> CommAlpha -> [CommType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CommType -> CommType -> Bool) -> [CommType] -> [[CommType]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy CommType -> CommType -> Bool
sameChan ([CommType] -> [[CommType]])
-> (CommAlpha -> [CommType]) -> CommAlpha -> [[CommType]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList

cmpCommType :: Rel SORT -> CommType -> CommType -> Bool
cmpCommType :: Rel PROCESS_NAME -> CommType -> CommType -> Bool
cmpCommType rel :: Rel PROCESS_NAME
rel t1 :: CommType
t1 t2 :: CommType
t2 = let
  s1 :: PROCESS_NAME
s1 = CommType -> PROCESS_NAME
commType2Sort CommType
t1
  s2 :: PROCESS_NAME
s2 = CommType -> PROCESS_NAME
commType2Sort CommType
t2
  in PROCESS_NAME
s1 PROCESS_NAME -> PROCESS_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PROCESS_NAME
s2 Bool -> Bool -> Bool
|| PROCESS_NAME -> PROCESS_NAME -> Rel PROCESS_NAME -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
member PROCESS_NAME
s2 PROCESS_NAME
s1 Rel PROCESS_NAME
rel

commType2Sort :: CommType -> SORT
commType2Sort :: CommType -> PROCESS_NAME
commType2Sort c :: CommType
c = case CommType
c of
  CommTypeSort s :: PROCESS_NAME
s -> PROCESS_NAME
s
  CommTypeChan (TypedChanName _ s :: PROCESS_NAME
s) -> PROCESS_NAME
s

sameChan :: CommType -> CommType -> Bool
sameChan :: CommType -> CommType -> Bool
sameChan t1 :: CommType
t1 t2 :: CommType
t2 = case (CommType
t1, CommType
t2) of
  (CommTypeSort _, CommTypeSort _) -> Bool
True
  (CommTypeChan (TypedChanName c1 :: PROCESS_NAME
c1 _), CommTypeChan (TypedChanName c2 :: PROCESS_NAME
c2 _))
      -> PROCESS_NAME
c1 PROCESS_NAME -> PROCESS_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PROCESS_NAME
c2
  _ -> Bool
False

-- | CSP process signature.
data CspSign = CspSign
    { CspSign -> ChanNameMap
chans :: ChanNameMap
    , CspSign -> ProcNameMap
procSet :: ProcNameMap
    } deriving (Int -> CspSign -> String -> String
[CspSign] -> String -> String
CspSign -> String
(Int -> CspSign -> String -> String)
-> (CspSign -> String)
-> ([CspSign] -> String -> String)
-> Show CspSign
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CspSign] -> String -> String
$cshowList :: [CspSign] -> String -> String
show :: CspSign -> String
$cshow :: CspSign -> String
showsPrec :: Int -> CspSign -> String -> String
$cshowsPrec :: Int -> CspSign -> String -> String
Show, CspSign -> CspSign -> Bool
(CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> Bool) -> Eq CspSign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspSign -> CspSign -> Bool
$c/= :: CspSign -> CspSign -> Bool
== :: CspSign -> CspSign -> Bool
$c== :: CspSign -> CspSign -> Bool
Eq, Eq CspSign
Eq CspSign =>
(CspSign -> CspSign -> Ordering)
-> (CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> CspSign)
-> (CspSign -> CspSign -> CspSign)
-> Ord CspSign
CspSign -> CspSign -> Bool
CspSign -> CspSign -> Ordering
CspSign -> CspSign -> CspSign
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CspSign -> CspSign -> CspSign
$cmin :: CspSign -> CspSign -> CspSign
max :: CspSign -> CspSign -> CspSign
$cmax :: CspSign -> CspSign -> CspSign
>= :: CspSign -> CspSign -> Bool
$c>= :: CspSign -> CspSign -> Bool
> :: CspSign -> CspSign -> Bool
$c> :: CspSign -> CspSign -> Bool
<= :: CspSign -> CspSign -> Bool
$c<= :: CspSign -> CspSign -> Bool
< :: CspSign -> CspSign -> Bool
$c< :: CspSign -> CspSign -> Bool
compare :: CspSign -> CspSign -> Ordering
$ccompare :: CspSign -> CspSign -> Ordering
$cp1Ord :: Eq CspSign
Ord, Typeable, Typeable CspSign
Constr
DataType
Typeable CspSign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspSign -> c CspSign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspSign)
-> (CspSign -> Constr)
-> (CspSign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspSign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign))
-> ((forall b. Data b => b -> b) -> CspSign -> CspSign)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSign -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSign -> r)
-> (forall u. (forall d. Data d => d -> u) -> CspSign -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CspSign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CspSign -> m CspSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSign -> m CspSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSign -> m CspSign)
-> Data CspSign
CspSign -> Constr
CspSign -> DataType
(forall b. Data b => b -> b) -> CspSign -> CspSign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSign -> c CspSign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSign
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CspSign -> u
forall u. (forall d. Data d => d -> u) -> CspSign -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSign -> m CspSign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSign -> m CspSign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSign -> c CspSign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign)
$cCspSign :: Constr
$tCspSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CspSign -> m CspSign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSign -> m CspSign
gmapMp :: (forall d. Data d => d -> m d) -> CspSign -> m CspSign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSign -> m CspSign
gmapM :: (forall d. Data d => d -> m d) -> CspSign -> m CspSign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSign -> m CspSign
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CspSign -> u
gmapQ :: (forall d. Data d => d -> u) -> CspSign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspSign -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSign -> r
gmapT :: (forall b. Data b => b -> b) -> CspSign -> CspSign
$cgmapT :: (forall b. Data b => b -> b) -> CspSign -> CspSign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspSign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSign)
dataTypeOf :: CspSign -> DataType
$cdataTypeOf :: CspSign -> DataType
toConstr :: CspSign -> Constr
$ctoConstr :: CspSign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSign -> c CspSign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSign -> c CspSign
$cp1Data :: Typeable CspSign
Data)

-- | plain union
cspSignUnion :: CspSign -> CspSign -> CspSign
cspSignUnion :: CspSign -> CspSign -> CspSign
cspSignUnion sign1 :: CspSign
sign1 sign2 :: CspSign
sign2 = CspSign
emptyCspSign
    { chans :: ChanNameMap
chans = CspSign -> ChanNameMap
chans CspSign
sign1 ChanNameMap -> ChanNameMap -> ChanNameMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
`MapSet.union` CspSign -> ChanNameMap
chans CspSign
sign2
    , procSet :: ProcNameMap
procSet = CspSign -> ProcNameMap
procSet CspSign
sign1 ProcNameMap -> ProcNameMap -> ProcNameMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
`MapSet.union` CspSign -> ProcNameMap
procSet CspSign
sign2 }

{- | A CspCASL signature is a CASL signature with a CSP process
signature in the extendedInfo part. -}
type CspCASLSign = Sign CspSen CspSign

ccSig2CASLSign :: CspCASLSign -> CASLSign
ccSig2CASLSign :: CspCASLSign -> CASLSign
ccSig2CASLSign sigma :: CspCASLSign
sigma = CspCASLSign
sigma { extendedInfo :: ()
extendedInfo = (), sentences :: [Named (FORMULA ())]
sentences = [] }

-- | Projection from CspCASL signature to Csp signature
ccSig2CspSign :: CspCASLSign -> CspSign
ccSig2CspSign :: CspCASLSign -> CspSign
ccSig2CspSign = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo

-- | Empty CspCASL signature.
emptyCspCASLSign :: CspCASLSign
emptyCspCASLSign :: CspCASLSign
emptyCspCASLSign = CspSign -> CspCASLSign
forall e f. e -> Sign f e
emptySign CspSign
emptyCspSign

-- | Empty CSP process signature.
emptyCspSign :: CspSign
emptyCspSign :: CspSign
emptyCspSign = CspSign :: ChanNameMap -> ProcNameMap -> CspSign
CspSign
    { chans :: ChanNameMap
chans = ChanNameMap
forall a b. MapSet a b
MapSet.empty
    , procSet :: ProcNameMap
procSet = ProcNameMap
forall a b. MapSet a b
MapSet.empty }

-- | Compute union of two CSP CASL signatures.
unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
unionCspCASLSign s1 :: CspCASLSign
s1 s2 :: CspCASLSign
s2 = do
  -- Compute the unioned data signature ignoring the csp signatures
  let newDataSig :: CspCASLSign
newDataSig = (CspSign -> CspSign -> CspSign)
-> CspCASLSign -> CspCASLSign -> CspCASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig (\ _ _ -> CspSign
emptyCspSign) CspCASLSign
s1 CspCASLSign
s2
  -- Check that the new data signature has local top elements
      rel :: Rel PROCESS_NAME
rel = CspCASLSign -> Rel PROCESS_NAME
forall f e. Sign f e -> Rel PROCESS_NAME
sortRel CspCASLSign
newDataSig
      diags' :: [Diagnosis]
diags' = Rel PROCESS_NAME -> [Diagnosis]
LocalTop.checkLocalTops Rel PROCESS_NAME
rel
  -- Compute the unioned csp signature with respect to the new data signature
      newCspSign :: CspSign
newCspSign = Rel PROCESS_NAME -> CspSign -> CspSign -> CspSign
unionCspSign Rel PROCESS_NAME
rel (CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
s1) (CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
s2)
  {- Only error will be added if there are any probelms. If there are no
  problems no errors will be added and hets will continue as normal. -}
  [Diagnosis] -> Result ()
appendDiags [Diagnosis]
diags'
  -- put both the new data signature and the csp signature back together
  CspCASLSign -> Result CspCASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CspCASLSign -> Result CspCASLSign)
-> CspCASLSign -> Result CspCASLSign
forall a b. (a -> b) -> a -> b
$ CspCASLSign
newDataSig {extendedInfo :: CspSign
extendedInfo = CspSign
newCspSign}

{- | Compute union of two CSP signatures assuming the new already computed data
signature. -}
unionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
unionCspSign :: Rel PROCESS_NAME -> CspSign -> CspSign -> CspSign
unionCspSign sr :: Rel PROCESS_NAME
sr a :: CspSign
a b :: CspSign
b = Rel PROCESS_NAME -> CspSign -> CspSign
reduceProcNamesInSig Rel PROCESS_NAME
sr (CspSign -> CspSign) -> CspSign -> CspSign
forall a b. (a -> b) -> a -> b
$ CspSign -> CspSign -> CspSign
cspSignUnion CspSign
a CspSign
b

-- | Compute difference of two CSP process signatures.
diffCspSig :: CspSign -> CspSign -> CspSign
diffCspSig :: CspSign -> CspSign -> CspSign
diffCspSig a :: CspSign
a b :: CspSign
b = CspSign
emptyCspSign
  { chans :: ChanNameMap
chans = ChanNameMap -> ChanNameMap -> ChanNameMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference (CspSign -> ChanNameMap
chans CspSign
a) (ChanNameMap -> ChanNameMap) -> ChanNameMap -> ChanNameMap
forall a b. (a -> b) -> a -> b
$ CspSign -> ChanNameMap
chans CspSign
b
  , procSet :: ProcNameMap
procSet = ProcNameMap -> ProcNameMap -> ProcNameMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference (CspSign -> ProcNameMap
procSet CspSign
a) (ProcNameMap -> ProcNameMap) -> ProcNameMap -> ProcNameMap
forall a b. (a -> b) -> a -> b
$ CspSign -> ProcNameMap
procSet CspSign
b
  }

-- | Is one CspCASL Signature a sub signature of another
isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
isCspCASLSubSig =
  -- Normal casl subsignature and our extended csp part
  (CspSign -> CspSign -> Bool) -> CspCASLSign -> CspCASLSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig CspSign -> CspSign -> Bool
isCspSubSign
  {- Also the sorts and sub-sort rels should be equal. If they are not then we
  cannot just add the processes in as their profiles need to be donward closed
  under the new sort-rels, but we do not check this here. -}

{- | Is one Csp Signature a sub signature of another assuming the same data
signature for now. -}
isCspSubSign :: CspSign -> CspSign -> Bool
isCspSubSign :: CspSign -> CspSign -> Bool
isCspSubSign a :: CspSign
a b :: CspSign
b =
     ChanNameMap -> ChanNameMap -> Bool
forall a b. (Ord a, Ord b) => MapSet a b -> MapSet a b -> Bool
MapSet.isSubmapOf (CspSign -> ChanNameMap
chans CspSign
a) (CspSign -> ChanNameMap
chans CspSign
b) Bool -> Bool -> Bool
&&
    -- Check for each profile that the set of names are included.
    ProcNameMap -> ProcNameMap -> Bool
forall a b. (Ord a, Ord b) => MapSet a b -> MapSet a b -> Bool
MapSet.isSubmapOf (CspSign -> ProcNameMap
procSet CspSign
a) (CspSign -> ProcNameMap
procSet CspSign
b)

-- | Pretty printing for CspCASL signatures
instance Pretty CspSign where
  pretty :: CspSign -> Doc
pretty = CspSign -> Doc
printCspSign

printCspSign :: CspSign -> Doc
printCspSign :: CspSign -> Doc
printCspSign sigma :: CspSign
sigma =
    case ChanNameMap -> [(PROCESS_NAME, PROCESS_NAME)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (ChanNameMap -> [(PROCESS_NAME, PROCESS_NAME)])
-> ChanNameMap -> [(PROCESS_NAME, PROCESS_NAME)]
forall a b. (a -> b) -> a -> b
$ CspSign -> ChanNameMap
chans CspSign
sigma of
      [] -> Doc
empty
      s :: [(PROCESS_NAME, PROCESS_NAME)]
s -> String -> Doc
keyword (String
channelS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(PROCESS_NAME, PROCESS_NAME)] -> String
forall a. [a] -> String
appendS [(PROCESS_NAME, PROCESS_NAME)]
s) Doc -> Doc -> Doc
<+> [(PROCESS_NAME, PROCESS_NAME)] -> Doc
printChanList [(PROCESS_NAME, PROCESS_NAME)]
s
    Doc -> Doc -> Doc
$+$ case ProcNameMap -> [(PROCESS_NAME, ProcProfile)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (ProcNameMap -> [(PROCESS_NAME, ProcProfile)])
-> ProcNameMap -> [(PROCESS_NAME, ProcProfile)]
forall a b. (a -> b) -> a -> b
$ CspSign -> ProcNameMap
procSet CspSign
sigma of
      [] -> Doc
empty
      ps :: [(PROCESS_NAME, ProcProfile)]
ps -> String -> Doc
keyword String
processS Doc -> Doc -> Doc
<+> [(PROCESS_NAME, ProcProfile)] -> Doc
printProcList [(PROCESS_NAME, ProcProfile)]
ps

-- | Pretty printing for channels
printChanList :: [(CHANNEL_NAME, SORT)] -> Doc
printChanList :: [(PROCESS_NAME, PROCESS_NAME)] -> Doc
printChanList l :: [(PROCESS_NAME, PROCESS_NAME)]
l = let
  gl :: [[(PROCESS_NAME, PROCESS_NAME)]]
gl = ((PROCESS_NAME, PROCESS_NAME)
 -> (PROCESS_NAME, PROCESS_NAME) -> Bool)
-> [(PROCESS_NAME, PROCESS_NAME)]
-> [[(PROCESS_NAME, PROCESS_NAME)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (_, s1 :: PROCESS_NAME
s1) (_, s2 :: PROCESS_NAME
s2) -> PROCESS_NAME
s1 PROCESS_NAME -> PROCESS_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PROCESS_NAME
s2) ([(PROCESS_NAME, PROCESS_NAME)]
 -> [[(PROCESS_NAME, PROCESS_NAME)]])
-> [(PROCESS_NAME, PROCESS_NAME)]
-> [[(PROCESS_NAME, PROCESS_NAME)]]
forall a b. (a -> b) -> a -> b
$ ((PROCESS_NAME, PROCESS_NAME)
 -> (PROCESS_NAME, PROCESS_NAME) -> Ordering)
-> [(PROCESS_NAME, PROCESS_NAME)] -> [(PROCESS_NAME, PROCESS_NAME)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((PROCESS_NAME, PROCESS_NAME) -> PROCESS_NAME)
-> (PROCESS_NAME, PROCESS_NAME)
-> (PROCESS_NAME, PROCESS_NAME)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (PROCESS_NAME, PROCESS_NAME) -> PROCESS_NAME
forall a b. (a, b) -> b
snd) [(PROCESS_NAME, PROCESS_NAME)]
l
  printChan :: [(a, a)] -> Doc
printChan cl :: [(a, a)]
cl = case [(a, a)]
cl of
    [] -> Doc
empty -- should not happen
    (_, s :: a
s) : _ -> [Doc] -> Doc
fsep [[a] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas (((a, a) -> a) -> [(a, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> a
forall a b. (a, b) -> a
fst [(a, a)]
cl), Doc
colon Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
s]
  in [Doc] -> Doc
sepBySemis ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([(PROCESS_NAME, PROCESS_NAME)] -> Doc)
-> [[(PROCESS_NAME, PROCESS_NAME)]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [(PROCESS_NAME, PROCESS_NAME)] -> Doc
forall a a. (Pretty a, Pretty a) => [(a, a)] -> Doc
printChan [[(PROCESS_NAME, PROCESS_NAME)]]
gl

-- | Pretty printing for processes
printProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
printProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
printProcList = [Doc] -> Doc
sepBySemis ([Doc] -> Doc)
-> ([(PROCESS_NAME, ProcProfile)] -> [Doc])
-> [(PROCESS_NAME, ProcProfile)]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((PROCESS_NAME, ProcProfile) -> Doc)
-> [(PROCESS_NAME, ProcProfile)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map
  (\ (procName :: PROCESS_NAME
procName, procProfile :: ProcProfile
procProfile) -> PROCESS_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS_NAME
procName Doc -> Doc -> Doc
<+> ProcProfile -> Doc
forall a. Pretty a => a -> Doc
pretty ProcProfile
procProfile)

-- * overload relations: We do not have one of these yet in theory

relatedSorts :: CspCASLSign -> SORT -> SORT -> Bool
relatedSorts :: CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
relatedSorts sig :: CspCASLSign
sig s1 :: PROCESS_NAME
s1 s2 :: PROCESS_NAME
s2 = Bool -> CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
forall f e.
Bool -> Sign f e -> PROCESS_NAME -> PROCESS_NAME -> Bool
haveCommonSupersorts Bool
True CspCASLSign
sig PROCESS_NAME
s1 PROCESS_NAME
s2
  Bool -> Bool -> Bool
|| Bool -> CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
forall f e.
Bool -> Sign f e -> PROCESS_NAME -> PROCESS_NAME -> Bool
haveCommonSupersorts Bool
False CspCASLSign
sig PROCESS_NAME
s1 PROCESS_NAME
s2

relatedCommTypes :: CspCASLSign -> CommType -> CommType -> Bool
relatedCommTypes :: CspCASLSign -> CommType -> CommType -> Bool
relatedCommTypes sig :: CspCASLSign
sig ct1 :: CommType
ct1 ct2 :: CommType
ct2 = case (CommType
ct1, CommType
ct2) of
  (CommTypeSort s1 :: PROCESS_NAME
s1, CommTypeSort s2 :: PROCESS_NAME
s2) -> CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
relatedSorts CspCASLSign
sig PROCESS_NAME
s1 PROCESS_NAME
s2
  (CommTypeChan (TypedChanName c1 :: PROCESS_NAME
c1 s1 :: PROCESS_NAME
s1), CommTypeChan (TypedChanName c2 :: PROCESS_NAME
c2 s2 :: PROCESS_NAME
s2))
    -> PROCESS_NAME
c1 PROCESS_NAME -> PROCESS_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PROCESS_NAME
c2 Bool -> Bool -> Bool
&& CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
relatedSorts CspCASLSign
sig PROCESS_NAME
s1 PROCESS_NAME
s2
  _ -> Bool
False

relatedCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha -> Bool
relatedCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha -> Bool
relatedCommAlpha sig :: CspCASLSign
sig al1 :: CommAlpha
al1 al2 :: CommAlpha
al2 = CommAlpha -> Bool
forall a. Set a -> Bool
Set.null CommAlpha
al1 Bool -> Bool -> Bool
|| CommAlpha -> Bool
forall a. Set a -> Bool
Set.null CommAlpha
al2 Bool -> Bool -> Bool
||
  (CommType -> Bool) -> [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a :: CommType
a -> (CommType -> Bool) -> [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CspCASLSign -> CommType -> CommType -> Bool
relatedCommTypes CspCASLSign
sig CommType
a) ([CommType] -> Bool) -> [CommType] -> Bool
forall a b. (a -> b) -> a -> b
$ CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList CommAlpha
al1) (CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList CommAlpha
al2)

relatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool
relatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool
relatedProcs sig :: CspCASLSign
sig (ProcProfile l1 :: PROC_ARGS
l1 al1 :: CommAlpha
al1) (ProcProfile l2 :: PROC_ARGS
l2 al2 :: CommAlpha
al2) =
  PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
l2 Bool -> Bool -> Bool
&&
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((PROCESS_NAME -> PROCESS_NAME -> Bool)
-> PROC_ARGS -> PROC_ARGS -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (CspCASLSign -> PROCESS_NAME -> PROCESS_NAME -> Bool
relatedSorts CspCASLSign
sig) PROC_ARGS
l1 PROC_ARGS
l2)
    Bool -> Bool -> Bool
&& CspCASLSign -> CommAlpha -> CommAlpha -> Bool
relatedCommAlpha CspCASLSign
sig CommAlpha
al1 CommAlpha
al2

-- * Sentences

{- | FQProcVarList should only contain fully qualified CASL variables which are
TERMs i.e. constructed via the TERM constructor Qual_var. -}
type FQProcVarList = [TERM ()]

{- | A CspCASl senetence is either a CASL formula or a Procsses equation. A
process equation has on the LHS a process name, a list of parameters which
are qualified variables (which are terms), a constituent( or is it permitted
?) communication alphabet and finally on the RHS a fully qualified process. -}
data CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
      deriving (Int -> CspSen -> String -> String
[CspSen] -> String -> String
CspSen -> String
(Int -> CspSen -> String -> String)
-> (CspSen -> String)
-> ([CspSen] -> String -> String)
-> Show CspSen
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CspSen] -> String -> String
$cshowList :: [CspSen] -> String -> String
show :: CspSen -> String
$cshow :: CspSen -> String
showsPrec :: Int -> CspSen -> String -> String
$cshowsPrec :: Int -> CspSen -> String -> String
Show, CspSen -> CspSen -> Bool
(CspSen -> CspSen -> Bool)
-> (CspSen -> CspSen -> Bool) -> Eq CspSen
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspSen -> CspSen -> Bool
$c/= :: CspSen -> CspSen -> Bool
== :: CspSen -> CspSen -> Bool
$c== :: CspSen -> CspSen -> Bool
Eq, Eq CspSen
Eq CspSen =>
(CspSen -> CspSen -> Ordering)
-> (CspSen -> CspSen -> Bool)
-> (CspSen -> CspSen -> Bool)
-> (CspSen -> CspSen -> Bool)
-> (CspSen -> CspSen -> Bool)
-> (CspSen -> CspSen -> CspSen)
-> (CspSen -> CspSen -> CspSen)
-> Ord CspSen
CspSen -> CspSen -> Bool
CspSen -> CspSen -> Ordering
CspSen -> CspSen -> CspSen
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CspSen -> CspSen -> CspSen
$cmin :: CspSen -> CspSen -> CspSen
max :: CspSen -> CspSen -> CspSen
$cmax :: CspSen -> CspSen -> CspSen
>= :: CspSen -> CspSen -> Bool
$c>= :: CspSen -> CspSen -> Bool
> :: CspSen -> CspSen -> Bool
$c> :: CspSen -> CspSen -> Bool
<= :: CspSen -> CspSen -> Bool
$c<= :: CspSen -> CspSen -> Bool
< :: CspSen -> CspSen -> Bool
$c< :: CspSen -> CspSen -> Bool
compare :: CspSen -> CspSen -> Ordering
$ccompare :: CspSen -> CspSen -> Ordering
$cp1Ord :: Eq CspSen
Ord, Typeable, Typeable CspSen
Constr
DataType
Typeable CspSen =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspSen -> c CspSen)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspSen)
-> (CspSen -> Constr)
-> (CspSen -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspSen))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen))
-> ((forall b. Data b => b -> b) -> CspSen -> CspSen)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSen -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSen -> r)
-> (forall u. (forall d. Data d => d -> u) -> CspSen -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CspSen -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CspSen -> m CspSen)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSen -> m CspSen)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSen -> m CspSen)
-> Data CspSen
CspSen -> Constr
CspSen -> DataType
(forall b. Data b => b -> b) -> CspSen -> CspSen
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSen -> c CspSen
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSen
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CspSen -> u
forall u. (forall d. Data d => d -> u) -> CspSen -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSen -> m CspSen
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSen -> m CspSen
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSen
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSen -> c CspSen
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSen)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen)
$cProcessEq :: Constr
$tCspSen :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CspSen -> m CspSen
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSen -> m CspSen
gmapMp :: (forall d. Data d => d -> m d) -> CspSen -> m CspSen
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSen -> m CspSen
gmapM :: (forall d. Data d => d -> m d) -> CspSen -> m CspSen
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSen -> m CspSen
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSen -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CspSen -> u
gmapQ :: (forall d. Data d => d -> u) -> CspSen -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspSen -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r
gmapT :: (forall b. Data b => b -> b) -> CspSen -> CspSen
$cgmapT :: (forall b. Data b => b -> b) -> CspSen -> CspSen
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspSen)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSen)
dataTypeOf :: CspSen -> DataType
$cdataTypeOf :: CspSen -> DataType
toConstr :: CspSen -> Constr
$ctoConstr :: CspSen -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSen
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSen
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSen -> c CspSen
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSen -> c CspSen
$cp1Data :: Typeable CspSen
Data)

type CspCASLSen = FORMULA CspSen

instance GetRange CspSen

instance Pretty CspSen where
    pretty :: CspSen -> Doc
pretty (ProcessEq pn :: FQ_PROCESS_NAME
pn varList :: FQProcVarList
varList _commAlpha :: CommAlpha
_commAlpha proc :: PROCESS
proc) =
        let varDoc :: Doc
varDoc = if FQProcVarList -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FQProcVarList
varList
                     then Doc
empty
                     else Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FQProcVarList -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas FQProcVarList
varList
        in [Doc] -> Doc
fsep [FQ_PROCESS_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty FQ_PROCESS_NAME
pn, Doc
varDoc, Doc
equals Doc -> Doc -> Doc
<+> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
proc]

instance FormExtension CspSen where
  prefixExt :: CspSen -> Doc -> Doc
prefixExt (ProcessEq pn :: FQ_PROCESS_NAME
pn _ _ _) = case FQ_PROCESS_NAME
pn of
    PROCESS_NAME _ -> (String -> Doc
keyword String
processS Doc -> Doc -> Doc
<+>)
    FQ_PROCESS_NAME {} -> Doc -> Doc
forall a. a -> a
id

instance TermExtension CspSen
instance TermParser CspSen

isProcessEq :: CspCASLSen -> Bool
isProcessEq :: FORMULA CspSen -> Bool
isProcessEq f :: FORMULA CspSen
f = case FORMULA CspSen
f of
   ExtFORMULA _ -> Bool
True
   _ -> Bool
False