src/HOL/TPTP/TPTP_Parser/tptp.yacc
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47360 d1ecc9cec531
child 47569 fce9d97a3258
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
open TPTP_Syntax
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
exception UNRECOGNISED_SYMBOL of string * string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
exception UNRECOGNISED_ROLE of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     6
fun classify_role role =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     7
  case role of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
    "axiom" => Role_Axiom
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
  | "hypothesis" => Role_Hypothesis
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    10
  | "definition" => Role_Definition
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
  | "assumption" => Role_Assumption
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
  | "lemma" => Role_Lemma
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
  | "theorem" => Role_Theorem
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
  | "conjecture" => Role_Conjecture
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
  | "negated_conjecture" => Role_Negated_Conjecture
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    16
  | "plain" => Role_Plain
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    17
  | "fi_domain" => Role_Fi_Domain
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    18
  | "fi_functors" => Role_Fi_Functors
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    19
  | "fi_predicates" => Role_Fi_Predicates
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
  | "type" => Role_Type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
  | "unknown" => Role_Unknown
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
  | thing => raise (UNRECOGNISED_ROLE thing)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    24
fun extract_quant_info (Quant (quantifier, vars, tptp_formula)) =
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    25
  (quantifier, vars, tptp_formula)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    26
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
%%
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
%name TPTP
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
%term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    30
  | LET | ARROW | FI | IFF | IMPLIES | INCLUDE
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
  | LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
  | NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
  | TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
  | TOK_TYPE | VLINE | EOF | DTHF | DFOF | DCNF | DFOT | DTFF | REAL of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
  | RATIONAL of string | SIGNED_INTEGER of string | UNSIGNED_INTEGER of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
  | DOT_DECIMAL of string | SINGLE_QUOTED of string | UPPER_WORD of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
  | LOWER_WORD of string | COMMENT of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
  | DISTINCT_OBJECT of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
  | DUD | INDEF_CHOICE | DEFIN_CHOICE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
  | OPERATOR_FORALL | OPERATOR_EXISTS
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
  | PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    42
  | DOLLAR_WORD of string | DOLLAR_DOLLAR_WORD of string
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
  | SUBTYPE | LET_TERM
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
  | THF | TFF | FOF | CNF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
  | ITE_F | ITE_T
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    46
  | LET_TF | LET_FF | LET_FT | LET_TT
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
    47
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
%nonterm
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
    annotations of annotation option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
  | name of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
  | name_list of string list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
  | formula_selection of string list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
  | optional_info of general_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
  | general_list of general_list | general_terms of general_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    55
  | general_term of general_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    56
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    57
  | atomic_word of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    58
  | general_data of general_data | variable_ of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    59
  | number of number_kind * string | formula_data of general_data
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    60
  | integer of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    61
  | identifier of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    62
  | general_function of general_data | useful_info of general_list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    63
  | file_name of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    64
  | functor_ of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    65
  | term of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
  | arguments of tptp_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
  | defined_functor of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
  | system_functor of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
  | system_constant of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
  | system_term of symbol * tptp_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    71
  | defined_constant of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    72
  | defined_plain_term of symbol * tptp_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    73
  | defined_atomic_term of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    74
  | defined_atom of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    75
  | defined_term of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
  | constant of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    77
  | plain_term of symbol * tptp_term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
  | function_term of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
  | conditional_term of tptp_term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
  | system_atomic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
  | infix_equality of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
  | infix_inequality of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    83
  | defined_infix_pred of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
  | defined_infix_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    85
  | defined_prop of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    86
  | defined_pred of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    87
  | defined_plain_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    88
  | defined_atomic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
  | plain_atomic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    90
  | atomic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
  | unary_connective of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
  | defined_type of tptp_base_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
  | system_type of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
  | assoc_connective of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
  | binary_connective of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
  | fol_quantifier of quantifier
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
  | thf_unary_connective of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    99
  | thf_pair_connective of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   100
  | thf_quantifier of quantifier
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   101
  | fol_infix_unary of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   102
  | thf_conn_term of symbol
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   103
  | literal of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
  | disjunction of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
  | cnf_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
  | fof_tuple_list of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
  | fof_tuple of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
  | fof_sequent of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
  | fof_unary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
  | fof_variable_list of string list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
  | fof_quantified_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
  | fof_unitary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
  | fof_and_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
  | fof_or_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
  | fof_binary_assoc of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
  | fof_binary_nonassoc of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
  | fof_binary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
  | fof_logic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
  | fof_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
  | tff_tuple of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
  | tff_tuple_list of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
  | tff_sequent of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
  | tff_conditional of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
  | tff_xprod_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
  | tff_mapping_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
  | tff_atomic_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
  | tff_unitary_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
  | tff_top_level_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
  | tff_untyped_atom of symbol * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   130
  | tff_typed_atom of symbol * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
  | tff_unary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
  | tff_typed_variable of string * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
  | tff_variable of string * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
  | tff_variable_list of (string * tptp_type option) list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
  | tff_quantified_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
  | tff_unitary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
  | tff_and_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
  | tff_or_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
  | tff_binary_assoc of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
  | tff_binary_nonassoc of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
  | tff_binary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
  | tff_logic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   143
  | tff_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
  | thf_tuple of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
  | thf_tuple_list of tptp_formula list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
  | thf_sequent of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
  | thf_conditional of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
  | thf_let of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
  | thf_atom of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   151
  | thf_union_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   152
  | thf_xprod_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   153
  | thf_mapping_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   154
  | thf_binary_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   155
  | thf_unitary_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   156
  | thf_top_level_type of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   157
  | thf_subtype of tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   158
  | thf_typeable_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   159
  | thf_type_formula of tptp_formula * tptp_type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   160
  | thf_unary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   161
  | thf_typed_variable of string * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   162
  | thf_variable of string * tptp_type option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   163
  | thf_variable_list of (string * tptp_type option) list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   164
  | thf_quantified_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   165
  | thf_unitary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   166
  | thf_apply_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   167
  | thf_and_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   168
  | thf_or_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   169
  | thf_binary_tuple of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   170
  | thf_binary_pair of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   171
  | thf_binary_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   172
  | thf_logic_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   173
  | thf_formula of tptp_formula
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   174
  | formula_role of role
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   175
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   176
  | cnf_annotated of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   177
  | fof_annotated of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   178
  | tff_annotated of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   179
  | thf_annotated of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   180
  | annotated_formula of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   181
  | include_ of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   182
  | tptp_input of tptp_line
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   183
  | tptp_file of tptp_problem
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   184
  | tptp of tptp_problem
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   185
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   186
  | thf_let_defn of tptp_let list
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   187
  | tff_let of tptp_formula
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   188
  | tff_let_term_defn of tptp_let list
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   189
  | tff_let_formula_defn of tptp_let list
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   190
  | tff_quantified_type of tptp_type
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   191
  | tff_monotype of tptp_type
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   192
  | tff_type_arguments of tptp_type list
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   193
  | let_term of tptp_term
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   194
  | atomic_defined_word of string
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   195
  | atomic_system_word of string
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   196
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   197
%pos int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   198
%eop EOF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   199
%noshift EOF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   200
%arg (file_name) : string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   201
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   202
%nonassoc LET
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   203
%nonassoc RPAREN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   204
%nonassoc DUD
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   205
%right COMMA
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   206
%left COLON
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   207
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   208
%left AT_SIGN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   209
%nonassoc IFF XOR
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   210
%right IMPLIES FI
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   211
%nonassoc EQUALS NEQUALS
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   212
%right VLINE NOR
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   213
%left AMPERSAND NAND
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   214
%right ARROW
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   215
%left PLUS
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   216
%left TIMES
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   217
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   218
%right OPERATOR_FORALL OPERATOR_EXISTS
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   219
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   220
%nonassoc EXCLAMATION QUESTION LAMBDA CARET
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   221
%nonassoc TILDE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   222
%pure
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   223
%start tptp
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   224
%verbose
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   225
%%
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   226
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   227
(*  Title:      HOL/TPTP/TPTP_Parser/tptp.yacc
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   228
    Author:     Nik Sultana, Cambridge University Computer Laboratory
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   229
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   230
 Parser for TPTP languages. Latest version of the language spec can
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   231
 be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   232
 This implements version 5.3.0.
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   233
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   234
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   235
tptp : tptp_file (( tptp_file ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   236
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   237
tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   238
          | COMMENT tptp_file    (( tptp_file ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   239
          |                      (( [] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   240
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   241
tptp_input : annotated_formula (( annotated_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   242
           | include_           (( include_ ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   243
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   244
annotated_formula : thf_annotated (( thf_annotated ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   245
                  | tff_annotated (( tff_annotated ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   246
                  | fof_annotated (( fof_annotated ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   247
                  | cnf_annotated (( cnf_annotated ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   248
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   249
thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   250
  Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   251
   THF, name, formula_role, thf_formula, annotations)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   252
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   253
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   254
tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   255
  Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   256
   TFF, name, formula_role, tff_formula, annotations)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   257
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   258
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   259
fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   260
  Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   261
   FOF, name, formula_role, fof_formula, annotations)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   262
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   263
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   264
cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   265
  Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   266
   CNF, name, formula_role, cnf_formula, annotations)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   267
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   268
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   269
annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   270
            |                                  (( NONE ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   271
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   272
formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   273
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   274
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   275
(* THF formulas *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   276
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   277
thf_formula : thf_logic_formula (( thf_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   278
            | thf_sequent       (( thf_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   279
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   280
thf_logic_formula : thf_binary_formula   (( thf_binary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   281
                  | thf_unitary_formula  (( thf_unitary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   282
                  | thf_type_formula     (( THF_typing thf_type_formula ))
47360
sultana
parents: 47358
diff changeset
   283
                  | thf_subtype          (( Type_fmla thf_subtype ))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   284
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   285
thf_binary_formula : thf_binary_pair   (( thf_binary_pair ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   286
                   | thf_binary_tuple  (( thf_binary_tuple ))
47360
sultana
parents: 47358
diff changeset
   287
                   | thf_binary_type   (( Type_fmla thf_binary_type ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   288
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   289
thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   290
  Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   291
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   292
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   293
thf_binary_tuple : thf_or_formula    (( thf_or_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   294
                 | thf_and_formula   (( thf_and_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   295
                 | thf_apply_formula (( thf_apply_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   296
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   297
thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   298
               | thf_or_formula VLINE thf_unitary_formula      (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   299
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   300
thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   301
                | thf_and_formula AMPERSAND thf_unitary_formula     (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   302
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   303
thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   304
                  | thf_apply_formula AT_SIGN thf_unitary_formula   (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   305
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   306
thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   307
                    | thf_unary_formula      (( thf_unary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   308
                    | thf_atom               (( thf_atom ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   309
                    | thf_conditional        (( thf_conditional ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   310
                    | thf_let                (( thf_let ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   311
                    | LPAREN thf_logic_formula RPAREN  (( thf_logic_formula ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   312
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   313
thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   314
  Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   315
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   316
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   317
thf_variable_list : thf_variable                          (( [thf_variable] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   318
                  | thf_variable COMMA thf_variable_list  (( thf_variable :: thf_variable_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   319
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   320
thf_variable : thf_typed_variable (( thf_typed_variable ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   321
             | variable_          (( (variable_, NONE) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   322
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   323
thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   324
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   325
thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   326
  Fmla (thf_unary_connective, [thf_logic_formula])
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   327
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   328
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   329
thf_atom : term          (( Atom (THF_Atom_term term) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   330
         | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   331
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   332
thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   333
  Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   334
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   335
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   336
thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   337
  Let (thf_let_defn, thf_formula)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   338
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   339
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   340
(*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   341
thf_let_defn : thf_quantified_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   342
  let
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   343
    val (_, vars, fmla) = extract_quant_info thf_quantified_formula
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   344
  in [Let_fmla (hd vars, fmla)]
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   345
  end
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   346
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   347
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   348
thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   349
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   350
thf_typeable_formula : thf_atom                         (( thf_atom ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   351
                     | LPAREN thf_logic_formula RPAREN  (( thf_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   352
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   353
thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   354
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   355
thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   356
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   357
thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   358
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   359
thf_binary_type : thf_mapping_type (( thf_mapping_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   360
                | thf_xprod_type   (( thf_xprod_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   361
                | thf_union_type   (( thf_union_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   362
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   363
thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   364
                 | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   365
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   366
thf_xprod_type : thf_unitary_type TIMES thf_unitary_type   (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   367
               | thf_xprod_type TIMES thf_unitary_type     (( Prod_type(thf_xprod_type, thf_unitary_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   368
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   369
thf_union_type : thf_unitary_type PLUS thf_unitary_type    (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   370
               | thf_union_type PLUS thf_unitary_type      (( Sum_type(thf_union_type, thf_unitary_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   371
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   372
thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple  (( Sequent(thf_tuple1, thf_tuple2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   373
            | LPAREN thf_sequent RPAREN          (( thf_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   374
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   375
thf_tuple : LBRKT RBRKT                (( [] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   376
          | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   377
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   378
thf_tuple_list : thf_logic_formula                      (( [thf_logic_formula] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   379
               | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   380
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   381
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   382
(* TFF Formulas *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   383
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   384
tff_formula : tff_logic_formula  (( tff_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   385
            | tff_typed_atom     (( Atom (TFF_Typed_Atom tff_typed_atom) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   386
            | tff_sequent        (( tff_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   387
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   388
tff_logic_formula : tff_binary_formula   (( tff_binary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   389
                  | tff_unitary_formula  (( tff_unitary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   390
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   391
tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   392
                   | tff_binary_assoc    (( tff_binary_assoc ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   393
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   394
tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   395
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   396
tff_binary_assoc : tff_or_formula  (( tff_or_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   397
                 | tff_and_formula (( tff_and_formula ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   398
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   399
tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula      (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   400
               | tff_or_formula VLINE tff_unitary_formula           (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   401
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   402
tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   403
                | tff_and_formula AMPERSAND tff_unitary_formula     (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   404
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   405
tff_unitary_formula : tff_quantified_formula           (( tff_quantified_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   406
                    | tff_unary_formula                (( tff_unary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   407
                    | atomic_formula                   (( atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   408
                    | tff_conditional                  (( tff_conditional ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   409
                    | tff_let                          (( tff_let ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   410
                    | LPAREN tff_logic_formula RPAREN  (( tff_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   411
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   412
tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   413
  Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   414
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   415
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   416
tff_variable_list : tff_variable                         (( [tff_variable] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   417
                  | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   418
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   419
tff_variable : tff_typed_variable (( tff_typed_variable ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   420
             | variable_          (( (variable_, NONE) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   421
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   422
tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   423
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   424
tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   425
                  | fol_infix_unary                      (( fol_infix_unary ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   426
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   427
tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   428
  Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   429
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   430
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   431
tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   432
        | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   433
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   434
(*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   435
(*FIXME why "term" if using "Let_fmla"?*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   436
tff_let_term_defn : tff_quantified_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   437
  let
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   438
    val (_, vars, fmla) = extract_quant_info tff_quantified_formula
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   439
  in [Let_fmla (hd vars, fmla)]
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   440
  end
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   441
))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   442
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   443
(*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   444
tff_let_formula_defn : tff_quantified_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   445
  let
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   446
    val (_, vars, fmla) = extract_quant_info tff_quantified_formula
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   447
  in [Let_fmla (hd vars, fmla)]
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   448
  end
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   449
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   450
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   451
tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   452
            | LPAREN tff_sequent RPAREN         (( tff_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   453
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   454
tff_tuple : LBRKT RBRKT    (( [] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   455
          | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   456
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   457
tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   458
               | tff_logic_formula                      (( [tff_logic_formula] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   459
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   460
tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   461
               | LPAREN tff_typed_atom RPAREN              (( tff_typed_atom ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   462
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   463
tff_untyped_atom : functor_       (( (functor_, NONE) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   464
                 | system_functor (( (system_functor, NONE) ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   465
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   466
tff_top_level_type : tff_atomic_type     (( tff_atomic_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   467
                   | tff_mapping_type    (( tff_mapping_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   468
                   | tff_quantified_type (( tff_quantified_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   469
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   470
tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
47360
sultana
parents: 47358
diff changeset
   471
       Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   472
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   473
                    | LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   474
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   475
tff_monotype : tff_atomic_type                (( tff_atomic_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   476
             | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   477
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   478
tff_unitary_type : tff_atomic_type               (( tff_atomic_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   479
                 | LPAREN tff_xprod_type RPAREN  (( tff_xprod_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   480
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   481
tff_atomic_type : atomic_word   (( Atom_type atomic_word ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   482
                | defined_type  (( Defined_type defined_type ))
47360
sultana
parents: 47358
diff changeset
   483
                | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   484
                | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   485
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   486
tff_type_arguments : tff_atomic_type   (( [tff_atomic_type]  ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   487
                   | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   488
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   489
tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   490
                 | LPAREN tff_mapping_type RPAREN         (( tff_mapping_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   491
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   492
tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   493
               | tff_xprod_type TIMES tff_atomic_type  (( Prod_type(tff_xprod_type, tff_atomic_type) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   494
               | LPAREN tff_xprod_type RPAREN          (( tff_xprod_type ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   495
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   496
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   497
(* FOF Formulas *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   498
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   499
fof_formula : fof_logic_formula  (( fof_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   500
            | fof_sequent        (( fof_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   501
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   502
fof_logic_formula : fof_binary_formula   (( fof_binary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   503
                  | fof_unitary_formula  (( fof_unitary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   504
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   505
fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   506
                   | fof_binary_assoc    (( fof_binary_assoc ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   507
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   508
fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   509
  Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   510
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   511
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   512
fof_binary_assoc : fof_or_formula  (( fof_or_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   513
                 | fof_and_formula (( fof_and_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   514
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   515
fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula  (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   516
               | fof_or_formula VLINE fof_unitary_formula       (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   517
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   518
fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   519
                | fof_and_formula AMPERSAND fof_unitary_formula     (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   520
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   521
fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   522
                    | fof_unary_formula      (( fof_unary_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   523
                    | atomic_formula         (( atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   524
                    | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   525
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   526
fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   527
  Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   528
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   529
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   530
fof_variable_list : variable_                          (( [variable_] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   531
                  | variable_ COMMA fof_variable_list  (( variable_ :: fof_variable_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   532
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   533
fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   534
                  | fol_infix_unary                      (( fol_infix_unary ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   535
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   536
fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   537
            | LPAREN fof_sequent RPAREN         (( fof_sequent ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   538
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   539
fof_tuple : LBRKT RBRKT                 (( [] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   540
          | LBRKT fof_tuple_list RBRKT  (( fof_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   541
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   542
fof_tuple_list : fof_logic_formula                      (( [fof_logic_formula] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   543
               | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   544
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   545
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   546
(* CNF Formulas *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   547
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   548
cnf_formula : LPAREN disjunction RPAREN  (( disjunction ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   549
            | disjunction                (( disjunction ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   550
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   551
disjunction : literal                    (( literal ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   552
            | disjunction VLINE literal  (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   553
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   554
literal : atomic_formula        (( atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   555
        | TILDE atomic_formula  (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   556
        | fol_infix_unary       (( fol_infix_unary ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   557
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   558
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   559
(* Special Formulas  *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   560
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   561
thf_conn_term : thf_pair_connective   (( thf_pair_connective ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   562
              | assoc_connective      (( assoc_connective ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   563
              | thf_unary_connective  (( thf_unary_connective ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   564
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   565
fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   566
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   567
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   568
(* Connectives - THF *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   569
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   570
thf_quantifier : fol_quantifier (( fol_quantifier ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   571
               | CARET          (( Lambda ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   572
               | DEP_PROD       (( Dep_Prod ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   573
               | DEP_SUM        (( Dep_Sum ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   574
               | INDEF_CHOICE   (( Epsilon ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   575
               | DEFIN_CHOICE   (( Iota ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   576
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   577
thf_pair_connective : infix_equality    (( infix_equality ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   578
                    | infix_inequality  (( infix_inequality ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   579
                    | binary_connective (( binary_connective ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   580
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   581
thf_unary_connective : unary_connective (( unary_connective ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   582
                     | OPERATOR_FORALL  (( Interpreted_Logic Op_Forall ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   583
                     | OPERATOR_EXISTS  (( Interpreted_Logic Op_Exists ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   584
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   585
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   586
(* Connectives - THF and TFF
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   587
instead of subtype_sign use token SUBTYPE
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   588
*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   589
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   590
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   591
(* Connectives - FOF *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   592
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   593
fol_quantifier : EXCLAMATION  (( Forall ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   594
               | QUESTION     (( Exists ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   595
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   596
binary_connective : IFF       (( Interpreted_Logic Iff ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   597
                  | IMPLIES   (( Interpreted_Logic If ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   598
                  | FI        (( Interpreted_Logic Fi ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   599
                  | XOR       (( Interpreted_Logic Xor ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   600
                  | NOR       (( Interpreted_Logic Nor ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   601
                  | NAND      (( Interpreted_Logic Nand ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   602
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   603
assoc_connective : VLINE      (( Interpreted_Logic Or ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   604
                 | AMPERSAND  (( Interpreted_Logic And ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   605
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   606
unary_connective : TILDE (( Interpreted_Logic Not ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   607
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   608
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   609
(* The sequent arrow
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   610
use token GENTZEN_ARROW
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   611
*)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   612
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   613
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   614
(* Types for THF and TFF *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   615
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   616
defined_type : atomic_defined_word ((
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   617
  case atomic_defined_word of
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   618
    "$oType" => Type_Bool
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   619
  | "$o" => Type_Bool
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   620
  | "$iType" => Type_Ind
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   621
  | "$i" => Type_Ind
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   622
  | "$tType" => Type_Type
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   623
  | "$real" => Type_Real
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   624
  | "$rat" => Type_Rat
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   625
  | "$int" => Type_Int
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   626
  | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   627
))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   628
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   629
system_type : atomic_system_word (( atomic_system_word ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   630
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   631
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   632
(* First-order atoms *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   633
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   634
atomic_formula : plain_atomic_formula   (( plain_atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   635
               | defined_atomic_formula (( defined_atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   636
               | system_atomic_formula  (( system_atomic_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   637
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   638
plain_atomic_formula : plain_term (( Pred plain_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   639
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   640
defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   641
                       | defined_infix_formula (( defined_infix_formula ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   642
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   643
defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   644
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   645
(*FIXME not used*)
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   646
defined_prop : atomic_defined_word ((
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   647
  case atomic_defined_word of
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   648
    "$true"  => "$true"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   649
  | "$false" => "$false"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   650
  | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   651
))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   652
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   653
(*FIXME not used*)
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   654
defined_pred : atomic_defined_word ((
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   655
  case atomic_defined_word of
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   656
    "$distinct"  => "$distinct"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   657
  | "$ite_f" => "$ite_f"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   658
  | "$less" => "$less"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   659
  | "$lesseq" => "$lesseq"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   660
  | "$greater" => "$greater"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   661
  | "$greatereq" => "$greatereq"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   662
  | "$is_int" => "$is_int"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   663
  | "$is_rat" => "$is_rat"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   664
  | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   665
))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   666
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   667
defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   668
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   669
defined_infix_pred : infix_equality  (( infix_equality ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   670
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   671
infix_equality : EQUALS    (( Interpreted_Logic Equals ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   672
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   673
infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   674
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   675
system_atomic_formula : system_term  (( Pred system_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   676
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   677
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   678
(* First-order terms *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   679
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   680
term : function_term     (( function_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   681
     | variable_         (( Term_Var variable_ ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   682
     | conditional_term  (( conditional_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   683
     | let_term          (( let_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   684
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   685
function_term : plain_term    (( Term_Func plain_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   686
              | defined_term  (( defined_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   687
              | system_term   (( Term_Func system_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   688
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   689
plain_term : constant                          (( (constant, []) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   690
           | functor_ LPAREN arguments RPAREN  (( (functor_, arguments) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   691
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   692
constant : functor_ (( functor_ ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   693
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   694
functor_ : atomic_word (( Uninterpreted atomic_word ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   695
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   696
defined_term : defined_atom        (( defined_atom ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   697
             | defined_atomic_term (( defined_atomic_term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   698
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   699
defined_atom : number          (( Term_Num number ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   700
             | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   701
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   702
defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   703
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   704
defined_plain_term : defined_constant                        (( (defined_constant, []) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   705
                   | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   706
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   707
defined_constant : defined_functor (( defined_functor ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   708
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   709
(*FIXME would be nicer to split these up*)
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   710
defined_functor : atomic_defined_word ((
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   711
  case atomic_defined_word of
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   712
    "$uminus" => Interpreted_ExtraLogic UMinus
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   713
  | "$sum" => Interpreted_ExtraLogic Sum
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   714
  | "$difference" => Interpreted_ExtraLogic Difference
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   715
  | "$product" => Interpreted_ExtraLogic Product
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   716
  | "$quotient" => Interpreted_ExtraLogic Quotient
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   717
  | "$quotient_e" => Interpreted_ExtraLogic Quotient_E
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   718
  | "$quotient_t" => Interpreted_ExtraLogic Quotient_T
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   719
  | "$quotient_f" => Interpreted_ExtraLogic Quotient_F
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   720
  | "$remainder_e" => Interpreted_ExtraLogic Remainder_E
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   721
  | "$remainder_t" => Interpreted_ExtraLogic Remainder_T
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   722
  | "$remainder_f" => Interpreted_ExtraLogic Remainder_F
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   723
  | "$floor" => Interpreted_ExtraLogic Floor
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   724
  | "$ceiling" => Interpreted_ExtraLogic Ceiling
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   725
  | "$truncate" => Interpreted_ExtraLogic Truncate
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   726
  | "$round" => Interpreted_ExtraLogic Round
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   727
  | "$to_int" => Interpreted_ExtraLogic To_Int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   728
  | "$to_rat" => Interpreted_ExtraLogic To_Rat
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   729
  | "$to_real" => Interpreted_ExtraLogic To_Real
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   730
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   731
  | "$i" => TypeSymbol Type_Ind
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   732
  | "$o" => TypeSymbol Type_Bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   733
  | "$iType" => TypeSymbol Type_Ind
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   734
  | "$oType" => TypeSymbol Type_Bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   735
  | "$int" => TypeSymbol Type_Int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   736
  | "$real" => TypeSymbol Type_Real
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   737
  | "$rat" => TypeSymbol Type_Rat
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   738
  | "$tType" => TypeSymbol Type_Type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   739
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   740
  | "$true" => Interpreted_Logic True
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   741
  | "$false" => Interpreted_Logic False
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   742
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   743
  | "$less" => Interpreted_ExtraLogic Less
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   744
  | "$lesseq" => Interpreted_ExtraLogic LessEq
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   745
  | "$greatereq" => Interpreted_ExtraLogic GreaterEq
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   746
  | "$greater" => Interpreted_ExtraLogic Greater
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   747
  | "$evaleq" => Interpreted_ExtraLogic EvalEq
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   748
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   749
  | "$is_int" => Interpreted_ExtraLogic Is_Int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   750
  | "$is_rat" => Interpreted_ExtraLogic Is_Rat
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   751
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   752
  | "$distinct" => Interpreted_ExtraLogic Distinct
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   753
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   754
  | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   755
))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   756
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   757
system_term : system_constant                         (( (system_constant, []) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   758
            | system_functor LPAREN arguments RPAREN  (( (system_functor, arguments) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   759
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   760
system_constant : system_functor (( system_functor ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   761
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   762
system_functor : atomic_system_word (( System atomic_system_word ))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   763
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   764
variable_ : UPPER_WORD  (( UPPER_WORD ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   765
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   766
arguments : term                  (( [term] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   767
          | term COMMA arguments  (( term :: arguments ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   768
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   769
conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   770
  Term_Conditional (tff_logic_formula, term1, term2)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   771
))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   772
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   773
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   774
let_term : LET_FT LPAREN tff_let_formula_defn COMMA term RPAREN ((Term_Let (tff_let_formula_defn, term) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   775
         | LET_TT LPAREN tff_let_term_defn COMMA term RPAREN ((Term_Let (tff_let_term_defn, term) ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   776
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   777
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   778
(* Formula sources
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   779
Don't currently use following non-terminals:
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   780
source, sources, dag_source, inference_record, inference_rule, parent_list,
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   781
parent_info, parent_details, internal_source, intro_type, external_source,
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   782
file_source, file_info, theory, theory_name, creator_source, creator_name.
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   783
*)
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   784
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   785
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   786
(* Useful info fields *)
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   787
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   788
optional_info : COMMA useful_info (( useful_info ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   789
              |                   (( [] ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   790
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   791
useful_info : general_list (( general_list ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   792
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   793
include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   794
  Include (file_name, formula_selection)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   795
))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   796
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   797
formula_selection : COMMA LBRKT name_list RBRKT   (( name_list  ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   798
                  |                               (( [] ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   799
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   800
name_list : name COMMA name_list   (( name :: name_list ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   801
          | name                   (( [name] ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   802
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   803
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   804
(* Non-logical data *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   805
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   806
general_term : general_data                    (( General_Data general_data ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   807
             | general_data COLON general_term (( General_Term (general_data, general_term) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   808
             | general_list                    (( General_List general_list ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   809
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   810
general_data : atomic_word       (( Atomic_Word atomic_word ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   811
             | general_function  (( general_function ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   812
             | variable_         (( V variable_ ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   813
             | number            (( Number number ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   814
             | DISTINCT_OBJECT   (( Distinct_Object DISTINCT_OBJECT ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   815
             | formula_data      (( formula_data ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   816
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   817
general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   818
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   819
formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   820
             | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   821
             | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   822
             | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   823
             | DFOT LPAREN term RPAREN (( Term_Data term ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   824
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   825
general_list : LBRKT general_terms RBRKT (( general_terms ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   826
             | LBRKT RBRKT               (( [] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   827
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   828
general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   829
              | general_term                     (( [general_term] ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   830
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   831
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   832
(* General purpose *)
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   833
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   834
name : atomic_word (( atomic_word ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   835
     | integer     (( integer ))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   836
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   837
atomic_word : LOWER_WORD    (( LOWER_WORD ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   838
            | SINGLE_QUOTED (( SINGLE_QUOTED ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   839
            | THF           (( "thf" ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   840
            | TFF           (( "tff" ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   841
            | FOF           (( "fof" ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   842
            | CNF           (( "cnf" ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   843
            | INCLUDE       (( "include" ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   844
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   845
atomic_defined_word : DOLLAR_WORD (( DOLLAR_WORD ))
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   846
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   847
atomic_system_word : DOLLAR_DOLLAR_WORD (( DOLLAR_DOLLAR_WORD ))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   848
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   849
integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   850
       | SIGNED_INTEGER   (( SIGNED_INTEGER ))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   851
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   852
number : integer          (( (Int_num, integer) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   853
       | REAL             (( (Real_num, REAL) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   854
       | RATIONAL         (( (Rat_num, RATIONAL) ))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   855
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   856
file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))