--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200
@@ -15,9 +15,6 @@
val proverK = "prover" (*=NAME: name of the external prover to call*)
val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*)
-val minimizeK = "minimize" (*: enable minimization of theorem set found by sledgehammer*)
- (*refers to minimization attempted by Mirabelle*)
-val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*)
val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
@@ -43,7 +40,6 @@
val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
-fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
val separator = "-----"
@@ -60,7 +56,6 @@
val slice_default = "true"
val max_calls_default = "10000000"
val trivial_default = "false"
-val minimize_timeout_default = 5
(*If a key is present in args then augment a list with its pair*)
(*This is used to avoid fixing default values at the Mirabelle level, and
@@ -93,11 +88,6 @@
posns: (Position.T * bool) list
}
-datatype min_data = MinData of {
- succs: int,
- ab_ratios: int
- }
-
fun make_sh_data
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
time_prover,time_prover_fail) =
@@ -106,9 +96,6 @@
time_isa=time_isa, time_prover=time_prover,
time_prover_fail=time_prover_fail}
-fun make_min_data (succs, ab_ratios) =
- MinData{succs=succs, ab_ratios=ab_ratios}
-
fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
timeout,lemmas,posns) =
ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,
@@ -116,7 +103,6 @@
timeout=timeout, lemmas=lemmas, posns=posns}
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
-val empty_min_data = make_min_data (0, 0)
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
@@ -124,55 +110,37 @@
time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
-fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
-
fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
nontriv_success, proofs, time, timeout, lemmas, posns)
-datatype proof_method_mode =
- Unminimized | Minimized | UnminimizedFT | MinimizedFT
+datatype proof_method_mode = Unminimized | UnminimizedFT
datatype data = Data of {
sh: sh_data,
- min: min_data,
re_u: re_data, (* proof method with unminimized set of lemmas *)
- re_m: re_data, (* proof method with minimized set of lemmas *)
- re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *)
- re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *)
- mini: bool (* with minimization *)
+ re_uft: re_data (* proof method with unminimized set of lemmas and fully-typed *)
}
-fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =
- Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,
- mini=mini}
+fun make_data (sh, re_u, re_uft) = Data {sh=sh, re_u=re_u, re_uft=re_uft}
-val empty_data = make_data (empty_sh_data, empty_min_data,
- empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)
-
-fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
- let val sh' = make_sh_data (f (tuple_of_sh_data sh))
- in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end
+val empty_data = make_data (empty_sh_data, empty_re_data, empty_re_data)
-fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
- let val min' = make_min_data (f (tuple_of_min_data min))
- in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end
+fun map_sh_data f (Data {sh, re_u, re_uft}) =
+ let val sh' = make_sh_data (f (tuple_of_sh_data sh))
+ in make_data (sh', re_u, re_uft) end
-fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
+fun map_re_data f m (Data {sh, re_u, re_uft}) =
let
- fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft)
- | map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft)
- | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
- | map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft)
+ fun map_me g Unminimized (u, uft) = (g u, uft)
+ | map_me g UnminimizedFT (u, uft) = (u, g uft)
val f' = make_re_data o f o tuple_of_re_data
- val (re_u', re_m', re_uft', re_mft') =
- map_me f' m (re_u, re_m, re_uft, re_mft)
- in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end
+ val (re_u', re_uft') = map_me f' m (re_u, re_uft)
+ in make_data (sh, re_u', re_uft') end
-fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =
- make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)
+fun set_mini (Data {sh, re_u, re_uft, ...}) = make_data (sh, re_u, re_uft)
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
@@ -212,12 +180,6 @@
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
-val inc_min_succs = map_min_data
- (fn (succs,ab_ratios) => (succs+1, ab_ratios))
-
-fun inc_min_ab_ratios r = map_min_data
- (fn (succs, ab_ratios) => (succs, ab_ratios+r))
-
val inc_proof_method_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
@@ -311,14 +273,9 @@
else ()
)
-fun log_min_data log (succs, ab_ratios) =
- (log ("Number of successful minimizations: " ^ string_of_int succs);
- log ("After/before ratios: " ^ string_of_int ab_ratios)
- )
-
in
-fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
+fun log_data id log (Data {sh, re_u, re_uft}) =
let
val ShData {calls=sh_calls, ...} = sh
@@ -333,15 +290,7 @@
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
log_sh_data log (tuple_of_sh_data sh);
log "";
- if not mini
- then log_proof_method ("", re_u) ("fully-typed ", re_uft)
- else
- app_if re_u (fn () =>
- (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
- log "";
- app_if re_m (fn () =>
- (log_min_data log (tuple_of_min_data min); log "";
- log_proof_method ("", re_m) ("fully-typed ", re_mft))))))
+ log_proof_method ("", re_u) ("fully-typed ", re_uft))
else ()
end
@@ -573,60 +522,6 @@
end
-fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
- let
- val thy = Proof.theory_of st
- val {goal, ...} = Proof.goal st
- val i = 1
- val preferred_methss =
- (Sledgehammer_Proof_Methods.Auto_Method, [[Sledgehammer_Proof_Methods.Auto_Method]]) (* wrong *)
- val n0 = length (these (!named_thms))
- val prover_name = get_prover_name thy args
- val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
- val strict = AList.lookup (op =) args strictK |> the_default strict_default
- val timeout =
- AList.lookup (op =) args minimize_timeoutK
- |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
- |> the_default minimize_timeout_default
- val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
- |> the_default preplay_timeout_default
- val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs"
- val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
- val max_new_mono_instancesLST =
- available_parameter args max_new_mono_instancesK max_new_mono_instancesK
- val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
- val params as {preplay_timeout, ...} = Sledgehammer_Commands.default_params thy
- ([("provers", prover_name),
- ("verbose", "true"),
- ("type_enc", type_enc),
- ("strict", strict),
- ("timeout", string_of_int timeout),
- ("preplay_timeout", preplay_timeout)]
- |> isar_proofsLST
- |> sh_minimizeLST (*don't confuse the two minimization flags*)
- |> max_new_mono_instancesLST
- |> max_mono_itersLST)
- val minimize =
- Sledgehammer_Prover_Minimize.minimize_facts (K ()) prover_name params true 1
- (Sledgehammer_Util.subgoal_count st)
- val _ = log separator
- val (used_facts, message) = minimize st goal (these (!named_thms))
- val msg = message (fn () => Sledgehammer.play_one_line_proof preplay_timeout
- (map fst (these used_facts)) st i preferred_methss)
- in
- (case used_facts of
- SOME named_thms' =>
- (change_data id inc_min_succs;
- change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
- if length named_thms' = n0
- then log (minimize_tag id ^ "already minimal")
- else (meth := proof_method_from_msg args msg;
- named_thms := SOME named_thms';
- log (minimize_tag id ^ "succeeded:\n" ^ msg))
- )
- | NONE => log (minimize_tag id ^ "failed: " ^ msg))
- end
-
fun override_params prover type_enc timeout =
[("provers", prover),
("max_facts", "0"),
@@ -726,7 +621,6 @@
val meth = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
- val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
val trivial =
if AList.lookup (op =) args check_trivialK |> the_default trivial_default
@@ -747,17 +641,9 @@
(Mirabelle.catch_result (proof_method_tag meth) false
(run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
in
- change_data id (set_mini minimize);
+ change_data id set_mini;
Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
- if is_some (!named_thms)
- then
- (apply_method Unminimized UnminimizedFT;
- if minimize andalso not (null (these (!named_thms)))
- then
- (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st;
- apply_method Minimized MinimizedFT)
- else ())
- else ()
+ if is_some (!named_thms) then apply_method Unminimized UnminimizedFT else ()
end
end
end