Copyright	(c) C. Maeder DFKI 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (via Logic.Logic)
Safe Haskell	None

VSE.Logic_VSE

Contents

Orphan instances

Description

morphisms and symbols need to be extended, too

Documentation

data VSE Source #

Constructors

VSE

Instances

Instances details

Show VSE Source #
Instance details Defined in VSE.Logic_VSE Methods showsPrec :: Int -> VSE -> ShowS show :: VSE -> String showList :: [VSE] -> ShowS
Language VSE Source #
Instance details Defined in VSE.Logic_VSE Methods language_name :: VSE -> String Source # description :: VSE -> String Source #
Sentences VSE Sentence VSESign VSEMor Symbol Source #
Instance details Defined in VSE.Logic_VSE Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in VSE.Logic_VSE Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Instance details Defined in VSE.Logic_VSE Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in VSE.Logic_VSE Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source # sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSERefine Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #

interSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e) Source #

Orphan instances

SignExtension Procs Source #
Instance details Methods isSubSignExtension :: Procs -> Procs -> Bool Source #