678 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b) |
685 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b) |
679 val as_time = |
686 val as_time = |
680 raw_explode #> Scan.read Symbol.stopper time #> the_default 0 |
687 raw_explode #> Scan.read Symbol.stopper time #> the_default 0 |
681 in (output, as_time t |> Time.fromMilliseconds) end |
688 in (output, as_time t |> Time.fromMilliseconds) end |
682 fun run_on prob_file = |
689 fun run_on prob_file = |
683 case find_first (forall (fn var => getenv var = "")) |
690 let |
684 (fst exec :: required_vars) of |
691 (* If slicing is disabled, we expand the last slice to fill the entire |
685 SOME home_vars => |
692 time available. *) |
686 error ("The environment variable " ^ quote (hd home_vars) ^ |
693 val actual_slices = get_slices slice (best_slices ctxt) |
687 " is not set.") |
694 val num_actual_slices = length actual_slices |
688 | NONE => |
695 fun monomorphize_facts facts = |
689 if File.exists command then |
|
690 let |
696 let |
691 (* If slicing is disabled, we expand the last slice to fill the |
697 val ctxt = |
692 entire time available. *) |
698 ctxt |
693 val actual_slices = get_slices slice (best_slices ctxt) |
699 |> repair_monomorph_context max_mono_iters best_max_mono_iters |
694 val num_actual_slices = length actual_slices |
700 max_new_mono_instances best_max_new_mono_instances |
695 fun monomorphize_facts facts = |
701 (* pseudo-theorem involving the same constants as the subgoal *) |
696 let |
702 val subgoal_th = |
697 val ctxt = |
703 Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
698 ctxt |
704 val rths = |
699 |> repair_monomorph_context max_mono_iters best_max_mono_iters |
705 facts |> chop mono_max_privileged_facts |
700 max_new_mono_instances best_max_new_mono_instances |
706 |>> map (pair 1 o snd) |
701 (* pseudo-theorem involving the same constants as the subgoal *) |
707 ||> map (pair 2 o snd) |
702 val subgoal_th = |
708 |> op @ |
703 Logic.list_implies (hyp_ts, concl_t) |
709 |> cons (0, subgoal_th) |
704 |> Skip_Proof.make_thm thy |
|
705 val rths = |
|
706 facts |> chop mono_max_privileged_facts |
|
707 |>> map (pair 1 o snd) |
|
708 ||> map (pair 2 o snd) |
|
709 |> op @ |
|
710 |> cons (0, subgoal_th) |
|
711 in |
|
712 Monomorph.monomorph atp_schematic_consts_of rths ctxt |
|
713 |> fst |> tl |
|
714 |> curry ListPair.zip (map fst facts) |
|
715 |> maps (fn (name, rths) => |
|
716 map (pair name o zero_var_indexes o snd) rths) |
|
717 end |
|
718 fun run_slice time_left (cache_key, cache_value) |
|
719 (slice, (time_frac, (complete, |
|
720 (key as (best_max_facts, format, best_type_enc, |
|
721 best_lam_trans, best_uncurried_aliases), |
|
722 extra)))) = |
|
723 let |
|
724 val num_facts = |
|
725 length facts |> is_none max_facts ? Integer.min best_max_facts |
|
726 val soundness = if strict then Strict else Non_Strict |
|
727 val type_enc = |
|
728 type_enc |> choose_type_enc soundness best_type_enc format |
|
729 val sound = is_type_enc_sound type_enc |
|
730 val real_ms = Real.fromInt o Time.toMilliseconds |
|
731 val slice_timeout = |
|
732 ((real_ms time_left |
|
733 |> (if slice < num_actual_slices - 1 then |
|
734 curry Real.min (time_frac * real_ms timeout) |
|
735 else |
|
736 I)) |
|
737 * 0.001) |> seconds |
|
738 val generous_slice_timeout = |
|
739 Time.+ (slice_timeout, atp_timeout_slack) |
|
740 val _ = |
|
741 if debug then |
|
742 quote name ^ " slice #" ^ string_of_int (slice + 1) ^ |
|
743 " with " ^ string_of_int num_facts ^ " fact" ^ |
|
744 plural_s num_facts ^ " for " ^ |
|
745 string_from_time slice_timeout ^ "..." |
|
746 |> Output.urgent_message |
|
747 else |
|
748 () |
|
749 val readable_names = not (Config.get ctxt atp_full_names) |
|
750 val lam_trans = |
|
751 case lam_trans of |
|
752 SOME s => s |
|
753 | NONE => best_lam_trans |
|
754 val uncurried_aliases = |
|
755 case uncurried_aliases of |
|
756 SOME b => b |
|
757 | NONE => best_uncurried_aliases |
|
758 val value as (atp_problem, _, fact_names, _, _) = |
|
759 if cache_key = SOME key then |
|
760 cache_value |
|
761 else |
|
762 facts |
|
763 |> map untranslated_fact |
|
764 |> not sound |
|
765 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
|
766 |> take num_facts |
|
767 |> not (is_type_enc_polymorphic type_enc) |
|
768 ? monomorphize_facts |
|
769 |> map (apsnd prop_of) |
|
770 |> prepare_atp_problem ctxt format prem_role type_enc |
|
771 atp_mode lam_trans uncurried_aliases |
|
772 readable_names true hyp_ts concl_t |
|
773 fun sel_weights () = atp_problem_selection_weights atp_problem |
|
774 fun ord_info () = atp_problem_term_order_info atp_problem |
|
775 val ord = effective_term_order ctxt name |
|
776 val full_proof = debug orelse isar_proof |
|
777 val args = arguments ctxt full_proof extra slice_timeout |
|
778 (ord, ord_info, sel_weights) |
|
779 val command = |
|
780 File.shell_path command ^ " " ^ args ^ " " ^ |
|
781 File.shell_path prob_file |
|
782 |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" |
|
783 val _ = |
|
784 atp_problem |
|
785 |> lines_for_atp_problem format ord ord_info |
|
786 |> cons ("% " ^ command ^ "\n") |
|
787 |> File.write_list prob_file |
|
788 val ((output, run_time), (atp_proof, outcome)) = |
|
789 TimeLimit.timeLimit generous_slice_timeout |
|
790 Isabelle_System.bash_output command |
|
791 |>> (if overlord then |
|
792 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
793 else |
|
794 I) |
|
795 |> fst |> split_time |
|
796 |> (fn accum as (output, _) => |
|
797 (accum, |
|
798 extract_tstplike_proof_and_outcome verbose complete |
|
799 proof_delims known_failures output |
|
800 |>> atp_proof_from_tstplike_proof atp_problem |
|
801 handle UNRECOGNIZED_ATP_PROOF () => |
|
802 ([], SOME ProofIncomplete))) |
|
803 handle TimeLimit.TimeOut => |
|
804 (("", slice_timeout), ([], SOME TimedOut)) |
|
805 val outcome = |
|
806 case outcome of |
|
807 NONE => |
|
808 (case used_facts_in_unsound_atp_proof ctxt fact_names |
|
809 atp_proof |
|
810 |> Option.map (sort string_ord) of |
|
811 SOME facts => |
|
812 let |
|
813 val failure = |
|
814 UnsoundProof (is_type_enc_sound type_enc, facts) |
|
815 in |
|
816 if debug then |
|
817 (warning (string_for_failure failure); NONE) |
|
818 else |
|
819 SOME failure |
|
820 end |
|
821 | NONE => NONE) |
|
822 | _ => outcome |
|
823 in ((SOME key, value), (output, run_time, atp_proof, outcome)) end |
|
824 val timer = Timer.startRealTimer () |
|
825 fun maybe_run_slice slice |
|
826 (result as (cache, (_, run_time0, _, SOME _))) = |
|
827 let |
|
828 val time_left = Time.- (timeout, Timer.checkRealTimer timer) |
|
829 in |
|
830 if Time.<= (time_left, Time.zeroTime) then |
|
831 result |
|
832 else |
|
833 run_slice time_left cache slice |
|
834 |> (fn (cache, (output, run_time, atp_proof, outcome)) => |
|
835 (cache, (output, Time.+ (run_time0, run_time), |
|
836 atp_proof, outcome))) |
|
837 end |
|
838 | maybe_run_slice _ result = result |
|
839 in |
710 in |
840 ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), |
711 Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl |
841 ("", Time.zeroTime, [], SOME InternalError)) |
712 |> curry ListPair.zip (map fst facts) |
842 |> fold maybe_run_slice actual_slices |
713 |> maps (fn (name, rths) => |
|
714 map (pair name o zero_var_indexes o snd) rths) |
843 end |
715 end |
844 else |
716 fun run_slice time_left (cache_key, cache_value) |
845 error ("Bad executable: " ^ Path.print command) |
717 (slice, (time_frac, (complete, |
|
718 (key as (best_max_facts, format, best_type_enc, |
|
719 best_lam_trans, best_uncurried_aliases), |
|
720 extra)))) = |
|
721 let |
|
722 val num_facts = |
|
723 length facts |> is_none max_facts ? Integer.min best_max_facts |
|
724 val soundness = if strict then Strict else Non_Strict |
|
725 val type_enc = |
|
726 type_enc |> choose_type_enc soundness best_type_enc format |
|
727 val sound = is_type_enc_sound type_enc |
|
728 val real_ms = Real.fromInt o Time.toMilliseconds |
|
729 val slice_timeout = |
|
730 ((real_ms time_left |
|
731 |> (if slice < num_actual_slices - 1 then |
|
732 curry Real.min (time_frac * real_ms timeout) |
|
733 else |
|
734 I)) |
|
735 * 0.001) |> seconds |
|
736 val generous_slice_timeout = |
|
737 Time.+ (slice_timeout, atp_timeout_slack) |
|
738 val _ = |
|
739 if debug then |
|
740 quote name ^ " slice #" ^ string_of_int (slice + 1) ^ |
|
741 " with " ^ string_of_int num_facts ^ " fact" ^ |
|
742 plural_s num_facts ^ " for " ^ |
|
743 string_from_time slice_timeout ^ "..." |
|
744 |> Output.urgent_message |
|
745 else |
|
746 () |
|
747 val readable_names = not (Config.get ctxt atp_full_names) |
|
748 val lam_trans = |
|
749 case lam_trans of |
|
750 SOME s => s |
|
751 | NONE => best_lam_trans |
|
752 val uncurried_aliases = |
|
753 case uncurried_aliases of |
|
754 SOME b => b |
|
755 | NONE => best_uncurried_aliases |
|
756 val value as (atp_problem, _, fact_names, _, _) = |
|
757 if cache_key = SOME key then |
|
758 cache_value |
|
759 else |
|
760 facts |
|
761 |> map untranslated_fact |
|
762 |> not sound |
|
763 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
|
764 |> take num_facts |
|
765 |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |
|
766 |> map (apsnd prop_of) |
|
767 |> prepare_atp_problem ctxt format prem_role type_enc atp_mode |
|
768 lam_trans uncurried_aliases |
|
769 readable_names true hyp_ts concl_t |
|
770 fun sel_weights () = atp_problem_selection_weights atp_problem |
|
771 fun ord_info () = atp_problem_term_order_info atp_problem |
|
772 val ord = effective_term_order ctxt name |
|
773 val full_proof = debug orelse isar_proof |
|
774 val args = arguments ctxt full_proof extra slice_timeout |
|
775 (ord, ord_info, sel_weights) |
|
776 val command = |
|
777 File.shell_path command0 ^ " " ^ args ^ " " ^ |
|
778 File.shell_path prob_file |
|
779 |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" |
|
780 val _ = |
|
781 atp_problem |
|
782 |> lines_for_atp_problem format ord ord_info |
|
783 |> cons ("% " ^ command ^ "\n") |
|
784 |> File.write_list prob_file |
|
785 val ((output, run_time), (atp_proof, outcome)) = |
|
786 TimeLimit.timeLimit generous_slice_timeout |
|
787 Isabelle_System.bash_output command |
|
788 |>> (if overlord then |
|
789 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
790 else |
|
791 I) |
|
792 |> fst |> split_time |
|
793 |> (fn accum as (output, _) => |
|
794 (accum, |
|
795 extract_tstplike_proof_and_outcome verbose complete |
|
796 proof_delims known_failures output |
|
797 |>> atp_proof_from_tstplike_proof atp_problem |
|
798 handle UNRECOGNIZED_ATP_PROOF () => |
|
799 ([], SOME ProofIncomplete))) |
|
800 handle TimeLimit.TimeOut => |
|
801 (("", slice_timeout), ([], SOME TimedOut)) |
|
802 val outcome = |
|
803 case outcome of |
|
804 NONE => |
|
805 (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof |
|
806 |> Option.map (sort string_ord) of |
|
807 SOME facts => |
|
808 let |
|
809 val failure = |
|
810 UnsoundProof (is_type_enc_sound type_enc, facts) |
|
811 in |
|
812 if debug then (warning (string_for_failure failure); NONE) |
|
813 else SOME failure |
|
814 end |
|
815 | NONE => NONE) |
|
816 | _ => outcome |
|
817 in ((SOME key, value), (output, run_time, atp_proof, outcome)) end |
|
818 val timer = Timer.startRealTimer () |
|
819 fun maybe_run_slice slice |
|
820 (result as (cache, (_, run_time0, _, SOME _))) = |
|
821 let |
|
822 val time_left = Time.- (timeout, Timer.checkRealTimer timer) |
|
823 in |
|
824 if Time.<= (time_left, Time.zeroTime) then |
|
825 result |
|
826 else |
|
827 run_slice time_left cache slice |
|
828 |> (fn (cache, (output, run_time, atp_proof, outcome)) => |
|
829 (cache, (output, Time.+ (run_time0, run_time), |
|
830 atp_proof, outcome))) |
|
831 end |
|
832 | maybe_run_slice _ result = result |
|
833 in |
|
834 ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), |
|
835 ("", Time.zeroTime, [], SOME InternalError)) |
|
836 |> fold maybe_run_slice actual_slices |
|
837 end |
846 |
838 |
847 (* If the problem file has not been exported, remove it; otherwise, export |
839 (* If the problem file has not been exported, remove it; otherwise, export |
848 the proof file too. *) |
840 the proof file too. *) |
849 fun cleanup prob_file = |
841 fun cleanup prob_file = |
850 if dest_dir = "" then try File.rm prob_file else NONE |
842 if dest_dir = "" then try File.rm prob_file else NONE |
851 fun export prob_file (_, (output, _, _, _)) = |
843 fun export prob_file (_, (output, _, _, _)) = |
852 if dest_dir = "" then |
844 if dest_dir = "" then () |
853 () |
845 else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output |
854 else |
|
855 File.write (Path.explode (Path.implode prob_file ^ "_proof")) output |
|
856 val ((_, (_, pool, fact_names, _, sym_tab)), |
846 val ((_, (_, pool, fact_names, _, sym_tab)), |
857 (output, run_time, atp_proof, outcome)) = |
847 (output, run_time, atp_proof, outcome)) = |
858 with_path cleanup export run_on problem_path_name |
848 with_path cleanup export run_on problem_path_name |
859 val important_message = |
849 val important_message = |
860 if mode = Normal andalso |
850 if mode = Normal andalso |