Documentation

Methods

projectSublogic :: HolLightSL -> HolLightMorphism -> HolLightMorphism Source #

Methods

projectSublogic :: THFSl -> MorphismTHF -> MorphismTHF Source #

Methods

projectSublogic :: Sublogic -> Morphism -> Morphism Source #

Methods

minSublogic :: HolLightMorphism -> HolLightSL Source #

Methods

minSublogic :: MorphismTHF -> THFSl Source #

Methods

minSublogic :: Morphism -> Sublogic 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 #

Methods

map_sen :: THF -> MorphismTHF -> THFFormula -> Result THFFormula Source #

simplify_sen :: THF -> SignTHF -> THFFormula -> THFFormula Source #

negation :: THF -> THFFormula -> Maybe THFFormula Source #

print_sign :: THF -> SignTHF -> Doc Source #

print_named :: THF -> Named THFFormula -> Doc Source #

sym_of :: THF -> SignTHF -> [Set SymbolTHF] Source #

mostSymsOf :: THF -> SignTHF -> [SymbolTHF] Source #

symmap_of :: THF -> MorphismTHF -> EndoMap SymbolTHF Source #

sym_name :: THF -> SymbolTHF -> Id Source #

sym_label :: THF -> SymbolTHF -> Maybe String Source #

fullSymName :: THF -> SymbolTHF -> String Source #

symKind :: THF -> SymbolTHF -> String Source #

symsOfSen :: THF -> SignTHF -> THFFormula -> [SymbolTHF] Source #

pair_symbols :: THF -> SymbolTHF -> SymbolTHF -> Result SymbolTHF Source #

Methods

map_sen :: TPTP -> Morphism -> Sentence -> Result Sentence Source #

simplify_sen :: TPTP -> Sign -> Sentence -> Sentence Source #

negation :: TPTP -> Sentence -> Maybe Sentence Source #

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

print_named :: TPTP -> Named Sentence -> Doc Source #

sym_of :: TPTP -> Sign -> [Set Symbol] Source #

mostSymsOf :: TPTP -> Sign -> [Symbol] Source #

symmap_of :: TPTP -> Morphism -> EndoMap Symbol Source #

sym_name :: TPTP -> Symbol -> Id Source #

sym_label :: TPTP -> Symbol -> Maybe String Source #

fullSymName :: TPTP -> Symbol -> String Source #

symKind :: TPTP -> Symbol -> String Source #

symsOfSen :: TPTP -> Sign -> Sentence -> [Symbol] Source #

pair_symbols :: TPTP -> Symbol -> Symbol -> Result Symbol Source #

Methods

map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence Source #

simplify_sen :: SoftFOL -> Sign -> Sentence -> Sentence Source #

negation :: SoftFOL -> Sentence -> Maybe Sentence Source #

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

print_named :: SoftFOL -> Named Sentence -> Doc Source #

sym_of :: SoftFOL -> Sign -> [Set SFSymbol] Source #

mostSymsOf :: SoftFOL -> Sign -> [SFSymbol] Source #

symmap_of :: SoftFOL -> SoftFOLMorphism -> EndoMap SFSymbol Source #

sym_name :: SoftFOL -> SFSymbol -> Id Source #

sym_label :: SoftFOL -> SFSymbol -> Maybe String Source #

fullSymName :: SoftFOL -> SFSymbol -> String Source #

symKind :: SoftFOL -> SFSymbol -> String Source #

symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol] Source #

pair_symbols :: SoftFOL -> SFSymbol -> SFSymbol -> Result SFSymbol Source #

Methods

map_sen :: Isabelle -> IsabelleMorphism -> Sentence -> Result Sentence Source #

simplify_sen :: Isabelle -> Sign -> Sentence -> Sentence Source #

negation :: Isabelle -> Sentence -> Maybe Sentence Source #

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

print_named :: Isabelle -> Named Sentence -> Doc Source #

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

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

symmap_of :: Isabelle -> IsabelleMorphism -> EndoMap () Source #

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

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

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

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

symsOfSen :: Isabelle -> Sign -> Sentence -> [()] Source #

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

Methods

map_sen :: HolLight -> HolLightMorphism -> Sentence -> Result Sentence Source #

simplify_sen :: HolLight -> Sign -> Sentence -> Sentence Source #

negation :: HolLight -> Sentence -> Maybe Sentence Source #

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

print_named :: HolLight -> Named Sentence -> Doc Source #

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

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

symmap_of :: HolLight -> HolLightMorphism -> EndoMap () Source #

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

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

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

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

symsOfSen :: HolLight -> Sign -> Sentence -> [()] Source #

pair_symbols :: HolLight -> () -> () -> Result () 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 #

Methods

map_sen :: FrameworkCom -> MorphismCom -> () -> Result () Source #

simplify_sen :: FrameworkCom -> ComorphismDef -> () -> () Source #

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

print_sign :: FrameworkCom -> ComorphismDef -> Doc Source #

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

sym_of :: FrameworkCom -> ComorphismDef -> [Set ()] Source #

mostSymsOf :: FrameworkCom -> ComorphismDef -> [()] Source #

symmap_of :: FrameworkCom -> MorphismCom -> EndoMap () Source #

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

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

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

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

symsOfSen :: FrameworkCom -> ComorphismDef -> () -> [()] Source #

pair_symbols :: FrameworkCom -> () -> () -> Result () 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 #

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 #

Methods

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

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

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

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

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

sym_of :: Adl -> Sign -> [Set Symbol] Source #

mostSymsOf :: Adl -> Sign -> [Symbol] Source #

symmap_of :: Adl -> Morphism -> EndoMap Symbol Source #

sym_name :: Adl -> Symbol -> Id Source #

sym_label :: Adl -> Symbol -> Maybe String Source #

fullSymName :: Adl -> Symbol -> String Source #

symKind :: Adl -> Symbol -> String Source #

symsOfSen :: Adl -> Sign -> Sen -> [Symbol] Source #

pair_symbols :: Adl -> Symbol -> Symbol -> Result Symbol 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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

Methods

parse_basic_sen :: QVTR -> Maybe (Transformation -> AParser st Sen) Source #

stability :: QVTR -> Stability Source #

data_logic :: QVTR -> Maybe AnyLogic Source #

top_sublogic :: QVTR -> () Source #

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

bottomSublogic :: QVTR -> Maybe () Source #

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

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

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

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

default_prover :: QVTR -> String Source #

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

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

empty_proof_tree :: QVTR -> () Source #

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

omdoc_metatheory :: QVTR -> Maybe OMCD Source #

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

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

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

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

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

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

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

sublogicOfTheo :: QVTR -> (Sign, [Sen]) -> () 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 #

sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl 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 #

sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic 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 #

sublogicOfTheo :: Isabelle -> (Sign, [Sentence]) -> () Source #

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 #

sublogicOfTheo :: HolLight -> (Sign, [Sentence]) -> HolLightSL 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 #

sublogicOfTheo :: FrameworkCom -> (ComorphismDef, [()]) -> () 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 #

sublogicOfTheo :: Framework -> (LogicDef, [()]) -> () 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 #

sublogicOfTheo :: CSMOF -> (Sign, [Sen]) -> () 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 #

sublogicOfTheo :: Adl -> (Sign, [Sen]) -> () Source #

Methods

sourceLogic :: THFP_P2THFP -> THF Source #

sourceSublogic :: THFP_P2THFP -> THFSl Source #

sourceSublogicLossy :: THFP_P2THFP -> THFSl Source #

minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source #

targetLogic :: THFP_P2THFP -> THF Source #

mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source #

map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source #

map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source #

map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source #

extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP_P2THFP -> Bool Source #

has_model_expansion :: THFP_P2THFP -> Bool Source #

is_weakly_amalgamable :: THFP_P2THFP -> Bool Source #

constituents :: THFP_P2THFP -> [String] Source #

isInclusionComorphism :: THFP_P2THFP -> Bool Source #

rps :: THFP_P2THFP -> Bool Source #

eps :: THFP_P2THFP -> Bool Source #

isGTC :: THFP_P2THFP -> Bool Source #

Methods

sourceLogic :: THFP_P2HasCASL -> THF Source #

sourceSublogic :: THFP_P2HasCASL -> THFSl Source #

sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source #

minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source #

targetLogic :: THFP_P2HasCASL -> HasCASL Source #

mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source #

map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source #

mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source #

map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source #

map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source #

map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source #

extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP_P2HasCASL -> Bool Source #

has_model_expansion :: THFP_P2HasCASL -> Bool Source #

is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source #

constituents :: THFP_P2HasCASL -> [String] Source #

isInclusionComorphism :: THFP_P2HasCASL -> Bool Source #

rps :: THFP_P2HasCASL -> Bool Source #

eps :: THFP_P2HasCASL -> Bool Source #

isGTC :: THFP_P2HasCASL -> Bool Source #

Methods

sourceLogic :: THFP2THF0 -> THF Source #

sourceSublogic :: THFP2THF0 -> THFSl Source #

sourceSublogicLossy :: THFP2THF0 -> THFSl Source #

minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source #

targetLogic :: THFP2THF0 -> THF Source #

mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source #

map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source #

map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source #

map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source #

extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP2THF0 -> Bool Source #

has_model_expansion :: THFP2THF0 -> Bool Source #

is_weakly_amalgamable :: THFP2THF0 -> Bool Source #

constituents :: THFP2THF0 -> [String] Source #

isInclusionComorphism :: THFP2THF0 -> Bool Source #

rps :: THFP2THF0 -> Bool Source #

eps :: THFP2THF0 -> Bool Source #

isGTC :: THFP2THF0 -> Bool Source #

Methods

sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source #

sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source #

sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source #

minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source #

targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source #

mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source #

map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source #

map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source #

map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source #

extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source #

is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source #

isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

Methods

sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source #

sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source #

sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source #

minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source #

targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source #

mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source #

map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source #

map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source #

map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source #

extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source #

is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source #

isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #

Methods

sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source #

sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source #

sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source #

minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source #

targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source #

mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source #

map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source #

map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source #

map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source #

extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source #

is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source #

has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source #

is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source #

constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source #

isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source #

rps :: MonadicHasCASL2IsabelleHOL -> Bool Source #

eps :: MonadicHasCASL2IsabelleHOL -> Bool Source #

isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #

Methods

sourceLogic :: HolLight2Isabelle -> HolLight Source #

sourceSublogic :: HolLight2Isabelle -> HolLightSL Source #

sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source #

minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source #

targetLogic :: HolLight2Isabelle -> Isabelle Source #

mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source #

map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source #

map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source #

map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source #

extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source #

is_model_transportable :: HolLight2Isabelle -> Bool Source #

has_model_expansion :: HolLight2Isabelle -> Bool Source #

is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source #

constituents :: HolLight2Isabelle -> [String] Source #

isInclusionComorphism :: HolLight2Isabelle -> Bool Source #

rps :: HolLight2Isabelle -> Bool Source #

eps :: HolLight2Isabelle -> Bool Source #

isGTC :: HolLight2Isabelle -> Bool Source #

Methods

sourceLogic :: HasCASL2THFP_P -> HasCASL Source #

sourceSublogic :: HasCASL2THFP_P -> Sublogic Source #

sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source #

minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source #

targetLogic :: HasCASL2THFP_P -> THF Source #

mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source #

map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source #

map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source #