SymMapAna.hs revision 2d61745163e6a52a1cf8b838a0e045ca13d4538e
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : symbol map analysis for the CspCASL logic.
76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : portable
76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport qualified Common.Lib.Rel as Rel
d48085f765fca838c1d972d2123601997174583dChristian Maederimport qualified Common.Lib.MapSet as MapSet
d48085f765fca838c1d972d2123601997174583dChristian Maederimport qualified Data.Map as Map
d48085f765fca838c1d972d2123601997174583dChristian Maederimport qualified Data.Set as Set
d48085f765fca838c1d972d2123601997174583dChristian Maederimport Data.List (partition)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maedertype CspRawMap = Map.Map CspRawSymbol CspRawSymbol
a39a820684c1974350f46593025e0bb279f41bc6Christian MaedercspInducedFromToMorphism :: CspRawMap -> ExtSign CspCASLSign CspSymbol
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism
76647324ed70f33b95a881b536d883daccf9568dChristian MaedercspInducedFromToMorphism rmap (ExtSign sSig sy) (ExtSign tSig tSy) =
d48085f765fca838c1d972d2123601997174583dChristian Maeder let (crm, rm) = splitSymbolMap rmap
d48085f765fca838c1d972d2123601997174583dChristian Maeder inducedFromToMorphismExt inducedCspSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder (constMorphExt emptyCspAddMorphism)
d48085f765fca838c1d972d2123601997174583dChristian Maeder composeMorphismExtension isCspSubSign diffCspSig
d48085f765fca838c1d972d2123601997174583dChristian Maeder crm (ExtSign sSig $ getCASLSymbols sy)
d48085f765fca838c1d972d2123601997174583dChristian Maeder $ ExtSign tSig $ getCASLSymbols tSy
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder mor <- cspInducedFromMorphism rmap sSig
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let iSig = mtarget mor
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder if isSubSig isCspSubSign iSig tSig then do
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder incl <- sigInclusion emptyCspAddMorphism iSig tSig
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder composeM composeMorphismExtension mor incl
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ("No signature morphism for csp symbol map found.\n" ++
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder "The following mapped symbols are missing in the target signature:\n"
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ++ showDoc (diffSig diffCspSig iSig tSig) "")
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder $ concatMapRange getRange $ Map.keys rmap
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedercspInducedFromMorphism :: CspRawMap -> CspCASLSign -> Result CspCASLMorphism
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedercspInducedFromMorphism rmap sigma = do
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let (crm, _) = splitSymbolMap rmap
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder m <- inducedFromMorphism emptyCspAddMorphism crm sigma
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let sm = sort_map m
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder om = op_map m
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder pm = pred_map m
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder csig = extendedInfo sigma
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder newSRel = Rel.transClosure . sortRel $ mtarget m
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -- compute the channel name map (as a Map)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder cm <- Map.foldWithKey (chanFun sigma rmap sm)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (return Map.empty) (MapSet.toMap $ chans csig)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -- compute the process name map (as a Map)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder proc_Map <- Map.foldWithKey (procFun sigma rmap sm newSRel cm)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (return Map.empty) (MapSet.toMap $ procSet csig)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let em = emptyCspAddMorphism
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder { channelMap = cm
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder , processMap = proc_Map }
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder return (embedMorphism em sigma $ closeSortRel
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder $ inducedSignAux inducedCspSign sm om pm em sigma)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder { sort_map = sm
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder , op_map = om
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder , pred_map = pm }
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederchanFun :: CspCASLSign -> CspRawMap -> Sort_map -> Id -> Set.Set SORT
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -> Result ChanMap -> Result ChanMap
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederchanFun sig rmap sm cn ss m =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let sls = Rel.partSet (relatedSorts sig) ss
d48085f765fca838c1d972d2123601997174583dChristian Maeder m1 = foldr (directChanMap rmap sm cn) m sls
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder in case (Map.lookup (CspKindedSymb ChannelKind cn) rmap,
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Map.lookup (CspKindedSymb (CaslKind Implicit) cn) rmap) of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Just rsy1, Just rsy2) -> let
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder m2 = Set.fold (insertChanSym sm cn rsy1) m1 ss
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder in Set.fold (insertChanSym sm cn rsy2) m2 ss
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Just rsy, Nothing) ->
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Set.fold (insertChanSym sm cn rsy) m1 ss
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Nothing, Just rsy) ->
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Set.fold (insertChanSym sm cn rsy) m1 ss
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- Anything not mapped explicitly is left unchanged
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (Nothing, Nothing) -> m1
d48085f765fca838c1d972d2123601997174583dChristian MaederdirectChanMap :: CspRawMap -> Sort_map -> Id -> Set.Set SORT
d48085f765fca838c1d972d2123601997174583dChristian Maeder -> Result ChanMap -> Result ChanMap
d48085f765fca838c1d972d2123601997174583dChristian MaederdirectChanMap rmap sm cn ss m =
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder rl = map (\ s -> Map.lookup (ACspSymbol $ toChanSymbol (cn, s)) rmap) sl
d48085f765fca838c1d972d2123601997174583dChristian Maeder (ms, ps) = partition (isJust . fst) $ zip rl sl
d48085f765fca838c1d972d2123601997174583dChristian Maeder in case ms of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder l@((Just rsy, _) : rs) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder foldr (\ (_, s) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder insertChanSym sm cn
d48085f765fca838c1d972d2123601997174583dChristian Maeder (ACspSymbol $ toChanSymbol
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (rawId rsy, mapSort sm s)) s)
d48085f765fca838c1d972d2123601997174583dChristian Maeder (foldr (\ (rsy2, s) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder insertChanSym sm cn (fromJust rsy2) s) m l)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederinsertChanSym :: Sort_map -> Id -> CspRawSymbol -> SORT -> Result ChanMap
d48085f765fca838c1d972d2123601997174583dChristian Maeder -> Result ChanMap
d48085f765fca838c1d972d2123601997174583dChristian MaederinsertChanSym sm cn rsy s m = do
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder c1 <- mappedChanSym sm cn s rsy
d48085f765fca838c1d972d2123601997174583dChristian Maeder let ptsy = CspSymbol cn $ ChanAsItemType s
d48085f765fca838c1d972d2123601997174583dChristian Maeder pos = getRange rsy
d48085f765fca838c1d972d2123601997174583dChristian Maeder m2 = Map.insert (cn, s) c1 m1
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder case Map.lookup (cn, s) m1 of
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Nothing -> if cn == c1 then
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder ACspSymbol _ -> return m1
d48085f765fca838c1d972d2123601997174583dChristian Maeder _ -> hint m1 ("identity mapping of "
d48085f765fca838c1d972d2123601997174583dChristian Maeder ++ showDoc ptsy "") pos
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder else return m2
d48085f765fca838c1d972d2123601997174583dChristian Maeder Just c2 -> if c1 == c2 then
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder ("ignoring duplicate mapping of " ++ showDoc ptsy "") pos
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder else plain_error m1
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder ("conflicting mapping of " ++ showDoc ptsy " to " ++
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder show c1 ++ " and " ++ show c2) pos
76647324ed70f33b95a881b536d883daccf9568dChristian MaedermappedChanSym :: Sort_map -> Id -> SORT -> CspRawSymbol -> Result Id
d48085f765fca838c1d972d2123601997174583dChristian MaedermappedChanSym sm cn s rsy =
d48085f765fca838c1d972d2123601997174583dChristian Maeder let chanSym = "channel symbol " ++ showDoc (toChanSymbol (cn, s))
d48085f765fca838c1d972d2123601997174583dChristian Maeder " is mapped to "
d48085f765fca838c1d972d2123601997174583dChristian Maeder in case rsy of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ACspSymbol (CspSymbol ide (ChanAsItemType s1)) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder let s2 = mapSort sm s
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder in if s1 == s2
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder then return ide
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder else plain_error cn
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (chanSym ++ "sort " ++ showDoc s1
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder " but should be mapped to type " ++
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder showDoc s2 "") $ getRange rsy
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder CspKindedSymb k ide | elem k [CaslKind Implicit, ChannelKind] ->
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder _ -> plain_error cn
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (chanSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder $ getRange rsy
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprocFun :: CspCASLSign -> CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap -> Id
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprocFun sig rmap sm rel cm pn ps m =
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder let pls = Rel.partSet (relatedProcs sig) ps
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder m1 = foldr (directProcMap rmap sm rel cm pn) m pls
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- now try the remaining ones with (un)kinded raw symbol
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder in case (Map.lookup (CspKindedSymb ProcessKind pn) rmap,
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Map.lookup (CspKindedSymb (CaslKind Implicit) pn) rmap) of
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder (Just rsy1, Just rsy2) -> let
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder m2 = Set.fold (insertProcSym sm rel cm pn rsy1) m1 ps
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder in Set.fold (insertProcSym sm rel cm pn rsy2) m2 ps
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (Just rsy, Nothing) ->
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder Set.fold (insertProcSym sm rel cm pn rsy) m1 ps
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder (Nothing, Just rsy) ->
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Set.fold (insertProcSym sm rel cm pn rsy) m1 ps
d48085f765fca838c1d972d2123601997174583dChristian Maeder -- Anything not mapped explicitly is left unchanged
d48085f765fca838c1d972d2123601997174583dChristian Maeder (Nothing, Nothing) -> m1
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederdirectProcMap :: CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder -> Id -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederdirectProcMap rmap sm rel cm pn ps m =
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder rl = map (lookupProcSymbol rmap pn) pl
d48085f765fca838c1d972d2123601997174583dChristian Maeder (ms, os) = partition (isJust . fst) $ zip rl pl
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder in case ms of
d48085f765fca838c1d972d2123601997174583dChristian Maeder l@((Just rsy, _) : rs) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder foldr (\ (_, p) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder insertProcSym sm rel cm pn
d48085f765fca838c1d972d2123601997174583dChristian Maeder (ACspSymbol $ toProcSymbol
d48085f765fca838c1d972d2123601997174583dChristian Maeder (rawId rsy, mapProcProfile sm cm p)) p)
d48085f765fca838c1d972d2123601997174583dChristian Maeder (foldr (\ (rsy2, p) ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder insertProcSym sm rel cm pn (fromJust rsy2) p) m l)
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederlookupProcSymbol :: CspRawMap -> Id -> ProcProfile
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder -> Maybe CspRawSymbol
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederlookupProcSymbol rmap pn p = case
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder filter (\ (k, _) -> case k of
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ACspSymbol (CspSymbol i (ProcAsItemType pf)) ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder i == pn && matchProcTypes p pf
d48085f765fca838c1d972d2123601997174583dChristian Maeder _ -> False) $ Map.toList rmap of
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder [(_, r)] -> Just r
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder [] -> Nothing
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder -- in case of ambiguities try to find an exact match
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder l -> lookup (ACspSymbol $ toProcSymbol (pn, p)) l
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederinsertProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id -> CspRawSymbol
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -> ProcProfile -> Result ProcessMap -> Result ProcessMap
76647324ed70f33b95a881b536d883daccf9568dChristian MaederinsertProcSym sm rel cm pn rsy pf@(ProcProfile _ al) m = do
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (p1, al1) <- mappedProcSym sm rel cm pn pf rsy
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let otsy = toProcSymbol (pn, pf)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder pos = getRange rsy
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder m2 = Map.insert (pn, pf) (p1, al1) m1
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case Map.lookup (pn, pf) m1 of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Nothing -> if pn == p1 && al == al1 then
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ACspSymbol _ -> return m1
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder _ -> hint m1 ("identity mapping of "
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ++ showDoc otsy "") pos
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder else return m2
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder Just (p2, al2) -> if p1 == p2 then
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder warning (if al1 /= al2 then m2 else m1)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ("ignoring duplicate mapping of " ++ showDoc otsy "")
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder else plain_error m1
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ("conflicting mapping of " ++ showDoc otsy " to " ++
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder show p1 ++ " and " ++ show p2) pos
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaedermappedProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder -> ProcProfile -> CspRawSymbol -> Result (Id, CommAlpha)
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian MaedermappedProcSym sm rel cm pn pfSrc rsy =
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder let procSym = "process symbol " ++ showDoc (toProcSymbol (pn, pfSrc))
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder " is mapped to "
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder pfMapped@(ProcProfile _ al2) = reduceProcProfile rel
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder $ mapProcProfile sm cm pfSrc
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder in case rsy of
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder ACspSymbol (CspSymbol ide (ProcAsItemType pf)) ->
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder let pfTar@(ProcProfile _ al1) = reduceProcProfile rel pf
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder in if compatibleProcTypes rel pfMapped pfTar
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder then return (ide, al1)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder else plain_error (pn, al2)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder (procSym ++ "type " ++ showDoc pfTar
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder "\nbut should be mapped to type " ++
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder showDoc pfMapped
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder "\npossibly using a sub-alphabet of " ++ showDoc al2 ".")
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder $ getRange rsy
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder CspKindedSymb k ide | elem k [CaslKind Implicit, ProcessKind] ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return (ide, al2)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder _ -> plain_error (pn, al2)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (procSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder $ getRange rsy
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedercompatibleProcTypes :: Rel.Rel SORT -> ProcProfile -> ProcProfile -> Bool
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedercompatibleProcTypes rel (ProcProfile l1 al1) (ProcProfile l2 al2) =
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder l1 == l2 && liamsRelatedCommAlpha rel al1 al2
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederliamsRelatedCommAlpha :: Rel.Rel SORT -> CommAlpha -> CommAlpha -> Bool
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederliamsRelatedCommAlpha rel al1 al2 =
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder all (\ a2 -> any (\a1 -> liamsRelatedCommTypes rel a1 a2) $ Set.toList al1)
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederliamsRelatedCommTypes :: Rel.Rel SORT -> CommType -> CommType -> Bool
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederliamsRelatedCommTypes rel ct1 ct2 = case (ct1, ct2) of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (CommTypeSort s1, CommTypeSort s2)
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder -> s1 == s2 || s1 `Set.member` Rel.succs rel s2
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder (CommTypeChan (TypedChanName c1 s1), CommTypeChan (TypedChanName c2 s2))
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder -> c1 == c2 && s1 == s2
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermatchProcTypes :: ProcProfile -> ProcProfile -> Bool
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermatchProcTypes (ProcProfile l1 al1) (ProcProfile l2 al2) = l1 == l2
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder && (Set.null al2 || Set.null al1 || not (Set.null $ Set.intersection al1 al2))
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedercspMatches :: CspSymbol -> CspRawSymbol -> Bool
76647324ed70f33b95a881b536d883daccf9568dChristian MaedercspMatches (CspSymbol i t) rsy = case rsy of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ACspSymbol (CspSymbol j t2) -> i == j && case (t, t2) of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (CaslSymbType t1, CaslSymbType t3) -> matches (Symbol i t1)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder $ ASymbol $ Symbol j t3
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (ChanAsItemType s1, ChanAsItemType s2) -> s1 == s2
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (ProcAsItemType p1, ProcAsItemType p2) -> matchProcTypes p1 p2
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder CspKindedSymb k j -> let res = i == j in case (k, t) of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (CaslKind ck, CaslSymbType t1) -> matches (Symbol i t1)
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder $ AKindedSymb ck j
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder (ChannelKind, ChanAsItemType _) -> res
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder (ProcessKind, ProcAsItemType _) -> res
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder (CaslKind Implicit, _) -> res
19f104861f1832b452c9f98e59880d05e865d9bdChristian MaederprocProfile2Sorts :: ProcProfile -> Set.Set SORT
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprocProfile2Sorts (ProcProfile sorts al) =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Set.union (Set.fromList sorts) $ Set.map commType2Sort al
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedercspRevealSym :: CspSymbol -> CspCASLSign -> CspCASLSign
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspRevealSym sy sig = let
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder n = cspSymName sy
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder r = sortRel sig
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ext = extendedInfo sig
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder cs = chans ext
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in case cspSymbType sy of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder CaslSymbType t -> revealSym (Symbol n t) sig
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ChanAsItemType s -> sig
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder , extendedInfo = ext { chans = MapSet.insert n s cs }}
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ProcAsItemType p@(ProcProfile _ al) -> sig
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder { sortRel = Rel.union (Rel.fromKeysSet $ procProfile2Sorts p) r
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , extendedInfo = ext
d1012ae182d765c4e6986029d210b9e7b48de205Christian Maeder { chans = Set.fold (\ ct -> case ct of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder CommTypeSort _ -> id
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder CommTypeChan (TypedChanName c s) -> MapSet.insert c s) cs al
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , procSet = MapSet.insert n p $ procSet ext }
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedercspGeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedercspGeneratedSign sys sigma = let
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder symset = Set.unions $ symSets sigma
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder sigma1 = Set.fold cspRevealSym sigma
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , extendedInfo = emptyCspSign } sys
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder sigma2 = sigma1
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder { sortRel = sortRel sigma `Rel.restrict` sortSet sigma1
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder in if not $ Set.isSubsetOf sys symset
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski then let diffsyms = sys Set.\\ symset in
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder fatal_error ("Revealing: The following symbols "
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ++ showDoc diffsyms " are not in the signature")
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder $ getRange diffsyms
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder else cspSubsigInclusion sigma2 sigma
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercspCogeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercspCogeneratedSign symset sigma = let
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder symset0 = Set.unions $ symSets sigma
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder symset1 = Set.fold cspHideSym symset0 symset
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder in if Set.isSubsetOf symset symset0
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder then cspGeneratedSign symset1 sigma
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder else let diffsyms = symset Set.\\ symset0 in
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder fatal_error ("Hiding: The following symbols "
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ++ showDoc diffsyms " are not in the signature")
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder $ getRange diffsyms
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian MaedercspHideSym :: CspSymbol -> Set.Set CspSymbol -> Set.Set CspSymbol
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedercspHideSym sy set1 = let
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder n = cspSymName sy
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder in case cspSymbType sy of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder CaslSymbType SortAsItemType ->
94b34b35075c9115a22b512fd4ec3fb290f13d59Christian Maeder Set.filter (not . cspProfileContains n . cspSymbType) set2
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ChanAsItemType s ->
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder Set.filter (unusedChan n s) set2
76647324ed70f33b95a881b536d883daccf9568dChristian MaedercspProfileContains :: Id -> CspSymbType -> Bool
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedercspProfileContains s ty = case ty of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder CaslSymbType t -> profileContainsSort s t
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder ChanAsItemType s2 -> s == s2
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder ProcAsItemType p -> Set.member s $ procProfile2Sorts p
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederunusedChan :: Id -> SORT -> CspSymbol -> Bool
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederunusedChan c s sy = case cspSymbType sy of
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder ProcAsItemType (ProcProfile _ al) ->
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder Set.fold (\ ct b -> case ct of
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder CommTypeSort _ -> b
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder CommTypeChan (TypedChanName c2 s2) -> b && (c, s) /= (c2, s2)) True al