Symbol.hs revision 634f844958d5f75ad95583351efb582b9d233506
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederDescription : semantic csp-casl symbols
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederMaintainer : Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder-}
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedermodule CspCASL.Symbol where
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport CspCASL.AS_CspCASL_Process
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport CspCASL.CspCASL_Keywords
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport CspCASL.SignCSP
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport CspCASL.SymbItems
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maederimport CASL.AS_Basic_CASL
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maederimport CASL.Morphism
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport CASL.Sign
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Common.Doc
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.DocUtils
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Id
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport Common.Result
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport qualified Data.Map as Map
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport qualified Data.Set as Set
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Control.Monad
62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata CspSymbType
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder = CaslSymbType SymbType
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder | ProcAsItemType ProcProfile
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder | ChanAsItemType Id -- the SORT
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder deriving (Show, Eq, Ord)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederdata CspSymbol = CspSymbol {cspSymName :: Id, cspSymbType :: CspSymbType}
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder deriving (Show, Eq, Ord)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maederdata CspRawSymbol = ACspSymbol CspSymbol | CspKindedSymb CspSymbKind Id
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder deriving (Show, Eq, Ord)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederrawId :: CspRawSymbol -> Id
975642b989852fc24119c59cf40bc1af653608ffChristian MaederrawId r = case r of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ACspSymbol s -> cspSymName s
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder CspKindedSymb _ i -> i
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maederinstance Pretty CspSymbType where
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder pretty t = case t of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder CaslSymbType c -> pretty c
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ProcAsItemType p -> pretty p
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ChanAsItemType s -> pretty s
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederinstance Pretty CspSymbol where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder pretty (CspSymbol i t) = case t of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ProcAsItemType p -> keyword processS <+> pretty i <+> pretty p
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder ChanAsItemType s -> keyword channelS <+> pretty i <+> colon <+> pretty s
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder CaslSymbType c -> pretty $ Symbol i c
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance GetRange CspSymbol where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder getRange (CspSymbol i _) = getRange i
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Pretty CspRawSymbol where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder pretty r = case r of
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder ACspSymbol s -> pretty s
fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder CspKindedSymb k i -> pretty k <+> pretty i
25612a7b3ce708909298d5426406592473880a20Christian Maeder
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederinstance GetRange CspRawSymbol where
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder getRange r = case r of
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder ACspSymbol s -> getRange s
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder CspKindedSymb _ i -> getRange i
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercspCheckSymbList :: [CspSymbMap] -> [Diagnosis]
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedercspCheckSymbList l = case l of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder CspSymbMap (CspSymb a Nothing) Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder : CspSymbMap (CspSymb b (Just t)) _ : r -> mkDiag Warning
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ("profile '" ++ showDoc t "' does not apply to '"
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ++ showId a "' but only to") b : cspCheckSymbList r
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder _ : r -> cspCheckSymbList r
18b709ce961d68328da768318dcc70067f066d86Christian Maeder [] -> []
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaedertoChanSymbol :: (CHANNEL_NAME, SORT) -> CspSymbol
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian MaedertoChanSymbol (c, s) = CspSymbol (simpleIdToId c) $ ChanAsItemType s
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertoProcSymbol :: (SIMPLE_PROCESS_NAME, ProcProfile) -> CspSymbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertoProcSymbol (n, p) = CspSymbol (simpleIdToId n) $ ProcAsItemType p
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederidToCspRaw :: Id -> CspRawSymbol
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederidToCspRaw = CspKindedSymb $ CaslKind Implicit
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedercspTypedSymbKindToRaw :: CspSymbKind -> Id -> CspType -> Result CspRawSymbol
797f811e57952d59e73b8cd03b667eef276db972Christian MaedercspTypedSymbKindToRaw k idt t = let
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder err = plain_error (idToCspRaw idt)
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder (showDoc idt " " ++ showDoc t
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder " does not have kind " ++ showDoc k "") nullRange
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder mkSimple i = if isSimpleId i then return $ idToSimpleId i else
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mkError "not a simple id" i
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski in case k of
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder ProcessKind -> do
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder si <- mkSimple idt
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder case t of
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ProcType p -> return $ ACspSymbol $ toProcSymbol (si, p)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder CaslType (A_type s) -> return
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder $ ACspSymbol $ toProcSymbol
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (si, ProcProfile [] $ Set.singleton $ CommTypeSort s)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> err
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder ChannelKind -> do
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder si <- mkSimple idt
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder case t of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder CaslType (A_type s) ->
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder return $ ACspSymbol $ toChanSymbol (si, s)
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder _ -> err
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder CaslKind ck -> case t of
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder CaslType ct -> fmap (\ r -> case r of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder ASymbol sy -> ACspSymbol $ CspSymbol idt $ CaslSymbType $ symbType sy
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder _ -> CspKindedSymb k idt)
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder $ typedSymbKindToRaw ck idt ct
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder _ -> err
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedercspSymbToRaw :: CspSymbKind -> CspSymb -> Result CspRawSymbol
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedercspSymbToRaw k (CspSymb idt mt) = case mt of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> return $ case k of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder CaslKind Sorts_kind ->
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ACspSymbol $ CspSymbol idt $ CaslSymbType SortAsItemType
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder _ -> CspKindedSymb k idt
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder Just t -> cspTypedSymbKindToRaw k idt t
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedercspStatSymbItems :: [CspSymbItems] -> Result [CspRawSymbol]
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedercspStatSymbItems sl =
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder let st (CspSymbItems kind l) = do
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder appendDiags $ cspCheckSymbList $ map (`CspSymbMap` Nothing) l
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder mapM (cspSymbToRaw kind) l
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder in fmap concat (mapM st sl)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian MaedercspSymbOrMapToRaw :: CspSymbKind -> CspSymbMap
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder -> Result [(CspRawSymbol, CspRawSymbol)]
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaedercspSymbOrMapToRaw k (CspSymbMap s mt) = case mt of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Nothing -> do
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder v <- cspSymbToRaw k s
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return [(v, v)]
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder Just t -> do
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder appendDiags $ case (s, t) of
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder (CspSymb a Nothing, CspSymb b Nothing) | a == b ->
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder [mkDiag Hint "unneeded identical mapping of" a]
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder _ -> []
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder w <- cspSymbToRaw k s
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder x <- cspSymbToRaw k t
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder let mkS i = ACspSymbol $ CspSymbol i $ CaslSymbType SortAsItemType
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder pairS s1 s2 = (mkS s1, mkS s2)
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder case (w, x) of
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder (ACspSymbol (CspSymbol _ t1), ACspSymbol (CspSymbol _ t2)) ->
65835942d66905c377fa503e0d577df5aade58feChristian Maeder case (t1, t2) of
65835942d66905c377fa503e0d577df5aade58feChristian Maeder (ChanAsItemType s1, ChanAsItemType s2) ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return [(w, x), (mkS s1, mkS s2)]
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (ProcAsItemType (ProcProfile args1 _),
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder ProcAsItemType (ProcProfile args2 _))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | length args1 == length args2 ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return $ (w, x)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder : zipWith pairS args1 args2
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (CaslSymbType (PredAsItemType (PredType args1)),
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder CaslSymbType (PredAsItemType (PredType args2)))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | length args1 == length args2 ->
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return $ (w, x)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder : zipWith pairS args1 args2
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder (CaslSymbType (OpAsItemType (OpType _ args1 res1)),
CaslSymbType (OpAsItemType (OpType _ args2 res2)))
| length args1 == length args2 ->
return $ (w, x)
: zipWith pairS (res1 : args1) (res2 : args2)
(CaslSymbType SortAsItemType, CaslSymbType SortAsItemType) ->
return [(w, x)]
_ -> fail $ "profiles '" ++ showDoc t1 "' and '"
++ showDoc t2 "' do not match"
_ -> return [(w, x)]
cspStatSymbMapItems :: [CspSymbMapItems]
-> Result (Map.Map CspRawSymbol CspRawSymbol)
cspStatSymbMapItems sl = do
let st (CspSymbMapItems kind l) = do
appendDiags $ cspCheckSymbList l
fmap concat $ mapM (cspSymbOrMapToRaw kind) l
getSort rsy = case rsy of
ACspSymbol (CspSymbol i (CaslSymbType SortAsItemType)) -> Just i
_ -> Nothing
getImplicit rsy = case rsy of
CspKindedSymb (CaslKind Implicit) i -> Just i
_ -> Nothing
mkSort i = ACspSymbol $ CspSymbol i $ CaslSymbType SortAsItemType
mkImplicit = idToCspRaw
ls <- mapM st sl
foldM (insertRsys rawId getSort mkSort getImplicit mkImplicit)
Map.empty (concat ls)
toSymbolSet :: CspSign -> [Set.Set CspSymbol]
toSymbolSet csig = map Set.fromList
[ map toChanSymbol $ mapSetToList $ chans csig
, map toProcSymbol $ mapSetToList $ procSet csig ]
symSets :: CspCASLSign -> [Set.Set CspSymbol]
symSets sig = map (Set.map caslToCspSymbol) (symOf sig)
++ toSymbolSet (extendedInfo sig)
caslToCspSymbol :: Symbol -> CspSymbol
caslToCspSymbol sy = CspSymbol (symName sy) $ CaslSymbType $ symbType sy
-- | try to convert a csp raw symbol to a CASL raw symbol
toRawSymbol :: CspRawSymbol -> Maybe RawSymbol
toRawSymbol r = case r of
ACspSymbol (CspSymbol i (CaslSymbType t)) -> Just (ASymbol $ Symbol i t)
CspKindedSymb (CaslKind k) i -> Just (AKindedSymb k i)
_ -> Nothing
splitSymbolMap :: Map.Map CspRawSymbol CspRawSymbol
-> (RawSymbolMap, Map.Map CspRawSymbol CspRawSymbol)
splitSymbolMap = Map.foldWithKey (\ s t (cm, ccm) ->
case (toRawSymbol s, toRawSymbol t) of
(Just c, Just d) -> (Map.insert c d cm, ccm)
_ -> (cm, Map.insert s t ccm)) (Map.empty, Map.empty)