--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 09:28:20 2013 +0100
@@ -464,7 +464,7 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play
+ preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed
Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 09:28:20 2013 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
Compression of isar proofs by merging steps.
Only proof steps using the same proof method are merged.
@@ -170,13 +170,13 @@
| _ => raise Fail "Sledgehammer_Compress: elim_subproofs'")
fun elim_subproofs (step as Let _) = step
- | elim_subproofs
- (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
- if subproofs = [] then step else
- case get_preplay_time l of
- (true, _) => step (* timeout or fail *)
- | (false, time) =>
- elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+ if subproofs = [] then
+ step
+ else
+ (case get_preplay_time l of
+ (true, _) => step (* timeout or fail *)
+ | (false, time) => elim_subproofs' time qs fix l t lfs gfs meth subproofs [])
(** top_level compression: eliminate steps by merging them into their
successors **)
@@ -229,8 +229,7 @@
val succs = collect_successors steps' succ_lbls
val succs' = map (try_merge cand #> the) succs
- (* TODO: should be lazy: stop preplaying as soon as one step
- fails/times out *)
+ (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
val preplay_times = map2 preplay_quietly timeouts succs'
(* ensure none of the modified successors timed out *)
@@ -243,8 +242,7 @@
decrement_step_count (); (* candidate successfully eliminated *)
map2 set_preplay_time succ_lbls preplay_times;
map (replace_successor l succ_lbls) lfs;
- (* removing the step would mess up the indices
- -> replace with dummy step instead *)
+ (* removing the step would mess up the indices -> replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
end
handle Bind => steps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 09:28:20 2013 +0100
@@ -239,8 +239,7 @@
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
- (NONE, (Lazy.value (Failed_to_Play plain_metis),
- fn _ => "Error: " ^ msg, ""))
+ (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
end
fun adjust_reconstructor_params override_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 09:28:20 2013 +0100
@@ -28,8 +28,7 @@
| min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
(case get_preplay_time l of
- (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
- (true, _) => step
+ (true, _) => step (* don't touch steps that time out or fail *)
| (false, time) =>
let
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
@@ -69,12 +68,12 @@
(case label_of_step step of
NONE => (refed, step :: accu)
| SOME l =>
- if Ord_List.member label_ord refed l then
- do_refed_step step
- |>> Ord_List.union label_ord refed
- ||> (fn x => x :: accu)
- else
- (refed, accu))
+ if Ord_List.member label_ord refed l then
+ do_refed_step step
+ |>> Ord_List.union label_ord refed
+ ||> (fn x => x :: accu)
+ else
+ (refed, accu))
and do_refed_step step = step |> postproc_step |> do_refed_step'
and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
| do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 09:28:20 2013 +0100
@@ -132,9 +132,10 @@
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
- val thesis = Term.Free ("thesis", HOLogic.boolT)
+ (* FIXME: generate fresh name *)
+ val thesis = Free ("thesis", HOLogic.boolT)
val thesis_prop = thesis |> HOLogic.mk_Trueprop
- val frees = map Term.Free xs
+ val frees = map Free xs
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 09:28:20 2013 +0100
@@ -88,12 +88,12 @@
val (failed, reconstr, ext_time) =
case preplay of
Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Trust_Playable (reconstr, time) =>
+ | Play_Timed_Out (reconstr, time) =>
(false, reconstr,
(case time of
NONE => NONE
| SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
- | Failed_to_Play reconstr => (true, reconstr, NONE)
+ | Play_Failed reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
|> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 09:28:20 2013 +0100
@@ -403,16 +403,15 @@
else List.last reconstrs
in
if timeout = SOME Time.zeroTime then
- Trust_Playable (get_preferred reconstrs, NONE)
+ Play_Timed_Out (get_preferred reconstrs, NONE)
else
let
val _ =
if mode = Minimize then Output.urgent_message "Preplaying proof..."
else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
- fun play [] [] = Failed_to_Play (get_preferred reconstrs)
- | play timed_outs [] =
- Trust_Playable (get_preferred timed_outs, timeout)
+ fun play [] [] = Play_Failed (get_preferred reconstrs)
+ | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
| play timed_out (reconstr :: reconstrs) =
let
val _ =
@@ -861,8 +860,7 @@
""))
end
| SOME failure =>
- ([], Lazy.value (Failed_to_Play plain_metis),
- fn _ => string_of_atp_failure failure, "")
+ ([], Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,
run_time = run_time, preplay = preplay, message = message,
@@ -1063,7 +1061,7 @@
else
"")
| SOME failure =>
- (Lazy.value (Failed_to_Play plain_metis),
+ (Lazy.value (Play_Failed plain_metis),
fn _ => string_of_atp_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,
@@ -1108,7 +1106,7 @@
message_tail = ""}
| play =>
let
- val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
+ val failure = case play of Play_Failed _ => GaveUp | _ => TimedOut
in
{outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime, preplay = Lazy.value play,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 09:28:20 2013 +0100
@@ -410,8 +410,8 @@
fun isar_proof_would_be_a_good_idea preplay =
(case preplay of
Played (reconstr, _) => reconstr = SMT
- | Trust_Playable _ => false
- | Failed_to_Play _ => true)
+ | Play_Timed_Out _ => false
+ | Play_Failed _ => true)
fun proof_text ctxt isar_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 09:28:20 2013 +0100
@@ -15,8 +15,8 @@
datatype play =
Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
+ Play_Timed_Out of reconstructor * Time.time option |
+ Play_Failed of reconstructor
type minimize_command = string list -> string
type one_line_params = play * string * (string * stature) list * minimize_command * int * int
@@ -35,8 +35,8 @@
datatype play =
Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
+ Play_Timed_Out of reconstructor * Time.time option |
+ Play_Failed of reconstructor
type minimize_command = string list -> string
type one_line_params = play * string * (string * stature) list * minimize_command * int * int