{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : $Header$

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)

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)

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