426 val proofstart = "proof (neg_clausify)\n"; |
426 val proofstart = "proof (neg_clausify)\n"; |
427 |
427 |
428 fun isar_header [] = proofstart |
428 fun isar_header [] = proofstart |
429 | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; |
429 | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; |
430 |
430 |
431 fun decode_tstp_file cnfs ctxt th sgno thm_names = |
431 fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names = |
432 let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n") |
432 let |
433 val tuples = map (dest_tstp o tstp_line o explode) cnfs |
433 val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") |
434 val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n") |
434 val tuples = map (dest_tstp o tstp_line o explode) cnfs |
435 val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt |
435 val _ = trace_proof_msg (fn () => |
436 val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) |
436 Int.toString (length tuples) ^ " tuples extracted\n") |
437 val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n") |
437 val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt |
438 val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines |
438 val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) |
439 val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") |
439 val _ = trace_proof_msg (fn () => |
440 val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines |
440 Int.toString (length raw_lines) ^ " raw_lines extracted\n") |
441 val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n") |
441 val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines |
442 val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno |
442 val _ = trace_proof_msg (fn () => |
443 val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n") |
443 Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") |
444 val ccls = map forall_intr_vars ccls |
444 val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines |
445 val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls |
445 val _ = trace_proof_msg (fn () => |
446 val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) |
446 Int.toString (length lines) ^ " lines extracted\n") |
447 val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n") |
447 val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno |
448 in |
448 val _ = trace_proof_msg (fn () => |
449 isar_header (map #1 fixes) ^ implode ilines ^ "qed\n" |
449 Int.toString (length ccls) ^ " conjecture clauses\n") |
450 end handle STREE _ => error "Could not extract proof (ATP output malformed?)"; |
450 val ccls = map forall_intr_vars ccls |
|
451 val _ = app (fn th => trace_proof_msg |
|
452 (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls |
|
453 val isar_lines = isar_lines ctxt (map prop_of ccls) |
|
454 (stringify_deps thm_names [] lines) |
|
455 val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") |
|
456 in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end |
|
457 handle STREE _ => error "Could not extract proof (ATP output malformed?)"; |
451 |
458 |
452 |
459 |
453 (*=== EXTRACTING PROOF-TEXT === *) |
460 (*=== EXTRACTING PROOF-TEXT === *) |
454 |
461 |
455 val begin_proof_strs = ["# SZS output start CNFRefutation.", |
462 val begin_proof_strs = ["# SZS output start CNFRefutation.", |
528 | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" |
535 | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" |
529 |
536 |
530 (* atp_minimize [atp=<prover>] <lemmas> *) |
537 (* atp_minimize [atp=<prover>] <lemmas> *) |
531 fun minimize_line _ [] = "" |
538 fun minimize_line _ [] = "" |
532 | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ |
539 | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ |
533 (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ |
540 Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ |
534 space_implode " " (kill_chained lemmas)) |
541 space_implode " " (kill_chained lemmas)) |
535 |
|
536 val sendback_metis_no_chained = |
|
537 Markup.markup Markup.sendback o metis_line o kill_chained |
|
538 |
542 |
539 fun metis_lemma_list dfg name result = |
543 fun metis_lemma_list dfg name result = |
540 let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result |
544 let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in |
541 in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^ |
545 (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^ |
542 (if used_conj then |
546 minimize_line name lemmas ^ |
543 "" |
547 (if used_conj then |
544 else |
548 "" |
545 "\nWarning: The goal is provable because the context is inconsistent."), |
549 else |
|
550 "\nWarning: The goal is provable because the context is inconsistent."), |
546 kill_chained lemmas) |
551 kill_chained lemmas) |
547 end; |
552 end; |
548 |
553 |
549 fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt, |
554 fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt, |
550 goal, subgoalno)) = |
555 goal, subgoalno)) = |
551 let |
556 let |
552 (* Could use "split_lines", but it can return blank lines *) |
557 (* Could use "split_lines", but it can return blank lines *) |
553 val lines = String.tokens (equal #"\n"); |
558 val lines = String.tokens (equal #"\n"); |
554 val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c) |
559 val kill_spaces = |
|
560 String.translate (fn c => if Char.isSpace c then "" else str c) |
555 val extract = get_proof_extract proof |
561 val extract = get_proof_extract proof |
556 val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) |
562 val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) |
557 val (one_line_proof, lemma_names) = metis_lemma_list false name result |
563 val (one_line_proof, lemma_names) = metis_lemma_list false name result |
558 val structured = |
564 val tokens = String.tokens (fn c => c = #" ") one_line_proof |
559 if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" |
565 val isar_proof = |
560 else decode_tstp_file cnfs ctxt goal subgoalno thm_names |
566 if member (op =) tokens chained_hint then "" |
|
567 else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names |
561 in |
568 in |
562 (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, |
569 (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof, |
563 lemma_names) |
570 lemma_names) |
564 end |
571 end |
565 |
572 |
566 end; |
573 end; |