bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederDescription : symbol map analysis for the CspCASL logic.

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : Christian.Maeder@dfki.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule CspCASL.SymMapAna where

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CspCASL.AS_CspCASL_Process

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CspCASL.Morphism

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport CspCASL.SignCSP

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport CspCASL.SymbItems

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport CspCASL.Symbol

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CASL.Sign

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport CASL.AS_Basic_CASL

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.Morphism

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport CASL.SymbolMapAnalysis

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.DocUtils

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport Common.ExtSign

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Id

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederimport Common.Result

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport qualified Common.Lib.Rel as Rel

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport qualified Common.Lib.MapSet as MapSet

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport qualified Data.Map as Map

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport qualified Data.Set as Set

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Data.List (partition)

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Data.Maybe

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport qualified Debug.Trace as Trace

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maedertype CspRawMap = Map.Map CspRawSymbol CspRawSymbol

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedercspInducedFromToMorphism :: CspRawMap -> ExtSign CspCASLSign CspSymbol

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedercspInducedFromToMorphism rmap (ExtSign sSig sy) (ExtSign tSig tSy) =

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder let (crm, rm) = splitSymbolMap rmap

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in if Map.null rm then

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder inducedFromToMorphismExt inducedCspSign

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder (constMorphExt emptyCspAddMorphism)

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder composeMorphismExtension isCspSubSign diffCspSig

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder crm (ExtSign sSig $ getCASLSymbols sy)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder $ ExtSign tSig $ getCASLSymbols tSy

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder else do

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder mor <- cspInducedFromMorphism rmap sSig

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder let iSig = mtarget mor

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder if isSubSig isCspSubSign iSig tSig then do

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder incl <- sigInclusion emptyCspAddMorphism iSig tSig

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder composeM composeMorphismExtension mor incl

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder else

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder fatal_error

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder ("No signature morphism for csp symbol map found.\n" ++

ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maeder "The following mapped symbols are missing in the target signature:\n"

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder ++ showDoc (diffSig diffCspSig iSig tSig) "")

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder $ concatMapRange getRange $ Map.keys rmap

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaedercspInducedFromMorphism :: CspRawMap -> CspCASLSign -> Result CspCASLMorphism

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspInducedFromMorphism rmap sigma = do

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder let (crm, _) = splitSymbolMap rmap

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder m <- inducedFromMorphism emptyCspAddMorphism crm sigma

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder let sm = sort_map m

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder om = op_map m

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder pm = pred_map m

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder csig = extendedInfo sigma

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder newSRel = sortRel $ mtarget m

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -- compute the channel name map (as a Map)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder cm <- Map.foldWithKey (chanFun sigma rmap sm)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (return Map.empty) (MapSet.toMap $ chans csig)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -- compute the process name map (as a Map)

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder proc_Map <- Map.foldWithKey (procFun sigma rmap sm newSRel cm)

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder (return Map.empty) (MapSet.toMap $ procSet csig)

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder let em = emptyCspAddMorphism

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder { channelMap = cm

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , processMap = proc_Map }

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (embedMorphism em sigma $ closeSortRel

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder $ inducedSignAux inducedCspSign sm om pm em sigma)

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder { sort_map = sm

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , op_map = om

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , pred_map = pm }

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederchanFun :: CspCASLSign -> CspRawMap -> Sort_map -> Id -> Set.Set SORT

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -> Result ChanMap -> Result ChanMap

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederchanFun sig rmap sm cn ss m =

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder let sls = Rel.partSet (relatedSorts sig) ss

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder m1 = foldr (directChanMap rmap sm cn) m sls

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder in case (Map.lookup (CspKindedSymb ChannelKind cn) rmap,

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Map.lookup (CspKindedSymb (CaslKind Implicit) cn) rmap) of

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder (Just rsy1, Just rsy2) -> let

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder m2 = Set.fold (insertChanSym sm cn rsy1) m1 ss

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder in Set.fold (insertChanSym sm cn rsy2) m2 ss

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder (Just rsy, Nothing) ->

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder Set.fold (insertChanSym sm cn rsy) m1 ss

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (Nothing, Just rsy) ->

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Set.fold (insertChanSym sm cn rsy) m1 ss

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- Anything not mapped explicitly is left unchanged

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (Nothing, Nothing) -> m1

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederdirectChanMap :: CspRawMap -> Sort_map -> Id -> Set.Set SORT

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -> Result ChanMap -> Result ChanMap

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederdirectChanMap rmap sm cn ss m =

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder let sl = Set.toList ss

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder rl = map (\ s -> Map.lookup (ACspSymbol $ toChanSymbol (cn, s)) rmap) sl

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder (ms, ps) = partition (isJust . fst) $ zip rl sl

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder in case ms of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder l@((Just rsy, _) : rs) ->

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder foldr (\ (_, s) ->

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder insertChanSym sm cn

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder (ACspSymbol $ toChanSymbol

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (rawId rsy, mapSort sm s)) s)

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder (foldr (\ (rsy2, s) ->

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder insertChanSym sm cn (fromJust rsy2) s) m l)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder $ rs ++ ps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> m

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederinsertChanSym :: Sort_map -> Id -> CspRawSymbol -> SORT -> Result ChanMap

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder -> Result ChanMap

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederinsertChanSym sm cn rsy s m = do

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder m1 <- m

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder c1 <- mappedChanSym sm cn s rsy

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let ptsy = CspSymbol cn $ ChanAsItemType s

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder pos = getRange rsy

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder m2 = Map.insert (cn, s) c1 m1

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder case Map.lookup (cn, s) m1 of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> if cn == c1 then

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case rsy of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ACspSymbol _ -> return m1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> hint m1 ("identity mapping of "

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ++ showDoc ptsy "") pos

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder else return m2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just c2 -> if c1 == c2 then

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder warning m1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ("ignoring duplicate mapping of " ++ showDoc ptsy "") pos

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else plain_error m1

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ("conflicting mapping of " ++ showDoc ptsy " to " ++

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show c1 ++ " and " ++ show c2) pos

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermappedChanSym :: Sort_map -> Id -> SORT -> CspRawSymbol -> Result Id

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedermappedChanSym sm cn s rsy =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let chanSym = "channel symbol " ++ showDoc (toChanSymbol (cn, s))

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder " is mapped to "

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder in case rsy of

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder ACspSymbol (CspSymbol ide (ChanAsItemType s1)) ->

1738d16957389457347bee85075d3d33d002158fChristian Maeder let s2 = mapSort sm s

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder in if s1 == s2

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder then return ide

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder else plain_error cn

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (chanSym ++ "sort " ++ showDoc s1

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder " but should be mapped to type " ++

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder showDoc s2 "") $ getRange rsy

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CspKindedSymb k ide | elem k [CaslKind Implicit, ChannelKind] ->

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return ide

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder _ -> plain_error cn

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder (chanSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder $ getRange rsy

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederprocFun :: CspCASLSign -> CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap -> Id

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederprocFun sig rmap sm rel cm pn ps m =

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder let pls = Rel.partSet (relatedProcs sig) ps

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder m1 = foldr (directProcMap sig rmap sm rel cm pn) m pls

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -- now try the remaining ones with (un)kinded raw symbol

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in case (Map.lookup (CspKindedSymb ProcessKind pn) rmap,

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Map.lookup (CspKindedSymb (CaslKind Implicit) pn) rmap) of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (Just rsy1, Just rsy2) -> let

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder m2 = Set.fold (insertProcSym sig sm rel cm pn rsy1) m1 ps

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in Set.fold (insertProcSym sig sm rel cm pn rsy2) m2 ps

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder (Just rsy, Nothing) ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Set.fold (insertProcSym sig sm rel cm pn rsy) m1 ps

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (Nothing, Just rsy) ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Set.fold (insertProcSym sig sm rel cm pn rsy) m1 ps

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- Anything not mapped explicitly is left unchanged

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (Nothing, Nothing) -> m1

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederdirectProcMap :: CspCASLSign -> CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -> Id -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederdirectProcMap sig rmap sm rel cm pn ps m =

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder let pl = Set.toList ps

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder rl = map (lookupProcSymbol sig rmap pn) pl

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (ms, os) = partition (isJust . fst) $ zip rl pl

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in case ms of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder l@((Just rsy, _) : rs) ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder foldr (\ (_, p) ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder insertProcSym sig sm rel cm pn

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (ACspSymbol $ toProcSymbol

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (rawId rsy, mapProcProfile sm cm p)) p)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (foldr (\ (rsy2, p) ->

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder insertProcSym sig sm rel cm pn (fromJust rsy2) p) m l)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $ rs ++ os

_ -> m

lookupProcSymbol :: CspCASLSign -> CspRawMap -> Id -> ProcProfile

-> Maybe CspRawSymbol

lookupProcSymbol sig rmap pn p = case

filter (\ (k, _) -> case k of

ACspSymbol (CspSymbol i (ProcAsItemType pf)) ->

i == pn && compatibleProcTypes (Just sig) p pf

_ -> False) $ Map.toList rmap of

[(_, r)] -> Just r

[] -> Nothing

-- in case of ambiguities try to find an exact match

l -> lookup (ACspSymbol $ toProcSymbol (pn, p)) l

insertProcSym :: CspCASLSign -> Sort_map -> Rel.Rel SORT -> ChanMap -> Id

-> CspRawSymbol -> ProcProfile -> Result ProcessMap -> Result ProcessMap

insertProcSym sig sm rel cm pn rsy pf@(ProcProfile _ al) m = do

m1 <- m

(p1, al0) <- mappedProcSym sig sm cm pn pf rsy

let al1 = closeCspCommAlpha rel al0

otsy = toProcSymbol (pn, pf)

pos = getRange rsy

m2 = Map.insert (pn, pf) (p1, al1) m1

case Map.lookup (pn, pf) m1 of

Nothing -> if pn == p1 && al == al1 then

case rsy of

ACspSymbol _ -> return m1

_ -> hint m1 ("identity mapping of "

++ showDoc otsy "") pos

else return m2

Just (p2, al2) -> if p1 == p2 then

warning (if al1 /= al2 then m2 else m1)

("ignoring duplicate mapping of " ++ showDoc otsy "")

pos

else plain_error m1

("conflicting mapping of " ++ showDoc otsy " to " ++

show p1 ++ " and " ++ show p2) pos

mappedProcSym :: CspCASLSign -> Sort_map -> ChanMap -> Id -> ProcProfile

-> CspRawSymbol -> Result (Id, CommAlpha)

mappedProcSym sig sm cm pn pf rsy =

let procSym = "process symbol " ++ showDoc (toProcSymbol (pn, pf))

" is mapped to "

pf2@(ProcProfile _ al2) = mapProcProfile sm cm pf

in case rsy of

ACspSymbol (CspSymbol ide (ProcAsItemType pf1@(ProcProfile _ al1))) ->

if compatibleProcTypes (Just sig) pf1 pf2

then return (ide, al1)

else plain_error (pn, al2)

(procSym ++ "type " ++ showDoc pf1

" but should be mapped to type " ++

showDoc pf2 "") $ getRange rsy

CspKindedSymb k ide | elem k [CaslKind Implicit, ProcessKind] ->

return (ide, al2)

_ -> plain_error (pn, al2)

(procSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

$ getRange rsy

-- BUG I am confused which parameter is which: the target seems to be the first

-- parameter and the source the seconds, in terms of signature morphism

-- analysis.

compatibleProcTypes :: Maybe CspCASLSign -> ProcProfile -> ProcProfile -> Bool

compatibleProcTypes msig (ProcProfile l1 al1) (ProcProfile l2 al2) =

l1 == l2 && liamsRelatedCommAlpha (fromMaybe emptyCspCASLSign msig) al1 al2

-- BUG I am confused which parameter is which: they seem backwards

liamsRelatedCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha -> Bool

liamsRelatedCommAlpha sig al2 al1 =

let msg = "al1 = [" ++ show al1 ++ "], al2= [" ++ show al2 ++ "]"

in Trace.trace (msg) $ all (\ a2 -> any (\a1 -> liamsRelatedCommTypes sig a1 a2) $ Set.toList al1)

(Set.toList al2)

liamsRelatedCommTypes :: CspCASLSign -> CommType -> CommType -> Bool

liamsRelatedCommTypes sig ct1 ct2 = case (ct1, ct2) of

(CommTypeSort s1, CommTypeSort s2)

-> s1 == s2 || s1 `Set.member` subsortsOf s1 sig

(CommTypeChan (TypedChanName c1 s1), CommTypeChan (TypedChanName c2 s2))

-> c1 == c2 && s1 == s2

_ -> False

cspMatches :: CspSymbol -> CspRawSymbol -> Bool

cspMatches (CspSymbol i t) rsy = case rsy of

ACspSymbol (CspSymbol j t2) -> i == j && case (t, t2) of

(CaslSymbType t1, CaslSymbType t3) -> matches (Symbol i t1)

$ ASymbol $ Symbol j t3

(ChanAsItemType s1, ChanAsItemType s2) -> s1 == s2

(ProcAsItemType (ProcProfile l1 al1), ProcAsItemType (ProcProfile l2 al2)) ->

l1 == l2 && (Set.null al2 || not (Set.null $ Set.intersection al1 al2))

_ -> False

CspKindedSymb k j -> let res = i == j in case (k, t) of

(CaslKind ck, CaslSymbType t1) -> matches (Symbol i t1)

$ AKindedSymb ck j

(ChannelKind, ChanAsItemType _) -> res

(ProcessKind, ProcAsItemType _) -> res

(CaslKind Implicit, _) -> res

_ -> False

commType2Sort :: CommType -> SORT

commType2Sort c = case c of

CommTypeSort s -> s

CommTypeChan (TypedChanName _ s) -> s

procProfile2Sorts :: ProcProfile -> Set.Set SORT

procProfile2Sorts (ProcProfile sorts al) =

Set.union (Set.fromList sorts) $ Set.map commType2Sort al

cspRevealSym :: CspSymbol -> CspCASLSign -> CspCASLSign

cspRevealSym sy sig = let

n = cspSymName sy

r = sortRel sig

ext = extendedInfo sig

cs = chans ext

in case cspSymbType sy of

CaslSymbType t -> revealSym (Symbol n t) sig

ChanAsItemType s -> sig

{ sortRel = Rel.insertKey s r

, extendedInfo = ext { chans = MapSet.insert n s cs }}

ProcAsItemType p@(ProcProfile _ al) -> sig

{ sortRel = Rel.union (Rel.fromKeysSet $ procProfile2Sorts p) r

, extendedInfo = ext

{ chans = Set.fold (\ ct -> case ct of

CommTypeSort _ -> id

CommTypeChan (TypedChanName c s) -> MapSet.insert c s) cs al

, procSet = MapSet.insert n p $ procSet ext }

}

cspGeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism

cspGeneratedSign sys sigma = let

symset = Set.unions $ symSets sigma

sigma1 = Set.fold cspRevealSym sigma

{ sortRel = Rel.empty

, opMap = MapSet.empty

, predMap = MapSet.empty

, extendedInfo = emptyCspSign } sys

sigma2 = sigma1

{ sortRel = sortRel sigma `Rel.restrict` sortSet sigma1

, emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }

in if not $ Set.isSubsetOf sys symset

then let diffsyms = sys Set.\\ symset in

fatal_error ("Revealing: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

else cspSubsigInclusion sigma2 sigma

cspCogeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism

cspCogeneratedSign symset sigma = let

symset0 = Set.unions $ symSets sigma

symset1 = Set.fold cspHideSym symset0 symset

in if Set.isSubsetOf symset symset0

then cspGeneratedSign symset1 sigma

else let diffsyms = symset Set.\\ symset0 in

fatal_error ("Hiding: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

cspHideSym :: CspSymbol -> Set.Set CspSymbol -> Set.Set CspSymbol

cspHideSym sy set1 = let

set2 = Set.delete sy set1

n = cspSymName sy

in case cspSymbType sy of

CaslSymbType SortAsItemType ->

Set.filter (not . cspProfileContains n . cspSymbType) set2

ChanAsItemType s ->

Set.filter (unusedChan n s) set2

_ -> set2

cspProfileContains :: Id -> CspSymbType -> Bool

cspProfileContains s ty = case ty of

CaslSymbType t -> profileContainsSort s t

ChanAsItemType s2 -> s == s2

ProcAsItemType p -> Set.member s $ procProfile2Sorts p

unusedChan :: Id -> SORT -> CspSymbol -> Bool

unusedChan c s sy = case cspSymbType sy of

ProcAsItemType (ProcProfile _ al) ->

Set.fold (\ ct b -> case ct of

CommTypeSort _ -> b

CommTypeChan (TypedChanName c2 s2) -> b && (c, s) /= (c2, s2)) True al

_ -> True