Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder DFKI Bremen 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerJonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stabilityexperimental
Portabilitynon-portable (via Logic.Logic)
Safe HaskellNone

THF.Sublogic

Description

Sublogics for THF

Documentation

data THFCoreSl Source #

Constructors

THF 
THFP 
THF0 

Instances

Eq THFCoreSl Source # 

Methods

(==) :: THFCoreSl -> THFCoreSl -> Bool

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

Data THFCoreSl Source # 

Methods

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

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

toConstr :: THFCoreSl -> Constr

dataTypeOf :: THFCoreSl -> DataType

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

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

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

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

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

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

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

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

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

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

Ord THFCoreSl Source # 

Methods

compare :: THFCoreSl -> THFCoreSl -> Ordering

(<) :: THFCoreSl -> THFCoreSl -> Bool

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

(>) :: THFCoreSl -> THFCoreSl -> Bool

(>=) :: THFCoreSl -> THFCoreSl -> Bool

max :: THFCoreSl -> THFCoreSl -> THFCoreSl

min :: THFCoreSl -> THFCoreSl -> THFCoreSl

Show THFCoreSl Source # 

Methods

showsPrec :: Int -> THFCoreSl -> ShowS

show :: THFCoreSl -> String

showList :: [THFCoreSl] -> ShowS

data THFSl Source #

Constructors

THFSl 

Fields

Instances

Eq THFSl Source # 

Methods

(==) :: THFSl -> THFSl -> Bool

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

Data THFSl Source # 

Methods

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

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

toConstr :: THFSl -> Constr

dataTypeOf :: THFSl -> DataType

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

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

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

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

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

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

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

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

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

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

Ord THFSl Source # 

Methods

compare :: THFSl -> THFSl -> Ordering

(<) :: THFSl -> THFSl -> Bool

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

(>) :: THFSl -> THFSl -> Bool

(>=) :: THFSl -> THFSl -> Bool

max :: THFSl -> THFSl -> THFSl

min :: THFSl -> THFSl -> THFSl

Show THFSl Source # 

Methods

showsPrec :: Int -> THFSl -> ShowS

show :: THFSl -> String

showList :: [THFSl] -> ShowS

MinSublogic THFSl DefinedType Source # 
MinSublogic THFSl THFUnaryConnective Source # 
MinSublogic THFSl THFPairConnective Source # 
MinSublogic THFSl Quantifier Source # 
MinSublogic THFSl THFQuantifier Source # 
MinSublogic THFSl THFSequent Source # 
MinSublogic THFSl THFAtom Source # 
MinSublogic THFSl THFBinaryType Source # 
MinSublogic THFSl THFUnitaryType Source # 
MinSublogic THFSl THFTopLevelType Source # 
MinSublogic THFSl THFSubType Source # 
MinSublogic THFSl THFTypeableFormula Source # 
MinSublogic THFSl THFTypeFormula Source # 
MinSublogic THFSl THFTypedConst Source # 
MinSublogic THFSl THFVariable Source # 
MinSublogic THFSl THFQuantifiedFormula Source # 
MinSublogic THFSl THFUnitaryFormula Source # 
MinSublogic THFSl THFBinaryTuple Source # 
MinSublogic THFSl THFBinaryFormula Source # 
MinSublogic THFSl THFLogicFormula Source # 
MinSublogic THFSl THFFormula Source # 
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 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 #

Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #