1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyDescription : Symbols and signature morphisms for the CspCASL logic
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyMaintainer : csliam@swansea.ac.uk
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillySymbols and signature morphisms for the CspCASL logic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ( CspCASLMorphism
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder , CspAddMorphism (..)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder , mapProcProfile
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , cspSubsigInclusion
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , emptyCspAddMorphism
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly , cspAddMorphismUnion
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , cspMorphismToCspSymbMap
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder , inducedCspSign
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reillyimport qualified CspCASL.LocalTop as LT
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maederimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..), OpKind (..))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CASL.Sign as CASL_Sign
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maederimport CASL.Morphism as CASL_Morphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport qualified CASL.MapSentence as CASL_MapSen
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maederimport Common.Utils (composeMap)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reillyimport qualified Common.Lib.Rel as Rel
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport qualified Data.Map as Map
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport qualified Data.Set as Set
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly{- | This is the second component of a CspCASL signature morphism, the process
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedername map. We map process name with a profile into new names and
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedercommunications alphabet. We follow CASL here and instread of mapping to a new
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedername and a new profile, we map just to the new name and the new
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedercommunications alphabet of the profile. This is because the argument sorts of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederthe profile have no chocie they have to be the sorts resultsing from maping
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederthe original sorts in the profile with the data part map. Note: the
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedercommunications alphabet of the source profile must be downward closed with
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederrespect to the CASL signature sub-sort relation (at source) and also the
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedertarget communications alphabet must be downward closed with respect to the
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederCASL signature sub-sort relation (at target). -}
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedertype ProcessMap =
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly Map.Map (PROCESS_NAME, ProcProfile) PROCESS_NAME
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maedertype ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | CspAddMorphism - This is just the extended part
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata CspAddMorphism = CspAddMorphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder {- Note that when applying the CspAddMorphism to process names or channel
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder names, if the name is not in the map in the morphism, then the
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder application is the identity function. Thus empty maps are used to form
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder the empty morphism and the identity morphism. -}
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder { channelMap :: ChanMap
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , processMap :: ProcessMap
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder-- | The empty CspAddMorphism.
fa373bc327620e08861294716b4454be8d25669fChristian MaederemptyCspAddMorphism :: CspAddMorphism
fa373bc327620e08861294716b4454be8d25669fChristian MaederemptyCspAddMorphism = CspAddMorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder {- Note that when applying the CspAddMorphism to process names or
fa373bc327620e08861294716b4454be8d25669fChristian Maeder channel names, if the name is not in the map in the morphism,
fa373bc327620e08861294716b4454be8d25669fChristian Maeder then the application is the identity function. Thus empty maps
fa373bc327620e08861294716b4454be8d25669fChristian Maeder are used to form the empty morphism. -}
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | Given two signatures (the first being a sub signature of the second
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederaccording to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedercspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'ReillycspSubsigInclusion sign = checkResultMorphismIsLegal .
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly CASL_Morphism.sigInclusion emptyCspAddMorphism sign
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder{- We use the empty morphism as it also represents the identity, thus this
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederwill embed channel names and process names properly. -}
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'ReillycheckResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian MaedercheckResultMorphismIsLegal rmor = do
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder legalMorphismExtension mor
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | lookup a typed channel
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaedermapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | Apply a signature morphism to a channel name
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> (CHANNEL_NAME, SORT)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapCommTypeAux sm cm ct = case ct of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CommTypeSort s -> CommTypeSort $ mapSort sm s
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CommTypeChan (TypedChanName c s) -> let (d, t) = mapChan sm cm (c, s) in
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CommTypeChan $ TypedChanName d t
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder-- | Apply a signature morphism to a CommType
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedermapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapCommAlphaAux sm = Set.map . mapCommTypeAux sm
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder-- | Apply a signature morphism to a CommAlpha
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapCommAlpha = Set.map . mapCommType
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcProfile sm cm (ProcProfile sl cs) =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ProcProfile (map (mapSort sm) sl) $ mapCommAlphaAux sm cm cs
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcId :: Sort_map -> ChanMap -> ProcessMap
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcId sm cm pm (i, p) = let
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly n@(ProcProfile args alpha) = mapProcProfile sm cm p
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in case Map.lookup (i, p) pm of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> (i, n)
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly Just j -> (j, ProcProfile args alpha)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcess :: Morphism f CspSign CspAddMorphism
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapProcess mor = let em = extended_map mor in
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder mapProcId (sort_map mor) (channelMap em) $ processMap em
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Compose two CspAddMorphisms
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedercomposeCspAddMorphism :: Morphism f CspSign CspAddMorphism
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedercomposeCspAddMorphism m1 m2 = let
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sMap1 = sort_map m1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sMap2 = sort_map m2
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder src = msource m1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder cSrc = extendedInfo src
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder cMap = MapSet.foldWithKey ( \ c s ->
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let p = (c, s)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ni = fst $ mapChannel m2 $ mapChannel m1 p
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in if c == ni then id else Map.insert p ni)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let pp = (p, pr)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (ni, ProcProfile _ na) =
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder mapProcess m2 $ mapProcess m1 pp
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder oa = mapCommAlphaAux sMap cMap a
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in if p == ni && oa == na then id else
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in return emptyCspAddMorphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder { channelMap = cMap
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , processMap = pMap }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | A CspCASLMorphism is a CASL Morphism with the extended_map to be a
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederCspAddMorphism. -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maedertype CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly{- | Check if a CspCASL signature morphism has the refl property i.e.,
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillysigma(s1) <= sigma(s2) implies s1 <= s2 for all s1, s2 in S -}
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'ReillycheckReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian MaedercheckReflCondition Morphism
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder { msource = sig
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , mtarget = sig'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , sort_map = sm } = do
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder let rel = sortRel sig
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly rel' = sortRel sig'
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly allPairs = LT.cartesian $ sortSet sig
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly failures = Set.filter (not . test) allPairs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder test (s1, s2) = not (Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSort sm s1 == mapSort sm s2) ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Rel.path s1 s2 rel || s1 == s2)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder produceDiag (s1, s2) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let x = mapSort sm s1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder y = mapSort sm s2
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder in Diag Error
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder ("CSP-CASL Signature Morphism Refl Property Violated:\n'"
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder ++ showDoc (Symbol x $ SubsortAsItemType y)
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder "' in target but not in source\n'"
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder ++ showDoc (Symbol s1 $ SubsortAsItemType s2) "'")
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder allDiags = map produceDiag $ Set.toList failures
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder unless (Set.null failures)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder $ Result allDiags Nothing -- failure with error messages
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly{- | Check if a CspCASL signature morphism has the weak non extension property
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillysigma(s1) <= u' and sigma(s2) <= u' implies there exists t in S with
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillys1 <= t and s2 <= t and sigma(t) <= u' for all s1,s2 in S and u' in S' -}
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'ReillycheckWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian MaedercheckWNECondition Morphism
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder { msource = sig
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , mtarget = sig'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , sort_map = sm } = do
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder let rel' = sortRel sig'
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly supers s signature = Set.insert s $ supersortsOf s signature
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly allPairsInSource = LT.cartesian $ sortSet sig
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly commonSuperSortsInTarget s1 s2 = Set.intersection
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly (supers (mapSort sm s1) sig')
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly (supers (mapSort sm s2) sig')
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly {- Candidates are triples (s1,s2,u') such that
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly \sigma(s1),\sigma(s2) < u' -}
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly createCandidateTripples (s1, s2) =
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly allCandidateTripples =
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly Set.unions $ Set.toList $ Set.map createCandidateTripples
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly allPairsInSource
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly testCandidate (s1, s2, u') =
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly in or $ Set.toList $ Set.map test possibleWitnesses
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly failures = Set.filter (not . testCandidate) allCandidateTripples
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder produceDiag (s1, s2, u') =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let x = mapSort sm s1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder y = mapSort sm s2
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder in Diag Error
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder ("CSP-CASL Signature Morphism Weak Non-Extension Property "
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder ++ "Violated:\n'"
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder (Subsort_decl [x, y] u' nullRange :: SORT_ITEM ())
dc403ff45531bc75a7544b8b5fc52a5217a1a54aChristian Maeder "' in target\nbut no common supersort for the sorts\n'"
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder (Sort_decl [s1, s2] nullRange :: SORT_ITEM ())
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder "' in source")
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder allDiags = map produceDiag $ Set.toList failures
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder unless (Set.null failures)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder $ Result allDiags Nothing -- failure with error messages
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | unite morphisms
fa373bc327620e08861294716b4454be8d25669fChristian MaedercspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -> Result CspAddMorphism
fa373bc327620e08861294716b4454be8d25669fChristian MaedercspAddMorphismUnion mor1 mor2 = let
fa373bc327620e08861294716b4454be8d25669fChristian Maeder s1 = extendedInfo $ msource mor1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder s2 = extendedInfo $ msource mor2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder m1 = extended_map mor1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder m2 = extended_map mor2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder chan1 = channelMap m1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder chan2 = channelMap m2
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder delChan (n, s) = MapSet.delete n s
fa373bc327620e08861294716b4454be8d25669fChristian Maeder uc1 = foldr delChan (chans s1) $ Map.keys chan1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder uc2 = foldr delChan (chans s2) $ Map.keys chan2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proc1 = processMap m1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proc2 = processMap m2
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder delProc (n, p) = MapSet.delete n p
fa373bc327620e08861294716b4454be8d25669fChristian Maeder up1 = foldr delProc (procSet s1) $ Map.keys proc1
fa373bc327620e08861294716b4454be8d25669fChristian Maeder up2 = foldr delProc (procSet s2) $ Map.keys proc2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (cds, cMap) = foldr ( \ (isc@(i, s), j) (ds, m) ->
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Nothing -> (ds, Map.insert isc j m)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Just k -> if j == k then (ds, m) else
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ("incompatible mapping of channel " ++ shows i ":"
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ++ showDoc s " to " ++ shows j " and "
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ++ shows k "") nullRange : ds, m)) ([], chan1)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Map.toList chan2 ++ concatMap ( \ (c, ts) -> map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ s -> ((c, s), c)) ts) (MapSet.toList uc))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (pds, pMap) =
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder foldr ( \ (isc@(i, pt), j) (ds, m) ->
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Nothing -> (ds, Map.insert isc j m)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Just k -> if j == k then (ds, m) else
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ("incompatible mapping of process " ++ shows i " "
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder ++ showDoc pt " to " ++ show j ++ " and "
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder ++ show k) nullRange : ds, m)) (cds, proc1)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Map.toList proc2 ++ concatMap ( \ (p, pts) -> map
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder ( \ pt -> ((p, pt), p)) pts)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder in if null pds then return emptyCspAddMorphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder { channelMap = cMap
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , processMap = pMap }
fa373bc327620e08861294716b4454be8d25669fChristian Maeder else Result pds Nothing
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedertoCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -> Map.Map CspSymbol CspSymbol
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedertoCspSymbMap b mor = let
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder src = extendedInfo $ msource mor
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ i t -> let
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder q@(j, _) = mapChannel mor p
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in if b && i == j then id else
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Map.insert (toChanSymbol p) $ toChanSymbol q)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ i t@(ProcProfile _ al) -> let
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder al1 = mapCommAlpha mor al
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder q@(j, ProcProfile _ al2) = mapProcess mor p
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in if b && i == j && al1 == al2 then id else
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Map.insert (toProcSymbol p) $ toProcSymbol q)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in Map.union chanSymMap procSymMap
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaedercspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian MaedercspMorphismToCspSymbMap mor =
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder . map (\ (a, b) -> (caslToCspSymbol a, caslToCspSymbol b))
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder $ Map.toList $ morphismToSymbMap mor)
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder $ toCspSymbMap False mor
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder-- | Instance for CspCASL signature extension
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maederinstance SignExtension CspSign where
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder isSubSignExtension = isCspSubSign
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder-- | a dummy instances used for the default definition
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Pretty CspAddMorphism where
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder pretty m = pretty $ toCspSymbMap False
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder $ embedMorphism m emptyCspCASLSign emptyCspCASLSign
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Instance for CspCASL morphism extension (used for Category)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ideMorphismExtension _ = emptyCspAddMorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly composeMorphismExtension = composeCspAddMorphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- we omit inverses here
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder isInclusionMorphismExtension m =
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder Map.null (channelMap m) && Map.null (processMap m)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -- pretty printing for Csp morphisms
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder prettyMorphismExtension = printMap id sepByCommas pairElems
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder . toCspSymbMap True
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder legalMorphismExtension m = do
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder checkReflCondition m
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder checkWNECondition m
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder-- * induced signature extension
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaederinducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederinducedChanMap sm cm = MapSet.foldWithKey
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder let (j, t) = mapChan sm cm (i, s)
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaederinducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder -> ProcNameMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederinducedProcMap sm cm pm = MapSet.foldWithKey
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder let (m, q) = mapProcId sm cm pm (n, p)
bcd914850de931848b86d7728192a149f9c0108bChristian MaederinducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian MaederinducedCspSign sm _ _ m sig =
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder let csig = extendedInfo sig
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder cm = channelMap m
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder in emptyCspSign
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder { chans = inducedChanMap sm cm $ chans csig
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder , procSet = inducedProcMap sm cm (processMap m) $ procSet csig }
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly-- * application of morphisms to sentences
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a Signature Morphism to a CspCASL Sentence
bcd914850de931848b86d7728192a149f9c0108bChristian MaedermapSen :: CspCASLMorphism -> CspSen -> CspSen
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymapSen mor sen =
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder CASL_Morphism.isInclusionMorphismExtension mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly else case sen of
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder ProcessEq procName fqVarList commAlpha proc ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let {- Map the morphism over all the parts of the process
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder newProcName = mapProcessName mor procName
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly newFqVarList = mapFQProcVarList mor fqVarList
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly newCommAlpha = mapCommAlpha mor commAlpha
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly newProc = mapProc mor proc
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder in ProcessEq newProcName newFqVarList
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder newCommAlpha newProc
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a signature morphism to a Fully Qualified Process Variable List
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaedermapFQProcVarList mor =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- As these are terms, just map the morphism over CASL TERMs
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder map (mapCASLTerm mor)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a signature morphism to a process
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapProc :: CspCASLMorphism -> PROCESS -> PROCESS
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymapProc mor proc =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let mapProc' = mapProc mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapProcessName' = mapProcessName mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapEvent' = mapEvent mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapEventSet' = mapEventSet mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapRenaming' = mapRenaming mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapCommAlpha' = mapCommAlpha mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapCASLTerm' = mapCASLTerm mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly mapCASLFormula' = mapCASLFormula mor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in case proc of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Skip r -> Skip r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Stop r -> Stop r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Div r -> Div r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Run es r -> Run (mapEventSet' es) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Chaos ev r -> Chaos (mapEventSet' ev) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly PrefixProcess e p r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly PrefixProcess (mapEvent' e) (mapProc' p) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly SynchronousParallel p q r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly SynchronousParallel (mapProc' p) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly GeneralisedParallel p es q r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly AlphabetisedParallel p les res q r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly AlphabetisedParallel (mapProc' p) (mapEventSet' les)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (mapEventSet' res) (mapProc' q) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Hiding p es r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Hiding (mapProc' p) (mapEventSet' es) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly RenamingProcess p re r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly RenamingProcess (mapProc' p) (mapRenaming' re) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ConditionalProcess f p q r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ConditionalProcess (mapCASLFormula' f)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (mapProc' p) (mapProc' q) r
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder NamedProcess pn fqParams r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly FQProcess p commAlpha r ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a signature morphism to an event set
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian MaedermapEventSet mor (EventSet fqComms r) =
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder EventSet (map (mapCommType mor) fqComms) r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a signature morphism to an event
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapEvent :: CspCASLMorphism -> EVENT -> EVENT
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymapEvent mor e =
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder let mapCASLTerm' = mapCASLTerm mor
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder mapChannelName' = mapChannel mor
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly -- Just map the morphism over the event (a term)
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQTermEvent t r -> FQTermEvent (mapCASLTerm' t) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Just map the morphism over the variable, this just maps the sort and
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly keep the same name -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQExternalPrefixChoice v r -> FQExternalPrefixChoice (mapCASLTerm' v) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Just map the morphism over the variable, this just maps the sort and
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly keep the same name -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQInternalPrefixChoice v r -> FQInternalPrefixChoice (mapCASLTerm' v) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly -- Just map the morphism over the event (a term) and the channel name
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanSend (c, s) t r ->
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanSend (mapChannelName' (c, s)) (mapCASLTerm' t) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Just map the morphism over the sort and the channel name, we keep
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly the variable name -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanNonDetSend (c, s) v r ->
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanNonDetSend (mapChannelName' (c, s)) (mapCASLTerm' v) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly {- Just map the morphism over the sort and the channel name, we keep
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly the variable name -}
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanRecv (c, s) v r ->
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanRecv (mapChannelName' (c, s)) (mapCASLTerm' v) r
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly _ -> error "CspCASL.Morphism.mapEvent: Cannot map unqualified event"
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian MaedermapRename :: CspCASLMorphism -> Rename -> Rename
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian MaedermapRename mor r@(Rename i mc) = case mc of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder Just (k, ms) -> case ms of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder Just (s1, s2) -> case k of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder BinPred -> let
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder (j, PredType [t1, t2]) = mapPredSym (sort_map mor) (pred_map mor)
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder (i, PredType [s1, s2])
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder in Rename j $ Just (k, Just (t1, t2))
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder (j, OpType _ [t1] t2) = mapOpSym (sort_map mor) (op_map mor)
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder (i, OpType Partial [s1] s2)
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder in Rename j $ Just (k, Just (t1, t2))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian MaedermapRenaming mor (Renaming rm) = Renaming $ map (mapRename mor) rm
bcd914850de931848b86d7728192a149f9c0108bChristian MaedercspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()
bcd914850de931848b86d7728192a149f9c0108bChristian MaedercspCASLMorphism2caslMorphism m =
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder m { msource = ccSig2CASLSign $ msource m
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder , mtarget = ccSig2CASLSign $ mtarget m
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder , extended_map = () }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederTERM that appears in CspCASL). -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder {- The error here is not used. It is a function to map over the morphism,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CspCASL does not use this functionality. -}
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm")
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder . cspCASLMorphism2caslMorphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederFORMULA that appears in CspCASL). -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaedermapCASLFormula =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder {- The error here is not used. It is a function to map over the morphism,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CspCASL does not use this functionality. -}
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula")
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder . cspCASLMorphism2caslMorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Apply a signature morphism to a process name
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaedermapProcessName mor pn = case pn of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FQ_PROCESS_NAME pn' procProfilePn' ->
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly let (m, procProfileM) =
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly mapProcess mor (pn', procProfilePn')
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly in FQ_PROCESS_NAME m procProfileM
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly _ -> error "unqualifed FQ_PROCESS_NAME"