# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID c4b9b4be90c4b583c3b7bf4d3a6a689e7c1aa06a # Parent f617a5323d07bef002b36ff04f34426d3f937642 show time taken for reconstruction diff -r f617a5323d07 -r c4b9b4be90c4 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:08 2011 +0200 @@ -11,14 +11,23 @@ type 'a proof = 'a ATP_Proof.proof type locality = Sledgehammer_Filter.locality type type_system = Sledgehammer_ATP_Translate.type_system + + datatype reconstructor = + Metis | + MetisFT | + SMT of string + + datatype preplay = + Preplayed of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option| + Preplay_Failed + type minimize_command = string list -> string - type metis_params = - string * minimize_command * type_system * string proof * int - * (string * locality) list vector * int list * thm * int + type one_line_params = + preplay * string * (string * locality) list * minimize_command * thm * int type isar_params = - bool * int * string Symtab.table * int list list * int Symtab.table - type text_result = string * (string * locality) list - + bool * bool * int * type_system * string Symtab.table * int list list + * int * (string * locality) list vector * int Symtab.table * string proof val repair_conjecture_shape_and_fact_names : type_system -> string -> int list list -> int -> (string * locality) list vector -> int list @@ -28,19 +37,22 @@ -> string proof -> (string * locality) list val used_facts_in_unsound_atp_proof : Proof.context -> type_system -> int list list -> int - -> (string * locality) list vector -> string proof -> string list option + -> (string * locality) list vector -> 'a proof -> string list option + val uses_typed_helpers : int list -> 'a proof -> bool + val reconstructor_name : reconstructor -> string + val reconstructor_settings : reconstructor -> string val apply_on_subgoal : string -> int -> int -> string val command_call : string -> string list -> string - val try_command_line : string -> string -> string + val try_command_line : string -> (bool * Time.time) option -> string -> string val minimize_line : ('a list -> string) -> 'a list -> string val split_used_facts : (string * locality) list -> (string * locality) list * (string * locality) list - val metis_proof_text : Proof.context -> metis_params -> text_result + val one_line_proof_text : one_line_params -> string val isar_proof_text : - Proof.context -> isar_params -> metis_params -> text_result + Proof.context -> isar_params -> one_line_params -> string val proof_text : - Proof.context -> bool -> isar_params -> metis_params -> text_result + Proof.context -> bool -> isar_params -> one_line_params -> string end; structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = @@ -53,13 +65,22 @@ open Sledgehammer_Filter open Sledgehammer_ATP_Translate +datatype reconstructor = + Metis | + MetisFT | + SMT of string + +datatype preplay = + Preplayed of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option | + Preplay_Failed + type minimize_command = string list -> string -type metis_params = - string * minimize_command * type_system * string proof * int - * (string * locality) list vector * int list * thm * int +type one_line_params = + preplay * string * (string * locality) list * minimize_command * thm * int type isar_params = - bool * int * string Symtab.table * int list list * int Symtab.table -type text_result = string * (string * locality) list + bool * bool * int * type_system * string Symtab.table * int list list * int + * (string * locality) list vector * int Symtab.table * string proof fun is_head_digit s = Char.isDigit (String.sub (s, 0)) val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) @@ -223,10 +244,25 @@ NONE end +fun uses_typed_helpers typed_helpers = + exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name + | _ => false) + + (** Soft-core proof reconstruction: Metis one-liner **) +fun reconstructor_name Metis = "metis" + | reconstructor_name MetisFT = "metisFT" + | reconstructor_name (SMT _) = "smt" + +fun reconstructor_settings (SMT settings) = settings + | reconstructor_settings _ = "" + fun string_for_label (s, num) = s ^ string_of_int num +fun show_time NONE = "" + | show_time (SOME ext_time) = " ~ " ^ string_from_ext_time ext_time + fun set_settings "" = "" | set_settings settings = "using [[" ^ settings ^ "]] " fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " @@ -235,15 +271,15 @@ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n fun command_call name [] = name | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" -fun try_command_line banner command = - banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." +fun try_command_line banner time command = + banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "." fun using_labels [] = "" | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_name full_types = if full_types then "metisFT" else "metis" -fun metis_call full_types ss = command_call (metis_name full_types) ss -fun metis_command full_types i n (ls, ss) = - using_labels ls ^ apply_on_subgoal "" i n ^ metis_call full_types ss +fun reconstructor_command reconstructor i n (ls, ss) = + using_labels ls ^ + apply_on_subgoal (reconstructor_settings reconstructor) i n ^ + command_call (reconstructor_name reconstructor) ss fun minimize_line _ [] = "" | minimize_line minimize_command ss = case minimize_command ss of @@ -254,24 +290,28 @@ List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) -fun uses_typed_helpers typed_helpers = - exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name - | _ => false) - -fun metis_proof_text ctxt (banner, minimize_command, type_sys, atp_proof, - facts_offset, fact_names, typed_helpers, goal, i) = +fun one_line_proof_text (preplay, banner, used_facts, minimize_command, + goal, i) = let - val (chained, extra) = - atp_proof |> used_facts_in_atp_proof ctxt type_sys facts_offset fact_names - |> split_used_facts - val full_types = uses_typed_helpers typed_helpers atp_proof + val (chained, extra) = split_used_facts used_facts + val (reconstructor, ext_time) = + case preplay of + Preplayed (reconstructor, time) => + (SOME reconstructor, (SOME (false, time))) + | Trust_Playable (reconstructor, time) => + (SOME reconstructor, + case time of + NONE => NONE + | SOME time => + if time = Time.zeroTime then NONE else SOME (true, time)) + | Preplay_Failed => (NONE, NONE) val n = Logic.count_prems (prop_of goal) - val metis = metis_command full_types i n ([], map fst extra) - in - (try_command_line banner metis ^ - minimize_line minimize_command (map fst (extra @ chained)), - extra @ chained) - end + val try_line = + case reconstructor of + SOME r => reconstructor_command r i n ([], map fst extra) + |> try_command_line banner ext_time + | NONE => "Proof reconstruction failed." + in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end (** Hard-core proof reconstruction: structured Isar proofs **) @@ -702,8 +742,8 @@ s fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor - atp_proof conjecture_shape facts_offset fact_names sym_tab params - frees = + conjecture_shape facts_offset fact_names sym_tab params frees + atp_proof = let val lines = atp_proof @@ -976,10 +1016,11 @@ else if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) + val reconstructor = if full_types then MetisFT else Metis fun do_facts (ls, ss) = - metis_command full_types 1 1 - (ls |> sort_distinct (prod_ord string_ord int_ord), - ss |> sort_distinct string_ord) + reconstructor_command reconstructor 1 1 + (ls |> sort_distinct (prod_ord string_ord int_ord), + ss |> sort_distinct string_ord) and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Let (t1, t2)) = @@ -1012,20 +1053,20 @@ in do_proof end fun isar_proof_text ctxt - (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) - (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names, - typed_helpers, goal, i)) = + (debug, full_types, isar_shrink_factor, type_sys, pool, + conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof) + (one_line_params as (_, _, _, _, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] - val full_types = uses_typed_helpers typed_helpers atp_proof val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = metis_proof_text ctxt metis_params + val one_line_proof = one_line_proof_text one_line_params fun isar_proof_for () = - case isar_proof_from_atp_proof pool ctxt type_sys tfrees - isar_shrink_factor atp_proof conjecture_shape facts_offset - fact_names sym_tab params frees + case atp_proof + |> isar_proof_from_atp_proof pool ctxt type_sys tfrees + isar_shrink_factor conjecture_shape facts_offset + fact_names sym_tab params frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof @@ -1040,9 +1081,13 @@ else try isar_proof_for () |> the_default "\nWarning: The Isar proof construction failed." - in (one_line_proof ^ isar_proof, lemma_names) end + in one_line_proof ^ isar_proof end -fun proof_text ctxt isar_proof isar_params = - if isar_proof then isar_proof_text ctxt isar_params else metis_proof_text ctxt +fun proof_text ctxt isar_proof isar_params + (one_line_params as (preplay, _, _, _, _, _)) = + (if isar_proof orelse preplay = Preplay_Failed then + isar_proof_text ctxt isar_params + else + one_line_proof_text) one_line_params end; diff -r f617a5323d07 -r c4b9b4be90c4 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 @@ -11,7 +11,6 @@ type params = Sledgehammer_Provers.params val binary_min_facts : int Config.T - val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list val minimize_facts : string -> params -> bool option -> bool -> int -> int -> Proof.state -> ((string * locality) * thm list) list @@ -97,8 +96,6 @@ Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20) -fun filter_used_facts used = filter (member (op =) used o fst) - fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = case test (xs @ seen) of @@ -204,7 +201,7 @@ | prover :: _ => (kill_provers (); minimize_facts prover params NONE false i n state facts - |> #2 |> Output.urgent_message) + |> snd |> Output.urgent_message) end end; diff -r f617a5323d07 -r c4b9b4be90c4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 @@ -99,6 +99,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit + val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list val get_prover : Proof.context -> mode -> string -> prover end; @@ -306,6 +307,7 @@ type prover = params -> minimize_command -> prover_problem -> prover_result + (* configuration attributes *) val dest_dir = @@ -318,20 +320,6 @@ val measure_run_time = Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false) -fun with_path cleanup after f path = - Exn.capture f path - |> tap (fn _ => cleanup path) - |> Exn.release - |> tap (after path) - -fun proof_banner mode blocking name = - case mode of - Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" - | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" - | Normal => if blocking then quote name ^ " found a proof" - else "Try this" - | Minimize => "Try this" - val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) val smt_weights = @@ -379,6 +367,41 @@ fun overlord_file_location_for_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) +fun with_path cleanup after f path = + Exn.capture f path + |> tap (fn _ => cleanup path) + |> Exn.release + |> tap (after path) + +fun proof_banner mode blocking name = + case mode of + Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" + | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" + | Normal => if blocking then quote name ^ " found a proof" + else "Try this" + | Minimize => "Try this" + +(* based on "Mirabelle.can_apply" and generalized *) +fun try_apply timeout tac state i = + let + val {context = ctxt, facts, goal} = Proof.goal state + val full_tac = Method.insert_tac facts i THEN tac ctxt i + in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end + +fun try_metis debug timeout ths = + try_apply timeout (Config.put Metis_Tactics.verbose debug + #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) + +fun filter_used_facts used = filter (member (op =) used o fst) + +fun preplay_one_line_proof debug reconstructor_guess timeout ths state i = + let val timer = Timer.startRealTimer () in + case try_metis debug timeout ths state i of + SOME (SOME _) => Preplayed (Metis, Timer.checkRealTimer timer) + | SOME NONE => Preplay_Failed + | NONE => Trust_Playable (reconstructor_guess, SOME timeout) + end + (* generic TPTP-based ATPs *) @@ -485,7 +508,7 @@ conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) ({debug, verbose, overlord, blocking, type_sys, max_relevant, max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof, - isar_shrink_factor, slicing, timeout, ...} : params) + isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val thy = Proof.theory_of state @@ -708,7 +731,7 @@ extract_important_message output else "" - fun append_to_message message = + fun complete_message message = message ^ (if verbose then "\nATP real CPU time: " ^ @@ -719,21 +742,34 @@ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") - val isar_params = - (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) - val metis_params = - (proof_banner mode blocking name, minimize_command, type_sys, atp_proof, - facts_offset, fact_names, typed_helpers, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE => - (NONE, proof_text ctxt isar_proof isar_params metis_params - |>> append_to_message) - | SOME failure => - if failure = ProofMissing orelse failure = ProofIncomplete then - (NONE, metis_proof_text ctxt metis_params |>> append_to_message) - else - (outcome, (string_for_failure failure, [])) + let + val used_facts = + used_facts_in_atp_proof ctxt type_sys facts_offset fact_names + atp_proof + val reconstructor_guess = + if uses_typed_helpers typed_helpers atp_proof then MetisFT + else Metis + val ths = facts |> map untranslated_fact + |> filter_used_facts used_facts + |> map snd + val preplay = + preplay_one_line_proof debug reconstructor_guess preplay_timeout ths + state subgoal + val full_types = uses_typed_helpers typed_helpers atp_proof + val isar_params = + (debug, full_types, isar_shrink_factor, type_sys, pool, + conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof) + val one_line_params = + (preplay, proof_banner mode blocking name, used_facts, + minimize_command, goal, subgoal) + in + (NONE, (proof_text ctxt isar_proof isar_params one_line_params + |> complete_message, used_facts)) + end + | SOME failure => (outcome, (string_for_failure failure, [])) in {outcome = outcome, message = message, used_facts = used_facts, run_time_in_msecs = msecs} @@ -877,30 +913,6 @@ end in do_slice timeout 1 NONE Time.zeroTime end -(* based on "Mirabelle.can_apply" and generalized *) -fun try_apply timeout tac state i = - let - val {context = ctxt, facts, goal} = Proof.goal state - val full_tac = Method.insert_tac facts i THEN tac ctxt i - in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end - -fun try_metis debug timeout ths = - try_apply timeout (Config.put Metis_Tactics.verbose debug - #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) - -datatype metis_try = - Preplayed of string * Time.time | - Preplay_Timed_Out | - Preplay_Failed - -fun preplay debug timeout ths state i = - let val timer = Timer.startRealTimer () in - case try_metis debug timeout ths state i of - SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer) - | SOME NONE => Preplay_Failed - | NONE => Preplay_Timed_Out - end - fun run_smt_solver mode name (params as {debug, verbose, blocking, preplay_timeout, ...}) minimize_command @@ -920,14 +932,15 @@ NONE => let val (settings, method, time) = - case preplay debug preplay_timeout (map snd used_facts) state - subgoal of - Preplayed (method, time) => (method, "", SOME time) + case preplay_one_line_proof debug Metis preplay_timeout + (map snd used_facts) state subgoal of + Preplayed (method, time) => + ("", reconstructor_name method, SOME (false, time)) | _ => (if name = SMT_Solver.solver_name_of ctxt then "" else "smt_solver = " ^ maybe_quote name, "smt", NONE) in - try_command_line (proof_banner mode blocking name) + try_command_line (proof_banner mode blocking name) time (apply_on_subgoal settings subgoal subgoal_count ^ command_call method (map fst other_lemmas)) ^ minimize_line minimize_command diff -r f617a5323d07 -r c4b9b4be90c4 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:08 2011 +0200 @@ -11,6 +11,7 @@ val simplify_spaces : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val string_from_ext_time : bool * Time.time -> string val string_from_time : Time.time -> string val nat_subscript : int -> string val unyxml : string -> string @@ -67,8 +68,14 @@ SOME (seconds (the secs)) end -fun string_from_time t = - string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s" +fun string_from_ext_time (plus, time) = + let val ms = Time.toMilliseconds time in + if plus then signed_string_of_int ((ms + 999) div 1000) ^ "+ s" + else if ms < 1000 then signed_string_of_int ms ^ " ms" + else string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s" + end + +val string_from_time = string_from_ext_time o pair false val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) fun nat_subscript n =