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
Safe Haskell	None

CspCASL.Morphism

Description

Symbols and signature morphisms for the CspCASL logic

Synopsis

Documentation

type CspCASLMorphism = Morphism CspSen CspSign CspAddMorphism

A CspCASLMorphism is a CASL Morphism with the extended_map to be a CspAddMorphism.

data CspAddMorphism

CspAddMorphism - This is just the extended part

Constructors

CspAddMorphism
Fields channelMap :: ChanMap processMap :: ProcessMap

Instances

Eq CspAddMorphism
Data CspAddMorphism
Ord CspAddMorphism
Show CspAddMorphism
ShATermConvertible CspAddMorphism
Pretty CspAddMorphism	a dummy instances used for the default definition
Typeable * CspAddMorphism
MorphismExtension CspSign CspAddMorphism	Instance for CspCASL morphism extension (used for Category)
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol ()
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol	Instance of Sentences for CspCASL
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol	Static Analysis for CspCASL
CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()	Instance of Logic for CspCASL
(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

type ChanMap = Map (CHANNEL_NAME, SORT) CHANNEL_NAME

type ProcessMap = Map (PROCESS_NAME, ProcProfile) PROCESS_NAME

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).

mapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile

cspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism

Given two signatures (the first being a sub signature of the second according to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism.

emptyCspAddMorphism :: CspAddMorphism

The empty CspAddMorphism.

cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism

unite morphisms

cspMorphismToCspSymbMap :: CspCASLMorphism -> Map CspSymbol CspSymbol

inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign

mapSen :: CspCASLMorphism -> CspSen -> CspSen

Apply a Signature Morphism to a CspCASL Sentence