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 (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 ((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 ((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 ((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 ((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 (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 (( 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 ))