3 exception UNRECOGNISED_SYMBOL of string * string
5 exception UNRECOGNISED_ROLE of string
6 fun classify_role role =
9 | "hypothesis" => Role_Hypothesis
10 | "definition" => Role_Definition
11 | "assumption" => Role_Assumption
12 | "lemma" => Role_Lemma
13 | "theorem" => Role_Theorem
14 | "conjecture" => Role_Conjecture
15 | "negated_conjecture" => Role_Negated_Conjecture
16 | "plain" => Role_Plain
17 | "fi_domain" => Role_Fi_Domain
18 | "fi_functors" => Role_Fi_Functors
19 | "fi_predicates" => Role_Fi_Predicates
21 | "unknown" => Role_Unknown
22 | thing => raise (UNRECOGNISED_ROLE thing)
24 fun extract_quant_info (Quant (quantifier, vars, tptp_formula)) =
25 (quantifier, vars, tptp_formula)
29 %term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
30 | LET | ARROW | FI | IFF | IMPLIES | INCLUDE
31 | LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
32 | NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
33 | TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
34 | TOK_TYPE | VLINE | EOF | DTHF | DFOF | DCNF | DFOT | DTFF | REAL of string
35 | RATIONAL of string | SIGNED_INTEGER of string | UNSIGNED_INTEGER of string
36 | DOT_DECIMAL of string | SINGLE_QUOTED of string | UPPER_WORD of string
37 | LOWER_WORD of string | COMMENT of string
38 | DISTINCT_OBJECT of string
39 | DUD | INDEF_CHOICE | DEFIN_CHOICE
40 | OPERATOR_FORALL | OPERATOR_EXISTS
41 | PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
42 | ATOMIC_DEFINED_WORD of string | ATOMIC_SYSTEM_WORD of string
44 | THF | TFF | FOF | CNF
46 | LET_TF | LET_FF | LET_FT | LET_TT
49 annotations of annotation option
51 | name_list of string list
52 | formula_selection of string list
53 | optional_info of general_term list
54 | general_list of general_list | general_terms of general_term list
55 | general_term of general_term
57 | atomic_word of string
58 | general_data of general_data | variable_ of string
59 | number of number_kind * string | formula_data of general_data
61 | identifier of string
62 | general_function of general_data | useful_info of general_list
66 | arguments of tptp_term list
67 | defined_functor of symbol
68 | system_functor of symbol
69 | system_constant of symbol
70 | system_term of symbol * tptp_term list
71 | defined_constant of symbol
72 | defined_plain_term of symbol * tptp_term list
73 | defined_atomic_term of tptp_term
74 | defined_atom of tptp_term
75 | defined_term of tptp_term
77 | plain_term of symbol * tptp_term list
78 | function_term of tptp_term
79 | conditional_term of tptp_term
80 | system_atomic_formula of tptp_formula
81 | infix_equality of symbol
82 | infix_inequality of symbol
83 | defined_infix_pred of symbol
84 | defined_infix_formula of tptp_formula
85 | defined_prop of string
86 | defined_pred of string
87 | defined_plain_formula of tptp_formula
88 | defined_atomic_formula of tptp_formula
89 | plain_atomic_formula of tptp_formula
90 | atomic_formula of tptp_formula
91 | unary_connective of symbol
93 | defined_type of tptp_base_type
94 | system_type of string
95 | assoc_connective of symbol
96 | binary_connective of symbol
97 | fol_quantifier of quantifier
98 | thf_unary_connective of symbol
99 | thf_pair_connective of symbol
100 | thf_quantifier of quantifier
101 | fol_infix_unary of tptp_formula
102 | thf_conn_term of symbol
103 | literal of tptp_formula
104 | disjunction of tptp_formula
105 | cnf_formula of tptp_formula
106 | fof_tuple_list of tptp_formula list
107 | fof_tuple of tptp_formula list
108 | fof_sequent of tptp_formula
109 | fof_unary_formula of tptp_formula
110 | fof_variable_list of string list
111 | fof_quantified_formula of tptp_formula
112 | fof_unitary_formula of tptp_formula
113 | fof_and_formula of tptp_formula
114 | fof_or_formula of tptp_formula
115 | fof_binary_assoc of tptp_formula
116 | fof_binary_nonassoc of tptp_formula
117 | fof_binary_formula of tptp_formula
118 | fof_logic_formula of tptp_formula
119 | fof_formula of tptp_formula
120 | tff_tuple of tptp_formula list
121 | tff_tuple_list of tptp_formula list
122 | tff_sequent of tptp_formula
123 | tff_conditional of tptp_formula
124 | tff_xprod_type of tptp_type
125 | tff_mapping_type of tptp_type
126 | tff_atomic_type of tptp_type
127 | tff_unitary_type of tptp_type
128 | tff_top_level_type of tptp_type
129 | tff_untyped_atom of symbol * tptp_type option
130 | tff_typed_atom of symbol * tptp_type option
131 | tff_unary_formula of tptp_formula
132 | tff_typed_variable of string * tptp_type option
133 | tff_variable of string * tptp_type option
134 | tff_variable_list of (string * tptp_type option) list
135 | tff_quantified_formula of tptp_formula
136 | tff_unitary_formula of tptp_formula
137 | tff_and_formula of tptp_formula
138 | tff_or_formula of tptp_formula
139 | tff_binary_assoc of tptp_formula
140 | tff_binary_nonassoc of tptp_formula
141 | tff_binary_formula of tptp_formula
142 | tff_logic_formula of tptp_formula
143 | tff_formula of tptp_formula
145 | thf_tuple of tptp_formula list
146 | thf_tuple_list of tptp_formula list
147 | thf_sequent of tptp_formula
148 | thf_conditional of tptp_formula
149 | thf_let of tptp_formula
150 | thf_atom of tptp_formula
151 | thf_union_type of tptp_type
152 | thf_xprod_type of tptp_type
153 | thf_mapping_type of tptp_type
154 | thf_binary_type of tptp_type
155 | thf_unitary_type of tptp_type
156 | thf_top_level_type of tptp_type
157 | thf_subtype of tptp_type
158 | thf_typeable_formula of tptp_formula
159 | thf_type_formula of tptp_formula * tptp_type
160 | thf_unary_formula of tptp_formula
161 | thf_typed_variable of string * tptp_type option
162 | thf_variable of string * tptp_type option
163 | thf_variable_list of (string * tptp_type option) list
164 | thf_quantified_formula of tptp_formula
165 | thf_unitary_formula of tptp_formula
166 | thf_apply_formula of tptp_formula
167 | thf_and_formula of tptp_formula
168 | thf_or_formula of tptp_formula
169 | thf_binary_tuple of tptp_formula
170 | thf_binary_pair of tptp_formula
171 | thf_binary_formula of tptp_formula
172 | thf_logic_formula of tptp_formula
173 | thf_formula of tptp_formula
174 | formula_role of role
176 | cnf_annotated of tptp_line
177 | fof_annotated of tptp_line
178 | tff_annotated of tptp_line
179 | thf_annotated of tptp_line
180 | annotated_formula of tptp_line
181 | include_ of tptp_line
182 | tptp_input of tptp_line
183 | tptp_file of tptp_problem
184 | tptp of tptp_problem
186 | thf_let_defn of tptp_let list
187 | tff_let of tptp_formula
188 | tff_let_term_defn of tptp_let list
189 | tff_let_formula_defn of tptp_let list
190 | tff_quantified_type of tptp_type
191 | tff_monotype of tptp_type
192 | tff_type_arguments of tptp_type list
193 | let_term of tptp_term
198 %arg (file_name) : string
209 %nonassoc EQUALS NEQUALS
216 %right OPERATOR_FORALL OPERATOR_EXISTS
218 %nonassoc EXCLAMATION QUESTION LAMBDA CARET
225 (* Title: HOL/TPTP/TPTP_Parser/tptp.yacc
226 Author: Nik Sultana, Cambridge University Computer Laboratory
228 Parser for TPTP languages. Latest version of the language spec can
229 be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
230 This implements version 5.3.0.
233 tptp : tptp_file (( tptp_file ))
235 tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
236 | COMMENT tptp_file (( tptp_file ))
239 tptp_input : annotated_formula (( annotated_formula ))
240 | include_ (( include_ ))
242 annotated_formula : thf_annotated (( thf_annotated ))
243 | tff_annotated (( tff_annotated ))
244 | fof_annotated (( fof_annotated ))
245 | cnf_annotated (( cnf_annotated ))
247 thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
248 Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
249 THF, name, formula_role, thf_formula, annotations)
252 tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
253 Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
254 TFF, name, formula_role, tff_formula, annotations)
257 fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
258 Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
259 FOF, name, formula_role, fof_formula, annotations)
262 cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
263 Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
264 CNF, name, formula_role, cnf_formula, annotations)
267 annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
270 formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
275 thf_formula : thf_logic_formula (( thf_logic_formula ))
276 | thf_sequent (( thf_sequent ))
278 thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
279 | thf_unitary_formula (( thf_unitary_formula ))
280 | thf_type_formula (( THF_typing thf_type_formula ))
281 | thf_subtype (( THF_type thf_subtype ))
283 thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
284 | thf_binary_tuple (( thf_binary_tuple ))
285 | thf_binary_type (( THF_type thf_binary_type ))
287 thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
288 Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
291 thf_binary_tuple : thf_or_formula (( thf_or_formula ))
292 | thf_and_formula (( thf_and_formula ))
293 | thf_apply_formula (( thf_apply_formula ))
295 thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
296 | thf_or_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
298 thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
299 | thf_and_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
301 thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
302 | thf_apply_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
304 thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
305 | thf_unary_formula (( thf_unary_formula ))
306 | thf_atom (( thf_atom ))
307 | thf_conditional (( thf_conditional ))
308 | thf_let (( thf_let ))
309 | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
311 thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
312 Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
315 thf_variable_list : thf_variable (( [thf_variable] ))
316 | thf_variable COMMA thf_variable_list (( thf_variable :: thf_variable_list ))
318 thf_variable : thf_typed_variable (( thf_typed_variable ))
319 | variable_ (( (variable_, NONE) ))
321 thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
323 thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
324 Fmla (thf_unary_connective, [thf_logic_formula])
327 thf_atom : term (( Atom (THF_Atom_term term) ))
328 | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
330 thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
331 Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
334 thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN ((
335 Let (thf_let_defn, thf_formula)
338 (*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*)
339 thf_let_defn : thf_quantified_formula ((
341 val (_, vars, fmla) = extract_quant_info thf_quantified_formula
342 in [Let_fmla (hd vars, fmla)]
346 thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
348 thf_typeable_formula : thf_atom (( thf_atom ))
349 | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
351 thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
353 thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
355 thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
357 thf_binary_type : thf_mapping_type (( thf_mapping_type ))
358 | thf_xprod_type (( thf_xprod_type ))
359 | thf_union_type (( thf_union_type ))
361 thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
362 | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
364 thf_xprod_type : thf_unitary_type TIMES thf_unitary_type (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
365 | thf_xprod_type TIMES thf_unitary_type (( Prod_type(thf_xprod_type, thf_unitary_type) ))
367 thf_union_type : thf_unitary_type PLUS thf_unitary_type (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
368 | thf_union_type PLUS thf_unitary_type (( Sum_type(thf_union_type, thf_unitary_type) ))
370 thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple (( Sequent(thf_tuple1, thf_tuple2) ))
371 | LPAREN thf_sequent RPAREN (( thf_sequent ))
373 thf_tuple : LBRKT RBRKT (( [] ))
374 | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
376 thf_tuple_list : thf_logic_formula (( [thf_logic_formula] ))
377 | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
382 tff_formula : tff_logic_formula (( tff_logic_formula ))
383 | tff_typed_atom (( Atom (TFF_Typed_Atom tff_typed_atom) ))
384 | tff_sequent (( tff_sequent ))
386 tff_logic_formula : tff_binary_formula (( tff_binary_formula ))
387 | tff_unitary_formula (( tff_unitary_formula ))
389 tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
390 | tff_binary_assoc (( tff_binary_assoc ))
392 tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
394 tff_binary_assoc : tff_or_formula (( tff_or_formula ))
395 | tff_and_formula (( tff_and_formula ))
397 tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
398 | tff_or_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
400 tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
401 | tff_and_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
403 tff_unitary_formula : tff_quantified_formula (( tff_quantified_formula ))
404 | tff_unary_formula (( tff_unary_formula ))
405 | atomic_formula (( atomic_formula ))
406 | tff_conditional (( tff_conditional ))
407 | tff_let (( tff_let ))
408 | LPAREN tff_logic_formula RPAREN (( tff_logic_formula ))
410 tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
411 Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
414 tff_variable_list : tff_variable (( [tff_variable] ))
415 | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
417 tff_variable : tff_typed_variable (( tff_typed_variable ))
418 | variable_ (( (variable_, NONE) ))
420 tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
422 tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
423 | fol_infix_unary (( fol_infix_unary ))
425 tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
426 Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
429 tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
430 | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))
432 (*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*)
433 (*FIXME why "term" if using "Let_fmla"?*)
434 tff_let_term_defn : tff_quantified_formula ((
436 val (_, vars, fmla) = extract_quant_info tff_quantified_formula
437 in [Let_fmla (hd vars, fmla)]
441 (*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*)
442 tff_let_formula_defn : tff_quantified_formula ((
444 val (_, vars, fmla) = extract_quant_info tff_quantified_formula
445 in [Let_fmla (hd vars, fmla)]
449 tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
450 | LPAREN tff_sequent RPAREN (( tff_sequent ))
452 tff_tuple : LBRKT RBRKT (( [] ))
453 | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
455 tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
456 | tff_logic_formula (( [tff_logic_formula] ))
458 tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
459 | LPAREN tff_typed_atom RPAREN (( tff_typed_atom ))
461 tff_untyped_atom : functor_ (( (functor_, NONE) ))
462 | system_functor (( (system_functor, NONE) ))
464 tff_top_level_type : tff_atomic_type (( tff_atomic_type ))
465 | tff_mapping_type (( tff_mapping_type ))
466 | tff_quantified_type (( tff_quantified_type ))
468 tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
469 Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
471 | LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
473 tff_monotype : tff_atomic_type (( tff_atomic_type ))
474 | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
476 tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
477 | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
479 tff_atomic_type : atomic_word (( Atom_type atomic_word ))
480 | defined_type (( Defined_type defined_type ))
481 | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) ))
482 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
484 tff_type_arguments : tff_atomic_type (( [tff_atomic_type] ))
485 | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments ))
487 tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
488 | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
490 tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
491 | tff_xprod_type TIMES tff_atomic_type (( Prod_type(tff_xprod_type, tff_atomic_type) ))
492 | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
497 fof_formula : fof_logic_formula (( fof_logic_formula ))
498 | fof_sequent (( fof_sequent ))
500 fof_logic_formula : fof_binary_formula (( fof_binary_formula ))
501 | fof_unitary_formula (( fof_unitary_formula ))
503 fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
504 | fof_binary_assoc (( fof_binary_assoc ))
506 fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
507 Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
510 fof_binary_assoc : fof_or_formula (( fof_or_formula ))
511 | fof_and_formula (( fof_and_formula ))
513 fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
514 | fof_or_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
516 fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
517 | fof_and_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
519 fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
520 | fof_unary_formula (( fof_unary_formula ))
521 | atomic_formula (( atomic_formula ))
522 | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
524 fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
525 Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
528 fof_variable_list : variable_ (( [variable_] ))
529 | variable_ COMMA fof_variable_list (( variable_ :: fof_variable_list ))
531 fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
532 | fol_infix_unary (( fol_infix_unary ))
534 fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
535 | LPAREN fof_sequent RPAREN (( fof_sequent ))
537 fof_tuple : LBRKT RBRKT (( [] ))
538 | LBRKT fof_tuple_list RBRKT (( fof_tuple_list ))
540 fof_tuple_list : fof_logic_formula (( [fof_logic_formula] ))
541 | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
546 cnf_formula : LPAREN disjunction RPAREN (( disjunction ))
547 | disjunction (( disjunction ))
549 disjunction : literal (( literal ))
550 | disjunction VLINE literal (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
552 literal : atomic_formula (( atomic_formula ))
553 | TILDE atomic_formula (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
554 | fol_infix_unary (( fol_infix_unary ))
557 (* Special Formulas *)
559 thf_conn_term : thf_pair_connective (( thf_pair_connective ))
560 | assoc_connective (( assoc_connective ))
561 | thf_unary_connective (( thf_unary_connective ))
563 fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
566 (* Connectives - THF *)
568 thf_quantifier : fol_quantifier (( fol_quantifier ))
570 | DEP_PROD (( Dep_Prod ))
571 | DEP_SUM (( Dep_Sum ))
572 | INDEF_CHOICE (( Epsilon ))
573 | DEFIN_CHOICE (( Iota ))
575 thf_pair_connective : infix_equality (( infix_equality ))
576 | infix_inequality (( infix_inequality ))
577 | binary_connective (( binary_connective ))
579 thf_unary_connective : unary_connective (( unary_connective ))
580 | OPERATOR_FORALL (( Interpreted_Logic Op_Forall ))
581 | OPERATOR_EXISTS (( Interpreted_Logic Op_Exists ))
584 (* Connectives - THF and TFF
585 instead of subtype_sign use token SUBTYPE
589 (* Connectives - FOF *)
591 fol_quantifier : EXCLAMATION (( Forall ))
592 | QUESTION (( Exists ))
594 binary_connective : IFF (( Interpreted_Logic Iff ))
595 | IMPLIES (( Interpreted_Logic If ))
596 | FI (( Interpreted_Logic Fi ))
597 | XOR (( Interpreted_Logic Xor ))
598 | NOR (( Interpreted_Logic Nor ))
599 | NAND (( Interpreted_Logic Nand ))
601 assoc_connective : VLINE (( Interpreted_Logic Or ))
602 | AMPERSAND (( Interpreted_Logic And ))
604 unary_connective : TILDE (( Interpreted_Logic Not ))
608 use token GENTZEN_ARROW
612 (* Types for THF and TFF *)
614 defined_type : ATOMIC_DEFINED_WORD ((
615 case ATOMIC_DEFINED_WORD of
616 "$oType" => Type_Bool
618 | "$iType" => Type_Ind
620 | "$tType" => Type_Type
621 | "$real" => Type_Real
624 | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
627 system_type : ATOMIC_SYSTEM_WORD (( ATOMIC_SYSTEM_WORD ))
630 (* First-order atoms *)
632 atomic_formula : plain_atomic_formula (( plain_atomic_formula ))
633 | defined_atomic_formula (( defined_atomic_formula ))
634 | system_atomic_formula (( system_atomic_formula ))
636 plain_atomic_formula : plain_term (( Pred plain_term ))
638 defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
639 | defined_infix_formula (( defined_infix_formula ))
641 defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
644 defined_prop : ATOMIC_DEFINED_WORD ((
645 case ATOMIC_DEFINED_WORD of
647 | "$false" => "$false"
648 | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
652 defined_pred : ATOMIC_DEFINED_WORD ((
653 case ATOMIC_DEFINED_WORD of
654 "$distinct" => "$distinct"
655 | "$ite_f" => "$ite_f"
657 | "$lesseq" => "$lesseq"
658 | "$greater" => "$greater"
659 | "$greatereq" => "$greatereq"
660 | "$is_int" => "$is_int"
661 | "$is_rat" => "$is_rat"
662 | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
665 defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
667 defined_infix_pred : infix_equality (( infix_equality ))
669 infix_equality : EQUALS (( Interpreted_Logic Equals ))
671 infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
673 system_atomic_formula : system_term (( Pred system_term ))
676 (* First-order terms *)
678 term : function_term (( function_term ))
679 | variable_ (( Term_Var variable_ ))
680 | conditional_term (( conditional_term ))
681 | let_term (( let_term ))
683 function_term : plain_term (( Term_Func plain_term ))
684 | defined_term (( defined_term ))
685 | system_term (( Term_Func system_term ))
687 plain_term : constant (( (constant, []) ))
688 | functor_ LPAREN arguments RPAREN (( (functor_, arguments) ))
690 constant : functor_ (( functor_ ))
692 functor_ : atomic_word (( Uninterpreted atomic_word ))
694 defined_term : defined_atom (( defined_atom ))
695 | defined_atomic_term (( defined_atomic_term ))
697 defined_atom : number (( Term_Num number ))
698 | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
700 defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
702 defined_plain_term : defined_constant (( (defined_constant, []) ))
703 | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
705 defined_constant : defined_functor (( defined_functor ))
707 (*FIXME must the ones other than the first batch be included here?*)
708 defined_functor : ATOMIC_DEFINED_WORD ((
709 case ATOMIC_DEFINED_WORD of
710 "$uminus" => Interpreted_ExtraLogic UMinus
711 | "$sum" => Interpreted_ExtraLogic Sum
712 | "$difference" => Interpreted_ExtraLogic Difference
713 | "$product" => Interpreted_ExtraLogic Product
714 | "$quotient" => Interpreted_ExtraLogic Quotient
715 | "$quotient_e" => Interpreted_ExtraLogic Quotient_E
716 | "$quotient_t" => Interpreted_ExtraLogic Quotient_T
717 | "$quotient_f" => Interpreted_ExtraLogic Quotient_F
718 | "$remainder_e" => Interpreted_ExtraLogic Remainder_E
719 | "$remainder_t" => Interpreted_ExtraLogic Remainder_T
720 | "$remainder_f" => Interpreted_ExtraLogic Remainder_F
721 | "$floor" => Interpreted_ExtraLogic Floor
722 | "$ceiling" => Interpreted_ExtraLogic Ceiling
723 | "$truncate" => Interpreted_ExtraLogic Truncate
724 | "$round" => Interpreted_ExtraLogic Round
725 | "$to_int" => Interpreted_ExtraLogic To_Int
726 | "$to_rat" => Interpreted_ExtraLogic To_Rat
727 | "$to_real" => Interpreted_ExtraLogic To_Real
729 | "$i" => TypeSymbol Type_Ind
730 | "$o" => TypeSymbol Type_Bool
731 | "$iType" => TypeSymbol Type_Ind
732 | "$oType" => TypeSymbol Type_Bool
733 | "$int" => TypeSymbol Type_Int
734 | "$real" => TypeSymbol Type_Real
735 | "$rat" => TypeSymbol Type_Rat
736 | "$tType" => TypeSymbol Type_Type
738 | "$true" => Interpreted_Logic True
739 | "$false" => Interpreted_Logic False
741 | "$less" => Interpreted_ExtraLogic Less
742 | "$lesseq" => Interpreted_ExtraLogic LessEq
743 | "$greatereq" => Interpreted_ExtraLogic GreaterEq
744 | "$greater" => Interpreted_ExtraLogic Greater
745 | "$evaleq" => Interpreted_ExtraLogic EvalEq
747 | "$is_int" => Interpreted_ExtraLogic Is_Int
748 | "$is_rat" => Interpreted_ExtraLogic Is_Rat
750 | "$distinct" => Interpreted_ExtraLogic Distinct
752 | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
755 system_term : system_constant (( (system_constant, []) ))
756 | system_functor LPAREN arguments RPAREN (( (system_functor, arguments) ))
758 system_constant : system_functor (( system_functor ))
760 system_functor : ATOMIC_SYSTEM_WORD (( System ATOMIC_SYSTEM_WORD ))
762 variable_ : UPPER_WORD (( UPPER_WORD ))
764 arguments : term (( [term] ))
765 | term COMMA arguments (( term :: arguments ))
767 conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
768 Term_Conditional (tff_logic_formula, term1, term2)
772 let_term : LET_FT LPAREN tff_let_formula_defn COMMA term RPAREN ((Term_Let (tff_let_formula_defn, term) ))
773 | LET_TT LPAREN tff_let_term_defn COMMA term RPAREN ((Term_Let (tff_let_term_defn, term) ))
777 Don't currently use following non-terminals:
778 source, sources, dag_source, inference_record, inference_rule, parent_list,
779 parent_info, parent_details, internal_source, intro_type, external_source,
780 file_source, file_info, theory, theory_name, creator_source, creator_name.
784 (* Useful info fields *)
786 optional_info : COMMA useful_info (( useful_info ))
789 useful_info : general_list (( general_list ))
791 include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
792 Include (file_name, formula_selection)
795 formula_selection : COMMA LBRKT name_list RBRKT (( name_list ))
798 name_list : name COMMA name_list (( name :: name_list ))
802 (* Non-logical data *)
804 general_term : general_data (( General_Data general_data ))
805 | general_data COLON general_term (( General_Term (general_data, general_term) ))
806 | general_list (( General_List general_list ))
808 general_data : atomic_word (( Atomic_Word atomic_word ))
809 | general_function (( general_function ))
810 | variable_ (( V variable_ ))
811 | number (( Number number ))
812 | DISTINCT_OBJECT (( Distinct_Object DISTINCT_OBJECT ))
813 | formula_data (( formula_data ))
815 general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
817 formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
818 | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
819 | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
820 | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
821 | DFOT LPAREN term RPAREN (( Term_Data term ))
823 general_list : LBRKT general_terms RBRKT (( general_terms ))
824 | LBRKT RBRKT (( [] ))
826 general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
827 | general_term (( [general_term] ))
830 (* General purpose *)
832 name : atomic_word (( atomic_word ))
833 | integer (( integer ))
835 (*FIXME -- "THF" onwards*)
836 atomic_word : LOWER_WORD (( LOWER_WORD ))
837 | SINGLE_QUOTED (( SINGLE_QUOTED ))
842 | INCLUDE (( "include" ))
844 (*atomic_defined_word and atomic_system_word are picked up by lex*)
846 integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
847 | SIGNED_INTEGER (( SIGNED_INTEGER ))
849 number : integer (( (Int_num, integer) ))
850 | REAL (( (Real_num, REAL) ))
851 | RATIONAL (( (Rat_num, RATIONAL) ))
853 file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))