Hets - the Heterogeneous Tool Set

Copyright(c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
LicenseGPLv2 or higher, see LICENSE.txt
Maintainercsliam@swansea.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellNone

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

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

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.

mapSen :: CspCASLMorphism -> CspSen -> CspSen

Apply a Signature Morphism to a CspCASL Sentence