3db86aab554edbb4244c8d1a1c90f152eee768afstevel{-# LANGUAGE MultiParamTypeClasses #-}

3db86aab554edbb4244c8d1a1c90f152eee768afstevel{- |

3db86aab554edbb4244c8d1a1c90f152eee768afstevelModule : $Header$

3db86aab554edbb4244c8d1a1c90f152eee768afstevelDescription : Symbols and signature morphisms for the CspCASL logic

3db86aab554edbb4244c8d1a1c90f152eee768afstevelCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008

3db86aab554edbb4244c8d1a1c90f152eee768afstevelLicense : GPLv2 or higher, see LICENSE.txt

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelMaintainer : csliam@swansea.ac.uk

3db86aab554edbb4244c8d1a1c90f152eee768afstevelStability : provisional

3db86aab554edbb4244c8d1a1c90f152eee768afstevelPortability : portable

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelSymbols and signature morphisms for the CspCASL logic

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-}

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmodule CspCASL.Morphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel ( CspCASLMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , CspAddMorphism (..)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , ChanMap

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , ProcessMap

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , mapProcProfile

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , cspSubsigInclusion

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , emptyCspAddMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , cspAddMorphismUnion

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , cspMorphismToCspSymbMap

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , inducedCspSign

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , mapSen

3db86aab554edbb4244c8d1a1c90f152eee768afstevel ) where

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CspCASL.AS_CspCASL_Process

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CspCASL.SignCSP

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CspCASL.Symbol

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified CspCASL.LocalTop as LT

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..))

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CASL.Sign as CASL_Sign

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport CASL.Morphism as CASL_Morphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified CASL.MapSentence as CASL_MapSen

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport Common.Doc

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport Common.DocUtils

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport Common.Id

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport Common.Result

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport Common.Utils (composeMap, isSingleton)

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified Common.Lib.MapSet as MapSet

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified Common.Lib.Rel as Rel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified Data.Map as Map

3db86aab554edbb4244c8d1a1c90f152eee768afstevelimport qualified Data.Set as Set

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- Morphisms

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel{- | This is the second component of a CspCASL signature moprhism, the process

3db86aab554edbb4244c8d1a1c90f152eee768afstevelname map. We map process name with a profile into new names and

3db86aab554edbb4244c8d1a1c90f152eee768afstevelcommunications alphabet. We follow CASL here and instread of mapping to a new

3db86aab554edbb4244c8d1a1c90f152eee768afstevelname and a new profile, we map just to the new name and the new

3db86aab554edbb4244c8d1a1c90f152eee768afstevelcommunications alphabet of the profile. This is because the argument sorts of

3db86aab554edbb4244c8d1a1c90f152eee768afstevelthe profile have no chocie they have to be the sorts resultsing from maping

3db86aab554edbb4244c8d1a1c90f152eee768afstevelthe original sorts in the profile with the data part map. Note: the

3db86aab554edbb4244c8d1a1c90f152eee768afstevelcommunications alphabet of the source profile must be downward closed with

3db86aab554edbb4244c8d1a1c90f152eee768afstevelrespect to the CASL signature sub-sort relation (at source) and also the

3db86aab554edbb4244c8d1a1c90f152eee768afsteveltarget communications alphabet must be downward closed with respect to the

3db86aab554edbb4244c8d1a1c90f152eee768afstevelCASL signature sub-sort relation (at target). -}

3db86aab554edbb4244c8d1a1c90f152eee768afsteveltype ProcessMap =

3db86aab554edbb4244c8d1a1c90f152eee768afstevel Map.Map (PROCESS_NAME, ProcProfile) (PROCESS_NAME, CommAlpha)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afsteveltype ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- | CspAddMorphism - This is just the extended part

3db86aab554edbb4244c8d1a1c90f152eee768afsteveldata CspAddMorphism = CspAddMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel {- Note that when applying the CspAddMorphism to process names or channel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel names, if the name is not in the map in the morphism, then the

3db86aab554edbb4244c8d1a1c90f152eee768afstevel application is the identity function. Thus empty maps are used to form

3db86aab554edbb4244c8d1a1c90f152eee768afstevel the empty morphism and the identity morphism. -}

3db86aab554edbb4244c8d1a1c90f152eee768afstevel { channelMap :: ChanMap

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , processMap :: ProcessMap

3db86aab554edbb4244c8d1a1c90f152eee768afstevel } deriving (Eq, Ord, Show)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- | The empty CspAddMorphism.

3db86aab554edbb4244c8d1a1c90f152eee768afstevelemptyCspAddMorphism :: CspAddMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevelemptyCspAddMorphism = CspAddMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel {- Note that when applying the CspAddMorphism to process names or

3db86aab554edbb4244c8d1a1c90f152eee768afstevel channel names, if the name is not in the map in the morphism,

3db86aab554edbb4244c8d1a1c90f152eee768afstevel then the application is the identity function. Thus empty maps

3db86aab554edbb4244c8d1a1c90f152eee768afstevel are used to form the empty morphism. -}

3db86aab554edbb4244c8d1a1c90f152eee768afstevel { channelMap = Map.empty

3db86aab554edbb4244c8d1a1c90f152eee768afstevel , processMap = Map.empty

3db86aab554edbb4244c8d1a1c90f152eee768afstevel }

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel{- | Given two signatures (the first being a sub signature of the second

3db86aab554edbb4244c8d1a1c90f152eee768afstevelaccording to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}

3db86aab554edbb4244c8d1a1c90f152eee768afstevelcspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevelcspSubsigInclusion = CASL_Morphism.sigInclusion emptyCspAddMorphism

3db86aab554edbb4244c8d1a1c90f152eee768afstevel{- We use the empty morphism as it also represents the identity, thus this

3db86aab554edbb4244c8d1a1c90f152eee768afstevelwill embed channel names and process names properly. -}

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- | lookup a typed channel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- | Apply a signature morphism to a channel name

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel -> (CHANNEL_NAME, SORT)

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapCommTypeAux sm cm ct = case ct of

3db86aab554edbb4244c8d1a1c90f152eee768afstevel CommTypeSort s -> CommTypeSort $ mapSort sm s

3db86aab554edbb4244c8d1a1c90f152eee768afstevel CommTypeChan (TypedChanName c s) -> let (d, t) = mapChan sm cm (c, s) in

3db86aab554edbb4244c8d1a1c90f152eee768afstevel CommTypeChan $ TypedChanName d t

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

3db86aab554edbb4244c8d1a1c90f152eee768afstevel-- | Apply a signature morphism to a CommType

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType

3db86aab554edbb4244c8d1a1c90f152eee768afstevelmapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)

3db86aab554edbb4244c8d1a1c90f152eee768afstevel

mapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha

mapCommAlphaAux sm = Set.map . mapCommTypeAux sm

-- | Apply a signature morphism to a CommAlpha

mapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha

mapCommAlpha = Set.map . mapCommType

mapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile

mapProcProfile sm cm (ProcProfile sl cs) =

ProcProfile (map (mapSort sm) sl) $ mapCommAlphaAux sm cm cs

mapProcId :: Sort_map -> ChanMap -> ProcessMap

-> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)

mapProcId sm cm pm (i, p) = let

n@(ProcProfile args _) = mapProcProfile sm cm p

in case Map.lookup (i, p) pm of

Nothing -> (i, n)

Just (j, alpha) -> (j, ProcProfile args alpha)

mapProcess :: Morphism f CspSign CspAddMorphism

-> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)

mapProcess mor = let em = extended_map mor in

mapProcId (sort_map mor) (channelMap em) $ processMap em

-- | Compose two CspAddMorphisms

composeCspAddMorphism :: Morphism f CspSign CspAddMorphism

-> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism

composeCspAddMorphism m1 m2 = let

sMap1 = sort_map m1

sMap2 = sort_map m2

sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2

src = msource m1

cSrc = extendedInfo src

cMap = MapSet.foldWithKey ( \ c s ->

let p = (c, s)

ni = fst $ mapChannel m2 $ mapChannel m1 p

in if c == ni then id else Map.insert p ni)

Map.empty $ chans cSrc

pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->

let pp = (p, pr)

(ni, ProcProfile _ na) =

mapProcess m2 $ mapProcess m1 pp

oa = mapCommAlphaAux sMap cMap a

in if p == ni && oa == na then id else

Map.insert pp (ni, na))

Map.empty $ procSet cSrc

in return emptyCspAddMorphism

{ channelMap = cMap

, 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 mor =

let sig = msource mor

sig' = mtarget mor

sm = sort_map mor

rel = sortRel sig

rel' = sortRel sig'

allPairs = LT.cartesian $ sortSet sig

failures = Set.filter (not . test) allPairs

test (s1, s2) = if Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||

mapSort sm s1 == mapSort sm s2

then Rel.path s1 s2 rel || s1 == s2

else True

in if Set.null failures

then return ()

else let produceDiag (s1, s2) =

let x = (mapSort sm s1)

y = (mapSort sm s2)

in Diag Error

("CSP-CASL Signature Morphism Refl Property Violated:\n'"

++ showDoc (Symbol x $ SubsortAsItemType y) "' but not\n'"

++ showDoc (Symbol s1 $ SubsortAsItemType s2) "'")

nullRange

allDiags = map produceDiag $ Set.toList failures

in Result allDiags 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 mor =

let sig = msource mor

sig' = mtarget mor

sm = sort_map mor

rel' = sortRel sig'

supers s signature = Set.insert s $ supersortsOf s signature

allPairsInSource = LT.cartesian $ sortSet sig

commonSuperSortsInTarget s1 s2 = Set.intersection

(supers (mapSort sm s1) sig')

(supers (mapSort sm s2) sig')

{- Candidates are triples (s1,s2,u') such that

\sigma(s1),\sigma(s2) < u' -}

createCandidateTripples (s1, s2) =

Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)

allCandidateTripples =

Set.unions $ Set.toList $ Set.map createCandidateTripples

allPairsInSource

testCandidate (s1, s2, u') =

let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)

test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'

in or $ Set.toList $ Set.map test possibleWitnesses

failures = Set.filter (not . testCandidate) allCandidateTripples

in if Set.null failures

then return ()

else let produceDiag (s1, s2, u') =

let x = (mapSort sm s1)

y = (mapSort sm s2)

in Diag Error

("CSP-CASL Signature Morphism Weak Non-Extension Property "

++ "Violated:\n'"

++ showDoc

(Subsort_decl [x, y] u' nullRange :: SORT_ITEM ())

"'\nbut no common supersort for\n'"

++ showDoc

(Sort_decl [s1, s2] nullRange :: SORT_ITEM ()) "'")

nullRange

allDiags = map produceDiag $ Set.toList failures

in Result allDiags Nothing -- failure with error messages

-- | unite morphisms

cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism

-> Result CspAddMorphism

cspAddMorphismUnion mor1 mor2 = let

s1 = extendedInfo $ msource mor1

s2 = extendedInfo $ msource mor2

m1 = extended_map mor1

m2 = extended_map mor2

chan1 = channelMap m1

chan2 = channelMap m2

delChan (n, s) m = MapSet.delete n s m

uc1 = foldr delChan (chans s1) $ Map.keys chan1

uc2 = foldr delChan (chans s2) $ Map.keys chan2

uc = MapSet.union uc1 uc2

proc1 = processMap m1

proc2 = processMap m2

delProc (n, p) m = MapSet.delete n p m

up1 = foldr delProc (procSet s1) $ Map.keys proc1

up2 = foldr delProc (procSet s2) $ Map.keys proc2

up = MapSet.union up1 up2

showAlpha (i, s) l = shows i (if null l then "" else "(..)") ++ ":"

++ if isSingleton s then showDoc (Set.findMin s) "" else showDoc s ""

(cds, cMap) = foldr ( \ (isc@(i, s), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of channel " ++ shows i ":"

++ showDoc s " to " ++ shows j " and "

++ shows k "") nullRange : ds, m)) ([], chan1)

(Map.toList chan2 ++ concatMap ( \ (c, ts) -> map

( \ s -> ((c, s), c)) ts) (MapSet.toList uc))

(pds, pMap) =

foldr ( \ (isc@(i, pt@(ProcProfile args _)), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of process " ++ shows i " "

++ showDoc pt " to " ++ showAlpha j args ++ " and "

++ showAlpha k args) nullRange : ds, m)) (cds, proc1)

(Map.toList proc2 ++ concatMap ( \ (p, pts) -> map

( \ pt@(ProcProfile _ al) -> ((p, pt), (p, al))) pts)

(MapSet.toList up))

in if null pds then return emptyCspAddMorphism

{ channelMap = cMap

, processMap = pMap }

else Result pds Nothing

toCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism

-> Map.Map CspSymbol CspSymbol

toCspSymbMap b mor = let

src = extendedInfo $ msource mor

chanSymMap = MapSet.foldWithKey

( \ i t -> let

p = (i, t)

q@(j, _) = mapChannel mor p

in if b && i == j then id else

Map.insert (toChanSymbol p) $ toChanSymbol q)

Map.empty $ chans src

procSymMap = MapSet.foldWithKey

( \ i t@(ProcProfile _ al) -> let

p = (i, t)

al1 = mapCommAlpha mor al

q@(j, ProcProfile _ al2) = mapProcess mor p

in if b && i == j && al1 == al2 then id else

Map.insert (toProcSymbol p) $ toProcSymbol q)

Map.empty $ procSet src

in Map.union chanSymMap procSymMap

cspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol

cspMorphismToCspSymbMap mor =

Map.union (Map.fromList

. map (\ (a, b) -> (caslToCspSymbol a, caslToCspSymbol b))

$ Map.toList $ morphismToSymbMap mor)

$ toCspSymbMap False mor

-- | Instance for CspCASL signature extension

instance SignExtension CspSign where

isSubSignExtension = isCspSubSign

-- | a dummy instances used for the default definition

instance Pretty CspAddMorphism where

pretty m = pretty $ toCspSymbMap False

$ embedMorphism m emptyCspCASLSign emptyCspCASLSign

-- | Instance for CspCASL morphism extension (used for Category)

instance CASL_Morphism.MorphismExtension CspSign CspAddMorphism

where

ideMorphismExtension _ = emptyCspAddMorphism

composeMorphismExtension = composeCspAddMorphism

-- we omit inverses here

isInclusionMorphismExtension m =

Map.null (channelMap m) && Map.null (processMap m)

-- pretty printing for Csp morphisms

prettyMorphismExtension = printMap id sepByCommas pairElems

. toCspSymbMap True

legalMorphismExtension m =

joinResult (checkReflCondition m) (checkWNECondition m)

-- * induced signature extension

inducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap

inducedChanMap sm cm = MapSet.foldWithKey

( \ i s ->

let (j, t) = mapChan sm cm (i, s)

in MapSet.insert j t) MapSet.empty

inducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap

-> ProcNameMap

inducedProcMap sm cm pm = MapSet.foldWithKey

( \ n p ->

let (m, q) = mapProcId sm cm pm (n, p)

in MapSet.insert m q) MapSet.empty

inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign

inducedCspSign sm _ _ m sig =

let csig = extendedInfo sig

cm = channelMap m

in emptyCspSign

{ chans = inducedChanMap sm cm $ chans csig

, procSet = inducedProcMap sm cm (processMap m) $ procSet csig }

-- * application of morhisms to sentences

-- | Apply a Signature Morphism to a CspCASL Sentence

mapSen :: CspCASLMorphism -> CspSen -> CspSen

mapSen mor sen =

if CASL_Morphism.isInclusionMorphism

CASL_Morphism.isInclusionMorphismExtension mor

then sen

else case sen of

ProcessEq procName fqVarList commAlpha proc ->

let {- Map the morphism over all the parts of the process

equation -}

newProcName = mapProcessName mor procName

newFqVarList = mapFQProcVarList mor fqVarList

newCommAlpha = mapCommAlpha mor commAlpha

newProc = mapProc mor proc

in ProcessEq newProcName newFqVarList

newCommAlpha newProc

-- | Apply a signature morphism to a Fully Qualified Process Variable List

mapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList

mapFQProcVarList mor =

-- As these are terms, just map the morphism over CASL TERMs

map (mapCASLTerm mor)

-- | Apply a signature morphism to a process

mapProc :: CspCASLMorphism -> PROCESS -> PROCESS

mapProc mor proc =

let mapProc' = mapProc mor

mapProcessName' = mapProcessName mor

mapEvent' = mapEvent mor

mapEventSet' = mapEventSet mor

mapRenaming' = mapRenaming mor

mapCommAlpha' = mapCommAlpha mor

mapCASLTerm' = mapCASLTerm mor

mapCASLFormula' = mapCASLFormula mor

in case proc of

Skip r -> Skip r

Stop r -> Stop r

Div r -> Div r

Run es r -> Run (mapEventSet' es) r

Chaos ev r -> Chaos (mapEventSet' ev) r

PrefixProcess e p r ->

PrefixProcess (mapEvent' e) (mapProc' p) r

Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r

ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r

InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r

Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r

SynchronousParallel p q r ->

SynchronousParallel (mapProc' p) (mapProc' q) r

GeneralisedParallel p es q r ->

GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r

AlphabetisedParallel p les res q r ->

AlphabetisedParallel (mapProc' p) (mapEventSet' les)

(mapEventSet' res) (mapProc' q) r

Hiding p es r ->

Hiding (mapProc' p) (mapEventSet' es) r

RenamingProcess p re r ->

RenamingProcess (mapProc' p) (mapRenaming' re) r

ConditionalProcess f p q r ->

ConditionalProcess (mapCASLFormula' f)

(mapProc' p) (mapProc' q) r

NamedProcess pn fqParams r ->

NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r

FQProcess p commAlpha r ->

FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r

-- | Apply a signature morphism to an event set

mapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET

mapEventSet mor (EventSet fqComms r) =

EventSet (map (mapCommType mor) fqComms) r

-- | Apply a signature morphism to an event

mapEvent :: CspCASLMorphism -> EVENT -> EVENT

mapEvent mor e =

let mapEvent' = mapEvent mor

mapCASLTerm' = mapCASLTerm mor

mapSort' = CASL_MapSen.mapSrt mor

mapChannelName' = mapChannel mor

in case e of

TermEvent t r ->

-- Just map the morphism over the event (a term)

TermEvent (mapCASLTerm' t) r

InternalPrefixChoice v s r ->

-- Just map the morphism over the sort, we keep the variable name

InternalPrefixChoice v (mapSort' s) r

ExternalPrefixChoice v s r ->

-- Just map the morphism over the sort, we keep the variable name

ExternalPrefixChoice v (mapSort' s) r

ChanSend c t r ->

-- Just map the morphism over the event (a term) and the channel name

ChanSend (fst $ mapChannelName' (c, sortOfTerm t)) (mapCASLTerm' t) r

ChanNonDetSend c v s r ->

{- Just map the morphism over the sort and the channel name, we keep

the variable name -}

ChanNonDetSend (fst $ mapChannelName' (c, s)) v (mapSort' s) r

ChanRecv c v s r ->

{- Just map the morphism over the sort and the channel name, we keep

the variable name -}

ChanRecv (fst $ mapChannelName' (c, s)) v (mapSort' s) r

FQEvent ev mfqc fqTerm r ->

-- Map the morphism over each part of the FQEvent

FQEvent (mapEvent' ev) (fmap mapChannelName' mfqc)

(mapCASLTerm' fqTerm) r

mapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING

mapRenaming mor re =

case re of

Renaming _ ->

{- There should be no (non fully qualified) Renamings (only

FQRenamings) as the static analysis should have transformed

EventSets into FQEventSets -}

error "CspCASL.Morphism.mapRenaming: Unexpected Renaming"

FQRenaming rs -> FQRenaming $ map (mapCASLTerm mor) rs

cspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()

cspCASLMorphism2caslMorphism m =

m { msource = ccSig2CASLSign $ msource m

, mtarget = ccSig2CASLSign $ mtarget m

, 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 =

{- The error here is not used. It is a function to map over the morphism,

CspCASL does not use this functionality. -}

CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm")

. 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 =

{- The error here is not used. It is a function to map over the morphism,

CspCASL does not use this functionality. -}

CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula")

. cspCASLMorphism2caslMorphism

-- | Apply a signature morphism to a process name

mapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME

mapProcessName mor pn = case pn of

FQ_PROCESS_NAME pn' procProfilePn' ->

let (m, procProfileM) =

mapProcess mor (pn', procProfilePn')

in FQ_PROCESS_NAME m procProfileM

_ -> error "unqualifed FQ_PROCESS_NAME"