{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}
{- |
Module      :  ./CspCASL/Morphism.hs
Description :  Symbols and signature morphisms for the CspCASL logic
Copyright   :  (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  provisional
Portability :  portable

Symbols and signature morphisms for the CspCASL logic
-}

module CspCASL.Morphism
    ( CspCASLMorphism
    , CspAddMorphism (..)
    , ChanMap
    , ProcessMap
    , mapProcProfile
    , cspSubsigInclusion
    , emptyCspAddMorphism
    , cspAddMorphismUnion
    , cspMorphismToCspSymbMap
    , inducedCspSign
    , mapSen
    ) where

import CspCASL.AS_CspCASL_Process
import CspCASL.SignCSP
import CspCASL.Symbol
import qualified CspCASL.LocalTop as LT

import CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..), OpKind (..))
import CASL.Sign as CASL_Sign
import CASL.Morphism as CASL_Morphism
import qualified CASL.MapSentence as CASL_MapSen

import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils (composeMap)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import Control.Monad

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

-- Morphisms

{- | This is the second component of a CspCASL signature morphism, the process
name map. We map process name with a profile into new names and
communications alphabet. We follow CASL here and instread of mapping to a new
name and a new profile, we map just to the new name and the new
communications alphabet of the profile. This is because the argument sorts of
the profile have no chocie they have to be the sorts resultsing from maping
the original sorts in the profile with the data part map. Note: the
communications alphabet of the source profile must be downward closed with
respect to the CASL signature sub-sort relation (at source) and also the
target communications alphabet must be downward closed with respect to the
CASL signature sub-sort relation (at target). -}
type ProcessMap =
  Map.Map (PROCESS_NAME, ProcProfile) PROCESS_NAME

type ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME

-- | CspAddMorphism - This is just the extended part
data CspAddMorphism = CspAddMorphism
    {- Note that when applying the CspAddMorphism to process names or channel
    names, if the name is not in the map in the morphism, then the
    application is the identity function. Thus empty maps are used to form
    the empty morphism and the identity morphism. -}
    { channelMap :: ChanMap
    , processMap :: ProcessMap
    } deriving (Show, Eq, Ord, Typeable, Data)

-- | The empty CspAddMorphism.
emptyCspAddMorphism :: CspAddMorphism
emptyCspAddMorphism = CspAddMorphism
    {- Note that when applying the CspAddMorphism to process names or
    channel names, if the name is not in the map in the morphism,
    then the application is the identity function. Thus empty maps
    are used to form the empty morphism. -}
    { channelMap = Map.empty
    , processMap = Map.empty
    }

{- | Given two signatures (the first being a sub signature of the second
according to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}
cspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
cspSubsigInclusion sign = checkResultMorphismIsLegal .
                          CASL_Morphism.sigInclusion emptyCspAddMorphism sign
{- We use the empty morphism as it also represents the identity, thus this
will embed channel names and process names properly. -}

checkResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism
checkResultMorphismIsLegal rmor = do
  mor <- rmor
  legalMorphismExtension mor
  return mor

-- | lookup a typed channel
mapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)
mapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)

-- | Apply a signature morphism to a channel name
mapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)
  -> (CHANNEL_NAME, SORT)
mapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor

mapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType
mapCommTypeAux sm cm ct = case ct of
   CommTypeSort s -> CommTypeSort $ mapSort sm s
   CommTypeChan (TypedChanName c s) -> let (d, t) = mapChan sm cm (c, s) in
     CommTypeChan $ TypedChanName d t

-- | Apply a signature morphism to a CommType
mapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType
mapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)

mapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha
mapCommAlphaAux sm = Set.map . mapCommTypeAux sm

-- | Apply a signature morphism  to a CommAlpha
mapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha
mapCommAlpha = Set.map . mapCommType

mapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile
mapProcProfile sm cm (ProcProfile sl cs) =
  ProcProfile (map (mapSort sm) sl) $ mapCommAlphaAux sm cm cs

mapProcId :: Sort_map -> ChanMap -> ProcessMap
  -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
mapProcId sm cm pm (i, p) = let
  n@(ProcProfile args alpha) = mapProcProfile sm cm p
  in case Map.lookup (i, p) pm of
       Nothing -> (i, n)
       Just j -> (j, ProcProfile args alpha)

mapProcess :: Morphism f CspSign CspAddMorphism
  -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)
mapProcess mor = let em = extended_map mor in
  mapProcId (sort_map mor) (channelMap em) $ processMap em

-- | Compose two CspAddMorphisms
composeCspAddMorphism :: Morphism f CspSign CspAddMorphism
  -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism
composeCspAddMorphism m1 m2 = let
    sMap1 = sort_map m1
    sMap2 = sort_map m2
    sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2
    src = msource m1
    cSrc = extendedInfo src
    cMap = MapSet.foldWithKey ( \ c s ->
                       let p = (c, s)
                           ni = fst $ mapChannel m2 $ mapChannel m1 p
                       in if c == ni then id else Map.insert p ni)
                      Map.empty $ chans cSrc
    pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->
                       let pp = (p, pr)
                           (ni, ProcProfile _ na) =
                             mapProcess m2 $ mapProcess m1 pp
                           oa = mapCommAlphaAux sMap cMap a
                       in if p == ni && oa == na then id else
                              Map.insert pp ni)
                      Map.empty $ procSet cSrc
  in return emptyCspAddMorphism
  { channelMap = cMap
  , processMap = pMap }

{- | A CspCASLMorphism is a CASL Morphism with the extended_map to be a
CspAddMorphism. -}
type CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism

{- | Check if a CspCASL signature morphism has the refl property i.e.,
sigma(s1) <= sigma(s2) implies s1 <= s2 for all s1, s2 in S -}
checkReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkReflCondition Morphism
  { msource = sig
  , mtarget = sig'
  , sort_map = sm } = do
  let rel = sortRel sig
      rel' = sortRel sig'
      allPairs = LT.cartesian $ sortSet sig
      failures = Set.filter (not . test) allPairs
      test (s1, s2) = not (Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||
                        mapSort sm s1 == mapSort sm s2) ||
                      (Rel.path s1 s2 rel || s1 == s2)
      produceDiag (s1, s2) =
                let x = mapSort sm s1
                    y = mapSort sm s2
                in Diag Error
                 ("CSP-CASL Signature Morphism Refl Property Violated:\n'"
                  ++ showDoc (Symbol x $ SubsortAsItemType y)
                         "' in target but not in source\n'"
                  ++ showDoc (Symbol s1 $ SubsortAsItemType s2) "'")
                  nullRange
      allDiags = map produceDiag $ Set.toList failures
  unless (Set.null failures)
    $ Result allDiags Nothing -- failure with error messages


{- | Check if a CspCASL signature morphism has the weak non extension property
i.e.,
sigma(s1) <= u' and sigma(s2) <= u' implies there exists t in S with
s1 <= t and s2 <= t and sigma(t) <= u' for all s1,s2 in S and u' in S' -}
checkWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()
checkWNECondition Morphism
  { msource = sig
  , mtarget = sig'
  , sort_map = sm } = do
  let rel' = sortRel sig'
      supers s signature = Set.insert s $ supersortsOf s signature
      allPairsInSource = LT.cartesian $ sortSet sig
      commonSuperSortsInTarget s1 s2 = Set.intersection
                                       (supers (mapSort sm s1) sig')
                                       (supers (mapSort sm s2) sig')
      {- Candidates are triples (s1,s2,u') such that
      \sigma(s1),\sigma(s2) < u' -}
      createCandidateTripples (s1, s2) =
        Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)
      allCandidateTripples =
        Set.unions $ Set.toList $ Set.map createCandidateTripples
        allPairsInSource
      testCandidate (s1, s2, u') =
        let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)
            test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'
         in or $ Set.toList $ Set.map test possibleWitnesses
      failures = Set.filter (not . testCandidate) allCandidateTripples
      produceDiag (s1, s2, u') =
                let x = mapSort sm s1
                    y = mapSort sm s2
                in Diag Error
                   ("CSP-CASL Signature Morphism Weak Non-Extension Property "
                    ++ "Violated:\n'"
                    ++ showDoc
                       (Subsort_decl [x, y] u' nullRange :: SORT_ITEM ())
                       "' in target\nbut no common supersort for the sorts\n'"
                    ++ showDoc
                       (Sort_decl [s1, s2] nullRange :: SORT_ITEM ())
                       "' in source")
                   nullRange
      allDiags = map produceDiag $ Set.toList failures
  unless (Set.null failures)
    $ Result allDiags Nothing -- failure with error messages

-- | unite morphisms
cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism
  -> Result CspAddMorphism
cspAddMorphismUnion mor1 mor2 = let
    s1 = extendedInfo $ msource mor1
    s2 = extendedInfo $ msource mor2
    m1 = extended_map mor1
    m2 = extended_map mor2
    chan1 = channelMap m1
    chan2 = channelMap m2
    delChan (n, s) = MapSet.delete n s
    uc1 = foldr delChan (chans s1) $ Map.keys chan1
    uc2 = foldr delChan (chans s2) $ Map.keys chan2
    uc = MapSet.union uc1 uc2
    proc1 = processMap m1
    proc2 = processMap m2
    delProc (n, p) = MapSet.delete n p
    up1 = foldr delProc (procSet s1) $ Map.keys proc1
    up2 = foldr delProc (procSet s2) $ Map.keys proc2
    up = MapSet.union up1 up2
    (cds, cMap) = foldr ( \ (isc@(i, s), j) (ds, m) ->
          case Map.lookup isc m of
          Nothing -> (ds, Map.insert isc j m)
          Just k -> if j == k then (ds, m) else
              (Diag Error
               ("incompatible mapping of channel " ++ shows i ":"
                ++ showDoc s " to " ++ shows j " and "
                ++ shows k "") nullRange : ds, m)) ([], chan1)
          (Map.toList chan2 ++ concatMap ( \ (c, ts) -> map
              ( \ s -> ((c, s), c)) ts) (MapSet.toList uc))
    (pds, pMap) =
      foldr ( \ (isc@(i, pt), j) (ds, m) ->
          case Map.lookup isc m of
          Nothing -> (ds, Map.insert isc j m)
          Just k -> if j == k then (ds, m) else
              (Diag Error
               ("incompatible mapping of process " ++ shows i " "
                ++ showDoc pt " to " ++ show j ++ " and "
                ++ show k) nullRange : ds, m)) (cds, proc1)
          (Map.toList proc2 ++ concatMap ( \ (p, pts) -> map
              ( \ pt -> ((p, pt), p)) pts)
              (MapSet.toList up))
     in if null pds then return emptyCspAddMorphism
        { channelMap = cMap
        , processMap = pMap }
        else Result pds Nothing

toCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism
  -> Map.Map CspSymbol CspSymbol
toCspSymbMap b mor = let
    src = extendedInfo $ msource mor
    chanSymMap = MapSet.foldWithKey
      ( \ i t -> let
              p = (i, t)
              q@(j, _) = mapChannel mor p
              in if b && i == j then id else
                     Map.insert (toChanSymbol p) $ toChanSymbol q)
      Map.empty $ chans src
    procSymMap = MapSet.foldWithKey
      ( \ i t@(ProcProfile _ al) -> let
              p = (i, t)
              al1 = mapCommAlpha mor al
              q@(j, ProcProfile _ al2) = mapProcess mor p
              in if b && i == j && al1 == al2 then id else
                     Map.insert (toProcSymbol p) $ toProcSymbol q)
      Map.empty $ procSet src
  in Map.union chanSymMap procSymMap

cspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol
cspMorphismToCspSymbMap mor =
  Map.union (Map.fromList
    . map (\ (a, b) -> (caslToCspSymbol a, caslToCspSymbol b))
    $ Map.toList $ morphismToSymbMap mor)
  $ toCspSymbMap False mor

-- | Instance for CspCASL signature extension
instance SignExtension CspSign where
  isSubSignExtension = isCspSubSign

-- | a dummy instances used for the default definition
instance Pretty CspAddMorphism where
  pretty m = pretty $ toCspSymbMap False
    $ embedMorphism m emptyCspCASLSign emptyCspCASLSign

-- | Instance for CspCASL morphism extension (used for Category)
instance CASL_Morphism.MorphismExtension CspSign CspAddMorphism
    where
      ideMorphismExtension _ = emptyCspAddMorphism
      composeMorphismExtension = composeCspAddMorphism
      -- we omit inverses here
      isInclusionMorphismExtension m =
        Map.null (channelMap m) && Map.null (processMap m)
      -- pretty printing for Csp morphisms
      prettyMorphismExtension = printMap id sepByCommas pairElems
        . toCspSymbMap True
      legalMorphismExtension m = do
        checkReflCondition m
        checkWNECondition m


-- * induced signature extension

inducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap
inducedChanMap sm cm = MapSet.foldWithKey
  ( \ i s ->
      let (j, t) = mapChan sm cm (i, s)
      in MapSet.insert j t) MapSet.empty

inducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap
  -> ProcNameMap
inducedProcMap sm cm pm = MapSet.foldWithKey
  ( \ n p ->
      let (m, q) = mapProcId sm cm pm (n, p)
      in MapSet.insert m q) MapSet.empty

inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign
inducedCspSign sm _ _ m sig =
  let csig = extendedInfo sig
      cm = channelMap m
  in emptyCspSign
     { chans = inducedChanMap sm cm $ chans csig
     , procSet = inducedProcMap sm cm (processMap m) $ procSet csig }

-- * application of morphisms to sentences

-- | Apply a Signature Morphism to a CspCASL Sentence
mapSen :: CspCASLMorphism -> CspSen -> CspSen
mapSen mor sen =
    if CASL_Morphism.isInclusionMorphism
       CASL_Morphism.isInclusionMorphismExtension mor
    then sen
    else case sen of
           ProcessEq procName fqVarList commAlpha proc ->
               let {- Map the morphism over all the parts of the process
                   equation -}
                   newProcName = mapProcessName mor procName
                   newFqVarList = mapFQProcVarList mor fqVarList
                   newCommAlpha = mapCommAlpha mor commAlpha
                   newProc = mapProc mor proc
               in ProcessEq newProcName newFqVarList
                                    newCommAlpha newProc

-- | Apply a signature morphism  to a Fully Qualified Process Variable List
mapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList
mapFQProcVarList mor =
    -- As these are terms, just map the morphism over CASL TERMs
    map (mapCASLTerm mor)

-- | Apply a signature morphism to a process
mapProc :: CspCASLMorphism -> PROCESS -> PROCESS
mapProc mor proc =
    let mapProc' = mapProc mor
        mapProcessName' = mapProcessName mor
        mapEvent' = mapEvent mor
        mapEventSet' = mapEventSet mor
        mapRenaming' = mapRenaming mor
        mapCommAlpha' = mapCommAlpha mor
        mapCASLTerm' = mapCASLTerm mor
        mapCASLFormula' = mapCASLFormula mor
    in case proc of
         Skip r -> Skip r
         Stop r -> Stop r
         Div r -> Div r
         Run es r -> Run (mapEventSet' es) r
         Chaos ev r -> Chaos (mapEventSet' ev) r
         PrefixProcess e p r ->
             PrefixProcess (mapEvent' e) (mapProc' p) r
         Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r
         ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r
         InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r
         Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r
         SynchronousParallel p q r ->
             SynchronousParallel (mapProc' p) (mapProc' q) r
         GeneralisedParallel p es q r ->
             GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r
         AlphabetisedParallel p les res q r ->
             AlphabetisedParallel (mapProc' p) (mapEventSet' les)
                                      (mapEventSet' res) (mapProc' q) r
         Hiding p es r ->
             Hiding (mapProc' p) (mapEventSet' es) r
         RenamingProcess p re r ->
             RenamingProcess (mapProc' p) (mapRenaming' re) r
         ConditionalProcess f p q r ->
             ConditionalProcess (mapCASLFormula' f)
                                    (mapProc' p) (mapProc' q) r
         NamedProcess pn fqParams r ->
             NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r
         FQProcess p commAlpha r ->
             FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r

-- | Apply a signature morphism to an event set
mapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET
mapEventSet mor (EventSet fqComms r) =
  EventSet (map (mapCommType mor) fqComms) r

-- | Apply a signature morphism to an event
mapEvent :: CspCASLMorphism -> EVENT -> EVENT
mapEvent mor e =
    let mapCASLTerm' = mapCASLTerm mor
        mapChannelName' = mapChannel mor
    in case e of
      -- Just map the morphism over the event (a term)
      FQTermEvent t r -> FQTermEvent (mapCASLTerm' t) r
      {- Just map the morphism over the variable, this just maps the sort and
         keep the same name -}
      FQExternalPrefixChoice v r -> FQExternalPrefixChoice (mapCASLTerm' v) r
      {- Just map the morphism over the variable, this just maps the sort and
         keep the same name -}
      FQInternalPrefixChoice v r -> FQInternalPrefixChoice (mapCASLTerm' v) r
      -- Just map the morphism over the event (a term) and the channel name
      FQChanSend (c, s) t r ->
        FQChanSend (mapChannelName' (c, s)) (mapCASLTerm' t) r
      {- Just map the morphism over the sort and the channel name, we keep
         the variable name -}
      FQChanNonDetSend (c, s) v r ->
        FQChanNonDetSend (mapChannelName' (c, s)) (mapCASLTerm' v) r
      {- Just map the morphism over the sort and the channel name, we keep
         the variable name -}
      FQChanRecv (c, s) v r ->
        FQChanRecv (mapChannelName' (c, s)) (mapCASLTerm' v) r
      _ -> error "CspCASL.Morphism.mapEvent: Cannot map unqualified event"

mapRename :: CspCASLMorphism -> Rename -> Rename
mapRename mor r@(Rename i mc) = case mc of
  Nothing -> r
  Just (k, ms) -> case ms of
    Nothing -> r
    Just (s1, s2) -> case k of
      BinPred -> let
        (j, PredType [t1, t2]) = mapPredSym (sort_map mor) (pred_map mor)
            (i, PredType [s1, s2])
        in Rename j $ Just (k, Just (t1, t2))
      _ -> let
        (j, OpType _ [t1] t2) = mapOpSym (sort_map mor) (op_map mor)
            (i, OpType Partial [s1] s2)
        in Rename j $ Just (k, Just (t1, t2))

mapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING
mapRenaming mor (Renaming rm) = Renaming $ map (mapRename mor) rm

cspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()
cspCASLMorphism2caslMorphism m =
  m { msource = ccSig2CASLSign $ msource m
    , mtarget = ccSig2CASLSign $ mtarget m
    , extended_map = () }

{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL
TERM that appears in CspCASL). -}
mapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()
mapCASLTerm =
    {- The error here is not used. It is a function to map over the morphism,
    CspCASL does not use this functionality. -}
    CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm")
      . cspCASLMorphism2caslMorphism

{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL
FORMULA that appears in CspCASL). -}
mapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()
mapCASLFormula =
    {- The error here is not used. It is a function to map over the morphism,
    CspCASL does not use this functionality. -}
    CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula")
      . cspCASLMorphism2caslMorphism

-- | Apply a signature morphism to a process name
mapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME
mapProcessName mor pn = case pn of
    FQ_PROCESS_NAME pn' procProfilePn' ->
      let (m, procProfileM) =
            mapProcess mor (pn', procProfilePn')
      in FQ_PROCESS_NAME m procProfileM
    _ -> error "unqualifed FQ_PROCESS_NAME"
