--- 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
@@ -24,10 +24,11 @@
type minimize_command = string list -> string
type one_line_params =
- preplay * string * (string * locality) list * minimize_command * thm * int
+ preplay * string * (string * locality) list * minimize_command * int * int
type isar_params =
bool * bool * int * type_system * string Symtab.table * int list list
* int * (string * locality) list vector * int Symtab.table * string proof
+ * thm
val repair_conjecture_shape_and_fact_names :
type_system -> string -> int list list -> int
-> (string * locality) list vector -> int list
@@ -39,15 +40,6 @@
Proof.context -> type_system -> int list list -> int
-> (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 -> (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 one_line_proof_text : one_line_params -> string
val isar_proof_text :
Proof.context -> isar_params -> one_line_params -> string
@@ -77,10 +69,10 @@
type minimize_command = string list -> string
type one_line_params =
- preplay * string * (string * locality) list * minimize_command * thm * int
+ preplay * string * (string * locality) list * minimize_command * int * int
type isar_params =
bool * bool * int * type_system * string Symtab.table * int list list * int
- * (string * locality) list vector * int Symtab.table * string proof
+ * (string * locality) list vector * int Symtab.table * string proof * thm
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)
@@ -291,7 +283,7 @@
#> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
- goal, i) =
+ subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
val (reconstructor, ext_time) =
@@ -305,10 +297,10 @@
| SOME time =>
if time = Time.zeroTime then NONE else SOME (true, time))
| Failed_to_Preplay => (NONE, NONE)
- val n = Logic.count_prems (prop_of goal)
val try_line =
case reconstructor of
- SOME r => reconstructor_command r i n ([], map fst extra)
+ SOME r => ([], map fst extra)
+ |> reconstructor_command r subgoal subgoal_count
|> try_command_line banner ext_time
| NONE => "Proof reconstruction failed."
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
@@ -1054,13 +1046,12 @@
fun isar_proof_text ctxt
(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)) =
+ conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal)
+ (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
- val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i
+ val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
- val n = Logic.count_prems (prop_of goal)
val one_line_proof = one_line_proof_text one_line_params
fun isar_proof_for () =
case atp_proof
@@ -1072,7 +1063,7 @@
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt full_types i n of
+ |> string_for_proof ctxt full_types subgoal subgoal_count of
"" => "\nNo structured proof available (proof too short)."
| proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
--- 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
@@ -521,7 +521,8 @@
({debug, verbose, overlord, blocking, type_sys, max_relevant,
max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
- minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
+ minimize_command
+ ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -743,18 +744,7 @@
extract_important_message output
else
""
- fun complete_message message =
- message ^
- (if verbose then
- "\nATP real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
- else
- "") ^
- (if important_message <> "" then
- "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
- else
- "")
- val (outcome, (message, used_facts)) =
+ val (message, used_facts) =
case outcome of
NONE =>
let
@@ -764,24 +754,36 @@
val reconstructor =
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 used_ths =
+ facts |> map untranslated_fact
+ |> filter_used_facts used_facts
+ |> map snd
val preplay =
- preplay_one_line_proof debug preplay_timeout ths state subgoal
+ preplay_one_line_proof debug preplay_timeout used_ths state subgoal
reconstructor
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)
+ conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
+ goal)
val one_line_params =
(preplay, proof_banner mode blocking name, used_facts,
- minimize_command, goal, subgoal)
+ minimize_command, subgoal, subgoal_count)
in
- (NONE, (proof_text ctxt isar_proof isar_params one_line_params
- |> complete_message, used_facts))
+ (proof_text ctxt isar_proof isar_params one_line_params ^
+ (if verbose then
+ "\nATP real CPU time: " ^
+ string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+ else
+ "") ^
+ (if important_message <> "" then
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+ important_message
+ else
+ ""),
+ used_facts)
end
- | SOME failure => (outcome, (string_for_failure failure, []))
+ | SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, used_facts = used_facts,
run_time_in_msecs = msecs}
@@ -937,26 +939,25 @@
|> map (smt_weighted_fact ctxt num_facts)
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop ctxt name params state subgoal smt_filter facts
- val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
+ val (used_facts, used_ths) = used_facts |> ListPair.unzip
val outcome = outcome |> Option.map failure_from_smt_failure
val message =
case outcome of
NONE =>
let
- val (settings, method, time) =
- case preplay_one_line_proof debug preplay_timeout
- (map snd used_facts) state subgoal Metis 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)
+ fun smt_settings () =
+ if name = SMT_Solver.solver_name_of ctxt then ""
+ else "smt_solver = " ^ maybe_quote name
+ val preplay =
+ case preplay_one_line_proof debug preplay_timeout used_ths state
+ subgoal Metis of
+ p as Preplayed _ => p
+ | _ => Trust_Playable (SMT (smt_settings ()), NONE)
+ val one_line_params =
+ (preplay, proof_banner mode blocking name, used_facts,
+ minimize_command, subgoal, subgoal_count)
in
- 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
- (map fst (other_lemmas @ chained_lemmas)) ^
+ one_line_proof_text one_line_params ^
(if verbose then
"\nSMT solver real CPU time: " ^
string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
@@ -966,7 +967,7 @@
end
| SOME failure => string_for_failure failure
in
- {outcome = outcome, used_facts = map fst used_facts,
+ {outcome = outcome, used_facts = used_facts,
run_time_in_msecs = run_time_in_msecs, message = message}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200
@@ -61,7 +61,7 @@
(if blocking then
"."
else
- ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+ "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
val auto_minimize_min_facts =
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}