author | sultana |
Wed, 04 Apr 2012 16:29:17 +0100 | |
changeset 47360 | d1ecc9cec531 |
parent 47358 | 26c4e431ef05 |
child 47569 | fce9d97a3258 |
permissions | -rw-r--r-- |
46844 | 1 |
open TPTP_Syntax |
2 |
||
3 |
exception UNRECOGNISED_SYMBOL of string * string |
|
4 |
||
5 |
exception UNRECOGNISED_ROLE of string |
|
6 |
fun classify_role role = |
|
7 |
case role of |
|
8 |
"axiom" => Role_Axiom |
|
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 |
|
20 |
| "type" => Role_Type |
|
21 |
| "unknown" => Role_Unknown |
|
22 |
| thing => raise (UNRECOGNISED_ROLE thing) |
|
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 | 27 |
%% |
28 |
%name TPTP |
|
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 | 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 |
|
47358 | 42 |
| DOLLAR_WORD of string | DOLLAR_DOLLAR_WORD of string |
46844 | 43 |
| SUBTYPE | LET_TERM |
44 |
| THF | TFF | FOF | CNF |
|
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 | 48 |
%nonterm |
49 |
annotations of annotation option |
|
50 |
| name of string |
|
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 |
|
56 |
||
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 |
|
60 |
| integer of string |
|
61 |
| identifier of string |
|
62 |
| general_function of general_data | useful_info of general_list |
|
63 |
| file_name of string |
|
64 |
| functor_ of symbol |
|
65 |
| term of tptp_term |
|
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 |
|
76 |
| constant of symbol |
|
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 |
|
92 |
||
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 |
|
144 |
||
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 |
|
175 |
||
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 |
|
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 | 194 |
| atomic_defined_word of string |
195 |
| atomic_system_word of string |
|
47357
15e579392a68
refactored tptp yacc to bring close to official spec;
sultana
parents:
46844
diff
changeset
|
196 |
|
46844 | 197 |
%pos int |
198 |
%eop EOF |
|
199 |
%noshift EOF |
|
200 |
%arg (file_name) : string |
|
201 |
||
202 |
%nonassoc LET |
|
203 |
%nonassoc RPAREN |
|
204 |
%nonassoc DUD |
|
205 |
%right COMMA |
|
206 |
%left COLON |
|
207 |
||
208 |
%left AT_SIGN |
|
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 | 211 |
%nonassoc EQUALS NEQUALS |
212 |
%right VLINE NOR |
|
213 |
%left AMPERSAND NAND |
|
214 |
%right ARROW |
|
215 |
%left PLUS |
|
216 |
%left TIMES |
|
217 |
||
218 |
%right OPERATOR_FORALL OPERATOR_EXISTS |
|
219 |
||
220 |
%nonassoc EXCLAMATION QUESTION LAMBDA CARET |
|
221 |
%nonassoc TILDE |
|
222 |
%pure |
|
223 |
%start tptp |
|
224 |
%verbose |
|
225 |
%% |
|
226 |
||
227 |
(* Title: HOL/TPTP/TPTP_Parser/tptp.yacc |
|
228 |
Author: Nik Sultana, Cambridge University Computer Laboratory |
|
229 |
||
230 |
Parser for TPTP languages. Latest version of the language spec can |
|
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 | 233 |
*) |
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 | 269 |
annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) )) |
270 |
| (( NONE )) |
|
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 | 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 | 287 |
| thf_binary_type (( Type_fmla thf_binary_type )) |
46844 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 616 |
defined_type : atomic_defined_word (( |
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 | 628 |
|
47358 | 629 |
system_type : atomic_system_word (( atomic_system_word )) |
46844 | 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 | 646 |
defined_prop : atomic_defined_word (( |
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 | 654 |
defined_pred : atomic_defined_word (( |
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 | 665 |
)) |
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 | 694 |
functor_ : atomic_word (( Uninterpreted atomic_word )) |
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 | 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 | 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 | 709 |
(*FIXME would be nicer to split these up*) |
710 |
defined_functor : atomic_defined_word (( |
|
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 | 714 |
| "$difference" => Interpreted_ExtraLogic Difference |
715 |
| "$product" => Interpreted_ExtraLogic Product |
|
716 |
| "$quotient" => Interpreted_ExtraLogic Quotient |
|
717 |
| "$quotient_e" => Interpreted_ExtraLogic Quotient_E |
|
718 |
| "$quotient_t" => Interpreted_ExtraLogic Quotient_T |
|
719 |
| "$quotient_f" => Interpreted_ExtraLogic Quotient_F |
|
720 |
| "$remainder_e" => Interpreted_ExtraLogic Remainder_E |
|
721 |
| "$remainder_t" => Interpreted_ExtraLogic Remainder_T |
|
722 |
| "$remainder_f" => Interpreted_ExtraLogic Remainder_F |
|
723 |
| "$floor" => Interpreted_ExtraLogic Floor |
|
724 |
| "$ceiling" => Interpreted_ExtraLogic Ceiling |
|
725 |
| "$truncate" => Interpreted_ExtraLogic Truncate |
|
726 |
| "$round" => Interpreted_ExtraLogic Round |
|
727 |
| "$to_int" => Interpreted_ExtraLogic To_Int |
|
728 |
| "$to_rat" => Interpreted_ExtraLogic To_Rat |
|
729 |
| "$to_real" => Interpreted_ExtraLogic To_Real |
|
730 |
||
731 |
| "$i" => TypeSymbol Type_Ind |
|
732 |
| "$o" => TypeSymbol Type_Bool |
|
733 |
| "$iType" => TypeSymbol Type_Ind |
|
734 |
| "$oType" => TypeSymbol Type_Bool |
|
735 |
| "$int" => TypeSymbol Type_Int |
|
736 |
| "$real" => TypeSymbol Type_Real |
|
737 |
| "$rat" => TypeSymbol Type_Rat |
|
738 |
| "$tType" => TypeSymbol Type_Type |
|
739 |
||
740 |
| "$true" => Interpreted_Logic True |
|
741 |
| "$false" => Interpreted_Logic False |
|
742 |
||
743 |
| "$less" => Interpreted_ExtraLogic Less |
|
744 |
| "$lesseq" => Interpreted_ExtraLogic LessEq |
|
745 |
| "$greatereq" => Interpreted_ExtraLogic GreaterEq |
|
746 |
| "$greater" => Interpreted_ExtraLogic Greater |
|
747 |
| "$evaleq" => Interpreted_ExtraLogic EvalEq |
|
748 |
||
749 |
| "$is_int" => Interpreted_ExtraLogic Is_Int |
|
750 |
| "$is_rat" => Interpreted_ExtraLogic Is_Rat |
|
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 | 754 |
| thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing) |
755 |
)) |
|
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 | 761 |
|
47358 | 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 | 768 |
|
769 |
conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN (( |
|
770 |
Term_Conditional (tff_logic_formula, term1, term2) |
|
771 |
)) |
|
772 |
||
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 | 776 |
|
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 | 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 | 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 | 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 | 792 |
|
793 |
include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD (( |
|
794 |
Include (file_name, formula_selection) |
|
795 |
)) |
|
796 |
||
797 |
formula_selection : COMMA LBRKT name_list RBRKT (( name_list )) |
|
798 |
| (( [] )) |
|
799 |
||
800 |
name_list : name COMMA name_list (( name :: name_list )) |
|
801 |
| name (( [name] )) |
|
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 | 834 |
name : atomic_word (( atomic_word )) |
835 |
| integer (( integer )) |
|
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 | 844 |
|
47358 | 845 |
atomic_defined_word : DOLLAR_WORD (( DOLLAR_WORD )) |
846 |
||
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 | 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 )) |