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