content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CspCASL/SignCSP.hs
  Description :  CspCASL signatures
  Copyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  M.Roggenbach@swansea.ac.uk
  Stability   :  provisional
  Portability :  portable
  
  signatures for CSP-CASL
  -}
  
  module CspCASL.SignCSP
    ( addProcNameToProcNameMap
    , ccSig2CASLSign
    , ccSig2CspSign
    , ChanNameMap
    , closeCspCommAlpha
    , CspCASLSign
    , CspCASLSen
    , CspSen (..)
    , CspSign (..)
    , cspSignUnion
    , diffCspSig
    , emptyCspCASLSign
    , emptyCspSign
    , FQProcVarList
    , getUniqueProfileInProcNameMap
    , isCspCASLSubSig
    , isCspSubSign
    , isNameInProcNameMap
    , isProcessEq
    , ProcNameMap
    , ProcVarList
    , ProcVarMap
    , reduceProcProfile
    , commType2Sort
    , relatedSorts
    , relatedProcs
    , unionCspCASLSign
    ) where
  
  import CASL.AS_Basic_CASL
  import CASL.Overload
  import CASL.Sign
  import CASL.ToDoc
  
  import CspCASL.AS_CspCASL_Process
  import CspCASL.AS_CspCASL ()
  import CspCASL.CspCASL_Keywords
  import qualified CspCASL.LocalTop as LocalTop
  import CspCASL.Print_CspCASL ()
  
  import Common.AnnoState
  import Common.Doc
  import Common.DocUtils
  import Common.Id
  import Common.Result
  import Common.Lib.Rel (Rel, predecessors, member)
  import qualified Common.Lib.MapSet as MapSet
  import Common.Utils (keepMins)
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.Data
  import Data.List
  import Data.Ord
  
  type ChanNameMap = MapSet.MapSet CHANNEL_NAME SORT
  type ProcNameMap = MapSet.MapSet PROCESS_NAME ProcProfile
  type ProcVarMap = Map.Map SIMPLE_ID SORT
  type ProcVarList = [(SIMPLE_ID, SORT)]
  
  -- | Add a process name and its profile to a process name map.  exist.
  addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap
    -> ProcNameMap
  addProcNameToProcNameMap = MapSet.insert
  
  -- | Test if a simple process name with a profile is in the process name map.
  isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
  isNameInProcNameMap = MapSet.member
  
  {- | Given a simple process name and a required number of parameters, find a
  unqiue profile with that many parameters if possible. If this is not possible
  (i.e., name does not exist, or no profile with the required number of
  arguments or not unique profile for the required number of arguments), then
  the functions returns a failed result with a helpful error message.  failure. -}
  getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
                                   Result ProcProfile
  getUniqueProfileInProcNameMap name numParams pm =
    let profiles = MapSet.lookup name pm
        isMatch (ProcProfile argSorts _) =
          length argSorts == numParams
        matchedProfiles = Set.filter isMatch profiles
    in case Set.toList matchedProfiles of
         [] -> mkError ("Process name not in signature with "
               ++ show numParams ++ " parameters:") name
         [p] -> return p
         _ -> mkError ("Process name not unique in signature with "
              ++ show numParams ++ " parameters:") name
  
  -- Close a communication alphabet under CASL subsort
  closeCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
  closeCspCommAlpha sr =
      Set.unions . Set.toList . Set.map (closeOneCspComm sr)
  
  -- Close one CommType under CASL subsort
  closeOneCspComm :: Rel SORT -> CommType -> CommAlpha
  closeOneCspComm sr x = let
    mkTypedChan c s = CommTypeChan $ TypedChanName c s
    subsorts s' = Set.insert s' $ predecessors sr s'
    in case x of
      CommTypeSort s ->
          Set.map CommTypeSort (subsorts s)
      CommTypeChan (TypedChanName c s) ->
          Set.map CommTypeSort (subsorts s)
        `Set.union` Set.map (mkTypedChan c) (subsorts s)
  
  {- | Remove the implicit sorts from the proc name map under a sub-sort
  relation. Assumes all the proc profile's comms are in the sub sort relation and
  simply makes the comms contain only the minimal super sorts under the sub-sort
  relation. -}
  reduceProcNamesInSig :: Rel SORT -> CspSign -> CspSign
  reduceProcNamesInSig sr cspSig =
    cspSig { procSet = reduceProcNameMap sr $ procSet cspSig }
  
  {- | Remove the implicit sorts from a proc name map under a sub-sort
  relation. Assumes all the proc profile's comms are in the sub sort relation and
  simply makes the comms contain only the minimal super sorts under the sub-sort
  relation. -}
  reduceProcNameMap :: Rel SORT -> ProcNameMap -> ProcNameMap
  reduceProcNameMap sr =
    MapSet.map (reduceProcProfile sr)
  
  {- | Remove the implicit sorts from a profile under a sub-sort relation. Assumes
  all the proc profile's comms are in the sub sort relation and simply makes the
  comms contain only the minimal super sorts under the sub-sort relation. -}
  reduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile
  reduceProcProfile sr (ProcProfile argSorts comms) =
    ProcProfile argSorts (reduceCspCommAlpha sr comms)
  
  {- | Remove the implicit sorts from a CommAlpha under a sub-sort
  relation. Assumes all the proc profile's comms are in the sub sort relation and
  simply makes the comms contain only the minimal super sorts under the sub-sort
  relation. -}
  reduceCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
  reduceCspCommAlpha sr =
    Set.fromList .
      concatMap (keepMins $ cmpCommType sr) . groupBy sameChan . Set.toList
  
  cmpCommType :: Rel SORT -> CommType -> CommType -> Bool
  cmpCommType rel t1 t2 = let
    s1 = commType2Sort t1
    s2 = commType2Sort t2
    in s1 == s2 || member s2 s1 rel
  
  commType2Sort :: CommType -> SORT
  commType2Sort c = case c of
    CommTypeSort s -> s
    CommTypeChan (TypedChanName _ s) -> s
  
  sameChan :: CommType -> CommType -> Bool
  sameChan t1 t2 = case (t1, t2) of
    (CommTypeSort _, CommTypeSort _) -> True
    (CommTypeChan (TypedChanName c1 _), CommTypeChan (TypedChanName c2 _))
        -> c1 == c2
    _ -> False
  
  -- | CSP process signature.
  data CspSign = CspSign
      { chans :: ChanNameMap
      , procSet :: ProcNameMap
      } deriving (Show, Eq, Ord, Typeable, Data)
  
  -- | plain union
  cspSignUnion :: CspSign -> CspSign -> CspSign
  cspSignUnion sign1 sign2 = emptyCspSign
      { chans = chans sign1 `MapSet.union` chans sign2
      , procSet = procSet sign1 `MapSet.union` procSet sign2 }
  
  {- | A CspCASL signature is a CASL signature with a CSP process
  signature in the extendedInfo part. -}
  type CspCASLSign = Sign CspSen CspSign
  
  ccSig2CASLSign :: CspCASLSign -> CASLSign
  ccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }
  
  -- | Projection from CspCASL signature to Csp signature
  ccSig2CspSign :: CspCASLSign -> CspSign
  ccSig2CspSign = extendedInfo
  
  -- | Empty CspCASL signature.
  emptyCspCASLSign :: CspCASLSign
  emptyCspCASLSign = emptySign emptyCspSign
  
  -- | Empty CSP process signature.
  emptyCspSign :: CspSign
  emptyCspSign = CspSign
      { chans = MapSet.empty
      , procSet = MapSet.empty }
  
  -- | Compute union of two CSP CASL signatures.
  unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
  unionCspCASLSign s1 s2 = do
    -- Compute the unioned data signature ignoring the csp signatures
    let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2
    -- Check that the new data signature has local top elements
        rel = sortRel newDataSig
        diags' = LocalTop.checkLocalTops rel
    -- Compute the unioned csp signature with respect to the new data signature
        newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)
    {- Only error will be added if there are any probelms. If there are no
    problems no errors will be added and hets will continue as normal. -}
    appendDiags diags'
    -- put both the new data signature and the csp signature back together
    return $ newDataSig {extendedInfo = newCspSign}
  
  {- | Compute union of two CSP signatures assuming the new already computed data
  signature. -}
  unionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
  unionCspSign sr a b = reduceProcNamesInSig sr $ cspSignUnion a b
  
  -- | Compute difference of two CSP process signatures.
  diffCspSig :: CspSign -> CspSign -> CspSign
  diffCspSig a b = emptyCspSign
    { chans = MapSet.difference (chans a) $ chans b
    , procSet = MapSet.difference (procSet a) $ procSet b
    }
  
  -- | Is one CspCASL Signature a sub signature of another
  isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
  isCspCASLSubSig =
    -- Normal casl subsignature and our extended csp part
    isSubSig isCspSubSign
    {- Also the sorts and sub-sort rels should be equal. If they are not then we
    cannot just add the processes in as their profiles need to be donward closed
    under the new sort-rels, but we do not check this here. -}
  
  {- | Is one Csp Signature a sub signature of another assuming the same data
  signature for now. -}
  isCspSubSign :: CspSign -> CspSign -> Bool
  isCspSubSign a b =
       MapSet.isSubmapOf (chans a) (chans b) &&
      -- Check for each profile that the set of names are included.
      MapSet.isSubmapOf (procSet a) (procSet b)
  
  -- | Pretty printing for CspCASL signatures
  instance Pretty CspSign where
    pretty = printCspSign
  
  printCspSign :: CspSign -> Doc
  printCspSign sigma =
      case mapSetToList $ chans sigma of
        [] -> empty
        s -> keyword (channelS ++ appendS s) <+> printChanList s
      $+$ case mapSetToList $ procSet sigma of
        [] -> empty
        ps -> keyword processS <+> printProcList ps
  
  -- | Pretty printing for channels
  printChanList :: [(CHANNEL_NAME, SORT)] -> Doc
  printChanList l = let
    gl = groupBy (\ (_, s1) (_, s2) -> s1 == s2) $ sortBy (comparing snd) l
    printChan cl = case cl of
      [] -> empty -- should not happen
      (_, s) : _ -> fsep [ppWithCommas (map fst cl), colon <+> pretty s]
    in sepBySemis $ map printChan gl
  
  -- | Pretty printing for processes
  printProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
  printProcList = sepBySemis . map
    (\ (procName, procProfile) -> pretty procName <+> pretty procProfile)
  
  -- * overload relations: We do not have one of these yet in theory
  
  relatedSorts :: CspCASLSign -> SORT -> SORT -> Bool
  relatedSorts sig s1 s2 = haveCommonSupersorts True sig s1 s2
    || haveCommonSupersorts False sig s1 s2
  
  relatedCommTypes :: CspCASLSign -> CommType -> CommType -> Bool
  relatedCommTypes sig ct1 ct2 = case (ct1, ct2) of
    (CommTypeSort s1, CommTypeSort s2) -> relatedSorts sig s1 s2
    (CommTypeChan (TypedChanName c1 s1), CommTypeChan (TypedChanName c2 s2))
      -> c1 == c2 && relatedSorts sig s1 s2
    _ -> False
  
  relatedCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha -> Bool
  relatedCommAlpha sig al1 al2 = Set.null al1 || Set.null al2 ||
    any (\ a -> any (relatedCommTypes sig a) $ Set.toList al1) (Set.toList al2)
  
  relatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool
  relatedProcs sig (ProcProfile l1 al1) (ProcProfile l2 al2) =
    length l1 == length l2 &&
      and (zipWith (relatedSorts sig) l1 l2)
      && relatedCommAlpha sig al1 al2
  
  -- * Sentences
  
  {- | FQProcVarList should only contain fully qualified CASL variables which are
  TERMs i.e. constructed via the TERM constructor Qual_var. -}
  type FQProcVarList = [TERM ()]
  
  {- | A CspCASl senetence is either a CASL formula or a Procsses equation. A
  process equation has on the LHS a process name, a list of parameters which
  are qualified variables (which are terms), a constituent( or is it permitted
  ?) communication alphabet and finally on the RHS a fully qualified process. -}
  data CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
        deriving (Show, Eq, Ord, Typeable, Data)
  
  type CspCASLSen = FORMULA CspSen
  
  instance GetRange CspSen
  
  instance Pretty CspSen where
      pretty (ProcessEq pn varList _commAlpha proc) =
          let varDoc = if null varList
                       then empty
                       else parens $ ppWithCommas varList
          in fsep [pretty pn, varDoc, equals <+> pretty proc]
  
  instance FormExtension CspSen where
    prefixExt (ProcessEq pn _ _ _) = case pn of
      PROCESS_NAME _ -> (keyword processS <+>)
      FQ_PROCESS_NAME {} -> id
  
  instance TermExtension CspSen
  instance TermParser CspSen
  
  isProcessEq :: CspCASLSen -> Bool
  isProcessEq f = case f of
     ExtFORMULA _ -> True
     _ -> False
  