{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./TPTP/AS.der.hs
Description : Abstract syntax for TPTP v6.4.0.11
Copyright : (c) Eugen Kuksa University of Magdeburg 2017
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability : provisional
Portability : portable
Definition of abstract syntax for TPTP taken from [1]
References
[1] G. Sutcliffe et al.: The TPTP language grammar in BNF.
<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
Note: The implemented version is saved at TPTP/Documents/SyntaxBNF.html
Note: The names of the data types are aligned with the names of the
grammar rules at this reference page (modulo case).
[2] C. Kaliszyk, G. Sutcliffe and F. Rabe:
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
<https://kwarc.info/people/frabe/Research/KRS_thf1_16.pdf>
Note: for further information on TF0, TF1, TH0 and TH1
-}
module TPTP.AS where
import Common.Id as Id
import Common.IRI
import Syntax.AS_Structured ()
import qualified Common.AS_Annotation as AS_Anno
import Data.Data
-- DrIFT command
{-! global: GetRange !-}
newtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted TPTP]
deriving (Show, Ord, Eq, Data, Typeable)
-- Files
-- %----Files. Empty file is OK.
-- <TPTP_file> ::= <TPTP_input>*<Paste>
newtype TPTP = TPTP [TPTP_input]
deriving (Show, Ord, Eq, Data, Typeable)
-- <TPTP_input> ::= <annotated_formula> | <include>
data TPTP_input = Annotated_formula Annotated_formula
| TPTP_include Include
| TPTP_comment Comment
| TPTP_defined_comment DefinedComment
| TPTP_system_comment SystemComment
deriving (Show, Ord, Eq, Data, Typeable)
-- Comments
data Comment = Comment_line Token
| Comment_block Token
deriving (Show, Eq, Ord, Data, Typeable)
data DefinedComment = Defined_comment_line Token
| Defined_comment_block Token
deriving (Show, Eq, Ord, Data, Typeable)
data SystemComment = System_comment_line Token
| System_comment_block Token
deriving (Show, Eq, Ord, Data, Typeable)
-- %----Formula records
-- <annotated_formula> ::= <thf_annotated> | <tfx_annotated> | <tff_annotated> |
-- <tcf_annotated> | <fof_annotated> | <cnf_annotated> |
-- <tpi_annotated>
data Annotated_formula = AF_THF_Annotated THF_annotated
| AF_TFX_Annotated TFX_annotated
| AF_TFF_Annotated TFF_annotated
| AF_TCF_Annotated TCF_annotated
| AF_FOF_Annotated FOF_annotated
| AF_CNF_Annotated CNF_annotated
| AF_TPI_Annotated TPI_annotated
deriving (Show, Ord, Eq, Data, Typeable)
-- <tpi_annotated> ::= tpi(<name>,<formula_role>,<tpi_formula><annotations>).
data TPI_annotated = TPI_annotated Name Formula_role TPI_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <tpi_formula> ::= <fof_formula>
type TPI_formula = FOF_formula
-- <thf_annotated> ::= thf(<name>,<formula_role>,<thf_formula>
-- <annotations>).
data THF_annotated = THF_annotated Name Formula_role THF_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <tfx_annotated> ::= tfx(<name>,<formula_role>,<tfx_formula>
-- <annotations>).
data TFX_annotated = TFX_annotated Name Formula_role TFX_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_annotated> ::= tff(<name>,<formula_role>,<tff_formula>
-- <annotations>).
data TFF_annotated = TFF_annotated Name Formula_role TFF_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <tcf_annotated> ::= tcf(<name>,<formula_role>,<tcf_formula>
-- <annotations>).
data TCF_annotated = TCF_annotated Name Formula_role TCF_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_annotated> ::= fof(<name>,<formula_role>,<fof_formula>
-- <annotations>).
data FOF_annotated = FOF_annotated Name Formula_role FOF_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
-- <cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula>
-- <annotations>).
data CNF_annotated = CNF_annotated Name Formula_role CNF_formula Annotations
deriving (Show, Ord, Eq, Data, Typeable)
name :: Annotated_formula -> Name
name f = case f of
AF_THF_Annotated (THF_annotated n _ _ _) -> n
AF_TFX_Annotated (TFX_annotated n _ _ _) -> n
AF_TFF_Annotated (TFF_annotated n _ _ _) -> n
AF_TCF_Annotated (TCF_annotated n _ _ _) -> n
AF_FOF_Annotated (FOF_annotated n _ _ _) -> n
AF_CNF_Annotated (CNF_annotated n _ _ _) -> n
AF_TPI_Annotated (TPI_annotated n _ _ _) -> n
formulaRole :: Annotated_formula -> Formula_role
formulaRole f = case f of
AF_THF_Annotated (THF_annotated _ r _ _) -> r
AF_TFX_Annotated (TFX_annotated _ r _ _) -> r
AF_TFF_Annotated (TFF_annotated _ r _ _) -> r
AF_TCF_Annotated (TCF_annotated _ r _ _) -> r
AF_FOF_Annotated (FOF_annotated _ r _ _) -> r
AF_CNF_Annotated (CNF_annotated _ r _ _) -> r
AF_TPI_Annotated (TPI_annotated _ r _ _) -> r
annotations :: Annotated_formula -> Annotations
annotations f = case f of
AF_THF_Annotated (THF_annotated _ _ _ a) -> a
AF_TFX_Annotated (TFX_annotated _ _ _ a) -> a
AF_TFF_Annotated (TFF_annotated _ _ _ a) -> a
AF_TCF_Annotated (TCF_annotated _ _ _ a) -> a
AF_FOF_Annotated (FOF_annotated _ _ _ a) -> a
AF_CNF_Annotated (CNF_annotated _ _ _ a) -> a
AF_TPI_Annotated (TPI_annotated _ _ _ a) -> a
-- <annotations> ::= ,<source><optional_info> | <null>
newtype Annotations = Annotations (Maybe (Source, Optional_info))
deriving (Show, Ord, Eq, Data, Typeable)
-- Types for problems
-- %----Types for problems.
-- <formula_role> ::= <lower_word>
-- <formula_role> :== axiom | hypothesis | definition | assumption |
-- lemma | theorem | corollary | conjecture |
-- negated_conjecture | plain | type |
-- fi_domain | fi_functors | fi_predicates | unknown
data Formula_role = Axiom
| Hypothesis
| Definition
| Assumption
| Lemma
| Theorem
| Corollary
| Conjecture
| Negated_conjecture
| Plain
| Type
| Fi_domain
| Fi_functors
| Fi_predicates
| Unknown
| Other_formula_role Token
-- ^ For future updates. Should not be used.
deriving (Show, Ord, Eq, Data, Typeable)
-- %----THF formulae.
-- <thf_formula> ::= <thf_logic_formula> | <thf_sequent>
data THF_formula = THFF_logic THF_logic_formula
| THFF_sequent THF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
-- <thf_type_formula> | <thf_subtype>
data THF_logic_formula = THFLF_binary THF_binary_formula
| THFLF_unitary THF_unitary_formula
| THFLF_type THF_type_formula
| THFLF_subtype THF_subtype
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_binary_formula> ::= <thf_binary_pair> | <thf_binary_tuple>
data THF_binary_formula = THFBF_pair THF_binary_pair
| THFBF_tuple THF_binary_tuple
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Only some binary connectives can be written without ()s.
-- %----There's no precedence among binary connectives
-- <thf_binary_pair> ::= <thf_unitary_formula> <thf_pair_connective>
-- <thf_unitary_formula>
data THF_binary_pair = THF_binary_pair THF_pair_connective THF_unitary_formula THF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_binary_tuple> ::= <thf_or_formula> | <thf_and_formula> |
-- <thf_apply_formula>
data THF_binary_tuple = THFBT_or THF_or_formula
| THFBT_and THF_and_formula
| THFBT_apply THF_apply_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_or_formula> ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
-- <thf_or_formula> <vline> <thf_unitary_formula>
type THF_or_formula = [THF_unitary_formula]
-- <thf_and_formula> ::= <thf_unitary_formula> & <thf_unitary_formula> |
-- <thf_and_formula> & <thf_unitary_formula>
type THF_and_formula = [THF_unitary_formula]
-- <thf_apply_formula> ::= <thf_unitary_formula> @ <thf_unitary_formula> |
-- <thf_apply_formula> @ <thf_unitary_formula>
type THF_apply_formula = [THF_unitary_formula]
-- <thf_unitary_formula> ::= <thf_quantified_formula> | <thf_unary_formula> |
-- <thf_atom> | <thf_conditional> | <thf_let> |
-- <thf_tuple> | (<thf_logic_formula>)
data THF_unitary_formula = THFUF_quantified THF_quantified_formula
| THFUF_unary THF_unary_formula
| THFUF_atom THF_atom
| THFUF_conditional THF_conditional
| THFUF_let THF_let
| THFUF_tuple THF_tuple
| THFUF_logic THF_logic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_quantified_formula> ::= <thf_quantification> <thf_unitary_formula>
data THF_quantified_formula = THF_quantified_formula THF_quantification THF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_quantification> ::= <thf_quantifier> [<thf_variable_list>] :
data THF_quantification = THF_quantification THF_quantifier THF_variable_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_variable_list> ::= <thf_variable> | <thf_variable>,<thf_variable_list>
type THF_variable_list = [THF_variable]
-- <thf_variable> ::= <thf_typed_variable> | <variable>
data THF_variable = THFV_typed THF_typed_variable
| THFV_variable Variable
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_typed_variable> ::= <variable> : <thf_top_level_type>
data THF_typed_variable = THF_typed_variable Variable THF_top_level_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_unary_formula> ::= <thf_unary_connective> (<thf_logic_formula>)
data THF_unary_formula = THF_unary_formula THF_unary_connective THF_logic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_atom> ::= <thf_function> | <variable> | <defined_term> |
-- <thf_conn_term>
data THF_atom = THF_atom_function THF_function
| THF_atom_variable Variable
| THF_atom_defined Defined_term
| THF_atom_conn THF_conn_term
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_function> ::= <atom> | <functor>(<thf_arguments>) |
-- <defined_functor>(<thf_arguments>) |
-- <system_functor>(<thf_arguments>)
data THF_function = THFF_atom Atom
| THFF_functor TPTP_functor THF_arguments
| THFF_defined Defined_functor THF_arguments
| THFF_system System_functor THF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_conn_term> ::= <thf_pair_connective> | <assoc_connective> |
-- <thf_unary_connective>
data THF_conn_term = THFC_pair THF_pair_connective
| THFC_assoc Assoc_connective
| THFC_unary THF_unary_connective
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_conditional> ::= $ite(<thf_logic_formula>,<thf_logic_formula>,
-- <thf_logic_formula>)
data THF_conditional = THF_conditional THF_logic_formula THF_logic_formula THF_logic_formula -- $ite
deriving (Show, Ord, Eq, Data, Typeable)
-- %----The LHS of a term or formula binding must be a non-variable term that
-- %----is flat with pairwise distinct variable arguments, and the variables in
-- %----the LHS must be exactly those bound in the universally quantified variable
-- %----list, in the same order. Let definitions are not recursive: a non-variable
-- %----symbol introduced in the LHS of a let definition cannot occur in the RHS.
-- %----If a symbol with the same signature as the one in the LHS of the binding
-- %----is declared above the let expression (at the top level or in an
-- %----encompassing let) then it can be used in the RHS of the binding, but it is
-- %----not accessible in the term or formula of the let expression. Let
-- %----expressions can be eliminated by a simple definition expansion.
-- <thf_let> ::= $let(<thf_unitary_formula>,<thf_formula>)
-- <thf_let> :== $let(<thf_let_defns>,<thf_formula>)
data THF_let = THF_let THF_let_defns THF_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_let_defns> :== <thf_let_defn> | [<thf_let_defn_list>]
data THF_let_defns = THFLD_single THF_let_defn
| THFLD_many THF_let_defn_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_let_defn_list> :== <thf_let_defn> | <thf_let_defn>,<thf_let_defn_list>
type THF_let_defn_list = [THF_let_defn]
-- <thf_let_defn> :== <thf_let_quantified_defn> | <thf_let_plain_defn>
data THF_let_defn = THFLD_quantified THF_let_quantified_defn
| THFLD_plain THF_let_plain_defn
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_let_quantified_defn> :== <thf_quantification> (<thf_let_plain_defn>)
data THF_let_quantified_defn = THF_let_quantified_defn THF_quantification THF_let_plain_defn
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_let_plain_defn> :== <thf_let_defn_LHS> <assignment> <thf_formula>
data THF_let_plain_defn = THF_let_plain_defn THF_let_defn_LHS THF_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_let_defn_LHS> :== <constant> | <functor>(<fof_arguments>) |
-- <thf_tuple>
-- %----The <fof_arguments> must all be <variable>s, and the <thf_tuple> may
-- %----contain only <constant>s and <functor>(<fof_arguments>)s
data THF_let_defn_LHS = THFLDL_constant Constant
| THFLDL_functor TPTP_functor FOF_arguments
| THFLDL_tuple THF_tuple
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_arguments> ::= <thf_formula_list>
type THF_arguments = THF_formula_list
-- <thf_type_formula> ::= <thf_typeable_formula> : <thf_top_level_type>
-- <thf_type_formula> :== <constant> : <thf_top_level_type>
data THF_type_formula = THFTF_typeable THF_typeable_formula THF_top_level_type
| THFTF_constant Constant THF_top_level_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_typeable_formula> ::= <thf_atom> | (<thf_logic_formula>)
data THF_typeable_formula = THFTF_atom THF_atom
| THFTF_logic THF_logic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_subtype> ::= <thf_atom> <subtype_sign> <thf_atom>
data THF_subtype = THF_subtype THF_atom THF_atom
deriving (Show, Ord, Eq, Data, Typeable)
-- %----<thf_top_level_type> appears after ":", where a type is being specified
-- %----for a term or variable. <thf_unitary_type> includes <thf_unitary_formula>,
-- %----so the syntax allows just about any lambda expression with "enough"
-- %----parentheses to serve as a type. The expected use of this flexibility is
-- %----parametric polymorphism in types, expressed with lambda abstraction.
-- %----Mapping is right-associative: o > o > o means o > (o > o).
-- %----Xproduct is left-associative: o * o * o means (o * o) * o.
-- %----Union is left-associative: o + o + o means (o + o) + o.
-- <thf_top_level_type> ::= <thf_unitary_type> | <thf_mapping_type>
data THF_top_level_type = THFTLT_unitary THF_unitary_type
| THFTLT_mapping THF_mapping_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_unitary_type> ::= <thf_unitary_formula> | (<thf_binary_type>)
data THF_unitary_type = THFUT_unitary THF_unitary_formula
| THFUT_binary THF_binary_type
deriving (Show, Ord, Eq, Data, Typeable)
-- Each of these binary types has at least two (!) list entries.
-- <thf_binary_type> ::= <thf_mapping_type> | <thf_xprod_type> |
-- <thf_union_type>
data THF_binary_type = THFBT_mapping THF_mapping_type
| THFBT_xprod THF_xprod_type
| THFBT_union THF_union_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_mapping_type> ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
-- <thf_unitary_type> <arrow> <thf_mapping_type>
type THF_mapping_type = [THF_unitary_type] -- right associative
-- <thf_xprod_type> ::= <thf_unitary_type> <star> <thf_unitary_type> |
-- <thf_xprod_type> <star> <thf_unitary_type>
type THF_xprod_type = [THF_unitary_type] -- left associative
-- <thf_union_type> ::= <thf_unitary_type> <plus> <thf_unitary_type> |
-- <thf_union_type> <plus> <thf_unitary_type>
type THF_union_type = [THF_unitary_type] -- right associative
-- %----Sequents using the Gentzen arrow
-- <thf_sequent> ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
-- (<thf_sequent>)
data THF_sequent = THFS_plain THF_tuple THF_tuple
| THFS_parens THF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_tuple> ::= [] | [<thf_formula_list>]
newtype THF_tuple = THF_tuple THF_formula_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_formula_list> ::= <thf_logic_formula> |
-- <thf_logic_formula>,<thf_formula_list>
type THF_formula_list = [THF_logic_formula]
-- NOTE: not used by parser
-- %----New material for modal logic semantics, not integrated yet
-- <logic_defn_rule> :== <logic_defn_LHS> <assignment> <logic_defn_RHS>-
-- data Logic_defn_rule = Logic_defn_rule Logic_defn_LHS Logic_defn_RHS
-- deriving (Show, Ord, Eq, Data, Typeable)
-- NOTE: not used by parser
-- <logic_defn_LHS> :== <logic_defn_value> | <thf_top_level_type> | <name>
-- <logic_defn_LHS> :== $constants | $quantification | $consequence |
-- $modalities
-- %----The $constants, $quantification, and $consequence apply to all of the
-- %----$modalities. Each of these may be specified only once, but not necessarily
-- %----all in a single annotated formula.-
-- data Logic_defn_LHS = Logic_defn_LHS_value Logic_defn_value
-- | Logic_defn_LHS_THF_Top_level_type THF_top_level_type
-- | Logic_defn_LHS_name Name
-- | LDLC_constants
-- | LDLC_quantification
-- | LDLC_consequence
-- | LDLC_modalities
-- deriving (Show, Ord, Eq, Data, Typeable)
-- NOTE: not used by parser
-- <logic_defn_RHS> :== <logic_defn_value> | <thf_unitary_formula>-
-- data Logic_defn_RHS = Logic_defn_RHS_value Logic_defn_value
-- | Logic_defn_RNG_THF_Unitary_forumla THF_unitary_formula
-- deriving (Show, Ord, Eq, Data, Typeable)
-- NOTE: not used by parser
-- <logic_defn_value> :== <defined_constant>
-- <logic_defn_value> :== $rigid | $flexible |
-- $constant | $varying | $cumulative | $decreasing |
-- $local | $global |
-- $modal_system_K | $modal_system_T | $modal_system_D |
-- $modal_system_S4 | $modal_system_S5 |
-- $modal_axiom_K | $modal_axiom_T | $modal_axiom_B |
-- $modal_axiom_D | $modal_axiom_4 | $modal_axiom_5-
-- data Logic_defn_value = Rigid
-- | Flexible
-- | Constant
-- | Varying
-- | Cumulative
-- | Decreasing
-- | Local
-- | Global
-- | Modal_system_K
-- | Modal_system_T
-- | Modal_system_D
-- | Modal_system_S4
-- | Modal_system_S5
-- | Modal_axiom_K
-- | Modal_axiom_T
-- | Modal_axiom_B
-- | Modal_axiom_D
-- | Modal_axiom_4
-- | Modal_axiom_5
-- deriving (Show, Ord, Eq, Data, Typeable)
-- %----TFX formulae
-- <tfx_formula> ::= <tfx_logic_formula> | <thf_sequent>
data TFX_formula = TFXF_logic TFX_logic_formula
| TFXF_sequent THF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <tfx_logic_formula> ::= <thf_logic_formula>
-- % <tfx_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
-- % <tff_typed_atom> | <tff_subtype>
data TFX_logic_formula = TFXLF_binary THF_binary_formula
| TFXLF_unitary THF_unitary_formula
| TFXLF_typed TFF_typed_atom
| TFXLF_subtype TFF_subtype
deriving (Show, Ord, Eq, Data, Typeable)
-- %----TFF formulae.
-- <tff_formula> ::= <tff_logic_formula> | <tff_typed_atom> |
-- <tff_sequent>
data TFF_formula = TFFF_logic TFF_logic_formula
| TFFF_atom TFF_typed_atom
| TFFF_sequent TFF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_logic_formula> ::= <tff_binary_formula> | <tff_unitary_formula> |
-- <tff_subtype>
data TFF_logic_formula = TFFLF_binary TFF_binary_formula
| TFFLF_unitary TFF_unitary_formula
| TFFLF_subtype TFF_subtype
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_binary_formula> ::= <tff_binary_nonassoc> | <tff_binary_assoc>
data TFF_binary_formula = TFFBF_nonassoc TFF_binary_nonassoc
| TFFBF_assoc TFF_binary_assoc
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_binary_nonassoc> ::= <tff_unitary_formula> <binary_connective>
-- <tff_unitary_formula>
data TFF_binary_nonassoc = TFF_binary_nonassoc Binary_connective TFF_unitary_formula TFF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_binary_assoc> ::= <tff_or_formula> | <tff_and_formula>
data TFF_binary_assoc = TFFBA_or TFF_or_formula
| TFFBA_and TFF_and_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_or_formula> ::= <tff_unitary_formula> <vline> <tff_unitary_formula> |
-- <tff_or_formula> <vline> <tff_unitary_formula>
type TFF_or_formula = [TFF_unitary_formula]
-- <tff_and_formula> ::= <tff_unitary_formula> & <tff_unitary_formula> |
-- <tff_and_formula> & <tff_unitary_formula>
type TFF_and_formula = [TFF_unitary_formula]
-- <tff_unitary_formula> ::= <tff_quantified_formula> | <tff_unary_formula> |
-- <tff_atomic_formula> | <tff_conditional> |
-- <tff_let> | (<tff_logic_formula>)
data TFF_unitary_formula = TFFUF_quantified TFF_quantified_formula
| TFFUF_unary TFF_unary_formula
| TFFUF_atomic TFF_atomic_formula
| TFFUF_conditional TFF_conditional
| TFFUF_let TFF_let
| TFFUF_logic TFF_logic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_quantified_formula> ::= <fof_quantifier> [<tff_variable_list>] :
-- <tff_unitary_formula>
data TFF_quantified_formula = TFF_quantified_formula FOF_quantifier TFF_variable_list TFF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_variable_list> ::= <tff_variable> | <tff_variable>,<tff_variable_list>
type TFF_variable_list = [TFF_variable]
-- <tff_variable> ::= <tff_typed_variable> | <variable>
data TFF_variable = TFFV_typed TFF_typed_variable
| TFFV_variable Variable
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_typed_variable> ::= <variable> : <tff_atomic_type>
data TFF_typed_variable = TFF_typed_variable Variable TFF_atomic_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_unary_formula> ::= <unary_connective> <tff_unitary_formula> |
-- <fof_infix_unary>
data TFF_unary_formula = TFFUF_connective Unary_connective TFF_unitary_formula
| TFFUF_infix FOF_infix_unary
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_atomic_formula> ::= <fof_atomic_formula>
type TFF_atomic_formula = FOF_atomic_formula
-- <tff_conditional> ::= $ite_f(<tff_logic_formula>,<tff_logic_formula>,
-- <tff_logic_formula>)
data TFF_conditional = TFF_conditional TFF_logic_formula TFF_logic_formula TFF_logic_formula -- $ite_f
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let> ::= $let_tf(<tff_let_term_defns>,<tff_formula>) |
-- $let_ff(<tff_let_formula_defns>,<tff_formula>)
data TFF_let = TFF_let_term_defns TFF_let_term_defns TFF_formula
| TFF_let_formula_defns TFF_let_formula_defns TFF_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- %----See the commentary for <thf_let>.
-- <tff_let_term_defns> ::= <tff_let_term_defn> | [<tff_let_term_list>]
data TFF_let_term_defns = TFFLTD_single TFF_let_term_defn
| TFFLTD_many TFF_let_term_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let_term_list> ::= <tff_let_term_defn> |
-- <tff_let_term_defn>,<tff_let_term_list>
type TFF_let_term_list = [TFF_let_term_defn]
-- <tff_let_term_defn> ::= ! [<tff_variable_list>] : <tff_let_term_defn> |
-- <tff_let_term_binding>
data TFF_let_term_defn = TFFLTD_variable TFF_variable_list TFF_let_term_defn
| TFFLTD_binding TFF_let_term_binding
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let_term_binding> ::= <fof_plain_term> = <fof_term> |
-- (<tff_let_term_binding>)
data TFF_let_term_binding = TFFLTB_plain FOF_plain_term FOF_term
| TFFLTB_binding TFF_let_term_binding
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let_formula_defns> ::= <tff_let_formula_defn> | [<tff_let_formula_list>]
data TFF_let_formula_defns = TFFLFD_single TFF_let_formula_defn
| TFFLFD_many TFF_let_formula_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let_formula_list> ::= <tff_let_formula_defn> |
-- <tff_let_formula_defn>,<tff_let_formula_list>
type TFF_let_formula_list = [TFF_let_formula_defn]
-- <tff_let_formula_defn> ::= ! [<tff_variable_list>] : <tff_let_formula_defn> |
-- <tff_let_formula_binding>
data TFF_let_formula_defn = TFFLFD_variable TFF_variable_list TFF_let_formula_defn
| TFFLFD_binding TFF_let_formula_binding
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_let_formula_binding> ::= <fof_plain_atomic_formula> <=>
-- <tff_unitary_formula> | (<tff_let_formula_binding>)
data TFF_let_formula_binding = TFFLFB_plain FOF_plain_atomic_formula TFF_unitary_formula
| TFFLFB_binding TFF_let_formula_binding
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_sequent> ::= <tff_formula_tuple> <gentzen_arrow>
-- <tff_formula_tuple> | (<tff_sequent>)
data TFF_sequent = TFFS_plain TFF_formula_tuple TFF_formula_tuple
| TFFS_parens TFF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_formula_tuple> ::= [] | [<tff_formula_tuple_list>]
newtype TFF_formula_tuple = TFF_formula_tuple TFF_formula_tuple_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_formula_tuple_list> ::= <tff_logic_formula> |
-- <tff_logic_formula>,<tff_formula_tuple_list>
type TFF_formula_tuple_list = [TFF_logic_formula]
-- %----<tff_typed_atom> can appear only at top level
-- <tff_typed_atom> ::= <untyped_atom> : <tff_top_level_type> |
-- (<tff_typed_atom>)
data TFF_typed_atom = TFFTA_plain Untyped_atom TFF_top_level_type
| TFFTA_parens TFF_typed_atom
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_subtype> ::= <untyped_atom> <subtype_sign> <atom>
data TFF_subtype = TFF_subtype Untyped_atom Atom
deriving (Show, Ord, Eq, Data, Typeable)
-- %----See <thf_top_level_type> for commentary.
-- <tff_top_level_type> ::= <tff_atomic_type> | <tff_mapping_type> |
-- <tf1_quantified_type> | (<tff_top_level_type>)
data TFF_top_level_type = TFFTLT_atomic TFF_atomic_type
| TFFTLT_mapping TFF_mapping_type
| TFFTLT_quantified TF1_quantified_type
| TFFTLT_parens TFF_top_level_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <tf1_quantified_type> ::= !> [<tff_variable_list>] : <tff_monotype>
data TF1_quantified_type = TF1_quantified_type TFF_variable_list TFF_monotype
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_monotype> ::= <tff_atomic_type> | (<tff_mapping_type>)
data TFF_monotype = TFFMT_atomic TFF_atomic_type
| TFFMT_mapping TFF_mapping_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_unitary_type> ::= <tff_atomic_type> | (<tff_xprod_type>)
data TFF_unitary_type = TFFUT_atomic TFF_atomic_type
| TFFUT_xprod TFF_xprod_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_atomic_type> ::= <type_constant> | <defined_type> |
-- <type_functor>(<tff_type_arguments>) | <variable>
data TFF_atomic_type = TFFAT_constant Type_constant
| TFFAT_defined Defined_type
| TFFAT_functor Type_functor TFF_type_arguments
| TFFAT_variable Variable
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_type_arguments> ::= <tff_atomic_type> |
-- <tff_atomic_type>,<tff_type_arguments>
type TFF_type_arguments = [TFF_atomic_type]
-- %----For consistency with <thf_unitary_type> (the analogue in thf),
-- %----<tff_atomic_type> should also allow (<tff_atomic_type>), but that causes
-- %----ambiguity.
-- <tff_mapping_type> ::= <tff_unitary_type> <arrow> <tff_atomic_type>
data TFF_mapping_type = TFF_mapping_type TFF_unitary_type TFF_atomic_type
deriving (Show, Ord, Eq, Data, Typeable)
-- <tff_xprod_type> ::= <tff_unitary_type> <star> <tff_atomic_type> |
-- <tff_xprod_type> <star> <tff_atomic_type>
data TFF_xprod_type = TFF_xprod_type TFF_unitary_type [TFF_atomic_type]
deriving (Show, Ord, Eq, Data, Typeable)
-- %----TCF formulae.
-- <tcf_formula> ::= <tcf_logic_formula> | <tff_typed_atom>
data TCF_formula = TCFF_logic TCF_logic_formula
| TCFF_atom TFF_typed_atom
deriving (Show, Ord, Eq, Data, Typeable)
-- <tcf_logic_formula> ::= <tcf_quantified_formula> | <cnf_formula>
data TCF_logic_formula = TCFLF_quantified TCF_quantified_formula
| TCFLF_cnf CNF_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <tcf_quantified_formula> ::= ! [<tff_variable_list>] : <cnf_formula>
data TCF_quantified_formula = TCF_quantified TFF_variable_list CNF_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- %----FOF formulae.
-- <fof_formula> ::= <fof_logic_formula> | <fof_sequent>
data FOF_formula = FOFF_logic FOF_logic_formula
| FOFF_sequent FOF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_logic_formula> ::= <fof_binary_formula> | <fof_unitary_formula>
data FOF_logic_formula = FOFLF_binary FOF_binary_formula
| FOFLF_unitary FOF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Future answer variable ideas | <answer_formula>
-- <fof_binary_formula> ::= <fof_binary_nonassoc> | <fof_binary_assoc>
data FOF_binary_formula = FOFBF_nonassoc FOF_binary_nonassoc
| FOFBF_assoc FOF_binary_assoc
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Only some binary connectives are associative
-- %----There's no precedence among binary connectives
-- <fof_binary_nonassoc> ::= <fof_unitary_formula> <binary_connective>
-- <fof_unitary_formula>
data FOF_binary_nonassoc = FOF_binary_nonassoc Binary_connective FOF_unitary_formula FOF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Associative connectives & and | are in <binary_assoc>
-- <fof_binary_assoc> ::= <fof_or_formula> | <fof_and_formula>
data FOF_binary_assoc = FOFBA_or FOF_or_formula
| FOFBA_and FOF_and_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_or_formula> ::= <fof_unitary_formula> <vline> <fof_unitary_formula> |
-- <fof_or_formula> <vline> <fof_unitary_formula>
type FOF_or_formula = [FOF_unitary_formula]
-- <fof_and_formula> ::= <fof_unitary_formula> & <fof_unitary_formula> |
-- <fof_and_formula> & <fof_unitary_formula>
type FOF_and_formula = [FOF_unitary_formula]
-- %----<fof_unitary_formula> are in ()s or do not have a <binary_connective> at
-- %----the top level.
-- <fof_unitary_formula> ::= <fof_quantified_formula> | <fof_unary_formula> |
-- <fof_atomic_formula> | (<fof_logic_formula>)
data FOF_unitary_formula = FOFUF_quantified FOF_quantified_formula
| FOFUF_unary FOF_unary_formula
| FOFUF_atomic FOF_atomic_formula
| FOFUF_logic FOF_logic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_quantified_formula> ::= <fof_quantifier> [<fof_variable_list>] :
-- <fof_unitary_formula>
data FOF_quantified_formula = FOF_quantified_formula FOF_quantifier FOF_variable_list FOF_unitary_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_variable_list> ::= <variable> | <variable>,<fof_variable_list>
type FOF_variable_list = [Variable]
-- <fof_unary_formula> ::= <unary_connective> <fof_unitary_formula> |
-- <fof_infix_unary>
data FOF_unary_formula = FOFUF_connective Unary_connective FOF_unitary_formula
| FOFUF_infix FOF_infix_unary
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_infix_unary> ::= <fof_term> <infix_inequality> <fof_term>
data FOF_infix_unary = FOF_infix_unary FOF_term FOF_term
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_atomic_formula> ::= <fof_plain_atomic_formula> |
-- <fof_defined_atomic_formula> |
-- <fof_system_atomic_formula>
data FOF_atomic_formula = FOFAT_plain FOF_plain_atomic_formula
| FOFAT_defined FOF_defined_atomic_formula
| FOFAT_system FOF_system_atomic_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_plain_atomic_formula> ::= <fof_plain_term>
-- <fof_plain_atomic_formula> :== <proposition> | <predicate>(<fof_arguments>)
data FOF_plain_atomic_formula = FOFPAF_proposition Proposition
| FOFPAF_predicate Predicate FOF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_defined_atomic_formula> ::= <fof_defined_plain_formula> |
-- <fof_defined_infix_formula>
data FOF_defined_atomic_formula = FOFDAF_plain FOF_defined_plain_formula
| FOFDAF_infix FOF_defined_infix_formula
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_defined_plain_formula> ::= <fof_defined_plain_term>
-- <fof_defined_plain_formula> :== <defined_proposition> |
-- <defined_predicate>(<fof_arguments>)
data FOF_defined_plain_formula = FOFDPF_proposition Defined_proposition
| FOFDPF_predicate Defined_predicate FOF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_defined_infix_formula> ::= <fof_term> <defined_infix_pred> <fof_term>
data FOF_defined_infix_formula = FOF_defined_infix_formula Defined_infix_pred FOF_term FOF_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %----System terms have system specific interpretations
-- <fof_system_atomic_formula> ::= <fof_system_term>
-- %----<fof_system_atomic_formula>s are used for evaluable predicates that are
-- %----available in particular tools. The predicate names are not controlled
-- %----by the TPTP syntax, so use with due care. The same is true for
-- %----<fof_system_term>s.
newtype FOF_system_atomic_formula = FOF_system_atomic_formula FOF_system_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %----FOF terms.
-- <fof_plain_term> ::= <constant> | <functor>(<fof_arguments>)
data FOF_plain_term = FOFPT_constant Constant
| FOFPT_functor TPTP_functor FOF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Defined terms have TPTP specific interpretations
-- <fof_defined_term> ::= <defined_term> | <fof_defined_atomic_term>
data FOF_defined_term = FOFDT_term Defined_term
| FOFDT_atomic FOF_defined_atomic_term
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_defined_atomic_term> ::= <fof_defined_plain_term>
-- %----None yet | <defined_infix_term>
data FOF_defined_atomic_term = FOFDAT_plain FOF_defined_plain_term
-- | FOFDAT_indix Defined_infix_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %----None yet <defined_infix_term> ::= <fof_term> <defined_infix_func> <fof_term>
-- data Defined_infix_term = Defined_infix_term Defined_infix_func FOF_term FOF_term
-- deriving (Show, Ord, Eq, Data, Typeable)
-- %----None yet <defined_infix_func> ::=
-- data Defined_infix_func =
-- <fof_defined_plain_term> ::= <defined_constant> |
-- <defined_functor>(<fof_arguments>)
-- %----Add $tuple for tuples, because [<fof_arguments>] doesn't work.
data FOF_defined_plain_term = FOFDPT_constant Defined_constant
| FOFDPT_functor Defined_functor FOF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- %----System terms have system specific interpretations
-- <fof_system_term> ::= <system_constant> | <system_functor>(<fof_arguments>)
data FOF_system_term = FOFST_constant System_constant
| FOFST_functor System_functor FOF_arguments
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Arguments recurse back up to terms (this is the FOF world here)
-- <fof_arguments> ::= <fof_term> | <fof_term>,<fof_arguments>
type FOF_arguments = [FOF_term]
-- %----These are terms used as arguments. Not the entry point for terms because
-- %----<fof_plain_term> is also used as <fof_plain_atomic_formula>
-- <fof_term> ::= <fof_function_term> | <variable> |
-- <tff_conditional_term> | <tff_let_term>
data FOF_term = FOFT_function FOF_function_term
| FOFT_variable Variable
| FOFT_conditional TFF_conditional_term
| FOFT_let TFF_let_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %% DAMN THIS JUST WON'T WORK | <tuple_term>
-- %----<tuple_term> is for TFF only, but it's here because it's used in
-- %----<fof_atomic_formula>, which is also used as <tff_atomic_formula>.
-- % <tuple_term> ::= [] | [<fof_arguments>]
-- <fof_function_term> ::= <fof_plain_term> | <fof_defined_term> |
-- <fof_system_term>
data FOF_function_term = FOFFT_plain FOF_plain_term
| FOFFT_defined FOF_defined_term
| FOFFT_system FOF_system_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Conditional terms should be used by only TFF.
-- <tff_conditional_term> ::= $ite_t(<tff_logic_formula>,<fof_term>,<fof_term>)
data TFF_conditional_term = TFF_conditional_term TFF_logic_formula FOF_term FOF_term
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Let terms should be used by only TFF. $let_ft is for use when there is
-- %----a $ite_t in the <fof_term>. See the commentary for $let_tf and $let_ff.
-- <tff_let_term> ::= $let_ft(<tff_let_formula_defns>,<fof_term>) |
-- $let_tt(<tff_let_term_defns>,<fof_term>)
data TFF_let_term = TFFLT_formula TFF_let_formula_defns FOF_term
| TFFLT_term TFF_let_term_defns FOF_term
deriving (Show, Ord, Eq, Data, Typeable)
{-
%----This section is the FOFX syntax. Not yet in use.
% <fof_let> ::= := [<fof_let_list>] : <fof_unitary_formula>
% <fof_let_list> ::= <fof_defined_var> |
% <fof_defined_var>,<fof_let_list>
% <fof_defined_var> ::= <variable> := <fof_logic_formula> |
% <variable> :- <fof_term> | (<fof_defined_var>)
%
% <fof_conditional> ::= $ite_f(<fof_logic_formula>,<fof_logic_formula>,
% <fof_logic_formula>)
%
% <fof_conditional_term> ::= $ite_t(<fof_logic_formula>,<fof_term>,<fof_term>)
-}
-- <fof_sequent> ::= <fof_formula_tuple> <gentzen_arrow>
-- <fof_formula_tuple> | (<fof_sequent>)
data FOF_sequent = FOFS_plain FOF_formula_tuple FOF_formula_tuple
| FOFS_parens FOF_sequent
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_formula_tuple> ::= [] | [<fof_formula_tuple_list>]
newtype FOF_formula_tuple = FOF_formula_tuple FOF_formula_tuple_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <fof_formula_tuple_list> ::= <fof_logic_formula> |
-- <fof_logic_formula>,<fof_formula_tuple_list>
type FOF_formula_tuple_list = [FOF_logic_formula]
-- %----CNF formulae (variables implicitly universally quantified)
-- <cnf_formula> ::= <disjunction> | (<disjunction>)
data CNF_formula = CNFF_plain Disjunction
| CNFF_parens Disjunction
deriving (Show, Ord, Eq, Data, Typeable)
-- <disjunction> ::= <literal> | <disjunction> <vline> <literal>
newtype Disjunction = Disjunction [Literal]
deriving (Show, Ord, Eq, Data, Typeable)
-- <literal> ::= <fof_atomic_formula> | ~ <fof_atomic_formula> |
-- <fof_infix_unary>
data Literal = Lit_atomic FOF_atomic_formula
| Lit_negative FOF_atomic_formula
| Lit_fof_infix FOF_infix_unary
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Connectives - THF
-- <thf_quantifier> ::= <fof_quantifier> | <th0_quantifier> |
-- <th1_quantifier>
data THF_quantifier = THFQ_fof FOF_quantifier
| THFQ_th0 TH0_quantifier
| THFQ_th1 TH1_quantifier
deriving (Show, Ord, Eq, Data, Typeable)
-- %----TH0 quantifiers are also available in TH1
-- <th1_quantifier> ::= !> | ?*
data TH1_quantifier = TH1_DependentProduct -- !>
| TH1_DependentSum -- ?*
deriving (Show, Ord, Eq, Data, Typeable)
-- <th0_quantifier> ::= ^ | @+ | @-
data TH0_quantifier = TH0_LambdaBinder -- ^
| TH0_IndefiniteDescription -- @+
| TH0_DefiniteDescription -- @-
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_pair_connective> ::= <infix_equality> | <infix_inequality> |
-- <binary_connective> | <assignment>
data THF_pair_connective = THF_infix_equality
| Infix_inequality
| THFPC_binary Binary_connective
| THF_assignment
deriving (Show, Ord, Eq, Data, Typeable)
-- <thf_unary_connective> ::= <unary_connective> | <th1_unary_connective>
data THF_unary_connective = THFUC_unary Unary_connective
| THFUC_th1 TH1_unary_connective
deriving (Show, Ord, Eq, Data, Typeable)
-- <th1_unary_connective> ::= !! | ?? | @@+ | @@- | @=
data TH1_unary_connective = TH1_PiForAll -- !!
| TH1_PiSigmaExists -- ??
| TH1_PiIndefiniteDescription -- @@+
| TH1_PiDefiniteDescription -- @@-
| TH1_PiEquality -- @=
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Connectives - TFF
-- % <tff_pair_connective> ::= <binary_connective> | <assignment>
-- Note: not used
-- data TFF_pair_connective = TFFPC_binary Binary_connective
-- | TFFPC_assignment TFF_assignment
-- deriving (Show, Ord, Eq, Data, Typeable)
-- %----Connectives - FOF
-- <fof_quantifier> ::= ! | ?
data FOF_quantifier = ForAll -- !
| Exists -- ?
deriving (Show, Ord, Eq, Data, Typeable)
-- <binary_connective> ::= <=> | => | <= | <~> | ~<vline> | ~&
data Binary_connective = Equivalence
| Implication
| ReverseImplication
| XOR
| NOR
| NAND
deriving (Show, Ord, Eq, Data, Typeable)
-- <assoc_connective> ::= <vline> | &
data Assoc_connective = OR
| AND
deriving (Show, Ord, Eq, Data, Typeable)
-- <unary_connective> ::= ~
data Unary_connective = NOT deriving (Show, Ord, Eq, Data, Typeable)
-- %----Types for THF and TFF
-- <type_constant> ::= <type_functor>
type Type_constant = Type_functor
-- <type_functor> ::= <atomic_word>
type Type_functor = Token
-- <defined_type> ::= <atomic_defined_word>
-- <defined_type> :== $oType | $o | $iType | $i | $tType |
-- $real | $rat | $int
data Defined_type = OType -- $oType/$o is the Boolean type, i.e., the type of $true and $false.
| O -- $oType/$o is the Boolean type, i.e., the type of $true and $false.
| IType -- $iType/$i is non-empty type of individuals, which may be finite or infinite.
| I -- $iType/$i is non-empty type of individuals, which may be finite or infinite.
| TType -- $tType is the type (kind) of all types.
| Real -- $real is the type of <real>s.
| Rat -- $rat is the type of <rational>s.
| Int -- $int is the type of <signed_integer>s and <unsigned_integer>s.
deriving (Show, Ord, Eq, Data, Typeable)
-- <system_type> :== <atomic_system_word>
-- Note: not used
-- type System_type = Token
-- %----For all language types
-- <atom> ::= <untyped_atom> | <defined_constant>
data Atom = Atom_untyped Untyped_atom
| Atom_constant Defined_constant
deriving (Show, Ord, Eq, Data, Typeable)
-- <untyped_atom> ::= <constant> | <system_constant>
data Untyped_atom = UA_constant Constant
| UA_system System_constant
deriving (Show, Ord, Eq, Data, Typeable)
type Proposition = Predicate
type Predicate = Token
-- <defined_proposition> :== <atomic_defined_word>
-- <defined_proposition> :== $true | $false
data Defined_proposition = TPTP_true
| TPTP_false
deriving (Show, Ord, Eq, Data, Typeable)
-- <defined_predicate> :== <atomic_defined_word>
-- <defined_predicate> :== $distinct |
-- $less | $lesseq | $greater | $greatereq |
-- $is_int | $is_rat |
-- $box_P | $box_i | $box_int | $box |
-- $dia_P | $dia_i | $dia_int | $dia
-- %----$distinct means that each of it's constant arguments are pairwise !=. It
-- %----is part of the TFF syntax. It can be used only as a fact, not under any
-- %----connective.
data Defined_predicate = Distinct
| Less
| Lesseq
| Greater
| Greatereq
| Is_int
| Is_rat
| Box_P
| Box_i
| Box_int
| Box
| Dia_P
| Dia_i
| Dia_int
| Dia
deriving (Show, Ord, Eq, Data, Typeable)
-- <defined_infix_pred> ::= <infix_equality> | <assignment>
-- <infix_equality> ::= =
-- <infix_inequality> ::= !=
data Defined_infix_pred = Defined_infix_equality
| Defined_assignment
deriving (Show, Ord, Eq, Data, Typeable)
-- <constant> ::= <functor>
type Constant = TPTP_functor
-- <functor> ::= <atomic_word>
type TPTP_functor = Token
-- <system_constant> ::= <system_functor>
type System_constant = System_functor
-- <system_functor> ::= <atomic_system_word>
type System_functor = Token
-- <defined_constant> ::= <defined_functor>
type Defined_constant = Defined_functor
-- <defined_functor> ::= <atomic_defined_word>
-- <defined_functor> :== $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
data Defined_functor = 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
| DF_atomic_defined_word Atomic_defined_word
deriving (Show, Ord, Eq, Data, Typeable)
-- <defined_term> ::= <number> | <distinct_object>
data Defined_term = DT_number Number
| DT_object Distinct_object
deriving (Show, Ord, Eq, Data, Typeable)
-- <variable> ::= <upper_word>
type Variable = Token
-- %----Formula sources
-- <source> ::= <general_term>
-- <source> :== <dag_source> | <internal_source> |
-- <external_source> | unknown | [<sources>]
data Source = Source_DAG DAG_source
| Source_internal Internal_source
| Source_external External_source
| Unknown_source
| Source_many Sources
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Alternative sources are recorded like this, thus allowing representation
-- %----of alternative derivations with shared parts.
-- <sources> :== <source> | <source>,<sources>
type Sources = [Source]
-- %----Only a <dag_source> can be a <name>, i.e., derived formulae can be
-- %----identified by a <name> or an <inference_record>
-- <dag_source> :== <name> | <inference_record>
data DAG_source = DAGS_name Name
| DAGS_record Inference_record
deriving (Show, Ord, Eq, Data, Typeable)
-- <inference_record> :== inference(<inference_rule>,<useful_info>,
-- <inference_parents>)
data Inference_record = Inference_record Inference_rule Useful_info Inference_parents
deriving (Show, Ord, Eq, Data, Typeable)
-- <inference_rule> :== <atomic_word>
-- %----Examples are deduction | modus_tollens | modus_ponens | rewrite |
-- % resolution | paramodulation | factorization |
-- % cnf_conversion | cnf_refutation | ...
type Inference_rule = Token
-- %----<inference_parents> can be empty in cases when there is a justification
-- %----for a tautologous theorem. In case when a tautology is introduced as
-- %----a leaf, e.g., for splitting, then use an <internal_source>.
-- <inference_parents> :== [] | [<parent_list>]
type Inference_parents = Parent_list
-- <parent_list> :== <parent_info> | <parent_info>,<parent_list>
type Parent_list = [Parent_info]
-- <parent_info> :== <source><parent_details>
data Parent_info = Parent_info Source Parent_details
deriving (Show, Ord, Eq, Data, Typeable)
-- <parent_details> :== :<general_list> | <null>
type Parent_details = Maybe General_list
-- <internal_source> :== introduced(<intro_type><optional_info>)
data Internal_source = Internal_source Intro_type Optional_info
deriving (Show, Ord, Eq, Data, Typeable)
-- <intro_type> :== definition | axiom_of_choice | tautology | assumption
-- %----This should be used to record the symbol being defined, or the function
-- %----for the axiom of choice
data Intro_type = IntroTypeDefinition
| AxiomOfChoice
| Tautology
| IntroTypeAssumption
deriving (Show, Ord, Eq, Data, Typeable)
-- <external_source> :== <file_source> | <theory> | <creator_source>
data External_source = ExtSrc_file File_source
| ExtSrc_theory Theory
| ExtSrc_creator Creator_source
deriving (Show, Ord, Eq, Data, Typeable)
-- <file_source> :== file(<file_name><file_info>)
data File_source = File_source File_name File_info
deriving (Show, Ord, Eq, Data, Typeable)
-- <file_info> :== ,<name> | <null>
type File_info = Maybe Name
-- <theory> :== theory(<theory_name><optional_info>)
data Theory = Theory Theory_name Optional_info
deriving (Show, Ord, Eq, Data, Typeable)
-- <theory_name> :== equality | ac
data Theory_name = TN_equality
| TN_ac
deriving (Show, Ord, Eq, Data, Typeable)
-- %----More theory names may be added in the future. The <optional_info> is
-- %----used to store, e.g., which axioms of equality have been implicitly used,
-- %----e.g., theory(equality,[rst]). Standard format still to be decided.
-- <creator_source> :== creator(<creator_name><optional_info>)
data Creator_source = Creator_source Creator_name Optional_info
deriving (Show, Ord, Eq, Data, Typeable)
-- <creator_name> :== <atomic_word>
type Creator_name = Token
-- %----Useful info fields
-- <optional_info> ::= ,<useful_info> | <null>
type Optional_info = Maybe Useful_info
-- <useful_info> ::= <general_list>
-- <useful_info> :== [] | [<info_items>]
data Useful_info = UI_items Info_items
| UI_general_list General_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <info_items> :== <info_item> | <info_item>,<info_items>
type Info_items = [Info_item]
-- <info_item> :== <formula_item> | <inference_item> |
-- <general_function>
data Info_item = Info_formula Formula_item
| Info_inference Inference_item
| Info_general General_function
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Useful info for formula records
-- <formula_item> :== <description_item> | <iquote_item>
data Formula_item = FI_description Description_item
| FI_iquote Iquote_item
deriving (Show, Ord, Eq, Data, Typeable)
-- <description_item> :== description(<atomic_word>)
type Description_item = Token
-- <iquote_item> :== iquote(<atomic_word>)
-- %----<iquote_item>s are used for recording exactly what the system output about
-- %----the inference step. In the future it is planned to encode this information
-- %----in standardized forms as <parent_details> in each <inference_record>.
-- %----Useful info for inference records
type Iquote_item = Token
-- <inference_item> :== <inference_status> | <assumptions_record> |
-- <new_symbol_record> | <refutation>
data Inference_item = Inf_status Inference_status
| Inf_assumption Assumptions_record
| Inf_symbol New_symbol_record
| Inf_refutation Refutation
deriving (Show, Ord, Eq, Data, Typeable)
-- <inference_status> :== status(<status_value>) | <inference_info>
data Inference_status = Inf_value Status_value
| Inf_info Inference_info
deriving (Show, Ord, Eq, Data, Typeable)
-- %----These are the success status values from the SZS ontology. The most
-- %----commonly used values are:
-- %---- thm - Every model of the parent formulae is a model of the inferred
-- %---- formula. Regular logical consequences.
-- %---- cth - Every model of the parent formulae is a model of the negation of
-- %---- the inferred formula. Used for negation of conjectures in FOF to
-- %---- CNF conversion.
-- %---- esa - There exists a model of the parent formulae iff there exists a
-- %---- model of the inferred formula. Used for Skolemization steps.
-- %----For the full hierarchy see the SZSOntology file distributed with the TPTP.
-- <status_value> :== 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
data Status_value = 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
deriving (Show, Ord, Eq, Data, Typeable)
-- %----<inference_info> is used to record standard information associated with an
-- %----arbitrary inference rule. The <inference_rule> is the same as the
-- %----<inference_rule> of the <inference_record>. The <atomic_word> indicates
-- %----the information being recorded in the <general_list>. The <atomic_word>
-- %----are (loosely) set by TPTP conventions, and include esplit, sr_split, and
-- %----discharge.
-- <inference_info> :== <inference_rule>(<atomic_word>,<general_list>)
data Inference_info = Inference_info Inference_rule Atomic_word General_list
deriving (Show, Ord, Eq, Data, Typeable)
-- %----An <assumptions_record> lists the names of assumptions upon which this
-- %----inferred formula depends. These must be discharged in a completed proof.
-- <assumptions_record> :== assumptions([<name_list>])
type Assumptions_record = Name_list
-- %----A <refutation> record names a file in which the inference recorded here
-- %----is recorded as a proof by refutation.
-- <refutation> :== refutation(<file_source>)
type Refutation = File_source
-- %----A <new_symbol_record> provides information about a newly introduced symbol.
-- <new_symbol_record> :== new_symbols(<atomic_word>,[<new_symbol_list>])
data New_symbol_record = New_symbol_record Atomic_word New_symbol_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <new_symbol_list> :== <principal_symbol> |
-- <principal_symbol>,<new_symbol_list>
type New_symbol_list = [Principal_symbol]
-- %----Principal symbols are predicates, functions, variables
-- <principal_symbol> :== <functor> | <variable>
data Principal_symbol = PS_functor TPTP_functor
| PS_variable Variable
deriving (Show, Ord, Eq, Data, Typeable)
-- %----Include directives
-- <include> ::= include(<file_name><formula_selection>).
data Include = Include File_name Formula_selection
deriving (Show, Ord, Eq, Data, Typeable)
-- <formula_selection> ::= ,[<name_list>] | <null>
type Formula_selection = Maybe [Name]
-- <name_list> ::= <name> | <name>,<name_list>
type Name_list = [Name]
-- %----Non-logical data
-- <general_term> ::= <general_data> | <general_data>:<general_term> |
-- <general_list>
data General_term = GT_data General_data
| GT_DataTerm General_data General_term
| GT_list General_list
deriving (Show, Ord, Eq, Data, Typeable)
-- <general_data> ::= <atomic_word> | <general_function> |
-- <variable> | <number> | <distinct_object> |
-- <formula_data>
data General_data = GD_atomic_word Atomic_word
| GD_general_function General_function
| GD_variable Variable
| GD_number Number
| GD_distinct_object Distinct_object
| GD_formula_data Formula_data
-- %----A <general_data> bind() term is used to record a variable binding in an
-- %----inference, as an element of the <parent_details> list.
-- <general_data> :== bind(<variable>,<formula_data>)
| GD_bind Variable Formula_data -- only used in inference
deriving (Show, Ord, Eq, Data, Typeable)
-- <general_function> ::= <atomic_word>(<general_terms>)
data General_function = General_function Atomic_word General_terms
deriving (Show, Ord, Eq, Data, Typeable)
-- <formula_data> ::= $thf(<thf_formula>) | $tff(<tff_formula>) |
-- $fof(<fof_formula>) | $cnf(<cnf_formula>) |
-- $fot(<fof_term>)
-- only used in inference
data Formula_data = FD_THF THF_formula
| FD_TFF TFF_formula
| FD_FOF FOF_formula
| FD_CNF CNF_formula
| FD_FOT FOF_term
deriving (Show, Ord, Eq, Data, Typeable)
-- <general_list> ::= [] | [<general_terms>]
type General_list = [General_term]
-- <general_terms> ::= <general_term> | <general_term>,<general_terms>
type General_terms = [General_term]
-- %----General purpose
-- <name> ::= <atomic_word> | <integer>
-- %----Integer names are expected to be unsigned
data Name = NameString Token
| NameInteger Integer
deriving (Show, Ord, Eq, Data, Typeable)
-- <atomic_word> ::= <lower_word> | <single_quoted>
type Atomic_word = Token
-- <atomic_defined_word> ::= <dollar_word>
type Atomic_defined_word = Token
-- <atomic_system_word> ::= <dollar_dollar_word>
type Atomic_system_word = Token
-- <number> ::= <integer> | <rational> | <real>
data Number = NumInteger Integer
| NumRational Rational
| NumReal Double
deriving (Show, Ord, Eq, Data, Typeable)
-- <distinct_object> ::- <double_quote><do_char>*<double_quote>
type Distinct_object = Token
-- <file_name> ::= <single_quoted>
type File_name = IRI