Morphism.hs revision 431571057e88a650a974adec93ea4bb5173b6213
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce{-# LANGUAGE MultiParamTypeClasses #-}
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceModule : $Header$
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceDescription : Symbols and signature morphisms for the CspCASL logic
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceLicense : GPLv2 or higher, see LICENSE.txt
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceMaintainer : csliam@swansea.ac.uk
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceStability : provisional
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcePortability : portable
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceSymbols and signature morphisms for the CspCASL logic
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce ( CspCASLMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , CspAddMorphism (..)
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , ProcessMap
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , mapProcProfile
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , cspSubsigInclusion
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek , emptyCspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , cspAddMorphismUnion
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , cspMorphismToCspSymbMap
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , inducedCspSign
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport qualified CspCASL.LocalTop as LT
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..))
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport CASL.Sign as CASL_Sign
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport CASL.Morphism as CASL_Morphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport qualified CASL.MapSentence as CASL_MapSen
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport Common.Utils (composeMap, isSingleton)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport qualified Common.Lib.MapSet as MapSet
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport qualified Common.Lib.Rel as Rel
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinaimport qualified Data.Map as Map
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekimport qualified Data.Set as Set
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce{- | This is the second component of a CspCASL signature morphism, the process
b011330c77168cdd864aaae54a75214935136c05Pavel Reichlname map. We map process name with a profile into new names and
b011330c77168cdd864aaae54a75214935136c05Pavel Reichlcommunications alphabet. We follow CASL here and instread of mapping to a new
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinaname and a new profile, we map just to the new name and the new
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovcommunications alphabet of the profile. This is because the argument sorts of
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovthe profile have no chocie they have to be the sorts resultsing from maping
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinathe original sorts in the profile with the data part map. Note: the
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinacommunications alphabet of the source profile must be downward closed with
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinarespect to the CASL signature sub-sort relation (at source) and also the
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinatarget communications alphabet must be downward closed with respect to the
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinaCASL signature sub-sort relation (at target). -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozektype ProcessMap =
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov Map.Map (PROCESS_NAME, ProcProfile) (PROCESS_NAME, CommAlpha)
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorcetype ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce-- | CspAddMorphism - This is just the extended part
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorcedata CspAddMorphism = CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce {- Note that when applying the CspAddMorphism to process names or channel
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce names, if the name is not in the map in the morphism, then the
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce application is the identity function. Thus empty maps are used to form
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce the empty morphism and the identity morphism. -}
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce { channelMap :: ChanMap
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , processMap :: ProcessMap
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce } deriving (Eq, Ord, Show)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | The empty CspAddMorphism.
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovemptyCspAddMorphism :: CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceemptyCspAddMorphism = CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce {- Note that when applying the CspAddMorphism to process names or
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce channel names, if the name is not in the map in the morphism,
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce then the application is the identity function. Thus empty maps
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce are used to form the empty morphism. -}
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce { channelMap = Map.empty
b011330c77168cdd864aaae54a75214935136c05Pavel Reichl , processMap = Map.empty
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov{- | Given two signatures (the first being a sub signature of the second
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovaccording to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinacspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinacspSubsigInclusion sign = checkResultMorphismIsLegal .
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina CASL_Morphism.sigInclusion emptyCspAddMorphism sign
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina{- We use the empty morphism as it also represents the identity, thus this
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březinawill embed channel names and process names properly. -}
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovcheckResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovcheckResultMorphismIsLegal rmor = do
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce legalMorphismExtension mor
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce-- | lookup a typed channel
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a signature morphism to a channel name
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce -> (CHANNEL_NAME, SORT)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor
8e195a545d41647e591c1d06082133cbd25dc0a4Jakub HrozekmapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapCommTypeAux sm cm ct = case ct of
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina CommTypeSort s -> CommTypeSort $ mapSort sm s
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek CommTypeChan (TypedChanName c s) -> let (d, t) = mapChan sm cm (c, s) in
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek CommTypeChan $ TypedChanName d t
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce-- | Apply a signature morphism to a CommType
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapCommAlphaAux sm = Set.map . mapCommTypeAux sm
b011330c77168cdd864aaae54a75214935136c05Pavel Reichl-- | Apply a signature morphism to a CommAlpha
b011330c77168cdd864aaae54a75214935136c05Pavel ReichlmapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinamapCommAlpha = Set.map . mapCommType
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovmapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinamapProcProfile sm cm (ProcProfile sl cs) =
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina ProcProfile (map (mapSort sm) sl) $ mapCommAlphaAux sm cm cs
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapProcId :: Sort_map -> ChanMap -> ProcessMap
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
a0d010f488bf15fb3e170ce04092013fa494401fPavel BřezinamapProcId sm cm pm (i, p) = let
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce n@(ProcProfile args _) = mapProcProfile sm cm p
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce in case Map.lookup (i, p) pm of
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce Nothing -> (i, n)
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce Just (j, alpha) -> (j, ProcProfile args alpha)
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapProcess :: Morphism f CspSign CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcemapProcess mor = let em = extended_map mor in
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce mapProcId (sort_map mor) (channelMap em) $ processMap em
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- | Compose two CspAddMorphisms
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovcomposeCspAddMorphism :: Morphism f CspSign CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo SorcecomposeCspAddMorphism m1 m2 = let
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce sMap1 = sort_map m1
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce sMap2 = sort_map m2
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce src = msource m1
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce cSrc = extendedInfo src
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce cMap = MapSet.foldWithKey ( \ c s ->
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce let p = (c, s)
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce ni = fst $ mapChannel m2 $ mapChannel m1 p
b011330c77168cdd864aaae54a75214935136c05Pavel Reichl in if c == ni then id else Map.insert p ni)
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov let pp = (p, pr)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (ni, ProcProfile _ na) =
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina mapProcess m2 $ mapProcess m1 pp
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina oa = mapCommAlphaAux sMap cMap a
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina in if p == ni && oa == na then id else
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina Map.empty $ procSet cSrc
a0d010f488bf15fb3e170ce04092013fa494401fPavel Březina in return emptyCspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce { channelMap = cMap
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce , processMap = pMap }
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce{- | A CspCASLMorphism is a CASL Morphism with the extended_map to be a
225d845476b6136be9b77f528ed986bba7a7f732Simo SorceCspAddMorphism. -}
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorcetype CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce{- | Check if a CspCASL signature morphism has the refl property i.e.,
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorcesigma(s1) <= sigma(s2) implies s1 <= s2 for all s1, s2 in S -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcheckReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovcheckReflCondition mor =
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov let sig = msource mor
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce sig' = mtarget mor
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce sm = sort_map mor
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce rel = sortRel sig
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce rel' = sortRel sig'
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce allPairs = LT.cartesian $ sortSet sig
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce failures = Set.filter (not . test) allPairs
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek test (s1, s2) = if Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapSort sm s1 == mapSort sm s2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek then Rel.path s1 s2 rel || s1 == s2
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina in if Set.null failures
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek then return ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek else let produceDiag (s1, s2) =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let x = (mapSort sm s1)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek y = (mapSort sm s2)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in Diag Error
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ("CSP-CASL Signature Morphism Refl Property Violated:\n'"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ showDoc (Symbol x $ SubsortAsItemType y)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek "' in target but not in source\n'"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ showDoc (Symbol s1 $ SubsortAsItemType s2) "'")
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek allDiags = map produceDiag $ Set.toList failures
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in Result allDiags Nothing -- failure with error messages
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina{- | Check if a CspCASL signature morphism has the weak non extension property
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozeksigma(s1) <= u' and sigma(s2) <= u' implies there exists t in S with
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozeks1 <= t and s2 <= t and sigma(t) <= u' for all s1,s2 in S and u' in S' -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcheckWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcheckWNECondition mor =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let sig = msource mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek sig' = mtarget mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek sm = sort_map mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek rel' = sortRel sig'
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek supers s signature = Set.insert s $ supersortsOf s signature
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek allPairsInSource = LT.cartesian $ sortSet sig
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek commonSuperSortsInTarget s1 s2 = Set.intersection
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina (supers (mapSort sm s1) sig')
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (supers (mapSort sm s2) sig')
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- Candidates are triples (s1,s2,u') such that
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek \sigma(s1),\sigma(s2) < u' -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek createCandidateTripples (s1, s2) =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek allCandidateTripples =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Set.unions $ Set.toList $ Set.map createCandidateTripples
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov allPairsInSource
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek testCandidate (s1, s2, u') =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in or $ Set.toList $ Set.map test possibleWitnesses
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov failures = Set.filter (not . testCandidate) allCandidateTripples
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek then return ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek else let produceDiag (s1, s2, u') =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let x = (mapSort sm s1)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek y = (mapSort sm s2)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in Diag Error
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ("CSP-CASL Signature Morphism Weak Non-Extension Property "
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ "Violated:\n'"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (Subsort_decl [x, y] u' nullRange :: SORT_ITEM ())
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek "' in target\nbut no common supersort for the sorts\n'"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (Sort_decl [s1, s2] nullRange :: SORT_ITEM ())
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek "' in source")
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina allDiags = map produceDiag $ Set.toList failures
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in Result allDiags Nothing -- failure with error messages
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | unite morphisms
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -> Result CspAddMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspAddMorphismUnion mor1 mor2 = let
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek s1 = extendedInfo $ msource mor1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek s2 = extendedInfo $ msource mor2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek m1 = extended_map mor1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek m2 = extended_map mor2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek chan1 = channelMap m1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek chan2 = channelMap m2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek delChan (n, s) m = MapSet.delete n s m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek uc1 = foldr delChan (chans s1) $ Map.keys chan1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek uc2 = foldr delChan (chans s2) $ Map.keys chan2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek proc1 = processMap m1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek proc2 = processMap m2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek delProc (n, p) m = MapSet.delete n p m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek up1 = foldr delProc (procSet s1) $ Map.keys proc1
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek up2 = foldr delProc (procSet s2) $ Map.keys proc2
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek showAlpha (i, s) l = shows i (if null l then "" else "(..)") ++ ":"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ if isSingleton s then showDoc (Set.findMin s) "" else showDoc s ""
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (cds, cMap) = foldr ( \ (isc@(i, s), j) (ds, m) ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Nothing -> (ds, Map.insert isc j m)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Just k -> if j == k then (ds, m) else
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ("incompatible mapping of channel " ++ shows i ":"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ showDoc s " to " ++ shows j " and "
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ shows k "") nullRange : ds, m)) ([], chan1)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (Map.toList chan2 ++ concatMap ( \ (c, ts) -> map
4c08db0fb0dda3d27b1184248ca5c800d7ce23f0Michal Zidek ( \ s -> ((c, s), c)) ts) (MapSet.toList uc))
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (pds, pMap) =
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina foldr ( \ (isc@(i, pt@(ProcProfile args _)), j) (ds, m) ->
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina Nothing -> (ds, Map.insert isc j m)
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina Just k -> if j == k then (ds, m) else
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ("incompatible mapping of process " ++ shows i " "
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ++ showDoc pt " to " ++ showAlpha j args ++ " and "
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ++ showAlpha k args) nullRange : ds, m)) (cds, proc1)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (Map.toList proc2 ++ concatMap ( \ (p, pts) -> map
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ( \ pt@(ProcProfile _ al) -> ((p, pt), (p, al))) pts)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in if null pds then return emptyCspAddMorphism
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov { channelMap = cMap
18f01e63c1968c29bddb9e48c279b583c0444730Jakub Hrozek , processMap = pMap }
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek else Result pds Nothing
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozektoCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -> Map.Map CspSymbol CspSymbol
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovtoCspSymbMap b mor = let
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek src = extendedInfo $ msource mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ( \ i t -> let
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek q@(j, _) = mapChannel mor p
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in if b && i == j then id else
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Map.insert (toChanSymbol p) $ toChanSymbol q)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ( \ i t@(ProcProfile _ al) -> let
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek al1 = mapCommAlpha mor al
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek q@(j, ProcProfile _ al2) = mapProcess mor p
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in if b && i == j && al1 == al2 then id else
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Map.insert (toProcSymbol p) $ toProcSymbol q)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in Map.union chanSymMap procSymMap
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspMorphismToCspSymbMap mor =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek . map (\ (a, b) -> (caslToCspSymbol a, caslToCspSymbol b))
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek $ Map.toList $ morphismToSymbMap mor)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov $ toCspSymbMap False mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Instance for CspCASL signature extension
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekinstance SignExtension CspSign where
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek isSubSignExtension = isCspSubSign
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | a dummy instances used for the default definition
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovinstance Pretty CspAddMorphism where
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov pretty m = pretty $ toCspSymbMap False
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek $ embedMorphism m emptyCspCASLSign emptyCspCASLSign
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Instance for CspCASL morphism extension (used for Category)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozekinstance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ideMorphismExtension _ = emptyCspAddMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek composeMorphismExtension = composeCspAddMorphism
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov -- we omit inverses here
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek isInclusionMorphismExtension m =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Map.null (channelMap m) && Map.null (processMap m)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -- pretty printing for Csp morphisms
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek prettyMorphismExtension = printMap id sepByCommas pairElems
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek . toCspSymbMap True
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek legalMorphismExtension m = do
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek checkReflCondition m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek checkWNECondition m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- * induced signature extension
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekinducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekinducedChanMap sm cm = MapSet.foldWithKey
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let (j, t) = mapChan sm cm (i, s)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekinducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -> ProcNameMap
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekinducedProcMap sm cm pm = MapSet.foldWithKey
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina let (m, q) = mapProcId sm cm pm (n, p)
115241b0eeedd033d34d9721a896f031140944d7Pavel BřezinainducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign
115241b0eeedd033d34d9721a896f031140944d7Pavel BřezinainducedCspSign sm _ _ m sig =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let csig = extendedInfo sig
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek cm = channelMap m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in emptyCspSign
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina { chans = inducedChanMap sm cm $ chans csig
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek , procSet = inducedProcMap sm cm (processMap m) $ procSet csig }
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina-- * application of morphisms to sentences
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a Signature Morphism to a CspCASL Sentence
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapSen :: CspCASLMorphism -> CspSen -> CspSen
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapSen mor sen =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek else case sen of
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek ProcessEq procName fqVarList commAlpha proc ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let {- Map the morphism over all the parts of the process
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek newProcName = mapProcessName mor procName
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek newFqVarList = mapFQProcVarList mor fqVarList
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek newCommAlpha = mapCommAlpha mor commAlpha
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek newProc = mapProc mor proc
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in ProcessEq newProcName newFqVarList
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek newCommAlpha newProc
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a signature morphism to a Fully Qualified Process Variable List
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapFQProcVarList mor =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -- As these are terms, just map the morphism over CASL TERMs
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek map (mapCASLTerm mor)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a signature morphism to a process
115241b0eeedd033d34d9721a896f031140944d7Pavel BřezinamapProc :: CspCASLMorphism -> PROCESS -> PROCESS
115241b0eeedd033d34d9721a896f031140944d7Pavel BřezinamapProc mor proc =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let mapProc' = mapProc mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapProcessName' = mapProcessName mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapEvent' = mapEvent mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapEventSet' = mapEventSet mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapRenaming' = mapRenaming mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapCommAlpha' = mapCommAlpha mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapCASLTerm' = mapCASLTerm mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapCASLFormula' = mapCASLFormula mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in case proc of
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Skip r -> Skip r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Stop r -> Stop r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Div r -> Div r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Run es r -> Run (mapEventSet' es) r
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov Chaos ev r -> Chaos (mapEventSet' ev) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek PrefixProcess e p r ->
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina PrefixProcess (mapEvent' e) (mapProc' p) r
b011330c77168cdd864aaae54a75214935136c05Pavel Reichl Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina SynchronousParallel p q r ->
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina SynchronousParallel (mapProc' p) (mapProc' q) r
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina GeneralisedParallel p es q r ->
4c08db0fb0dda3d27b1184248ca5c800d7ce23f0Michal Zidek GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r
4c08db0fb0dda3d27b1184248ca5c800d7ce23f0Michal Zidek AlphabetisedParallel p les res q r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek AlphabetisedParallel (mapProc' p) (mapEventSet' les)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (mapEventSet' res) (mapProc' q) r
18f01e63c1968c29bddb9e48c279b583c0444730Jakub Hrozek Hiding p es r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Hiding (mapProc' p) (mapEventSet' es) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek RenamingProcess p re r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek RenamingProcess (mapProc' p) (mapRenaming' re) r
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ConditionalProcess f p q r ->
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ConditionalProcess (mapCASLFormula' f)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek (mapProc' p) (mapProc' q) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek NamedProcess pn fqParams r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r
d115f40c7a3999e3cbe705a2ff9cf0fd493f80fbMichal Zidek FQProcess p commAlpha r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a signature morphism to an event set
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapEventSet mor (EventSet fqComms r) =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek EventSet (map (mapCommType mor) fqComms) r
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- | Apply a signature morphism to an event
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovmapEvent :: CspCASLMorphism -> EVENT -> EVENT
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapEvent mor e =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let mapEvent' = mapEvent mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapCASLTerm' = mapCASLTerm mor
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina mapChannelName' = mapChannel mor
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -- Just map the morphism over the event (a term)
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQTermEvent t r -> FQTermEvent (mapCASLTerm' t) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- Just map the morphism over the variable, this just maps the sort and
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek keep the same name -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQExternalPrefixChoice v r -> FQExternalPrefixChoice (mapCASLTerm' v) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- Just map the morphism over the variable, this just maps the sort and
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek keep the same name -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQInternalPrefixChoice v r -> FQInternalPrefixChoice (mapCASLTerm' v) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek -- Just map the morphism over the event (a term) and the channel name
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanSend (c, s) t r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanSend (mapChannelName' (c, s)) (mapCASLTerm' t) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- Just map the morphism over the sort and the channel name, we keep
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek the variable name -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanNonDetSend (c, s) v r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanNonDetSend (mapChannelName' (c, s)) (mapCASLTerm' v) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- Just map the morphism over the sort and the channel name, we keep
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek the variable name -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanRecv (c, s) v r ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQChanRecv (mapChannelName' (c, s)) (mapCASLTerm' v) r
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek _ -> error "CspCASL.Morphism.mapEvent: Cannot map unqualified event"
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapRenaming mor re =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek Renaming _ ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- There should be no (non fully qualified) Renamings (only
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQRenamings) as the static analysis should have transformed
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek EventSets into FQEventSets -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek error "CspCASL.Morphism.mapRenaming: Unexpected non fully \
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek \qualified renaming"
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina FQRenaming rs -> FQRenaming $ map (mapCASLTerm mor) rs
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekcspCASLMorphism2caslMorphism m =
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov m { msource = ccSig2CASLSign $ msource m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek , mtarget = ccSig2CASLSign $ mtarget m
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek , extended_map = () }
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovTERM that appears in CspCASL). -}
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovmapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapCASLTerm =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- The error here is not used. It is a function to map over the morphism,
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina CspCASL does not use this functionality. -}
115241b0eeedd033d34d9721a896f031140944d7Pavel Březina CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm")
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek . cspCASLMorphism2caslMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekFORMULA that appears in CspCASL). -}
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapCASLFormula =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek {- The error here is not used. It is a function to map over the morphism,
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce CspCASL does not use this functionality. -}
225d845476b6136be9b77f528ed986bba7a7f732Simo Sorce CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula")
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek . cspCASLMorphism2caslMorphism
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek-- | Apply a signature morphism to a process name
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub HrozekmapProcessName mor pn = case pn of
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek FQ_PROCESS_NAME pn' procProfilePn' ->
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek let (m, procProfileM) =
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek mapProcess mor (pn', procProfilePn')
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek in FQ_PROCESS_NAME m procProfileM
c0bca1722d6f9dfb654ad78397be70f79ff39af1Jakub Hrozek _ -> error "unqualifed FQ_PROCESS_NAME"