{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}
{- |
Module      :  ./CspCASL/Morphism.hs
Description :  Symbols and signature morphisms for the CspCASL logic
Copyright   :  (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  provisional
Portability :  portable

Symbols and signature morphisms for the CspCASL logic
-}

module CspCASL.Morphism
    ( CspCASLMorphism
    , CspAddMorphism (..)
    , ChanMap
    , ProcessMap
    , mapProcProfile
    , cspSubsigInclusion
    , emptyCspAddMorphism
    , cspAddMorphismUnion
    , cspMorphismToCspSymbMap
    , inducedCspSign
    , mapSen
    ) where

import CspCASL.AS_CspCASL_Process
import CspCASL.SignCSP
import CspCASL.Symbol
import qualified CspCASL.LocalTop as LT

import CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..), OpKind (..))
import CASL.Sign as CASL_Sign
import CASL.Morphism as CASL_Morphism
import qualified CASL.MapSentence as CASL_MapSen

import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils (composeMap)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import Control.Monad

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

-- Morphisms

{- | This is the second component of a CspCASL signature morphism, the process
name map. We map process name with a profile into new names and
communications alphabet. We follow CASL here and instread of mapping to a new
name and a new profile, we map just to the new name and the new
communications alphabet of the profile. This is because the argument sorts of
the profile have no chocie they have to be the sorts resultsing from maping
the original sorts in the profile with the data part map. Note: the
communications alphabet of the source profile must be downward closed with
respect to the CASL signature sub-sort relation (at source) and also the
target communications alphabet must be downward closed with respect to the
CASL signature sub-sort relation (at target). -}
type ProcessMap =
  Map.Map (PROCESS_NAME, ProcProfile) PROCESS_NAME

type ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME

-- | CspAddMorphism - This is just the extended part
data CspAddMorphism = CspAddMorphism
    {- Note that when applying the CspAddMorphism to process names or channel
    names, if the name is not in the map in the morphism, then the
    application is the identity function. Thus empty maps are used to form
    the empty morphism and the identity morphism. -}
    { CspAddMorphism -> ChanMap
channelMap :: ChanMap
    , CspAddMorphism -> ProcessMap
processMap :: ProcessMap
    } deriving (Int -> CspAddMorphism -> ShowS
[CspAddMorphism] -> ShowS
CspAddMorphism -> String
(Int -> CspAddMorphism -> ShowS)
-> (CspAddMorphism -> String)
-> ([CspAddMorphism] -> ShowS)
-> Show CspAddMorphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CspAddMorphism] -> ShowS
$cshowList :: [CspAddMorphism] -> ShowS
show :: CspAddMorphism -> String
$cshow :: CspAddMorphism -> String
showsPrec :: Int -> CspAddMorphism -> ShowS
$cshowsPrec :: Int -> CspAddMorphism -> ShowS
Show, CspAddMorphism -> CspAddMorphism -> Bool
(CspAddMorphism -> CspAddMorphism -> Bool)
-> (CspAddMorphism -> CspAddMorphism -> Bool) -> Eq CspAddMorphism
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspAddMorphism -> CspAddMorphism -> Bool
$c/= :: CspAddMorphism -> CspAddMorphism -> Bool
== :: CspAddMorphism -> CspAddMorphism -> Bool
$c== :: CspAddMorphism -> CspAddMorphism -> Bool
Eq, Eq CspAddMorphism
Eq CspAddMorphism =>
(CspAddMorphism -> CspAddMorphism -> Ordering)
-> (CspAddMorphism -> CspAddMorphism -> Bool)
-> (CspAddMorphism -> CspAddMorphism -> Bool)
-> (CspAddMorphism -> CspAddMorphism -> Bool)
-> (CspAddMorphism -> CspAddMorphism -> Bool)
-> (CspAddMorphism -> CspAddMorphism -> CspAddMorphism)
-> (CspAddMorphism -> CspAddMorphism -> CspAddMorphism)
-> Ord CspAddMorphism
CspAddMorphism -> CspAddMorphism -> Bool
CspAddMorphism -> CspAddMorphism -> Ordering
CspAddMorphism -> CspAddMorphism -> CspAddMorphism
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 :: CspAddMorphism -> CspAddMorphism -> CspAddMorphism
$cmin :: CspAddMorphism -> CspAddMorphism -> CspAddMorphism
max :: CspAddMorphism -> CspAddMorphism -> CspAddMorphism
$cmax :: CspAddMorphism -> CspAddMorphism -> CspAddMorphism
>= :: CspAddMorphism -> CspAddMorphism -> Bool
$c>= :: CspAddMorphism -> CspAddMorphism -> Bool
> :: CspAddMorphism -> CspAddMorphism -> Bool
$c> :: CspAddMorphism -> CspAddMorphism -> Bool
<= :: CspAddMorphism -> CspAddMorphism -> Bool
$c<= :: CspAddMorphism -> CspAddMorphism -> Bool
< :: CspAddMorphism -> CspAddMorphism -> Bool
$c< :: CspAddMorphism -> CspAddMorphism -> Bool
compare :: CspAddMorphism -> CspAddMorphism -> Ordering
$ccompare :: CspAddMorphism -> CspAddMorphism -> Ordering
$cp1Ord :: Eq CspAddMorphism
Ord, Typeable, Typeable CspAddMorphism
Constr
DataType
Typeable CspAddMorphism =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspAddMorphism -> c CspAddMorphism)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspAddMorphism)
-> (CspAddMorphism -> Constr)
-> (CspAddMorphism -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspAddMorphism))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c CspAddMorphism))
-> ((forall b. Data b => b -> b)
    -> CspAddMorphism -> CspAddMorphism)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> CspAddMorphism -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CspAddMorphism -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> CspAddMorphism -> m CspAddMorphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CspAddMorphism -> m CspAddMorphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CspAddMorphism -> m CspAddMorphism)
-> Data CspAddMorphism
CspAddMorphism -> Constr
CspAddMorphism -> DataType
(forall b. Data b => b -> b) -> CspAddMorphism -> CspAddMorphism
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspAddMorphism -> c CspAddMorphism
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspAddMorphism
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) -> CspAddMorphism -> u
forall u. (forall d. Data d => d -> u) -> CspAddMorphism -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspAddMorphism
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspAddMorphism -> c CspAddMorphism
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspAddMorphism)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspAddMorphism)
$cCspAddMorphism :: Constr
$tCspAddMorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
gmapMp :: (forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
gmapM :: (forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> CspAddMorphism -> m CspAddMorphism
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspAddMorphism -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> CspAddMorphism -> u
gmapQ :: (forall d. Data d => d -> u) -> CspAddMorphism -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspAddMorphism -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspAddMorphism -> r
gmapT :: (forall b. Data b => b -> b) -> CspAddMorphism -> CspAddMorphism
$cgmapT :: (forall b. Data b => b -> b) -> CspAddMorphism -> CspAddMorphism
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspAddMorphism)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspAddMorphism)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspAddMorphism)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspAddMorphism)
dataTypeOf :: CspAddMorphism -> DataType
$cdataTypeOf :: CspAddMorphism -> DataType
toConstr :: CspAddMorphism -> Constr
$ctoConstr :: CspAddMorphism -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspAddMorphism
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspAddMorphism
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspAddMorphism -> c CspAddMorphism
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspAddMorphism -> c CspAddMorphism
$cp1Data :: Typeable CspAddMorphism
Data)

-- | The empty CspAddMorphism.
emptyCspAddMorphism :: CspAddMorphism
emptyCspAddMorphism :: CspAddMorphism
emptyCspAddMorphism = CspAddMorphism :: ChanMap -> ProcessMap -> CspAddMorphism
CspAddMorphism
    {- Note that when applying the CspAddMorphism to process names or
    channel names, if the name is not in the map in the morphism,
    then the application is the identity function. Thus empty maps
    are used to form the empty morphism. -}
    { channelMap :: ChanMap
channelMap = ChanMap
forall k a. Map k a
Map.empty
    , processMap :: ProcessMap
processMap = ProcessMap
forall k a. Map k a
Map.empty
    }

{- | Given two signatures (the first being a sub signature of the second
according to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}
cspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
cspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
cspSubsigInclusion sign :: CspCASLSign
sign = Result CspCASLMorphism -> Result CspCASLMorphism
checkResultMorphismIsLegal (Result CspCASLMorphism -> Result CspCASLMorphism)
-> (CspCASLSign -> Result CspCASLMorphism)
-> CspCASLSign
-> Result CspCASLMorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                          CspAddMorphism
-> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
CASL_Morphism.sigInclusion CspAddMorphism
emptyCspAddMorphism CspCASLSign
sign
{- We use the empty morphism as it also represents the identity, thus this
will embed channel names and process names properly. -}

checkResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism
checkResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism
checkResultMorphismIsLegal rmor :: Result CspCASLMorphism
rmor = do
  CspCASLMorphism
mor <- Result CspCASLMorphism
rmor
  CspCASLMorphism -> Result ()
forall e m f. MorphismExtension e m => Morphism f e m -> Result ()
legalMorphismExtension CspCASLMorphism
mor
  CspCASLMorphism -> Result CspCASLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return CspCASLMorphism
mor

-- | lookup a typed channel
mapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)
mapChan :: Sort_map
-> ChanMap
-> (CHANNEL_NAME, CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME)
mapChan sm :: Sort_map
sm cm :: ChanMap
cm p :: (CHANNEL_NAME, CHANNEL_NAME)
p@(c :: CHANNEL_NAME
c, s :: CHANNEL_NAME
s) = (CHANNEL_NAME
-> (CHANNEL_NAME, CHANNEL_NAME) -> ChanMap -> CHANNEL_NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault CHANNEL_NAME
c (CHANNEL_NAME, CHANNEL_NAME)
p ChanMap
cm, Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s)

-- | Apply a signature morphism to a channel name
mapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)
  -> (CHANNEL_NAME, SORT)
mapChannel :: Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannel mor :: Morphism f CspSign CspAddMorphism
mor = Sort_map
-> ChanMap
-> (CHANNEL_NAME, CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME)
mapChan (Morphism f CspSign CspAddMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f CspSign CspAddMorphism
mor) (ChanMap
 -> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME))
-> ChanMap
-> (CHANNEL_NAME, CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME)
forall a b. (a -> b) -> a -> b
$ CspAddMorphism -> ChanMap
channelMap (CspAddMorphism -> ChanMap) -> CspAddMorphism -> ChanMap
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism -> CspAddMorphism
forall f e m. Morphism f e m -> m
extended_map Morphism f CspSign CspAddMorphism
mor

mapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType
mapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType
mapCommTypeAux sm :: Sort_map
sm cm :: ChanMap
cm ct :: CommType
ct = case CommType
ct of
   CommTypeSort s :: CHANNEL_NAME
s -> CHANNEL_NAME -> CommType
CommTypeSort (CHANNEL_NAME -> CommType) -> CHANNEL_NAME -> CommType
forall a b. (a -> b) -> a -> b
$ Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s
   CommTypeChan (TypedChanName c :: CHANNEL_NAME
c s :: CHANNEL_NAME
s) -> let (d :: CHANNEL_NAME
d, t :: CHANNEL_NAME
t) = Sort_map
-> ChanMap
-> (CHANNEL_NAME, CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME)
mapChan Sort_map
sm ChanMap
cm (CHANNEL_NAME
c, CHANNEL_NAME
s) in
     TypedChanName -> CommType
CommTypeChan (TypedChanName -> CommType) -> TypedChanName -> CommType
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> CHANNEL_NAME -> TypedChanName
TypedChanName CHANNEL_NAME
d CHANNEL_NAME
t

-- | Apply a signature morphism to a CommType
mapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType
mapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType
mapCommType mor :: Morphism f CspSign CspAddMorphism
mor = Sort_map -> ChanMap -> CommType -> CommType
mapCommTypeAux (Morphism f CspSign CspAddMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f CspSign CspAddMorphism
mor) (CspAddMorphism -> ChanMap
channelMap (CspAddMorphism -> ChanMap) -> CspAddMorphism -> ChanMap
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism -> CspAddMorphism
forall f e m. Morphism f e m -> m
extended_map Morphism f CspSign CspAddMorphism
mor)

mapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha
mapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha
mapCommAlphaAux sm :: Sort_map
sm = (CommType -> CommType) -> CommAlpha -> CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((CommType -> CommType) -> CommAlpha -> CommAlpha)
-> (ChanMap -> CommType -> CommType)
-> ChanMap
-> CommAlpha
-> CommAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort_map -> ChanMap -> CommType -> CommType
mapCommTypeAux Sort_map
sm

-- | Apply a signature morphism  to a CommAlpha
mapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha = (CommType -> CommType) -> CommAlpha -> CommAlpha
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((CommType -> CommType) -> CommAlpha -> CommAlpha)
-> (Morphism f CspSign CspAddMorphism -> CommType -> CommType)
-> Morphism f CspSign CspAddMorphism
-> CommAlpha
-> CommAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f CspSign CspAddMorphism -> CommType -> CommType
forall f. Morphism f CspSign CspAddMorphism -> CommType -> CommType
mapCommType

mapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile sm :: Sort_map
sm cm :: ChanMap
cm (ProcProfile sl :: PROC_ARGS
sl cs :: CommAlpha
cs) =
  PROC_ARGS -> CommAlpha -> ProcProfile
ProcProfile ((CHANNEL_NAME -> CHANNEL_NAME) -> PROC_ARGS -> PROC_ARGS
forall a b. (a -> b) -> [a] -> [b]
map (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm) PROC_ARGS
sl) (CommAlpha -> ProcProfile) -> CommAlpha -> ProcProfile
forall a b. (a -> b) -> a -> b
$ Sort_map -> ChanMap -> CommAlpha -> CommAlpha
mapCommAlphaAux Sort_map
sm ChanMap
cm CommAlpha
cs

mapProcId :: Sort_map -> ChanMap -> ProcessMap
  -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
mapProcId :: Sort_map
-> ChanMap
-> ProcessMap
-> (CHANNEL_NAME, ProcProfile)
-> (CHANNEL_NAME, ProcProfile)
mapProcId sm :: Sort_map
sm cm :: ChanMap
cm pm :: ProcessMap
pm (i :: CHANNEL_NAME
i, p :: ProcProfile
p) = let
  n :: ProcProfile
n@(ProcProfile args :: PROC_ARGS
args alpha :: CommAlpha
alpha) = Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile Sort_map
sm ChanMap
cm ProcProfile
p
  in case (CHANNEL_NAME, ProcProfile) -> ProcessMap -> Maybe CHANNEL_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CHANNEL_NAME
i, ProcProfile
p) ProcessMap
pm of
       Nothing -> (CHANNEL_NAME
i, ProcProfile
n)
       Just j :: CHANNEL_NAME
j -> (CHANNEL_NAME
j, PROC_ARGS -> CommAlpha -> ProcProfile
ProcProfile PROC_ARGS
args CommAlpha
alpha)

mapProcess :: Morphism f CspSign CspAddMorphism
  -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
mapProcess :: Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
mapProcess mor :: Morphism f CspSign CspAddMorphism
mor = let em :: CspAddMorphism
em = Morphism f CspSign CspAddMorphism -> CspAddMorphism
forall f e m. Morphism f e m -> m
extended_map Morphism f CspSign CspAddMorphism
mor in
  Sort_map
-> ChanMap
-> ProcessMap
-> (CHANNEL_NAME, ProcProfile)
-> (CHANNEL_NAME, ProcProfile)
mapProcId (Morphism f CspSign CspAddMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f CspSign CspAddMorphism
mor) (CspAddMorphism -> ChanMap
channelMap CspAddMorphism
em) (ProcessMap
 -> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile))
-> ProcessMap
-> (CHANNEL_NAME, ProcProfile)
-> (CHANNEL_NAME, ProcProfile)
forall a b. (a -> b) -> a -> b
$ CspAddMorphism -> ProcessMap
processMap CspAddMorphism
em

-- | Compose two CspAddMorphisms
composeCspAddMorphism :: Morphism f CspSign CspAddMorphism
  -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
composeCspAddMorphism :: Morphism f CspSign CspAddMorphism
-> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
composeCspAddMorphism m1 :: Morphism f CspSign CspAddMorphism
m1 m2 :: Morphism f CspSign CspAddMorphism
m2 = let
    sMap1 :: Sort_map
sMap1 = Morphism f CspSign CspAddMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f CspSign CspAddMorphism
m1
    sMap2 :: Sort_map
sMap2 = Morphism f CspSign CspAddMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f CspSign CspAddMorphism
m2
    sMap :: Sort_map
sMap = Sort_map -> Sort_map -> Sort_map -> Sort_map
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Set CHANNEL_NAME -> Sort_map
forall a. Ord a => Set a -> Map a a
MapSet.setToMap (Set CHANNEL_NAME -> Sort_map) -> Set CHANNEL_NAME -> Sort_map
forall a b. (a -> b) -> a -> b
$ Sign f CspSign -> Set CHANNEL_NAME
forall f e. Sign f e -> Set CHANNEL_NAME
sortSet Sign f CspSign
src) Sort_map
sMap1 Sort_map
sMap2
    src :: Sign f CspSign
src = Morphism f CspSign CspAddMorphism -> Sign f CspSign
forall f e m. Morphism f e m -> Sign f e
msource Morphism f CspSign CspAddMorphism
m1
    cSrc :: CspSign
cSrc = Sign f CspSign -> CspSign
forall f e. Sign f e -> e
extendedInfo Sign f CspSign
src
    cMap :: ChanMap
cMap = (CHANNEL_NAME -> CHANNEL_NAME -> ChanMap -> ChanMap)
-> ChanMap -> MapSet CHANNEL_NAME CHANNEL_NAME -> ChanMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey ( \ c :: CHANNEL_NAME
c s :: CHANNEL_NAME
s ->
                       let p :: (CHANNEL_NAME, CHANNEL_NAME)
p = (CHANNEL_NAME
c, CHANNEL_NAME
s)
                           ni :: CHANNEL_NAME
ni = (CHANNEL_NAME, CHANNEL_NAME) -> CHANNEL_NAME
forall a b. (a, b) -> a
fst ((CHANNEL_NAME, CHANNEL_NAME) -> CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME) -> CHANNEL_NAME
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannel Morphism f CspSign CspAddMorphism
m2 ((CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME))
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannel Morphism f CspSign CspAddMorphism
m1 (CHANNEL_NAME, CHANNEL_NAME)
p
                       in if CHANNEL_NAME
c CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
ni then ChanMap -> ChanMap
forall a. a -> a
id else (CHANNEL_NAME, CHANNEL_NAME) -> CHANNEL_NAME -> ChanMap -> ChanMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (CHANNEL_NAME, CHANNEL_NAME)
p CHANNEL_NAME
ni)
                      ChanMap
forall k a. Map k a
Map.empty (MapSet CHANNEL_NAME CHANNEL_NAME -> ChanMap)
-> MapSet CHANNEL_NAME CHANNEL_NAME -> ChanMap
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME CHANNEL_NAME
chans CspSign
cSrc
    pMap :: ProcessMap
pMap = (CHANNEL_NAME -> ProcProfile -> ProcessMap -> ProcessMap)
-> ProcessMap -> MapSet CHANNEL_NAME ProcProfile -> ProcessMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey ( \ p :: CHANNEL_NAME
p pr :: ProcProfile
pr@(ProcProfile _ a :: CommAlpha
a) ->
                       let pp :: (CHANNEL_NAME, ProcProfile)
pp = (CHANNEL_NAME
p, ProcProfile
pr)
                           (ni :: CHANNEL_NAME
ni, ProcProfile _ na :: CommAlpha
na) =
                             Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
mapProcess Morphism f CspSign CspAddMorphism
m2 ((CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile))
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
mapProcess Morphism f CspSign CspAddMorphism
m1 (CHANNEL_NAME, ProcProfile)
pp
                           oa :: CommAlpha
oa = Sort_map -> ChanMap -> CommAlpha -> CommAlpha
mapCommAlphaAux Sort_map
sMap ChanMap
cMap CommAlpha
a
                       in if CHANNEL_NAME
p CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
ni Bool -> Bool -> Bool
&& CommAlpha
oa CommAlpha -> CommAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== CommAlpha
na then ProcessMap -> ProcessMap
forall a. a -> a
id else
                              (CHANNEL_NAME, ProcProfile)
-> CHANNEL_NAME -> ProcessMap -> ProcessMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (CHANNEL_NAME, ProcProfile)
pp CHANNEL_NAME
ni)
                      ProcessMap
forall k a. Map k a
Map.empty (MapSet CHANNEL_NAME ProcProfile -> ProcessMap)
-> MapSet CHANNEL_NAME ProcProfile -> ProcessMap
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME ProcProfile
procSet CspSign
cSrc
  in CspAddMorphism -> Result CspAddMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return CspAddMorphism
emptyCspAddMorphism
  { channelMap :: ChanMap
channelMap = ChanMap
cMap
  , processMap :: ProcessMap
processMap = ProcessMap
pMap }

{- | A CspCASLMorphism is a CASL Morphism with the extended_map to be a
CspAddMorphism. -}
type CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism

{- | Check if a CspCASL signature morphism has the refl property i.e.,
sigma(s1) <= sigma(s2) implies s1 <= s2 for all s1, s2 in S -}
checkReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkReflCondition Morphism
  { msource :: forall f e m. Morphism f e m -> Sign f e
msource = Sign f CspSign
sig
  , mtarget :: forall f e m. Morphism f e m -> Sign f e
mtarget = Sign f CspSign
sig'
  , sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm } = do
  let rel :: Rel CHANNEL_NAME
rel = Sign f CspSign -> Rel CHANNEL_NAME
forall f e. Sign f e -> Rel CHANNEL_NAME
sortRel Sign f CspSign
sig
      rel' :: Rel CHANNEL_NAME
rel' = Sign f CspSign -> Rel CHANNEL_NAME
forall f e. Sign f e -> Rel CHANNEL_NAME
sortRel Sign f CspSign
sig'
      allPairs :: Set (CHANNEL_NAME, CHANNEL_NAME)
allPairs = Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME)
forall a. Ord a => Set a -> Set (a, a)
LT.cartesian (Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME))
-> Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME)
forall a b. (a -> b) -> a -> b
$ Sign f CspSign -> Set CHANNEL_NAME
forall f e. Sign f e -> Set CHANNEL_NAME
sortSet Sign f CspSign
sig
      failures :: Set (CHANNEL_NAME, CHANNEL_NAME)
failures = ((CHANNEL_NAME, CHANNEL_NAME) -> Bool)
-> Set (CHANNEL_NAME, CHANNEL_NAME)
-> Set (CHANNEL_NAME, CHANNEL_NAME)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool)
-> ((CHANNEL_NAME, CHANNEL_NAME) -> Bool)
-> (CHANNEL_NAME, CHANNEL_NAME)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CHANNEL_NAME, CHANNEL_NAME) -> Bool
test) Set (CHANNEL_NAME, CHANNEL_NAME)
allPairs
      test :: (CHANNEL_NAME, CHANNEL_NAME) -> Bool
test (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2) = Bool -> Bool
not (CHANNEL_NAME -> CHANNEL_NAME -> Rel CHANNEL_NAME -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s1) (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s2) Rel CHANNEL_NAME
rel' Bool -> Bool -> Bool
||
                        Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s1 CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s2) Bool -> Bool -> Bool
||
                      (CHANNEL_NAME -> CHANNEL_NAME -> Rel CHANNEL_NAME -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path CHANNEL_NAME
s1 CHANNEL_NAME
s2 Rel CHANNEL_NAME
rel Bool -> Bool -> Bool
|| CHANNEL_NAME
s1 CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
s2)
      produceDiag :: (CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis
produceDiag (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2) =
                let x :: CHANNEL_NAME
x = Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s1
                    y :: CHANNEL_NAME
y = Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s2
                in DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
                 ("CSP-CASL Signature Morphism Refl Property Violated:\n'"
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (CHANNEL_NAME -> SymbType -> Symbol
Symbol CHANNEL_NAME
x (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> SymbType
SubsortAsItemType CHANNEL_NAME
y)
                         "' in target but not in source\n'"
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (CHANNEL_NAME -> SymbType -> Symbol
Symbol CHANNEL_NAME
s1 (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> SymbType
SubsortAsItemType CHANNEL_NAME
s2) "'")
                  Range
nullRange
      allDiags :: [Diagnosis]
allDiags = ((CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis)
-> [(CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis
produceDiag ([(CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis])
-> [(CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Set (CHANNEL_NAME, CHANNEL_NAME) -> [(CHANNEL_NAME, CHANNEL_NAME)]
forall a. Set a -> [a]
Set.toList Set (CHANNEL_NAME, CHANNEL_NAME)
failures
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set (CHANNEL_NAME, CHANNEL_NAME) -> Bool
forall a. Set a -> Bool
Set.null Set (CHANNEL_NAME, CHANNEL_NAME)
failures)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
allDiags Maybe ()
forall a. Maybe a
Nothing -- failure with error messages


{- | Check if a CspCASL signature morphism has the weak non extension property
i.e.,
sigma(s1) <= u' and sigma(s2) <= u' implies there exists t in S with
s1 <= t and s2 <= t and sigma(t) <= u' for all s1,s2 in S and u' in S' -}
checkWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkWNECondition Morphism
  { msource :: forall f e m. Morphism f e m -> Sign f e
msource = Sign f CspSign
sig
  , mtarget :: forall f e m. Morphism f e m -> Sign f e
mtarget = Sign f CspSign
sig'
  , sort_map :: forall f e m. Morphism f e m -> Sort_map
sort_map = Sort_map
sm } = do
  let rel' :: Rel CHANNEL_NAME
rel' = Sign f CspSign -> Rel CHANNEL_NAME
forall f e. Sign f e -> Rel CHANNEL_NAME
sortRel Sign f CspSign
sig'
      supers :: CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supers s :: CHANNEL_NAME
s signature :: Sign f e
signature = CHANNEL_NAME -> Set CHANNEL_NAME -> Set CHANNEL_NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert CHANNEL_NAME
s (Set CHANNEL_NAME -> Set CHANNEL_NAME)
-> Set CHANNEL_NAME -> Set CHANNEL_NAME
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
forall f e. CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supersortsOf CHANNEL_NAME
s Sign f e
signature
      allPairsInSource :: Set (CHANNEL_NAME, CHANNEL_NAME)
allPairsInSource = Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME)
forall a. Ord a => Set a -> Set (a, a)
LT.cartesian (Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME))
-> Set CHANNEL_NAME -> Set (CHANNEL_NAME, CHANNEL_NAME)
forall a b. (a -> b) -> a -> b
$ Sign f CspSign -> Set CHANNEL_NAME
forall f e. Sign f e -> Set CHANNEL_NAME
sortSet Sign f CspSign
sig
      commonSuperSortsInTarget :: CHANNEL_NAME -> CHANNEL_NAME -> Set CHANNEL_NAME
commonSuperSortsInTarget s1 :: CHANNEL_NAME
s1 s2 :: CHANNEL_NAME
s2 = Set CHANNEL_NAME -> Set CHANNEL_NAME -> Set CHANNEL_NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                                       (CHANNEL_NAME -> Sign f CspSign -> Set CHANNEL_NAME
forall f e. CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supers (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s1) Sign f CspSign
sig')
                                       (CHANNEL_NAME -> Sign f CspSign -> Set CHANNEL_NAME
forall f e. CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supers (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s2) Sign f CspSign
sig')
      {- Candidates are triples (s1,s2,u') such that
      \sigma(s1),\sigma(s2) < u' -}
      createCandidateTripples :: (CHANNEL_NAME, CHANNEL_NAME)
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
createCandidateTripples (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2) =
        (CHANNEL_NAME -> (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
-> Set CHANNEL_NAME
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ u' :: CHANNEL_NAME
u' -> (CHANNEL_NAME
s1, CHANNEL_NAME
s2, CHANNEL_NAME
u')) (CHANNEL_NAME -> CHANNEL_NAME -> Set CHANNEL_NAME
commonSuperSortsInTarget CHANNEL_NAME
s1 CHANNEL_NAME
s2)
      allCandidateTripples :: Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
allCandidateTripples =
        [Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
 -> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
-> [Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
forall a b. (a -> b) -> a -> b
$ Set (Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
-> [Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
forall a. Set a -> [a]
Set.toList (Set (Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
 -> [Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)])
-> Set (Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
-> [Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
forall a b. (a -> b) -> a -> b
$ ((CHANNEL_NAME, CHANNEL_NAME)
 -> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
-> Set (CHANNEL_NAME, CHANNEL_NAME)
-> Set (Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (CHANNEL_NAME, CHANNEL_NAME)
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
createCandidateTripples
        Set (CHANNEL_NAME, CHANNEL_NAME)
allPairsInSource
      testCandidate :: (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Bool
testCandidate (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2, u' :: CHANNEL_NAME
u') =
        let possibleWitnesses :: Set CHANNEL_NAME
possibleWitnesses = Set CHANNEL_NAME -> Set CHANNEL_NAME -> Set CHANNEL_NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (CHANNEL_NAME -> Sign f CspSign -> Set CHANNEL_NAME
forall f e. CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supers CHANNEL_NAME
s1 Sign f CspSign
sig) (CHANNEL_NAME -> Sign f CspSign -> Set CHANNEL_NAME
forall f e. CHANNEL_NAME -> Sign f e -> Set CHANNEL_NAME
supers CHANNEL_NAME
s2 Sign f CspSign
sig)
            test :: CHANNEL_NAME -> Bool
test t :: CHANNEL_NAME
t = CHANNEL_NAME -> CHANNEL_NAME -> Rel CHANNEL_NAME -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path (Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
t) CHANNEL_NAME
u' Rel CHANNEL_NAME
rel' Bool -> Bool -> Bool
|| Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
t CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
u'
         in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ Set Bool -> [Bool]
forall a. Set a -> [a]
Set.toList (Set Bool -> [Bool]) -> Set Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ (CHANNEL_NAME -> Bool) -> Set CHANNEL_NAME -> Set Bool
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map CHANNEL_NAME -> Bool
test Set CHANNEL_NAME
possibleWitnesses
      failures :: Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
failures = ((CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Bool)
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
-> Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool)
-> ((CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Bool)
-> (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Bool
testCandidate) Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
allCandidateTripples
      produceDiag :: (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis
produceDiag (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2, u' :: CHANNEL_NAME
u') =
                let x :: CHANNEL_NAME
x = Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s1
                    y :: CHANNEL_NAME
y = Sort_map -> CHANNEL_NAME -> CHANNEL_NAME
mapSort Sort_map
sm CHANNEL_NAME
s2
                in DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
                   ("CSP-CASL Signature Morphism Weak Non-Extension Property "
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Violated:\n'"
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT_ITEM () -> ShowS
forall a. Pretty a => a -> ShowS
showDoc
                       (PROC_ARGS -> CHANNEL_NAME -> Range -> SORT_ITEM ()
forall f. PROC_ARGS -> CHANNEL_NAME -> Range -> SORT_ITEM f
Subsort_decl [CHANNEL_NAME
x, CHANNEL_NAME
y] CHANNEL_NAME
u' Range
nullRange :: SORT_ITEM ())
                       "' in target\nbut no common supersort for the sorts\n'"
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT_ITEM () -> ShowS
forall a. Pretty a => a -> ShowS
showDoc
                       (PROC_ARGS -> Range -> SORT_ITEM ()
forall f. PROC_ARGS -> Range -> SORT_ITEM f
Sort_decl [CHANNEL_NAME
s1, CHANNEL_NAME
s2] Range
nullRange :: SORT_ITEM ())
                       "' in source")
                   Range
nullRange
      allDiags :: [Diagnosis]
allDiags = ((CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis)
-> [(CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Diagnosis
produceDiag ([(CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis])
-> [(CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
-> [(CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)]
forall a. Set a -> [a]
Set.toList Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
failures
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME) -> Bool
forall a. Set a -> Bool
Set.null Set (CHANNEL_NAME, CHANNEL_NAME, CHANNEL_NAME)
failures)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
allDiags Maybe ()
forall a. Maybe a
Nothing -- failure with error messages

-- | unite morphisms
cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism
  -> Result CspAddMorphism
cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism
cspAddMorphismUnion mor1 :: CspCASLMorphism
mor1 mor2 :: CspCASLMorphism
mor2 = let
    s1 :: CspSign
s1 = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo (CspCASLSign -> CspSign) -> CspCASLSign -> CspSign
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
msource CspCASLMorphism
mor1
    s2 :: CspSign
s2 = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo (CspCASLSign -> CspSign) -> CspCASLSign -> CspSign
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
msource CspCASLMorphism
mor2
    m1 :: CspAddMorphism
m1 = CspCASLMorphism -> CspAddMorphism
forall f e m. Morphism f e m -> m
extended_map CspCASLMorphism
mor1
    m2 :: CspAddMorphism
m2 = CspCASLMorphism -> CspAddMorphism
forall f e m. Morphism f e m -> m
extended_map CspCASLMorphism
mor2
    chan1 :: ChanMap
chan1 = CspAddMorphism -> ChanMap
channelMap CspAddMorphism
m1
    chan2 :: ChanMap
chan2 = CspAddMorphism -> ChanMap
channelMap CspAddMorphism
m2
    delChan :: (a, b) -> MapSet a b -> MapSet a b
delChan (n :: a
n, s :: b
s) = a -> b -> MapSet a b -> MapSet a b
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete a
n b
s
    uc1 :: MapSet CHANNEL_NAME CHANNEL_NAME
uc1 = ((CHANNEL_NAME, CHANNEL_NAME)
 -> MapSet CHANNEL_NAME CHANNEL_NAME
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> [(CHANNEL_NAME, CHANNEL_NAME)]
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CHANNEL_NAME, CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delChan (CspSign -> MapSet CHANNEL_NAME CHANNEL_NAME
chans CspSign
s1) ([(CHANNEL_NAME, CHANNEL_NAME)]
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> [(CHANNEL_NAME, CHANNEL_NAME)]
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (a -> b) -> a -> b
$ ChanMap -> [(CHANNEL_NAME, CHANNEL_NAME)]
forall k a. Map k a -> [k]
Map.keys ChanMap
chan1
    uc2 :: MapSet CHANNEL_NAME CHANNEL_NAME
uc2 = ((CHANNEL_NAME, CHANNEL_NAME)
 -> MapSet CHANNEL_NAME CHANNEL_NAME
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> [(CHANNEL_NAME, CHANNEL_NAME)]
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CHANNEL_NAME, CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delChan (CspSign -> MapSet CHANNEL_NAME CHANNEL_NAME
chans CspSign
s2) ([(CHANNEL_NAME, CHANNEL_NAME)]
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> [(CHANNEL_NAME, CHANNEL_NAME)]
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (a -> b) -> a -> b
$ ChanMap -> [(CHANNEL_NAME, CHANNEL_NAME)]
forall k a. Map k a -> [k]
Map.keys ChanMap
chan2
    uc :: MapSet CHANNEL_NAME CHANNEL_NAME
uc = MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union MapSet CHANNEL_NAME CHANNEL_NAME
uc1 MapSet CHANNEL_NAME CHANNEL_NAME
uc2
    proc1 :: ProcessMap
proc1 = CspAddMorphism -> ProcessMap
processMap CspAddMorphism
m1
    proc2 :: ProcessMap
proc2 = CspAddMorphism -> ProcessMap
processMap CspAddMorphism
m2
    delProc :: (a, b) -> MapSet a b -> MapSet a b
delProc (n :: a
n, p :: b
p) = a -> b -> MapSet a b -> MapSet a b
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete a
n b
p
    up1 :: MapSet CHANNEL_NAME ProcProfile
up1 = ((CHANNEL_NAME, ProcProfile)
 -> MapSet CHANNEL_NAME ProcProfile
 -> MapSet CHANNEL_NAME ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> [(CHANNEL_NAME, ProcProfile)]
-> MapSet CHANNEL_NAME ProcProfile
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CHANNEL_NAME, ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delProc (CspSign -> MapSet CHANNEL_NAME ProcProfile
procSet CspSign
s1) ([(CHANNEL_NAME, ProcProfile)] -> MapSet CHANNEL_NAME ProcProfile)
-> [(CHANNEL_NAME, ProcProfile)] -> MapSet CHANNEL_NAME ProcProfile
forall a b. (a -> b) -> a -> b
$ ProcessMap -> [(CHANNEL_NAME, ProcProfile)]
forall k a. Map k a -> [k]
Map.keys ProcessMap
proc1
    up2 :: MapSet CHANNEL_NAME ProcProfile
up2 = ((CHANNEL_NAME, ProcProfile)
 -> MapSet CHANNEL_NAME ProcProfile
 -> MapSet CHANNEL_NAME ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> [(CHANNEL_NAME, ProcProfile)]
-> MapSet CHANNEL_NAME ProcProfile
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CHANNEL_NAME, ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delProc (CspSign -> MapSet CHANNEL_NAME ProcProfile
procSet CspSign
s2) ([(CHANNEL_NAME, ProcProfile)] -> MapSet CHANNEL_NAME ProcProfile)
-> [(CHANNEL_NAME, ProcProfile)] -> MapSet CHANNEL_NAME ProcProfile
forall a b. (a -> b) -> a -> b
$ ProcessMap -> [(CHANNEL_NAME, ProcProfile)]
forall k a. Map k a -> [k]
Map.keys ProcessMap
proc2
    up :: MapSet CHANNEL_NAME ProcProfile
up = MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union MapSet CHANNEL_NAME ProcProfile
up1 MapSet CHANNEL_NAME ProcProfile
up2
    (cds :: [Diagnosis]
cds, cMap :: ChanMap
cMap) = (((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)
 -> ([Diagnosis], ChanMap) -> ([Diagnosis], ChanMap))
-> ([Diagnosis], ChanMap)
-> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
-> ([Diagnosis], ChanMap)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (isc :: (CHANNEL_NAME, CHANNEL_NAME)
isc@(i :: CHANNEL_NAME
i, s :: CHANNEL_NAME
s), j :: CHANNEL_NAME
j) (ds :: [Diagnosis]
ds, m :: ChanMap
m) ->
          case (CHANNEL_NAME, CHANNEL_NAME) -> ChanMap -> Maybe CHANNEL_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CHANNEL_NAME, CHANNEL_NAME)
isc ChanMap
m of
          Nothing -> ([Diagnosis]
ds, (CHANNEL_NAME, CHANNEL_NAME) -> CHANNEL_NAME -> ChanMap -> ChanMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (CHANNEL_NAME, CHANNEL_NAME)
isc CHANNEL_NAME
j ChanMap
m)
          Just k :: CHANNEL_NAME
k -> if CHANNEL_NAME
j CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
k then ([Diagnosis]
ds, ChanMap
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of channel " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> ShowS
forall a. Show a => a -> ShowS
shows CHANNEL_NAME
i ":"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CHANNEL_NAME
s " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> ShowS
forall a. Show a => a -> ShowS
shows CHANNEL_NAME
j " and "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> ShowS
forall a. Show a => a -> ShowS
shows CHANNEL_NAME
k "") Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, ChanMap
m)) ([], ChanMap
chan1)
          (ChanMap -> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList ChanMap
chan2 [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
-> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
-> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
forall a. [a] -> [a] -> [a]
++ ((CHANNEL_NAME, PROC_ARGS)
 -> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)])
-> [(CHANNEL_NAME, PROC_ARGS)]
-> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ (c :: CHANNEL_NAME
c, ts :: PROC_ARGS
ts) -> (CHANNEL_NAME -> ((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME))
-> PROC_ARGS -> [((CHANNEL_NAME, CHANNEL_NAME), CHANNEL_NAME)]
forall a b. (a -> b) -> [a] -> [b]
map
              ( \ s :: CHANNEL_NAME
s -> ((CHANNEL_NAME
c, CHANNEL_NAME
s), CHANNEL_NAME
c)) PROC_ARGS
ts) (MapSet CHANNEL_NAME CHANNEL_NAME -> [(CHANNEL_NAME, PROC_ARGS)]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList MapSet CHANNEL_NAME CHANNEL_NAME
uc))
    (pds :: [Diagnosis]
pds, pMap :: ProcessMap
pMap) =
      (((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)
 -> ([Diagnosis], ProcessMap) -> ([Diagnosis], ProcessMap))
-> ([Diagnosis], ProcessMap)
-> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
-> ([Diagnosis], ProcessMap)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (isc :: (CHANNEL_NAME, ProcProfile)
isc@(i :: CHANNEL_NAME
i, pt :: ProcProfile
pt), j :: CHANNEL_NAME
j) (ds :: [Diagnosis]
ds, m :: ProcessMap
m) ->
          case (CHANNEL_NAME, ProcProfile) -> ProcessMap -> Maybe CHANNEL_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CHANNEL_NAME, ProcProfile)
isc ProcessMap
m of
          Nothing -> ([Diagnosis]
ds, (CHANNEL_NAME, ProcProfile)
-> CHANNEL_NAME -> ProcessMap -> ProcessMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (CHANNEL_NAME, ProcProfile)
isc CHANNEL_NAME
j ProcessMap
m)
          Just k :: CHANNEL_NAME
k -> if CHANNEL_NAME
j CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
k then ([Diagnosis]
ds, ProcessMap
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of process " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> ShowS
forall a. Show a => a -> ShowS
shows CHANNEL_NAME
i " "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ ProcProfile -> ShowS
forall a. Pretty a => a -> ShowS
showDoc ProcProfile
pt " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
forall a. Show a => a -> String
show CHANNEL_NAME
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
forall a. Show a => a -> String
show CHANNEL_NAME
k) Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, ProcessMap
m)) ([Diagnosis]
cds, ProcessMap
proc1)
          (ProcessMap -> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList ProcessMap
proc2 [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
-> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
-> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
forall a. [a] -> [a] -> [a]
++ ((CHANNEL_NAME, [ProcProfile])
 -> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)])
-> [(CHANNEL_NAME, [ProcProfile])]
-> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ (p :: CHANNEL_NAME
p, pts :: [ProcProfile]
pts) -> (ProcProfile -> ((CHANNEL_NAME, ProcProfile), CHANNEL_NAME))
-> [ProcProfile] -> [((CHANNEL_NAME, ProcProfile), CHANNEL_NAME)]
forall a b. (a -> b) -> [a] -> [b]
map
              ( \ pt :: ProcProfile
pt -> ((CHANNEL_NAME
p, ProcProfile
pt), CHANNEL_NAME
p)) [ProcProfile]
pts)
              (MapSet CHANNEL_NAME ProcProfile -> [(CHANNEL_NAME, [ProcProfile])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList MapSet CHANNEL_NAME ProcProfile
up))
     in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
pds then CspAddMorphism -> Result CspAddMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return CspAddMorphism
emptyCspAddMorphism
        { channelMap :: ChanMap
channelMap = ChanMap
cMap
        , processMap :: ProcessMap
processMap = ProcessMap
pMap }
        else [Diagnosis] -> Maybe CspAddMorphism -> Result CspAddMorphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
pds Maybe CspAddMorphism
forall a. Maybe a
Nothing

toCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism
  -> Map.Map CspSymbol CspSymbol
toCspSymbMap :: Bool
-> Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol
toCspSymbMap b :: Bool
b mor :: Morphism f CspSign CspAddMorphism
mor = let
    src :: CspSign
src = Sign f CspSign -> CspSign
forall f e. Sign f e -> e
extendedInfo (Sign f CspSign -> CspSign) -> Sign f CspSign -> CspSign
forall a b. (a -> b) -> a -> b
$ Morphism f CspSign CspAddMorphism -> Sign f CspSign
forall f e m. Morphism f e m -> Sign f e
msource Morphism f CspSign CspAddMorphism
mor
    chanSymMap :: Map CspSymbol CspSymbol
chanSymMap = (CHANNEL_NAME
 -> CHANNEL_NAME
 -> Map CspSymbol CspSymbol
 -> Map CspSymbol CspSymbol)
-> Map CspSymbol CspSymbol
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> Map CspSymbol CspSymbol
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
      ( \ i :: CHANNEL_NAME
i t :: CHANNEL_NAME
t -> let
              p :: (CHANNEL_NAME, CHANNEL_NAME)
p = (CHANNEL_NAME
i, CHANNEL_NAME
t)
              q :: (CHANNEL_NAME, CHANNEL_NAME)
q@(j :: CHANNEL_NAME
j, _) = Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannel Morphism f CspSign CspAddMorphism
mor (CHANNEL_NAME, CHANNEL_NAME)
p
              in if Bool
b Bool -> Bool -> Bool
&& CHANNEL_NAME
i CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
j then Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall a. a -> a
id else
                     CspSymbol
-> CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((CHANNEL_NAME, CHANNEL_NAME) -> CspSymbol
toChanSymbol (CHANNEL_NAME, CHANNEL_NAME)
p) (CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol)
-> CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ (CHANNEL_NAME, CHANNEL_NAME) -> CspSymbol
toChanSymbol (CHANNEL_NAME, CHANNEL_NAME)
q)
      Map CspSymbol CspSymbol
forall k a. Map k a
Map.empty (MapSet CHANNEL_NAME CHANNEL_NAME -> Map CspSymbol CspSymbol)
-> MapSet CHANNEL_NAME CHANNEL_NAME -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME CHANNEL_NAME
chans CspSign
src
    procSymMap :: Map CspSymbol CspSymbol
procSymMap = (CHANNEL_NAME
 -> ProcProfile
 -> Map CspSymbol CspSymbol
 -> Map CspSymbol CspSymbol)
-> Map CspSymbol CspSymbol
-> MapSet CHANNEL_NAME ProcProfile
-> Map CspSymbol CspSymbol
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
      ( \ i :: CHANNEL_NAME
i t :: ProcProfile
t@(ProcProfile _ al :: CommAlpha
al) -> let
              p :: (CHANNEL_NAME, ProcProfile)
p = (CHANNEL_NAME
i, ProcProfile
t)
              al1 :: CommAlpha
al1 = Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
forall f.
Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha Morphism f CspSign CspAddMorphism
mor CommAlpha
al
              q :: (CHANNEL_NAME, ProcProfile)
q@(j :: CHANNEL_NAME
j, ProcProfile _ al2 :: CommAlpha
al2) = Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
mapProcess Morphism f CspSign CspAddMorphism
mor (CHANNEL_NAME, ProcProfile)
p
              in if Bool
b Bool -> Bool -> Bool
&& CHANNEL_NAME
i CHANNEL_NAME -> CHANNEL_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== CHANNEL_NAME
j Bool -> Bool -> Bool
&& CommAlpha
al1 CommAlpha -> CommAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== CommAlpha
al2 then Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall a. a -> a
id else
                     CspSymbol
-> CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((CHANNEL_NAME, ProcProfile) -> CspSymbol
toProcSymbol (CHANNEL_NAME, ProcProfile)
p) (CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol)
-> CspSymbol -> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ (CHANNEL_NAME, ProcProfile) -> CspSymbol
toProcSymbol (CHANNEL_NAME, ProcProfile)
q)
      Map CspSymbol CspSymbol
forall k a. Map k a
Map.empty (MapSet CHANNEL_NAME ProcProfile -> Map CspSymbol CspSymbol)
-> MapSet CHANNEL_NAME ProcProfile -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME ProcProfile
procSet CspSign
src
  in Map CspSymbol CspSymbol
-> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map CspSymbol CspSymbol
chanSymMap Map CspSymbol CspSymbol
procSymMap

cspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol
cspMorphismToCspSymbMap :: CspCASLMorphism -> Map CspSymbol CspSymbol
cspMorphismToCspSymbMap mor :: CspCASLMorphism
mor =
  Map CspSymbol CspSymbol
-> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(CspSymbol, CspSymbol)] -> Map CspSymbol CspSymbol
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    ([(CspSymbol, CspSymbol)] -> Map CspSymbol CspSymbol)
-> ([(Symbol, Symbol)] -> [(CspSymbol, CspSymbol)])
-> [(Symbol, Symbol)]
-> Map CspSymbol CspSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Symbol) -> (CspSymbol, CspSymbol))
-> [(Symbol, Symbol)] -> [(CspSymbol, CspSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: Symbol
a, b :: Symbol
b) -> (Symbol -> CspSymbol
caslToCspSymbol Symbol
a, Symbol -> CspSymbol
caslToCspSymbol Symbol
b))
    ([(Symbol, Symbol)] -> Map CspSymbol CspSymbol)
-> [(Symbol, Symbol)] -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ Map Symbol Symbol -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Symbol Symbol -> [(Symbol, Symbol)])
-> Map Symbol Symbol -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> Map Symbol Symbol
forall f e m. Morphism f e m -> Map Symbol Symbol
morphismToSymbMap CspCASLMorphism
mor)
  (Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol)
-> Map CspSymbol CspSymbol -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ Bool -> CspCASLMorphism -> Map CspSymbol CspSymbol
forall f.
Bool
-> Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol
toCspSymbMap Bool
False CspCASLMorphism
mor

-- | Instance for CspCASL signature extension
instance SignExtension CspSign where
  isSubSignExtension :: CspSign -> CspSign -> Bool
isSubSignExtension = CspSign -> CspSign -> Bool
isCspSubSign

-- | a dummy instances used for the default definition
instance Pretty CspAddMorphism where
  pretty :: CspAddMorphism -> Doc
pretty m :: CspAddMorphism
m = Map CspSymbol CspSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty (Map CspSymbol CspSymbol -> Doc) -> Map CspSymbol CspSymbol -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> CspCASLMorphism -> Map CspSymbol CspSymbol
forall f.
Bool
-> Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol
toCspSymbMap Bool
False
    (CspCASLMorphism -> Map CspSymbol CspSymbol)
-> CspCASLMorphism -> Map CspSymbol CspSymbol
forall a b. (a -> b) -> a -> b
$ CspAddMorphism -> CspCASLSign -> CspCASLSign -> CspCASLMorphism
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism CspAddMorphism
m CspCASLSign
emptyCspCASLSign CspCASLSign
emptyCspCASLSign

-- | Instance for CspCASL morphism extension (used for Category)
instance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
    where
      ideMorphismExtension :: CspSign -> CspAddMorphism
ideMorphismExtension _ = CspAddMorphism
emptyCspAddMorphism
      composeMorphismExtension :: Morphism f CspSign CspAddMorphism
-> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
composeMorphismExtension = Morphism f CspSign CspAddMorphism
-> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
forall f.
Morphism f CspSign CspAddMorphism
-> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
composeCspAddMorphism
      -- we omit inverses here
      isInclusionMorphismExtension :: CspAddMorphism -> Bool
isInclusionMorphismExtension m :: CspAddMorphism
m =
        ChanMap -> Bool
forall k a. Map k a -> Bool
Map.null (CspAddMorphism -> ChanMap
channelMap CspAddMorphism
m) Bool -> Bool -> Bool
&& ProcessMap -> Bool
forall k a. Map k a -> Bool
Map.null (CspAddMorphism -> ProcessMap
processMap CspAddMorphism
m)
      -- pretty printing for Csp morphisms
      prettyMorphismExtension :: Morphism f CspSign CspAddMorphism -> Doc
prettyMorphismExtension = (Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map CspSymbol CspSymbol
-> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id [Doc] -> Doc
sepByCommas Doc -> Doc -> Doc
pairElems
        (Map CspSymbol CspSymbol -> Doc)
-> (Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol)
-> Morphism f CspSign CspAddMorphism
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol
forall f.
Bool
-> Morphism f CspSign CspAddMorphism -> Map CspSymbol CspSymbol
toCspSymbMap Bool
True
      legalMorphismExtension :: Morphism f CspSign CspAddMorphism -> Result ()
legalMorphismExtension m :: Morphism f CspSign CspAddMorphism
m = do
        Morphism f CspSign CspAddMorphism -> Result ()
forall f. Morphism f CspSign CspAddMorphism -> Result ()
checkReflCondition Morphism f CspSign CspAddMorphism
m
        Morphism f CspSign CspAddMorphism -> Result ()
forall f. Morphism f CspSign CspAddMorphism -> Result ()
checkWNECondition Morphism f CspSign CspAddMorphism
m


-- * induced signature extension

inducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap
inducedChanMap :: Sort_map
-> ChanMap
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
inducedChanMap sm :: Sort_map
sm cm :: ChanMap
cm = (CHANNEL_NAME
 -> CHANNEL_NAME
 -> MapSet CHANNEL_NAME CHANNEL_NAME
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  ( \ i :: CHANNEL_NAME
i s :: CHANNEL_NAME
s ->
      let (j :: CHANNEL_NAME
j, t :: CHANNEL_NAME
t) = Sort_map
-> ChanMap
-> (CHANNEL_NAME, CHANNEL_NAME)
-> (CHANNEL_NAME, CHANNEL_NAME)
mapChan Sort_map
sm ChanMap
cm (CHANNEL_NAME
i, CHANNEL_NAME
s)
      in CHANNEL_NAME
-> CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert CHANNEL_NAME
j CHANNEL_NAME
t) MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. MapSet a b
MapSet.empty

inducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap
  -> ProcNameMap
inducedProcMap :: Sort_map
-> ChanMap
-> ProcessMap
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
inducedProcMap sm :: Sort_map
sm cm :: ChanMap
cm pm :: ProcessMap
pm = (CHANNEL_NAME
 -> ProcProfile
 -> MapSet CHANNEL_NAME ProcProfile
 -> MapSet CHANNEL_NAME ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  ( \ n :: CHANNEL_NAME
n p :: ProcProfile
p ->
      let (m :: CHANNEL_NAME
m, q :: ProcProfile
q) = Sort_map
-> ChanMap
-> ProcessMap
-> (CHANNEL_NAME, ProcProfile)
-> (CHANNEL_NAME, ProcProfile)
mapProcId Sort_map
sm ChanMap
cm ProcessMap
pm (CHANNEL_NAME
n, ProcProfile
p)
      in CHANNEL_NAME
-> ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert CHANNEL_NAME
m ProcProfile
q) MapSet CHANNEL_NAME ProcProfile
forall a b. MapSet a b
MapSet.empty

inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign
inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign
inducedCspSign sm :: Sort_map
sm _ _ m :: CspAddMorphism
m sig :: Sign f CspSign
sig =
  let csig :: CspSign
csig = Sign f CspSign -> CspSign
forall f e. Sign f e -> e
extendedInfo Sign f CspSign
sig
      cm :: ChanMap
cm = CspAddMorphism -> ChanMap
channelMap CspAddMorphism
m
  in CspSign
emptyCspSign
     { chans :: MapSet CHANNEL_NAME CHANNEL_NAME
chans = Sort_map
-> ChanMap
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
inducedChanMap Sort_map
sm ChanMap
cm (MapSet CHANNEL_NAME CHANNEL_NAME
 -> MapSet CHANNEL_NAME CHANNEL_NAME)
-> MapSet CHANNEL_NAME CHANNEL_NAME
-> MapSet CHANNEL_NAME CHANNEL_NAME
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME CHANNEL_NAME
chans CspSign
csig
     , procSet :: MapSet CHANNEL_NAME ProcProfile
procSet = Sort_map
-> ChanMap
-> ProcessMap
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
inducedProcMap Sort_map
sm ChanMap
cm (CspAddMorphism -> ProcessMap
processMap CspAddMorphism
m) (MapSet CHANNEL_NAME ProcProfile
 -> MapSet CHANNEL_NAME ProcProfile)
-> MapSet CHANNEL_NAME ProcProfile
-> MapSet CHANNEL_NAME ProcProfile
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet CHANNEL_NAME ProcProfile
procSet CspSign
csig }

-- * application of morphisms to sentences

-- | Apply a Signature Morphism to a CspCASL Sentence
mapSen :: CspCASLMorphism -> CspSen -> CspSen
mapSen :: CspCASLMorphism -> CspSen -> CspSen
mapSen mor :: CspCASLMorphism
mor sen :: CspSen
sen =
    if (CspAddMorphism -> Bool) -> CspCASLMorphism -> Bool
forall m f e. (m -> Bool) -> Morphism f e m -> Bool
CASL_Morphism.isInclusionMorphism
       CspAddMorphism -> Bool
forall e m. MorphismExtension e m => m -> Bool
CASL_Morphism.isInclusionMorphismExtension CspCASLMorphism
mor
    then CspSen
sen
    else case CspSen
sen of
           ProcessEq procName :: FQ_PROCESS_NAME
procName fqVarList :: FQProcVarList
fqVarList commAlpha :: CommAlpha
commAlpha proc :: PROCESS
proc ->
               let {- Map the morphism over all the parts of the process
                   equation -}
                   newProcName :: FQ_PROCESS_NAME
newProcName = CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName CspCASLMorphism
mor FQ_PROCESS_NAME
procName
                   newFqVarList :: FQProcVarList
newFqVarList = CspCASLMorphism -> FQProcVarList -> FQProcVarList
mapFQProcVarList CspCASLMorphism
mor FQProcVarList
fqVarList
                   newCommAlpha :: CommAlpha
newCommAlpha = CspCASLMorphism -> CommAlpha -> CommAlpha
forall f.
Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha CspCASLMorphism
mor CommAlpha
commAlpha
                   newProc :: PROCESS
newProc = CspCASLMorphism -> PROCESS -> PROCESS
mapProc CspCASLMorphism
mor PROCESS
proc
               in FQ_PROCESS_NAME -> FQProcVarList -> CommAlpha -> PROCESS -> CspSen
ProcessEq FQ_PROCESS_NAME
newProcName FQProcVarList
newFqVarList
                                    CommAlpha
newCommAlpha PROCESS
newProc

-- | Apply a signature morphism  to a Fully Qualified Process Variable List
mapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList
mapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList
mapFQProcVarList mor :: CspCASLMorphism
mor =
    -- As these are terms, just map the morphism over CASL TERMs
    (TERM () -> TERM ()) -> FQProcVarList -> FQProcVarList
forall a b. (a -> b) -> [a] -> [b]
map (CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm CspCASLMorphism
mor)

-- | Apply a signature morphism to a process
mapProc :: CspCASLMorphism -> PROCESS -> PROCESS
mapProc :: CspCASLMorphism -> PROCESS -> PROCESS
mapProc mor :: CspCASLMorphism
mor proc :: PROCESS
proc =
    let mapProc' :: PROCESS -> PROCESS
mapProc' = CspCASLMorphism -> PROCESS -> PROCESS
mapProc CspCASLMorphism
mor
        mapProcessName' :: FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName' = CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName CspCASLMorphism
mor
        mapEvent' :: EVENT -> EVENT
mapEvent' = CspCASLMorphism -> EVENT -> EVENT
mapEvent CspCASLMorphism
mor
        mapEventSet' :: EVENT_SET -> EVENT_SET
mapEventSet' = CspCASLMorphism -> EVENT_SET -> EVENT_SET
mapEventSet CspCASLMorphism
mor
        mapRenaming' :: RENAMING -> RENAMING
mapRenaming' = CspCASLMorphism -> RENAMING -> RENAMING
mapRenaming CspCASLMorphism
mor
        mapCommAlpha' :: CommAlpha -> CommAlpha
mapCommAlpha' = CspCASLMorphism -> CommAlpha -> CommAlpha
forall f.
Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha CspCASLMorphism
mor
        mapCASLTerm' :: TERM () -> TERM ()
mapCASLTerm' = CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm CspCASLMorphism
mor
        mapCASLFormula' :: FORMULA () -> FORMULA ()
mapCASLFormula' = CspCASLMorphism -> FORMULA () -> FORMULA ()
mapCASLFormula CspCASLMorphism
mor
    in case PROCESS
proc of
         Skip r :: Range
r -> Range -> PROCESS
Skip Range
r
         Stop r :: Range
r -> Range -> PROCESS
Stop Range
r
         Div r :: Range
r -> Range -> PROCESS
Div Range
r
         Run es :: EVENT_SET
es r :: Range
r -> EVENT_SET -> Range -> PROCESS
Run (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
es) Range
r
         Chaos ev :: EVENT_SET
ev r :: Range
r -> EVENT_SET -> Range -> PROCESS
Chaos (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
ev) Range
r
         PrefixProcess e :: EVENT
e p :: PROCESS
p r :: Range
r ->
             EVENT -> PROCESS -> Range -> PROCESS
PrefixProcess (EVENT -> EVENT
mapEvent' EVENT
e) (PROCESS -> PROCESS
mapProc' PROCESS
p) Range
r
         Sequential p :: PROCESS
p q :: PROCESS
q r :: Range
r -> PROCESS -> PROCESS -> Range -> PROCESS
Sequential (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         ExternalChoice p :: PROCESS
p q :: PROCESS
q r :: Range
r -> PROCESS -> PROCESS -> Range -> PROCESS
ExternalChoice (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         InternalChoice p :: PROCESS
p q :: PROCESS
q r :: Range
r -> PROCESS -> PROCESS -> Range -> PROCESS
InternalChoice (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         Interleaving p :: PROCESS
p q :: PROCESS
q r :: Range
r -> PROCESS -> PROCESS -> Range -> PROCESS
Interleaving (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         SynchronousParallel p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
             PROCESS -> PROCESS -> Range -> PROCESS
SynchronousParallel (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q r :: Range
r ->
             PROCESS -> EVENT_SET -> PROCESS -> Range -> PROCESS
GeneralisedParallel (PROCESS -> PROCESS
mapProc' PROCESS
p) (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
es) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         AlphabetisedParallel p :: PROCESS
p les :: EVENT_SET
les res :: EVENT_SET
res q :: PROCESS
q r :: Range
r ->
             PROCESS -> EVENT_SET -> EVENT_SET -> PROCESS -> Range -> PROCESS
AlphabetisedParallel (PROCESS -> PROCESS
mapProc' PROCESS
p) (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
les)
                                      (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
res) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         Hiding p :: PROCESS
p es :: EVENT_SET
es r :: Range
r ->
             PROCESS -> EVENT_SET -> Range -> PROCESS
Hiding (PROCESS -> PROCESS
mapProc' PROCESS
p) (EVENT_SET -> EVENT_SET
mapEventSet' EVENT_SET
es) Range
r
         RenamingProcess p :: PROCESS
p re :: RENAMING
re r :: Range
r ->
             PROCESS -> RENAMING -> Range -> PROCESS
RenamingProcess (PROCESS -> PROCESS
mapProc' PROCESS
p) (RENAMING -> RENAMING
mapRenaming' RENAMING
re) Range
r
         ConditionalProcess f :: FORMULA ()
f p :: PROCESS
p q :: PROCESS
q r :: Range
r ->
             FORMULA () -> PROCESS -> PROCESS -> Range -> PROCESS
ConditionalProcess (FORMULA () -> FORMULA ()
mapCASLFormula' FORMULA ()
f)
                                    (PROCESS -> PROCESS
mapProc' PROCESS
p) (PROCESS -> PROCESS
mapProc' PROCESS
q) Range
r
         NamedProcess pn :: FQ_PROCESS_NAME
pn fqParams :: FQProcVarList
fqParams r :: Range
r ->
             FQ_PROCESS_NAME -> FQProcVarList -> Range -> PROCESS
NamedProcess (FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName' FQ_PROCESS_NAME
pn) ((TERM () -> TERM ()) -> FQProcVarList -> FQProcVarList
forall a b. (a -> b) -> [a] -> [b]
map TERM () -> TERM ()
mapCASLTerm' FQProcVarList
fqParams) Range
r
         FQProcess p :: PROCESS
p commAlpha :: CommAlpha
commAlpha r :: Range
r ->
             PROCESS -> CommAlpha -> Range -> PROCESS
FQProcess (PROCESS -> PROCESS
mapProc' PROCESS
p) (CommAlpha -> CommAlpha
mapCommAlpha' CommAlpha
commAlpha) Range
r

-- | Apply a signature morphism to an event set
mapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET
mapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET
mapEventSet mor :: CspCASLMorphism
mor (EventSet fqComms :: [CommType]
fqComms r :: Range
r) =
  [CommType] -> Range -> EVENT_SET
EventSet ((CommType -> CommType) -> [CommType] -> [CommType]
forall a b. (a -> b) -> [a] -> [b]
map (CspCASLMorphism -> CommType -> CommType
forall f. Morphism f CspSign CspAddMorphism -> CommType -> CommType
mapCommType CspCASLMorphism
mor) [CommType]
fqComms) Range
r

-- | Apply a signature morphism to an event
mapEvent :: CspCASLMorphism -> EVENT -> EVENT
mapEvent :: CspCASLMorphism -> EVENT -> EVENT
mapEvent mor :: CspCASLMorphism
mor e :: EVENT
e =
    let mapCASLTerm' :: TERM () -> TERM ()
mapCASLTerm' = CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm CspCASLMorphism
mor
        mapChannelName' :: (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannelName' = CspCASLMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannel CspCASLMorphism
mor
    in case EVENT
e of
      -- Just map the morphism over the event (a term)
      FQTermEvent t :: TERM ()
t r :: Range
r -> TERM () -> Range -> EVENT
FQTermEvent (TERM () -> TERM ()
mapCASLTerm' TERM ()
t) Range
r
      {- Just map the morphism over the variable, this just maps the sort and
         keep the same name -}
      FQExternalPrefixChoice v :: TERM ()
v r :: Range
r -> TERM () -> Range -> EVENT
FQExternalPrefixChoice (TERM () -> TERM ()
mapCASLTerm' TERM ()
v) Range
r
      {- Just map the morphism over the variable, this just maps the sort and
         keep the same name -}
      FQInternalPrefixChoice v :: TERM ()
v r :: Range
r -> TERM () -> Range -> EVENT
FQInternalPrefixChoice (TERM () -> TERM ()
mapCASLTerm' TERM ()
v) Range
r
      -- Just map the morphism over the event (a term) and the channel name
      FQChanSend (c :: CHANNEL_NAME
c, s :: CHANNEL_NAME
s) t :: TERM ()
t r :: Range
r ->
        (CHANNEL_NAME, CHANNEL_NAME) -> TERM () -> Range -> EVENT
FQChanSend ((CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannelName' (CHANNEL_NAME
c, CHANNEL_NAME
s)) (TERM () -> TERM ()
mapCASLTerm' TERM ()
t) Range
r
      {- Just map the morphism over the sort and the channel name, we keep
         the variable name -}
      FQChanNonDetSend (c :: CHANNEL_NAME
c, s :: CHANNEL_NAME
s) v :: TERM ()
v r :: Range
r ->
        (CHANNEL_NAME, CHANNEL_NAME) -> TERM () -> Range -> EVENT
FQChanNonDetSend ((CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannelName' (CHANNEL_NAME
c, CHANNEL_NAME
s)) (TERM () -> TERM ()
mapCASLTerm' TERM ()
v) Range
r
      {- Just map the morphism over the sort and the channel name, we keep
         the variable name -}
      FQChanRecv (c :: CHANNEL_NAME
c, s :: CHANNEL_NAME
s) v :: TERM ()
v r :: Range
r ->
        (CHANNEL_NAME, CHANNEL_NAME) -> TERM () -> Range -> EVENT
FQChanRecv ((CHANNEL_NAME, CHANNEL_NAME) -> (CHANNEL_NAME, CHANNEL_NAME)
mapChannelName' (CHANNEL_NAME
c, CHANNEL_NAME
s)) (TERM () -> TERM ()
mapCASLTerm' TERM ()
v) Range
r
      _ -> String -> EVENT
forall a. HasCallStack => String -> a
error "CspCASL.Morphism.mapEvent: Cannot map unqualified event"

mapRename :: CspCASLMorphism -> Rename -> Rename
mapRename :: CspCASLMorphism -> Rename -> Rename
mapRename mor :: CspCASLMorphism
mor r :: Rename
r@(Rename i :: CHANNEL_NAME
i mc :: Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
mc) = case Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
mc of
  Nothing -> Rename
r
  Just (k :: RenameKind
k, ms :: Maybe (CHANNEL_NAME, CHANNEL_NAME)
ms) -> case Maybe (CHANNEL_NAME, CHANNEL_NAME)
ms of
    Nothing -> Rename
r
    Just (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2) -> case RenameKind
k of
      BinPred -> let
        (j :: CHANNEL_NAME
j, PredType [t1 :: CHANNEL_NAME
t1, t2 :: CHANNEL_NAME
t2]) = Sort_map
-> Pred_map -> (CHANNEL_NAME, PredType) -> (CHANNEL_NAME, PredType)
mapPredSym (CspCASLMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map CspCASLMorphism
mor) (CspCASLMorphism -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map CspCASLMorphism
mor)
            (CHANNEL_NAME
i, PROC_ARGS -> PredType
PredType [CHANNEL_NAME
s1, CHANNEL_NAME
s2])
        in CHANNEL_NAME
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename
Rename CHANNEL_NAME
j (Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename)
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename
forall a b. (a -> b) -> a -> b
$ (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
forall a. a -> Maybe a
Just (RenameKind
k, (CHANNEL_NAME, CHANNEL_NAME) -> Maybe (CHANNEL_NAME, CHANNEL_NAME)
forall a. a -> Maybe a
Just (CHANNEL_NAME
t1, CHANNEL_NAME
t2))
      _ -> let
        (j :: CHANNEL_NAME
j, OpType _ [t1 :: CHANNEL_NAME
t1] t2 :: CHANNEL_NAME
t2) = Sort_map
-> Op_map -> (CHANNEL_NAME, OpType) -> (CHANNEL_NAME, OpType)
mapOpSym (CspCASLMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map CspCASLMorphism
mor) (CspCASLMorphism -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CspCASLMorphism
mor)
            (CHANNEL_NAME
i, OpKind -> PROC_ARGS -> CHANNEL_NAME -> OpType
OpType OpKind
Partial [CHANNEL_NAME
s1] CHANNEL_NAME
s2)
        in CHANNEL_NAME
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename
Rename CHANNEL_NAME
j (Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename)
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME)) -> Rename
forall a b. (a -> b) -> a -> b
$ (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
-> Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
forall a. a -> Maybe a
Just (RenameKind
k, (CHANNEL_NAME, CHANNEL_NAME) -> Maybe (CHANNEL_NAME, CHANNEL_NAME)
forall a. a -> Maybe a
Just (CHANNEL_NAME
t1, CHANNEL_NAME
t2))

mapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING
mapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING
mapRenaming mor :: CspCASLMorphism
mor (Renaming rm :: [Rename]
rm) = [Rename] -> RENAMING
Renaming ([Rename] -> RENAMING) -> [Rename] -> RENAMING
forall a b. (a -> b) -> a -> b
$ (Rename -> Rename) -> [Rename] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map (CspCASLMorphism -> Rename -> Rename
mapRename CspCASLMorphism
mor) [Rename]
rm

cspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()
cspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()
cspCASLMorphism2caslMorphism m :: CspCASLMorphism
m =
  CspCASLMorphism
m { msource :: Sign () ()
msource = CspCASLSign -> Sign () ()
ccSig2CASLSign (CspCASLSign -> Sign () ()) -> CspCASLSign -> Sign () ()
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
msource CspCASLMorphism
m
    , mtarget :: Sign () ()
mtarget = CspCASLSign -> Sign () ()
ccSig2CASLSign (CspCASLSign -> Sign () ()) -> CspCASLSign -> Sign () ()
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CspCASLMorphism
m
    , extended_map :: ()
extended_map = () }

{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
TERM that appears in CspCASL). -}
mapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm =
    {- The error here is not used. It is a function to map over the morphism,
    CspCASL does not use this functionality. -}
    MapSen () () () -> Morphism () () () -> TERM () -> TERM ()
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
CASL_MapSen.mapTerm (String -> MapSen () () ()
forall a. HasCallStack => String -> a
error "CspCASL.Morphism.mapCASLTerm")
      (Morphism () () () -> TERM () -> TERM ())
-> (CspCASLMorphism -> Morphism () () ())
-> CspCASLMorphism
-> TERM ()
-> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspCASLMorphism -> Morphism () () ()
cspCASLMorphism2caslMorphism

{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL
FORMULA that appears in CspCASL). -}
mapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()
mapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()
mapCASLFormula =
    {- The error here is not used. It is a function to map over the morphism,
    CspCASL does not use this functionality. -}
    MapSen () () () -> Morphism () () () -> FORMULA () -> FORMULA ()
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
CASL_MapSen.mapSen (String -> MapSen () () ()
forall a. HasCallStack => String -> a
error "CspCASL.Morphism.mapCASLFormula")
      (Morphism () () () -> FORMULA () -> FORMULA ())
-> (CspCASLMorphism -> Morphism () () ())
-> CspCASLMorphism
-> FORMULA ()
-> FORMULA ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspCASLMorphism -> Morphism () () ()
cspCASLMorphism2caslMorphism

-- | Apply a signature morphism to a process name
mapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName mor :: CspCASLMorphism
mor pn :: FQ_PROCESS_NAME
pn = case FQ_PROCESS_NAME
pn of
    FQ_PROCESS_NAME pn' :: CHANNEL_NAME
pn' procProfilePn' :: ProcProfile
procProfilePn' ->
      let (m :: CHANNEL_NAME
m, procProfileM :: ProcProfile
procProfileM) =
            CspCASLMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
forall f.
Morphism f CspSign CspAddMorphism
-> (CHANNEL_NAME, ProcProfile) -> (CHANNEL_NAME, ProcProfile)
mapProcess CspCASLMorphism
mor (CHANNEL_NAME
pn', ProcProfile
procProfilePn')
      in CHANNEL_NAME -> ProcProfile -> FQ_PROCESS_NAME
FQ_PROCESS_NAME CHANNEL_NAME
m ProcProfile
procProfileM
    _ -> String -> FQ_PROCESS_NAME
forall a. HasCallStack => String -> a
error "unqualifed FQ_PROCESS_NAME"