--- 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
@@ -17,7 +17,6 @@
val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*)
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*)
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
@@ -114,33 +113,24 @@
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
nontriv_success, proofs, time, timeout, lemmas, posns)
-datatype proof_method_mode = Unminimized | UnminimizedFT
-
datatype data = Data of {
sh: sh_data,
- re_u: re_data, (* proof method with unminimized set of lemmas *)
- re_uft: re_data (* proof method with unminimized set of lemmas and fully-typed *)
+ re_u: re_data (* proof method with unminimized set of lemmas *)
}
-fun make_data (sh, re_u, re_uft) = Data {sh=sh, re_u=re_u, re_uft=re_uft}
+fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u}
-val empty_data = make_data (empty_sh_data, empty_re_data, empty_re_data)
+val empty_data = make_data (empty_sh_data, empty_re_data)
-fun map_sh_data f (Data {sh, re_u, re_uft}) =
+fun map_sh_data f (Data {sh, re_u}) =
let val sh' = make_sh_data (f (tuple_of_sh_data sh))
- in make_data (sh', re_u, re_uft) end
+ in make_data (sh', re_u) end
-fun map_re_data f m (Data {sh, re_u, re_uft}) =
+fun map_re_data f (Data {sh, re_u}) =
let
- 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_uft') = map_me f' m (re_u, re_uft)
- in make_data (sh, re_u', re_uft') end
-
-fun set_mini (Data {sh, re_u, re_uft, ...}) = make_data (sh, re_u, re_uft)
+ val re_u' = f' re_u
+ in make_data (sh, re_u') end
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
@@ -200,21 +190,21 @@
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
-fun inc_proof_method_time m t = map_re_data
+fun inc_proof_method_time t = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
- => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
+ => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns))
val inc_proof_method_timeout = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
-fun inc_proof_method_lemmas m n = map_re_data
+fun inc_proof_method_lemmas n = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
- => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
+ => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns))
-fun inc_proof_method_posns m pos = map_re_data
+fun inc_proof_method_posns pos = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
- => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
+ => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns))
val str0 = string_of_int o the_default 0
@@ -275,22 +265,21 @@
in
-fun log_data id log (Data {sh, re_u, re_uft}) =
+fun log_data id log (Data {sh, re_u}) =
let
val ShData {calls=sh_calls, ...} = sh
fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
fun log_re tag m =
log_re_data log tag sh_calls (tuple_of_re_data m)
- fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
- (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
+ fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log ""))
in
if sh_calls > 0
then
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
log_sh_data log (tuple_of_sh_data sh);
log "";
- log_proof_method ("", re_u) ("fully-typed ", re_uft))
+ log_proof_method ("", re_u))
else ()
end
@@ -530,7 +519,7 @@
("slice", "false"),
("timeout", timeout |> Time.toSeconds |> string_of_int)]
-fun run_proof_method trivial full m name meth named_thms id
+fun run_proof_method trivial full name meth named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
fun do_method named_thms ctxt =
@@ -577,22 +566,22 @@
Mirabelle.can_apply timeout (do_method named_thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
- | with_time (true, t) = (change_data id (inc_proof_method_success m);
+ | with_time (true, t) = (change_data id inc_proof_method_success;
if trivial then ()
- else change_data id (inc_proof_method_nontriv_success m);
- change_data id (inc_proof_method_lemmas m (length named_thms));
- change_data id (inc_proof_method_time m t);
- change_data id (inc_proof_method_posns m (pos, trivial));
- if name = "proof" then change_data id (inc_proof_method_proofs m) else ();
+ else change_data id inc_proof_method_nontriv_success;
+ change_data id (inc_proof_method_lemmas (length named_thms));
+ change_data id (inc_proof_method_time t);
+ change_data id (inc_proof_method_posns (pos, trivial));
+ if name = "proof" then change_data id inc_proof_method_proofs else ();
"succeeded (" ^ string_of_int t ^ ")")
fun timed_method named_thms =
(with_time (Mirabelle.cpu_time apply_method named_thms), true)
- handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false))
+ handle TimeLimit.TimeOut => (change_data id inc_proof_method_timeout; ("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
val _ = log separator
- val _ = change_data id (inc_proof_method_calls m)
- val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m)
+ val _ = change_data id inc_proof_method_calls
+ val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls
in
named_thms
|> timed_method
@@ -621,29 +610,18 @@
val meth = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
- val metis_ft = AList.defined (op =) args metis_ftK
val trivial =
if AList.lookup (op =) args check_trivialK |> the_default trivial_default
|> Markup.parse_bool then
Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
else false
- fun apply_method m1 m2 =
- if metis_ft
- then
- if not (Mirabelle.catch_result (proof_method_tag meth) false
- (run_proof_method trivial false m1 name meth (these (!named_thms))) id st)
- then
- (Mirabelle.catch_result (proof_method_tag meth) false
- (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ())
- else ()
- else
- (Mirabelle.catch_result (proof_method_tag meth) false
- (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
+ fun apply_method () =
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false name meth (these (!named_thms))) id st; ())
in
- 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 else ()
+ if is_some (!named_thms) then apply_method () else ()
end
end
end