Hets - the Heterogeneous Tool Set
Copyright(c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerM.Roggenbach@swansea.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CspCASL.SignCSP

Description

signatures for CSP-CASL

Synopsis

Documentation

addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap Source #

Add a process name and its profile to a process name map. exist.

ccSig2CspSign :: CspCASLSign -> CspSign Source #

Projection from CspCASL signature to Csp signature

type CspCASLSign = Sign CspSen CspSign Source #

A CspCASL signature is a CASL signature with a CSP process signature in the extendedInfo part.

data CspSen Source #

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.

Instances

Instances details
Eq CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

(==) :: CspSen -> CspSen -> Bool

(/=) :: CspSen -> CspSen -> Bool

Data CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CspSen -> c CspSen

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CspSen

toConstr :: CspSen -> Constr

dataTypeOf :: CspSen -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CspSen)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen)

gmapT :: (forall b. Data b => b -> b) -> CspSen -> CspSen

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r

gmapQ :: (forall d. Data d => d -> u) -> CspSen -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSen -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen

Ord CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

compare :: CspSen -> CspSen -> Ordering

(<) :: CspSen -> CspSen -> Bool

(<=) :: CspSen -> CspSen -> Bool

(>) :: CspSen -> CspSen -> Bool

(>=) :: CspSen -> CspSen -> Bool

max :: CspSen -> CspSen -> CspSen

min :: CspSen -> CspSen -> CspSen

Show CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

showsPrec :: Int -> CspSen -> ShowS

show :: CspSen -> String

showList :: [CspSen] -> ShowS

Generic CspSen 
Instance details

Defined in CspCASL.ATC_CspCASL

Associated Types

type Rep CspSen :: Type -> Type

Methods

from :: CspSen -> Rep CspSen x

to :: Rep CspSen x -> CspSen

GetRange CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

FromJSON CspSen 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

parseJSON :: Value -> Parser CspSen

parseJSONList :: Value -> Parser [CspSen]

ToJSON CspSen 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

toJSON :: CspSen -> Value

toEncoding :: CspSen -> Encoding

toJSONList :: [CspSen] -> Value

toEncodingList :: [CspSen] -> Encoding

ShATermConvertible CspSen 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

toShATermAux :: ATermTable -> CspSen -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CspSen] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CspSen)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CspSen])

Pretty CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

FormExtension CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

TermExtension CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

TermParser CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

termParser :: Bool -> AParser st CspSen Source #

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 () Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

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 () Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #

Instance of Sentences for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #

Syntax of CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #

Static Analysis for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source #

sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source #

extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source #

stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source #

convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source #

ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source #

qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source #

symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source #

id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source #

matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source #

empty_signature :: GenCspCASL a -> CspCASLSign Source #

add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source #

signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source #

is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source #

subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source #

generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source #

is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source #

corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #

Instance of Logic for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source #

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

all_sublogics :: GenCspCASL a -> [()] Source #

bottomSublogic :: GenCspCASL a -> Maybe () Source #

sublogicDimensions :: GenCspCASL a -> [[()]] Source #

parseSublogic :: GenCspCASL a -> String -> Maybe () Source #

proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source #

provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source #

default_prover :: GenCspCASL a -> String Source #

cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source #

conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source #

empty_proof_tree :: GenCspCASL a -> () Source #

syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source #

export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source #

omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source #

omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source #

addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #

(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 () Source # 
Instance details

Defined in CspCASL.Comorphisms

type Rep CspSen 
Instance details

Defined in CspCASL.ATC_CspCASL

type Rep CspSen = D1 ('MetaData "CspSen" "CspCASL.SignCSP" "main" 'False) (C1 ('MetaCons "ProcessEq" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FQ_PROCESS_NAME) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FQProcVarList)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CommAlpha) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PROCESS))))

data CspSign Source #

CSP process signature.

Constructors

CspSign 

Instances

Instances details
Eq CspSign Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

(==) :: CspSign -> CspSign -> Bool

(/=) :: CspSign -> CspSign -> Bool

Data CspSign Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CspSign -> c CspSign

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CspSign

toConstr :: CspSign -> Constr

dataTypeOf :: CspSign -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CspSign)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign)

gmapT :: (forall b. Data b => b -> b) -> CspSign -> CspSign

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSign -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSign -> r

gmapQ :: (forall d. Data d => d -> u) -> CspSign -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSign -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign

Ord CspSign Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

compare :: CspSign -> CspSign -> Ordering

(<) :: CspSign -> CspSign -> Bool

(<=) :: CspSign -> CspSign -> Bool

(>) :: CspSign -> CspSign -> Bool

(>=) :: CspSign -> CspSign -> Bool

max :: CspSign -> CspSign -> CspSign

min :: CspSign -> CspSign -> CspSign

Show CspSign Source # 
Instance details

Defined in CspCASL.SignCSP

Methods

showsPrec :: Int -> CspSign -> ShowS

show :: CspSign -> String

showList :: [CspSign] -> ShowS

Generic CspSign 
Instance details

Defined in CspCASL.ATC_CspCASL

Associated Types

type Rep CspSign :: Type -> Type

Methods

from :: CspSign -> Rep CspSign x

to :: Rep CspSign x -> CspSign

FromJSON CspSign 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

parseJSON :: Value -> Parser CspSign

parseJSONList :: Value -> Parser [CspSign]

ToJSON CspSign 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

toJSON :: CspSign -> Value

toEncoding :: CspSign -> Encoding

toJSONList :: [CspSign] -> Value

toEncodingList :: [CspSign] -> Encoding

ShATermConvertible CspSign 
Instance details

Defined in CspCASL.ATC_CspCASL

Methods

toShATermAux :: ATermTable -> CspSign -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CspSign] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CspSign)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CspSign])

Pretty CspSign Source #

Pretty printing for CspCASL signatures

Instance details

Defined in CspCASL.SignCSP

SignExtension CspSign Source #

Instance for CspCASL signature extension

Instance details

Defined in CspCASL.Morphism

MorphismExtension CspSign CspAddMorphism Source #

Instance for CspCASL morphism extension (used for Category)

Instance details

Defined in CspCASL.Morphism

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 () Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

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 () Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #

Instance of Sentences for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #

Static Analysis for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source #

sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source #

extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source #

stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source #

convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source #

ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source #

qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source #

symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source #

id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source #

matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source #

empty_signature :: GenCspCASL a -> CspCASLSign Source #

add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source #

signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source #

is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source #

subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source #

generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source #

is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source #

corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #

Instance of Logic for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source #

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

all_sublogics :: GenCspCASL a -> [()] Source #

bottomSublogic :: GenCspCASL a -> Maybe () Source #

sublogicDimensions :: GenCspCASL a -> [[()]] Source #

parseSublogic :: GenCspCASL a -> String -> Maybe () Source #

proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source #

provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source #

default_prover :: GenCspCASL a -> String Source #

cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source #

conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source #

empty_proof_tree :: GenCspCASL a -> () Source #

syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source #

export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source #

omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source #

omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source #

addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #

(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 () Source # 
Instance details

Defined in CspCASL.Comorphisms

type Rep CspSign 
Instance details

Defined in CspCASL.ATC_CspCASL

type Rep CspSign = D1 ('MetaData "CspSign" "CspCASL.SignCSP" "main" 'False) (C1 ('MetaCons "CspSign" 'PrefixI 'True) (S1 ('MetaSel ('Just "chans") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ChanNameMap) :*: S1 ('MetaSel ('Just "procSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProcNameMap)))

diffCspSig :: CspSign -> CspSign -> CspSign Source #

Compute difference of two CSP process signatures.

emptyCspCASLSign :: CspCASLSign Source #

Empty CspCASL signature.

emptyCspSign :: CspSign Source #

Empty CSP process signature.

type FQProcVarList = [TERM ()] Source #

FQProcVarList should only contain fully qualified CASL variables which are TERMs i.e. constructed via the TERM constructor Qual_var.

getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap -> Result ProcProfile Source #

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.

isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool Source #

Is one CspCASL Signature a sub signature of another

isCspSubSign :: CspSign -> CspSign -> Bool Source #

Is one Csp Signature a sub signature of another assuming the same data signature for now.

isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool Source #

Test if a simple process name with a profile is in the process name map.

reduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile Source #

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.

unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

Compute union of two CSP CASL signatures.