Copyright	(c) Markus Roggenbach Till Mossakowski and Uni Bremen 2003
License	GPLv2 or higher, see LICENSE.txt
Maintainer	M.Roggenbach@swansea.ac.uk
Stability	experimental
Portability	non-portable(import Logic.Logic)
Safe Haskell	None

CspCASL.Logic_CspCASL

Description

Here is the place where the class Logic is instantiated for CspCASL. A CspCASL signature is a CASL signature with a set of named channels and processes. Every process has a profile. Morphisms are supposed to allow renaming of channels and processes, too. Also sublogics (as a superset of some CASL sublogics) are still missing.

Synopsis

data GenCspCASL a = GenCspCASL a
class Show a => CspCASLSemantics a
type CspCASL = GenCspCASL ()
cspCASL :: GenCspCASL ()
data Trace = Trace
traceCspCASL :: GenCspCASL Trace
data Failure = Failure
failureCspCASL :: GenCspCASL Failure

Documentation

data GenCspCASL a Source #

a generic logic id for CspCASL with different semantics

Constructors

GenCspCASL a

Instances

Instances details

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 Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
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 Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Show a => Show (GenCspCASL a) Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods showsPrec :: Int -> GenCspCASL a -> ShowS show :: GenCspCASL a -> String showList :: [GenCspCASL a] -> ShowS
Show a => Language (GenCspCASL a) Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods language_name :: GenCspCASL a -> String Source # description :: GenCspCASL a -> String Source #
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #	Instance of Sentences for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods map_sen :: GenCspCASL a -> CspCASLMorphism -> CspCASLSen -> Result CspCASLSen Source # simplify_sen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> CspCASLSen Source # negation :: GenCspCASL a -> CspCASLSen -> Maybe CspCASLSen Source # print_sign :: GenCspCASL a -> CspCASLSign -> Doc Source # print_named :: GenCspCASL a -> Named CspCASLSen -> Doc Source # sym_of :: GenCspCASL a -> CspCASLSign -> [Set CspSymbol] Source # mostSymsOf :: GenCspCASL a -> CspCASLSign -> [CspSymbol] Source # symmap_of :: GenCspCASL a -> CspCASLMorphism -> EndoMap CspSymbol Source # sym_name :: GenCspCASL a -> CspSymbol -> Id Source # sym_label :: GenCspCASL a -> CspSymbol -> Maybe String Source # fullSymName :: GenCspCASL a -> CspSymbol -> String Source # symKind :: GenCspCASL a -> CspSymbol -> String Source # symsOfSen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> [CspSymbol] Source # pair_symbols :: GenCspCASL a -> CspSymbol -> CspSymbol -> Result CspSymbol Source #
Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #	Syntax of CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parsersAndPrinters :: GenCspCASL a -> Map String (PrefixMap -> AParser st CspBasicSpec, CspBasicSpec -> Doc) Source # parse_basic_spec :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspBasicSpec) Source # parseSingleSymbItem :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_map_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbMapItems) Source # toItem :: GenCspCASL a -> CspBasicSpec -> Item Source # symb_items_name :: GenCspCASL a -> CspSymbItems -> [String] Source #
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 Methods sourceLogic :: CspCASL2CspCASL a b -> GenCspCASL a Source # sourceSublogic :: CspCASL2CspCASL a b -> () Source # sourceSublogicLossy :: CspCASL2CspCASL a b -> () Source # minSourceTheory :: CspCASL2CspCASL a b -> Maybe (LibName, String) Source # targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b Source # mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe () Source # map_theory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism Source # map_sentence :: CspCASL2CspCASL a b -> CspCASLSign -> CspCASLSen -> Result CspCASLSen Source # map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol Source # extractModel :: CspCASL2CspCASL a b -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2CspCASL a b -> Bool Source # has_model_expansion :: CspCASL2CspCASL a b -> Bool Source # is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool Source # constituents :: CspCASL2CspCASL a b -> [String] Source # isInclusionComorphism :: CspCASL2CspCASL a b -> Bool Source # rps :: CspCASL2CspCASL a b -> Bool Source # eps :: CspCASL2CspCASL a b -> Bool Source # isGTC :: CspCASL2CspCASL a b -> Bool Source #

class Show a => CspCASLSemantics a Source #

Instances

Instances details

CspCASLSemantics () Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods cspProvers :: () -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
CspCASLSemantics Failure Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods cspProvers :: Failure -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
CspCASLSemantics Trace Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods cspProvers :: Trace -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]

type CspCASL = GenCspCASL () Source #

The top-level logic with the loosest semantics (and without provers)

cspCASL :: GenCspCASL () Source #

data Trace Source #

Constructors

Trace

Instances

Instances details

Show Trace Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods showsPrec :: Int -> Trace -> ShowS show :: Trace -> String showList :: [Trace] -> ShowS
CspCASLSemantics Trace Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods cspProvers :: Trace -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]

traceCspCASL :: GenCspCASL Trace Source #

data Failure Source #

Constructors

Failure

Instances

Instances details

Show Failure Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods showsPrec :: Int -> Failure -> ShowS show :: Failure -> String showList :: [Failure] -> ShowS
CspCASLSemantics Failure Source #
Instance details Defined in CspCASL.Logic_CspCASL Methods cspProvers :: Failure -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]

failureCspCASL :: GenCspCASL Failure Source #