{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CspCASL/AS_CspCASL_Process.der.hs
Description :  Abstract syntax of CSP-CASL processes
Copyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  a.m.gimblett@swan.ac.uk
Stability   :  provisional
Portability :  portable

Abstract syntax of CSP-CASL processes.

-}

module CspCASL.AS_CspCASL_Process
  ( CHANNEL_NAME
  , CommAlpha
  , CommType (..)
  , EVENT (..)
  , EVENT_SET (..)
  , FQ_PROCESS_NAME (..)
  , PROCESS (..)
  , PROCESS_NAME
  , PROC_ARGS
  , PROC_ALPHABET (..)
  , procNameToSimpProcName
  , ProcProfile (..)
  , RenameKind (..)
  , Rename (..)
  , RENAMING (..)
  , splitCASLVar
  , TypedChanName (..)
  ) where

import CASL.AS_Basic_CASL (FORMULA, SORT, TERM (..), VAR)

import Common.Id

import Data.Data
import qualified Data.Set as Set

-- DrIFT command
{-! global: GetRange !-}

data EVENT
    -- | @t -> p@ - Term prefix
    = TermEvent (TERM ()) Range
    -- | @[] var :: s -> p@ - External nondeterministic prefix choice
    | ExternalPrefixChoice VAR SORT Range
    -- | @|~| var :: s -> p@ - Internal nondeterministic prefix choice
    | InternalPrefixChoice VAR SORT Range
    -- | @c ! t -> p@ - Channel send
    | ChanSend CHANNEL_NAME (TERM ()) Range
    -- | @c ! var :: s -> p@ - Channel nondeterministic send
    | ChanNonDetSend CHANNEL_NAME VAR SORT Range
    -- | @c ? var :: s -> p@ - Channel recieve
    | ChanRecv CHANNEL_NAME VAR SORT Range
    -- | @t -> p@ - Fully Qualified Term prefix
    | FQTermEvent (TERM ()) Range
    {- | @[] var :: s -> p@ - Fully Qualified External nondeterministic prefix
    choice. The term here holds the fully qualified variable (name and sort). -}
    | FQExternalPrefixChoice (TERM ()) Range
    {- | @|~| var :: s -> p@ - Fully Qualified Internal nondeterministic prefix
    choice. The term here holds the fully qualified variable (name and sort). -}
    | FQInternalPrefixChoice (TERM ()) Range
    {- | @c ! t -> p@ - Fully Qualified Channel send. The term holds the fully
    term to send. -}
    | FQChanSend (CHANNEL_NAME, SORT) (TERM ()) Range
    {- | @c ! var :: s -> p@ - Fully Qualified Channel nondeterministic
    send. The term here holds the fully qualified variable (name and sort). -}
    | FQChanNonDetSend (CHANNEL_NAME, SORT) (TERM ()) Range
    {- | @c ? var :: s -> p@ - Fully Qualified Channel recieve. The term here
    holds the fully qualified variable (name and sort). -}
    | FQChanRecv (CHANNEL_NAME, SORT) (TERM ()) Range
    deriving (Int -> EVENT -> ShowS
[EVENT] -> ShowS
EVENT -> String
(Int -> EVENT -> ShowS)
-> (EVENT -> String) -> ([EVENT] -> ShowS) -> Show EVENT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EVENT] -> ShowS
$cshowList :: [EVENT] -> ShowS
show :: EVENT -> String
$cshow :: EVENT -> String
showsPrec :: Int -> EVENT -> ShowS
$cshowsPrec :: Int -> EVENT -> ShowS
Show, EVENT -> EVENT -> Bool
(EVENT -> EVENT -> Bool) -> (EVENT -> EVENT -> Bool) -> Eq EVENT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EVENT -> EVENT -> Bool
$c/= :: EVENT -> EVENT -> Bool
== :: EVENT -> EVENT -> Bool
$c== :: EVENT -> EVENT -> Bool
Eq, Eq EVENT
Eq EVENT =>
(EVENT -> EVENT -> Ordering)
-> (EVENT -> EVENT -> Bool)
-> (EVENT -> EVENT -> Bool)
-> (EVENT -> EVENT -> Bool)
-> (EVENT -> EVENT -> Bool)
-> (EVENT -> EVENT -> EVENT)
-> (EVENT -> EVENT -> EVENT)
-> Ord EVENT
EVENT -> EVENT -> Bool
EVENT -> EVENT -> Ordering
EVENT -> EVENT -> EVENT
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 :: EVENT -> EVENT -> EVENT
$cmin :: EVENT -> EVENT -> EVENT
max :: EVENT -> EVENT -> EVENT
$cmax :: EVENT -> EVENT -> EVENT
>= :: EVENT -> EVENT -> Bool
$c>= :: EVENT -> EVENT -> Bool
> :: EVENT -> EVENT -> Bool
$c> :: EVENT -> EVENT -> Bool
<= :: EVENT -> EVENT -> Bool
$c<= :: EVENT -> EVENT -> Bool
< :: EVENT -> EVENT -> Bool
$c< :: EVENT -> EVENT -> Bool
compare :: EVENT -> EVENT -> Ordering
$ccompare :: EVENT -> EVENT -> Ordering
$cp1Ord :: Eq EVENT
Ord, Typeable, Typeable EVENT
Constr
DataType
Typeable EVENT =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EVENT -> c EVENT)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EVENT)
-> (EVENT -> Constr)
-> (EVENT -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EVENT))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT))
-> ((forall b. Data b => b -> b) -> EVENT -> EVENT)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r)
-> (forall u. (forall d. Data d => d -> u) -> EVENT -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> EVENT -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EVENT -> m EVENT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EVENT -> m EVENT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EVENT -> m EVENT)
-> Data EVENT
EVENT -> Constr
EVENT -> DataType
(forall b. Data b => b -> b) -> EVENT -> EVENT
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT -> c EVENT
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT
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) -> EVENT -> u
forall u. (forall d. Data d => d -> u) -> EVENT -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EVENT -> m EVENT
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT -> m EVENT
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT -> c EVENT
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EVENT)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT)
$cFQChanRecv :: Constr
$cFQChanNonDetSend :: Constr
$cFQChanSend :: Constr
$cFQInternalPrefixChoice :: Constr
$cFQExternalPrefixChoice :: Constr
$cFQTermEvent :: Constr
$cChanRecv :: Constr
$cChanNonDetSend :: Constr
$cChanSend :: Constr
$cInternalPrefixChoice :: Constr
$cExternalPrefixChoice :: Constr
$cTermEvent :: Constr
$tEVENT :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EVENT -> m EVENT
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT -> m EVENT
gmapMp :: (forall d. Data d => d -> m d) -> EVENT -> m EVENT
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT -> m EVENT
gmapM :: (forall d. Data d => d -> m d) -> EVENT -> m EVENT
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EVENT -> m EVENT
gmapQi :: Int -> (forall d. Data d => d -> u) -> EVENT -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EVENT -> u
gmapQ :: (forall d. Data d => d -> u) -> EVENT -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EVENT -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EVENT -> r
gmapT :: (forall b. Data b => b -> b) -> EVENT -> EVENT
$cgmapT :: (forall b. Data b => b -> b) -> EVENT -> EVENT
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EVENT)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EVENT)
dataTypeOf :: EVENT -> DataType
$cdataTypeOf :: EVENT -> DataType
toConstr :: EVENT -> Constr
$ctoConstr :: EVENT -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT -> c EVENT
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT -> c EVENT
$cp1Data :: Typeable EVENT
Data)

-- | Event sets are sets of communication types.
data EVENT_SET = EventSet [CommType] Range
                 deriving (Int -> EVENT_SET -> ShowS
[EVENT_SET] -> ShowS
EVENT_SET -> String
(Int -> EVENT_SET -> ShowS)
-> (EVENT_SET -> String)
-> ([EVENT_SET] -> ShowS)
-> Show EVENT_SET
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EVENT_SET] -> ShowS
$cshowList :: [EVENT_SET] -> ShowS
show :: EVENT_SET -> String
$cshow :: EVENT_SET -> String
showsPrec :: Int -> EVENT_SET -> ShowS
$cshowsPrec :: Int -> EVENT_SET -> ShowS
Show, EVENT_SET -> EVENT_SET -> Bool
(EVENT_SET -> EVENT_SET -> Bool)
-> (EVENT_SET -> EVENT_SET -> Bool) -> Eq EVENT_SET
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EVENT_SET -> EVENT_SET -> Bool
$c/= :: EVENT_SET -> EVENT_SET -> Bool
== :: EVENT_SET -> EVENT_SET -> Bool
$c== :: EVENT_SET -> EVENT_SET -> Bool
Eq, Eq EVENT_SET
Eq EVENT_SET =>
(EVENT_SET -> EVENT_SET -> Ordering)
-> (EVENT_SET -> EVENT_SET -> Bool)
-> (EVENT_SET -> EVENT_SET -> Bool)
-> (EVENT_SET -> EVENT_SET -> Bool)
-> (EVENT_SET -> EVENT_SET -> Bool)
-> (EVENT_SET -> EVENT_SET -> EVENT_SET)
-> (EVENT_SET -> EVENT_SET -> EVENT_SET)
-> Ord EVENT_SET
EVENT_SET -> EVENT_SET -> Bool
EVENT_SET -> EVENT_SET -> Ordering
EVENT_SET -> EVENT_SET -> EVENT_SET
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 :: EVENT_SET -> EVENT_SET -> EVENT_SET
$cmin :: EVENT_SET -> EVENT_SET -> EVENT_SET
max :: EVENT_SET -> EVENT_SET -> EVENT_SET
$cmax :: EVENT_SET -> EVENT_SET -> EVENT_SET
>= :: EVENT_SET -> EVENT_SET -> Bool
$c>= :: EVENT_SET -> EVENT_SET -> Bool
> :: EVENT_SET -> EVENT_SET -> Bool
$c> :: EVENT_SET -> EVENT_SET -> Bool
<= :: EVENT_SET -> EVENT_SET -> Bool
$c<= :: EVENT_SET -> EVENT_SET -> Bool
< :: EVENT_SET -> EVENT_SET -> Bool
$c< :: EVENT_SET -> EVENT_SET -> Bool
compare :: EVENT_SET -> EVENT_SET -> Ordering
$ccompare :: EVENT_SET -> EVENT_SET -> Ordering
$cp1Ord :: Eq EVENT_SET
Ord, Typeable, Typeable EVENT_SET
Constr
DataType
Typeable EVENT_SET =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EVENT_SET -> c EVENT_SET)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EVENT_SET)
-> (EVENT_SET -> Constr)
-> (EVENT_SET -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EVENT_SET))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT_SET))
-> ((forall b. Data b => b -> b) -> EVENT_SET -> EVENT_SET)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r)
-> (forall u. (forall d. Data d => d -> u) -> EVENT_SET -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> EVENT_SET -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET)
-> Data EVENT_SET
EVENT_SET -> Constr
EVENT_SET -> DataType
(forall b. Data b => b -> b) -> EVENT_SET -> EVENT_SET
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT_SET -> c EVENT_SET
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT_SET
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) -> EVENT_SET -> u
forall u. (forall d. Data d => d -> u) -> EVENT_SET -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT_SET
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT_SET -> c EVENT_SET
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EVENT_SET)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT_SET)
$cEventSet :: Constr
$tEVENT_SET :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
gmapMp :: (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
gmapM :: (forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EVENT_SET -> m EVENT_SET
gmapQi :: Int -> (forall d. Data d => d -> u) -> EVENT_SET -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EVENT_SET -> u
gmapQ :: (forall d. Data d => d -> u) -> EVENT_SET -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EVENT_SET -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EVENT_SET -> r
gmapT :: (forall b. Data b => b -> b) -> EVENT_SET -> EVENT_SET
$cgmapT :: (forall b. Data b => b -> b) -> EVENT_SET -> EVENT_SET
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT_SET)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EVENT_SET)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EVENT_SET)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EVENT_SET)
dataTypeOf :: EVENT_SET -> DataType
$cdataTypeOf :: EVENT_SET -> DataType
toConstr :: EVENT_SET -> Constr
$ctoConstr :: EVENT_SET -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT_SET
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EVENT_SET
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT_SET -> c EVENT_SET
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EVENT_SET -> c EVENT_SET
$cp1Data :: Typeable EVENT_SET
Data)

data RenameKind = TotOp | PartOp | BinPred deriving (Int -> RenameKind -> ShowS
[RenameKind] -> ShowS
RenameKind -> String
(Int -> RenameKind -> ShowS)
-> (RenameKind -> String)
-> ([RenameKind] -> ShowS)
-> Show RenameKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RenameKind] -> ShowS
$cshowList :: [RenameKind] -> ShowS
show :: RenameKind -> String
$cshow :: RenameKind -> String
showsPrec :: Int -> RenameKind -> ShowS
$cshowsPrec :: Int -> RenameKind -> ShowS
Show, RenameKind -> RenameKind -> Bool
(RenameKind -> RenameKind -> Bool)
-> (RenameKind -> RenameKind -> Bool) -> Eq RenameKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RenameKind -> RenameKind -> Bool
$c/= :: RenameKind -> RenameKind -> Bool
== :: RenameKind -> RenameKind -> Bool
$c== :: RenameKind -> RenameKind -> Bool
Eq, Eq RenameKind
Eq RenameKind =>
(RenameKind -> RenameKind -> Ordering)
-> (RenameKind -> RenameKind -> Bool)
-> (RenameKind -> RenameKind -> Bool)
-> (RenameKind -> RenameKind -> Bool)
-> (RenameKind -> RenameKind -> Bool)
-> (RenameKind -> RenameKind -> RenameKind)
-> (RenameKind -> RenameKind -> RenameKind)
-> Ord RenameKind
RenameKind -> RenameKind -> Bool
RenameKind -> RenameKind -> Ordering
RenameKind -> RenameKind -> RenameKind
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 :: RenameKind -> RenameKind -> RenameKind
$cmin :: RenameKind -> RenameKind -> RenameKind
max :: RenameKind -> RenameKind -> RenameKind
$cmax :: RenameKind -> RenameKind -> RenameKind
>= :: RenameKind -> RenameKind -> Bool
$c>= :: RenameKind -> RenameKind -> Bool
> :: RenameKind -> RenameKind -> Bool
$c> :: RenameKind -> RenameKind -> Bool
<= :: RenameKind -> RenameKind -> Bool
$c<= :: RenameKind -> RenameKind -> Bool
< :: RenameKind -> RenameKind -> Bool
$c< :: RenameKind -> RenameKind -> Bool
compare :: RenameKind -> RenameKind -> Ordering
$ccompare :: RenameKind -> RenameKind -> Ordering
$cp1Ord :: Eq RenameKind
Ord, Typeable, Typeable RenameKind
Constr
DataType
Typeable RenameKind =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RenameKind -> c RenameKind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RenameKind)
-> (RenameKind -> Constr)
-> (RenameKind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RenameKind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RenameKind))
-> ((forall b. Data b => b -> b) -> RenameKind -> RenameKind)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RenameKind -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RenameKind -> r)
-> (forall u. (forall d. Data d => d -> u) -> RenameKind -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RenameKind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind)
-> Data RenameKind
RenameKind -> Constr
RenameKind -> DataType
(forall b. Data b => b -> b) -> RenameKind -> RenameKind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RenameKind -> c RenameKind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RenameKind
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) -> RenameKind -> u
forall u. (forall d. Data d => d -> u) -> RenameKind -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RenameKind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RenameKind -> c RenameKind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RenameKind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RenameKind)
$cBinPred :: Constr
$cPartOp :: Constr
$cTotOp :: Constr
$tRenameKind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
gmapMp :: (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
gmapM :: (forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RenameKind -> m RenameKind
gmapQi :: Int -> (forall d. Data d => d -> u) -> RenameKind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RenameKind -> u
gmapQ :: (forall d. Data d => d -> u) -> RenameKind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RenameKind -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RenameKind -> r
gmapT :: (forall b. Data b => b -> b) -> RenameKind -> RenameKind
$cgmapT :: (forall b. Data b => b -> b) -> RenameKind -> RenameKind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RenameKind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RenameKind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RenameKind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RenameKind)
dataTypeOf :: RenameKind -> DataType
$cdataTypeOf :: RenameKind -> DataType
toConstr :: RenameKind -> Constr
$ctoConstr :: RenameKind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RenameKind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RenameKind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RenameKind -> c RenameKind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RenameKind -> c RenameKind
$cp1Data :: Typeable RenameKind
Data)

data Rename = Rename Id (Maybe (RenameKind, Maybe (SORT, SORT)))
    deriving (Int -> Rename -> ShowS
[Rename] -> ShowS
Rename -> String
(Int -> Rename -> ShowS)
-> (Rename -> String) -> ([Rename] -> ShowS) -> Show Rename
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rename] -> ShowS
$cshowList :: [Rename] -> ShowS
show :: Rename -> String
$cshow :: Rename -> String
showsPrec :: Int -> Rename -> ShowS
$cshowsPrec :: Int -> Rename -> ShowS
Show, Rename -> Rename -> Bool
(Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool) -> Eq Rename
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rename -> Rename -> Bool
$c/= :: Rename -> Rename -> Bool
== :: Rename -> Rename -> Bool
$c== :: Rename -> Rename -> Bool
Eq, Eq Rename
Eq Rename =>
(Rename -> Rename -> Ordering)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Rename)
-> (Rename -> Rename -> Rename)
-> Ord Rename
Rename -> Rename -> Bool
Rename -> Rename -> Ordering
Rename -> Rename -> Rename
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 :: Rename -> Rename -> Rename
$cmin :: Rename -> Rename -> Rename
max :: Rename -> Rename -> Rename
$cmax :: Rename -> Rename -> Rename
>= :: Rename -> Rename -> Bool
$c>= :: Rename -> Rename -> Bool
> :: Rename -> Rename -> Bool
$c> :: Rename -> Rename -> Bool
<= :: Rename -> Rename -> Bool
$c<= :: Rename -> Rename -> Bool
< :: Rename -> Rename -> Bool
$c< :: Rename -> Rename -> Bool
compare :: Rename -> Rename -> Ordering
$ccompare :: Rename -> Rename -> Ordering
$cp1Ord :: Eq Rename
Ord, Typeable, Typeable Rename
Constr
DataType
Typeable Rename =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Rename -> c Rename)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Rename)
-> (Rename -> Constr)
-> (Rename -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Rename))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rename))
-> ((forall b. Data b => b -> b) -> Rename -> Rename)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Rename -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Rename -> r)
-> (forall u. (forall d. Data d => d -> u) -> Rename -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Rename -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Rename -> m Rename)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Rename -> m Rename)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Rename -> m Rename)
-> Data Rename
Rename -> Constr
Rename -> DataType
(forall b. Data b => b -> b) -> Rename -> Rename
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rename -> c Rename
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rename
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) -> Rename -> u
forall u. (forall d. Data d => d -> u) -> Rename -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rename -> m Rename
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rename -> m Rename
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rename
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rename -> c Rename
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rename)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rename)
$cRename :: Constr
$tRename :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Rename -> m Rename
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rename -> m Rename
gmapMp :: (forall d. Data d => d -> m d) -> Rename -> m Rename
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rename -> m Rename
gmapM :: (forall d. Data d => d -> m d) -> Rename -> m Rename
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rename -> m Rename
gmapQi :: Int -> (forall d. Data d => d -> u) -> Rename -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Rename -> u
gmapQ :: (forall d. Data d => d -> u) -> Rename -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Rename -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rename -> r
gmapT :: (forall b. Data b => b -> b) -> Rename -> Rename
$cgmapT :: (forall b. Data b => b -> b) -> Rename -> Rename
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rename)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rename)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Rename)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Rename)
dataTypeOf :: Rename -> DataType
$cdataTypeOf :: Rename -> DataType
toConstr :: Rename -> Constr
$ctoConstr :: Rename -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rename
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Rename
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rename -> c Rename
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rename -> c Rename
$cp1Data :: Typeable Rename
Data)

-- | CSP renamings are predicate names or op names.
data RENAMING = Renaming [Rename]
                deriving (Int -> RENAMING -> ShowS
[RENAMING] -> ShowS
RENAMING -> String
(Int -> RENAMING -> ShowS)
-> (RENAMING -> String) -> ([RENAMING] -> ShowS) -> Show RENAMING
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RENAMING] -> ShowS
$cshowList :: [RENAMING] -> ShowS
show :: RENAMING -> String
$cshow :: RENAMING -> String
showsPrec :: Int -> RENAMING -> ShowS
$cshowsPrec :: Int -> RENAMING -> ShowS
Show, RENAMING -> RENAMING -> Bool
(RENAMING -> RENAMING -> Bool)
-> (RENAMING -> RENAMING -> Bool) -> Eq RENAMING
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RENAMING -> RENAMING -> Bool
$c/= :: RENAMING -> RENAMING -> Bool
== :: RENAMING -> RENAMING -> Bool
$c== :: RENAMING -> RENAMING -> Bool
Eq, Eq RENAMING
Eq RENAMING =>
(RENAMING -> RENAMING -> Ordering)
-> (RENAMING -> RENAMING -> Bool)
-> (RENAMING -> RENAMING -> Bool)
-> (RENAMING -> RENAMING -> Bool)
-> (RENAMING -> RENAMING -> Bool)
-> (RENAMING -> RENAMING -> RENAMING)
-> (RENAMING -> RENAMING -> RENAMING)
-> Ord RENAMING
RENAMING -> RENAMING -> Bool
RENAMING -> RENAMING -> Ordering
RENAMING -> RENAMING -> RENAMING
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 :: RENAMING -> RENAMING -> RENAMING
$cmin :: RENAMING -> RENAMING -> RENAMING
max :: RENAMING -> RENAMING -> RENAMING
$cmax :: RENAMING -> RENAMING -> RENAMING
>= :: RENAMING -> RENAMING -> Bool
$c>= :: RENAMING -> RENAMING -> Bool
> :: RENAMING -> RENAMING -> Bool
$c> :: RENAMING -> RENAMING -> Bool
<= :: RENAMING -> RENAMING -> Bool
$c<= :: RENAMING -> RENAMING -> Bool
< :: RENAMING -> RENAMING -> Bool
$c< :: RENAMING -> RENAMING -> Bool
compare :: RENAMING -> RENAMING -> Ordering
$ccompare :: RENAMING -> RENAMING -> Ordering
$cp1Ord :: Eq RENAMING
Ord, Typeable, Typeable RENAMING
Constr
DataType
Typeable RENAMING =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RENAMING -> c RENAMING)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RENAMING)
-> (RENAMING -> Constr)
-> (RENAMING -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RENAMING))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RENAMING))
-> ((forall b. Data b => b -> b) -> RENAMING -> RENAMING)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RENAMING -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RENAMING -> r)
-> (forall u. (forall d. Data d => d -> u) -> RENAMING -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> RENAMING -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING)
-> Data RENAMING
RENAMING -> Constr
RENAMING -> DataType
(forall b. Data b => b -> b) -> RENAMING -> RENAMING
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RENAMING -> c RENAMING
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RENAMING
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) -> RENAMING -> u
forall u. (forall d. Data d => d -> u) -> RENAMING -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RENAMING
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RENAMING -> c RENAMING
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RENAMING)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RENAMING)
$cRenaming :: Constr
$tRENAMING :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
gmapMp :: (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
gmapM :: (forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RENAMING -> m RENAMING
gmapQi :: Int -> (forall d. Data d => d -> u) -> RENAMING -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RENAMING -> u
gmapQ :: (forall d. Data d => d -> u) -> RENAMING -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RENAMING -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RENAMING -> r
gmapT :: (forall b. Data b => b -> b) -> RENAMING -> RENAMING
$cgmapT :: (forall b. Data b => b -> b) -> RENAMING -> RENAMING
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RENAMING)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RENAMING)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RENAMING)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RENAMING)
dataTypeOf :: RENAMING -> DataType
$cdataTypeOf :: RENAMING -> DataType
toConstr :: RENAMING -> Constr
$ctoConstr :: RENAMING -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RENAMING
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RENAMING
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RENAMING -> c RENAMING
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RENAMING -> c RENAMING
$cp1Data :: Typeable RENAMING
Data)

type CHANNEL_NAME = Id

type PROCESS_NAME = Id

type PROC_ARGS = [SORT]

data PROC_ALPHABET = ProcAlphabet [CommType]
                     deriving (Int -> PROC_ALPHABET -> ShowS
[PROC_ALPHABET] -> ShowS
PROC_ALPHABET -> String
(Int -> PROC_ALPHABET -> ShowS)
-> (PROC_ALPHABET -> String)
-> ([PROC_ALPHABET] -> ShowS)
-> Show PROC_ALPHABET
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PROC_ALPHABET] -> ShowS
$cshowList :: [PROC_ALPHABET] -> ShowS
show :: PROC_ALPHABET -> String
$cshow :: PROC_ALPHABET -> String
showsPrec :: Int -> PROC_ALPHABET -> ShowS
$cshowsPrec :: Int -> PROC_ALPHABET -> ShowS
Show, PROC_ALPHABET -> PROC_ALPHABET -> Bool
(PROC_ALPHABET -> PROC_ALPHABET -> Bool)
-> (PROC_ALPHABET -> PROC_ALPHABET -> Bool) -> Eq PROC_ALPHABET
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c/= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
== :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c== :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
Eq, Eq PROC_ALPHABET
Eq PROC_ALPHABET =>
(PROC_ALPHABET -> PROC_ALPHABET -> Ordering)
-> (PROC_ALPHABET -> PROC_ALPHABET -> Bool)
-> (PROC_ALPHABET -> PROC_ALPHABET -> Bool)
-> (PROC_ALPHABET -> PROC_ALPHABET -> Bool)
-> (PROC_ALPHABET -> PROC_ALPHABET -> Bool)
-> (PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET)
-> (PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET)
-> Ord PROC_ALPHABET
PROC_ALPHABET -> PROC_ALPHABET -> Bool
PROC_ALPHABET -> PROC_ALPHABET -> Ordering
PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET
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 :: PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET
$cmin :: PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET
max :: PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET
$cmax :: PROC_ALPHABET -> PROC_ALPHABET -> PROC_ALPHABET
>= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c>= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
> :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c> :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
<= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c<= :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
< :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
$c< :: PROC_ALPHABET -> PROC_ALPHABET -> Bool
compare :: PROC_ALPHABET -> PROC_ALPHABET -> Ordering
$ccompare :: PROC_ALPHABET -> PROC_ALPHABET -> Ordering
$cp1Ord :: Eq PROC_ALPHABET
Ord, Typeable, Typeable PROC_ALPHABET
Constr
DataType
Typeable PROC_ALPHABET =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PROC_ALPHABET -> c PROC_ALPHABET)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PROC_ALPHABET)
-> (PROC_ALPHABET -> Constr)
-> (PROC_ALPHABET -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PROC_ALPHABET))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PROC_ALPHABET))
-> ((forall b. Data b => b -> b) -> PROC_ALPHABET -> PROC_ALPHABET)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r)
-> (forall u. (forall d. Data d => d -> u) -> PROC_ALPHABET -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PROC_ALPHABET -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET)
-> Data PROC_ALPHABET
PROC_ALPHABET -> Constr
PROC_ALPHABET -> DataType
(forall b. Data b => b -> b) -> PROC_ALPHABET -> PROC_ALPHABET
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROC_ALPHABET -> c PROC_ALPHABET
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROC_ALPHABET
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) -> PROC_ALPHABET -> u
forall u. (forall d. Data d => d -> u) -> PROC_ALPHABET -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROC_ALPHABET
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROC_ALPHABET -> c PROC_ALPHABET
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PROC_ALPHABET)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PROC_ALPHABET)
$cProcAlphabet :: Constr
$tPROC_ALPHABET :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
gmapMp :: (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
gmapM :: (forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PROC_ALPHABET -> m PROC_ALPHABET
gmapQi :: Int -> (forall d. Data d => d -> u) -> PROC_ALPHABET -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PROC_ALPHABET -> u
gmapQ :: (forall d. Data d => d -> u) -> PROC_ALPHABET -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PROC_ALPHABET -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROC_ALPHABET -> r
gmapT :: (forall b. Data b => b -> b) -> PROC_ALPHABET -> PROC_ALPHABET
$cgmapT :: (forall b. Data b => b -> b) -> PROC_ALPHABET -> PROC_ALPHABET
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PROC_ALPHABET)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PROC_ALPHABET)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PROC_ALPHABET)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PROC_ALPHABET)
dataTypeOf :: PROC_ALPHABET -> DataType
$cdataTypeOf :: PROC_ALPHABET -> DataType
toConstr :: PROC_ALPHABET -> Constr
$ctoConstr :: PROC_ALPHABET -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROC_ALPHABET
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROC_ALPHABET
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROC_ALPHABET -> c PROC_ALPHABET
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROC_ALPHABET -> c PROC_ALPHABET
$cp1Data :: Typeable PROC_ALPHABET
Data)

splitCASLVar :: TERM () -> (VAR, SORT)
splitCASLVar :: TERM () -> (VAR, SORT)
splitCASLVar (Qual_var v :: VAR
v s :: SORT
s _ ) = (VAR
v, SORT
s)
splitCASLVar _ =
  String -> (VAR, SORT)
forall a. HasCallStack => String -> a
error "CspCASL.AS_CspCASL_Process: Can not split non Qual_var CASL Term"

{- | Fully qualified process names have parameter sorts, and a communication
alphabet (a Set of sorts). The CommAlpha here should always contain the minimal
super sorts only. The communication over subsorts is implied -}
data ProcProfile = ProcProfile PROC_ARGS CommAlpha
                   deriving (Int -> ProcProfile -> ShowS
[ProcProfile] -> ShowS
ProcProfile -> String
(Int -> ProcProfile -> ShowS)
-> (ProcProfile -> String)
-> ([ProcProfile] -> ShowS)
-> Show ProcProfile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProcProfile] -> ShowS
$cshowList :: [ProcProfile] -> ShowS
show :: ProcProfile -> String
$cshow :: ProcProfile -> String
showsPrec :: Int -> ProcProfile -> ShowS
$cshowsPrec :: Int -> ProcProfile -> ShowS
Show, ProcProfile -> ProcProfile -> Bool
(ProcProfile -> ProcProfile -> Bool)
-> (ProcProfile -> ProcProfile -> Bool) -> Eq ProcProfile
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProcProfile -> ProcProfile -> Bool
$c/= :: ProcProfile -> ProcProfile -> Bool
== :: ProcProfile -> ProcProfile -> Bool
$c== :: ProcProfile -> ProcProfile -> Bool
Eq, Eq ProcProfile
Eq ProcProfile =>
(ProcProfile -> ProcProfile -> Ordering)
-> (ProcProfile -> ProcProfile -> Bool)
-> (ProcProfile -> ProcProfile -> Bool)
-> (ProcProfile -> ProcProfile -> Bool)
-> (ProcProfile -> ProcProfile -> Bool)
-> (ProcProfile -> ProcProfile -> ProcProfile)
-> (ProcProfile -> ProcProfile -> ProcProfile)
-> Ord ProcProfile
ProcProfile -> ProcProfile -> Bool
ProcProfile -> ProcProfile -> Ordering
ProcProfile -> ProcProfile -> ProcProfile
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 :: ProcProfile -> ProcProfile -> ProcProfile
$cmin :: ProcProfile -> ProcProfile -> ProcProfile
max :: ProcProfile -> ProcProfile -> ProcProfile
$cmax :: ProcProfile -> ProcProfile -> ProcProfile
>= :: ProcProfile -> ProcProfile -> Bool
$c>= :: ProcProfile -> ProcProfile -> Bool
> :: ProcProfile -> ProcProfile -> Bool
$c> :: ProcProfile -> ProcProfile -> Bool
<= :: ProcProfile -> ProcProfile -> Bool
$c<= :: ProcProfile -> ProcProfile -> Bool
< :: ProcProfile -> ProcProfile -> Bool
$c< :: ProcProfile -> ProcProfile -> Bool
compare :: ProcProfile -> ProcProfile -> Ordering
$ccompare :: ProcProfile -> ProcProfile -> Ordering
$cp1Ord :: Eq ProcProfile
Ord, Typeable, Typeable ProcProfile
Constr
DataType
Typeable ProcProfile =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProcProfile -> c ProcProfile)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProcProfile)
-> (ProcProfile -> Constr)
-> (ProcProfile -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProcProfile))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ProcProfile))
-> ((forall b. Data b => b -> b) -> ProcProfile -> ProcProfile)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProcProfile -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProcProfile -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProcProfile -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProcProfile -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile)
-> Data ProcProfile
ProcProfile -> Constr
ProcProfile -> DataType
(forall b. Data b => b -> b) -> ProcProfile -> ProcProfile
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcProfile -> c ProcProfile
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcProfile
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) -> ProcProfile -> u
forall u. (forall d. Data d => d -> u) -> ProcProfile -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcProfile
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcProfile -> c ProcProfile
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProcProfile)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcProfile)
$cProcProfile :: Constr
$tProcProfile :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
gmapMp :: (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
gmapM :: (forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProcProfile -> m ProcProfile
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProcProfile -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProcProfile -> u
gmapQ :: (forall d. Data d => d -> u) -> ProcProfile -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProcProfile -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcProfile -> r
gmapT :: (forall b. Data b => b -> b) -> ProcProfile -> ProcProfile
$cgmapT :: (forall b. Data b => b -> b) -> ProcProfile -> ProcProfile
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcProfile)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcProfile)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProcProfile)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProcProfile)
dataTypeOf :: ProcProfile -> DataType
$cdataTypeOf :: ProcProfile -> DataType
toConstr :: ProcProfile -> Constr
$ctoConstr :: ProcProfile -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcProfile
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcProfile
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcProfile -> c ProcProfile
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcProfile -> c ProcProfile
$cp1Data :: Typeable ProcProfile
Data)

{- | A process name is either a fully qualified process name or a plain process
name. -}
data FQ_PROCESS_NAME
  -- | A non-fully qualified process name
  = PROCESS_NAME PROCESS_NAME
  {- | A name with parameter sorts and communication ids from the parser.
  This is where the user has tried to specify a fully qualified process name -}
  | FQ_PROCESS_NAME PROCESS_NAME ProcProfile
                  deriving (Int -> FQ_PROCESS_NAME -> ShowS
[FQ_PROCESS_NAME] -> ShowS
FQ_PROCESS_NAME -> String
(Int -> FQ_PROCESS_NAME -> ShowS)
-> (FQ_PROCESS_NAME -> String)
-> ([FQ_PROCESS_NAME] -> ShowS)
-> Show FQ_PROCESS_NAME
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FQ_PROCESS_NAME] -> ShowS
$cshowList :: [FQ_PROCESS_NAME] -> ShowS
show :: FQ_PROCESS_NAME -> String
$cshow :: FQ_PROCESS_NAME -> String
showsPrec :: Int -> FQ_PROCESS_NAME -> ShowS
$cshowsPrec :: Int -> FQ_PROCESS_NAME -> ShowS
Show, FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
(FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> Eq FQ_PROCESS_NAME
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c/= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
== :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c== :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
Eq, Eq FQ_PROCESS_NAME
Eq FQ_PROCESS_NAME =>
(FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Ordering)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME)
-> (FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME)
-> Ord FQ_PROCESS_NAME
FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Ordering
FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
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 :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
$cmin :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
max :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
$cmax :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
>= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c>= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
> :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c> :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
<= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c<= :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
< :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
$c< :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Bool
compare :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Ordering
$ccompare :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME -> Ordering
$cp1Ord :: Eq FQ_PROCESS_NAME
Ord, Typeable, Typeable FQ_PROCESS_NAME
Constr
DataType
Typeable FQ_PROCESS_NAME =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FQ_PROCESS_NAME -> c FQ_PROCESS_NAME)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FQ_PROCESS_NAME)
-> (FQ_PROCESS_NAME -> Constr)
-> (FQ_PROCESS_NAME -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FQ_PROCESS_NAME))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c FQ_PROCESS_NAME))
-> ((forall b. Data b => b -> b)
    -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME)
-> Data FQ_PROCESS_NAME
FQ_PROCESS_NAME -> Constr
FQ_PROCESS_NAME -> DataType
(forall b. Data b => b -> b) -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FQ_PROCESS_NAME -> c FQ_PROCESS_NAME
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FQ_PROCESS_NAME
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) -> FQ_PROCESS_NAME -> u
forall u. (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FQ_PROCESS_NAME
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FQ_PROCESS_NAME -> c FQ_PROCESS_NAME
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FQ_PROCESS_NAME)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FQ_PROCESS_NAME)
$cFQ_PROCESS_NAME :: Constr
$cPROCESS_NAME :: Constr
$tFQ_PROCESS_NAME :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
gmapMp :: (forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
gmapM :: (forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> FQ_PROCESS_NAME -> m FQ_PROCESS_NAME
gmapQi :: Int -> (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> u
gmapQ :: (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FQ_PROCESS_NAME -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FQ_PROCESS_NAME -> r
gmapT :: (forall b. Data b => b -> b) -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
$cgmapT :: (forall b. Data b => b -> b) -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FQ_PROCESS_NAME)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FQ_PROCESS_NAME)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FQ_PROCESS_NAME)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FQ_PROCESS_NAME)
dataTypeOf :: FQ_PROCESS_NAME -> DataType
$cdataTypeOf :: FQ_PROCESS_NAME -> DataType
toConstr :: FQ_PROCESS_NAME -> Constr
$ctoConstr :: FQ_PROCESS_NAME -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FQ_PROCESS_NAME
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FQ_PROCESS_NAME
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FQ_PROCESS_NAME -> c FQ_PROCESS_NAME
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FQ_PROCESS_NAME -> c FQ_PROCESS_NAME
$cp1Data :: Typeable FQ_PROCESS_NAME
Data)

procNameToSimpProcName :: FQ_PROCESS_NAME -> PROCESS_NAME
procNameToSimpProcName :: FQ_PROCESS_NAME -> SORT
procNameToSimpProcName (PROCESS_NAME pn :: SORT
pn) = SORT
pn
procNameToSimpProcName (FQ_PROCESS_NAME pn :: SORT
pn _) = SORT
pn

{- | A process communication alphabet consists of a set of sort names
and typed channel names. -}
data TypedChanName = TypedChanName CHANNEL_NAME SORT
                     deriving (Int -> TypedChanName -> ShowS
[TypedChanName] -> ShowS
TypedChanName -> String
(Int -> TypedChanName -> ShowS)
-> (TypedChanName -> String)
-> ([TypedChanName] -> ShowS)
-> Show TypedChanName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypedChanName] -> ShowS
$cshowList :: [TypedChanName] -> ShowS
show :: TypedChanName -> String
$cshow :: TypedChanName -> String
showsPrec :: Int -> TypedChanName -> ShowS
$cshowsPrec :: Int -> TypedChanName -> ShowS
Show, TypedChanName -> TypedChanName -> Bool
(TypedChanName -> TypedChanName -> Bool)
-> (TypedChanName -> TypedChanName -> Bool) -> Eq TypedChanName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedChanName -> TypedChanName -> Bool
$c/= :: TypedChanName -> TypedChanName -> Bool
== :: TypedChanName -> TypedChanName -> Bool
$c== :: TypedChanName -> TypedChanName -> Bool
Eq, Eq TypedChanName
Eq TypedChanName =>
(TypedChanName -> TypedChanName -> Ordering)
-> (TypedChanName -> TypedChanName -> Bool)
-> (TypedChanName -> TypedChanName -> Bool)
-> (TypedChanName -> TypedChanName -> Bool)
-> (TypedChanName -> TypedChanName -> Bool)
-> (TypedChanName -> TypedChanName -> TypedChanName)
-> (TypedChanName -> TypedChanName -> TypedChanName)
-> Ord TypedChanName
TypedChanName -> TypedChanName -> Bool
TypedChanName -> TypedChanName -> Ordering
TypedChanName -> TypedChanName -> TypedChanName
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 :: TypedChanName -> TypedChanName -> TypedChanName
$cmin :: TypedChanName -> TypedChanName -> TypedChanName
max :: TypedChanName -> TypedChanName -> TypedChanName
$cmax :: TypedChanName -> TypedChanName -> TypedChanName
>= :: TypedChanName -> TypedChanName -> Bool
$c>= :: TypedChanName -> TypedChanName -> Bool
> :: TypedChanName -> TypedChanName -> Bool
$c> :: TypedChanName -> TypedChanName -> Bool
<= :: TypedChanName -> TypedChanName -> Bool
$c<= :: TypedChanName -> TypedChanName -> Bool
< :: TypedChanName -> TypedChanName -> Bool
$c< :: TypedChanName -> TypedChanName -> Bool
compare :: TypedChanName -> TypedChanName -> Ordering
$ccompare :: TypedChanName -> TypedChanName -> Ordering
$cp1Ord :: Eq TypedChanName
Ord, Typeable, Typeable TypedChanName
Constr
DataType
Typeable TypedChanName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypedChanName -> c TypedChanName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TypedChanName)
-> (TypedChanName -> Constr)
-> (TypedChanName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TypedChanName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TypedChanName))
-> ((forall b. Data b => b -> b) -> TypedChanName -> TypedChanName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypedChanName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypedChanName -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypedChanName -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TypedChanName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName)
-> Data TypedChanName
TypedChanName -> Constr
TypedChanName -> DataType
(forall b. Data b => b -> b) -> TypedChanName -> TypedChanName
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypedChanName -> c TypedChanName
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypedChanName
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) -> TypedChanName -> u
forall u. (forall d. Data d => d -> u) -> TypedChanName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypedChanName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypedChanName -> c TypedChanName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypedChanName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypedChanName)
$cTypedChanName :: Constr
$tTypedChanName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
gmapMp :: (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
gmapM :: (forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypedChanName -> m TypedChanName
gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedChanName -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypedChanName -> u
gmapQ :: (forall d. Data d => d -> u) -> TypedChanName -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TypedChanName -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypedChanName -> r
gmapT :: (forall b. Data b => b -> b) -> TypedChanName -> TypedChanName
$cgmapT :: (forall b. Data b => b -> b) -> TypedChanName -> TypedChanName
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypedChanName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TypedChanName)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TypedChanName)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypedChanName)
dataTypeOf :: TypedChanName -> DataType
$cdataTypeOf :: TypedChanName -> DataType
toConstr :: TypedChanName -> Constr
$ctoConstr :: TypedChanName -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypedChanName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypedChanName
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypedChanName -> c TypedChanName
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypedChanName -> c TypedChanName
$cp1Data :: Typeable TypedChanName
Data)

data CommType = CommTypeSort SORT
              | CommTypeChan TypedChanName
                deriving (CommType -> CommType -> Bool
(CommType -> CommType -> Bool)
-> (CommType -> CommType -> Bool) -> Eq CommType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CommType -> CommType -> Bool
$c/= :: CommType -> CommType -> Bool
== :: CommType -> CommType -> Bool
$c== :: CommType -> CommType -> Bool
Eq, Eq CommType
Eq CommType =>
(CommType -> CommType -> Ordering)
-> (CommType -> CommType -> Bool)
-> (CommType -> CommType -> Bool)
-> (CommType -> CommType -> Bool)
-> (CommType -> CommType -> Bool)
-> (CommType -> CommType -> CommType)
-> (CommType -> CommType -> CommType)
-> Ord CommType
CommType -> CommType -> Bool
CommType -> CommType -> Ordering
CommType -> CommType -> CommType
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 :: CommType -> CommType -> CommType
$cmin :: CommType -> CommType -> CommType
max :: CommType -> CommType -> CommType
$cmax :: CommType -> CommType -> CommType
>= :: CommType -> CommType -> Bool
$c>= :: CommType -> CommType -> Bool
> :: CommType -> CommType -> Bool
$c> :: CommType -> CommType -> Bool
<= :: CommType -> CommType -> Bool
$c<= :: CommType -> CommType -> Bool
< :: CommType -> CommType -> Bool
$c< :: CommType -> CommType -> Bool
compare :: CommType -> CommType -> Ordering
$ccompare :: CommType -> CommType -> Ordering
$cp1Ord :: Eq CommType
Ord, Typeable, Typeable CommType
Constr
DataType
Typeable CommType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CommType -> c CommType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CommType)
-> (CommType -> Constr)
-> (CommType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CommType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CommType))
-> ((forall b. Data b => b -> b) -> CommType -> CommType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CommType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CommType -> r)
-> (forall u. (forall d. Data d => d -> u) -> CommType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CommType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CommType -> m CommType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CommType -> m CommType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CommType -> m CommType)
-> Data CommType
CommType -> Constr
CommType -> DataType
(forall b. Data b => b -> b) -> CommType -> CommType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CommType -> c CommType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CommType
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) -> CommType -> u
forall u. (forall d. Data d => d -> u) -> CommType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CommType -> m CommType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CommType -> m CommType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CommType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CommType -> c CommType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CommType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CommType)
$cCommTypeChan :: Constr
$cCommTypeSort :: Constr
$tCommType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CommType -> m CommType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CommType -> m CommType
gmapMp :: (forall d. Data d => d -> m d) -> CommType -> m CommType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CommType -> m CommType
gmapM :: (forall d. Data d => d -> m d) -> CommType -> m CommType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CommType -> m CommType
gmapQi :: Int -> (forall d. Data d => d -> u) -> CommType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CommType -> u
gmapQ :: (forall d. Data d => d -> u) -> CommType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CommType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CommType -> r
gmapT :: (forall b. Data b => b -> b) -> CommType -> CommType
$cgmapT :: (forall b. Data b => b -> b) -> CommType -> CommType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CommType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CommType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CommType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CommType)
dataTypeOf :: CommType -> DataType
$cdataTypeOf :: CommType -> DataType
toConstr :: CommType -> Constr
$ctoConstr :: CommType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CommType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CommType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CommType -> c CommType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CommType -> c CommType
$cp1Data :: Typeable CommType
Data)

{- | Type of communication types, either a sort communication or a typed channel
communications. -}
instance Show CommType where
    show :: CommType -> String
show (CommTypeSort s :: SORT
s) = SORT -> String
forall a. Show a => a -> String
show SORT
s
    show (CommTypeChan (TypedChanName c :: SORT
c s :: SORT
s)) = (SORT, SORT) -> String
forall a. Show a => a -> String
show (SORT
c, SORT
s)

-- | Type of communication alphabet
type CommAlpha = Set.Set CommType

-- | CSP-CASL process expressions.
data PROCESS
    -- | @Skip@ - Terminate immediately
    = Skip Range
    -- | @Stop@ - Do nothing
    | Stop Range
    -- | @div@ - Divergence
    | Div Range
    -- | @Run es@ - Accept any event in es, forever
    | Run EVENT_SET Range
    -- | @Chaos es@ - Accept\/refuse any event in es, forever
    | Chaos EVENT_SET Range
    -- | @event -> p@ - Prefix process
    | PrefixProcess EVENT PROCESS Range
    -- | @p ; q@ - Sequential process
    | Sequential PROCESS PROCESS Range
    -- | @p [] q@ - External choice
    | ExternalChoice PROCESS PROCESS Range
    -- | @p |~| q@ - Internal choice
    | InternalChoice PROCESS PROCESS Range
    -- | @p ||| q@ - Interleaving
    | Interleaving PROCESS PROCESS Range
    -- | @p || q @ - Synchronous parallel
    | SynchronousParallel PROCESS PROCESS Range
    -- | @p [| a |] q@ - Generalised parallel
    | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
    -- | @p [ a || b ] q@ - Alphabetised parallel
    | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
    -- | @p \\ es@ - Hiding
    | Hiding PROCESS EVENT_SET Range
    -- | @p [[r]]@ - Renaming
    | RenamingProcess PROCESS RENAMING Range
    -- | @if f then p else q@ - Conditional
    | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
    -- | Named process
    | NamedProcess FQ_PROCESS_NAME [TERM ()] Range
    {- | Fully qualified process. The range here shall be the same as
    in the process. -}
    | FQProcess PROCESS CommAlpha Range
    deriving (Int -> PROCESS -> ShowS
[PROCESS] -> ShowS
PROCESS -> String
(Int -> PROCESS -> ShowS)
-> (PROCESS -> String) -> ([PROCESS] -> ShowS) -> Show PROCESS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PROCESS] -> ShowS
$cshowList :: [PROCESS] -> ShowS
show :: PROCESS -> String
$cshow :: PROCESS -> String
showsPrec :: Int -> PROCESS -> ShowS
$cshowsPrec :: Int -> PROCESS -> ShowS
Show, PROCESS -> PROCESS -> Bool
(PROCESS -> PROCESS -> Bool)
-> (PROCESS -> PROCESS -> Bool) -> Eq PROCESS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PROCESS -> PROCESS -> Bool
$c/= :: PROCESS -> PROCESS -> Bool
== :: PROCESS -> PROCESS -> Bool
$c== :: PROCESS -> PROCESS -> Bool
Eq, Eq PROCESS
Eq PROCESS =>
(PROCESS -> PROCESS -> Ordering)
-> (PROCESS -> PROCESS -> Bool)
-> (PROCESS -> PROCESS -> Bool)
-> (PROCESS -> PROCESS -> Bool)
-> (PROCESS -> PROCESS -> Bool)
-> (PROCESS -> PROCESS -> PROCESS)
-> (PROCESS -> PROCESS -> PROCESS)
-> Ord PROCESS
PROCESS -> PROCESS -> Bool
PROCESS -> PROCESS -> Ordering
PROCESS -> PROCESS -> PROCESS
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 :: PROCESS -> PROCESS -> PROCESS
$cmin :: PROCESS -> PROCESS -> PROCESS
max :: PROCESS -> PROCESS -> PROCESS
$cmax :: PROCESS -> PROCESS -> PROCESS
>= :: PROCESS -> PROCESS -> Bool
$c>= :: PROCESS -> PROCESS -> Bool
> :: PROCESS -> PROCESS -> Bool
$c> :: PROCESS -> PROCESS -> Bool
<= :: PROCESS -> PROCESS -> Bool
$c<= :: PROCESS -> PROCESS -> Bool
< :: PROCESS -> PROCESS -> Bool
$c< :: PROCESS -> PROCESS -> Bool
compare :: PROCESS -> PROCESS -> Ordering
$ccompare :: PROCESS -> PROCESS -> Ordering
$cp1Ord :: Eq PROCESS
Ord, Typeable, Typeable PROCESS
Constr
DataType
Typeable PROCESS =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PROCESS -> c PROCESS)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PROCESS)
-> (PROCESS -> Constr)
-> (PROCESS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PROCESS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PROCESS))
-> ((forall b. Data b => b -> b) -> PROCESS -> PROCESS)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PROCESS -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PROCESS -> r)
-> (forall u. (forall d. Data d => d -> u) -> PROCESS -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PROCESS -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS)
-> Data PROCESS
PROCESS -> Constr
PROCESS -> DataType
(forall b. Data b => b -> b) -> PROCESS -> PROCESS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROCESS -> c PROCESS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROCESS
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) -> PROCESS -> u
forall u. (forall d. Data d => d -> u) -> PROCESS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROCESS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROCESS -> c PROCESS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PROCESS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PROCESS)
$cFQProcess :: Constr
$cNamedProcess :: Constr
$cConditionalProcess :: Constr
$cRenamingProcess :: Constr
$cHiding :: Constr
$cAlphabetisedParallel :: Constr
$cGeneralisedParallel :: Constr
$cSynchronousParallel :: Constr
$cInterleaving :: Constr
$cInternalChoice :: Constr
$cExternalChoice :: Constr
$cSequential :: Constr
$cPrefixProcess :: Constr
$cChaos :: Constr
$cRun :: Constr
$cDiv :: Constr
$cStop :: Constr
$cSkip :: Constr
$tPROCESS :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
gmapMp :: (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
gmapM :: (forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PROCESS -> m PROCESS
gmapQi :: Int -> (forall d. Data d => d -> u) -> PROCESS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PROCESS -> u
gmapQ :: (forall d. Data d => d -> u) -> PROCESS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PROCESS -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PROCESS -> r
gmapT :: (forall b. Data b => b -> b) -> PROCESS -> PROCESS
$cgmapT :: (forall b. Data b => b -> b) -> PROCESS -> PROCESS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PROCESS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PROCESS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PROCESS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PROCESS)
dataTypeOf :: PROCESS -> DataType
$cdataTypeOf :: PROCESS -> DataType
toConstr :: PROCESS -> Constr
$ctoConstr :: PROCESS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROCESS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PROCESS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROCESS -> c PROCESS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PROCESS -> c PROCESS
$cp1Data :: Typeable PROCESS
Data)

-- Generated by DrIFT, look but don't touch!

instance GetRange EVENT where
  getRange :: EVENT -> Range
getRange x :: EVENT
x = case EVENT
x of
    TermEvent _ p :: Range
p -> Range
p
    ExternalPrefixChoice _ _ p :: Range
p -> Range
p
    InternalPrefixChoice _ _ p :: Range
p -> Range
p
    ChanSend _ _ p :: Range
p -> Range
p
    ChanNonDetSend _ _ _ p :: Range
p -> Range
p
    ChanRecv _ _ _ p :: Range
p -> Range
p
    FQTermEvent _ p :: Range
p -> Range
p
    FQExternalPrefixChoice _ p :: Range
p -> Range
p
    FQInternalPrefixChoice _ p :: Range
p -> Range
p
    FQChanSend _ _ p :: Range
p -> Range
p
    FQChanNonDetSend _ _ p :: Range
p -> Range
p
    FQChanRecv _ _ p :: Range
p -> Range
p
  rangeSpan :: EVENT -> [Pos]
rangeSpan x :: EVENT
x = case EVENT
x of
    TermEvent a :: TERM ()
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    ExternalPrefixChoice a :: VAR
a b :: SORT
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [VAR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VAR
a, SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
b,
                                              Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    InternalPrefixChoice a :: VAR
a b :: SORT
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [VAR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VAR
a, SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
b,
                                              Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    ChanSend a :: SORT
a b :: TERM ()
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
b,
                                  Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    ChanNonDetSend a :: SORT
a b :: VAR
b c :: SORT
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, VAR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VAR
b,
                                          SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    ChanRecv a :: SORT
a b :: VAR
b c :: SORT
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, VAR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan VAR
b,
                                    SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    FQTermEvent a :: TERM ()
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    FQExternalPrefixChoice a :: TERM ()
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    FQInternalPrefixChoice a :: TERM ()
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    FQChanSend a :: (SORT, SORT)
a b :: TERM ()
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [(SORT, SORT) -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan (SORT, SORT)
a, TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    FQChanNonDetSend a :: (SORT, SORT)
a b :: TERM ()
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [(SORT, SORT) -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan (SORT, SORT)
a, TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
b,
                                          Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    FQChanRecv a :: (SORT, SORT)
a b :: TERM ()
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [(SORT, SORT) -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan (SORT, SORT)
a, TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange EVENT_SET where
  getRange :: EVENT_SET -> Range
getRange x :: EVENT_SET
x = case EVENT_SET
x of
    EventSet _ p :: Range
p -> Range
p
  rangeSpan :: EVENT_SET -> [Pos]
rangeSpan x :: EVENT_SET
x = case EVENT_SET
x of
    EventSet a :: [CommType]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[CommType] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [CommType]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange RenameKind where
  getRange :: RenameKind -> Range
getRange = Range -> RenameKind -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: RenameKind -> [Pos]
rangeSpan x :: RenameKind
x = case RenameKind
x of
    TotOp -> []
    PartOp -> []
    BinPred -> []

instance GetRange Rename where
  getRange :: Rename -> Range
getRange = Range -> Rename -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: Rename -> [Pos]
rangeSpan x :: Rename
x = case Rename
x of
    Rename a :: SORT
a b :: Maybe (RenameKind, Maybe (SORT, SORT))
b -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, Maybe (RenameKind, Maybe (SORT, SORT)) -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Maybe (RenameKind, Maybe (SORT, SORT))
b]

instance GetRange RENAMING where
  getRange :: RENAMING -> Range
getRange = Range -> RENAMING -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: RENAMING -> [Pos]
rangeSpan x :: RENAMING
x = case RENAMING
x of
    Renaming a :: [Rename]
a -> [[Pos]] -> [Pos]
joinRanges [[Rename] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Rename]
a]

instance GetRange PROC_ALPHABET where
  getRange :: PROC_ALPHABET -> Range
getRange = Range -> PROC_ALPHABET -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: PROC_ALPHABET -> [Pos]
rangeSpan x :: PROC_ALPHABET
x = case PROC_ALPHABET
x of
    ProcAlphabet a :: [CommType]
a -> [[Pos]] -> [Pos]
joinRanges [[CommType] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [CommType]
a]

instance GetRange ProcProfile where
  getRange :: ProcProfile -> Range
getRange = Range -> ProcProfile -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ProcProfile -> [Pos]
rangeSpan x :: ProcProfile
x = case ProcProfile
x of
    ProcProfile a :: PROC_ARGS
a b :: CommAlpha
b -> [[Pos]] -> [Pos]
joinRanges [PROC_ARGS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROC_ARGS
a, CommAlpha -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan CommAlpha
b]

instance GetRange FQ_PROCESS_NAME where
  getRange :: FQ_PROCESS_NAME -> Range
getRange = Range -> FQ_PROCESS_NAME -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: FQ_PROCESS_NAME -> [Pos]
rangeSpan x :: FQ_PROCESS_NAME
x = case FQ_PROCESS_NAME
x of
    PROCESS_NAME a :: SORT
a -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a]
    FQ_PROCESS_NAME a :: SORT
a b :: ProcProfile
b -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, ProcProfile -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ProcProfile
b]

instance GetRange TypedChanName where
  getRange :: TypedChanName -> Range
getRange = Range -> TypedChanName -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: TypedChanName -> [Pos]
rangeSpan x :: TypedChanName
x = case TypedChanName
x of
    TypedChanName a :: SORT
a b :: SORT
b -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
b]

instance GetRange CommType where
  getRange :: CommType -> Range
getRange = Range -> CommType -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: CommType -> [Pos]
rangeSpan x :: CommType
x = case CommType
x of
    CommTypeSort a :: SORT
a -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a]
    CommTypeChan a :: TypedChanName
a -> [[Pos]] -> [Pos]
joinRanges [TypedChanName -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TypedChanName
a]

instance GetRange PROCESS where
  getRange :: PROCESS -> Range
getRange x :: PROCESS
x = case PROCESS
x of
    Skip p :: Range
p -> Range
p
    Stop p :: Range
p -> Range
p
    Div p :: Range
p -> Range
p
    Run _ p :: Range
p -> Range
p
    Chaos _ p :: Range
p -> Range
p
    PrefixProcess _ _ p :: Range
p -> Range
p
    Sequential _ _ p :: Range
p -> Range
p
    ExternalChoice _ _ p :: Range
p -> Range
p
    InternalChoice _ _ p :: Range
p -> Range
p
    Interleaving _ _ p :: Range
p -> Range
p
    SynchronousParallel _ _ p :: Range
p -> Range
p
    GeneralisedParallel _ _ _ p :: Range
p -> Range
p
    AlphabetisedParallel _ _ _ _ p :: Range
p -> Range
p
    Hiding _ _ p :: Range
p -> Range
p
    RenamingProcess _ _ p :: Range
p -> Range
p
    ConditionalProcess _ _ _ p :: Range
p -> Range
p
    NamedProcess _ _ p :: Range
p -> Range
p
    FQProcess _ _ p :: Range
p -> Range
p
  rangeSpan :: PROCESS -> [Pos]
rangeSpan x :: PROCESS
x = case PROCESS
x of
    Skip a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    Stop a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    Div a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    Run a :: EVENT_SET
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Chaos a :: EVENT_SET
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    PrefixProcess a :: EVENT
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [EVENT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                       Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Sequential a :: PROCESS
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                    Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    ExternalChoice a :: PROCESS
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    InternalChoice a :: PROCESS
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Interleaving a :: PROCESS
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                      Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    SynchronousParallel a :: PROCESS
a b :: PROCESS
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                             Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    GeneralisedParallel a :: PROCESS
a b :: EVENT_SET
b c :: PROCESS
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a,
                                               EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
b, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    AlphabetisedParallel a :: PROCESS
a b :: EVENT_SET
b c :: EVENT_SET
c d :: PROCESS
d e :: Range
e -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a,
                                                  EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
b, EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
c, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
d,
                                                  Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
e]
    Hiding a :: PROCESS
a b :: EVENT_SET
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, EVENT_SET -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan EVENT_SET
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    RenamingProcess a :: PROCESS
a b :: RENAMING
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, RENAMING -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RENAMING
b,
                                         Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    ConditionalProcess a :: FORMULA ()
a b :: PROCESS
b c :: PROCESS
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [FORMULA () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA ()
a, PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
b,
                                              PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    NamedProcess a :: FQ_PROCESS_NAME
a b :: [TERM ()]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FQ_PROCESS_NAME -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FQ_PROCESS_NAME
a, [TERM ()] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [TERM ()]
b,
                                      Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    FQProcess a :: PROCESS
a b :: CommAlpha
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [PROCESS -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PROCESS
a, CommAlpha -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan CommAlpha
b,
                                   Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]