# HG changeset patch # User blanchet # Date 1391418858 -3600 # Node ID e68fd012bbf3c8d3d751c8a72359bbf78966d331 # Parent d9d31354834e286c117575b3264d654f49a0846e got rid of 'try0' step that is now redundant diff -r d9d31354834e -r e68fd012bbf3 src/HOL/Sledgehammer.thy --- 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" diff -r d9d31354834e -r e68fd012bbf3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.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 diff -r d9d31354834e -r e68fd012bbf3 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- 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; diff -r d9d31354834e -r e68fd012bbf3 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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,