# HG changeset patch # User blanchet # Date 1379709570 -7200 # Node ID eba0d1c069b8938a8e8a53838571fab144b511bc # Parent 70d370743dc663c36eb0177d21904901d4a17e4f merged "isar_try0" and "isar_minimize" options diff -r 70d370743dc6 -r eba0d1c069b8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200 @@ -94,8 +94,7 @@ ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("isar_compress", "10"), - ("isar_try0", "true"), (* TODO: document *) - ("isar_minimize", "true"), (* TODO: document *) + ("isar_try0", "true"), ("slice", "true"), ("minimize", "smart"), ("preplay_timeout", "3")] @@ -116,8 +115,7 @@ ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), - ("dont_try0_isar", "isar_try0"), - ("dont_minimize_isar", "isar_minimize")] + ("dont_try0_isar", "isar_try0")] val params_not_for_minimize = ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", @@ -304,7 +302,6 @@ val isar_proofs = lookup_option lookup_bool "isar_proofs" val isar_compress = Real.max (1.0, lookup_real "isar_compress") val isar_try0 = lookup_bool "isar_try0" - val isar_minimize = lookup_bool "isar_minimize" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" @@ -320,9 +317,9 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_compress = isar_compress, isar_try0 = isar_try0, - isar_minimize = isar_minimize, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r 70d370743dc6 -r eba0d1c069b8 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200 @@ -57,8 +57,8 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, - uncurried_aliases, isar_proofs, isar_compress, - isar_try0, isar_minimize, preplay_timeout, ...} : params) + uncurried_aliases, isar_proofs, isar_compress, isar_try0, + preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let val _ = @@ -80,9 +80,8 @@ fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, isar_compress = isar_compress, - isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = false, - minimize = SOME false, timeout = timeout, - preplay_timeout = preplay_timeout, expect = ""} + isar_try0 = isar_try0, slice = false, minimize = SOME false, + timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} @@ -252,8 +251,8 @@ ({debug, verbose, overlord, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, - isar_compress, isar_try0, isar_minimize, slice, minimize, timeout, - preplay_timeout, expect} : params) = + isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout, + expect} : params) = let fun lookup_override name default_value = case AList.lookup (op =) override_params name of @@ -270,9 +269,9 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_compress = isar_compress, isar_try0 = isar_try0, - isar_minimize = isar_minimize, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun maybe_minimize ctxt mode do_learn name diff -r 70d370743dc6 -r eba0d1c069b8 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Sep 20 22:39:30 2013 +0200 @@ -49,8 +49,8 @@ mk_step_lfs_gfs min_lfs min_gfs end) -fun minimize_dependencies_and_remove_unrefed_steps - isar_minimize preplay_interface proof = +fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface + proof = let fun cons_to xs x = x :: xs @@ -86,7 +86,7 @@ and do_refed_step step = step - |> isar_minimize ? min_deps_of_step preplay_interface + |> isar_try0 ? min_deps_of_step preplay_interface |> do_refed_step' and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" @@ -101,7 +101,6 @@ in (refed, step) end - in snd (do_proof proof) end diff -r 70d370743dc6 -r eba0d1c069b8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200 @@ -37,7 +37,6 @@ isar_proofs : bool option, isar_compress : real, isar_try0 : bool, - isar_minimize : bool, slice : bool, minimize : bool option, timeout : Time.time option, @@ -349,7 +348,6 @@ isar_proofs : bool option, isar_compress : real, isar_try0 : bool, - isar_minimize : bool, slice : bool, minimize : bool option, timeout : Time.time option, @@ -675,8 +673,7 @@ (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, isar_compress, - isar_try0, isar_minimize, slice, timeout, - preplay_timeout, ...}) + isar_try0, slice, timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -952,8 +949,7 @@ () val isar_params = (debug, verbose, preplay_timeout, isar_compress, isar_try0, - isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, - goal) + pool, fact_names, lifted, sym_tab, atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command ctxt params minimize_command name diff -r 70d370743dc6 -r eba0d1c069b8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200 @@ -12,7 +12,7 @@ type one_line_params = Sledgehammer_Print.one_line_params type isar_params = - bool * bool * Time.time option * real * bool * bool * string Symtab.table + bool * bool * Time.time option * real * bool * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string atp_proof * thm @@ -408,13 +408,13 @@ in chain_proof end type isar_params = - bool * bool * Time.time option * real * bool * bool * string Symtab.table + bool * bool * Time.time option * real * bool * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string atp_proof * thm fun isar_proof_text ctxt isar_proofs - (debug, verbose, preplay_timeout, isar_compress, isar_try0, isar_minimize, - pool, fact_names, lifted, sym_tab, atp_proof, goal) + (debug, verbose, preplay_timeout, isar_compress, isar_try0, pool, + fact_names, lifted, sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt @@ -592,7 +592,7 @@ (if isar_proofs = SOME true then isar_compress else 1000.0) preplay_interface |> isar_try0 ? try0 preplay_timeout preplay_interface - |> minimize_dependencies_and_remove_unrefed_steps isar_minimize + |> minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface |> `overall_preplay_stats ||> clean_up_labels_in_proof