{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./CspCASL/Symbol.hs
Description : semantic csp-casl symbols
Copyright : (c) Christian Maeder, DFKI GmbH 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
-}
module CspCASL.Symbol where
import CspCASL.AS_CspCASL_Process
import CspCASL.CspCASL_Keywords
import CspCASL.SignCSP
import CspCASL.SymbItems
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.Sign
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import qualified Common.Lib.MapSet as MapSet
import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad
data CspSymbType
= CaslSymbType SymbType
| ProcAsItemType ProcProfile
| ChanAsItemType Id -- the SORT
deriving (Show, Eq, Ord, Typeable, Data)
instance Pretty CspSymbType where
pretty (CaslSymbType st) = pretty $ symbolKind st
pretty (ProcAsItemType _) = text "process"
pretty (ChanAsItemType _) = text "channel"
data CspSymbol = CspSymbol {cspSymName :: Id, cspSymbType :: CspSymbType}
deriving (Show, Eq, Ord, Typeable, Data)
data CspRawSymbol = ACspSymbol CspSymbol | CspKindedSymb CspSymbKind Id
deriving (Show, Eq, Ord, Typeable, Data)
rawId :: CspRawSymbol -> Id
rawId r = case r of
ACspSymbol s -> cspSymName s
CspKindedSymb _ i -> i
instance Pretty CspSymbol where
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
reduce = reduceProcProfile $ sortRel sig
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, reduce p)
CaslType (A_type s) -> return
$ ACspSymbol $ toProcSymbol
(idt, reduce $ 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
ProcType p | ck == Implicit ->
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)
getCASLSymbols = Set.fold (\ (CspSymbol i ty) -> case ty of
CaslSymbType t -> Set.insert $ Symbol i t
_ -> id) Set.empty