--- a/src/HOL/Sledgehammer.thy Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Feb 03 10:14:18 2014 +0100
@@ -22,7 +22,6 @@
ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_try0.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100
@@ -16,7 +16,7 @@
val trace : bool Config.T
type isar_params =
- bool * (string option * string option) * Time.time * real * bool
+ bool * (string option * string option) * Time.time * real * bool * bool
* (term, string) atp_step list * thm
val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
@@ -35,7 +35,6 @@
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Compress
-open Sledgehammer_Isar_Try0
open Sledgehammer_Isar_Minimize
structure String_Redirect = ATP_Proof_Redirect(
@@ -109,8 +108,8 @@
end
type isar_params =
- bool * (string option * string option) * Time.time * real * bool * (term, string) atp_step list
- * thm
+ bool * (string option * string option) * Time.time * real * bool * bool
+ * (term, string) atp_step list * thm
val arith_methods =
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
@@ -129,8 +128,8 @@
let
fun isar_proof_of () =
let
- val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, atp_proof,
- goal) = try isar_params ()
+ val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
+ atp_proof, goal) = try isar_params ()
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
@@ -139,7 +138,6 @@
val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
val do_preplay = preplay_timeout <> Time.zeroTime
- val try0_isar = try0_isar andalso do_preplay
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
@@ -311,11 +309,10 @@
|> tap (trace_isar_proof "Original")
|> compress_isar_proof ctxt compress_isar preplay_data
|> tap (trace_isar_proof "Compressed")
- |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
|> tap (trace_isar_proof "Tried0")
|> postprocess_isar_proof_remove_unreferenced_steps
(keep_fastest_method_of_isar_step (!preplay_data)
- #> try0_isar(*### minimize*) ? minimize_isar_step_dependencies ctxt preplay_data)
+ #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `(preplay_outcome_of_isar_proof (!preplay_data))
||> chain_isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Mon Feb 03 10:14:18 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
- Author: Steffen Juilf Smolka, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Try replacing calls to "metis" with calls to other proof methods to speed up proofs, eliminate
-dependencies, and repair broken proof steps.
-*)
-
-signature SLEDGEHAMMER_ISAR_TRY0 =
-sig
- type isar_proof = Sledgehammer_Isar_Proof.isar_proof
- type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
-
- val try0_isar_proof : Proof.context -> Time.time -> isar_preplay_data Unsynchronized.ref ->
- isar_proof -> isar_proof
-end;
-
-structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Isar_Proof
-open Sledgehammer_Isar_Preplay
-
-fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) =
- Prove (qs, xs, l, t, subproofs, (facts, [meth]))
-
-val slack = seconds 0.05
-
-fun try0_step _ _ _ (step as Let _) = step
- | try0_step ctxt preplay_timeout preplay_data
- (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
- let
- val timeout =
- (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
- Played time => Time.+ (time, slack)
- | _ => preplay_timeout)
-
- fun try_method meth =
- (case preplay_isar_step ctxt timeout meth step of
- outcome as Played _ => SOME (meth, outcome)
- | _ => NONE)
- in
- (* FIXME: create variant after success *)
- (case Par_List.get_some try_method meths of
- SOME (meth', outcome) =>
- let val step' = step_with_method meth' step in
- (set_preplay_outcomes_of_isar_step ctxt timeout preplay_data step'
- [(meth', Lazy.value outcome)];
- step')
- end
- | NONE => step)
- end
-
-val try0_isar_proof = map_isar_steps ooo try0_step
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 10:14:18 2014 +0100
@@ -132,7 +132,7 @@
fun run_atp mode name
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
- try0_isar, slice, timeout, preplay_timeout, ...})
+ try0_isar, slice, minimize, timeout, preplay_timeout, ...})
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -372,7 +372,7 @@
|> factify_atp_proof fact_names hyp_ts concl_t
in
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
- try0_isar, atp_proof, goal)
+ try0_isar, minimize |> the_default true, atp_proof, goal)
end
val one_line_params =
(preplay, proof_banner mode name, used_facts,