Copyright	(c) Till Mossakowski Uni Bremen 2002-2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	hausmann@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	None

CoCASL.Logic_CoCASL

Contents

Orphan instances

Description

Instance of class Logic for CoCASL.

Documentation

data CoCASL Source #

Constructors

CoCASL

Instances

Instances details

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

type CoCASLMor = Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign) Source #

type CoCASLFORMULA = FORMULA C_FORMULA Source #

map_C_FORMULA :: MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign) Source #

parseCo :: String -> Maybe (Bool, String) Source #

Orphan instances

SignExtension CoCASLSign Source #
Instance details Methods isSubSignExtension :: CoCASLSign -> CoCASLSign -> Bool Source #
NameSL Bool Source #
Instance details Methods nameSL :: Bool -> String Source #
ProjForm Bool C_FORMULA Source #
Instance details Methods projForm :: CASL_SL Bool -> C_FORMULA -> Maybe (FORMULA C_FORMULA) Source #
MinSL Bool C_FORMULA Source #
Instance details Methods minSL :: C_FORMULA -> CASL_SL Bool Source #
MinSL Bool C_SIG_ITEM Source #
Instance details Methods minSL :: C_SIG_ITEM -> CASL_SL Bool Source #
MinSL Bool C_BASIC_ITEM Source #
Instance details Methods minSL :: C_BASIC_ITEM -> CASL_SL Bool Source #
MinSL Bool CoCASLSign Source #
Instance details Methods minSL :: CoCASLSign -> CASL_SL Bool Source #
ProjSigItem Bool C_SIG_ITEM C_FORMULA Source #
Instance details Methods projSigItems :: CASL_SL Bool -> C_SIG_ITEM -> (Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA), [SORT]) Source #
ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #
Instance details Methods projBasicItems :: CASL_SL Bool -> C_BASIC_ITEM -> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [SORT]) Source #