Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

Common.DefaultMorphism

Description

Supply a default morphism for a given signature type

Documentation

data DefaultMorphism sign Source #

Constructors

MkMorphism 

Instances

Sentences CSMOF Sen Sign Morphism () Source # 

Methods

map_sen :: CSMOF -> Morphism -> Sen -> Result Sen Source #

simplify_sen :: CSMOF -> Sign -> Sen -> Sen Source #

negation :: CSMOF -> Sen -> Maybe Sen Source #

print_sign :: CSMOF -> Sign -> Doc Source #

print_named :: CSMOF -> Named Sen -> Doc Source #

sym_of :: CSMOF -> Sign -> [Set ()] Source #

mostSymsOf :: CSMOF -> Sign -> [()] Source #

symmap_of :: CSMOF -> Morphism -> EndoMap () Source #

sym_name :: CSMOF -> () -> Id Source #

sym_label :: CSMOF -> () -> Maybe String Source #

fullSymName :: CSMOF -> () -> String Source #

symKind :: CSMOF -> () -> String Source #

symsOfSen :: CSMOF -> Sign -> Sen -> [()] Source #

pair_symbols :: CSMOF -> () -> () -> Result () Source #

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
Sentences QVTR Sen Sign Morphism () Source # 

Methods

map_sen :: QVTR -> Morphism -> Sen -> Result Sen Source #

simplify_sen :: QVTR -> Sign -> Sen -> Sen Source #

negation :: QVTR -> Sen -> Maybe Sen Source #

print_sign :: QVTR -> Sign -> Doc Source #

print_named :: QVTR -> Named Sen -> Doc Source #

sym_of :: QVTR -> Sign -> [Set ()] Source #

mostSymsOf :: QVTR -> Sign -> [()] Source #

symmap_of :: QVTR -> Morphism -> EndoMap () Source #

sym_name :: QVTR -> () -> Id Source #

sym_label :: QVTR -> () -> Maybe String Source #

fullSymName :: QVTR -> () -> String Source #

symKind :: QVTR -> () -> String Source #

symsOfSen :: QVTR -> Sign -> Sen -> [()] Source #

pair_symbols :: QVTR -> () -> () -> Result () Source #

Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source # 
Sentences Adl Sen Sign Morphism Symbol Source # 
Sentences FrameworkCom () ComorphismDef MorphismCom () Source # 
Sentences Framework () LogicDef Morphism () Source # 

Methods

map_sen :: Framework -> Morphism -> () -> Result () Source #

simplify_sen :: Framework -> LogicDef -> () -> () Source #

negation :: Framework -> () -> Maybe () Source #

print_sign :: Framework -> LogicDef -> Doc Source #

print_named :: Framework -> Named () -> Doc Source #

sym_of :: Framework -> LogicDef -> [Set ()] Source #

mostSymsOf :: Framework -> LogicDef -> [()] Source #

symmap_of :: Framework -> Morphism -> EndoMap () Source #

sym_name :: Framework -> () -> Id Source #

sym_label :: Framework -> () -> Maybe String Source #

fullSymName :: Framework -> () -> String Source #

symKind :: Framework -> () -> String Source #

symsOfSen :: Framework -> LogicDef -> () -> [()] Source #

pair_symbols :: Framework -> () -> () -> Result () Source #

Sentences FreeCAD () Sign FCMorphism () Source # 

Methods

map_sen :: FreeCAD -> FCMorphism -> () -> Result () Source #

simplify_sen :: FreeCAD -> Sign -> () -> () Source #

negation :: FreeCAD -> () -> Maybe () Source #

print_sign :: FreeCAD -> Sign -> Doc Source #

print_named :: FreeCAD -> Named () -> Doc Source #

sym_of :: FreeCAD -> Sign -> [Set ()] Source #

mostSymsOf :: FreeCAD -> Sign -> [()] Source #

symmap_of :: FreeCAD -> FCMorphism -> EndoMap () Source #

sym_name :: FreeCAD -> () -> Id Source #

sym_label :: FreeCAD -> () -> Maybe String Source #

fullSymName :: FreeCAD -> () -> String Source #

symKind :: FreeCAD -> () -> String Source #

symsOfSen :: FreeCAD -> Sign -> () -> [()] Source #

pair_symbols :: FreeCAD -> () -> () -> Result () Source #

Sentences HolLight Sentence Sign HolLightMorphism () Source # 
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source # 
Sentences TPTP Sentence Sign Morphism Symbol Source # 
StaticAnalysis CSMOF Metamodel Sen () () Sign Morphism () () Source # 

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 Isabelle () Sentence () () Sign IsabelleMorphism () () Source # 

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 QVTR Transformation Sen () () Sign Morphism () () Source # 

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 THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source # 

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 Adl Context Sen () () Sign Morphism Symbol RawSymbol Source # 

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 FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # 

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 # 

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 FreeCAD Document () () () Sign FCMorphism () () Source # 

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 HolLight () Sentence () () Sign HolLightMorphism () () Source #

Static Analysis for propositional logic

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 TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # 

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 #

LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

base_sig :: Isabelle -> Sign Source #

write_logic :: Isabelle -> String -> String Source #

write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_model :: Isabelle -> String -> IsabelleMorphism -> String Source #

read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source #

write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #

Logic CSMOF () Metamodel Sen () () Sign Morphism () () () Source # 

Methods

parse_basic_sen :: CSMOF -> Maybe (Metamodel -> AParser st Sen) Source #

stability :: CSMOF -> Stability Source #

data_logic :: CSMOF -> Maybe AnyLogic Source #

top_sublogic :: CSMOF -> () Source #

all_sublogics :: CSMOF -> [()] Source #

bottomSublogic :: CSMOF -> Maybe () Source #

sublogicDimensions :: CSMOF -> [[()]] Source #

parseSublogic :: CSMOF -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSMOF -> () -> Sign -> Morphism Source #

provers :: CSMOF -> [Prover Sign Sen Morphism () ()] Source #

default_prover :: CSMOF -> String Source #

cons_checkers :: CSMOF -> [ConsChecker Sign Sen () Morphism ()] Source #

conservativityCheck :: CSMOF -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: CSMOF -> () Source #

syntaxTable :: CSMOF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSMOF -> Maybe OMCD Source #

export_symToOmdoc :: CSMOF -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: CSMOF -> NameMap () -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSMOF -> SigMap () -> Sign -> [Named Sen] -> Result [TCElement] Source #

omdocToSym :: CSMOF -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: CSMOF -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

addOMadtToTheory :: CSMOF -> SigMapI () -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source #

addOmdocToTheory :: CSMOF -> SigMapI () -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source #

Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source #

stability :: Isabelle -> Stability Source #

data_logic :: Isabelle -> Maybe AnyLogic Source #

top_sublogic :: Isabelle -> () Source #

all_sublogics :: Isabelle -> [()] Source #

bottomSublogic :: Isabelle -> Maybe () Source #

sublogicDimensions :: Isabelle -> [[()]] Source #

parseSublogic :: Isabelle -> String -> Maybe () Source #

proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source #

provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source #

default_prover :: Isabelle -> String Source #

cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source #

conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source #

empty_proof_tree :: Isabelle -> () Source #

syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Isabelle -> Maybe OMCD Source #

export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Logic QVTR () Transformation Sen () () Sign Morphism () () () Source # 
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 

Methods

parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source #

stability :: THF -> Stability Source #

data_logic :: THF -> Maybe AnyLogic Source #

top_sublogic :: THF -> THFSl Source #

all_sublogics :: THF -> [THFSl] Source #

bottomSublogic :: THF -> Maybe THFSl Source #

sublogicDimensions :: THF -> [[THFSl]] Source #

parseSublogic :: THF -> String -> Maybe THFSl Source #

proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source #

provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source #

default_prover :: THF -> String Source #

cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source #

conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source #

empty_proof_tree :: THF -> ProofTree Source #

syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source #

omdoc_metatheory :: THF -> Maybe OMCD Source #

export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source #

export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source #

export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source #

omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source #

omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source #

addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source #

addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source #

Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source # 

Methods

parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source #

stability :: Adl -> Stability Source #

data_logic :: Adl -> Maybe AnyLogic Source #

top_sublogic :: Adl -> () Source #

all_sublogics :: Adl -> [()] Source #

bottomSublogic :: Adl -> Maybe () Source #

sublogicDimensions :: Adl -> [[()]] Source #

parseSublogic :: Adl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Adl -> () -> Sign -> Morphism Source #

provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source #

default_prover :: Adl -> String Source #

cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source #

conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: Adl -> ProofTree Source #

syntaxTable :: Adl -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Adl -> Maybe OMCD Source #

export_symToOmdoc :: Adl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source #

omdocToSym :: Adl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

addOMadtToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source #

addOmdocToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source #

Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source # 

Methods

parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source #

stability :: FrameworkCom -> Stability Source #

data_logic :: FrameworkCom -> Maybe AnyLogic Source #

top_sublogic :: FrameworkCom -> () Source #

all_sublogics :: FrameworkCom -> [()] Source #

bottomSublogic :: FrameworkCom -> Maybe () Source #

sublogicDimensions :: FrameworkCom -> [[()]] Source #

parseSublogic :: FrameworkCom -> String -> Maybe () Source #

proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source #

provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source #

default_prover :: FrameworkCom -> String Source #

cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source #

conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source #

empty_proof_tree :: FrameworkCom -> () Source #

syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source #

export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source #

addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source #

Logic Framework () LogicDef () () () LogicDef Morphism () () () Source # 

Methods

parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source #

stability :: Framework -> Stability Source #

data_logic :: Framework -> Maybe AnyLogic Source #

top_sublogic :: Framework -> () Source #

all_sublogics :: Framework -> [()] Source #

bottomSublogic :: Framework -> Maybe () Source #

sublogicDimensions :: Framework -> [[()]] Source #

parseSublogic :: Framework -> String -> Maybe () Source #

proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source #

provers :: Framework -> [Prover LogicDef () Morphism () ()] Source #

default_prover :: Framework -> String Source #

cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source #

conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source #

empty_proof_tree :: Framework -> () Source #

syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: Framework -> Maybe OMCD Source #

export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Framework -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source #

addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source #

Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Source #

Instance of Logic for propositional logc

Methods

parse_basic_sen :: HolLight -> Maybe (() -> AParser st Sentence) Source #

stability :: HolLight -> Stability Source #

data_logic :: HolLight -> Maybe AnyLogic Source #

top_sublogic :: HolLight -> HolLightSL Source #

all_sublogics :: HolLight -> [HolLightSL] Source #

bottomSublogic :: HolLight -> Maybe HolLightSL Source #

sublogicDimensions :: HolLight -> [[HolLightSL]] Source #

parseSublogic :: HolLight -> String -> Maybe HolLightSL Source #

proj_sublogic_epsilon :: HolLight -> HolLightSL -> Sign -> HolLightMorphism Source #

provers :: HolLight -> [Prover Sign Sentence HolLightMorphism HolLightSL ()] Source #

default_prover :: HolLight -> String Source #

cons_checkers :: HolLight -> [ConsChecker Sign Sentence HolLightSL HolLightMorphism ()] Source #

conservativityCheck :: HolLight -> [ConservativityChecker Sign Sentence HolLightMorphism] Source #

empty_proof_tree :: HolLight -> () Source #

syntaxTable :: HolLight -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: HolLight -> Maybe OMCD Source #

export_symToOmdoc :: HolLight -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: HolLight -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HolLight -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HolLight -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: HolLight -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: HolLight -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Logic DMU () Text () () () Text (DefaultMorphism Text) () () () Source # 

Methods

parse_basic_sen :: DMU -> Maybe (Text -> AParser st ()) Source #

stability :: DMU -> Stability Source #

data_logic :: DMU -> Maybe AnyLogic Source #

top_sublogic :: DMU -> () Source #

all_sublogics :: DMU -> [()] Source #

bottomSublogic :: DMU -> Maybe () Source #

sublogicDimensions :: DMU -> [[()]] Source #

parseSublogic :: DMU -> String -> Maybe () Source #

proj_sublogic_epsilon :: DMU -> () -> Text -> DefaultMorphism Text Source #

provers :: DMU -> [Prover Text () (DefaultMorphism Text) () ()] Source #

default_prover :: DMU -> String Source #

cons_checkers :: DMU -> [ConsChecker Text () () (DefaultMorphism Text) ()] Source #

conservativityCheck :: DMU -> [ConservativityChecker Text () (DefaultMorphism Text)] Source #

empty_proof_tree :: DMU -> () Source #

syntaxTable :: DMU -> Text -> Maybe SyntaxTable Source #

omdoc_metatheory :: DMU -> Maybe OMCD Source #

export_symToOmdoc :: DMU -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: DMU -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: DMU -> SigMap () -> Text -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: DMU -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: DMU -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [[OmdADT]] -> Result (Text, [Named ()]) Source #

addOmdocToTheory :: DMU -> SigMapI () -> (Text, [Named ()]) -> [TCElement] -> Result (Text, [Named ()]) Source #

Logic FreeCAD () Document () () () Sign (DefaultMorphism Sign) () () () Source # 

Methods

parse_basic_sen :: FreeCAD -> Maybe (Document -> AParser st ()) Source #

stability :: FreeCAD -> Stability Source #

data_logic :: FreeCAD -> Maybe AnyLogic Source #

top_sublogic :: FreeCAD -> () Source #

all_sublogics :: FreeCAD -> [()] Source #

bottomSublogic :: FreeCAD -> Maybe () Source #

sublogicDimensions :: FreeCAD -> [[()]] Source #

parseSublogic :: FreeCAD -> String -> Maybe () Source #

proj_sublogic_epsilon :: FreeCAD -> () -> Sign -> DefaultMorphism Sign Source #

provers :: FreeCAD -> [Prover Sign () (DefaultMorphism Sign) () ()] Source #

default_prover :: FreeCAD -> String Source #

cons_checkers :: FreeCAD -> [ConsChecker Sign () () (DefaultMorphism Sign) ()] Source #

conservativityCheck :: FreeCAD -> [ConservativityChecker Sign () (DefaultMorphism Sign)] Source #

empty_proof_tree :: FreeCAD -> () Source #

syntaxTable :: FreeCAD -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: FreeCAD -> Maybe OMCD Source #

export_symToOmdoc :: FreeCAD -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FreeCAD -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FreeCAD -> SigMap () -> Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FreeCAD -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FreeCAD -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [[OmdADT]] -> Result (Sign, [Named ()]) Source #

addOmdocToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [TCElement] -> Result (Sign, [Named ()]) Source #

StaticAnalysis DMU Text () () () Text (DefaultMorphism Text) () () Source # 

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 #

Sentences DMU () Text (DefaultMorphism Text) () Source # 

Methods

map_sen :: DMU -> DefaultMorphism Text -> () -> Result () Source #

simplify_sen :: DMU -> Text -> () -> () Source #

negation :: DMU -> () -> Maybe () Source #

print_sign :: DMU -> Text -> Doc Source #

print_named :: DMU -> Named () -> Doc Source #

sym_of :: DMU -> Text -> [Set ()] Source #

mostSymsOf :: DMU -> Text -> [()] Source #

symmap_of :: DMU -> DefaultMorphism Text -> EndoMap () Source #

sym_name :: DMU -> () -> Id Source #

sym_label :: DMU -> () -> Maybe String Source #

fullSymName :: DMU -> () -> String Source #

symKind :: DMU -> () -> String Source #

symsOfSen :: DMU -> Text -> () -> [()] Source #

pair_symbols :: DMU -> () -> () -> Result () Source #

Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

Methods

parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source #

stability :: SoftFOL -> Stability Source #

data_logic :: SoftFOL -> Maybe AnyLogic Source #

top_sublogic :: SoftFOL -> () Source #

all_sublogics :: SoftFOL -> [()] Source #

bottomSublogic :: SoftFOL -> Maybe () Source #

sublogicDimensions :: SoftFOL -> [[()]] Source #

parseSublogic :: SoftFOL -> String -> Maybe () Source #

proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source #

provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source #

default_prover :: SoftFOL -> String Source #

cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source #

conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source #

empty_proof_tree :: SoftFOL -> ProofTree Source #

syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: SoftFOL -> Maybe OMCD Source #

export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source #

omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Ord sign => Category sign (DefaultMorphism sign) Source # 
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

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 #

Eq sign => Eq (DefaultMorphism sign) Source # 

Methods

(==) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

(/=) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

Data sign => Data (DefaultMorphism sign) Source # 

Methods

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

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

toConstr :: DefaultMorphism sign -> Constr

dataTypeOf :: DefaultMorphism sign -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign))

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

gmapT :: (forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign

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

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

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

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

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

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

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

Ord sign => Ord (DefaultMorphism sign) Source # 

Methods

compare :: DefaultMorphism sign -> DefaultMorphism sign -> Ordering

(<) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

(<=) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

(>) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

(>=) :: DefaultMorphism sign -> DefaultMorphism sign -> Bool

max :: DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign

min :: DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign

Show sign => Show (DefaultMorphism sign) Source # 

Methods

showsPrec :: Int -> DefaultMorphism sign -> ShowS

show :: DefaultMorphism sign -> String

showList :: [DefaultMorphism sign] -> ShowS

Pretty a => Pretty (DefaultMorphism a) Source # 

defaultInclusion :: Monad m => sign -> sign -> m (DefaultMorphism sign) Source #