Copyright | (c) A. Tsogias DFKI Bremen 2011 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Alexis.Tsogias@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
THF.As
Description
A Abstract Syntax for the TPTP-THF Input Syntax v5.1.0.2 taken from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html In addition the Syntax for THF0 taken from http://www.ags.uni-sb.de/~chris/papers/C25.pdf P. 15-16 has been added where needed.
Documentation
Constructors
Comment_Line Token | |
Comment_Block Token |
data DefinedComment Source #
Constructors
Defined_Comment_Line Token | |
Defined_Comment_Block Token |
Instances
Eq DefinedComment Source # | |
Data DefinedComment Source # | |
Ord DefinedComment Source # | |
Show DefinedComment Source # | |
GetRange DefinedComment Source # | |
data SystemComment Source #
Constructors
System_Comment_Line Token | |
System_Comment_Block Token |
Instances
Eq SystemComment Source # | |
Data SystemComment Source # | |
Ord SystemComment Source # | |
Show SystemComment Source # | |
GetRange SystemComment Source # | |
data Annotations Source #
Constructors
Annotations Source OptionalInfo | |
Null |
Instances
Eq Annotations Source # | |
Data Annotations Source # | |
Ord Annotations Source # | |
Show Annotations Source # | |
GetRange Annotations Source # | |
data FormulaRole Source #
Constructors
Axiom | |
Hypothesis | |
Definition | |
Assumption | |
Lemma | |
Theorem | |
Conjecture | |
Negated_Conjecture | |
Plain | |
Fi_Domain | |
Fi_Functors | |
Fi_Predicates | |
Type | |
Unknown |
Instances
Eq FormulaRole Source # | |
Data FormulaRole Source # | |
Ord FormulaRole Source # | |
Show FormulaRole Source # | |
GetRange FormulaRole Source # | |
data THFFormula Source #
Constructors
TF_THF_Logic_Formula THFLogicFormula | |
TF_THF_Sequent THFSequent | |
T0F_THF_Typed_Const THFTypedConst |
Instances
data THFLogicFormula Source #
Constructors
TLF_THF_Binary_Formula THFBinaryFormula | |
TLF_THF_Unitary_Formula THFUnitaryFormula | |
TLF_THF_Type_Formula THFTypeFormula | |
TLF_THF_Sub_Type THFSubType |
Instances
data THFBinaryFormula Source #
Constructors
TBF_THF_Binary_Pair THFUnitaryFormula THFPairConnective THFUnitaryFormula | |
TBF_THF_Binary_Tuple THFBinaryTuple | |
TBF_THF_Binary_Type THFBinaryType |
Instances
data THFBinaryTuple Source #
Constructors
TBT_THF_Or_Formula [THFUnitaryFormula] | |
TBT_THF_And_Formula [THFUnitaryFormula] | |
TBT_THF_Apply_Formula [THFUnitaryFormula] |
Instances
data THFUnitaryFormula Source #
Constructors
Instances
data THFQuantifiedFormula Source #
Constructors
Instances
type THFVariableList = [THFVariable] Source #
data THFVariable Source #
Constructors
TV_THF_Typed_Variable Token THFTopLevelType | |
TV_Variable Token |
Instances
Eq THFVariable Source # | |
Data THFVariable Source # | |
Ord THFVariable Source # | |
Show THFVariable Source # | |
GetRange THFVariable Source # | |
MinSublogic THFSl THFVariable Source # | |
data THFTypedConst Source #
Instances
Eq THFTypedConst Source # | |
Data THFTypedConst Source # | |
Ord THFTypedConst Source # | |
Show THFTypedConst Source # | |
GetRange THFTypedConst Source # | |
MinSublogic THFSl THFTypedConst Source # | |
data THFTypeFormula Source #
Constructors
TTF_THF_Type_Formula THFTypeableFormula THFTopLevelType | |
TTF_THF_Typed_Const Constant THFTopLevelType |
Instances
data THFTypeableFormula Source #
Instances
data THFSubType Source #
Constructors
TST_THF_Sub_Type Constant Constant |
Instances
Eq THFSubType Source # | |
Data THFSubType Source # | |
Ord THFSubType Source # | |
Show THFSubType Source # | |
GetRange THFSubType Source # | |
MinSublogic THFSl THFSubType Source # | |
data THFTopLevelType Source #
Constructors
TTLT_THF_Logic_Formula THFLogicFormula | |
T0TLT_Constant Constant | |
T0TLT_Variable Token | |
T0TLT_Defined_Type DefinedType | |
T0TLT_System_Type Token | |
T0TLT_THF_Binary_Type THFBinaryType |
Instances
data THFUnitaryType Source #
Constructors
TUT_THF_Unitary_Formula THFUnitaryFormula | |
T0UT_Constant Constant | |
T0UT_Variable Token | |
T0UT_Defined_Type DefinedType | |
T0UT_System_Type Token | |
T0UT_THF_Binary_Type_Par THFBinaryType |
Instances
data THFBinaryType Source #
Constructors
TBT_THF_Mapping_Type [THFUnitaryType] | |
TBT_THF_Xprod_Type [THFUnitaryType] | |
TBT_THF_Union_Type [THFUnitaryType] | |
T0BT_THF_Binary_Type_Par THFBinaryType |
Instances
Eq THFBinaryType Source # | |
Data THFBinaryType Source # | |
Ord THFBinaryType Source # | |
Show THFBinaryType Source # | |
GetRange THFBinaryType Source # | |
MinSublogic THFSl THFBinaryType Source # | |
type THFTuple = [THFLogicFormula] Source #
data THFSequent Source #
Constructors
TS_THF_Sequent THFTuple THFTuple | |
TS_THF_Sequent_Par THFSequent |
Instances
Eq THFSequent Source # | |
Data THFSequent Source # | |
Ord THFSequent Source # | |
Show THFSequent Source # | |
GetRange THFSequent Source # | |
MinSublogic THFSl THFSequent Source # | |
data THFConnTerm Source #
Constructors
TCT_THF_Pair_Connective THFPairConnective | |
TCT_Assoc_Connective AssocConnective | |
TCT_THF_Unary_Connective THFUnaryConnective | |
T0CT_THF_Quantifier THFQuantifier |
Instances
Eq THFConnTerm Source # | |
Data THFConnTerm Source # | |
Ord THFConnTerm Source # | |
Show THFConnTerm Source # | |
GetRange THFConnTerm Source # | |
data THFQuantifier Source #
Constructors
TQ_ForAll | |
TQ_Exists | |
TQ_Lambda_Binder | |
TQ_Dependent_Product | |
TQ_Dependent_Sum | |
TQ_Indefinite_Description | |
TQ_Definite_Description | |
T0Q_PiForAll | |
T0Q_SigmaExists |
Instances
Eq THFQuantifier Source # | |
Data THFQuantifier Source # | |
Ord THFQuantifier Source # | |
Show THFQuantifier Source # | |
GetRange THFQuantifier Source # | |
MinSublogic THFSl THFQuantifier Source # | |
data Quantifier Source #
Constructors
T0Q_ForAll | |
T0Q_Exists |
Instances
Eq Quantifier Source # | |
Data Quantifier Source # | |
Ord Quantifier Source # | |
Show Quantifier Source # | |
GetRange Quantifier Source # | |
MinSublogic THFSl Quantifier Source # | |
data THFPairConnective Source #
Constructors
Infix_Equality | |
Infix_Inequality | |
Equivalent | |
Implication | |
IF | |
XOR | |
NOR | |
NAND |
Instances
data AssocConnective Source #
Instances
Eq AssocConnective Source # | |
Data AssocConnective Source # | |
Ord AssocConnective Source # | |
Show AssocConnective Source # | |
GetRange AssocConnective Source # | |
data DefinedType Source #
Instances
Eq DefinedType Source # | |
Data DefinedType Source # | |
Ord DefinedType Source # | |
Show DefinedType Source # | |
GetRange DefinedType Source # | |
MinSublogic THFSl DefinedType Source # | |
data DefinedPlainFormula Source #
Instances
data DefinedProp Source #
Instances
Eq DefinedProp Source # | |
Data DefinedProp Source # | |
Ord DefinedProp Source # | |
Show DefinedProp Source # | |
GetRange DefinedProp Source # | |
data DefinedPred Source #
Instances
Eq DefinedPred Source # | |
Data DefinedPred Source # | |
Ord DefinedPred Source # | |
Show DefinedPred Source # | |
GetRange DefinedPred Source # | |
Constructors
T_Function_Term FunctionTerm | |
T_Variable Token |
data FunctionTerm Source #
Instances
Eq FunctionTerm Source # | |
Data FunctionTerm Source # | |
Ord FunctionTerm Source # | |
Show FunctionTerm Source # | |
GetRange FunctionTerm Source # | |
Constructors
PT_Plain_Term AtomicWord Arguments | |
PT_Constant Constant |
type Constant = AtomicWord Source #
data DefinedTerm Source #
Instances
Eq DefinedTerm Source # | |
Data DefinedTerm Source # | |
Ord DefinedTerm Source # | |
Show DefinedTerm Source # | |
GetRange DefinedTerm Source # | |
data DefinedAtom Source #
Constructors
DA_Number Number | |
DA_Distinct_Object Token |
Instances
Eq DefinedAtom Source # | |
Data DefinedAtom Source # | |
Ord DefinedAtom Source # | |
Show DefinedAtom Source # | |
GetRange DefinedAtom Source # | |
data DefinedPlainTerm Source #
Instances
Eq DefinedPlainTerm Source # | |
Data DefinedPlainTerm Source # | |
Ord DefinedPlainTerm Source # | |
Show DefinedPlainTerm Source # | |
GetRange DefinedPlainTerm Source # | |
data DefinedFunctor Source #
Constructors
UMinus | |
Sum | |
Difference | |
Product | |
Quotient | |
Quotient_e | |
Quotient_t | |
Quotient_f | |
Remainder_e | |
Remainder_t | |
Remainder_f | |
Floor | |
Ceiling | |
Truncate | |
Round | |
To_int | |
To_rat | |
To_real |
Instances
Eq DefinedFunctor Source # | |
Data DefinedFunctor Source # | |
Ord DefinedFunctor Source # | |
Show DefinedFunctor Source # | |
GetRange DefinedFunctor Source # | |
data SystemTerm Source #
Constructors
ST_System_Term Token Arguments | |
ST_System_Constant Token |
Instances
Eq SystemTerm Source # | |
Data SystemTerm Source # | |
Ord SystemTerm Source # | |
Show SystemTerm Source # | |
GetRange SystemTerm Source # | |
data PrincipalSymbol Source #
Constructors
PS_Functor AtomicWord | |
PS_Variable Token |
Instances
Eq PrincipalSymbol Source # | |
Data PrincipalSymbol Source # | |
Ord PrincipalSymbol Source # | |
Show PrincipalSymbol Source # | |
GetRange PrincipalSymbol Source # | |
Constructors
DS_Name Name | |
DS_Inference_Record AtomicWord UsefulInfo [ParentInfo] |
data ParentInfo Source #
Constructors
PI_Parent_Info Source (Maybe GeneralList) |
Instances
Eq ParentInfo Source # | |
Data ParentInfo Source # | |
Ord ParentInfo Source # | |
Show ParentInfo Source # | |
GetRange ParentInfo Source # | |
Constructors
IT_definition | |
IT_axiom_of_choice | |
IT_tautology | |
IT_assumption |
data ExternalSource Source #
Constructors
ES_File_Source FileSource | |
ES_Theory TheoryName OptionalInfo | |
ES_Creator_Source AtomicWord OptionalInfo |
Instances
Eq ExternalSource Source # | |
Data ExternalSource Source # | |
Ord ExternalSource Source # | |
Show ExternalSource Source # | |
GetRange ExternalSource Source # | |
data FileSource Source #
Instances
Eq FileSource Source # | |
Data FileSource Source # | |
Ord FileSource Source # | |
Show FileSource Source # | |
GetRange FileSource Source # | |
data TheoryName Source #
Instances
Eq TheoryName Source # | |
Data TheoryName Source # | |
Ord TheoryName Source # | |
Show TheoryName Source # | |
GetRange TheoryName Source # | |
type OptionalInfo = Maybe UsefulInfo Source #
type UsefulInfo = [InfoItem] Source #
data FormulaItem Source #
Constructors
FI_Description_Item AtomicWord | |
FI_Iquote_Item AtomicWord |
Instances
Eq FormulaItem Source # | |
Data FormulaItem Source # | |
Ord FormulaItem Source # | |
Show FormulaItem Source # | |
GetRange FormulaItem Source # | |
data InferenceItem Source #
Constructors
II_Inference_Status InferenceStatus | |
II_Assumptions_Record NameList | |
II_New_Symbol_Record AtomicWord [PrincipalSymbol] | |
II_Refutation FileSource |
Instances
Eq InferenceItem Source # | |
Data InferenceItem Source # | |
Ord InferenceItem Source # | |
Show InferenceItem Source # | |
GetRange InferenceItem Source # | |
data InferenceStatus Source #
Constructors
IS_Status StatusValue | |
IS_Inference_Info AtomicWord AtomicWord GeneralList |
Instances
Eq InferenceStatus Source # | |
Data InferenceStatus Source # | |
Ord InferenceStatus Source # | |
Show InferenceStatus Source # | |
GetRange InferenceStatus Source # | |
data StatusValue Source #
Constructors
Suc | |
Unp | |
Sap | |
Esa | |
Sat | |
Fsa | |
Thm | |
Eqv | |
Tac | |
Wec | |
Eth | |
Tau | |
Wtc | |
Wth | |
Cax | |
Sca | |
Tca | |
Wca | |
Cup | |
Csp | |
Ecs | |
Csa | |
Cth | |
Ceq | |
Unc | |
Wcc | |
Ect | |
Fun | |
Uns | |
Wuc | |
Wct | |
Scc | |
Uca | |
Noc |
Instances
Eq StatusValue Source # | |
Data StatusValue Source # | |
Ord StatusValue Source # | |
Show StatusValue Source # | |
GetRange StatusValue Source # | |
data GeneralTerm Source #
Constructors
GT_General_Data GeneralData | |
GT_General_Data_Term GeneralData GeneralTerm | |
GT_General_List GeneralList |
Instances
Eq GeneralTerm Source # | |
Data GeneralTerm Source # | |
Ord GeneralTerm Source # | |
Show GeneralTerm Source # | |
GetRange GeneralTerm Source # | |
data GeneralData Source #
Constructors
GD_Atomic_Word AtomicWord | |
GD_Variable Token | |
GD_Number Number | |
GD_Distinct_Object Token | |
GD_Formula_Data FormulaData | |
GD_Bind Token FormulaData | |
GD_General_Function GeneralFunction |
Instances
Eq GeneralData Source # | |
Data GeneralData Source # | |
Ord GeneralData Source # | |
Show GeneralData Source # | |
GetRange GeneralData Source # | |
data GeneralFunction Source #
Constructors
GF_General_Function AtomicWord GeneralTerms |
Instances
Eq GeneralFunction Source # | |
Data GeneralFunction Source # | |
Ord GeneralFunction Source # | |
Show GeneralFunction Source # | |
GetRange GeneralFunction Source # | |
data FormulaData Source #
Constructors
THF_Formula THFFormula |
Instances
Eq FormulaData Source # | |
Data FormulaData Source # | |
Ord FormulaData Source # | |
Show FormulaData Source # | |
GetRange FormulaData Source # | |
type GeneralList = GeneralTerms Source #
type GeneralTerms = [GeneralTerm] Source #
Constructors
N_Atomic_Word AtomicWord | |
N_Integer Token | |
T0N_Unsigned_Integer Token |
data AtomicWord Source #
Constructors
A_Lower_Word Token | |
A_Single_Quoted Token |
Instances
Eq AtomicWord Source # | |
Data AtomicWord Source # | |
Ord AtomicWord Source # | |
Show AtomicWord Source # | |
GetRange AtomicWord Source # | |