{- |
Module      :  ./CspCASL/SymMapAna.hs
Description :  symbol map analysis for the CspCASL logic.
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.SymMapAna where

import CspCASL.AS_CspCASL_Process
import CspCASL.Morphism
import CspCASL.SignCSP
import CspCASL.SymbItems
import CspCASL.Symbol

import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.SymbolMapAnalysis

import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List (partition)
import Data.Maybe

type CspRawMap = Map.Map CspRawSymbol CspRawSymbol

cspInducedFromToMorphism :: CspRawMap -> ExtSign CspCASLSign CspSymbol
  -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism
cspInducedFromToMorphism :: CspRawMap
-> ExtSign CspCASLSign CspSymbol
-> ExtSign CspCASLSign CspSymbol
-> Result CspCASLMorphism
cspInducedFromToMorphism rmap :: CspRawMap
rmap (ExtSign sSig :: CspCASLSign
sSig sy :: Set CspSymbol
sy) (ExtSign tSig :: CspCASLSign
tSig tSy :: Set CspSymbol
tSy) =
  let (crm :: RawSymbolMap
crm, rm :: CspRawMap
rm) = CspRawMap -> (RawSymbolMap, CspRawMap)
splitSymbolMap CspRawMap
rmap
  in if CspRawMap -> Bool
forall k a. Map k a -> Bool
Map.null CspRawMap
rm then
         InducedSign CspSen CspSign CspAddMorphism CspSign
-> InducedMorphism CspSign CspAddMorphism
-> (CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism)
-> (CspSign -> CspSign -> Bool)
-> (CspSign -> CspSign -> CspSign)
-> RawSymbolMap
-> ExtSign CspCASLSign Symbol
-> ExtSign CspCASLSign Symbol
-> Result CspCASLMorphism
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismExt InducedSign CspSen CspSign CspAddMorphism CspSign
forall f. InducedSign f CspSign CspAddMorphism CspSign
inducedCspSign
         (CspAddMorphism -> InducedMorphism CspSign CspAddMorphism
forall m e. m -> InducedMorphism e m
constMorphExt CspAddMorphism
emptyCspAddMorphism)
         CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism
forall e m f.
MorphismExtension e m =>
Morphism f e m -> Morphism f e m -> Result m
composeMorphismExtension CspSign -> CspSign -> Bool
isCspSubSign CspSign -> CspSign -> CspSign
diffCspSig
         RawSymbolMap
crm (CspCASLSign -> Set Symbol -> ExtSign CspCASLSign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign CspCASLSign
sSig (Set Symbol -> ExtSign CspCASLSign Symbol)
-> Set Symbol -> ExtSign CspCASLSign Symbol
forall a b. (a -> b) -> a -> b
$ Set CspSymbol -> Set Symbol
getCASLSymbols Set CspSymbol
sy)
         (ExtSign CspCASLSign Symbol -> Result CspCASLMorphism)
-> ExtSign CspCASLSign Symbol -> Result CspCASLMorphism
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> Set Symbol -> ExtSign CspCASLSign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign CspCASLSign
tSig (Set Symbol -> ExtSign CspCASLSign Symbol)
-> Set Symbol -> ExtSign CspCASLSign Symbol
forall a b. (a -> b) -> a -> b
$ Set CspSymbol -> Set Symbol
getCASLSymbols Set CspSymbol
tSy
     else do
       CspCASLMorphism
mor <- CspRawMap -> CspCASLSign -> Result CspCASLMorphism
cspInducedFromMorphism CspRawMap
rmap CspCASLSign
sSig
       let iSig :: CspCASLSign
iSig = CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CspCASLMorphism
mor
       if (CspSign -> CspSign -> Bool) -> CspCASLSign -> CspCASLSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig CspSign -> CspSign -> Bool
isCspSubSign CspCASLSign
iSig CspCASLSign
tSig then do
          CspCASLMorphism
incl <- CspAddMorphism
-> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion CspAddMorphism
emptyCspAddMorphism CspCASLSign
iSig CspCASLSign
tSig
          (CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism)
-> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism
forall e f m.
Eq e =>
(Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism
forall e m f.
MorphismExtension e m =>
Morphism f e m -> Morphism f e m -> Result m
composeMorphismExtension CspCASLMorphism
mor CspCASLMorphism
incl
         else
           String -> Range -> Result CspCASLMorphism
forall a. String -> Range -> Result a
fatal_error
         ("No signature morphism for csp symbol map found.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
          "The following mapped symbols are missing in the target signature:\n"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspCASLSign -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((CspSign -> CspSign -> CspSign)
-> CspCASLSign -> CspCASLSign -> CspCASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig CspSign -> CspSign -> CspSign
diffCspSig CspCASLSign
iSig CspCASLSign
tSig) "")
          (Range -> Result CspCASLMorphism)
-> Range -> Result CspCASLMorphism
forall a b. (a -> b) -> a -> b
$ (CspRawSymbol -> Range) -> [CspRawSymbol] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange ([CspRawSymbol] -> Range) -> [CspRawSymbol] -> Range
forall a b. (a -> b) -> a -> b
$ CspRawMap -> [CspRawSymbol]
forall k a. Map k a -> [k]
Map.keys CspRawMap
rmap

cspInducedFromMorphism :: CspRawMap -> CspCASLSign -> Result CspCASLMorphism
cspInducedFromMorphism :: CspRawMap -> CspCASLSign -> Result CspCASLMorphism
cspInducedFromMorphism rmap :: CspRawMap
rmap sigma :: CspCASLSign
sigma = do
  let (crm :: RawSymbolMap
crm, _) = CspRawMap -> (RawSymbolMap, CspRawMap)
splitSymbolMap CspRawMap
rmap
  CspCASLMorphism
m <- CspAddMorphism
-> RawSymbolMap -> CspCASLSign -> Result CspCASLMorphism
forall e f m.
(Pretty e, Show f) =>
m -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism CspAddMorphism
emptyCspAddMorphism RawSymbolMap
crm CspCASLSign
sigma
  let sm :: Sort_map
sm = CspCASLMorphism -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map CspCASLMorphism
m
      om :: Op_map
om = CspCASLMorphism -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CspCASLMorphism
m
      pm :: Pred_map
pm = CspCASLMorphism -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map CspCASLMorphism
m
      csig :: CspSign
csig = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sigma
      newSRel :: Rel SORT
newSRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT)
-> (CspCASLSign -> Rel SORT) -> CspCASLSign -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel (CspCASLSign -> Rel SORT) -> CspCASLSign -> Rel SORT
forall a b. (a -> b) -> a -> b
$ CspCASLMorphism -> CspCASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CspCASLMorphism
m
  -- compute the channel name map (as a Map)
  ChanMap
cm <- (SORT -> Set SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> Map SORT (Set SORT) -> Result ChanMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (CspCASLSign
-> CspRawMap
-> Sort_map
-> SORT
-> Set SORT
-> Result ChanMap
-> Result ChanMap
chanFun CspCASLSign
sigma CspRawMap
rmap Sort_map
sm)
              (ChanMap -> Result ChanMap
forall (m :: * -> *) a. Monad m => a -> m a
return ChanMap
forall k a. Map k a
Map.empty) (MapSet SORT SORT -> Map SORT (Set SORT)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet SORT SORT -> Map SORT (Set SORT))
-> MapSet SORT SORT -> Map SORT (Set SORT)
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet SORT SORT
chans CspSign
csig)
  -- compute the process name map (as a Map)
  ProcessMap
proc_Map <- (SORT -> Set ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap
-> Map SORT (Set ProcProfile)
-> Result ProcessMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (CspCASLSign
-> CspRawMap
-> Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> Set ProcProfile
-> Result ProcessMap
-> Result ProcessMap
procFun CspCASLSign
sigma CspRawMap
rmap Sort_map
sm Rel SORT
newSRel ChanMap
cm)
              (ProcessMap -> Result ProcessMap
forall (m :: * -> *) a. Monad m => a -> m a
return ProcessMap
forall k a. Map k a
Map.empty) (MapSet SORT ProcProfile -> Map SORT (Set ProcProfile)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet SORT ProcProfile -> Map SORT (Set ProcProfile))
-> MapSet SORT ProcProfile -> Map SORT (Set ProcProfile)
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet SORT ProcProfile
procSet CspSign
csig)
  let em :: CspAddMorphism
em = CspAddMorphism
emptyCspAddMorphism
        { channelMap :: ChanMap
channelMap = ChanMap
cm
        , processMap :: ProcessMap
processMap = ProcessMap
proc_Map }
  CspCASLMorphism -> Result CspCASLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (CspAddMorphism -> CspCASLSign -> CspCASLSign -> CspCASLMorphism
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism CspAddMorphism
em CspCASLSign
sigma (CspCASLSign -> CspCASLMorphism) -> CspCASLSign -> CspCASLMorphism
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> CspCASLSign
forall f e. Sign f e -> Sign f e
closeSortRel
          (CspCASLSign -> CspCASLSign) -> CspCASLSign -> CspCASLSign
forall a b. (a -> b) -> a -> b
$ InducedSign CspSen CspSign CspAddMorphism CspSign
-> InducedSign CspSen CspSign CspAddMorphism CspCASLSign
forall f e m. InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux InducedSign CspSen CspSign CspAddMorphism CspSign
forall f. InducedSign f CspSign CspAddMorphism CspSign
inducedCspSign Sort_map
sm Op_map
om Pred_map
pm CspAddMorphism
em CspCASLSign
sigma)
    { sort_map :: Sort_map
sort_map = Sort_map
sm
    , op_map :: Op_map
op_map = Op_map
om
    , pred_map :: Pred_map
pred_map = Pred_map
pm }

chanFun :: CspCASLSign -> CspRawMap -> Sort_map -> Id -> Set.Set SORT
  -> Result ChanMap -> Result ChanMap
chanFun :: CspCASLSign
-> CspRawMap
-> Sort_map
-> SORT
-> Set SORT
-> Result ChanMap
-> Result ChanMap
chanFun sig :: CspCASLSign
sig rmap :: CspRawMap
rmap sm :: Sort_map
sm cn :: SORT
cn ss :: Set SORT
ss m :: Result ChanMap
m =
  let sls :: [Set SORT]
sls = (SORT -> SORT -> Bool) -> Set SORT -> [Set SORT]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (CspCASLSign -> SORT -> SORT -> Bool
relatedSorts CspCASLSign
sig) Set SORT
ss
      m1 :: Result ChanMap
m1 = (Set SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> [Set SORT] -> Result ChanMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CspRawMap
-> Sort_map -> SORT -> Set SORT -> Result ChanMap -> Result ChanMap
directChanMap CspRawMap
rmap Sort_map
sm SORT
cn) Result ChanMap
m [Set SORT]
sls
  in case (CspRawSymbol -> CspRawMap -> Maybe CspRawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CspSymbKind -> SORT -> CspRawSymbol
CspKindedSymb CspSymbKind
ChannelKind SORT
cn) CspRawMap
rmap,
                CspRawSymbol -> CspRawMap -> Maybe CspRawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CspSymbKind -> SORT -> CspRawSymbol
CspKindedSymb (SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Implicit) SORT
cn) CspRawMap
rmap) of
       (Just rsy1 :: CspRawSymbol
rsy1, Just rsy2 :: CspRawSymbol
rsy2) -> let
          m2 :: Result ChanMap
m2 = (SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> Set SORT -> Result ChanMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn CspRawSymbol
rsy1) Result ChanMap
m1 Set SORT
ss
          in (SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> Set SORT -> Result ChanMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn CspRawSymbol
rsy2) Result ChanMap
m2 Set SORT
ss
       (Just rsy :: CspRawSymbol
rsy, Nothing) ->
          (SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> Set SORT -> Result ChanMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn CspRawSymbol
rsy) Result ChanMap
m1 Set SORT
ss
       (Nothing, Just rsy :: CspRawSymbol
rsy) ->
          (SORT -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> Set SORT -> Result ChanMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn CspRawSymbol
rsy) Result ChanMap
m1 Set SORT
ss
       -- Anything not mapped explicitly is left unchanged
       (Nothing, Nothing) -> Result ChanMap
m1

directChanMap :: CspRawMap -> Sort_map -> Id -> Set.Set SORT
  -> Result ChanMap -> Result ChanMap
directChanMap :: CspRawMap
-> Sort_map -> SORT -> Set SORT -> Result ChanMap -> Result ChanMap
directChanMap rmap :: CspRawMap
rmap sm :: Sort_map
sm cn :: SORT
cn ss :: Set SORT
ss m :: Result ChanMap
m =
  let sl :: [SORT]
sl = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
ss
      rl :: [Maybe CspRawSymbol]
rl = (SORT -> Maybe CspRawSymbol) -> [SORT] -> [Maybe CspRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: SORT
s -> CspRawSymbol -> CspRawMap -> Maybe CspRawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspSymbol
toChanSymbol (SORT
cn, SORT
s)) CspRawMap
rmap) [SORT]
sl
      (ms :: [(Maybe CspRawSymbol, SORT)]
ms, ps :: [(Maybe CspRawSymbol, SORT)]
ps) = ((Maybe CspRawSymbol, SORT) -> Bool)
-> [(Maybe CspRawSymbol, SORT)]
-> ([(Maybe CspRawSymbol, SORT)], [(Maybe CspRawSymbol, SORT)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe CspRawSymbol -> Bool
forall a. Maybe a -> Bool
isJust (Maybe CspRawSymbol -> Bool)
-> ((Maybe CspRawSymbol, SORT) -> Maybe CspRawSymbol)
-> (Maybe CspRawSymbol, SORT)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe CspRawSymbol, SORT) -> Maybe CspRawSymbol
forall a b. (a, b) -> a
fst) ([(Maybe CspRawSymbol, SORT)]
 -> ([(Maybe CspRawSymbol, SORT)], [(Maybe CspRawSymbol, SORT)]))
-> [(Maybe CspRawSymbol, SORT)]
-> ([(Maybe CspRawSymbol, SORT)], [(Maybe CspRawSymbol, SORT)])
forall a b. (a -> b) -> a -> b
$ [Maybe CspRawSymbol] -> [SORT] -> [(Maybe CspRawSymbol, SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe CspRawSymbol]
rl [SORT]
sl
  in case [(Maybe CspRawSymbol, SORT)]
ms of
       l :: [(Maybe CspRawSymbol, SORT)]
l@((Just rsy :: CspRawSymbol
rsy, _) : rs :: [(Maybe CspRawSymbol, SORT)]
rs) ->
         ((Maybe CspRawSymbol, SORT) -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> [(Maybe CspRawSymbol, SORT)] -> Result ChanMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, s :: SORT
s) ->
           Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn
              (CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspSymbol
toChanSymbol
               (CspRawSymbol -> SORT
rawId CspRawSymbol
rsy, Sort_map -> SORT -> SORT
mapSort Sort_map
sm SORT
s)) SORT
s)
         (((Maybe CspRawSymbol, SORT) -> Result ChanMap -> Result ChanMap)
-> Result ChanMap -> [(Maybe CspRawSymbol, SORT)] -> Result ChanMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (rsy2 :: Maybe CspRawSymbol
rsy2, s :: SORT
s) ->
           Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym Sort_map
sm SORT
cn (Maybe CspRawSymbol -> CspRawSymbol
forall a. HasCallStack => Maybe a -> a
fromJust Maybe CspRawSymbol
rsy2) SORT
s) Result ChanMap
m [(Maybe CspRawSymbol, SORT)]
l)
         ([(Maybe CspRawSymbol, SORT)] -> Result ChanMap)
-> [(Maybe CspRawSymbol, SORT)] -> Result ChanMap
forall a b. (a -> b) -> a -> b
$ [(Maybe CspRawSymbol, SORT)]
rs [(Maybe CspRawSymbol, SORT)]
-> [(Maybe CspRawSymbol, SORT)] -> [(Maybe CspRawSymbol, SORT)]
forall a. [a] -> [a] -> [a]
++ [(Maybe CspRawSymbol, SORT)]
ps
       _ -> Result ChanMap
m

insertChanSym :: Sort_map -> Id -> CspRawSymbol -> SORT -> Result ChanMap
  -> Result ChanMap
insertChanSym :: Sort_map
-> SORT -> CspRawSymbol -> SORT -> Result ChanMap -> Result ChanMap
insertChanSym sm :: Sort_map
sm cn :: SORT
cn rsy :: CspRawSymbol
rsy s :: SORT
s m :: Result ChanMap
m = do
      ChanMap
m1 <- Result ChanMap
m
      SORT
c1 <- Sort_map -> SORT -> SORT -> CspRawSymbol -> Result SORT
mappedChanSym Sort_map
sm SORT
cn SORT
s CspRawSymbol
rsy
      let ptsy :: CspSymbol
ptsy = SORT -> CspSymbType -> CspSymbol
CspSymbol SORT
cn (CspSymbType -> CspSymbol) -> CspSymbType -> CspSymbol
forall a b. (a -> b) -> a -> b
$ SORT -> CspSymbType
ChanAsItemType SORT
s
          pos :: Range
pos = CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy
          m2 :: ChanMap
m2 = (SORT, SORT) -> SORT -> ChanMap -> ChanMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT
cn, SORT
s) SORT
c1 ChanMap
m1
      case (SORT, SORT) -> ChanMap -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SORT
cn, SORT
s) ChanMap
m1 of
        Nothing -> if SORT
cn SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
c1 then
            case CspRawSymbol
rsy of
              ACspSymbol _ -> ChanMap -> Result ChanMap
forall (m :: * -> *) a. Monad m => a -> m a
return ChanMap
m1
              _ -> ChanMap -> String -> Range -> Result ChanMap
forall a. a -> String -> Range -> Result a
hint ChanMap
m1 ("identity mapping of "
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
ptsy "") Range
pos
            else ChanMap -> Result ChanMap
forall (m :: * -> *) a. Monad m => a -> m a
return ChanMap
m2
        Just c2 :: SORT
c2 -> if SORT
c1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
c2 then
            ChanMap -> String -> Range -> Result ChanMap
forall a. a -> String -> Range -> Result a
warning ChanMap
m1
             ("ignoring duplicate mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
ptsy "") Range
pos
            else ChanMap -> String -> Range -> Result ChanMap
forall a. a -> String -> Range -> Result a
plain_error ChanMap
m1
             ("conflicting mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
ptsy " to " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               SORT -> String
forall a. Show a => a -> String
show SORT
c1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
c2) Range
pos

mappedChanSym :: Sort_map -> Id -> SORT -> CspRawSymbol -> Result Id
mappedChanSym :: Sort_map -> SORT -> SORT -> CspRawSymbol -> Result SORT
mappedChanSym sm :: Sort_map
sm cn :: SORT
cn s :: SORT
s rsy :: CspRawSymbol
rsy =
    let chanSym :: String
chanSym = "channel symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((SORT, SORT) -> CspSymbol
toChanSymbol (SORT
cn, SORT
s))
                  " is mapped to "
    in case CspRawSymbol
rsy of
      ACspSymbol (CspSymbol ide :: SORT
ide (ChanAsItemType s1 :: SORT
s1)) ->
        let s2 :: SORT
s2 = Sort_map -> SORT -> SORT
mapSort Sort_map
sm SORT
s
        in if SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2
           then SORT -> Result SORT
forall (m :: * -> *) a. Monad m => a -> m a
return SORT
ide
           else SORT -> String -> Range -> Result SORT
forall a. a -> String -> Range -> Result a
plain_error SORT
cn
             (String
chanSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "sort " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
s1
              " but should be mapped to type " String -> String -> String
forall a. [a] -> [a] -> [a]
++
              SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
s2 "") (Range -> Result SORT) -> Range -> Result SORT
forall a b. (a -> b) -> a -> b
$ CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy
      CspKindedSymb k :: CspSymbKind
k ide :: SORT
ide | CspSymbKind -> [CspSymbKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem CspSymbKind
k [SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Implicit, CspSymbKind
ChannelKind] ->
        SORT -> Result SORT
forall (m :: * -> *) a. Monad m => a -> m a
return SORT
ide
      _ -> SORT -> String -> Range -> Result SORT
forall a. a -> String -> Range -> Result a
plain_error SORT
cn
               (String
chanSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "symbol of wrong kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspRawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspRawSymbol
rsy "")
               (Range -> Result SORT) -> Range -> Result SORT
forall a b. (a -> b) -> a -> b
$ CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy

procFun :: CspCASLSign -> CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap -> Id
  -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
procFun :: CspCASLSign
-> CspRawMap
-> Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> Set ProcProfile
-> Result ProcessMap
-> Result ProcessMap
procFun sig :: CspCASLSign
sig rmap :: CspRawMap
rmap sm :: Sort_map
sm rel :: Rel SORT
rel cm :: ChanMap
cm pn :: SORT
pn ps :: Set ProcProfile
ps m :: Result ProcessMap
m =
    let pls :: [Set ProcProfile]
pls = (ProcProfile -> ProcProfile -> Bool)
-> Set ProcProfile -> [Set ProcProfile]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (CspCASLSign -> ProcProfile -> ProcProfile -> Bool
relatedProcs CspCASLSign
sig) Set ProcProfile
ps
        m1 :: Result ProcessMap
m1 = (Set ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap -> [Set ProcProfile] -> Result ProcessMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CspRawMap
-> Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> Set ProcProfile
-> Result ProcessMap
-> Result ProcessMap
directProcMap CspRawMap
rmap Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn) Result ProcessMap
m [Set ProcProfile]
pls
    -- now try the remaining ones with (un)kinded raw symbol
    in case (CspRawSymbol -> CspRawMap -> Maybe CspRawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CspSymbKind -> SORT -> CspRawSymbol
CspKindedSymb CspSymbKind
ProcessKind SORT
pn) CspRawMap
rmap,
                CspRawSymbol -> CspRawMap -> Maybe CspRawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CspSymbKind -> SORT -> CspRawSymbol
CspKindedSymb (SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Implicit) SORT
pn) CspRawMap
rmap) of
       (Just rsy1 :: CspRawSymbol
rsy1, Just rsy2 :: CspRawSymbol
rsy2) -> let
          m2 :: Result ProcessMap
m2 = (ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap -> Set ProcProfile -> Result ProcessMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn CspRawSymbol
rsy1) Result ProcessMap
m1 Set ProcProfile
ps
          in (ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap -> Set ProcProfile -> Result ProcessMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn CspRawSymbol
rsy2) Result ProcessMap
m2 Set ProcProfile
ps
       (Just rsy :: CspRawSymbol
rsy, Nothing) ->
          (ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap -> Set ProcProfile -> Result ProcessMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn CspRawSymbol
rsy) Result ProcessMap
m1 Set ProcProfile
ps
       (Nothing, Just rsy :: CspRawSymbol
rsy) ->
          (ProcProfile -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap -> Set ProcProfile -> Result ProcessMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn CspRawSymbol
rsy) Result ProcessMap
m1 Set ProcProfile
ps
       -- Anything not mapped explicitly is left unchanged
       (Nothing, Nothing) -> Result ProcessMap
m1

directProcMap :: CspRawMap -> Sort_map -> Rel.Rel SORT -> ChanMap
  -> Id -> Set.Set ProcProfile -> Result ProcessMap -> Result ProcessMap
directProcMap :: CspRawMap
-> Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> Set ProcProfile
-> Result ProcessMap
-> Result ProcessMap
directProcMap rmap :: CspRawMap
rmap sm :: Sort_map
sm rel :: Rel SORT
rel cm :: ChanMap
cm pn :: SORT
pn ps :: Set ProcProfile
ps m :: Result ProcessMap
m =
  let pl :: [ProcProfile]
pl = Set ProcProfile -> [ProcProfile]
forall a. Set a -> [a]
Set.toList Set ProcProfile
ps
      rl :: [Maybe CspRawSymbol]
rl = (ProcProfile -> Maybe CspRawSymbol)
-> [ProcProfile] -> [Maybe CspRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (CspRawMap -> SORT -> ProcProfile -> Maybe CspRawSymbol
lookupProcSymbol CspRawMap
rmap SORT
pn) [ProcProfile]
pl
      (ms :: [(Maybe CspRawSymbol, ProcProfile)]
ms, os :: [(Maybe CspRawSymbol, ProcProfile)]
os) = ((Maybe CspRawSymbol, ProcProfile) -> Bool)
-> [(Maybe CspRawSymbol, ProcProfile)]
-> ([(Maybe CspRawSymbol, ProcProfile)],
    [(Maybe CspRawSymbol, ProcProfile)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe CspRawSymbol -> Bool
forall a. Maybe a -> Bool
isJust (Maybe CspRawSymbol -> Bool)
-> ((Maybe CspRawSymbol, ProcProfile) -> Maybe CspRawSymbol)
-> (Maybe CspRawSymbol, ProcProfile)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe CspRawSymbol, ProcProfile) -> Maybe CspRawSymbol
forall a b. (a, b) -> a
fst) ([(Maybe CspRawSymbol, ProcProfile)]
 -> ([(Maybe CspRawSymbol, ProcProfile)],
     [(Maybe CspRawSymbol, ProcProfile)]))
-> [(Maybe CspRawSymbol, ProcProfile)]
-> ([(Maybe CspRawSymbol, ProcProfile)],
    [(Maybe CspRawSymbol, ProcProfile)])
forall a b. (a -> b) -> a -> b
$ [Maybe CspRawSymbol]
-> [ProcProfile] -> [(Maybe CspRawSymbol, ProcProfile)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe CspRawSymbol]
rl [ProcProfile]
pl
  in case [(Maybe CspRawSymbol, ProcProfile)]
ms of
       l :: [(Maybe CspRawSymbol, ProcProfile)]
l@((Just rsy :: CspRawSymbol
rsy, _) : rs :: [(Maybe CspRawSymbol, ProcProfile)]
rs) ->
         ((Maybe CspRawSymbol, ProcProfile)
 -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap
-> [(Maybe CspRawSymbol, ProcProfile)]
-> Result ProcessMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, p :: ProcProfile
p) ->
           Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn
              (CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (SORT, ProcProfile) -> CspSymbol
toProcSymbol
                (CspRawSymbol -> SORT
rawId CspRawSymbol
rsy, Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile Sort_map
sm ChanMap
cm ProcProfile
p)) ProcProfile
p)
         (((Maybe CspRawSymbol, ProcProfile)
 -> Result ProcessMap -> Result ProcessMap)
-> Result ProcessMap
-> [(Maybe CspRawSymbol, ProcProfile)]
-> Result ProcessMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (rsy2 :: Maybe CspRawSymbol
rsy2, p :: ProcProfile
p) ->
           Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn (Maybe CspRawSymbol -> CspRawSymbol
forall a. HasCallStack => Maybe a -> a
fromJust Maybe CspRawSymbol
rsy2) ProcProfile
p) Result ProcessMap
m [(Maybe CspRawSymbol, ProcProfile)]
l)
         ([(Maybe CspRawSymbol, ProcProfile)] -> Result ProcessMap)
-> [(Maybe CspRawSymbol, ProcProfile)] -> Result ProcessMap
forall a b. (a -> b) -> a -> b
$ [(Maybe CspRawSymbol, ProcProfile)]
rs [(Maybe CspRawSymbol, ProcProfile)]
-> [(Maybe CspRawSymbol, ProcProfile)]
-> [(Maybe CspRawSymbol, ProcProfile)]
forall a. [a] -> [a] -> [a]
++ [(Maybe CspRawSymbol, ProcProfile)]
os
       _ -> Result ProcessMap
m

lookupProcSymbol :: CspRawMap -> Id -> ProcProfile
  -> Maybe CspRawSymbol
lookupProcSymbol :: CspRawMap -> SORT -> ProcProfile -> Maybe CspRawSymbol
lookupProcSymbol rmap :: CspRawMap
rmap pn :: SORT
pn p :: ProcProfile
p = case
  ((CspRawSymbol, CspRawSymbol) -> Bool)
-> [(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (k :: CspRawSymbol
k, _) -> case CspRawSymbol
k of
    ACspSymbol (CspSymbol i :: SORT
i (ProcAsItemType pf :: ProcProfile
pf)) ->
      SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
pn Bool -> Bool -> Bool
&& ProcProfile -> ProcProfile -> Bool
matchProcTypes ProcProfile
p ProcProfile
pf
    _ -> Bool
False) ([(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)])
-> [(CspRawSymbol, CspRawSymbol)] -> [(CspRawSymbol, CspRawSymbol)]
forall a b. (a -> b) -> a -> b
$ CspRawMap -> [(CspRawSymbol, CspRawSymbol)]
forall k a. Map k a -> [(k, a)]
Map.toList CspRawMap
rmap of
  [(_, r :: CspRawSymbol
r)] -> CspRawSymbol -> Maybe CspRawSymbol
forall a. a -> Maybe a
Just CspRawSymbol
r
  [] -> Maybe CspRawSymbol
forall a. Maybe a
Nothing
       -- in case of ambiguities try to find an exact match
  l :: [(CspRawSymbol, CspRawSymbol)]
l -> CspRawSymbol
-> [(CspRawSymbol, CspRawSymbol)] -> Maybe CspRawSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (CspSymbol -> CspRawSymbol
ACspSymbol (CspSymbol -> CspRawSymbol) -> CspSymbol -> CspRawSymbol
forall a b. (a -> b) -> a -> b
$ (SORT, ProcProfile) -> CspSymbol
toProcSymbol (SORT
pn, ProcProfile
p)) [(CspRawSymbol, CspRawSymbol)]
l

insertProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id -> CspRawSymbol
  -> ProcProfile -> Result ProcessMap -> Result ProcessMap
insertProcSym :: Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> CspRawSymbol
-> ProcProfile
-> Result ProcessMap
-> Result ProcessMap
insertProcSym sm :: Sort_map
sm rel :: Rel SORT
rel cm :: ChanMap
cm pn :: SORT
pn rsy :: CspRawSymbol
rsy pf :: ProcProfile
pf@(ProcProfile _ al :: CommAlpha
al) m :: Result ProcessMap
m = do
      ProcessMap
m1 <- Result ProcessMap
m
      (p1 :: SORT
p1, al1 :: CommAlpha
al1) <- Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> ProcProfile
-> CspRawSymbol
-> Result (SORT, CommAlpha)
mappedProcSym Sort_map
sm Rel SORT
rel ChanMap
cm SORT
pn ProcProfile
pf CspRawSymbol
rsy
      let otsy :: CspSymbol
otsy = (SORT, ProcProfile) -> CspSymbol
toProcSymbol (SORT
pn, ProcProfile
pf)
          pos :: Range
pos = CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy
          m2 :: ProcessMap
m2 = (SORT, ProcProfile) -> SORT -> ProcessMap -> ProcessMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT
pn, ProcProfile
pf) SORT
p1 ProcessMap
m1
      case (SORT, ProcProfile) -> ProcessMap -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SORT
pn, ProcProfile
pf) ProcessMap
m1 of
        Nothing -> if SORT
pn SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
p1 Bool -> Bool -> Bool
&& CommAlpha
al CommAlpha -> CommAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== CommAlpha
al1 then
            case CspRawSymbol
rsy of
              ACspSymbol _ -> ProcessMap -> Result ProcessMap
forall (m :: * -> *) a. Monad m => a -> m a
return ProcessMap
m1
              _ -> ProcessMap -> String -> Range -> Result ProcessMap
forall a. a -> String -> Range -> Result a
hint ProcessMap
m1 ("identity mapping of "
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
otsy "") Range
pos
            else ProcessMap -> Result ProcessMap
forall (m :: * -> *) a. Monad m => a -> m a
return ProcessMap
m2
        Just p2 :: SORT
p2 -> if SORT
p1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
p2 then
             ProcessMap -> String -> Range -> Result ProcessMap
forall a. a -> String -> Range -> Result a
warning ProcessMap
m1
             ("ignoring duplicate mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
otsy "")
             Range
pos
            else ProcessMap -> String -> Range -> Result ProcessMap
forall a. a -> String -> Range -> Result a
plain_error ProcessMap
m1
             ("conflicting mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspSymbol
otsy " to " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               SORT -> String
forall a. Show a => a -> String
show SORT
p1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
p2) Range
pos

mappedProcSym :: Sort_map -> Rel.Rel SORT -> ChanMap -> Id
  -> ProcProfile -> CspRawSymbol -> Result (Id, CommAlpha)
mappedProcSym :: Sort_map
-> Rel SORT
-> ChanMap
-> SORT
-> ProcProfile
-> CspRawSymbol
-> Result (SORT, CommAlpha)
mappedProcSym sm :: Sort_map
sm rel :: Rel SORT
rel cm :: ChanMap
cm pn :: SORT
pn pfSrc :: ProcProfile
pfSrc rsy :: CspRawSymbol
rsy =
    let procSym :: String
procSym = "process symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((SORT, ProcProfile) -> CspSymbol
toProcSymbol (SORT
pn, ProcProfile
pfSrc))
                " is mapped to "
        pfMapped :: ProcProfile
pfMapped@(ProcProfile _ al2 :: CommAlpha
al2) = Rel SORT -> ProcProfile -> ProcProfile
reduceProcProfile Rel SORT
rel
          (ProcProfile -> ProcProfile) -> ProcProfile -> ProcProfile
forall a b. (a -> b) -> a -> b
$ Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile Sort_map
sm ChanMap
cm ProcProfile
pfSrc
    in case CspRawSymbol
rsy of
      ACspSymbol (CspSymbol ide :: SORT
ide (ProcAsItemType pf :: ProcProfile
pf)) ->
        let pfTar :: ProcProfile
pfTar@(ProcProfile _ al1 :: CommAlpha
al1) = Rel SORT -> ProcProfile -> ProcProfile
reduceProcProfile Rel SORT
rel ProcProfile
pf
        in if Rel SORT -> ProcProfile -> ProcProfile -> Bool
compatibleProcTypes Rel SORT
rel ProcProfile
pfMapped ProcProfile
pfTar
           then (SORT, CommAlpha) -> Result (SORT, CommAlpha)
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT
ide, CommAlpha
al1)
           else (SORT, CommAlpha) -> String -> Range -> Result (SORT, CommAlpha)
forall a. a -> String -> Range -> Result a
plain_error (SORT
pn, CommAlpha
al2)
             (String
procSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ProcProfile -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ProcProfile
pfTar
              "\nbut should be mapped to type " String -> String -> String
forall a. [a] -> [a] -> [a]
++
              ProcProfile -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ProcProfile
pfMapped
              "\npossibly using a sub-alphabet of " String -> String -> String
forall a. [a] -> [a] -> [a]
++
              CommAlpha -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (Rel SORT -> CommAlpha -> CommAlpha
closeCspCommAlpha Rel SORT
rel CommAlpha
al2) ".")
             (Range -> Result (SORT, CommAlpha))
-> Range -> Result (SORT, CommAlpha)
forall a b. (a -> b) -> a -> b
$ CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy
      CspKindedSymb k :: CspSymbKind
k ide :: SORT
ide | CspSymbKind -> [CspSymbKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem CspSymbKind
k [SYMB_KIND -> CspSymbKind
CaslKind SYMB_KIND
Implicit, CspSymbKind
ProcessKind] ->
        (SORT, CommAlpha) -> Result (SORT, CommAlpha)
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT
ide, CommAlpha
al2)
      _ -> (SORT, CommAlpha) -> String -> Range -> Result (SORT, CommAlpha)
forall a. a -> String -> Range -> Result a
plain_error (SORT
pn, CommAlpha
al2)
               (String
procSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "symbol of wrong kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CspRawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc CspRawSymbol
rsy "")
               (Range -> Result (SORT, CommAlpha))
-> Range -> Result (SORT, CommAlpha)
forall a b. (a -> b) -> a -> b
$ CspRawSymbol -> Range
forall a. GetRange a => a -> Range
getRange CspRawSymbol
rsy

compatibleProcTypes :: Rel.Rel SORT -> ProcProfile -> ProcProfile -> Bool
compatibleProcTypes :: Rel SORT -> ProcProfile -> ProcProfile -> Bool
compatibleProcTypes rel :: Rel SORT
rel (ProcProfile l1 :: [SORT]
l1 al1 :: CommAlpha
al1) (ProcProfile l2 :: [SORT]
l2 al2 :: CommAlpha
al2) =
  [SORT]
l1 [SORT] -> [SORT] -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT]
l2 Bool -> Bool -> Bool
&& Rel SORT -> CommAlpha -> CommAlpha -> Bool
liamsRelatedCommAlpha Rel SORT
rel CommAlpha
al1 CommAlpha
al2

liamsRelatedCommAlpha :: Rel.Rel SORT -> CommAlpha -> CommAlpha -> Bool
liamsRelatedCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha -> Bool
liamsRelatedCommAlpha rel :: Rel SORT
rel al1 :: CommAlpha
al1 al2 :: CommAlpha
al2 =
  (CommType -> Bool) -> [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ a2 :: CommType
a2 -> (CommType -> Bool) -> [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a1 :: CommType
a1 -> Rel SORT -> CommType -> CommType -> Bool
liamsRelatedCommTypes Rel SORT
rel CommType
a1 CommType
a2) ([CommType] -> Bool) -> [CommType] -> Bool
forall a b. (a -> b) -> a -> b
$ CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList CommAlpha
al1)
  ([CommType] -> Bool) -> [CommType] -> Bool
forall a b. (a -> b) -> a -> b
$ CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList CommAlpha
al2

liamsRelatedCommTypes :: Rel.Rel SORT -> CommType -> CommType -> Bool
liamsRelatedCommTypes :: Rel SORT -> CommType -> CommType -> Bool
liamsRelatedCommTypes rel :: Rel SORT
rel ct1 :: CommType
ct1 ct2 :: CommType
ct2 = case (CommType
ct1, CommType
ct2) of
  (CommTypeSort s1 :: SORT
s1, CommTypeSort s2 :: SORT
s2)
    -> SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2 Bool -> Bool -> Bool
|| SORT
s1 SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Rel SORT -> SORT -> Set SORT
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel SORT
rel SORT
s2
  (CommTypeChan (TypedChanName c1 :: SORT
c1 s1 :: SORT
s1), CommTypeChan (TypedChanName c2 :: SORT
c2 s2 :: SORT
s2))
    -> SORT
c1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
c2 Bool -> Bool -> Bool
&& SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2
  _ -> Bool
False

matchProcTypes :: ProcProfile -> ProcProfile -> Bool
matchProcTypes :: ProcProfile -> ProcProfile -> Bool
matchProcTypes (ProcProfile l1 :: [SORT]
l1 al1 :: CommAlpha
al1) (ProcProfile l2 :: [SORT]
l2 al2 :: CommAlpha
al2) = [SORT]
l1 [SORT] -> [SORT] -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT]
l2
  Bool -> Bool -> Bool
&& (CommAlpha -> Bool
forall a. Set a -> Bool
Set.null CommAlpha
al2 Bool -> Bool -> Bool
|| CommAlpha -> Bool
forall a. Set a -> Bool
Set.null CommAlpha
al1 Bool -> Bool -> Bool
|| Bool -> Bool
not (CommAlpha -> Bool
forall a. Set a -> Bool
Set.null (CommAlpha -> Bool) -> CommAlpha -> Bool
forall a b. (a -> b) -> a -> b
$ CommAlpha -> CommAlpha -> CommAlpha
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection CommAlpha
al1 CommAlpha
al2))

cspMatches :: CspSymbol -> CspRawSymbol -> Bool
cspMatches :: CspSymbol -> CspRawSymbol -> Bool
cspMatches (CspSymbol i :: SORT
i t :: CspSymbType
t) rsy :: CspRawSymbol
rsy = case CspRawSymbol
rsy of
  ACspSymbol (CspSymbol j :: SORT
j t2 :: CspSymbType
t2) -> SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
j Bool -> Bool -> Bool
&& case (CspSymbType
t, CspSymbType
t2) of
    (CaslSymbType t1 :: SymbType
t1, CaslSymbType t3 :: SymbType
t3) -> Symbol -> RawSymbol -> Bool
matches (SORT -> SymbType -> Symbol
Symbol SORT
i SymbType
t1)
      (RawSymbol -> Bool) -> RawSymbol -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ SORT -> SymbType -> Symbol
Symbol SORT
j SymbType
t3
    (ChanAsItemType s1 :: SORT
s1, ChanAsItemType s2 :: SORT
s2) -> SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2
    (ProcAsItemType p1 :: ProcProfile
p1, ProcAsItemType p2 :: ProcProfile
p2) -> ProcProfile -> ProcProfile -> Bool
matchProcTypes ProcProfile
p1 ProcProfile
p2
    _ -> Bool
False
  CspKindedSymb k :: CspSymbKind
k j :: SORT
j -> let res :: Bool
res = SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
j in case (CspSymbKind
k, CspSymbType
t) of
    (CaslKind ck :: SYMB_KIND
ck, CaslSymbType t1 :: SymbType
t1) -> Symbol -> RawSymbol -> Bool
matches (SORT -> SymbType -> Symbol
Symbol SORT
i SymbType
t1)
      (RawSymbol -> Bool) -> RawSymbol -> Bool
forall a b. (a -> b) -> a -> b
$ SYMB_KIND -> SORT -> RawSymbol
AKindedSymb SYMB_KIND
ck SORT
j
    (ChannelKind, ChanAsItemType _) -> Bool
res
    (ProcessKind, ProcAsItemType _) -> Bool
res
    (CaslKind Implicit, _) -> Bool
res
    _ -> Bool
False

procProfile2Sorts :: ProcProfile -> Set.Set SORT
procProfile2Sorts :: ProcProfile -> Set SORT
procProfile2Sorts (ProcProfile sorts :: [SORT]
sorts al :: CommAlpha
al) =
  Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT]
sorts) (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ (CommType -> SORT) -> CommAlpha -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map CommType -> SORT
commType2Sort CommAlpha
al

cspRevealSym :: CspSymbol -> CspCASLSign -> CspCASLSign
cspRevealSym :: CspSymbol -> CspCASLSign -> CspCASLSign
cspRevealSym sy :: CspSymbol
sy sig :: CspCASLSign
sig = let
  n :: SORT
n = CspSymbol -> SORT
cspSymName CspSymbol
sy
  r :: Rel SORT
r = CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CspCASLSign
sig
  ext :: CspSign
ext = CspCASLSign -> CspSign
forall f e. Sign f e -> e
extendedInfo CspCASLSign
sig
  cs :: MapSet SORT SORT
cs = CspSign -> MapSet SORT SORT
chans CspSign
ext
  in case CspSymbol -> CspSymbType
cspSymbType CspSymbol
sy of
    CaslSymbType t :: SymbType
t -> Symbol -> CspCASLSign -> CspCASLSign
forall f e. Symbol -> Sign f e -> Sign f e
revealSym (SORT -> SymbType -> Symbol
Symbol SORT
n SymbType
t) CspCASLSign
sig
    ChanAsItemType s :: SORT
s -> CspCASLSign
sig
      { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
s Rel SORT
r
      , extendedInfo :: CspSign
extendedInfo = CspSign
ext { chans :: MapSet SORT SORT
chans = SORT -> SORT -> MapSet SORT SORT -> MapSet SORT SORT
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
n SORT
s MapSet SORT SORT
cs }}
    ProcAsItemType p :: ProcProfile
p@(ProcProfile _ al :: CommAlpha
al) -> CspCASLSign
sig
      { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (Set SORT -> Rel SORT
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet (Set SORT -> Rel SORT) -> Set SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ ProcProfile -> Set SORT
procProfile2Sorts ProcProfile
p) Rel SORT
r
      , extendedInfo :: CspSign
extendedInfo = CspSign
ext
        { chans :: MapSet SORT SORT
chans = (CommType -> MapSet SORT SORT -> MapSet SORT SORT)
-> MapSet SORT SORT -> CommAlpha -> MapSet SORT SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ ct :: CommType
ct -> case CommType
ct of
            CommTypeSort _ -> MapSet SORT SORT -> MapSet SORT SORT
forall a. a -> a
id
            CommTypeChan (TypedChanName c :: SORT
c s :: SORT
s) -> SORT -> SORT -> MapSet SORT SORT -> MapSet SORT SORT
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
c SORT
s) MapSet SORT SORT
cs CommAlpha
al
        , procSet :: MapSet SORT ProcProfile
procSet = SORT
-> ProcProfile
-> MapSet SORT ProcProfile
-> MapSet SORT ProcProfile
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
n ProcProfile
p (MapSet SORT ProcProfile -> MapSet SORT ProcProfile)
-> MapSet SORT ProcProfile -> MapSet SORT ProcProfile
forall a b. (a -> b) -> a -> b
$ CspSign -> MapSet SORT ProcProfile
procSet CspSign
ext }
      }

cspGeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspGeneratedSign :: Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspGeneratedSign sys :: Set CspSymbol
sys sigma :: CspCASLSign
sigma = let
  symset :: Set CspSymbol
symset = [Set CspSymbol] -> Set CspSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set CspSymbol] -> Set CspSymbol)
-> [Set CspSymbol] -> Set CspSymbol
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> [Set CspSymbol]
symSets CspCASLSign
sigma
  sigma1 :: CspCASLSign
sigma1 = (CspSymbol -> CspCASLSign -> CspCASLSign)
-> CspCASLSign -> Set CspSymbol -> CspCASLSign
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold CspSymbol -> CspCASLSign -> CspCASLSign
cspRevealSym CspCASLSign
sigma
    { sortRel :: Rel SORT
sortRel = Rel SORT
forall a. Rel a
Rel.empty
    , opMap :: OpMap
opMap = OpMap
forall a b. MapSet a b
MapSet.empty
    , predMap :: PredMap
predMap = PredMap
forall a b. MapSet a b
MapSet.empty
    , extendedInfo :: CspSign
extendedInfo = CspSign
emptyCspSign } Set CspSymbol
sys
  sigma2 :: CspCASLSign
sigma2 = CspCASLSign
sigma1
    { sortRel :: Rel SORT
sortRel = CspCASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CspCASLSign
sigma Rel SORT -> Set SORT -> Rel SORT
forall a. Ord a => Rel a -> Set a -> Rel a
`Rel.restrict` CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CspCASLSign
sigma1
    , emptySortSet :: Set SORT
emptySortSet = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CspCASLSign
sigma1) (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet CspCASLSign
sigma }
  in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set CspSymbol -> Set CspSymbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set CspSymbol
sys Set CspSymbol
symset
   then let diffsyms :: Set CspSymbol
diffsyms = Set CspSymbol
sys Set CspSymbol -> Set CspSymbol -> Set CspSymbol
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set CspSymbol
symset in
        String -> Range -> Result CspCASLMorphism
forall a. String -> Range -> Result a
fatal_error ("Revealing: The following symbols "
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set CspSymbol
diffsyms " are not in the signature")
        (Range -> Result CspCASLMorphism)
-> Range -> Result CspCASLMorphism
forall a b. (a -> b) -> a -> b
$ Set CspSymbol -> Range
forall a. GetRange a => a -> Range
getRange Set CspSymbol
diffsyms
   else CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
cspSubsigInclusion CspCASLSign
sigma2 CspCASLSign
sigma

cspCogeneratedSign :: Set.Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspCogeneratedSign :: Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspCogeneratedSign symset :: Set CspSymbol
symset sigma :: CspCASLSign
sigma = let
  symset0 :: Set CspSymbol
symset0 = [Set CspSymbol] -> Set CspSymbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set CspSymbol] -> Set CspSymbol)
-> [Set CspSymbol] -> Set CspSymbol
forall a b. (a -> b) -> a -> b
$ CspCASLSign -> [Set CspSymbol]
symSets CspCASLSign
sigma
  symset1 :: Set CspSymbol
symset1 = (CspSymbol -> Set CspSymbol -> Set CspSymbol)
-> Set CspSymbol -> Set CspSymbol -> Set CspSymbol
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold CspSymbol -> Set CspSymbol -> Set CspSymbol
cspHideSym Set CspSymbol
symset0 Set CspSymbol
symset
  in if Set CspSymbol -> Set CspSymbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set CspSymbol
symset Set CspSymbol
symset0
   then Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspGeneratedSign Set CspSymbol
symset1 CspCASLSign
sigma
   else let diffsyms :: Set CspSymbol
diffsyms = Set CspSymbol
symset Set CspSymbol -> Set CspSymbol -> Set CspSymbol
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set CspSymbol
symset0 in
        String -> Range -> Result CspCASLMorphism
forall a. String -> Range -> Result a
fatal_error ("Hiding: The following symbols "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set CspSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set CspSymbol
diffsyms " are not in the signature")
        (Range -> Result CspCASLMorphism)
-> Range -> Result CspCASLMorphism
forall a b. (a -> b) -> a -> b
$ Set CspSymbol -> Range
forall a. GetRange a => a -> Range
getRange Set CspSymbol
diffsyms

cspHideSym :: CspSymbol -> Set.Set CspSymbol -> Set.Set CspSymbol
cspHideSym :: CspSymbol -> Set CspSymbol -> Set CspSymbol
cspHideSym sy :: CspSymbol
sy set1 :: Set CspSymbol
set1 = let
  set2 :: Set CspSymbol
set2 = CspSymbol -> Set CspSymbol -> Set CspSymbol
forall a. Ord a => a -> Set a -> Set a
Set.delete CspSymbol
sy Set CspSymbol
set1
  n :: SORT
n = CspSymbol -> SORT
cspSymName CspSymbol
sy
  in case CspSymbol -> CspSymbType
cspSymbType CspSymbol
sy of
  CaslSymbType SortAsItemType ->
    (CspSymbol -> Bool) -> Set CspSymbol -> Set CspSymbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (CspSymbol -> Bool) -> CspSymbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> CspSymbType -> Bool
cspProfileContains SORT
n (CspSymbType -> Bool)
-> (CspSymbol -> CspSymbType) -> CspSymbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspSymbol -> CspSymbType
cspSymbType) Set CspSymbol
set2
  ChanAsItemType s :: SORT
s ->
    (CspSymbol -> Bool) -> Set CspSymbol -> Set CspSymbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (SORT -> SORT -> CspSymbol -> Bool
unusedChan SORT
n SORT
s) Set CspSymbol
set2
  _ -> Set CspSymbol
set2

cspProfileContains :: Id -> CspSymbType -> Bool
cspProfileContains :: SORT -> CspSymbType -> Bool
cspProfileContains s :: SORT
s ty :: CspSymbType
ty = case CspSymbType
ty of
  CaslSymbType t :: SymbType
t -> SORT -> SymbType -> Bool
profileContainsSort SORT
s SymbType
t
  ChanAsItemType s2 :: SORT
s2 -> SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2
  ProcAsItemType p :: ProcProfile
p -> SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ ProcProfile -> Set SORT
procProfile2Sorts ProcProfile
p

unusedChan :: Id -> SORT -> CspSymbol -> Bool
unusedChan :: SORT -> SORT -> CspSymbol -> Bool
unusedChan c :: SORT
c s :: SORT
s sy :: CspSymbol
sy = case CspSymbol -> CspSymbType
cspSymbType CspSymbol
sy of
  ProcAsItemType (ProcProfile _ al :: CommAlpha
al) ->
    (CommType -> Bool -> Bool) -> Bool -> CommAlpha -> Bool
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ ct :: CommType
ct b :: Bool
b -> case CommType
ct of
       CommTypeSort _ -> Bool
b
       CommTypeChan (TypedChanName c2 :: SORT
c2 s2 :: SORT
s2) -> Bool
b Bool -> Bool -> Bool
&& (SORT
c, SORT
s) (SORT, SORT) -> (SORT, SORT) -> Bool
forall a. Eq a => a -> a -> Bool
/= (SORT
c2, SORT
s2)) Bool
True CommAlpha
al
  _ -> Bool
True