added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
open TPTP_Syntax
exception UNRECOGNISED_SYMBOL of string * string
exception UNRECOGNISED_ROLE of string
fun classify_role role =
case role of
"axiom" => Role_Axiom
| "hypothesis" => Role_Hypothesis
| "definition" => Role_Definition
| "assumption" => Role_Assumption
| "lemma" => Role_Lemma
| "theorem" => Role_Theorem
| "conjecture" => Role_Conjecture
| "negated_conjecture" => Role_Negated_Conjecture
| "plain" => Role_Plain
| "fi_domain" => Role_Fi_Domain
| "fi_functors" => Role_Fi_Functors
| "fi_predicates" => Role_Fi_Predicates
| "type" => Role_Type
| "unknown" => Role_Unknown
| thing => raise (UNRECOGNISED_ROLE thing)
fun extract_quant_info (Quant (quantifier, vars, tptp_formula)) =
(quantifier, vars, tptp_formula)
%%
%name TPTP
%term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
| LET | ARROW | FI | IFF | IMPLIES | INCLUDE
| LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
| NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
| TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
| TOK_TYPE | VLINE | EOF | DTHF | DFOF | DCNF | DFOT | DTFF | REAL of string
| RATIONAL of string | SIGNED_INTEGER of string | UNSIGNED_INTEGER of string
| DOT_DECIMAL of string | SINGLE_QUOTED of string | UPPER_WORD of string
| LOWER_WORD of string | COMMENT of string
| DISTINCT_OBJECT of string
| DUD | INDEF_CHOICE | DEFIN_CHOICE
| OPERATOR_FORALL | OPERATOR_EXISTS
| PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
| DOLLAR_WORD of string | DOLLAR_DOLLAR_WORD of string
| SUBTYPE | LET_TERM
| THF | TFF | FOF | CNF
| ITE_F | ITE_T
| LET_TF | LET_FF | LET_FT | LET_TT
%nonterm
annotations of annotation option
| name of string
| name_list of string list
| formula_selection of string list
| optional_info of general_term list
| general_list of general_list | general_terms of general_term list
| general_term of general_term
| atomic_word of string
| general_data of general_data | variable_ of string
| number of number_kind * string | formula_data of general_data
| integer of string
| identifier of string
| general_function of general_data | useful_info of general_list
| file_name of string
| functor_ of symbol
| term of tptp_term
| arguments of tptp_term list
| defined_functor of symbol
| system_functor of symbol
| system_constant of symbol
| system_term of symbol * tptp_term list
| defined_constant of symbol
| defined_plain_term of symbol * tptp_term list
| defined_atomic_term of tptp_term
| defined_atom of tptp_term
| defined_term of tptp_term
| constant of symbol
| plain_term of symbol * tptp_term list
| function_term of tptp_term
| conditional_term of tptp_term
| system_atomic_formula of tptp_formula
| infix_equality of symbol
| infix_inequality of symbol
| defined_infix_pred of symbol
| defined_infix_formula of tptp_formula
| defined_prop of string
| defined_pred of string
| defined_plain_formula of tptp_formula
| defined_atomic_formula of tptp_formula
| plain_atomic_formula of tptp_formula
| atomic_formula of tptp_formula
| unary_connective of symbol
| defined_type of tptp_base_type
| system_type of string
| assoc_connective of symbol
| binary_connective of symbol
| fol_quantifier of quantifier
| thf_unary_connective of symbol
| thf_pair_connective of symbol
| thf_quantifier of quantifier
| fol_infix_unary of tptp_formula
| thf_conn_term of symbol
| literal of tptp_formula
| disjunction of tptp_formula
| cnf_formula of tptp_formula
| fof_tuple_list of tptp_formula list
| fof_tuple of tptp_formula list
| fof_sequent of tptp_formula
| fof_unary_formula of tptp_formula
| fof_variable_list of string list
| fof_quantified_formula of tptp_formula
| fof_unitary_formula of tptp_formula
| fof_and_formula of tptp_formula
| fof_or_formula of tptp_formula
| fof_binary_assoc of tptp_formula
| fof_binary_nonassoc of tptp_formula
| fof_binary_formula of tptp_formula
| fof_logic_formula of tptp_formula
| fof_formula of tptp_formula
| tff_tuple of tptp_formula list
| tff_tuple_list of tptp_formula list
| tff_sequent of tptp_formula
| tff_conditional of tptp_formula
| tff_xprod_type of tptp_type
| tff_mapping_type of tptp_type
| tff_atomic_type of tptp_type
| tff_unitary_type of tptp_type
| tff_top_level_type of tptp_type
| tff_untyped_atom of symbol * tptp_type option
| tff_typed_atom of symbol * tptp_type option
| tff_unary_formula of tptp_formula
| tff_typed_variable of string * tptp_type option
| tff_variable of string * tptp_type option
| tff_variable_list of (string * tptp_type option) list
| tff_quantified_formula of tptp_formula
| tff_unitary_formula of tptp_formula
| tff_and_formula of tptp_formula
| tff_or_formula of tptp_formula
| tff_binary_assoc of tptp_formula
| tff_binary_nonassoc of tptp_formula
| tff_binary_formula of tptp_formula
| tff_logic_formula of tptp_formula
| tff_formula of tptp_formula
| thf_tuple of tptp_formula list
| thf_tuple_list of tptp_formula list
| thf_sequent of tptp_formula
| thf_conditional of tptp_formula
| thf_let of tptp_formula
| thf_atom of tptp_formula
| thf_union_type of tptp_type
| thf_xprod_type of tptp_type
| thf_mapping_type of tptp_type
| thf_binary_type of tptp_type
| thf_unitary_type of tptp_type
| thf_top_level_type of tptp_type
| thf_subtype of tptp_type
| thf_typeable_formula of tptp_formula
| thf_type_formula of tptp_formula * tptp_type
| thf_unary_formula of tptp_formula
| thf_typed_variable of string * tptp_type option
| thf_variable of string * tptp_type option
| thf_variable_list of (string * tptp_type option) list
| thf_quantified_formula of tptp_formula
| thf_unitary_formula of tptp_formula
| thf_apply_formula of tptp_formula
| thf_and_formula of tptp_formula
| thf_or_formula of tptp_formula
| thf_binary_tuple of tptp_formula
| thf_binary_pair of tptp_formula
| thf_binary_formula of tptp_formula
| thf_logic_formula of tptp_formula
| thf_formula of tptp_formula
| formula_role of role
| cnf_annotated of tptp_line
| fof_annotated of tptp_line
| tff_annotated of tptp_line
| thf_annotated of tptp_line
| annotated_formula of tptp_line
| include_ of tptp_line
| tptp_input of tptp_line
| tptp_file of tptp_problem
| tptp of tptp_problem
| thf_let_defn of tptp_let list
| tff_let of tptp_formula
| tff_let_term_defn of tptp_let list
| tff_let_formula_defn of tptp_let list
| tff_quantified_type of tptp_type
| tff_monotype of tptp_type
| tff_type_arguments of tptp_type list
| let_term of tptp_term
| atomic_defined_word of string
| atomic_system_word of string
%pos int
%eop EOF
%noshift EOF
%arg (this_file_name) : string
%nonassoc LET
%nonassoc RPAREN
%nonassoc DUD
%right COMMA
%left COLON
%left AT_SIGN
%nonassoc IFF XOR
%right IMPLIES FI
%nonassoc EQUALS NEQUALS
%right VLINE NOR
%left AMPERSAND NAND
%right ARROW
%left PLUS
%left TIMES
%right OPERATOR_FORALL OPERATOR_EXISTS
%nonassoc EXCLAMATION QUESTION LAMBDA CARET
%nonassoc TILDE
%pure
%start tptp
%verbose
%%
(* Title: HOL/TPTP/TPTP_Parser/tptp.yacc
Author: Nik Sultana, Cambridge University Computer Laboratory
Parser for TPTP languages. Latest version of the language spec can
be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
This implements version 5.3.0.
*)
tptp : tptp_file (( tptp_file ))
tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
| COMMENT tptp_file (( tptp_file ))
| (( [] ))
tptp_input : annotated_formula (( annotated_formula ))
| include_ (( include_ ))
annotated_formula : thf_annotated (( thf_annotated ))
| tff_annotated (( tff_annotated ))
| fof_annotated (( fof_annotated ))
| cnf_annotated (( cnf_annotated ))
thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
THF, name, formula_role, thf_formula, annotations)
))
tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
TFF, name, formula_role, tff_formula, annotations)
))
fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
FOF, name, formula_role, fof_formula, annotations)
))
cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
CNF, name, formula_role, cnf_formula, annotations)
))
annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
| (( NONE ))
formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
(* THF formulas *)
thf_formula : thf_logic_formula (( thf_logic_formula ))
| thf_sequent (( thf_sequent ))
thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
| thf_unitary_formula (( thf_unitary_formula ))
| thf_type_formula (( THF_typing thf_type_formula ))
| thf_subtype (( Type_fmla thf_subtype ))
thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
| thf_binary_tuple (( thf_binary_tuple ))
| thf_binary_type (( Type_fmla thf_binary_type ))
thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
))
thf_binary_tuple : thf_or_formula (( thf_or_formula ))
| thf_and_formula (( thf_and_formula ))
| thf_apply_formula (( thf_apply_formula ))
thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
| thf_or_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
| thf_and_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
| thf_apply_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
| thf_unary_formula (( thf_unary_formula ))
| thf_atom (( thf_atom ))
| thf_conditional (( thf_conditional ))
| thf_let (( thf_let ))
| LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
))
thf_variable_list : thf_variable (( [thf_variable] ))
| thf_variable COMMA thf_variable_list (( thf_variable :: thf_variable_list ))
thf_variable : thf_typed_variable (( thf_typed_variable ))
| variable_ (( (variable_, NONE) ))
thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
Fmla (thf_unary_connective, [thf_logic_formula])
))
thf_atom : term (( Atom (THF_Atom_term term) ))
| thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
))
thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN ((
Let (thf_let_defn, thf_formula)
))
(*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*)
thf_let_defn : thf_quantified_formula ((
let
val (_, vars, fmla) = extract_quant_info thf_quantified_formula
in [Let_fmla (hd vars, fmla)]
end
))
thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
thf_typeable_formula : thf_atom (( thf_atom ))
| LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
thf_binary_type : thf_mapping_type (( thf_mapping_type ))
| thf_xprod_type (( thf_xprod_type ))
| thf_union_type (( thf_union_type ))
thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
| thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
thf_xprod_type : thf_unitary_type TIMES thf_unitary_type (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
| thf_xprod_type TIMES thf_unitary_type (( Prod_type(thf_xprod_type, thf_unitary_type) ))
thf_union_type : thf_unitary_type PLUS thf_unitary_type (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
| thf_union_type PLUS thf_unitary_type (( Sum_type(thf_union_type, thf_unitary_type) ))
thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple (( Sequent(thf_tuple1, thf_tuple2) ))
| LPAREN thf_sequent RPAREN (( thf_sequent ))
thf_tuple : LBRKT RBRKT (( [] ))
| LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
thf_tuple_list : thf_logic_formula (( [thf_logic_formula] ))
| thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
(* TFF Formulas *)
tff_formula : tff_logic_formula (( tff_logic_formula ))
| tff_typed_atom (( Atom (TFF_Typed_Atom tff_typed_atom) ))
| tff_sequent (( tff_sequent ))
tff_logic_formula : tff_binary_formula (( tff_binary_formula ))
| tff_unitary_formula (( tff_unitary_formula ))
tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
| tff_binary_assoc (( tff_binary_assoc ))
tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
tff_binary_assoc : tff_or_formula (( tff_or_formula ))
| tff_and_formula (( tff_and_formula ))
tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
| tff_or_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
| tff_and_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
tff_unitary_formula : tff_quantified_formula (( tff_quantified_formula ))
| tff_unary_formula (( tff_unary_formula ))
| atomic_formula (( atomic_formula ))
| tff_conditional (( tff_conditional ))
| tff_let (( tff_let ))
| LPAREN tff_logic_formula RPAREN (( tff_logic_formula ))
tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
))
tff_variable_list : tff_variable (( [tff_variable] ))
| tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
tff_variable : tff_typed_variable (( tff_typed_variable ))
| variable_ (( (variable_, NONE) ))
tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
| fol_infix_unary (( fol_infix_unary ))
tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
))
tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
| LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))
(*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*)
(*FIXME why "term" if using "Let_fmla"?*)
tff_let_term_defn : tff_quantified_formula ((
let
val (_, vars, fmla) = extract_quant_info tff_quantified_formula
in [Let_fmla (hd vars, fmla)]
end
))
(*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*)
tff_let_formula_defn : tff_quantified_formula ((
let
val (_, vars, fmla) = extract_quant_info tff_quantified_formula
in [Let_fmla (hd vars, fmla)]
end
))
tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
| LPAREN tff_sequent RPAREN (( tff_sequent ))
tff_tuple : LBRKT RBRKT (( [] ))
| LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
| tff_logic_formula (( [tff_logic_formula] ))
tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
| LPAREN tff_typed_atom RPAREN (( tff_typed_atom ))
tff_untyped_atom : functor_ (( (functor_, NONE) ))
| system_functor (( (system_functor, NONE) ))
tff_top_level_type : tff_atomic_type (( tff_atomic_type ))
| tff_mapping_type (( tff_mapping_type ))
| tff_quantified_type (( tff_quantified_type ))
tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
))
| LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
tff_monotype : tff_atomic_type (( tff_atomic_type ))
| LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
| LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
tff_atomic_type : atomic_word (( Atom_type atomic_word ))
| defined_type (( Defined_type defined_type ))
| atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
| variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
tff_type_arguments : tff_atomic_type (( [tff_atomic_type] ))
| tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments ))
tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
| LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
| tff_xprod_type TIMES tff_atomic_type (( Prod_type(tff_xprod_type, tff_atomic_type) ))
| LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
(* FOF Formulas *)
fof_formula : fof_logic_formula (( fof_logic_formula ))
| fof_sequent (( fof_sequent ))
fof_logic_formula : fof_binary_formula (( fof_binary_formula ))
| fof_unitary_formula (( fof_unitary_formula ))
fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
| fof_binary_assoc (( fof_binary_assoc ))
fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
))
fof_binary_assoc : fof_or_formula (( fof_or_formula ))
| fof_and_formula (( fof_and_formula ))
fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
| fof_or_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
| fof_and_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
| fof_unary_formula (( fof_unary_formula ))
| atomic_formula (( atomic_formula ))
| LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
))
fof_variable_list : variable_ (( [variable_] ))
| variable_ COMMA fof_variable_list (( variable_ :: fof_variable_list ))
fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
| fol_infix_unary (( fol_infix_unary ))
fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
| LPAREN fof_sequent RPAREN (( fof_sequent ))
fof_tuple : LBRKT RBRKT (( [] ))
| LBRKT fof_tuple_list RBRKT (( fof_tuple_list ))
fof_tuple_list : fof_logic_formula (( [fof_logic_formula] ))
| fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
(* CNF Formulas *)
cnf_formula : LPAREN disjunction RPAREN (( disjunction ))
| disjunction (( disjunction ))
disjunction : literal (( literal ))
| disjunction VLINE literal (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
literal : atomic_formula (( atomic_formula ))
| TILDE atomic_formula (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
| fol_infix_unary (( fol_infix_unary ))
(* Special Formulas *)
thf_conn_term : thf_pair_connective (( thf_pair_connective ))
| assoc_connective (( assoc_connective ))
| thf_unary_connective (( thf_unary_connective ))
fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
(* Connectives - THF *)
thf_quantifier : fol_quantifier (( fol_quantifier ))
| CARET (( Lambda ))
| DEP_PROD (( Dep_Prod ))
| DEP_SUM (( Dep_Sum ))
| INDEF_CHOICE (( Epsilon ))
| DEFIN_CHOICE (( Iota ))
thf_pair_connective : infix_equality (( infix_equality ))
| infix_inequality (( infix_inequality ))
| binary_connective (( binary_connective ))
thf_unary_connective : unary_connective (( unary_connective ))
| OPERATOR_FORALL (( Interpreted_Logic Op_Forall ))
| OPERATOR_EXISTS (( Interpreted_Logic Op_Exists ))
(* Connectives - THF and TFF
instead of subtype_sign use token SUBTYPE
*)
(* Connectives - FOF *)
fol_quantifier : EXCLAMATION (( Forall ))
| QUESTION (( Exists ))
binary_connective : IFF (( Interpreted_Logic Iff ))
| IMPLIES (( Interpreted_Logic If ))
| FI (( Interpreted_Logic Fi ))
| XOR (( Interpreted_Logic Xor ))
| NOR (( Interpreted_Logic Nor ))
| NAND (( Interpreted_Logic Nand ))
assoc_connective : VLINE (( Interpreted_Logic Or ))
| AMPERSAND (( Interpreted_Logic And ))
unary_connective : TILDE (( Interpreted_Logic Not ))
(* The sequent arrow
use token GENTZEN_ARROW
*)
(* Types for THF and TFF *)
defined_type : atomic_defined_word ((
case atomic_defined_word of
"$oType" => Type_Bool
| "$o" => Type_Bool
| "$iType" => Type_Ind
| "$i" => Type_Ind
| "$tType" => Type_Type
| "$real" => Type_Real
| "$rat" => Type_Rat
| "$int" => Type_Int
| thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
))
system_type : atomic_system_word (( atomic_system_word ))
(* First-order atoms *)
atomic_formula : plain_atomic_formula (( plain_atomic_formula ))
| defined_atomic_formula (( defined_atomic_formula ))
| system_atomic_formula (( system_atomic_formula ))
plain_atomic_formula : plain_term (( Pred plain_term ))
defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
| defined_infix_formula (( defined_infix_formula ))
defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
(*FIXME not used*)
defined_prop : atomic_defined_word ((
case atomic_defined_word of
"$true" => "$true"
| "$false" => "$false"
| thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
))
(*FIXME not used*)
defined_pred : atomic_defined_word ((
case atomic_defined_word of
"$distinct" => "$distinct"
| "$ite_f" => "$ite_f"
| "$less" => "$less"
| "$lesseq" => "$lesseq"
| "$greater" => "$greater"
| "$greatereq" => "$greatereq"
| "$is_int" => "$is_int"
| "$is_rat" => "$is_rat"
| thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
))
defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
defined_infix_pred : infix_equality (( infix_equality ))
infix_equality : EQUALS (( Interpreted_Logic Equals ))
infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
system_atomic_formula : system_term (( Pred system_term ))
(* First-order terms *)
term : function_term (( function_term ))
| variable_ (( Term_Var variable_ ))
| conditional_term (( conditional_term ))
| let_term (( let_term ))
function_term : plain_term (( Term_Func plain_term ))
| defined_term (( defined_term ))
| system_term (( Term_Func system_term ))
plain_term : constant (( (constant, []) ))
| functor_ LPAREN arguments RPAREN (( (functor_, arguments) ))
constant : functor_ (( functor_ ))
functor_ : atomic_word (( Uninterpreted atomic_word ))
defined_term : defined_atom (( defined_atom ))
| defined_atomic_term (( defined_atomic_term ))
defined_atom : number (( Term_Num number ))
| DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
defined_plain_term : defined_constant (( (defined_constant, []) ))
| defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
defined_constant : defined_functor (( defined_functor ))
(*FIXME would be nicer to split these up*)
defined_functor : atomic_defined_word ((
case atomic_defined_word of
"$uminus" => Interpreted_ExtraLogic UMinus
| "$sum" => Interpreted_ExtraLogic Sum
| "$difference" => Interpreted_ExtraLogic Difference
| "$product" => Interpreted_ExtraLogic Product
| "$quotient" => Interpreted_ExtraLogic Quotient
| "$quotient_e" => Interpreted_ExtraLogic Quotient_E
| "$quotient_t" => Interpreted_ExtraLogic Quotient_T
| "$quotient_f" => Interpreted_ExtraLogic Quotient_F
| "$remainder_e" => Interpreted_ExtraLogic Remainder_E
| "$remainder_t" => Interpreted_ExtraLogic Remainder_T
| "$remainder_f" => Interpreted_ExtraLogic Remainder_F
| "$floor" => Interpreted_ExtraLogic Floor
| "$ceiling" => Interpreted_ExtraLogic Ceiling
| "$truncate" => Interpreted_ExtraLogic Truncate
| "$round" => Interpreted_ExtraLogic Round
| "$to_int" => Interpreted_ExtraLogic To_Int
| "$to_rat" => Interpreted_ExtraLogic To_Rat
| "$to_real" => Interpreted_ExtraLogic To_Real
| "$i" => TypeSymbol Type_Ind
| "$o" => TypeSymbol Type_Bool
| "$iType" => TypeSymbol Type_Ind
| "$oType" => TypeSymbol Type_Bool
| "$int" => TypeSymbol Type_Int
| "$real" => TypeSymbol Type_Real
| "$rat" => TypeSymbol Type_Rat
| "$tType" => TypeSymbol Type_Type
| "$true" => Interpreted_Logic True
| "$false" => Interpreted_Logic False
| "$less" => Interpreted_ExtraLogic Less
| "$lesseq" => Interpreted_ExtraLogic LessEq
| "$greatereq" => Interpreted_ExtraLogic GreaterEq
| "$greater" => Interpreted_ExtraLogic Greater
| "$evaleq" => Interpreted_ExtraLogic EvalEq
| "$is_int" => Interpreted_ExtraLogic Is_Int
| "$is_rat" => Interpreted_ExtraLogic Is_Rat
| "$distinct" => Interpreted_ExtraLogic Distinct
| thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
))
system_term : system_constant (( (system_constant, []) ))
| system_functor LPAREN arguments RPAREN (( (system_functor, arguments) ))
system_constant : system_functor (( system_functor ))
system_functor : atomic_system_word (( System atomic_system_word ))
variable_ : UPPER_WORD (( UPPER_WORD ))
arguments : term (( [term] ))
| term COMMA arguments (( term :: arguments ))
conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
Term_Conditional (tff_logic_formula, term1, term2)
))
let_term : LET_FT LPAREN tff_let_formula_defn COMMA term RPAREN ((Term_Let (tff_let_formula_defn, term) ))
| LET_TT LPAREN tff_let_term_defn COMMA term RPAREN ((Term_Let (tff_let_term_defn, term) ))
(* Formula sources
Don't currently use following non-terminals:
source, sources, dag_source, inference_record, inference_rule, parent_list,
parent_info, parent_details, internal_source, intro_type, external_source,
file_source, file_info, theory, theory_name, creator_source, creator_name.
*)
(* Useful info fields *)
optional_info : COMMA useful_info (( useful_info ))
| (( [] ))
useful_info : general_list (( general_list ))
include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
file_name, formula_selection)
))
formula_selection : COMMA LBRKT name_list RBRKT (( name_list ))
| (( [] ))
name_list : name COMMA name_list (( name :: name_list ))
| name (( [name] ))
(* Non-logical data *)
general_term : general_data (( General_Data general_data ))
| general_data COLON general_term (( General_Term (general_data, general_term) ))
| general_list (( General_List general_list ))
general_data : atomic_word (( Atomic_Word atomic_word ))
| general_function (( general_function ))
| variable_ (( V variable_ ))
| number (( Number number ))
| DISTINCT_OBJECT (( Distinct_Object DISTINCT_OBJECT ))
| formula_data (( formula_data ))
general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
| DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
| DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
| DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
| DFOT LPAREN term RPAREN (( Term_Data term ))
general_list : LBRKT general_terms RBRKT (( general_terms ))
| LBRKT RBRKT (( [] ))
general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
| general_term (( [general_term] ))
(* General purpose *)
name : atomic_word (( atomic_word ))
| integer (( integer ))
atomic_word : LOWER_WORD (( LOWER_WORD ))
| SINGLE_QUOTED (( dequote SINGLE_QUOTED ))
| THF (( "thf" ))
| TFF (( "tff" ))
| FOF (( "fof" ))
| CNF (( "cnf" ))
| INCLUDE (( "include" ))
atomic_defined_word : DOLLAR_WORD (( DOLLAR_WORD ))
atomic_system_word : DOLLAR_DOLLAR_WORD (( DOLLAR_DOLLAR_WORD ))
integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
| SIGNED_INTEGER (( SIGNED_INTEGER ))
number : integer (( (Int_num, integer) ))
| REAL (( (Real_num, REAL) ))
| RATIONAL (( (Rat_num, RATIONAL) ))
file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))