{-# 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
import qualified Control.Monad.Fail as Fail

data CspSymbType
  = CaslSymbType SymbType
  | ProcAsItemType ProcProfile
  | ChanAsItemType Id -- the SORT
  deriving (Int -> CspSymbType -> ShowS
[CspSymbType] -> ShowS
CspSymbType -> String
(Int -> CspSymbType -> ShowS)
-> (CspSymbType -> String)
-> ([CspSymbType] -> ShowS)
-> Show CspSymbType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CspSymbType] -> ShowS
$cshowList :: [CspSymbType] -> ShowS
show :: CspSymbType -> String
$cshow :: CspSymbType -> String
showsPrec :: Int -> CspSymbType -> ShowS
$cshowsPrec :: Int -> CspSymbType -> ShowS
Show, CspSymbType -> CspSymbType -> Bool
(CspSymbType -> CspSymbType -> Bool)
-> (CspSymbType -> CspSymbType -> Bool) -> Eq CspSymbType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspSymbType -> CspSymbType -> Bool
$c/= :: CspSymbType -> CspSymbType -> Bool
== :: CspSymbType -> CspSymbType -> Bool
$c== :: CspSymbType -> CspSymbType -> Bool
Eq, Eq CspSymbType
Eq CspSymbType =>
(CspSymbType -> CspSymbType -> Ordering)
-> (CspSymbType -> CspSymbType -> Bool)
-> (CspSymbType -> CspSymbType -> Bool)
-> (CspSymbType -> CspSymbType -> Bool)
-> (CspSymbType -> CspSymbType -> Bool)
-> (CspSymbType -> CspSymbType -> CspSymbType)
-> (CspSymbType -> CspSymbType -> CspSymbType)
-> Ord CspSymbType
CspSymbType -> CspSymbType -> Bool
CspSymbType -> CspSymbType -> Ordering
CspSymbType -> CspSymbType -> CspSymbType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CspSymbType -> CspSymbType -> CspSymbType
$cmin :: CspSymbType -> CspSymbType -> CspSymbType
max :: CspSymbType -> CspSymbType -> CspSymbType
$cmax :: CspSymbType -> CspSymbType -> CspSymbType
>= :: CspSymbType -> CspSymbType -> Bool
$c>= :: CspSymbType -> CspSymbType -> Bool
> :: CspSymbType -> CspSymbType -> Bool
$c> :: CspSymbType -> CspSymbType -> Bool
<= :: CspSymbType -> CspSymbType -> Bool
$c<= :: CspSymbType -> CspSymbType -> Bool
< :: CspSymbType -> CspSymbType -> Bool
$c< :: CspSymbType -> CspSymbType -> Bool
compare :: CspSymbType -> CspSymbType -> Ordering
$ccompare :: CspSymbType -> CspSymbType -> Ordering
$cp1Ord :: Eq CspSymbType
Ord, Typeable, Typeable CspSymbType
Constr
DataType
Typeable CspSymbType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspSymbType -> c CspSymbType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspSymbType)
-> (CspSymbType -> Constr)
-> (CspSymbType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspSymbType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c CspSymbType))
-> ((forall b. Data b => b -> b) -> CspSymbType -> CspSymbType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSymbType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSymbType -> r)
-> (forall u. (forall d. Data d => d -> u) -> CspSymbType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CspSymbType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType)
-> Data CspSymbType
CspSymbType -> Constr
CspSymbType -> DataType
(forall b. Data b => b -> b) -> CspSymbType -> CspSymbType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbType -> c CspSymbType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CspSymbType -> u
forall u. (forall d. Data d => d -> u) -> CspSymbType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbType -> c CspSymbType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSymbType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspSymbType)
$cChanAsItemType :: Constr
$cProcAsItemType :: Constr
$cCaslSymbType :: Constr
$tCspSymbType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
gmapMp :: (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
gmapM :: (forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSymbType -> m CspSymbType
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSymbType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CspSymbType -> u
gmapQ :: (forall d. Data d => d -> u) -> CspSymbType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspSymbType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbType -> r
gmapT :: (forall b. Data b => b -> b) -> CspSymbType -> CspSymbType
$cgmapT :: (forall b. Data b => b -> b) -> CspSymbType -> CspSymbType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspSymbType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspSymbType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspSymbType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSymbType)
dataTypeOf :: CspSymbType -> DataType
$cdataTypeOf :: CspSymbType -> DataType
toConstr :: CspSymbType -> Constr
$ctoConstr :: CspSymbType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbType -> c CspSymbType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbType -> c CspSymbType
$cp1Data :: Typeable CspSymbType
Data)

instance Pretty CspSymbType where
 pretty :: CspSymbType -> Doc
pretty (CaslSymbType st :: SymbType
st)  = SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> SYMB_KIND -> Doc
forall a b. (a -> b) -> a -> b
$ SymbType -> SYMB_KIND
symbolKind SymbType
st
 pretty (ProcAsItemType _) = String -> Doc
text "process"
 pretty (ChanAsItemType _) = String -> Doc
text "channel"

data CspSymbol = CspSymbol {CspSymbol -> Id
cspSymName :: Id, CspSymbol -> CspSymbType
cspSymbType :: CspSymbType}
  deriving (Int -> CspSymbol -> ShowS
[CspSymbol] -> ShowS
CspSymbol -> String
(Int -> CspSymbol -> ShowS)
-> (CspSymbol -> String)
-> ([CspSymbol] -> ShowS)
-> Show CspSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CspSymbol] -> ShowS
$cshowList :: [CspSymbol] -> ShowS
show :: CspSymbol -> String
$cshow :: CspSymbol -> String
showsPrec :: Int -> CspSymbol -> ShowS
$cshowsPrec :: Int -> CspSymbol -> ShowS
Show, CspSymbol -> CspSymbol -> Bool
(CspSymbol -> CspSymbol -> Bool)
-> (CspSymbol -> CspSymbol -> Bool) -> Eq CspSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspSymbol -> CspSymbol -> Bool
$c/= :: CspSymbol -> CspSymbol -> Bool
== :: CspSymbol -> CspSymbol -> Bool
$c== :: CspSymbol -> CspSymbol -> Bool
Eq, Eq CspSymbol
Eq CspSymbol =>
(CspSymbol -> CspSymbol -> Ordering)
-> (CspSymbol -> CspSymbol -> Bool)
-> (CspSymbol -> CspSymbol -> Bool)
-> (CspSymbol -> CspSymbol -> Bool)
-> (CspSymbol -> CspSymbol -> Bool)
-> (CspSymbol -> CspSymbol -> CspSymbol)
-> (CspSymbol -> CspSymbol -> CspSymbol)
-> Ord CspSymbol
CspSymbol -> CspSymbol -> Bool
CspSymbol -> CspSymbol -> Ordering
CspSymbol -> CspSymbol -> CspSymbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CspSymbol -> CspSymbol -> CspSymbol
$cmin :: CspSymbol -> CspSymbol -> CspSymbol
max :: CspSymbol -> CspSymbol -> CspSymbol
$cmax :: CspSymbol -> CspSymbol -> CspSymbol
>= :: CspSymbol -> CspSymbol -> Bool
$c>= :: CspSymbol -> CspSymbol -> Bool
> :: CspSymbol -> CspSymbol -> Bool
$c> :: CspSymbol -> CspSymbol -> Bool
<= :: CspSymbol -> CspSymbol -> Bool
$c<= :: CspSymbol -> CspSymbol -> Bool
< :: CspSymbol -> CspSymbol -> Bool
$c< :: CspSymbol -> CspSymbol -> Bool
compare :: CspSymbol -> CspSymbol -> Ordering
$ccompare :: CspSymbol -> CspSymbol -> Ordering
$cp1Ord :: Eq CspSymbol
Ord, Typeable, Typeable CspSymbol
Constr
DataType
Typeable CspSymbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspSymbol -> c CspSymbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspSymbol)
-> (CspSymbol -> Constr)
-> (CspSymbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspSymbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSymbol))
-> ((forall b. Data b => b -> b) -> CspSymbol -> CspSymbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSymbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspSymbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> CspSymbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CspSymbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol)
-> Data CspSymbol
CspSymbol -> Constr
CspSymbol -> DataType
(forall b. Data b => b -> b) -> CspSymbol -> CspSymbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbol -> c CspSymbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CspSymbol -> u
forall u. (forall d. Data d => d -> u) -> CspSymbol -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbol -> c CspSymbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSymbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSymbol)
$cCspSymbol :: Constr
$tCspSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
gmapMp :: (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
gmapM :: (forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspSymbol -> m CspSymbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CspSymbol -> u
gmapQ :: (forall d. Data d => d -> u) -> CspSymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspSymbol -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspSymbol -> r
gmapT :: (forall b. Data b => b -> b) -> CspSymbol -> CspSymbol
$cgmapT :: (forall b. Data b => b -> b) -> CspSymbol -> CspSymbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSymbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspSymbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspSymbol)
dataTypeOf :: CspSymbol -> DataType
$cdataTypeOf :: CspSymbol -> DataType
toConstr :: CspSymbol -> Constr
$ctoConstr :: CspSymbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspSymbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbol -> c CspSymbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspSymbol -> c CspSymbol
$cp1Data :: Typeable CspSymbol
Data)

data CspRawSymbol = ACspSymbol CspSymbol | CspKindedSymb CspSymbKind Id
  deriving (Int -> CspRawSymbol -> ShowS
[CspRawSymbol] -> ShowS
CspRawSymbol -> String
(Int -> CspRawSymbol -> ShowS)
-> (CspRawSymbol -> String)
-> ([CspRawSymbol] -> ShowS)
-> Show CspRawSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CspRawSymbol] -> ShowS
$cshowList :: [CspRawSymbol] -> ShowS
show :: CspRawSymbol -> String
$cshow :: CspRawSymbol -> String
showsPrec :: Int -> CspRawSymbol -> ShowS
$cshowsPrec :: Int -> CspRawSymbol -> ShowS
Show, CspRawSymbol -> CspRawSymbol -> Bool
(CspRawSymbol -> CspRawSymbol -> Bool)
-> (CspRawSymbol -> CspRawSymbol -> Bool) -> Eq CspRawSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CspRawSymbol -> CspRawSymbol -> Bool
$c/= :: CspRawSymbol -> CspRawSymbol -> Bool
== :: CspRawSymbol -> CspRawSymbol -> Bool
$c== :: CspRawSymbol -> CspRawSymbol -> Bool
Eq, Eq CspRawSymbol
Eq CspRawSymbol =>
(CspRawSymbol -> CspRawSymbol -> Ordering)
-> (CspRawSymbol -> CspRawSymbol -> Bool)
-> (CspRawSymbol -> CspRawSymbol -> Bool)
-> (CspRawSymbol -> CspRawSymbol -> Bool)
-> (CspRawSymbol -> CspRawSymbol -> Bool)
-> (CspRawSymbol -> CspRawSymbol -> CspRawSymbol)
-> (CspRawSymbol -> CspRawSymbol -> CspRawSymbol)
-> Ord CspRawSymbol
CspRawSymbol -> CspRawSymbol -> Bool
CspRawSymbol -> CspRawSymbol -> Ordering
CspRawSymbol -> CspRawSymbol -> CspRawSymbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CspRawSymbol -> CspRawSymbol -> CspRawSymbol
$cmin :: CspRawSymbol -> CspRawSymbol -> CspRawSymbol
max :: CspRawSymbol -> CspRawSymbol -> CspRawSymbol
$cmax :: CspRawSymbol -> CspRawSymbol -> CspRawSymbol
>= :: CspRawSymbol -> CspRawSymbol -> Bool
$c>= :: CspRawSymbol -> CspRawSymbol -> Bool
> :: CspRawSymbol -> CspRawSymbol -> Bool
$c> :: CspRawSymbol -> CspRawSymbol -> Bool
<= :: CspRawSymbol -> CspRawSymbol -> Bool
$c<= :: CspRawSymbol -> CspRawSymbol -> Bool
< :: CspRawSymbol -> CspRawSymbol -> Bool
$c< :: CspRawSymbol -> CspRawSymbol -> Bool
compare :: CspRawSymbol -> CspRawSymbol -> Ordering
$ccompare :: CspRawSymbol -> CspRawSymbol -> Ordering
$cp1Ord :: Eq CspRawSymbol
Ord, Typeable, Typeable CspRawSymbol
Constr
DataType
Typeable CspRawSymbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CspRawSymbol -> c CspRawSymbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CspRawSymbol)
-> (CspRawSymbol -> Constr)
-> (CspRawSymbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CspRawSymbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c CspRawSymbol))
-> ((forall b. Data b => b -> b) -> CspRawSymbol -> CspRawSymbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> CspRawSymbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CspRawSymbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol)
-> Data CspRawSymbol
CspRawSymbol -> Constr
CspRawSymbol -> DataType
(forall b. Data b => b -> b) -> CspRawSymbol -> CspRawSymbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspRawSymbol -> c CspRawSymbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspRawSymbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CspRawSymbol -> u
forall u. (forall d. Data d => d -> u) -> CspRawSymbol -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspRawSymbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspRawSymbol -> c CspRawSymbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspRawSymbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspRawSymbol)
$cCspKindedSymb :: Constr
$cACspSymbol :: Constr
$tCspRawSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
gmapMp :: (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
gmapM :: (forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CspRawSymbol -> m CspRawSymbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> CspRawSymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CspRawSymbol -> u
gmapQ :: (forall d. Data d => d -> u) -> CspRawSymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CspRawSymbol -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CspRawSymbol -> r
gmapT :: (forall b. Data b => b -> b) -> CspRawSymbol -> CspRawSymbol
$cgmapT :: (forall b. Data b => b -> b) -> CspRawSymbol -> CspRawSymbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspRawSymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CspRawSymbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CspRawSymbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CspRawSymbol)
dataTypeOf :: CspRawSymbol -> DataType
$cdataTypeOf :: CspRawSymbol -> DataType
toConstr :: CspRawSymbol -> Constr
$ctoConstr :: CspRawSymbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspRawSymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CspRawSymbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspRawSymbol -> c CspRawSymbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CspRawSymbol -> c CspRawSymbol
$cp1Data :: Typeable CspRawSymbol
Data)

rawId :: CspRawSymbol -> Id
rawId :: CspRawSymbol -> Id
rawId r :: CspRawSymbol
r = case CspRawSymbol
r of
  ACspSymbol s :: CspSymbol
s -> CspSymbol -> Id
cspSymName CspSymbol
s
  CspKindedSymb _ i :: Id
i -> Id
i

instance Pretty CspSymbol where
  pretty :: CspSymbol -> Doc
pretty (CspSymbol i :: Id
i t :: CspSymbType
t) = case CspSymbType
t of
    ProcAsItemType p :: ProcProfile
p -> String -> Doc
keyword String
processS Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> ProcProfile -> Doc
forall a. Pretty a => a -> Doc
pretty ProcProfile
p
    ChanAsItemType s :: Id
s -> String -> Doc
keyword String
channelS Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
s
    CaslSymbType c :: SymbType
c -> Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ Id -> SymbType -> Symbol
Symbol Id
i SymbType
c

instance GetRange CspSymbol where
  getRange :: CspSymbol -> Range
getRange (CspSymbol i :: Id
i _) = Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i

instance Pretty CspRawSymbol where
  pretty :: CspRawSymbol -> Doc
pretty r :: CspRawSymbol
r = case CspRawSymbol
r of
    ACspSymbol s :: CspSymbol
s -> CspSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty CspSymbol
s
    CspKindedSymb k :: CspSymbKind
k i :: Id
i -> CspSymbKind -> Doc
forall a. Pretty a => a -> Doc
pretty CspSymbKind
k Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i

instance GetRange CspRawSymbol where
  getRange :: CspRawSymbol -> Range
getRange r :: CspRawSymbol
r = case CspRawSymbol
r of
    ACspSymbol s :: CspSymbol
s -> CspSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspSymbol
s
    CspKindedSymb _ i :: Id
i -> Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i

cspCheckSymbList :: [CspSymbMap] -> [Diagnosis]
cspCheckSymbList :: [CspSymbMap] -> [Diagnosis]
cspCheckSymbList l :: [CspSymbMap]
l = case [CspSymbMap]
l of
  CspSymbMap (CspSymb a :: Id
a Nothing) Nothing
    : CspSymbMap (CspSymb b :: Id
b (Just t :: CspType
t)) _ : r :: [CspSymbMap]
r -> DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
           ("profile '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CspType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CspType
t "' does not apply to '"
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
a "' but only to") Id
b Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [CspSymbMap] -> [Diagnosis]
cspCheckSymbList [CspSymbMap]
r
  _ : r :: [CspSymbMap]
r -> [CspSymbMap] -> [Diagnosis]
cspCheckSymbList [CspSymbMap]
r
  [] -> []

toChanSymbol :: (CHANNEL_NAME, SORT) -> CspSymbol
toChanSymbol :: (Id, Id) -> CspSymbol
toChanSymbol (c :: Id
c, s :: Id
s) = Id -> CspSymbType -> CspSymbol
CspSymbol Id
c (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ Id -> CspSymbType
ChanAsItemType Id
s

toProcSymbol :: (PROCESS_NAME, ProcProfile) -> CspSymbol
toProcSymbol :: (Id, ProcProfile) -> CspSymbol
toProcSymbol (n :: Id
n, p :: ProcProfile
p) = Id -> CspSymbType -> CspSymbol
CspSymbol Id
n (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ ProcProfile -> CspSymbType
ProcAsItemType ProcProfile
p

idToCspRaw :: Id -> CspRawSymbol
idToCspRaw :: Id -> CspRawSymbol
idToCspRaw = CspSymbKind -> Id -> CspRawSymbol
CspKindedSymb (CspSymbKind -> Id -> CspRawSymbol)
-> CspSymbKind -> Id -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Implicit

sortToProcProfile :: SORT -> ProcProfile
sortToProcProfile :: Id -> ProcProfile
sortToProcProfile = PROC_ARGS -> CommAlpha -> ProcProfile
ProcProfile [] (CommAlpha -> ProcProfile)
-> (Id -> CommAlpha) -> Id -> ProcProfile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommType -> CommAlpha
forall a. a -> Set a
Set.singleton (CommType -> CommAlpha) -> (Id -> CommType) -> Id -> CommAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> CommType
CommTypeSort

cspTypedSymbKindToRaw :: Bool -> CspCASLSign -> CspSymbKind -> Id -> CspType
  -> Result CspRawSymbol
cspTypedSymbKindToRaw :: Bool
-> CspCASLSign
-> CspSymbKind
-> Id
-> CspType
-> Result CspRawSymbol
cspTypedSymbKindToRaw b :: Bool
b sig :: CspCASLSign
sig k :: CspSymbKind
k idt :: Id
idt t :: CspType
t = let
    csig :: CspSign
csig = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
    getSet :: MapSet Id b -> Set b
getSet = Id -> MapSet Id b -> Set b
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
idt
    chs :: Set Id
chs = MapSet Id Id -> Set Id
forall b. MapSet Id b -> Set b
getSet (MapSet Id Id -> Set Id) -> MapSet Id Id -> Set Id
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet Id Id
chans CspSign
csig
    prs :: Set ProcProfile
prs = MapSet Id ProcProfile -> Set ProcProfile
forall b. MapSet Id b -> Set b
getSet (MapSet Id ProcProfile -> Set ProcProfile)
-> MapSet Id ProcProfile -> Set ProcProfile
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet Id ProcProfile
procSet CspSign
csig
    reduce :: ProcProfile -> ProcProfile
reduce = Rel Id -> ProcProfile -> ProcProfile
reduceProcProfile (Rel Id -> ProcProfile -> ProcProfile)
-> Rel Id -> ProcProfile -> ProcProfile
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel CspCASLSign
sig
    err :: Result CspRawSymbol
err = CspRawSymbol -> String -> Range -> Result CspRawSymbol
forall a. a -> String -> Range -> Result a
plain_error (Id -> CspRawSymbol
idToCspRaw Id
idt)
              (Id -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Id
idt " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CspType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CspType
t
               " does not have kind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CspSymbKind -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CspSymbKind
k "") Range
nullRange
    in case CspSymbKind
k of
     ProcessKind -> case CspType
t of
       ProcType p :: ProcProfile
p -> CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, ProcProfile) -> CspSymbol
toProcSymbol (Id
idt, ProcProfile -> ProcProfile
reduce ProcProfile
p)
       CaslType (A_type s :: Id
s) -> CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return
         (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, ProcProfile) -> CspSymbol
toProcSymbol
             (Id
idt, ProcProfile -> ProcProfile
reduce (ProcProfile -> ProcProfile) -> ProcProfile -> ProcProfile
forall a b. (a -> b) -> a -> b
$ Id -> ProcProfile
sortToProcProfile Id
s)
       _ -> Result CspRawSymbol
err
     ChannelKind -> case CspType
t of
       CaslType (A_type s :: Id
s) ->
         CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, Id) -> CspSymbol
toChanSymbol (Id
idt, Id
s)
       _ -> Result CspRawSymbol
err
     CaslKind ck :: SYMB_KIND
ck -> case CspType
t of
       CaslType ct :: TYPE
ct -> let
         caslAnno :: Result CspRawSymbol
caslAnno = (RawSymbol -> CspRawSymbol)
-> Result RawSymbol -> Result CspRawSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ r :: RawSymbol
r -> case RawSymbol
r of
           ASymbol sy :: Symbol
sy -> CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> CspSymbType -> CspSymbol
CspSymbol Id
idt (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SymbType -> CspSymbType
CaslSymbType (SymbType -> CspSymbType) -> SymbType -> CspSymbType
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbType
symbType Symbol
sy
           _ -> CspSymbKind -> Id -> CspRawSymbol
CspKindedSymb CspSymbKind
k Id
idt) (Result RawSymbol -> Result CspRawSymbol)
-> Result RawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ Bool -> CspCASLSign -> SYMB_KIND -> Id -> TYPE -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE -> Result RawSymbol
typedSymbKindToRaw Bool
b CspCASLSign
sig SYMB_KIND
ck Id
idt TYPE
ct
         in case TYPE
ct of
         A_type s :: Id
s | Bool
b Bool -> Bool -> Bool
&& SYMB_KIND
ck SYMB_KIND -> SYMB_KIND -> Bool
forall a. Eq a => a -> a -> Bool
== SYMB_KIND
Implicit ->
           let hasChan :: Bool
hasChan = Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
s Set Id
chs
               cprs :: Set ProcProfile
cprs = (ProcProfile -> Bool) -> Set ProcProfile -> Set ProcProfile
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ (ProcProfile args :: PROC_ARGS
args al :: CommAlpha
al) ->
                 PROC_ARGS -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null PROC_ARGS
args Bool -> Bool -> Bool
&& (CommType -> Bool) -> [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ cs :: CommType
cs -> case CommType
cs of
                            CommTypeSort r :: Id
r -> Id
r Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s
                              Bool -> Bool -> Bool
|| Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
s (Id -> CspCASLSign -> Set Id
forall f e. Id -> Sign f e -> Set Id
subsortsOf Id
r CspCASLSign
sig)
                            CommTypeChan (TypedChanName c :: Id
c _) ->
                              Id
c Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s) (CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList CommAlpha
al)) Set ProcProfile
prs
           in case Set ProcProfile -> [ProcProfile]
forall a. Set a -> [a]
Set.toList Set ProcProfile
cprs of
             [] -> if Bool
hasChan then do
                 [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "matched channel" Id
idt]
                 CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, Id) -> CspSymbol
toChanSymbol (Id
idt, Id
s)
               else Result CspRawSymbol
caslAnno
             pr :: ProcProfile
pr : rpr :: [ProcProfile]
rpr -> do
               Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
hasChan Bool -> Bool -> Bool
|| Bool -> Bool
not ([ProcProfile] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProcProfile]
rpr)) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
                 [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "ambiguous matches" Id
idt]
               [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "matched process" Id
idt]
               CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, ProcProfile) -> CspSymbol
toProcSymbol (Id
idt, ProcProfile
pr)
         _ -> Result CspRawSymbol
caslAnno
       ProcType p :: ProcProfile
p | SYMB_KIND
ck SYMB_KIND -> SYMB_KIND -> Bool
forall a. Eq a => a -> a -> Bool
== SYMB_KIND
Implicit ->
         CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (Id, ProcProfile) -> CspSymbol
toProcSymbol (Id
idt, ProcProfile -> ProcProfile
reduce ProcProfile
p)
       _ -> Result CspRawSymbol
err

cspSymbToRaw :: Bool -> CspCASLSign -> CspSymbKind -> CspSymb
  -> Result CspRawSymbol
cspSymbToRaw :: Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw b :: Bool
b sig :: CspCASLSign
sig k :: CspSymbKind
k (CspSymb idt :: Id
idt mt :: Maybe CspType
mt) = case Maybe CspType
mt of
  Nothing -> CspRawSymbol -> Result CspRawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (CspRawSymbol -> Result CspRawSymbol)
-> CspRawSymbol -> Result CspRawSymbol
forall a b. (a -> b) -> a -> b
$ case CspSymbKind
k of
    CaslKind Sorts_kind ->
      CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> CspSymbType -> CspSymbol
CspSymbol Id
idt (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SymbType -> CspSymbType
CaslSymbType SymbType
SortAsItemType
    _ -> CspSymbKind -> Id -> CspRawSymbol
CspKindedSymb CspSymbKind
k Id
idt
  Just t :: CspType
t -> Bool
-> CspCASLSign
-> CspSymbKind
-> Id
-> CspType
-> Result CspRawSymbol
cspTypedSymbKindToRaw Bool
b CspCASLSign
sig CspSymbKind
k Id
idt CspType
t

cspStatSymbItems :: CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol]
cspStatSymbItems :: CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol]
cspStatSymbItems sig :: CspCASLSign
sig sl :: [CspSymbItems]
sl =
  let st :: CspSymbItems -> Result [CspRawSymbol]
st (CspSymbItems kind :: CspSymbKind
kind l :: [CspSymb]
l) = do
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [CspSymbMap] -> [Diagnosis]
cspCheckSymbList ([CspSymbMap] -> [Diagnosis]) -> [CspSymbMap] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ (CspSymb -> CspSymbMap) -> [CspSymb] -> [CspSymbMap]
forall a b. (a -> b) -> [a] -> [b]
map (CspSymb -> Maybe CspSymb -> CspSymbMap
`CspSymbMap` Maybe CspSymb
forall a. Maybe a
Nothing) [CspSymb]
l
        (CspSymb -> Result CspRawSymbol)
-> [CspSymb] -> Result [CspRawSymbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw Bool
True CspCASLSign
sig CspSymbKind
kind) [CspSymb]
l
  in ([[CspRawSymbol]] -> [CspRawSymbol])
-> Result [[CspRawSymbol]] -> Result [CspRawSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[CspRawSymbol]] -> [CspRawSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((CspSymbItems -> Result [CspRawSymbol])
-> [CspSymbItems] -> Result [[CspRawSymbol]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CspSymbItems -> Result [CspRawSymbol]
st [CspSymbItems]
sl)

maxKind :: CspSymbKind -> CspRawSymbol -> CspSymbKind
maxKind :: CspSymbKind -> CspRawSymbol -> CspSymbKind
maxKind k :: CspSymbKind
k rs :: CspRawSymbol
rs = case CspSymbKind
k of
  CaslKind Implicit -> case CspRawSymbol
rs of
    ACspSymbol (CspSymbol _ ty :: CspSymbType
ty) -> case CspSymbType
ty of
      ProcAsItemType _ -> CspSymbKind
ProcessKind
      ChanAsItemType _ -> CspSymbKind
ChannelKind
      CaslSymbType cTy :: SymbType
cTy -> case SymbType
cTy of
        OpAsItemType _ -> SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Ops_kind
        PredAsItemType _ -> SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Preds_kind
        _ -> SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Sorts_kind
    _ -> CspSymbKind
k
  _ -> CspSymbKind
k

cspSymbOrMapToRaw :: CspCASLSign -> Maybe CspCASLSign -> CspSymbKind
  -> CspSymbMap -> Result [(CspRawSymbol, CspRawSymbol)]
cspSymbOrMapToRaw :: CspCASLSign
-> Maybe CspCASLSign
-> CspSymbKind
-> CspSymbMap
-> Result [(CspRawSymbol, CspRawSymbol)]
cspSymbOrMapToRaw sig :: CspCASLSign
sig msig :: Maybe CspCASLSign
msig k :: CspSymbKind
k (CspSymbMap s :: CspSymb
s mt :: Maybe CspSymb
mt) = case Maybe CspSymb
mt of
  Nothing -> do
      CspRawSymbol
v <- Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw Bool
True CspCASLSign
sig CspSymbKind
k CspSymb
s
      [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(CspRawSymbol
v, CspRawSymbol
v)]
  Just t :: CspSymb
t -> do
      [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ case (CspSymb
s, CspSymb
t) of
        (CspSymb a :: Id
a Nothing, CspSymb b :: Id
b Nothing) | Id
a Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
b ->
          [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "unneeded identical mapping of" Id
a]
        _ -> []
      CspRawSymbol
w <- Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw Bool
True CspCASLSign
sig CspSymbKind
k CspSymb
s
      let nk :: CspSymbKind
nk = CspSymbKind -> CspRawSymbol -> CspSymbKind
maxKind CspSymbKind
k CspRawSymbol
w
      CspRawSymbol
x <- case Maybe CspCASLSign
msig of
             Nothing -> Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw Bool
False CspCASLSign
sig CspSymbKind
nk CspSymb
t
             Just tsig :: CspCASLSign
tsig -> Bool
-> CspCASLSign -> CspSymbKind -> CspSymb -> Result CspRawSymbol
cspSymbToRaw Bool
True CspCASLSign
tsig CspSymbKind
nk CspSymb
t
      let mkS :: Id -> CspRawSymbol
mkS i :: Id
i = CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> CspSymbType -> CspSymbol
CspSymbol Id
i (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SymbType -> CspSymbType
CaslSymbType SymbType
SortAsItemType
          pairS :: Id -> Id -> (CspRawSymbol, CspRawSymbol)
pairS s1 :: Id
s1 s2 :: Id
s2 = (Id -> CspRawSymbol
mkS Id
s1, Id -> CspRawSymbol
mkS Id
s2)
      case (CspRawSymbol
w, CspRawSymbol
x) of
        (ACspSymbol c1 :: CspSymbol
c1@(CspSymbol _ t1 :: CspSymbType
t1), ACspSymbol c2 :: CspSymbol
c2@(CspSymbol _ t2 :: CspSymbType
t2)) ->
          case (CspSymbType
t1, CspSymbType
t2) of
            (ChanAsItemType s1 :: Id
s1, ChanAsItemType s2 :: Id
s2) ->
              [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(CspRawSymbol
w, CspRawSymbol
x), (Id -> CspRawSymbol
mkS Id
s1, Id -> CspRawSymbol
mkS Id
s2)]
            (ProcAsItemType (ProcProfile args1 :: PROC_ARGS
args1 _),
             ProcAsItemType (ProcProfile args2 :: PROC_ARGS
args2 _))
              | PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args2 ->
              [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CspRawSymbol, CspRawSymbol)]
 -> Result [(CspRawSymbol, CspRawSymbol)])
-> [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ (CspRawSymbol
w, CspRawSymbol
x)
                (CspRawSymbol, CspRawSymbol)
-> [(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> Id -> (CspRawSymbol, CspRawSymbol))
-> PROC_ARGS -> PROC_ARGS -> [(CspRawSymbol, CspRawSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Id -> Id -> (CspRawSymbol, CspRawSymbol)
pairS PROC_ARGS
args1 PROC_ARGS
args2
            (CaslSymbType (PredAsItemType (PredType args1 :: PROC_ARGS
args1)),
             CaslSymbType (PredAsItemType (PredType args2 :: PROC_ARGS
args2)))
              | PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args2 ->
              [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CspRawSymbol, CspRawSymbol)]
 -> Result [(CspRawSymbol, CspRawSymbol)])
-> [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ (CspRawSymbol
w, CspRawSymbol
x)
                (CspRawSymbol, CspRawSymbol)
-> [(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> Id -> (CspRawSymbol, CspRawSymbol))
-> PROC_ARGS -> PROC_ARGS -> [(CspRawSymbol, CspRawSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Id -> Id -> (CspRawSymbol, CspRawSymbol)
pairS PROC_ARGS
args1 PROC_ARGS
args2
            (CaslSymbType (OpAsItemType (OpType _ args1 :: PROC_ARGS
args1 res1 :: Id
res1)),
             CaslSymbType (OpAsItemType (OpType _ args2 :: PROC_ARGS
args2 res2 :: Id
res2)))
              | PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PROC_ARGS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PROC_ARGS
args2 ->
              [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CspRawSymbol, CspRawSymbol)]
 -> Result [(CspRawSymbol, CspRawSymbol)])
-> [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ (CspRawSymbol
w, CspRawSymbol
x)
                (CspRawSymbol, CspRawSymbol)
-> [(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> Id -> (CspRawSymbol, CspRawSymbol))
-> PROC_ARGS -> PROC_ARGS -> [(CspRawSymbol, CspRawSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Id -> Id -> (CspRawSymbol, CspRawSymbol)
pairS (Id
res1 Id -> PROC_ARGS -> PROC_ARGS
forall a. a -> [a] -> [a]
: PROC_ARGS
args1) (Id
res2 Id -> PROC_ARGS -> PROC_ARGS
forall a. a -> [a] -> [a]
: PROC_ARGS
args2)
            (CaslSymbType SortAsItemType, CaslSymbType SortAsItemType) ->
              [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(CspRawSymbol
w, CspRawSymbol
x)]
            _ -> String -> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [(CspRawSymbol, CspRawSymbol)])
-> String -> Result [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ "profiles of '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CspSymbol -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CspSymbol
c1 "' and '"
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ CspSymbol -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CspSymbol
c2 "' do not match"
        _ -> [(CspRawSymbol, CspRawSymbol)]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(CspRawSymbol
w, CspRawSymbol
x)]

cspStatSymbMapItems :: CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems]
  -> Result (Map.Map CspRawSymbol CspRawSymbol)
cspStatSymbMapItems :: CspCASLSign
-> Maybe CspCASLSign
-> [CspSymbMapItems]
-> Result (Map CspRawSymbol CspRawSymbol)
cspStatSymbMapItems sig :: CspCASLSign
sig msig :: Maybe CspCASLSign
msig sl :: [CspSymbMapItems]
sl = do
  let st :: CspSymbMapItems -> Result [(CspRawSymbol, CspRawSymbol)]
st (CspSymbMapItems kind :: CspSymbKind
kind l :: [CspSymbMap]
l) = do
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [CspSymbMap] -> [Diagnosis]
cspCheckSymbList [CspSymbMap]
l
        ([[(CspRawSymbol, CspRawSymbol)]]
 -> [(CspRawSymbol, CspRawSymbol)])
-> Result [[(CspRawSymbol, CspRawSymbol)]]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(CspRawSymbol, CspRawSymbol)]] -> [(CspRawSymbol, CspRawSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Result [[(CspRawSymbol, CspRawSymbol)]]
 -> Result [(CspRawSymbol, CspRawSymbol)])
-> Result [[(CspRawSymbol, CspRawSymbol)]]
-> Result [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ (CspSymbMap -> Result [(CspRawSymbol, CspRawSymbol)])
-> [CspSymbMap] -> Result [[(CspRawSymbol, CspRawSymbol)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CspCASLSign
-> Maybe CspCASLSign
-> CspSymbKind
-> CspSymbMap
-> Result [(CspRawSymbol, CspRawSymbol)]
cspSymbOrMapToRaw CspCASLSign
sig Maybe CspCASLSign
msig CspSymbKind
kind) [CspSymbMap]
l
      getSort :: CspRawSymbol -> Maybe Id
getSort rsy :: CspRawSymbol
rsy = case CspRawSymbol
rsy of
        ACspSymbol (CspSymbol i :: Id
i (CaslSymbType SortAsItemType)) -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i
        _ -> Maybe Id
forall a. Maybe a
Nothing
      getImplicit :: CspRawSymbol -> Maybe Id
getImplicit rsy :: CspRawSymbol
rsy = case CspRawSymbol
rsy of
        CspKindedSymb (CaslKind Implicit) i :: Id
i -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i
        _ -> Maybe Id
forall a. Maybe a
Nothing
      mkSort :: Id -> CspRawSymbol
mkSort i :: Id
i = CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> CspSymbType -> CspSymbol
CspSymbol Id
i (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SymbType -> CspSymbType
CaslSymbType SymbType
SortAsItemType
      mkImplicit :: Id -> CspRawSymbol
mkImplicit = Id -> CspRawSymbol
idToCspRaw
  [[(CspRawSymbol, CspRawSymbol)]]
ls <- (CspSymbMapItems -> Result [(CspRawSymbol, CspRawSymbol)])
-> [CspSymbMapItems] -> Result [[(CspRawSymbol, CspRawSymbol)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CspSymbMapItems -> Result [(CspRawSymbol, CspRawSymbol)]
st [CspSymbMapItems]
sl
  (Map CspRawSymbol CspRawSymbol
 -> (CspRawSymbol, CspRawSymbol)
 -> Result (Map CspRawSymbol CspRawSymbol))
-> Map CspRawSymbol CspRawSymbol
-> [(CspRawSymbol, CspRawSymbol)]
-> Result (Map CspRawSymbol CspRawSymbol)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((CspRawSymbol -> Id)
-> (CspRawSymbol -> Maybe Id)
-> (Id -> CspRawSymbol)
-> (CspRawSymbol -> Maybe Id)
-> (Id -> CspRawSymbol)
-> Map CspRawSymbol CspRawSymbol
-> (CspRawSymbol, CspRawSymbol)
-> Result (Map CspRawSymbol CspRawSymbol)
forall r.
(Pretty r, GetRange r, Ord r) =>
(r -> Id)
-> (r -> Maybe Id)
-> (Id -> r)
-> (r -> Maybe Id)
-> (Id -> r)
-> Map r r
-> (r, r)
-> Result (Map r r)
insertRsys CspRawSymbol -> Id
rawId CspRawSymbol -> Maybe Id
getSort Id -> CspRawSymbol
mkSort CspRawSymbol -> Maybe Id
getImplicit Id -> CspRawSymbol
mkImplicit)
                    Map CspRawSymbol CspRawSymbol
forall k a. Map k a
Map.empty ([[(CspRawSymbol, CspRawSymbol)]] -> [(CspRawSymbol, CspRawSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(CspRawSymbol, CspRawSymbol)]]
ls)

toSymbolSet :: CspSign -> [Set.Set CspSymbol]
toSymbolSet :: CspSign -> [Set CspSymbol]
toSymbolSet csig :: CspSign
csig = ([CspSymbol] -> Set CspSymbol) -> [[CspSymbol]] -> [Set CspSymbol]
forall a b. (a -> b) -> [a] -> [b]
map [CspSymbol] -> Set CspSymbol
forall a. Ord a => [a] -> Set a
Set.fromList
  [ ((Id, Id) -> CspSymbol) -> [(Id, Id)] -> [CspSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (Id, Id) -> CspSymbol
toChanSymbol ([(Id, Id)] -> [CspSymbol]) -> [(Id, Id)] -> [CspSymbol]
forall a b. (a -> b) -> a -> b
$ MapSet Id Id -> [(Id, Id)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (MapSet Id Id -> [(Id, Id)]) -> MapSet Id Id -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet Id Id
chans CspSign
csig
  , ((Id, ProcProfile) -> CspSymbol)
-> [(Id, ProcProfile)] -> [CspSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (Id, ProcProfile) -> CspSymbol
toProcSymbol ([(Id, ProcProfile)] -> [CspSymbol])
-> [(Id, ProcProfile)] -> [CspSymbol]
forall a b. (a -> b) -> a -> b
$ MapSet Id ProcProfile -> [(Id, ProcProfile)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (MapSet Id ProcProfile -> [(Id, ProcProfile)])
-> MapSet Id ProcProfile -> [(Id, ProcProfile)]
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet Id ProcProfile
procSet CspSign
csig ]

symSets :: CspCASLSign -> [Set.Set CspSymbol]
symSets :: CspCASLSign -> [Set CspSymbol]
symSets sig :: CspCASLSign
sig = (Set Symbol -> Set CspSymbol) -> [Set Symbol] -> [Set CspSymbol]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> CspSymbol) -> Set Symbol -> Set CspSymbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> CspSymbol
caslToCspSymbol) (CspCASLSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf CspCASLSign
sig)
  [Set CspSymbol] -> [Set CspSymbol] -> [Set CspSymbol]
forall a. [a] -> [a] -> [a]
++ CspSign -> [Set CspSymbol]
toSymbolSet (CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig)

caslToCspSymbol :: Symbol -> CspSymbol
caslToCspSymbol :: Symbol -> CspSymbol
caslToCspSymbol sy :: Symbol
sy = Id -> CspSymbType -> CspSymbol
CspSymbol (Symbol -> Id
symName Symbol
sy) (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SymbType -> CspSymbType
CaslSymbType (SymbType -> CspSymbType) -> SymbType -> CspSymbType
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbType
symbType Symbol
sy

-- | try to convert a csp raw symbol to a CASL raw symbol
toRawSymbol :: CspRawSymbol -> Maybe RawSymbol
toRawSymbol :: CspRawSymbol -> Maybe RawSymbol
toRawSymbol r :: CspRawSymbol
r = case CspRawSymbol
r of
  ACspSymbol (CspSymbol i :: Id
i (CaslSymbType t :: SymbType
t)) -> RawSymbol -> Maybe RawSymbol
forall a. a -> Maybe a
Just (Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbType -> Symbol
Symbol Id
i SymbType
t)
  CspKindedSymb (CaslKind k :: SYMB_KIND
k) i :: Id
i -> RawSymbol -> Maybe RawSymbol
forall a. a -> Maybe a
Just (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
k Id
i)
  _ -> Maybe RawSymbol
forall a. Maybe a
Nothing

splitSymbolMap :: Map.Map CspRawSymbol CspRawSymbol
  -> (RawSymbolMap, Map.Map CspRawSymbol CspRawSymbol)
splitSymbolMap :: Map CspRawSymbol CspRawSymbol
-> (RawSymbolMap, Map CspRawSymbol CspRawSymbol)
splitSymbolMap = (CspRawSymbol
 -> CspRawSymbol
 -> (RawSymbolMap, Map CspRawSymbol CspRawSymbol)
 -> (RawSymbolMap, Map CspRawSymbol CspRawSymbol))
-> (RawSymbolMap, Map CspRawSymbol CspRawSymbol)
-> Map CspRawSymbol CspRawSymbol
-> (RawSymbolMap, Map CspRawSymbol CspRawSymbol)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ s :: CspRawSymbol
s t :: CspRawSymbol
t (cm :: RawSymbolMap
cm, ccm :: Map CspRawSymbol CspRawSymbol
ccm) ->
  case (CspRawSymbol -> Maybe RawSymbol
toRawSymbol CspRawSymbol
s, CspRawSymbol -> Maybe RawSymbol
toRawSymbol CspRawSymbol
t) of
    (Just c :: RawSymbol
c, Just d :: RawSymbol
d) -> (RawSymbol -> RawSymbol -> RawSymbolMap -> RawSymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert RawSymbol
c RawSymbol
d RawSymbolMap
cm, Map CspRawSymbol CspRawSymbol
ccm)
    _ -> (RawSymbolMap
cm, CspRawSymbol
-> CspRawSymbol
-> Map CspRawSymbol CspRawSymbol
-> Map CspRawSymbol CspRawSymbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CspRawSymbol
s CspRawSymbol
t Map CspRawSymbol CspRawSymbol
ccm)) (RawSymbolMap
forall k a. Map k a
Map.empty, Map CspRawSymbol CspRawSymbol
forall k a. Map k a
Map.empty)

getCASLSymbols :: Set.Set CspSymbol -> Set.Set Symbol
getCASLSymbols :: Set CspSymbol -> Set Symbol
getCASLSymbols = (CspSymbol -> Set Symbol -> Set Symbol)
-> Set Symbol -> Set CspSymbol -> Set Symbol
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ (CspSymbol i :: Id
i ty :: CspSymbType
ty) -> case CspSymbType
ty of
    CaslSymbType t :: SymbType
t -> Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> Set Symbol -> Set Symbol)
-> Symbol -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbType -> Symbol
Symbol Id
i SymbType
t
    _ -> Set Symbol -> Set Symbol
forall a. a -> a
id) Set Symbol
forall a. Set a
Set.empty