Morphism.hs revision 50c62c8c45643f09bcb2f4a99b07bf1d072ecf40
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-# LANGUAGE MultiParamTypeClasses #-}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : Symbols and signature morphisms for the CspCASL logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : csliam@swansea.ac.uk
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : portable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederSymbols and signature morphisms for the CspCASL logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ( CspCASLMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , CspAddMorphism (..)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , mapProcProfile
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , cspSubsigInclusion
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , emptyCspAddMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , cspAddMorphismUnion
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , cspMorphismToCspSymbMap
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , inducedCspSign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified CspCASL.LocalTop as LT
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..), OpKind (..))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CASL.Sign as CASL_Sign
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CASL.Morphism as CASL_Morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified CASL.MapSentence as CASL_MapSen
import Common.Utils (composeMap, isSingleton)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import qualified Data.Map as Map
import qualified Data.Set as Set
Map.Map (PROCESS_NAME, ProcProfile) (PROCESS_NAME, CommAlpha)
type ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME
{ channelMap = Map.empty
, processMap = Map.empty
according to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}
CASL_Morphism.sigInclusion emptyCspAddMorphism sign
mapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)
mapCommAlphaAux sm = Set.map . mapCommTypeAux sm
mapCommAlpha = Set.map . mapCommType
in case Map.lookup (i, p) pm of
sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2
cMap = MapSet.foldWithKey ( \ c s ->
in if c == ni then id else Map.insert p ni)
Map.empty $ chans cSrc
pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->
Map.insert pp (ni, na))
Map.empty $ procSet cSrc
type CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism
{- | Check if a CspCASL signature morphism has the refl property i.e.,
allPairs = LT.cartesian $ sortSet sig
failures = Set.filter (not . test) allPairs
test (s1, s2) = if Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||
then Rel.path s1 s2 rel || s1 == s2
in if Set.null failures
allDiags = map produceDiag $ Set.toList failures
i.e.,
supers s signature = Set.insert s $ supersortsOf s signature
allPairsInSource = LT.cartesian $ sortSet sig
commonSuperSortsInTarget s1 s2 = Set.intersection
Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)
let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)
test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'
failures = Set.filter (not . testCandidate) allCandidateTripples
in if Set.null failures
allDiags = map produceDiag $ Set.toList failures
delChan (n, s) m = MapSet.delete n s m
uc1 = foldr delChan (chans s1) $ Map.keys chan1
uc2 = foldr delChan (chans s2) $ Map.keys chan2
uc = MapSet.union uc1 uc2
delProc (n, p) m = MapSet.delete n p m
up1 = foldr delProc (procSet s1) $ Map.keys proc1
up2 = foldr delProc (procSet s2) $ Map.keys proc2
up = MapSet.union up1 up2
++ if isSingleton s then showDoc (Set.findMin s) "" else showDoc s ""
case Map.lookup isc m of
Nothing -> (ds, Map.insert isc j m)
(Map.toList chan2 ++ concatMap ( \ (c, ts) -> map
( \ s -> ((c, s), c)) ts) (MapSet.toList uc))
case Map.lookup isc m of
Nothing -> (ds, Map.insert isc j m)
(Map.toList proc2 ++ concatMap ( \ (p, pts) -> map
(MapSet.toList up))
-> Map.Map CspSymbol CspSymbol
chanSymMap = MapSet.foldWithKey
Map.insert (toChanSymbol p) $ toChanSymbol q)
Map.empty $ chans src
procSymMap = MapSet.foldWithKey
Map.insert (toProcSymbol p) $ toProcSymbol q)
Map.empty $ procSet src
in Map.union chanSymMap procSymMap
cspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol
$ Map.toList $ morphismToSymbMap mor)
instance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
inducedChanMap sm cm = MapSet.foldWithKey
inducedProcMap sm cm pm = MapSet.foldWithKey
mapSort' = CASL_MapSen.mapSrt mor
_ -> error "CspCASL.Morphism.mapEvent: Cannot map unqualified event"
{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL