532 string_from_time slice_timeout ^ "..." |
532 string_from_time slice_timeout ^ "..." |
533 |> Output.urgent_message |
533 |> Output.urgent_message |
534 else |
534 else |
535 () |
535 () |
536 val (atp_problem, pool, conjecture_offset, facts_offset, |
536 val (atp_problem, pool, conjecture_offset, facts_offset, |
537 fact_names, sym_tab) = |
537 fact_names, typed_helpers, sym_tab) = |
538 prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys |
538 prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys |
539 explicit_apply hyp_ts concl_t facts |
539 explicit_apply hyp_ts concl_t facts |
540 fun weights () = atp_problem_weights atp_problem |
540 fun weights () = atp_problem_weights atp_problem |
541 val core = |
541 val core = |
542 File.shell_path command ^ " " ^ |
542 File.shell_path command ^ " " ^ |
565 |>> (if measure_run_time then split_time else rpair NONE) |
565 |>> (if measure_run_time then split_time else rpair NONE) |
566 val (atp_proof, outcome) = |
566 val (atp_proof, outcome) = |
567 extract_tstplike_proof_and_outcome verbose complete res_code |
567 extract_tstplike_proof_and_outcome verbose complete res_code |
568 proof_delims known_failures output |
568 proof_delims known_failures output |
569 |>> atp_proof_from_tstplike_proof |
569 |>> atp_proof_from_tstplike_proof |
570 val (conjecture_shape, facts_offset, fact_names) = |
570 val (conjecture_shape, facts_offset, fact_names, |
|
571 typed_helpers) = |
571 if is_none outcome then |
572 if is_none outcome then |
572 repair_conjecture_shape_and_fact_names type_sys output |
573 repair_conjecture_shape_and_fact_names type_sys output |
573 conjecture_shape facts_offset fact_names |
574 conjecture_shape facts_offset fact_names typed_helpers |
574 else |
575 else |
575 (* don't bother repairing *) |
576 (* don't bother repairing *) |
576 (conjecture_shape, facts_offset, fact_names) |
577 (conjecture_shape, facts_offset, fact_names, typed_helpers) |
577 val outcome = |
578 val outcome = |
578 case outcome of |
579 case outcome of |
579 NONE => |
580 NONE => |
580 used_facts_in_unsound_atp_proof type_sys |
581 used_facts_in_unsound_atp_proof type_sys |
581 conjecture_shape facts_offset fact_names atp_proof |
582 conjecture_shape facts_offset fact_names atp_proof |
585 | SOME Unprovable => |
586 | SOME Unprovable => |
586 if null blacklist then outcome |
587 if null blacklist then outcome |
587 else SOME IncompleteUnprovable |
588 else SOME IncompleteUnprovable |
588 | _ => outcome |
589 | _ => outcome |
589 in |
590 in |
590 ((pool, conjecture_shape, facts_offset, fact_names, sym_tab), |
591 ((pool, conjecture_shape, facts_offset, fact_names, |
|
592 typed_helpers, sym_tab), |
591 (output, msecs, type_sys, atp_proof, outcome)) |
593 (output, msecs, type_sys, atp_proof, outcome)) |
592 end |
594 end |
593 val timer = Timer.startRealTimer () |
595 val timer = Timer.startRealTimer () |
594 fun maybe_run_slice blacklist slice |
596 fun maybe_run_slice blacklist slice |
595 (result as (_, (_, msecs0, _, _, SOME _))) = |
597 (result as (_, (_, msecs0, _, _, SOME _))) = |
605 (stuff, (output, int_opt_add msecs0 msecs, type_sys, |
607 (stuff, (output, int_opt_add msecs0 msecs, type_sys, |
606 atp_proof, outcome)))) |
608 atp_proof, outcome)))) |
607 end |
609 end |
608 | maybe_run_slice _ _ result = result |
610 | maybe_run_slice _ _ result = result |
609 fun maybe_blacklist_facts_and_retry iter blacklist |
611 fun maybe_blacklist_facts_and_retry iter blacklist |
610 (result as ((_, _, facts_offset, fact_names, _), |
612 (result as ((_, _, facts_offset, fact_names, _, _), |
611 (_, _, type_sys, atp_proof, |
613 (_, _, type_sys, atp_proof, |
612 SOME (UnsoundProof (false, _))))) = |
614 SOME (UnsoundProof (false, _))))) = |
613 (case used_facts_in_atp_proof type_sys facts_offset fact_names |
615 (case used_facts_in_atp_proof type_sys facts_offset fact_names |
614 atp_proof of |
616 atp_proof of |
615 [] => result |
617 [] => result |
622 end |
624 end |
623 else |
625 else |
624 result) |
626 result) |
625 | maybe_blacklist_facts_and_retry _ _ result = result |
627 | maybe_blacklist_facts_and_retry _ _ result = result |
626 in |
628 in |
627 ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty), |
629 ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty), |
628 ("", SOME 0, hd fallback_best_type_systems, [], |
630 ("", SOME 0, hd fallback_best_type_systems, [], |
629 SOME InternalError)) |
631 SOME InternalError)) |
630 |> fold (maybe_run_slice []) actual_slices |
632 |> fold (maybe_run_slice []) actual_slices |
631 (* The ATP found an unsound proof? Automatically try again |
633 (* The ATP found an unsound proof? Automatically try again |
632 without the offending facts! *) |
634 without the offending facts! *) |
642 fun export prob_file (_, (output, _, _, _, _)) = |
644 fun export prob_file (_, (output, _, _, _, _)) = |
643 if dest_dir = "" then |
645 if dest_dir = "" then |
644 () |
646 () |
645 else |
647 else |
646 File.write (Path.explode (Path.implode prob_file ^ "_proof")) output |
648 File.write (Path.explode (Path.implode prob_file ^ "_proof")) output |
647 val ((pool, conjecture_shape, facts_offset, fact_names, sym_tab), |
649 val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers, |
|
650 sym_tab), |
648 (output, msecs, type_sys, atp_proof, outcome)) = |
651 (output, msecs, type_sys, atp_proof, outcome)) = |
649 with_path cleanup export run_on problem_path_name |
652 with_path cleanup export run_on problem_path_name |
650 val important_message = |
653 val important_message = |
651 if not auto andalso |
654 if not auto andalso |
652 random_range 0 (atp_important_message_keep_quotient - 1) = 0 then |
655 random_range 0 (atp_important_message_keep_quotient - 1) = 0 then |
666 "") |
669 "") |
667 val isar_params = |
670 val isar_params = |
668 (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) |
671 (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) |
669 val metis_params = |
672 val metis_params = |
670 (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset, |
673 (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset, |
671 fact_names, goal, subgoal) |
674 fact_names, typed_helpers, goal, subgoal) |
672 val (outcome, (message, used_facts)) = |
675 val (outcome, (message, used_facts)) = |
673 case outcome of |
676 case outcome of |
674 NONE => |
677 NONE => |
675 (NONE, proof_text isar_proof isar_params metis_params |
678 (NONE, proof_text isar_proof isar_params metis_params |
676 |>> append_to_message) |
679 |>> append_to_message) |