98 \ sledgehammer\")." |
98 \ sledgehammer\")." |
99 | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover |
99 | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover |
100 | string_for_failure prover NoLibwwwPerl = |
100 | string_for_failure prover NoLibwwwPerl = |
101 "The Perl module \"libwww-perl\"" ^ missing_message_tail prover |
101 "The Perl module \"libwww-perl\"" ^ missing_message_tail prover |
102 | string_for_failure prover MalformedInput = |
102 | string_for_failure prover MalformedInput = |
103 "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \ |
103 "The " ^ prover ^ " problem is malformed. Please report this to the \ |
104 \developers." |
104 \Isabelle developers." |
105 | string_for_failure prover MalformedOutput = |
105 | string_for_failure prover MalformedOutput = |
106 "The " ^ prover ^ " output is malformed." |
106 "The " ^ prover ^ " output is malformed." |
107 | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted." |
107 | string_for_failure prover Interrupted = |
|
108 "The " ^ prover ^ " was interrupted." |
108 | string_for_failure prover Crashed = "The " ^ prover ^ " crashed." |
109 | string_for_failure prover Crashed = "The " ^ prover ^ " crashed." |
109 | string_for_failure prover InternalError = |
110 | string_for_failure prover InternalError = |
110 "An internal " ^ prover ^ " error occurred." |
111 "An internal " ^ prover ^ " error occurred." |
111 | string_for_failure prover UnknownError = |
112 | string_for_failure prover UnknownError = |
112 (* "An" is correct for "ATP" and "SMT". *) |
113 (* "An" is correct for "ATP" and "SMT". *) |
214 fun parse_vampire_detritus x = |
215 fun parse_vampire_detritus x = |
215 (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x |
216 (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x |
216 |
217 |
217 fun parse_term x = |
218 fun parse_term x = |
218 (scan_general_id |
219 (scan_general_id |
219 -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms) |
220 -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms) |
220 --| $$ ")") [] |
221 --| $$ ")") [] |
221 --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") [] |
222 --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") [] |
222 >> ATerm) x |
223 >> ATerm) x |
223 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
224 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
224 |
225 |
225 fun parse_atom x = |
226 fun parse_atom x = |
226 (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) |
227 (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) |
251 |
252 |
252 val parse_tstp_extra_arguments = |
253 val parse_tstp_extra_arguments = |
253 Scan.optional ($$ "," |-- parse_annotation false |
254 Scan.optional ($$ "," |-- parse_annotation false |
254 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
255 --| Scan.option ($$ "," |-- parse_annotations false)) [] |
255 |
256 |
|
257 val vampire_unknown_fact = "unknown" |
|
258 |
256 (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
259 (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
257 The <num> could be an identifier, but we assume integers. *) |
260 The <num> could be an identifier, but we assume integers. *) |
258 val parse_tstp_line = |
261 val parse_tstp_line = |
259 ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") |
262 ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") |
260 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
263 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
261 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
264 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
262 >> (fn (((num, role), phi), deps) => |
265 >> (fn (((num, role), phi), deps) => |
263 let |
266 let |
264 val (name, deps) = |
267 val (name, deps) = |
265 case deps of |
268 case deps of |
266 ["file", _, s] => ((num, SOME s), []) |
269 ["file", _, s] => |
|
270 ((num, if s = vampire_unknown_fact then NONE else SOME s), []) |
267 | _ => ((num, NONE), deps) |
271 | _ => ((num, NONE), deps) |
268 in |
272 in |
269 case role of |
273 case role of |
270 "definition" => |
274 "definition" => |
271 (case phi of |
275 (case phi of |
280 |
284 |
281 (**** PARSING OF VAMPIRE OUTPUT ****) |
285 (**** PARSING OF VAMPIRE OUTPUT ****) |
282 |
286 |
283 val parse_vampire_braced_stuff = |
287 val parse_vampire_braced_stuff = |
284 $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}" |
288 $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}" |
285 -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")") |
289 val parse_vampire_parenthesized_detritus = |
|
290 $$ "(" |-- parse_vampire_detritus --| $$ ")" |
286 |
291 |
287 (* Syntax: <num>. <formula> <annotation> *) |
292 (* Syntax: <num>. <formula> <annotation> *) |
288 val parse_vampire_line = |
293 val parse_vampire_line = |
289 scan_general_id --| $$ "." -- parse_formula |
294 scan_general_id --| $$ "." -- parse_formula |
290 --| Scan.option parse_vampire_braced_stuff -- parse_annotation true |
295 --| Scan.option parse_vampire_braced_stuff |
|
296 --| Scan.option parse_vampire_parenthesized_detritus |
|
297 -- parse_annotation true |
291 >> (fn ((num, phi), deps) => |
298 >> (fn ((num, phi), deps) => |
292 Inference ((num, NONE), phi, map (rpair NONE) deps)) |
299 Inference ((num, NONE), phi, map (rpair NONE) deps)) |
293 |
300 |
294 (**** PARSING OF SPASS OUTPUT ****) |
301 (**** PARSING OF SPASS OUTPUT ****) |
295 |
302 |