{-# LANGUAGE MultiParamTypeClasses #-}

{- |

Module : $Header$

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 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 (Eq, Ord, Show)

-- | 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"