Copyright	(c) Jonathan von Schroeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	jonathan.von_schroeder@dfki.de
Stability	experimental
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

HolLight.Logic_HolLight

Contents

Orphan instances

Description

Instance of class Logic for HolLight logic Also the instances for Syntax and Category.

Ref.

http://www.cl.cam.ac.uk/~jrh13/hol-light/

Synopsis

type HolLightMorphism = DefaultMorphism Sign
data HolLight = HolLight

Documentation

type HolLightMorphism = DefaultMorphism Sign Source #

data HolLight Source #

Lid for HolLight logic

Constructors

HolLight

Instances

Instances details

Show HolLight Source #
Instance details Defined in HolLight.Logic_HolLight Methods showsPrec :: Int -> HolLight -> ShowS show :: HolLight -> String showList :: [HolLight] -> ShowS
Language HolLight Source #
Instance details Defined in HolLight.Logic_HolLight Methods language_name :: HolLight -> String Source # description :: HolLight -> String Source #
Sentences HolLight Sentence Sign HolLightMorphism () Source #
Instance details Defined in HolLight.Logic_HolLight 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 #
Syntax HolLight () () () () Source #
Instance details Defined in HolLight.Logic_HolLight Methods parsersAndPrinters :: HolLight -> Map String (PrefixMap -> AParser st (), () -> Doc) Source # parse_basic_spec :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source # parseSingleSymbItem :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: HolLight -> () -> Item Source # symb_items_name :: HolLight -> () -> [String] Source #
StaticAnalysis HolLight () Sentence () () Sign HolLightMorphism () () Source #	Static Analysis for propositional logic
Instance details Defined in HolLight.Logic_HolLight Methods basic_analysis :: HolLight -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: HolLight -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HolLight -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: HolLight -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: HolLight -> Sign -> [()] -> Result [()] Source # convertTheory :: HolLight -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: HolLight -> ([CASLAmalgOpt], Gr Sign (Int, HolLightMorphism), [(Int, HolLightMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HolLight -> HolLightMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: HolLight -> Gr Sign (Int, HolLightMorphism) -> Result (Sign, Map Int HolLightMorphism) Source # qualify :: HolLight -> SIMPLE_ID -> LibName -> HolLightMorphism -> Sign -> Result (HolLightMorphism, [Named Sentence]) Source # symbol_to_raw :: HolLight -> () -> () Source # id_to_raw :: HolLight -> Id -> () Source # matches :: HolLight -> () -> () -> Bool Source # empty_signature :: HolLight -> Sign Source # add_symb_to_sign :: HolLight -> Sign -> () -> Result Sign Source # signature_union :: HolLight -> Sign -> Sign -> Result Sign Source # signatureDiff :: HolLight -> Sign -> Sign -> Result Sign Source # intersection :: HolLight -> Sign -> Sign -> Result Sign Source # final_union :: HolLight -> Sign -> Sign -> Result Sign Source # morphism_union :: HolLight -> HolLightMorphism -> HolLightMorphism -> Result HolLightMorphism Source # is_subsig :: HolLight -> Sign -> Sign -> Bool Source # subsig_inclusion :: HolLight -> Sign -> Sign -> Result HolLightMorphism Source # generated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source # cogenerated_sign :: HolLight -> Set () -> Sign -> Result HolLightMorphism Source # induced_from_morphism :: HolLight -> EndoMap () -> Sign -> Result HolLightMorphism Source # induced_from_to_morphism :: HolLight -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result HolLightMorphism Source # is_transportable :: HolLight -> HolLightMorphism -> Bool Source # is_injective :: HolLight -> HolLightMorphism -> Bool Source # theory_to_taxonomy :: HolLight -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HolLight -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: HolLight -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: HolLight -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Source #	Instance of Logic for propositional logc
Instance details Defined in HolLight.Logic_HolLight 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 #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle 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 #

Orphan instances

GetRange Sentence Source #
Instance details Methods getRange :: Sentence -> Range Source # rangeSpan :: Sentence -> [Pos] Source #
SublogicName HolLightSL Source #
Instance details Methods sublogicName :: HolLightSL -> String Source #
SemiLatticeWithTop HolLightSL Source #	Sublogics
Instance details Methods lub :: HolLightSL -> HolLightSL -> HolLightSL Source # top :: HolLightSL Source #
ProjectSublogicM HolLightSL () Source #
Instance details Methods projectSublogicM :: HolLightSL -> () -> Maybe () Source #
ProjectSublogic HolLightSL () Source #
Instance details Methods projectSublogic :: HolLightSL -> () -> () Source #
ProjectSublogic HolLightSL Sign Source #
Instance details Methods projectSublogic :: HolLightSL -> Sign -> Sign Source #
ProjectSublogic HolLightSL HolLightMorphism Source #
Instance details Methods projectSublogic :: HolLightSL -> HolLightMorphism -> HolLightMorphism Source #
MinSublogic HolLightSL () Source #
Instance details Methods minSublogic :: () -> HolLightSL Source #
MinSublogic HolLightSL Sign Source #
Instance details Methods minSublogic :: Sign -> HolLightSL Source #
MinSublogic HolLightSL Sentence Source #
Instance details Methods minSublogic :: Sentence -> HolLightSL Source #
MinSublogic HolLightSL HolLightMorphism Source #
Instance details Methods minSublogic :: HolLightMorphism -> HolLightSL Source #