SymMapAna.hs revision aa4d26536fffe0153cd81d28925985892ac2f300
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : symbol map analysis for the CspCASL logic.
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) Christian Maeder, DFKI GmbH 2011
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : Christian.Maeder@dfki.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Rel as Rel
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.MapSet as MapSet
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport qualified Data.Map as Map
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified Data.Set as Set
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Data.List (partition)
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimbletttype CspRawMap = Map.Map CspRawSymbol CspRawSymbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycspInducedFromToMorphism :: CspRawMap -> ExtSign CspCASLSign CspSymbol
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy GimblettcspInducedFromToMorphism rmap (ExtSign sSig sy) (ExtSign tSig tSy) =
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder let (crm, rm) = splitSymbolMap rmap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly inducedFromToMorphismExt inducedCspSign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (constMorphExt emptyCspAddMorphism)
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett composeMorphismExtension isCspSubSign diffCspSig
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly crm (ExtSign sSig $ getCASLSymbols sy)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly $ ExtSign tSig $ getCASLSymbols tSy
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly mor <- cspInducedFromMorphism rmap sSig
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly let iSig = mtarget mor
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett if isSubSig isCspSubSign iSig tSig then do
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder incl <- sigInclusion emptyCspAddMorphism iSig tSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly composeM composeMorphismExtension mor incl
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ("No signature morphism for csp symbol map found.\n" ++
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder "The following mapped symbols are missing in the target signature:\n"
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder ++ showDoc (diffSig diffCspSig iSig tSig) "")
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder $ concatMapRange getRange $ Map.keys rmap
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycspInducedFromMorphism :: CspRawMap -> CspCASLSign -> Result CspCASLMorphism
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycspInducedFromMorphism rmap sigma = do
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let (crm, _) = splitSymbolMap rmap
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly m <- inducedFromMorphism emptyCspAddMorphism crm sigma
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let sm = sort_map m
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder om = op_map m
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder pm = pred_map m
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder csig = extendedInfo sigma
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder newSRel = Rel.transClosure . sortRel $ mtarget m
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder -- compute the channel name map (as a Map)
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder cm <- Map.foldWithKey (chanFun sigma rmap sm)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (return Map.empty) (MapSet.toMap $ chans csig)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -- compute the process name map (as a Map)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett proc_Map <- Map.foldWithKey (procFun sigma rmap sm newSRel cm)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett (return Map.empty) (MapSet.toMap $ procSet csig)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett let em = emptyCspAddMorphism
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett { channelMap = cm
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , processMap = proc_Map }
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett return (embedMorphism em sigma $ closeSortRel
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett $ inducedSignAux inducedCspSign sm om pm em sigma)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett { sort_map = sm
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , op_map = om
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett , pred_map = pm }
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettchanFun :: CspCASLSign -> CspRawMap -> Sort_map -> Id -> Set.Set SORT
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> Result ChanMap -> Result ChanMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillychanFun sig rmap sm cn ss m =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let sls = Rel.partSet (relatedSorts sig) ss
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly m1 = foldr (directChanMap rmap sm cn) m sls
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett in case (Map.lookup (CspKindedSymb ChannelKind cn) rmap,
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett Map.lookup (CspKindedSymb (CaslKind Implicit) cn) rmap) of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Just rsy1, Just rsy2) -> let
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett m2 = Set.fold (insertChanSym sm cn rsy1) m1 ss
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett in Set.fold (insertChanSym sm cn rsy2) m2 ss
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (Just rsy, Nothing) ->
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett Set.fold (insertChanSym sm cn rsy) m1 ss
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett (Nothing, Just rsy) ->
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Set.fold (insertChanSym sm cn rsy) m1 ss
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett -- Anything not mapped explicitly is left unchanged
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (Nothing, Nothing) -> m1
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaederdirectChanMap :: CspRawMap -> Sort_map -> Id -> Set.Set SORT
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder -> Result ChanMap -> Result ChanMap
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettdirectChanMap rmap sm cn ss m =
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett rl = map (\ s -> Map.lookup (ACspSymbol $ toChanSymbol (cn, s)) rmap) sl
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett (ms, ps) = partition (isJust . fst) $ zip rl sl
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett in case ms of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett l@((Just rsy, _) : rs) ->
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett foldr (\ (_, s) ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett insertChanSym sm cn
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (ACspSymbol $ toChanSymbol
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (rawId rsy, mapSort sm s)) s)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (foldr (\ (rsy2, s) ->
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly insertChanSym sm cn (fromJust rsy2) s) m l)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillyinsertChanSym :: Sort_map -> Id -> CspRawSymbol -> SORT -> Result ChanMap
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly -> Result ChanMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettinsertChanSym sm cn rsy s m = do
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett c1 <- mappedChanSym sm cn s rsy
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett let ptsy = CspSymbol cn $ ChanAsItemType s
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett pos = getRange rsy
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett m2 = Map.insert (cn, s) c1 m1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case Map.lookup (cn, s) m1 of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Nothing -> if cn == c1 then
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ACspSymbol _ -> return m1
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach _ -> hint m1 ("identity mapping of "
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ++ showDoc ptsy "") pos
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else return m2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just c2 -> if c1 == c2 then
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ignoring duplicate mapping of " ++ showDoc ptsy "") pos
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else plain_error m1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("conflicting mapping of " ++ showDoc ptsy " to " ++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show c1 ++ " and " ++ show c2) pos
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettmappedChanSym :: Sort_map -> Id -> SORT -> CspRawSymbol -> Result Id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmappedChanSym sm cn s rsy =
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let chanSym = "channel symbol " ++ showDoc (toChanSymbol (cn, s))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly " is mapped to "
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett in case rsy of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ACspSymbol (CspSymbol ide (ChanAsItemType s1)) ->
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let s2 = mapSort sm s
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett in if s1 == s2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett then return ide
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else plain_error cn
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (chanSym ++ "sort " ++ showDoc s1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly " but should be mapped to type " ++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly showDoc s2 "") $ getRange rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CspKindedSymb k ide | elem k [CaslKind Implicit, ChannelKind] ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> plain_error cn
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (chanSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ getRange rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyprocFun :: CspCASLSign -> CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap -> Id
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyprocFun sig rmap sm rel cm pn ps m =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let pls = Rel.partSet (relatedProcs sig) ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly m1 = foldr (directProcMap rmap sm rel cm pn) m pls
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- now try the remaining ones with (un)kinded raw symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in case (Map.lookup (CspKindedSymb ProcessKind pn) rmap,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Map.lookup (CspKindedSymb (CaslKind Implicit) pn) rmap) of
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder (Just rsy1, Just rsy2) -> let
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder m2 = Set.fold (insertProcSym sm rel cm pn rsy1) m1 ps
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett in Set.fold (insertProcSym sm rel cm pn rsy2) m2 ps
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Just rsy, Nothing) ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Set.fold (insertProcSym sm rel cm pn rsy) m1 ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (Nothing, Just rsy) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Set.fold (insertProcSym sm rel cm pn rsy) m1 ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- Anything not mapped explicitly is left unchanged
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (Nothing, Nothing) -> m1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillydirectProcMap :: CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> Id -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillydirectProcMap rmap sm rel cm pn ps m =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly rl = map (lookupProcSymbol rmap pn) pl
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ms, os) = partition (isJust . fst) $ zip rl pl
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in case ms of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly l@((Just rsy, _) : rs) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly foldr (\ (_, p) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly insertProcSym sm rel cm pn
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ACspSymbol $ toProcSymbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (rawId rsy, mapProcProfile sm cm p)) p)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (foldr (\ (rsy2, p) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly insertProcSym sm rel cm pn (fromJust rsy2) p) m l)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupProcSymbol :: CspRawMap -> Id -> ProcProfile
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> Maybe CspRawSymbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupProcSymbol rmap pn p = case
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly filter (\ (k, _) -> case k of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ACspSymbol (CspSymbol i (ProcAsItemType pf)) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly i == pn && matchProcTypes p pf
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> False) $ Map.toList rmap of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [(_, r)] -> Just r
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [] -> Nothing
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- in case of ambiguities try to find an exact match
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly l -> lookup (ACspSymbol $ toProcSymbol (pn, p)) l
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyinsertProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id -> CspRawSymbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> ProcProfile -> Result ProcessMap -> Result ProcessMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyinsertProcSym sm rel cm pn rsy pf@(ProcProfile _ al) m = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (p1, al1) <- mappedProcSym sm rel cm pn pf rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let otsy = toProcSymbol (pn, pf)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pos = getRange rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly m2 = Map.insert (pn, pf) p1 m1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case Map.lookup (pn, pf) m1 of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> if pn == p1 && al == al1 then
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ACspSymbol _ -> return m1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> hint m1 ("identity mapping of "
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ++ showDoc otsy "") pos
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else return m2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just p2 -> if p1 == p2 then
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ("ignoring duplicate mapping of " ++ showDoc otsy "")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else plain_error m1
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett ("conflicting mapping of " ++ showDoc otsy " to " ++
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett show p1 ++ " and " ++ show p2) pos
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymappedProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> ProcProfile -> CspRawSymbol -> Result (Id, CommAlpha)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymappedProcSym sm rel cm pn pfSrc rsy =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let procSym = "process symbol " ++ showDoc (toProcSymbol (pn, pfSrc))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly " is mapped to "
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pfMapped@(ProcProfile _ al2) = reduceProcProfile rel
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ mapProcProfile sm cm pfSrc
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in case rsy of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ACspSymbol (CspSymbol ide (ProcAsItemType pf)) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let pfTar@(ProcProfile _ al1) = reduceProcProfile rel pf
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in if compatibleProcTypes rel pfMapped pfTar
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly then return (ide, al1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else plain_error (pn, al2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (procSym ++ "type " ++ showDoc pfTar
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "\nbut should be mapped to type " ++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly showDoc pfMapped
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "\npossibly using a sub-alphabet of " ++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly showDoc (closeCspCommAlpha rel al2) ".")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ getRange rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CspKindedSymb k ide | elem k [CaslKind Implicit, ProcessKind] ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (ide, al2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> plain_error (pn, al2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (procSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ getRange rsy
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycompatibleProcTypes :: Rel.Rel SORT -> ProcProfile -> ProcProfile -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycompatibleProcTypes rel (ProcProfile l1 al1) (ProcProfile l2 al2) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly l1 == l2 && liamsRelatedCommAlpha rel al1 al2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyliamsRelatedCommAlpha :: Rel.Rel SORT -> CommAlpha -> CommAlpha -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyliamsRelatedCommAlpha rel al1 al2 =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly all (\ a2 -> any (\ a1 -> liamsRelatedCommTypes rel a1 a2) $ Set.toList al1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyliamsRelatedCommTypes :: Rel.Rel SORT -> CommType -> CommType -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyliamsRelatedCommTypes rel ct1 ct2 = case (ct1, ct2) of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (CommTypeSort s1, CommTypeSort s2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> s1 == s2 || s1 `Set.member` Rel.succs rel s2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (CommTypeChan (TypedChanName c1 s1), CommTypeChan (TypedChanName c2 s2))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> c1 == c2 && s1 == s2
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettmatchProcTypes :: ProcProfile -> ProcProfile -> Bool
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettmatchProcTypes (ProcProfile l1 al1) (ProcProfile l2 al2) = l1 == l2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett && (Set.null al2 || Set.null al1 || not (Set.null $ Set.intersection al1 al2))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycspMatches :: CspSymbol -> CspRawSymbol -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycspMatches (CspSymbol i t) rsy = case rsy of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ACspSymbol (CspSymbol j t2) -> i == j && case (t, t2) of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (CaslSymbType t1, CaslSymbType t3) -> matches (Symbol i t1)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $ ASymbol $ Symbol j t3
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ChanAsItemType s1, ChanAsItemType s2) -> s1 == s2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ProcAsItemType p1, ProcAsItemType p2) -> matchProcTypes p1 p2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly CspKindedSymb k j -> let res = i == j in case (k, t) of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (CaslKind ck, CaslSymbType t1) -> matches (Symbol i t1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ AKindedSymb ck j
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ChannelKind, ChanAsItemType _) -> res
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (ProcessKind, ProcAsItemType _) -> res
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (CaslKind Implicit, _) -> res
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettprocProfile2Sorts :: ProcProfile -> Set.Set SORT
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyprocProfile2Sorts (ProcProfile sorts al) =
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Set.union (Set.fromList sorts) $ Set.map commType2Sort al
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillycspRevealSym :: CspSymbol -> CspCASLSign -> CspCASLSign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycspRevealSym sy sig = let
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett n = cspSymName sy
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly r = sortRel sig
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett ext = extendedInfo sig
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett cs = chans ext
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett in case cspSymbType sy of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly CaslSymbType t -> revealSym (Symbol n t) sig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ChanAsItemType s -> sig
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett { sortRel = Rel.insertKey s r
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , extendedInfo = ext { chans = MapSet.insert n s cs }}
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett ProcAsItemType p@(ProcProfile _ al) -> sig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly { sortRel = Rel.union (Rel.fromKeysSet $ procProfile2Sorts p) r
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , extendedInfo = ext
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly { chans = Set.fold (\ ct -> case ct of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett CommTypeSort _ -> id
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly CommTypeChan (TypedChanName c s) -> MapSet.insert c s) cs al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , procSet = MapSet.insert n p $ procSet ext }
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettcspGeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspGeneratedSign sys sigma = let
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly symset = Set.unions $ symSets sigma
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sigma1 = Set.fold cspRevealSym sigma
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , extendedInfo = emptyCspSign } sys
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sigma2 = sigma1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly { sortRel = sortRel sigma `Rel.restrict` sortSet sigma1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly , emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in if not $ Set.isSubsetOf sys symset
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett then let diffsyms = sys Set.\\ symset in
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly fatal_error ("Revealing: The following symbols "
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ++ showDoc diffsyms " are not in the signature")
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly $ getRange diffsyms
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly else cspSubsigInclusion sigma2 sigma
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillycspCogeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspCogeneratedSign symset sigma = let
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly symset0 = Set.unions $ symSets sigma
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly symset1 = Set.fold cspHideSym symset0 symset
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett in if Set.isSubsetOf symset symset0
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly then cspGeneratedSign symset1 sigma
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly else let diffsyms = symset Set.\\ symset0 in
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly fatal_error ("Hiding: The following symbols "
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ++ showDoc diffsyms " are not in the signature")
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly $ getRange diffsyms
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettcspHideSym :: CspSymbol -> Set.Set CspSymbol -> Set.Set CspSymbol
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycspHideSym sy set1 = let
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly set2 = Set.delete sy set1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly n = cspSymName sy
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in case cspSymbType sy of
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly CaslSymbType SortAsItemType ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.filter (not . cspProfileContains n . cspSymbType) set2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ChanAsItemType s ->
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Set.filter (unusedChan n s) set2
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProfileContains :: Id -> CspSymbType -> Bool
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillycspProfileContains s ty = case ty of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CaslSymbType t -> profileContainsSort s t
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ChanAsItemType s2 -> s == s2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ProcAsItemType p -> Set.member s $ procProfile2Sorts p
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyunusedChan :: Id -> SORT -> CspSymbol -> Bool
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyunusedChan c s sy = case cspSymbType sy of
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly ProcAsItemType (ProcProfile _ al) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.fold (\ ct b -> case ct of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett CommTypeSort _ -> b
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly CommTypeChan (TypedChanName c2 s2) -> b && (c, s) /= (c2, s2)) True al