1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{-# LANGUAGE DeriveDataTypeable #-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederModule : ./CspCASL/Symbol.hs

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederDescription : semantic csp-casl symbols

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : Christian.Maeder@dfki.de

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : portable

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule CspCASL.Symbol where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport CspCASL.AS_CspCASL_Process

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport CspCASL.CspCASL_Keywords

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport CspCASL.SignCSP

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederimport CspCASL.SymbItems

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport CASL.AS_Basic_CASL

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport CASL.Morphism

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport CASL.Sign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.DocUtils

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Id

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport Common.Result

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Common.Lib.MapSet as MapSet

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Data.Data

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport qualified Data.Map as Map

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport qualified Data.Set as Set

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Control.Monad

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata CspSymbType

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder = CaslSymbType SymbType

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder | ProcAsItemType ProcProfile

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder | ChanAsItemType Id -- the SORT

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq, Ord, Typeable, Data)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Pretty CspSymbType where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder pretty (CaslSymbType st) = pretty $ symbolKind st

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder pretty (ProcAsItemType _) = text "process"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder pretty (ChanAsItemType _) = text "channel"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata CspSymbol = CspSymbol {cspSymName :: Id, cspSymbType :: CspSymbType}

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder deriving (Show, Eq, Ord, Typeable, Data)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata CspRawSymbol = ACspSymbol CspSymbol | CspKindedSymb CspSymbKind Id

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder deriving (Show, Eq, Ord, Typeable, Data)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

65dce48b81f69e11a36bf1051314a845299446e1Christian MaederrawId :: CspRawSymbol -> Id

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederrawId r = case r of

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ACspSymbol s -> cspSymName s

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder CspKindedSymb _ i -> i

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Pretty CspSymbol where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder pretty (CspSymbol i t) = case t of

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder ProcAsItemType p -> keyword processS <+> pretty i <+> pretty p

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ChanAsItemType s -> keyword channelS <+> pretty i <+> colon <+> pretty s

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder CaslSymbType c -> pretty $ Symbol i c

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederinstance GetRange CspSymbol where

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder getRange (CspSymbol i _) = getRange i

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Pretty CspRawSymbol where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder pretty r = case r of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ACspSymbol s -> pretty s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder CspKindedSymb k i -> pretty k <+> pretty i

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance GetRange CspRawSymbol where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder getRange r = case r of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ACspSymbol s -> getRange s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder CspKindedSymb _ i -> getRange i

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercspCheckSymbList :: [CspSymbMap] -> [Diagnosis]

67869d63d1725c79e4c07b51acd466a31932b275Christian MaedercspCheckSymbList l = case l of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder CspSymbMap (CspSymb a Nothing) Nothing

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder : CspSymbMap (CspSymb b (Just t)) _ : r -> mkDiag Warning

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ("profile '" ++ showDoc t "' does not apply to '"

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ++ showId a "' but only to") b : cspCheckSymbList r

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder _ : r -> cspCheckSymbList r

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder [] -> []

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoChanSymbol :: (CHANNEL_NAME, SORT) -> CspSymbol

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoChanSymbol (c, s) = CspSymbol c $ ChanAsItemType s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian MaedertoProcSymbol :: (PROCESS_NAME, ProcProfile) -> CspSymbol

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoProcSymbol (n, p) = CspSymbol n $ ProcAsItemType p

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederidToCspRaw :: Id -> CspRawSymbol

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederidToCspRaw = CspKindedSymb $ CaslKind Implicit

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersortToProcProfile :: SORT -> ProcProfile

67869d63d1725c79e4c07b51acd466a31932b275Christian MaedersortToProcProfile = ProcProfile [] . Set.singleton . CommTypeSort

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercspTypedSymbKindToRaw :: Bool -> CspCASLSign -> CspSymbKind -> Id -> CspType

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> Result CspRawSymbol

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercspTypedSymbKindToRaw b sig k idt t = let

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder csig = extendedInfo sig

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder getSet = MapSet.lookup idt

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder chs = getSet $ chans csig

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder prs = getSet $ procSet csig

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder reduce = reduceProcProfile $ sortRel sig

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder err = plain_error (idToCspRaw idt)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (showDoc idt " " ++ showDoc t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder " does not have kind " ++ showDoc k "") nullRange

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in case k of

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder ProcessKind -> case t of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ProcType p -> return $ ACspSymbol $ toProcSymbol (idt, reduce p)

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder CaslType (A_type s) -> return

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder $ ACspSymbol $ toProcSymbol

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder (idt, reduce $ sortToProcProfile s)

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder _ -> err

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder ChannelKind -> case t of

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder CaslType (A_type s) ->

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder return $ ACspSymbol $ toChanSymbol (idt, s)

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder _ -> err

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder CaslKind ck -> case t of

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder CaslType ct -> let

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder caslAnno = fmap (\ r -> case r of

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder ASymbol sy -> ACspSymbol $ CspSymbol idt $ CaslSymbType $ symbType sy

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder _ -> CspKindedSymb k idt) $ typedSymbKindToRaw b sig ck idt ct

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder in case ct of

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder A_type s | b && ck == Implicit ->

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder let hasChan = Set.member s chs

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder cprs = Set.filter (\ (ProcProfile args al) ->

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder null args && any (\ cs -> case cs of

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder CommTypeSort r -> r == s

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder || Set.member s (subsortsOf r sig)

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder CommTypeChan (TypedChanName c _) ->

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder c == s) (Set.toList al)) prs

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder in case Set.toList cprs of

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder [] -> if hasChan then do

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder appendDiags [mkDiag Hint "matched channel" idt]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ ACspSymbol $ toChanSymbol (idt, s)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder else caslAnno

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder pr : rpr -> do

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder when (hasChan || not (null rpr)) $

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder appendDiags [mkDiag Warning "ambiguous matches" idt]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder appendDiags [mkDiag Hint "matched process" idt]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ ACspSymbol $ toProcSymbol (idt, pr)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder _ -> caslAnno

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ProcType p | ck == Implicit ->

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ ACspSymbol $ toProcSymbol (idt, reduce p)

_ -> err

cspSymbToRaw :: Bool -> CspCASLSign -> CspSymbKind -> CspSymb

-> Result CspRawSymbol

cspSymbToRaw b sig k (CspSymb idt mt) = case mt of

Nothing -> return $ case k of

CaslKind Sorts_kind ->

ACspSymbol $ CspSymbol idt $ CaslSymbType SortAsItemType

_ -> CspKindedSymb k idt

Just t -> cspTypedSymbKindToRaw b sig k idt t

cspStatSymbItems :: CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol]

cspStatSymbItems sig sl =

let st (CspSymbItems kind l) = do

appendDiags $ cspCheckSymbList $ map (`CspSymbMap` Nothing) l

mapM (cspSymbToRaw True sig kind) l

in fmap concat (mapM st sl)

maxKind :: CspSymbKind -> CspRawSymbol -> CspSymbKind

maxKind k rs = case k of

CaslKind Implicit -> case rs of

ACspSymbol (CspSymbol _ ty) -> case ty of

ProcAsItemType _ -> ProcessKind

ChanAsItemType _ -> ChannelKind

CaslSymbType cTy -> case cTy of

OpAsItemType _ -> CaslKind Ops_kind

PredAsItemType _ -> CaslKind Preds_kind

_ -> CaslKind Sorts_kind

_ -> k

_ -> k

cspSymbOrMapToRaw :: CspCASLSign -> Maybe CspCASLSign -> CspSymbKind

-> CspSymbMap -> Result [(CspRawSymbol, CspRawSymbol)]

cspSymbOrMapToRaw sig msig k (CspSymbMap s mt) = case mt of

Nothing -> do

v <- cspSymbToRaw True sig k s

return [(v, v)]

Just t -> do

appendDiags $ case (s, t) of

(CspSymb a Nothing, CspSymb b Nothing) | a == b ->

[mkDiag Hint "unneeded identical mapping of" a]

_ -> []

w <- cspSymbToRaw True sig k s

let nk = maxKind k w

x <- case msig of

Nothing -> cspSymbToRaw False sig nk t

Just tsig -> cspSymbToRaw True tsig nk t

let mkS i = ACspSymbol $ CspSymbol i $ CaslSymbType SortAsItemType

pairS s1 s2 = (mkS s1, mkS s2)

case (w, x) of

(ACspSymbol c1@(CspSymbol _ t1), ACspSymbol c2@(CspSymbol _ t2)) ->

case (t1, t2) of

(ChanAsItemType s1, ChanAsItemType s2) ->

return [(w, x), (mkS s1, mkS s2)]

(ProcAsItemType (ProcProfile args1 _),

ProcAsItemType (ProcProfile args2 _))

| length args1 == length args2 ->

return $ (w, x)

: zipWith pairS args1 args2

(CaslSymbType (PredAsItemType (PredType args1)),

CaslSymbType (PredAsItemType (PredType args2)))

| length args1 == length args2 ->

return $ (w, x)

: zipWith pairS args1 args2

(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 of '" ++ showDoc c1 "' and '"

++ showDoc c2 "' do not match"

_ -> return [(w, x)]

cspStatSymbMapItems :: CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems]

-> Result (Map.Map CspRawSymbol CspRawSymbol)

cspStatSymbMapItems sig msig sl = do

let st (CspSymbMapItems kind l) = do

appendDiags $ cspCheckSymbList l

fmap concat $ mapM (cspSymbOrMapToRaw sig msig 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)

getCASLSymbols :: Set.Set CspSymbol -> Set.Set Symbol

getCASLSymbols = Set.fold (\ (CspSymbol i ty) -> case ty of

CaslSymbType t -> Set.insert $ Symbol i t

_ -> id) Set.empty