--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
@@ -137,6 +137,7 @@
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
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -279,8 +280,8 @@
|> relabel_isar_proof_canonically
val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
- preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
- preplay_timeout isar_proof
+ preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout
+ isar_proof
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
@@ -299,8 +300,7 @@
val (play_outcome, isar_proof) =
isar_proof
|> tap (trace_isar_proof "Original")
- |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
- preplay_data
+ |> compress_isar_proof compress_isar preplay_data
|> tap (trace_isar_proof "Compressed")
|> try0_isar ? try0_isar_proof preplay_timeout preplay_data
|> tap (trace_isar_proof "Tried0")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -21,7 +21,7 @@
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
- val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
+ val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
isar_proof -> isar_preplay_data
end;
@@ -172,67 +172,60 @@
Precondition: The proof must be labeled canonically; cf.
"Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
-fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
- if not do_preplay then
- (* the "dont_preplay" option pretends that everything works just fine *)
- {set_preplay_outcomes = K (K ()),
- preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
- preplay_quietly = K (K (Played Time.zeroTime)),
- overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
- else
- let
- val ctxt = enrich_context_with_local_facts proof ctxt
+fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans preplay_timeout proof =
+ let
+ val ctxt = enrich_context_with_local_facts proof ctxt
- fun preplay quietly timeout meth step =
- preplay_raw debug type_enc lam_trans ctxt timeout meth step
- handle exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (if not quietly andalso debug then
- warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
- else
- ();
- Play_Failed)
+ fun preplay quietly timeout meth step =
+ preplay_raw debug type_enc lam_trans ctxt timeout meth step
+ handle exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (if not quietly andalso debug then
+ warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
+ else
+ ();
+ Play_Failed)
- (* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
- preplay true timeout meth step
- | preplay_quietly _ _ = Played Time.zeroTime
+ (* preplay steps treating exceptions like timeouts *)
+ fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
+ preplay true timeout meth step
+ | preplay_quietly _ _ = Played Time.zeroTime
- val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
+ val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
+
+ fun set_preplay_outcomes l meths_outcomes =
+ preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
+ (!preplay_tab)
- fun set_preplay_outcomes l meths_outcomes =
- preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
- (!preplay_tab)
+ fun preplay_outcome l meth =
+ (case Canonical_Label_Tab.lookup (!preplay_tab) l of
+ SOME meths_outcomes =>
+ (case AList.lookup (op =) meths_outcomes meth of
+ SOME outcome => outcome
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- fun preplay_outcome l meth =
- (case Canonical_Label_Tab.lookup (!preplay_tab) l of
- SOME meths_outcomes =>
- (case AList.lookup (op =) meths_outcomes meth of
- SOME outcome => outcome
- | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
- | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
-
- fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
- Lazy.force (preplay_outcome l meth)
- | result_of_step _ = Played Time.zeroTime
+ fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
+ Lazy.force (preplay_outcome l meth)
+ | result_of_step _ = Played Time.zeroTime
- fun overall_preplay_outcome (Proof (_, _, steps)) =
- fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
+ fun overall_preplay_outcome (Proof (_, _, steps)) =
+ fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
- fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
- preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
- (!preplay_tab)
- | reset_preplay_outcomes _ = ()
+ fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+ preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
+ (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
+ (!preplay_tab)
+ | reset_preplay_outcomes _ = ()
- val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
- in
- {set_preplay_outcomes = set_preplay_outcomes,
- preplay_outcome = preplay_outcome,
- preplay_quietly = preplay_quietly,
- overall_preplay_outcome = overall_preplay_outcome}
- end
+ val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
+ in
+ {set_preplay_outcomes = set_preplay_outcomes,
+ preplay_outcome = preplay_outcome,
+ preplay_quietly = preplay_quietly,
+ overall_preplay_outcome = overall_preplay_outcome}
+ end
end;