Morphism.hs revision 33bdce26495121cdbce30331ef90a1969126a840
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : Symbols and signature morphisms for the CspCASL logic
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : csliam@swansea.ac.uk
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederSymbols and signature morphisms for the CspCASL logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ( CspMorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , CspAddMorphism(..)
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder , emptyCspAddMorphism
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , makeChannelNameSymbol
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , makeProcNameSymbol
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport CASL.AS_Basic_CASL (FORMULA, TERM)
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maederimport CASL.Sign as CASL_Sign
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowskiimport qualified CASL.Morphism as CASL_Morphism
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maederimport qualified CASL.MapSentence as CASL_MapSen
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Common.Id(simpleIdToId)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport qualified Data.Map as Map
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport qualified Data.Set as Set
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichchannelNameSymbType :: SymbType
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederchannelNameSymbType = OtherTypeKind channelS
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian MaederprocessNameSymbType :: SymbType
4cb215739e9ab13447fa21162482ebe485b47455Christian MaederprocessNameSymbType = OtherTypeKind processS
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- | Calculate the set of symbols for a CspCASL signature
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedersymOf :: CspCASLSign -> Set.Set Symbol
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let caslSymbols = CASL_Morphism.symOf sigma -- Get CASL symbols
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder cspExt = extendedInfo sigma
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder chanNames = Map.keysSet (chans cspExt) -- Get the channel names
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder procNames = Map.keysSet (procSet cspExt) -- Get the process names
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder -- Make channel symbols from names
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder chanNameSymbols = Set.map makeChannelNameSymbol chanNames
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder -- Make process name symbols from names
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder procNameSymbols = Set.map makeProcNameSymbol procNames
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder in Set.unions [caslSymbols, chanNameSymbols, procNameSymbols]
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | Make a symbol form a channel name
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedermakeChannelNameSymbol :: CHANNEL_NAME -> Symbol
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaedermakeChannelNameSymbol c =
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder Symbol {symName = simpleIdToId c, symbType = channelNameSymbType}
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | Make a symbol form a process name
c3053d57f642ca507cdf79512e604437c4546cb9Christian MaedermakeProcNameSymbol :: PROCESS_NAME -> Symbol
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaedermakeProcNameSymbol p =
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Symbol {symName = simpleIdToId p, symbType = processNameSymbType}
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder-- | CspMorphism - This is just the extended part
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederdata CspAddMorphism = CspAddMorphism
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder { channelMap :: Map.Map CHANNEL_NAME CHANNEL_NAME
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder , processMap :: Map.Map PROCESS_NAME PROCESS_NAME
4ed0007ac9caea5b468f202521352d153481423cChristian Maeder } deriving (Eq, Ord, Show)
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder-- | Compose two Maps. We use this for Composing the channel and
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder-- process maps of a CspAddMorphism.
f13d1e86e58da53680e78043e8df182eed867efbChristian MaedercomposeMaps :: (Ord a, Ord b) => Map.Map a b -> Map.Map b c ->
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian MaedercomposeMaps m1 m2 =
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder Map.foldWithKey (\ i j -> case Map.lookup j m2 of
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder Nothing -> error "SignCsp.composeMaps"
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus Luettich-- | Compose two CspAddMorphisms
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus LuettichcomposeCspAddMorphism :: CspAddMorphism -> CspAddMorphism
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus Luettich -> Result CspAddMorphism
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichcomposeCspAddMorphism m1 m2 = return emptyCspAddMorphism
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich { channelMap = composeMaps (channelMap m1) $ channelMap m2
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich , processMap = composeMaps (processMap m1) $ processMap m2 }
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder-- | Calculate the inverse of a CspAddMorphism
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederinverseCspAddMorphism :: CspAddMorphism -> Result CspAddMorphism
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaederinverseCspAddMorphism cm = do
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder let chL = Map.toList $ channelMap cm
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder prL = Map.toList $ processMap cm
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich swap = map $ \ (a, b) -> (b, a)
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder isInj l = length l == Set.size (Set.fromList $ map snd l)
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder unless (isInj chL) $ fail "invertCspAddMorphism.channelMap"
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder unless (isInj prL) $ fail "invertCspAddMorphism.processMap"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return emptyCspAddMorphism
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder { channelMap = Map.fromList $ swap chL
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , processMap = Map.fromList $ swap prL }
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | A CspMorphism is a CASL Morphism with the extended_map to be a
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- CspAddMorphism.
9e748851c150e1022fb952bab3315e869aaf0214Christian Maedertype CspMorphism = CASL_Morphism.Morphism () CspSign CspAddMorphism
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | The empty CspAddMorphism.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederemptyCspAddMorphism :: CspAddMorphism
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederemptyCspAddMorphism =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- Note that when applying the CspAddMorphism to process names or
b886e9e5db2098d0112cc4f70aeba232962939ddChristian Maeder -- channel names, if the name is not in the map in the morphism,
15503d903d142d317200149b2d1d642053530365Christian Maeder -- then the application is the identity function. Thus empty maps
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -- are used to form the empty morphism.
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder CspAddMorphism { channelMap = Map.empty
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder-- | Pretty printing for Csp morphisms
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederinstance Pretty CspAddMorphism where
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder pretty = text . show
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | Instance for CspCASL morphism extension (used for Category)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederinstance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ideMorphismExtension _ = emptyCspAddMorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder composeMorphismExtension = composeCspAddMorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder inverseMorphismExtension = inverseCspAddMorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder isInclusionMorphismExtension _ = True -- missing! BUG
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- Application of morhisms to sentences
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Apply a Signature Morphism to a CspCASL Sentence
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian MaedermapSen :: CspMorphism -> CspCASLSen -> Result CspCASLSen
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermapSen mor sen =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder CASL_Morphism.isInclusionMorphismExtension) mor
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder then return sen
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder else case sen of
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder CASLSen caslSen ->
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder return $ CASLSen (mapCASLFormula mor caslSen)
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder ProcessEq procName fqVarList commAlpha proc ->
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder let -- Map the morphism over all the parts of the process
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder newProcName = mapProcessName mor procName
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder newFqVarList = mapFQProcVarList mor fqVarList
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder newCommAlpha = mapCommAlpha mor commAlpha
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder newProc = mapProc mor proc
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder in return (ProcessEq newProcName newFqVarList
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder newCommAlpha newProc)
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-- | Apply a signature morphism to a Fully Qualified Process Variable List
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian MaedermapFQProcVarList :: CspMorphism -> FQProcVarList -> FQProcVarList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermapFQProcVarList mor fqVarList =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- As these are terms, just map the morphism over CASL TERMs
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder map (mapCASLTerm mor) fqVarList
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Apply a signature morphism to a CommAlpha
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermapCommAlpha :: CspMorphism -> CommAlpha -> CommAlpha
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermapCommAlpha mor commAlpha = Set.map (mapCommType mor) commAlpha
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- | Apply a signature morphism to a CommType
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermapCommType :: CspMorphism -> CommType -> CommType
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian MaedermapCommType mor comm =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let mapSort' = CASL_MapSen.mapSrt mor
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapChannelName' = mapChannelName mor
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in case comm of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder CommTypeSort s ->
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder -- Just map the morphism over the sort
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder CommTypeSort (mapSort' s)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder CommTypeChan typedChanName ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case typedChanName of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder TypedChanName chanName chanSort ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- Just map the morphism over the sort and channel name
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder CommTypeChan $ TypedChanName (mapChannelName' chanName)
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder (mapSort' chanSort)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | Apply a signature morphism to a process
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichmapProc :: CspMorphism -> PROCESS -> PROCESS
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedermapProc mor proc =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let mapProc' = mapProc mor
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapProcessName' = mapProcessName mor
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapEvent' = mapEvent mor
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder mapEventSet' = mapEventSet mor
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mapRenaming' = mapRenaming mor
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mapCommAlpha' = mapCommAlpha mor
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mapCASLTerm' = mapCASLTerm mor
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mapCASLFormula' = mapCASLFormula mor
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder in case proc of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Skip r -> Skip r
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Stop r -> Stop r
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Div r -> Div r
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Run es r -> Run (mapEventSet' es) r
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Chaos ev r -> Chaos (mapEventSet' ev) r
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder PrefixProcess e p r ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder PrefixProcess (mapEvent' e) (mapProc' p) r
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder SynchronousParallel p q r ->
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder SynchronousParallel (mapProc' p) (mapProc' q) r
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder GeneralisedParallel p es q r ->
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder AlphabetisedParallel p les res q r ->
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder AlphabetisedParallel (mapProc' p) (mapEventSet' les)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder (mapEventSet' res) (mapProc' q) r
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Hiding p es r ->
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Hiding (mapProc' p) (mapEventSet' es) r
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich RenamingProcess p re r ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder RenamingProcess (mapProc' p) (mapRenaming' re) r
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ConditionalProcess f p q r ->
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich ConditionalProcess (mapCASLFormula' f)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (mapProc' p) (mapProc' q) r
4ed0007ac9caea5b468f202521352d153481423cChristian Maeder NamedProcess pn fqParams r ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder FQProcess p commAlpha r ->
b886e9e5db2098d0112cc4f70aeba232962939ddChristian Maeder FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Apply a signature morphism to an event set
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedermapEventSet :: CspMorphism -> EVENT_SET -> EVENT_SET
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermapEventSet mor evs =
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder EventSet _ _ ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- There should be no EventSets (only FQEventSets) as the static
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- analysis should have transformed EventSets into FQEventSets
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder error "CspCASL.Morphism.mapEventSet: Unexpected EventSet"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder FQEventSet fqComms r -> FQEventSet (map (mapCommType mor) fqComms) r
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Apply a signature morphism to an event
9df11f85fd7f8c4745d64464876e84ec4e263692Christian MaedermapEvent :: CspMorphism -> EVENT -> EVENT
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersmapEvent mor e =
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich let mapEvent' = mapEvent mor
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski mapCASLTerm' = mapCASLTerm mor
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder mapChannelName' = mapChannelName mor
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder TermEvent t r ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Just map the morphism over the event (a term)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder TermEvent (mapCASLTerm' t) r
9fa1f3f5e69f1dc502a3c8e448d3a8a88f68c28fChristian Maeder InternalPrefixChoice v s r ->
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- Just map the morphism over the sort, we keep the variable name
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder InternalPrefixChoice v (mapSort' s) r
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ExternalPrefixChoice v s r ->
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- Just map the morphism over the sort, we keep the variable name
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ExternalPrefixChoice v (mapSort' s) r
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ChanSend c t r ->
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- Just map the morphism over the event (a term) and the channel name
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ChanSend (mapChannelName' c) (mapCASLTerm' t) r
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ChanNonDetSend c v s r ->
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- Just map the morphism over the sort and the channel name, we keep
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- the variable name
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ChanNonDetSend (mapChannelName' c) v (mapSort' s) r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ChanRecv c v s r ->
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder -- Just map the morphism over the sort and the channel name, we keep
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder -- the variable name
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder ChanRecv (mapChannelName' c) v (mapSort' s) r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder FQEvent ev mfqc fqTerm r ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- Map the morphism over each part of the FQEvent
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let mfqc' = case mfqc of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- Just preserve nothings
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> Nothing
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (chanName, chanSort) ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- Just map the morphism over the channel name and
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- channel sort
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (mapChannelName' chanName, mapSort' chanSort)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder in FQEvent (mapEvent' ev) mfqc' (mapCASLTerm' fqTerm) r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedermapRenaming :: CspMorphism -> RENAMING -> RENAMING
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedermapRenaming mor re =
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder Renaming _ ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- There should be no (non fully qualified) Renamings (only
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder -- FQRenamings) as the static analysis should have transformed
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder -- EventSets into FQEventSets
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder error "CspCASL.Morphism.mapRenaming: Unexpected Renaming"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder FQRenaming rs -> FQRenaming $ map (mapCASLTerm mor) rs
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- TERM that appears in CspCASL).
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian MaedermapCASLTerm :: CspMorphism -> TERM () -> TERM ()
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedermapCASLTerm mor t =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- The error here is not used. It is a function to map over the morphism,
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke -- CspCASL does not use this functionality.
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik Luecke CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm") mor t
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski-- FORMULA that appears in CspCASL).
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaedermapCASLFormula :: CspMorphism -> FORMULA () -> FORMULA ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermapCASLFormula mor f =
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder -- The error here is not used. It is a function to map over the morphism,
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder -- CspCASL does not use this functionality.
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula") mor f
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich-- | Apply a signature morphism to a channel name
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus LuettichmapChannelName :: CspMorphism -> CHANNEL_NAME -> CHANNEL_NAME
e96a0bf4040fd789339958c01f145c5057d26db6René WagnermapChannelName mor cn =
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich let chanMap = channelMap $ CASL_Morphism.extended_map mor
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich -- Find look up the new channel name, if it does not exist then
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- use the original name.
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Apply a signature morphism to a process name
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedermapProcessName :: CspMorphism -> PROCESS_NAME -> PROCESS_NAME
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermapProcessName mor pn =
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder let procMap = processMap $ CASL_Morphism.extended_map mor
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder -- Find look up the new process name, if it does not exist then
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -- use the original name.