Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerjonathan.von_schroeder@dfki.de
Stabilityexperimental
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

HolLight.Logic_HolLight

Contents

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

Documentation

data HolLight Source #

Lid for HolLight logic

Constructors

HolLight 

Instances

Show HolLight Source # 

Methods

showsPrec :: Int -> HolLight -> ShowS

show :: HolLight -> String

showList :: [HolLight] -> ShowS

Language HolLight Source # 

Methods

language_name :: HolLight -> String Source #

description :: HolLight -> String Source #

Sentences HolLight Sentence Sign HolLightMorphism () Source # 
Syntax HolLight () () () () Source # 

Methods

parsersAndPrinters :: HolLight -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: HolLight -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: HolLight -> Maybe (AParser st ()) Source #

parse_symb_items :: HolLight -> Maybe (AParser st ()) Source #

parse_symb_map_items :: HolLight -> Maybe (AParser st ()) Source #

toItem :: HolLight -> () -> Item Source #

symb_items_name :: HolLight -> () -> [String] 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 #

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 #

Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Orphan instances