StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol Source # | Static Analysis for Rel |
Instance detailsDefined in RelationalScheme.Logic_Rel Methods basic_analysis :: RelScheme -> Maybe ((RSScheme, Sign, GlobalAnnos) -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])) Source # sen_analysis :: RelScheme -> Maybe ((RSScheme, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: RelScheme -> IRI -> LibName -> RSScheme -> Sign -> GlobalAnnos -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]) Source # stat_symb_map_items :: RelScheme -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RSRawSymbol) Source # stat_symb_items :: RelScheme -> Sign -> [()] -> Result [RSRawSymbol] Source # convertTheory :: RelScheme -> Maybe ((Sign, [Named Sentence]) -> RSScheme) Source # ensures_amalgamability :: RelScheme -> ([CASLAmalgOpt], Gr Sign (Int, RSMorphism), [(Int, RSMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: RelScheme -> RSMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: RelScheme -> Gr Sign (Int, RSMorphism) -> Result (Sign, Map Int RSMorphism) Source # qualify :: RelScheme -> SIMPLE_ID -> LibName -> RSMorphism -> Sign -> Result (RSMorphism, [Named Sentence]) Source # symbol_to_raw :: RelScheme -> RSSymbol -> RSRawSymbol Source # id_to_raw :: RelScheme -> Id -> RSRawSymbol Source # matches :: RelScheme -> RSSymbol -> RSRawSymbol -> Bool Source # empty_signature :: RelScheme -> Sign Source # add_symb_to_sign :: RelScheme -> Sign -> RSSymbol -> Result Sign Source # signature_union :: RelScheme -> Sign -> Sign -> Result Sign Source # signatureDiff :: RelScheme -> Sign -> Sign -> Result Sign Source # intersection :: RelScheme -> Sign -> Sign -> Result Sign Source # final_union :: RelScheme -> Sign -> Sign -> Result Sign Source # morphism_union :: RelScheme -> RSMorphism -> RSMorphism -> Result RSMorphism Source # is_subsig :: RelScheme -> Sign -> Sign -> Bool Source # subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism Source # generated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source # cogenerated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source # induced_from_morphism :: RelScheme -> EndoMap RSRawSymbol -> Sign -> Result RSMorphism Source # induced_from_to_morphism :: RelScheme -> EndoMap RSRawSymbol -> ExtSign Sign RSSymbol -> ExtSign Sign RSSymbol -> Result RSMorphism Source # is_transportable :: RelScheme -> RSMorphism -> Bool Source # is_injective :: RelScheme -> RSMorphism -> Bool Source # theory_to_taxonomy :: RelScheme -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: RelScheme -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap RSSymbol -> EndoMap RSSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source # equiv2cospan :: RelScheme -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source # extract_module :: RelScheme -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis RDF TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb Source # | |
Instance detailsDefined in RDF.Logic_RDF Methods basic_analysis :: RDF -> Maybe ((TurtleDocument, Sign, GlobalAnnos) -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom])) Source # sen_analysis :: RDF -> Maybe ((TurtleDocument, Sign, Axiom) -> Result Axiom) Source # extBasicAnalysis :: RDF -> IRI -> LibName -> TurtleDocument -> Sign -> GlobalAnnos -> Result (TurtleDocument, ExtSign Sign RDFEntity, [Named Axiom]) Source # stat_symb_map_items :: RDF -> Sign -> Maybe Sign -> [SymbMapItems] -> Result (EndoMap RawSymb) Source # stat_symb_items :: RDF -> Sign -> [SymbItems] -> Result [RawSymb] Source # convertTheory :: RDF -> Maybe ((Sign, [Named Axiom]) -> TurtleDocument) Source # ensures_amalgamability :: RDF -> ([CASLAmalgOpt], Gr Sign (Int, RDFMorphism), [(Int, RDFMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: RDF -> RDFMorphism -> [Named Axiom] -> Result (Sign, [Named Axiom]) Source # signature_colimit :: RDF -> Gr Sign (Int, RDFMorphism) -> Result (Sign, Map Int RDFMorphism) Source # qualify :: RDF -> SIMPLE_ID -> LibName -> RDFMorphism -> Sign -> Result (RDFMorphism, [Named Axiom]) Source # symbol_to_raw :: RDF -> RDFEntity -> RawSymb Source # id_to_raw :: RDF -> Id -> RawSymb Source # matches :: RDF -> RDFEntity -> RawSymb -> Bool Source # empty_signature :: RDF -> Sign Source # add_symb_to_sign :: RDF -> Sign -> RDFEntity -> Result Sign Source # signature_union :: RDF -> Sign -> Sign -> Result Sign Source # signatureDiff :: RDF -> Sign -> Sign -> Result Sign Source # intersection :: RDF -> Sign -> Sign -> Result Sign Source # final_union :: RDF -> Sign -> Sign -> Result Sign Source # morphism_union :: RDF -> RDFMorphism -> RDFMorphism -> Result RDFMorphism Source # is_subsig :: RDF -> Sign -> Sign -> Bool Source # subsig_inclusion :: RDF -> Sign -> Sign -> Result RDFMorphism Source # generated_sign :: RDF -> Set RDFEntity -> Sign -> Result RDFMorphism Source # cogenerated_sign :: RDF -> Set RDFEntity -> Sign -> Result RDFMorphism Source # induced_from_morphism :: RDF -> EndoMap RawSymb -> Sign -> Result RDFMorphism Source # induced_from_to_morphism :: RDF -> EndoMap RawSymb -> ExtSign Sign RDFEntity -> ExtSign Sign RDFEntity -> Result RDFMorphism Source # is_transportable :: RDF -> RDFMorphism -> Bool Source # is_injective :: RDF -> RDFMorphism -> Bool Source # theory_to_taxonomy :: RDF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Axiom] -> Result MMiSSOntology Source # corresp2th :: RDF -> String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> EndoMap RDFEntity -> EndoMap RDFEntity -> REL_REF -> Result (Sign, [Named Axiom], Sign, Sign, EndoMap RDFEntity, EndoMap RDFEntity) Source # equiv2cospan :: RDF -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> Result (Sign, Sign, Sign, EndoMap RDFEntity, EndoMap RDFEntity) Source # extract_module :: RDF -> [IRI] -> (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom]) Source # |
StaticAnalysis QVTR Transformation Sen () () Sign Morphism () () Source # | |
Instance detailsDefined in QVTR.Logic_QVTR Methods basic_analysis :: QVTR -> Maybe ((Transformation, Sign, GlobalAnnos) -> Result (Transformation, ExtSign Sign (), [Named Sen])) Source # sen_analysis :: QVTR -> Maybe ((Transformation, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: QVTR -> IRI -> LibName -> Transformation -> Sign -> GlobalAnnos -> Result (Transformation, ExtSign Sign (), [Named Sen]) Source # stat_symb_map_items :: QVTR -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: QVTR -> Sign -> [()] -> Result [()] Source # convertTheory :: QVTR -> Maybe ((Sign, [Named Sen]) -> Transformation) Source # ensures_amalgamability :: QVTR -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QVTR -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: QVTR -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QVTR -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: QVTR -> () -> () Source # id_to_raw :: QVTR -> Id -> () Source # matches :: QVTR -> () -> () -> Bool Source # empty_signature :: QVTR -> Sign Source # add_symb_to_sign :: QVTR -> Sign -> () -> Result Sign Source # signature_union :: QVTR -> Sign -> Sign -> Result Sign Source # signatureDiff :: QVTR -> Sign -> Sign -> Result Sign Source # intersection :: QVTR -> Sign -> Sign -> Result Sign Source # final_union :: QVTR -> Sign -> Sign -> Result Sign Source # morphism_union :: QVTR -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QVTR -> Sign -> Sign -> Bool Source # subsig_inclusion :: QVTR -> Sign -> Sign -> Result Morphism Source # generated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # cogenerated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # induced_from_morphism :: QVTR -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: QVTR -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source # is_transportable :: QVTR -> Morphism -> Bool Source # is_injective :: QVTR -> Morphism -> Bool Source # theory_to_taxonomy :: QVTR -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: QVTR -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: QVTR -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: QVTR -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source # |
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # | |
Instance detailsDefined in OMDoc.Logic_OMDoc Methods basic_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, GlobalAnnos) -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()])) Source # sen_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, ()) -> Result ()) Source # extBasicAnalysis :: OMDoc_PUN -> IRI -> LibName -> () -> OMDoc_Sign -> GlobalAnnos -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()]) Source # stat_symb_map_items :: OMDoc_PUN -> OMDoc_Sign -> Maybe OMDoc_Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: OMDoc_PUN -> OMDoc_Sign -> [()] -> Result [()] Source # convertTheory :: OMDoc_PUN -> Maybe ((OMDoc_Sign, [Named ()]) -> ()) Source # ensures_amalgamability :: OMDoc_PUN -> ([CASLAmalgOpt], Gr OMDoc_Sign (Int, OMDoc_Morphism), [(Int, OMDoc_Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: OMDoc_PUN -> OMDoc_Morphism -> [Named ()] -> Result (OMDoc_Sign, [Named ()]) Source # signature_colimit :: OMDoc_PUN -> Gr OMDoc_Sign (Int, OMDoc_Morphism) -> Result (OMDoc_Sign, Map Int OMDoc_Morphism) Source # qualify :: OMDoc_PUN -> SIMPLE_ID -> LibName -> OMDoc_Morphism -> OMDoc_Sign -> Result (OMDoc_Morphism, [Named ()]) Source # symbol_to_raw :: OMDoc_PUN -> Symbol -> () Source # id_to_raw :: OMDoc_PUN -> Id -> () Source # matches :: OMDoc_PUN -> Symbol -> () -> Bool Source # empty_signature :: OMDoc_PUN -> OMDoc_Sign Source # add_symb_to_sign :: OMDoc_PUN -> OMDoc_Sign -> Symbol -> Result OMDoc_Sign Source # signature_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # signatureDiff :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # intersection :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # final_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # morphism_union :: OMDoc_PUN -> OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism Source # is_subsig :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Bool Source # subsig_inclusion :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Morphism Source # generated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source # cogenerated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source # induced_from_morphism :: OMDoc_PUN -> EndoMap () -> OMDoc_Sign -> Result OMDoc_Morphism Source # induced_from_to_morphism :: OMDoc_PUN -> EndoMap () -> ExtSign OMDoc_Sign Symbol -> ExtSign OMDoc_Sign Symbol -> Result OMDoc_Morphism Source # is_transportable :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source # is_injective :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source # theory_to_taxonomy :: OMDoc_PUN -> TaxoGraphKind -> MMiSSOntology -> OMDoc_Sign -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: OMDoc_PUN -> String -> Bool -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (OMDoc_Sign, [Named ()], OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> Result (OMDoc_Sign, OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: OMDoc_PUN -> [IRI] -> (OMDoc_Sign, [Named ()]) -> Result (OMDoc_Sign, [Named ()]) Source # |
StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol Source # | Instance of StaticAnalysis for Maude |
Instance detailsDefined in Maude.Logic_Maude Methods basic_analysis :: Maude -> Maybe ((MaudeText, Sign, GlobalAnnos) -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence])) Source # sen_analysis :: Maude -> Maybe ((MaudeText, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: Maude -> IRI -> LibName -> MaudeText -> Sign -> GlobalAnnos -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence]) Source # stat_symb_map_items :: Maude -> Sign -> Maybe Sign -> [()] -> Result (EndoMap Symbol) Source # stat_symb_items :: Maude -> Sign -> [()] -> Result [Symbol] Source # convertTheory :: Maude -> Maybe ((Sign, [Named Sentence]) -> MaudeText) Source # ensures_amalgamability :: Maude -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Maude -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: Maude -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Maude -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: Maude -> Symbol -> Symbol Source # id_to_raw :: Maude -> Id -> Symbol Source # matches :: Maude -> Symbol -> Symbol -> Bool Source # empty_signature :: Maude -> Sign Source # add_symb_to_sign :: Maude -> Sign -> Symbol -> Result Sign Source # signature_union :: Maude -> Sign -> Sign -> Result Sign Source # signatureDiff :: Maude -> Sign -> Sign -> Result Sign Source # intersection :: Maude -> Sign -> Sign -> Result Sign Source # final_union :: Maude -> Sign -> Sign -> Result Sign Source # morphism_union :: Maude -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Maude -> Sign -> Sign -> Bool Source # subsig_inclusion :: Maude -> Sign -> Sign -> Result Morphism Source # generated_sign :: Maude -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Maude -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Maude -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Maude -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Maude -> Morphism -> Bool Source # is_injective :: Maude -> Morphism -> Bool Source # theory_to_taxonomy :: Maude -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: Maude -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Maude -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Maude -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source # | |
Instance detailsDefined in THF.Logic_THF Methods basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source # sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source # extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source # stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source # convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source # ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source # signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source # qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source # symbol_to_raw :: THF -> SymbolTHF -> () Source # id_to_raw :: THF -> Id -> () Source # matches :: THF -> SymbolTHF -> () -> Bool Source # empty_signature :: THF -> SignTHF Source # add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source # signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source # is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source # subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source # generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source # induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source # is_transportable :: THF -> MorphismTHF -> Bool Source # is_injective :: THF -> MorphismTHF -> Bool Source # theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source # corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # |
StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # | |
Instance detailsDefined in TPTP.Logic_TPTP Methods basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source # sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source # stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source # convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source # ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: TPTP -> Symbol -> () Source # id_to_raw :: TPTP -> Id -> () Source # matches :: TPTP -> Symbol -> () -> Bool Source # empty_signature :: TPTP -> Sign Source # add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source # signature_union :: TPTP -> Sign -> Sign -> Result Sign Source # signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source # intersection :: TPTP -> Sign -> Sign -> Result Sign Source # final_union :: TPTP -> Sign -> Sign -> Result Sign Source # morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: TPTP -> Sign -> Sign -> Bool Source # subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source # generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: TPTP -> Morphism -> Bool Source # is_injective :: TPTP -> Morphism -> Bool Source # theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source # | Static Analysis for propositional logic |
Instance detailsDefined in QBF.Logic_QBF Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # |
StaticAnalysis Propositional BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # | Static Analysis for propositional logic |
Instance detailsDefined in Propositional.Logic_Propositional Methods basic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: Propositional -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: Propositional -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source # ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Propositional -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Propositional -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: Propositional -> Symbol -> Symbol Source # id_to_raw :: Propositional -> Id -> Symbol Source # matches :: Propositional -> Symbol -> Symbol -> Bool Source # empty_signature :: Propositional -> Sign Source # add_symb_to_sign :: Propositional -> Sign -> Symbol -> Result Sign Source # signature_union :: Propositional -> Sign -> Sign -> Result Sign Source # signatureDiff :: Propositional -> Sign -> Sign -> Result Sign Source # intersection :: Propositional -> Sign -> Sign -> Result Sign Source # final_union :: Propositional -> Sign -> Sign -> Result Sign Source # morphism_union :: Propositional -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Propositional -> Sign -> Sign -> Bool Source # subsig_inclusion :: Propositional -> Sign -> Sign -> Result Morphism Source # generated_sign :: Propositional -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Propositional -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Propositional -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Propositional -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Propositional -> Morphism -> Bool Source # is_injective :: Propositional -> Morphism -> Bool Source # theory_to_taxonomy :: Propositional -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # |
StaticAnalysis OWL2 OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb Source # | |
Instance detailsDefined in OWL2.Logic_OWL2 Methods basic_analysis :: OWL2 -> Maybe ((OntologyDocument, Sign, GlobalAnnos) -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])) Source # sen_analysis :: OWL2 -> Maybe ((OntologyDocument, Sign, Axiom) -> Result Axiom) Source # extBasicAnalysis :: OWL2 -> IRI -> LibName -> OntologyDocument -> Sign -> GlobalAnnos -> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom]) Source # stat_symb_map_items :: OWL2 -> Sign -> Maybe Sign -> [SymbMapItems] -> Result (EndoMap RawSymb) Source # stat_symb_items :: OWL2 -> Sign -> [SymbItems] -> Result [RawSymb] Source # convertTheory :: OWL2 -> Maybe ((Sign, [Named Axiom]) -> OntologyDocument) Source # ensures_amalgamability :: OWL2 -> ([CASLAmalgOpt], Gr Sign (Int, OWLMorphism), [(Int, OWLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: OWL2 -> OWLMorphism -> [Named Axiom] -> Result (Sign, [Named Axiom]) Source # signature_colimit :: OWL2 -> Gr Sign (Int, OWLMorphism) -> Result (Sign, Map Int OWLMorphism) Source # qualify :: OWL2 -> SIMPLE_ID -> LibName -> OWLMorphism -> Sign -> Result (OWLMorphism, [Named Axiom]) Source # symbol_to_raw :: OWL2 -> Entity -> RawSymb Source # id_to_raw :: OWL2 -> Id -> RawSymb Source # matches :: OWL2 -> Entity -> RawSymb -> Bool Source # empty_signature :: OWL2 -> Sign Source # add_symb_to_sign :: OWL2 -> Sign -> Entity -> Result Sign Source # signature_union :: OWL2 -> Sign -> Sign -> Result Sign Source # signatureDiff :: OWL2 -> Sign -> Sign -> Result Sign Source # intersection :: OWL2 -> Sign -> Sign -> Result Sign Source # final_union :: OWL2 -> Sign -> Sign -> Result Sign Source # morphism_union :: OWL2 -> OWLMorphism -> OWLMorphism -> Result OWLMorphism Source # is_subsig :: OWL2 -> Sign -> Sign -> Bool Source # subsig_inclusion :: OWL2 -> Sign -> Sign -> Result OWLMorphism Source # generated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism Source # cogenerated_sign :: OWL2 -> Set Entity -> Sign -> Result OWLMorphism Source # induced_from_morphism :: OWL2 -> EndoMap RawSymb -> Sign -> Result OWLMorphism Source # induced_from_to_morphism :: OWL2 -> EndoMap RawSymb -> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism Source # is_transportable :: OWL2 -> OWLMorphism -> Bool Source # is_injective :: OWL2 -> OWLMorphism -> Bool Source # theory_to_taxonomy :: OWL2 -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Axiom] -> Result MMiSSOntology Source # corresp2th :: OWL2 -> String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> EndoMap Entity -> EndoMap Entity -> REL_REF -> Result (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity) Source # equiv2cospan :: OWL2 -> Sign -> Sign -> [SymbItems] -> [SymbItems] -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity) Source # extract_module :: OWL2 -> [IRI] -> (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom]) Source # |
StaticAnalysis NeSyPatterns BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # | Static Analysis for propositional logic |
Instance detailsDefined in NeSyPatterns.Logic_NeSyPatterns Methods basic_analysis :: NeSyPatterns -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()])) Source # sen_analysis :: NeSyPatterns -> Maybe ((BASIC_SPEC, Sign, ()) -> Result ()) Source # extBasicAnalysis :: NeSyPatterns -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named ()]) Source # stat_symb_map_items :: NeSyPatterns -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: NeSyPatterns -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: NeSyPatterns -> Maybe ((Sign, [Named ()]) -> BASIC_SPEC) Source # ensures_amalgamability :: NeSyPatterns -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: NeSyPatterns -> Morphism -> [Named ()] -> Result (Sign, [Named ()]) Source # signature_colimit :: NeSyPatterns -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: NeSyPatterns -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named ()]) Source # symbol_to_raw :: NeSyPatterns -> Symbol -> Symbol Source # id_to_raw :: NeSyPatterns -> Id -> Symbol Source # matches :: NeSyPatterns -> Symbol -> Symbol -> Bool Source # empty_signature :: NeSyPatterns -> Sign Source # add_symb_to_sign :: NeSyPatterns -> Sign -> Symbol -> Result Sign Source # signature_union :: NeSyPatterns -> Sign -> Sign -> Result Sign Source # signatureDiff :: NeSyPatterns -> Sign -> Sign -> Result Sign Source # intersection :: NeSyPatterns -> Sign -> Sign -> Result Sign Source # final_union :: NeSyPatterns -> Sign -> Sign -> Result Sign Source # morphism_union :: NeSyPatterns -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: NeSyPatterns -> Sign -> Sign -> Bool Source # subsig_inclusion :: NeSyPatterns -> Sign -> Sign -> Result Morphism Source # generated_sign :: NeSyPatterns -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: NeSyPatterns -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: NeSyPatterns -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: NeSyPatterns -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: NeSyPatterns -> Morphism -> Bool Source # is_injective :: NeSyPatterns -> Morphism -> Bool Source # theory_to_taxonomy :: NeSyPatterns -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: NeSyPatterns -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named ()], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: NeSyPatterns -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: NeSyPatterns -> [IRI] -> (Sign, [Named ()]) -> Result (Sign, [Named ()]) Source # |
StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM Source # | |
Instance detailsDefined in LF.Logic_LF Methods basic_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source # sen_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: LF -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source # stat_symb_map_items :: LF -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RAW_SYM) Source # stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [RAW_SYM] Source # convertTheory :: LF -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source # ensures_amalgamability :: LF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: LF -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: LF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: LF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: LF -> Symbol -> RAW_SYM Source # id_to_raw :: LF -> Id -> RAW_SYM Source # matches :: LF -> Symbol -> RAW_SYM -> Bool Source # empty_signature :: LF -> Sign Source # add_symb_to_sign :: LF -> Sign -> Symbol -> Result Sign Source # signature_union :: LF -> Sign -> Sign -> Result Sign Source # signatureDiff :: LF -> Sign -> Sign -> Result Sign Source # intersection :: LF -> Sign -> Sign -> Result Sign Source # final_union :: LF -> Sign -> Sign -> Result Sign Source # morphism_union :: LF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: LF -> Sign -> Sign -> Bool Source # subsig_inclusion :: LF -> Sign -> Sign -> Result Morphism Source # generated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: LF -> EndoMap RAW_SYM -> Sign -> Result Morphism Source # induced_from_to_morphism :: LF -> EndoMap RAW_SYM -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: LF -> Morphism -> Bool Source # is_injective :: LF -> Morphism -> Bool Source # theory_to_taxonomy :: LF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: LF -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: LF -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: LF -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source # | |
Instance detailsDefined in Isabelle.Logic_Isabelle Methods basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source # convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source # qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source # symbol_to_raw :: Isabelle -> () -> () Source # id_to_raw :: Isabelle -> Id -> () Source # matches :: Isabelle -> () -> () -> Bool Source # empty_signature :: Isabelle -> Sign Source # add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source # signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source # signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source # intersection :: Isabelle -> Sign -> Sign -> Result Sign Source # final_union :: Isabelle -> Sign -> Sign -> Result Sign Source # morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source # is_subsig :: Isabelle -> Sign -> Sign -> Bool Source # subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source # generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source # induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source # is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source # is_injective :: Isabelle -> IsabelleMorphism -> Bool Source # theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis HolLight () Sentence () () Sign HolLightMorphism () () Source # | Static Analysis for propositional logic |
Instance detailsDefined in HolLight.Logic_HolLight Methods basic_analysis :: HolLight -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: HolLight -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HolLight -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: HolLight -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: HolLight -> Sign -> [()] -> Result [()] Source # convertTheory :: HolLight -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: HolLight -> ([CASLAmalgOpt], Gr Sign (Int, HolLightMorphism), [(Int, HolLightMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HolLight -> HolLightMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: HolLight -> Gr Sign (Int, HolLightMorphism) -> Result (Sign, Map Int HolLightMorphism) Source # qualify :: HolLight -> SIMPLE_ID -> LibName -> HolLightMorphism -> Sign -> Result (HolLightMorphism, [Named Sentence]) Source # symbol_to_raw :: HolLight -> () -> () Source # id_to_raw :: HolLight -> Id -> () Source # matches :: HolLight -> () -> () -> Bool Source # empty_signature :: HolLight -> Sign Source # add_symb_to_sign :: HolLight -> Sign -> () -> Result Sign Source # signature_union :: HolLight -> Sign -> Sign -> Result Sign Source # signatureDiff :: HolLight -> Sign -> Sign -> Result Sign Source # intersection :: HolLight -> Sign -> Sign -> Result Sign Source # final_union :: HolLight -> Sign -> Sign -> Result Sign Source # morphism_union :: HolLight -> HolLightMorphism -> HolLightMorphism -> Result HolLightMorphism Source # is_subsig :: HolLight -> Sign -> Sign -> Bool Source # subsig_inclusion :: HolLight -> Sign -> Sign -> Result HolLightMorphism Source # generated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source # cogenerated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source # induced_from_morphism :: HolLight -> EndoMap () -> Sign -> Result HolLightMorphism Source # induced_from_to_morphism :: HolLight -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result HolLightMorphism Source # is_transportable :: HolLight -> HolLightMorphism -> Bool Source # is_injective :: HolLight -> HolLightMorphism -> Bool Source # theory_to_taxonomy :: HolLight -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HolLight -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: HolLight -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: HolLight -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # | |
Instance detailsDefined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # |
StaticAnalysis FreeCAD Document () () () Sign FCMorphism () () Source # | |
Instance detailsDefined in FreeCAD.Logic_FreeCAD Methods basic_analysis :: FreeCAD -> Maybe ((Document, Sign, GlobalAnnos) -> Result (Document, ExtSign Sign (), [Named ()])) Source # sen_analysis :: FreeCAD -> Maybe ((Document, Sign, ()) -> Result ()) Source # extBasicAnalysis :: FreeCAD -> IRI -> LibName -> Document -> Sign -> GlobalAnnos -> Result (Document, ExtSign Sign (), [Named ()]) Source # stat_symb_map_items :: FreeCAD -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: FreeCAD -> Sign -> [()] -> Result [()] Source # convertTheory :: FreeCAD -> Maybe ((Sign, [Named ()]) -> Document) Source # ensures_amalgamability :: FreeCAD -> ([CASLAmalgOpt], Gr Sign (Int, FCMorphism), [(Int, FCMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: FreeCAD -> FCMorphism -> [Named ()] -> Result (Sign, [Named ()]) Source # signature_colimit :: FreeCAD -> Gr Sign (Int, FCMorphism) -> Result (Sign, Map Int FCMorphism) Source # qualify :: FreeCAD -> SIMPLE_ID -> LibName -> FCMorphism -> Sign -> Result (FCMorphism, [Named ()]) Source # symbol_to_raw :: FreeCAD -> () -> () Source # id_to_raw :: FreeCAD -> Id -> () Source # matches :: FreeCAD -> () -> () -> Bool Source # empty_signature :: FreeCAD -> Sign Source # add_symb_to_sign :: FreeCAD -> Sign -> () -> Result Sign Source # signature_union :: FreeCAD -> Sign -> Sign -> Result Sign Source # signatureDiff :: FreeCAD -> Sign -> Sign -> Result Sign Source # intersection :: FreeCAD -> Sign -> Sign -> Result Sign Source # final_union :: FreeCAD -> Sign -> Sign -> Result Sign Source # morphism_union :: FreeCAD -> FCMorphism -> FCMorphism -> Result FCMorphism Source # is_subsig :: FreeCAD -> Sign -> Sign -> Bool Source # subsig_inclusion :: FreeCAD -> Sign -> Sign -> Result FCMorphism Source # generated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source # cogenerated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source # induced_from_morphism :: FreeCAD -> EndoMap () -> Sign -> Result FCMorphism Source # induced_from_to_morphism :: FreeCAD -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result FCMorphism Source # is_transportable :: FreeCAD -> FCMorphism -> Bool Source # is_injective :: FreeCAD -> FCMorphism -> Bool Source # theory_to_taxonomy :: FreeCAD -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: FreeCAD -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named ()], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: FreeCAD -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: FreeCAD -> [IRI] -> (Sign, [Named ()]) -> Result (Sign, [Named ()]) Source # |
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # | |
Instance detailsDefined in Framework.Logic_Framework Methods basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source # sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source # extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source # stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source # convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source # ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source # signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source # qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source # symbol_to_raw :: FrameworkCom -> () -> () Source # id_to_raw :: FrameworkCom -> Id -> () Source # matches :: FrameworkCom -> () -> () -> Bool Source # empty_signature :: FrameworkCom -> ComorphismDef Source # add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source # signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source # is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source # subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source # generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source # induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source # is_transportable :: FrameworkCom -> MorphismCom -> Bool Source # is_injective :: FrameworkCom -> MorphismCom -> Bool Source # theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source # |
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source # | |
Instance detailsDefined in Framework.Logic_Framework Methods basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source # sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source # extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source # stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source # convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source # ensures_amalgamability :: Framework -> ([CASLAmalgOpt], Gr LogicDef (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source # signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source # qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source # symbol_to_raw :: Framework -> () -> () Source # id_to_raw :: Framework -> Id -> () Source # matches :: Framework -> () -> () -> Bool Source # empty_signature :: Framework -> LogicDef Source # add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source # signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # morphism_union :: Framework -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source # subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source # generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source # induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source # is_transportable :: Framework -> Morphism -> Bool Source # is_injective :: Framework -> Morphism -> Bool Source # theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source # |
StaticAnalysis DFOL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # | |
Instance detailsDefined in DFOL.Logic_DFOL Methods basic_analysis :: DFOL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: DFOL -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: DFOL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: DFOL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: DFOL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: DFOL -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source # ensures_amalgamability :: DFOL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: DFOL -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: DFOL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: DFOL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: DFOL -> Symbol -> Symbol Source # id_to_raw :: DFOL -> Id -> Symbol Source # matches :: DFOL -> Symbol -> Symbol -> Bool Source # empty_signature :: DFOL -> Sign Source # add_symb_to_sign :: DFOL -> Sign -> Symbol -> Result Sign Source # signature_union :: DFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: DFOL -> Sign -> Sign -> Result Sign Source # intersection :: DFOL -> Sign -> Sign -> Result Sign Source # final_union :: DFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: DFOL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: DFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: DFOL -> Sign -> Sign -> Result Morphism Source # generated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: DFOL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: DFOL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: DFOL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: DFOL -> Morphism -> Bool Source # is_injective :: DFOL -> Morphism -> Bool Source # theory_to_taxonomy :: DFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: DFOL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: DFOL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: DFOL -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # |
StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # | |
Instance detailsDefined in CommonLogic.Logic_CommonLogic Methods basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source # sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source # extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source # stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source # ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source # signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source # symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source # id_to_raw :: CommonLogic -> Id -> Symbol Source # matches :: CommonLogic -> Symbol -> Symbol -> Bool Source # empty_signature :: CommonLogic -> Sign Source # add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source # signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source # signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source # intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source # final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source # morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source # subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source # generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CommonLogic -> Morphism -> Bool Source # is_injective :: CommonLogic -> Morphism -> Bool Source # theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source # corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # |
StaticAnalysis CSMOF Metamodel Sen () () Sign Morphism () () Source # | |
Instance detailsDefined in CSMOF.Logic_CSMOF Methods basic_analysis :: CSMOF -> Maybe ((Metamodel, Sign, GlobalAnnos) -> Result (Metamodel, ExtSign Sign (), [Named Sen])) Source # sen_analysis :: CSMOF -> Maybe ((Metamodel, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: CSMOF -> IRI -> LibName -> Metamodel -> Sign -> GlobalAnnos -> Result (Metamodel, ExtSign Sign (), [Named Sen]) Source # stat_symb_map_items :: CSMOF -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: CSMOF -> Sign -> [()] -> Result [()] Source # convertTheory :: CSMOF -> Maybe ((Sign, [Named Sen]) -> Metamodel) Source # ensures_amalgamability :: CSMOF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSMOF -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: CSMOF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSMOF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: CSMOF -> () -> () Source # id_to_raw :: CSMOF -> Id -> () Source # matches :: CSMOF -> () -> () -> Bool Source # empty_signature :: CSMOF -> Sign Source # add_symb_to_sign :: CSMOF -> Sign -> () -> Result Sign Source # signature_union :: CSMOF -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSMOF -> Sign -> Sign -> Result Sign Source # intersection :: CSMOF -> Sign -> Sign -> Result Sign Source # final_union :: CSMOF -> Sign -> Sign -> Result Sign Source # morphism_union :: CSMOF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSMOF -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSMOF -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSMOF -> Set () -> Sign -> Result Morphism Source # cogenerated_sign :: CSMOF -> Set () -> Sign -> Result Morphism Source # induced_from_morphism :: CSMOF -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSMOF -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source # is_transportable :: CSMOF -> Morphism -> Bool Source # is_injective :: CSMOF -> Morphism -> Bool Source # theory_to_taxonomy :: CSMOF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: CSMOF -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: CSMOF -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: CSMOF -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source # |
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # | Static Analysis for reduce logic |
Instance detailsDefined in CSL.Logic_CSL Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source # |
StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol Source # | |
Instance detailsDefined in Adl.Logic_Adl Methods basic_analysis :: Adl -> Maybe ((Context, Sign, GlobalAnnos) -> Result (Context, ExtSign Sign Symbol, [Named Sen])) Source # sen_analysis :: Adl -> Maybe ((Context, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: Adl -> IRI -> LibName -> Context -> Sign -> GlobalAnnos -> Result (Context, ExtSign Sign Symbol, [Named Sen]) Source # stat_symb_map_items :: Adl -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Adl -> Sign -> [()] -> Result [RawSymbol] Source # convertTheory :: Adl -> Maybe ((Sign, [Named Sen]) -> Context) Source # ensures_amalgamability :: Adl -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Adl -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: Adl -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Adl -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: Adl -> Symbol -> RawSymbol Source # id_to_raw :: Adl -> Id -> RawSymbol Source # matches :: Adl -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Adl -> Sign Source # add_symb_to_sign :: Adl -> Sign -> Symbol -> Result Sign Source # signature_union :: Adl -> Sign -> Sign -> Result Sign Source # signatureDiff :: Adl -> Sign -> Sign -> Result Sign Source # intersection :: Adl -> Sign -> Sign -> Result Sign Source # final_union :: Adl -> Sign -> Sign -> Result Sign Source # morphism_union :: Adl -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Adl -> Sign -> Sign -> Bool Source # subsig_inclusion :: Adl -> Sign -> Sign -> Result Morphism Source # generated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Adl -> EndoMap RawSymbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Adl -> EndoMap RawSymbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Adl -> Morphism -> Bool Source # is_injective :: Adl -> Morphism -> Bool Source # theory_to_taxonomy :: Adl -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: Adl -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Adl -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Adl -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source # |
StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # | |
Instance detailsDefined in CASL.Logic_CASL Methods basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source # sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source # extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source # stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source # ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source # signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source # qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source # symbol_to_raw :: CASL -> Symbol -> RawSymbol Source # id_to_raw :: CASL -> Id -> RawSymbol Source # matches :: CASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CASL -> CASLSign Source # add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source # signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source # is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source # subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source # generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source # cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source # induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source # induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source # is_transportable :: CASL -> CASLMor -> Bool Source # is_injective :: CASL -> CASLMor -> Bool Source # theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # |
StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # | |
Instance detailsDefined in Modal.Logic_Modal Methods basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source # sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source # extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source # stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source # ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source # signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source # qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source # symbol_to_raw :: Modal -> Symbol -> RawSymbol Source # id_to_raw :: Modal -> Id -> RawSymbol Source # matches :: Modal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Modal -> MSign Source # add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source # signature_union :: Modal -> MSign -> MSign -> Result MSign Source # signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source # intersection :: Modal -> MSign -> MSign -> Result MSign Source # final_union :: Modal -> MSign -> MSign -> Result MSign Source # morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source # is_subsig :: Modal -> MSign -> MSign -> Bool Source # subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source # generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source # induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source # is_transportable :: Modal -> ModalMor -> Bool Source # is_injective :: Modal -> ModalMor -> Bool Source # theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # |
StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # | |
Instance detailsDefined in Hybrid.Logic_Hybrid Methods basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source # sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source # extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source # stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source # ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source # signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source # qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source # symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source # id_to_raw :: Hybrid -> Id -> RawSymbol Source # matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybrid -> HSign Source # add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source # signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source # signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source # intersection :: Hybrid -> HSign -> HSign -> Result HSign Source # final_union :: Hybrid -> HSign -> HSign -> Result HSign Source # morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source # is_subsig :: Hybrid -> HSign -> HSign -> Bool Source # subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source # generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source # induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source # is_transportable :: Hybrid -> HybridMor -> Bool Source # is_injective :: Hybrid -> HybridMor -> Bool Source # theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source # corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # |
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # | |
Instance detailsDefined in Fpl.Logic_Fpl Methods basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source # sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source # extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source # stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source # ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source # signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source # qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source # symbol_to_raw :: Fpl -> Symbol -> RawSymbol Source # id_to_raw :: Fpl -> Id -> RawSymbol Source # matches :: Fpl -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Fpl -> FplSign Source # add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source # signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source # signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source # intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source # final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source # morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source # is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source # subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source # generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source # cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source # induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source # induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source # is_transportable :: Fpl -> FplMor -> Bool Source # is_injective :: Fpl -> FplMor -> Bool Source # theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source # corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source # |
StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # | |
Instance detailsDefined in ExtModal.Logic_ExtModal Methods basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source # sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source # extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source # stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source # ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source # qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source # symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source # id_to_raw :: ExtModal -> Id -> RawSymbol Source # matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ExtModal -> ExtModalSign Source # add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source # signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source # is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source # subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source # generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source # is_transportable :: ExtModal -> ExtModalMorph -> Bool Source # is_injective :: ExtModal -> ExtModalMorph -> Bool Source # theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # |
StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # | |
Instance detailsDefined in ConstraintCASL.Logic_ConstraintCASL Methods basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source # sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source # extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source # stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source # ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source # qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source # symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol Source # id_to_raw :: ConstraintCASL -> Id -> RawSymbol Source # matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ConstraintCASL -> ConstraintCASLSign Source # add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source # signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source # is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source # subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source # generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source # is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source # is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source # theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # |
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # | |
Instance detailsDefined 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 # |
StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # | |
Instance detailsDefined in COL.Logic_COL Methods basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source # sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source # extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source # stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source # signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source # qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source # symbol_to_raw :: COL -> Symbol -> RawSymbol Source # id_to_raw :: COL -> Id -> RawSymbol Source # matches :: COL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: COL -> CSign Source # add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source # signature_union :: COL -> CSign -> CSign -> Result CSign Source # signatureDiff :: COL -> CSign -> CSign -> Result CSign Source # intersection :: COL -> CSign -> CSign -> Result CSign Source # final_union :: COL -> CSign -> CSign -> Result CSign Source # morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source # is_subsig :: COL -> CSign -> CSign -> Bool Source # subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source # generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source # induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source # is_transportable :: COL -> COLMor -> Bool Source # is_injective :: COL -> COLMor -> Bool Source # theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source # corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source # |
StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # | |
Instance detailsDefined in CASL_DL.Logic_CASL_DL Methods basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source # sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source # extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source # stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source # ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source # signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source # qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source # symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source # id_to_raw :: CASL_DL -> Id -> RawSymbol Source # matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CASL_DL -> DLSign Source # add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source # signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source # is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source # subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source # generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source # induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source # is_transportable :: CASL_DL -> DLMor -> Bool Source # is_injective :: CASL_DL -> DLMor -> Bool Source # theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source # |
StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol Source # | Static Analysis for propositional logic |
Instance detailsDefined in Temporal.Logic_Temporal Methods basic_analysis :: Temporal -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: Temporal -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: Temporal -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: Temporal -> Sign -> Maybe Sign -> [()] -> Result (EndoMap Symbol) Source # stat_symb_items :: Temporal -> Sign -> [()] -> Result [Symbol] Source # convertTheory :: Temporal -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source # ensures_amalgamability :: Temporal -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Temporal -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: Temporal -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Temporal -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: Temporal -> Symbol -> Symbol Source # id_to_raw :: Temporal -> Id -> Symbol Source # matches :: Temporal -> Symbol -> Symbol -> Bool Source # empty_signature :: Temporal -> Sign Source # add_symb_to_sign :: Temporal -> Sign -> Symbol -> Result Sign Source # signature_union :: Temporal -> Sign -> Sign -> Result Sign Source # signatureDiff :: Temporal -> Sign -> Sign -> Result Sign Source # intersection :: Temporal -> Sign -> Sign -> Result Sign Source # final_union :: Temporal -> Sign -> Sign -> Result Sign Source # morphism_union :: Temporal -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Temporal -> Sign -> Sign -> Bool Source # subsig_inclusion :: Temporal -> Sign -> Sign -> Result Morphism Source # generated_sign :: Temporal -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Temporal -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Temporal -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Temporal -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Temporal -> Morphism -> Bool Source # is_injective :: Temporal -> Morphism -> Bool Source # theory_to_taxonomy :: Temporal -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: Temporal -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Temporal -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Temporal -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # |
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source # | |
Instance detailsDefined in TopHybrid.Logic_TopHybrid Methods basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source # sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source # extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source # stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source # ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source # qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source # symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source # id_to_raw :: Hybridize -> Id -> RawSymbol Source # matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybridize -> Sgn_Wrap Source # add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source # signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source # is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source # subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source # generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source # induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source # is_transportable :: Hybridize -> Mor -> Bool Source # is_injective :: Hybridize -> Mor -> Bool Source # theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source # corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # |
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # | |
Instance detailsDefined 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 # |
StaticAnalysis DMU Text () () () Text (DefaultMorphism Text) () () Source # | |
Instance detailsDefined in DMU.Logic_DMU Methods basic_analysis :: DMU -> Maybe ((Text, Text, GlobalAnnos) -> Result (Text, ExtSign Text (), [Named ()])) Source # sen_analysis :: DMU -> Maybe ((Text, Text, ()) -> Result ()) Source # extBasicAnalysis :: DMU -> IRI -> LibName -> Text -> Text -> GlobalAnnos -> Result (Text, ExtSign Text (), [Named ()]) Source # stat_symb_map_items :: DMU -> Text -> Maybe Text -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: DMU -> Text -> [()] -> Result [()] Source # convertTheory :: DMU -> Maybe ((Text, [Named ()]) -> Text) Source # ensures_amalgamability :: DMU -> ([CASLAmalgOpt], Gr Text (Int, DefaultMorphism Text), [(Int, DefaultMorphism Text)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: DMU -> DefaultMorphism Text -> [Named ()] -> Result (Text, [Named ()]) Source # signature_colimit :: DMU -> Gr Text (Int, DefaultMorphism Text) -> Result (Text, Map Int (DefaultMorphism Text)) Source # qualify :: DMU -> SIMPLE_ID -> LibName -> DefaultMorphism Text -> Text -> Result (DefaultMorphism Text, [Named ()]) Source # symbol_to_raw :: DMU -> () -> () Source # id_to_raw :: DMU -> Id -> () Source # matches :: DMU -> () -> () -> Bool Source # empty_signature :: DMU -> Text Source # add_symb_to_sign :: DMU -> Text -> () -> Result Text Source # signature_union :: DMU -> Text -> Text -> Result Text Source # signatureDiff :: DMU -> Text -> Text -> Result Text Source # intersection :: DMU -> Text -> Text -> Result Text Source # final_union :: DMU -> Text -> Text -> Result Text Source # morphism_union :: DMU -> DefaultMorphism Text -> DefaultMorphism Text -> Result (DefaultMorphism Text) Source # is_subsig :: DMU -> Text -> Text -> Bool Source # subsig_inclusion :: DMU -> Text -> Text -> Result (DefaultMorphism Text) Source # generated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # cogenerated_sign :: DMU -> Set () -> Text -> Result (DefaultMorphism Text) Source # induced_from_morphism :: DMU -> EndoMap () -> Text -> Result (DefaultMorphism Text) Source # induced_from_to_morphism :: DMU -> EndoMap () -> ExtSign Text () -> ExtSign Text () -> Result (DefaultMorphism Text) Source # is_transportable :: DMU -> DefaultMorphism Text -> Bool Source # is_injective :: DMU -> DefaultMorphism Text -> Bool Source # theory_to_taxonomy :: DMU -> TaxoGraphKind -> MMiSSOntology -> Text -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: DMU -> String -> Bool -> Text -> Text -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Text, [Named ()], Text, Text, EndoMap (), EndoMap ()) Source # equiv2cospan :: DMU -> Text -> Text -> [()] -> [()] -> Result (Text, Text, Text, EndoMap (), EndoMap ()) Source # extract_module :: DMU -> [IRI] -> (Text, [Named ()]) -> Result (Text, [Named ()]) Source # |
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # | |
Instance detailsDefined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source # |
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source # | Static Analysis for CspCASL |
Instance detailsDefined 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 # |
(Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2, Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1, Data sentence2) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source # | |
Instance detailsDefined in Logic.Morphism Methods basic_analysis :: SpanDomain cid -> Maybe (((), sign1, GlobalAnnos) -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)])) Source # sen_analysis :: SpanDomain cid -> Maybe (((), sign1, S2 sentence2) -> Result (S2 sentence2)) Source # extBasicAnalysis :: SpanDomain cid -> IRI -> LibName -> () -> sign1 -> GlobalAnnos -> Result ((), ExtSign sign1 sign_symbol1, [Named (S2 sentence2)]) Source # stat_symb_map_items :: SpanDomain cid -> sign1 -> Maybe sign1 -> [()] -> Result (EndoMap symbol1) Source # stat_symb_items :: SpanDomain cid -> sign1 -> [()] -> Result [symbol1] Source # convertTheory :: SpanDomain cid -> Maybe ((sign1, [Named (S2 sentence2)]) -> ()) Source # ensures_amalgamability :: SpanDomain cid -> ([CASLAmalgOpt], Gr sign1 (Int, morphism1), [(Int, morphism1)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SpanDomain cid -> morphism1 -> [Named (S2 sentence2)] -> Result (sign1, [Named (S2 sentence2)]) Source # signature_colimit :: SpanDomain cid -> Gr sign1 (Int, morphism1) -> Result (sign1, Map Int morphism1) Source # qualify :: SpanDomain cid -> SIMPLE_ID -> LibName -> morphism1 -> sign1 -> Result (morphism1, [Named (S2 sentence2)]) Source # symbol_to_raw :: SpanDomain cid -> sign_symbol1 -> symbol1 Source # id_to_raw :: SpanDomain cid -> Id -> symbol1 Source # matches :: SpanDomain cid -> sign_symbol1 -> symbol1 -> Bool Source # empty_signature :: SpanDomain cid -> sign1 Source # add_symb_to_sign :: SpanDomain cid -> sign1 -> sign_symbol1 -> Result sign1 Source # signature_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # signatureDiff :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # intersection :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # final_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1 Source # morphism_union :: SpanDomain cid -> morphism1 -> morphism1 -> Result morphism1 Source # is_subsig :: SpanDomain cid -> sign1 -> sign1 -> Bool Source # subsig_inclusion :: SpanDomain cid -> sign1 -> sign1 -> Result morphism1 Source # generated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # cogenerated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1 Source # induced_from_morphism :: SpanDomain cid -> EndoMap symbol1 -> sign1 -> Result morphism1 Source # induced_from_to_morphism :: SpanDomain cid -> EndoMap symbol1 -> ExtSign sign1 sign_symbol1 -> ExtSign sign1 sign_symbol1 -> Result morphism1 Source # is_transportable :: SpanDomain cid -> morphism1 -> Bool Source # is_injective :: SpanDomain cid -> morphism1 -> Bool Source # theory_to_taxonomy :: SpanDomain cid -> TaxoGraphKind -> MMiSSOntology -> sign1 -> [Named (S2 sentence2)] -> Result MMiSSOntology Source # corresp2th :: SpanDomain cid -> String -> Bool -> sign1 -> sign1 -> [()] -> [()] -> EndoMap sign_symbol1 -> EndoMap sign_symbol1 -> REL_REF -> Result (sign1, [Named (S2 sentence2)], sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # equiv2cospan :: SpanDomain cid -> sign1 -> sign1 -> [()] -> [()] -> Result (sign1, sign1, sign1, EndoMap sign_symbol1, EndoMap sign_symbol1) Source # extract_module :: SpanDomain cid -> [IRI] -> (sign1, [Named (S2 sentence2)]) -> Result (sign1, [Named (S2 sentence2)]) Source # |