b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett{- |

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettModule : $Header$

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettDescription : semantic csp-casl symbols

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettCopyright : (c) Christian Maeder, DFKI GmbH 2011

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettLicense : GPLv2 or higher, see LICENSE.txt

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettMaintainer : Christian.Maeder@dfki.de

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettStability : provisional

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettPortability : portable

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett-}

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettmodule CspCASL.Symbol where

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport CspCASL.AS_CspCASL_Process

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport CspCASL.CspCASL_Keywords

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport CspCASL.SignCSP

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport CspCASL.SymbItems

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport CASL.AS_Basic_CASL

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport CASL.Morphism

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport CASL.Sign

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Common.Doc

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Common.DocUtils

d64c27888613a81c9634cd939dd05618175465efAndy Gimblettimport Common.Id

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Common.Result

d64c27888613a81c9634cd939dd05618175465efAndy Gimblettimport qualified Common.Lib.MapSet as MapSet

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport qualified Data.Map as Map

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport qualified Data.Set as Set

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport Control.Monad

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettdata CspSymbType

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett = CaslSymbType SymbType

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett | ProcAsItemType ProcProfile

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett | ChanAsItemType Id -- the SORT

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett deriving (Show, Eq, Ord)

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettdata CspSymbol = CspSymbol {cspSymName :: Id, cspSymbType :: CspSymbType}

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett deriving (Show, Eq, Ord)

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

1ac35b084d7e57853f66169d2ca5532977fc403aJens Elknerdata CspRawSymbol = ACspSymbol CspSymbol | CspKindedSymb CspSymbKind Id

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett deriving (Show, Eq, Ord)

c01168f53431b6ad785bf8a8b12bd3a60b93b9b4Andy Gimblett

1ac35b084d7e57853f66169d2ca5532977fc403aJens ElknerrawId :: CspRawSymbol -> Id

c01168f53431b6ad785bf8a8b12bd3a60b93b9b4Andy GimblettrawId r = case r of

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett ACspSymbol s -> cspSymName s

adce8375991a372444ab995895442dca6faf9677Andy Gimblett CspKindedSymb _ i -> i

29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett

29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblettinstance Pretty CspSymbol where

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett pretty (CspSymbol i t) = case t of

ProcAsItemType p -> keyword processS <+> pretty i <+> pretty p

ChanAsItemType s -> keyword channelS <+> pretty i <+> colon <+> pretty s

CaslSymbType c -> pretty $ Symbol i c

instance GetRange CspSymbol where

getRange (CspSymbol i _) = getRange i

instance Pretty CspRawSymbol where

pretty r = case r of

ACspSymbol s -> pretty s

CspKindedSymb k i -> pretty k <+> pretty i

instance GetRange CspRawSymbol where

getRange r = case r of

ACspSymbol s -> getRange s

CspKindedSymb _ i -> getRange i

cspCheckSymbList :: [CspSymbMap] -> [Diagnosis]

cspCheckSymbList l = case l of

CspSymbMap (CspSymb a Nothing) Nothing

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

("profile '" ++ showDoc t "' does not apply to '"

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

_ : r -> cspCheckSymbList r

[] -> []

toChanSymbol :: (CHANNEL_NAME, SORT) -> CspSymbol

toChanSymbol (c, s) = CspSymbol c $ ChanAsItemType s

toProcSymbol :: (PROCESS_NAME, ProcProfile) -> CspSymbol

toProcSymbol (n, p) = CspSymbol n $ ProcAsItemType p

idToCspRaw :: Id -> CspRawSymbol

idToCspRaw = CspKindedSymb $ CaslKind Implicit

sortToProcProfile :: SORT -> ProcProfile

sortToProcProfile = ProcProfile [] . Set.singleton . CommTypeSort

cspTypedSymbKindToRaw :: Bool -> CspCASLSign -> CspSymbKind -> Id -> CspType

-> Result CspRawSymbol

cspTypedSymbKindToRaw b sig k idt t = let

csig = extendedInfo sig

getSet = MapSet.lookup idt

chs = getSet $ chans csig

prs = getSet $ procSet csig

err = plain_error (idToCspRaw idt)

(showDoc idt " " ++ showDoc t

" does not have kind " ++ showDoc k "") nullRange

in case k of

ProcessKind -> case t of

ProcType p -> return $ ACspSymbol $ toProcSymbol (idt, p)

CaslType (A_type s) -> return

$ ACspSymbol $ toProcSymbol

(idt, sortToProcProfile s)

_ -> err

ChannelKind -> case t of

CaslType (A_type s) ->

return $ ACspSymbol $ toChanSymbol (idt, s)

_ -> err

CaslKind ck -> case t of

CaslType ct -> let

caslAnno = fmap (\ r -> case r of

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

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

in case ct of

A_type s | b && ck == Implicit ->

let hasChan = Set.member s chs

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

null args && any (\ cs -> case cs of

CommTypeSort r -> r == s

|| Set.member s (subsortsOf r sig)

CommTypeChan (TypedChanName c _) ->

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

in case Set.toList cprs of

[] -> if hasChan then do

appendDiags [mkDiag Hint "matched channel" idt]

return $ ACspSymbol $ toChanSymbol (idt, s)

else caslAnno

pr : rpr -> do

when (hasChan || not (null rpr)) $

appendDiags [mkDiag Warning "ambiguous matches" idt]

appendDiags [mkDiag Hint "matched process" idt]

return $ ACspSymbol $ toProcSymbol (idt, pr)

_ -> caslAnno

_ -> 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)

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

x <- case msig of

Nothing -> cspSymbToRaw False sig k t

Just tsig -> cspSymbToRaw True tsig k 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)