--- 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;
--- 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;
--- 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
--- 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 =