52 -> string * failure option |
52 -> string * failure option |
53 val is_same_atp_step : step_name -> step_name -> bool |
53 val is_same_atp_step : step_name -> step_name -> bool |
54 val scan_general_id : string list -> string * string list |
54 val scan_general_id : string list -> string * string list |
55 val satallax_unsat_coreN : string |
55 val satallax_unsat_coreN : string |
56 val parse_formula : |
56 val parse_formula : |
57 string list -> (string, 'a, (string, 'a) ho_term) formula * string list |
57 string list |
|
58 -> (string, 'a, (string, 'a) ho_term) formula * string list |
58 val atp_proof_from_tstplike_proof : string problem -> string -> string proof |
59 val atp_proof_from_tstplike_proof : string problem -> string -> string proof |
59 val clean_up_atp_proof_dependencies : string proof -> string proof |
60 val clean_up_atp_proof_dependencies : string proof -> string proof |
60 val map_term_names_in_atp_proof : |
61 val map_term_names_in_atp_proof : |
61 (string -> string) -> string proof -> string proof |
62 (string -> string) -> string proof -> string proof |
62 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
63 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
249 |
250 |
250 datatype source = |
251 datatype source = |
251 File_Source of string * string option | |
252 File_Source of string * string option | |
252 Inference_Source of string * string list |
253 Inference_Source of string * string list |
253 |
254 |
254 val dummy_phi = AAtom (ATerm ("", [])) |
255 val dummy_phi = AAtom (ATerm (("", []), [])) |
255 val dummy_inference = Inference_Source ("", []) |
256 val dummy_inference = Inference_Source ("", []) |
256 |
257 |
257 (* "skip_term" is there to cope with Waldmeister nonsense such as |
258 (* "skip_term" is there to cope with Waldmeister nonsense such as |
258 "theory(equality)". *) |
259 "theory(equality)". *) |
259 val parse_dependency = scan_general_id --| skip_term |
260 val parse_dependency = scan_general_id --| skip_term |
269 -- parse_dependencies --| $$ "]" --| $$ ")" |
270 -- parse_dependencies --| $$ "]" --| $$ ")" |
270 >> Inference_Source |
271 >> Inference_Source |
271 || skip_term >> K dummy_inference) x |
272 || skip_term >> K dummy_inference) x |
272 |
273 |
273 fun list_app (f, args) = |
274 fun list_app (f, args) = |
274 fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f |
275 fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f |
275 |
276 |
276 (* We currently ignore TFF and THF types. *) |
277 (* We currently ignore TFF and THF types. *) |
277 fun parse_type_stuff x = |
278 fun parse_type_stuff x = |
278 Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x |
279 Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x |
279 and parse_arg x = |
280 and parse_arg x = |
280 ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff |
281 ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff |
281 || scan_general_id --| parse_type_stuff |
282 || scan_general_id --| parse_type_stuff |
282 -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] |
283 -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] |
283 >> ATerm) x |
284 >> (ATerm o apfst (rpair []))) x |
284 and parse_term x = |
285 and parse_term x = |
285 (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x |
286 (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x |
286 and parse_terms x = |
287 and parse_terms x = |
287 (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
288 (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
288 |
289 |
289 fun parse_atom x = |
290 fun parse_atom x = |
290 (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal |
291 (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal |
291 -- parse_term) |
292 -- parse_term) |
292 >> (fn (u1, NONE) => AAtom u1 |
293 >> (fn (u1, NONE) => AAtom u1 |
293 | (u1, SOME (neg, u2)) => |
294 | (u1, SOME (neg, u2)) => |
294 AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x |
295 AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x |
295 |
296 |
296 (* TPTP formulas are fully parenthesized, so we don't need to worry about |
297 (* TPTP formulas are fully parenthesized, so we don't need to worry about |
297 operator precedence. *) |
298 operator precedence. *) |
298 fun parse_literal x = |
299 fun parse_literal x = |
299 ((Scan.repeat ($$ tptp_not) >> length) |
300 ((Scan.repeat ($$ tptp_not) >> length) |
321 and parse_quantified_formula x = |
322 and parse_quantified_formula x = |
322 (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) |
323 (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) |
323 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal |
324 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal |
324 >> (fn ((q, ts), phi) => |
325 >> (fn ((q, ts), phi) => |
325 (* We ignore TFF and THF types for now. *) |
326 (* We ignore TFF and THF types for now. *) |
326 AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x |
327 AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x |
327 |
328 |
328 val parse_tstp_extra_arguments = |
329 val parse_tstp_extra_arguments = |
329 Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) |
330 Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) |
330 dummy_inference |
331 dummy_inference |
331 |
332 |
334 val tofof_fact_prefix = "fof_" |
335 val tofof_fact_prefix = "fof_" |
335 |
336 |
336 fun is_same_term subst tm1 tm2 = |
337 fun is_same_term subst tm1 tm2 = |
337 let |
338 let |
338 fun do_term_pair _ NONE = NONE |
339 fun do_term_pair _ NONE = NONE |
339 | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) = |
340 | do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) = |
340 case pairself is_tptp_variable (s1, s2) of |
341 case pairself is_tptp_variable (s1, s2) of |
341 (true, true) => |
342 (true, true) => |
342 (case AList.lookup (op =) subst s1 of |
343 (case AList.lookup (op =) subst s1 of |
343 SOME s2' => if s2' = s2 then SOME subst else NONE |
344 SOME s2' => if s2' = s2 then SOME subst else NONE |
344 | NONE => |
345 | NONE => |
356 q1 = q2 andalso length xs1 = length xs2 andalso |
357 q1 = q2 andalso length xs1 = length xs2 andalso |
357 is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 |
358 is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 |
358 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = |
359 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = |
359 c1 = c2 andalso length phis1 = length phis2 andalso |
360 c1 = c2 andalso length phis1 = length phis2 andalso |
360 forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) |
361 forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) |
361 | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12]))) |
362 | is_same_formula comm subst |
362 (AAtom tm2) = |
363 (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) = |
363 is_same_term subst tm1 tm2 orelse |
364 is_same_term subst tm1 tm2 orelse |
364 (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2) |
365 (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2) |
365 | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 |
366 | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 |
366 | is_same_formula _ _ _ _ = false |
367 | is_same_formula _ _ _ _ = false |
367 |
368 |
368 fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) = |
369 fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) = |
369 if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE |
370 if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE |
371 |
372 |
372 fun find_formula_in_problem problem phi = |
373 fun find_formula_in_problem problem phi = |
373 problem |> maps snd |> map_filter (matching_formula_line_identifier phi) |
374 problem |> maps snd |> map_filter (matching_formula_line_identifier phi) |
374 |> try (single o hd) |> the_default [] |
375 |> try (single o hd) |> the_default [] |
375 |
376 |
376 fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms)) |
377 fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms)) |
377 | commute_eq _ = raise Fail "expected equation" |
378 | commute_eq _ = raise Fail "expected equation" |
378 |
379 |
379 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, |
380 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, |
380 <formula> <extra_arguments>\). |
381 <formula> <extra_arguments>\). |
381 The <num> could be an identifier, but we assume integers. *) |
382 The <num> could be an identifier, but we assume integers. *) |
414 case role of |
415 case role of |
415 "definition" => |
416 "definition" => |
416 (case phi of |
417 (case phi of |
417 AConn (AIff, [phi1 as AAtom _, phi2]) => |
418 AConn (AIff, [phi1 as AAtom _, phi2]) => |
418 Definition_Step (name, phi1, phi2) |
419 Definition_Step (name, phi1, phi2) |
419 | AAtom (ATerm ("equal", _)) => |
420 | AAtom (ATerm (("equal", []), _)) => |
420 (* Vampire's equality proxy axiom *) |
421 (* Vampire's equality proxy axiom *) |
421 Inference_Step (name, phi, rule, map (rpair []) deps) |
422 Inference_Step (name, phi, rule, map (rpair []) deps) |
422 | _ => mk_step ()) |
423 | _ => mk_step ()) |
423 | _ => mk_step () |
424 | _ => mk_step () |
424 end) |
425 end) |
436 (* It is not clear why some literals are followed by sequences of stars and/or |
437 (* It is not clear why some literals are followed by sequences of stars and/or |
437 pluses. We ignore them. *) |
438 pluses. We ignore them. *) |
438 fun parse_decorated_atom x = |
439 fun parse_decorated_atom x = |
439 (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x |
440 (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x |
440 |
441 |
441 fun mk_horn ([], []) = AAtom (ATerm ("c_False", [])) |
442 fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) |
442 | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits |
443 | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits |
443 | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) |
444 | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) |
444 | mk_horn (neg_lits, pos_lits) = |
445 | mk_horn (neg_lits, pos_lits) = |
445 mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) |
446 mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) |
446 (foldr1 (uncurry (mk_aconn AOr)) pos_lits) |
447 (foldr1 (uncurry (mk_aconn AOr)) pos_lits) |
499 map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: |
500 map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: |
500 clean_up_dependencies (name :: seen) steps |
501 clean_up_dependencies (name :: seen) steps |
501 |
502 |
502 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
503 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof |
503 |
504 |
504 fun map_term_names_in_term f (ATerm (s, ts)) = |
505 fun map_term_names_in_term f (ATerm ((s, tys), ts)) = |
505 ATerm (f s, map (map_term_names_in_term f) ts) |
506 ATerm ((f s, tys), map (map_term_names_in_term f) ts) |
506 fun map_term_names_in_formula f (AQuant (q, xs, phi)) = |
507 fun map_term_names_in_formula f (AQuant (q, xs, phi)) = |
507 AQuant (q, xs, map_term_names_in_formula f phi) |
508 AQuant (q, xs, map_term_names_in_formula f phi) |
508 | map_term_names_in_formula f (AConn (c, phis)) = |
509 | map_term_names_in_formula f (AConn (c, phis)) = |
509 AConn (c, map (map_term_names_in_formula f) phis) |
510 AConn (c, map (map_term_names_in_formula f) phis) |
510 | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) |
511 | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) |