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
Portabilityportable
Safe HaskellSafe

HolLight.Sentence

Description

Definition of sentences for HolLight logic

Ref.

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

Documentation

data Sentence Source #

Constructors

Sentence 

Fields

Instances

Instances details
Eq Sentence Source # 
Instance details

Defined in HolLight.Sentence

Methods

(==) :: Sentence -> Sentence -> Bool

(/=) :: Sentence -> Sentence -> Bool

Data Sentence Source # 
Instance details

Defined in HolLight.Sentence

Methods

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

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

toConstr :: Sentence -> Constr

dataTypeOf :: Sentence -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sentence)

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

gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence

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

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

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

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

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

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

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

Ord Sentence Source # 
Instance details

Defined in HolLight.Sentence

Methods

compare :: Sentence -> Sentence -> Ordering

(<) :: Sentence -> Sentence -> Bool

(<=) :: Sentence -> Sentence -> Bool

(>) :: Sentence -> Sentence -> Bool

(>=) :: Sentence -> Sentence -> Bool

max :: Sentence -> Sentence -> Sentence

min :: Sentence -> Sentence -> Sentence

Show Sentence Source # 
Instance details

Defined in HolLight.Sentence

Methods

showsPrec :: Int -> Sentence -> ShowS

show :: Sentence -> String

showList :: [Sentence] -> ShowS

Generic Sentence 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep Sentence :: Type -> Type

Methods

from :: Sentence -> Rep Sentence x

to :: Rep Sentence x -> Sentence

GetRange Sentence Source # 
Instance details

Defined in HolLight.Logic_HolLight

FromJSON Sentence 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser Sentence

parseJSONList :: Value -> Parser [Sentence]

ToJSON Sentence 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: Sentence -> Value

toEncoding :: Sentence -> Encoding

toJSONList :: [Sentence] -> Value

toEncodingList :: [Sentence] -> Encoding

ShATermConvertible Sentence 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])

Pretty Sentence Source # 
Instance details

Defined in HolLight.Sentence

MinSublogic HolLightSL Sentence Source # 
Instance details

Defined in HolLight.Logic_HolLight

Sentences HolLight Sentence Sign HolLightMorphism () Source # 
Instance details

Defined in HolLight.Logic_HolLight

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

type Rep Sentence 
Instance details

Defined in HolLight.ATC_HolLight

type Rep Sentence = D1 ('MetaData "Sentence" "HolLight.Sentence" "main" 'False) (C1 ('MetaCons "Sentence" 'PrefixI 'True) (S1 ('MetaSel ('Just "term") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "proof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe HolProof))))

precParens :: Int -> Doc -> Doc Source #

printTerm :: Int -> Term -> Doc Source #

printTermSequence :: String -> Int -> [Term] -> Doc Source #

printBinder :: Int -> Term -> Doc Source #