Copyright	(c) Hendrik Iben Uni Bremen 2005-2007
License	GPLv2 or higher, see LICENSE.txt
Maintainer	hiben@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable
Safe Haskell	None

OMDoc.Logic_OMDoc

Contents

Orphan instances

Description

Logic and related instances for OMDoc.

Documentation

data OMDoc_PUN Source #

Constructors

OMDoc_PUN

Instances

Instances details

Show OMDoc_PUN Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods showsPrec :: Int -> OMDoc_PUN -> ShowS show :: OMDoc_PUN -> String showList :: [OMDoc_PUN] -> ShowS
Language OMDoc_PUN Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods language_name :: OMDoc_PUN -> String Source # description :: OMDoc_PUN -> String Source #
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods map_sen :: OMDoc_PUN -> OMDoc_Morphism -> () -> Result () Source # simplify_sen :: OMDoc_PUN -> OMDoc_Sign -> () -> () Source # negation :: OMDoc_PUN -> () -> Maybe () Source # print_sign :: OMDoc_PUN -> OMDoc_Sign -> Doc Source # print_named :: OMDoc_PUN -> Named () -> Doc Source # sym_of :: OMDoc_PUN -> OMDoc_Sign -> [Set Symbol] Source # mostSymsOf :: OMDoc_PUN -> OMDoc_Sign -> [Symbol] Source # symmap_of :: OMDoc_PUN -> OMDoc_Morphism -> EndoMap Symbol Source # sym_name :: OMDoc_PUN -> Symbol -> Id Source # sym_label :: OMDoc_PUN -> Symbol -> Maybe String Source # fullSymName :: OMDoc_PUN -> Symbol -> String Source # symKind :: OMDoc_PUN -> Symbol -> String Source # symsOfSen :: OMDoc_PUN -> OMDoc_Sign -> () -> [Symbol] Source # pair_symbols :: OMDoc_PUN -> Symbol -> Symbol -> Result Symbol Source #
Syntax OMDoc_PUN () Symbol () () Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods parsersAndPrinters :: OMDoc_PUN -> Map String (PrefixMap -> AParser st (), () -> Doc) Source # parse_basic_spec :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source # parseSingleSymbItem :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: OMDoc_PUN -> () -> Item Source # symb_items_name :: OMDoc_PUN -> () -> [String] Source #
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods basic_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, GlobalAnnos) -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()])) Source # sen_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, ()) -> Result ()) Source # extBasicAnalysis :: OMDoc_PUN -> IRI -> LibName -> () -> OMDoc_Sign -> GlobalAnnos -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()]) Source # stat_symb_map_items :: OMDoc_PUN -> OMDoc_Sign -> Maybe OMDoc_Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: OMDoc_PUN -> OMDoc_Sign -> [()] -> Result [()] Source # convertTheory :: OMDoc_PUN -> Maybe ((OMDoc_Sign, [Named ()]) -> ()) Source # ensures_amalgamability :: OMDoc_PUN -> ([CASLAmalgOpt], Gr OMDoc_Sign (Int, OMDoc_Morphism), [(Int, OMDoc_Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: OMDoc_PUN -> OMDoc_Morphism -> [Named ()] -> Result (OMDoc_Sign, [Named ()]) Source # signature_colimit :: OMDoc_PUN -> Gr OMDoc_Sign (Int, OMDoc_Morphism) -> Result (OMDoc_Sign, Map Int OMDoc_Morphism) Source # qualify :: OMDoc_PUN -> SIMPLE_ID -> LibName -> OMDoc_Morphism -> OMDoc_Sign -> Result (OMDoc_Morphism, [Named ()]) Source # symbol_to_raw :: OMDoc_PUN -> Symbol -> () Source # id_to_raw :: OMDoc_PUN -> Id -> () Source # matches :: OMDoc_PUN -> Symbol -> () -> Bool Source # empty_signature :: OMDoc_PUN -> OMDoc_Sign Source # add_symb_to_sign :: OMDoc_PUN -> OMDoc_Sign -> Symbol -> Result OMDoc_Sign Source # signature_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # signatureDiff :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # intersection :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # final_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source # morphism_union :: OMDoc_PUN -> OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism Source # is_subsig :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Bool Source # subsig_inclusion :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Morphism Source # generated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source # cogenerated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source # induced_from_morphism :: OMDoc_PUN -> EndoMap () -> OMDoc_Sign -> Result OMDoc_Morphism Source # induced_from_to_morphism :: OMDoc_PUN -> EndoMap () -> ExtSign OMDoc_Sign Symbol -> ExtSign OMDoc_Sign Symbol -> Result OMDoc_Morphism Source # is_transportable :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source # is_injective :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source # theory_to_taxonomy :: OMDoc_PUN -> TaxoGraphKind -> MMiSSOntology -> OMDoc_Sign -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: OMDoc_PUN -> String -> Bool -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (OMDoc_Sign, [Named ()], OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> Result (OMDoc_Sign, OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: OMDoc_PUN -> [IRI] -> (OMDoc_Sign, [Named ()]) -> Result (OMDoc_Sign, [Named ()]) Source #
Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source #
Instance details Defined in OMDoc.Logic_OMDoc Methods parse_basic_sen :: OMDoc_PUN -> Maybe (() -> AParser st ()) Source # stability :: OMDoc_PUN -> Stability Source # data_logic :: OMDoc_PUN -> Maybe AnyLogic Source # top_sublogic :: OMDoc_PUN -> () Source # all_sublogics :: OMDoc_PUN -> [()] Source # bottomSublogic :: OMDoc_PUN -> Maybe () Source # sublogicDimensions :: OMDoc_PUN -> [[()]] Source # parseSublogic :: OMDoc_PUN -> String -> Maybe () Source # proj_sublogic_epsilon :: OMDoc_PUN -> () -> OMDoc_Sign -> OMDoc_Morphism Source # provers :: OMDoc_PUN -> [Prover OMDoc_Sign () OMDoc_Morphism () ()] Source # default_prover :: OMDoc_PUN -> String Source # cons_checkers :: OMDoc_PUN -> [ConsChecker OMDoc_Sign () () OMDoc_Morphism ()] Source # conservativityCheck :: OMDoc_PUN -> [ConservativityChecker OMDoc_Sign () OMDoc_Morphism] Source # empty_proof_tree :: OMDoc_PUN -> () Source # syntaxTable :: OMDoc_PUN -> OMDoc_Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: OMDoc_PUN -> Maybe OMCD Source # export_symToOmdoc :: OMDoc_PUN -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: OMDoc_PUN -> NameMap Symbol -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: OMDoc_PUN -> SigMap Symbol -> OMDoc_Sign -> [Named ()] -> Result [TCElement] Source # omdocToSym :: OMDoc_PUN -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: OMDoc_PUN -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [[OmdADT]] -> Result (OMDoc_Sign, [Named ()]) Source # addOmdocToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [TCElement] -> Result (OMDoc_Sign, [Named ()]) Source # sublogicOfTheo :: OMDoc_PUN -> (OMDoc_Sign, [()]) -> () Source #

type OMDoc_Sign = Theory Source #

type OMDoc_Morphism = (Inclusion, Theory, Theory) Source #

is_subsig :: Theory -> Theory -> Bool Source #

Orphan instances

Category OMDoc_Sign OMDoc_Morphism Source #

Instance details

Methods

ide :: OMDoc_Sign -> OMDoc_Morphism Source #

composeMorphisms :: OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism Source #

dom :: OMDoc_Morphism -> OMDoc_Sign Source #

cod :: OMDoc_Morphism -> OMDoc_Sign Source #

inverse :: OMDoc_Morphism -> Result OMDoc_Morphism Source #

isInclusion :: OMDoc_Morphism -> Bool Source #

legal_mor :: OMDoc_Morphism -> Result () Source #