--- 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
@@ -307,12 +307,12 @@
val (play_outcome, isar_proof) =
canonical_isar_proof
|> tap (trace_isar_proof "Original")
- |> compress_isar_proof compress_isar preplay_data
+ |> compress_isar_proof preplay_ctxt compress_isar preplay_data
|> tap (trace_isar_proof "Compressed")
- |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
+ |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
|> tap (trace_isar_proof "Tried0")
|> postprocess_isar_proof_remove_unreferenced_steps
- (try0_isar ? minimize_isar_step_dependencies preplay_data)
+ (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `overall_preplay_outcome
||> chain_isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
@@ -11,7 +11,7 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val compress_isar_proof : real -> isar_preplay_data -> isar_proof -> isar_proof
+ val compress_isar_proof : Proof.context -> real -> isar_preplay_data -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
@@ -97,8 +97,8 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
-fun compress_isar_proof compress_isar
- ({preplay_step, preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof =
+fun compress_isar_proof ctxt compress_isar
+ ({preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
@@ -162,7 +162,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = time_mult merge_timeout_slack (Time.+ (time, time'))
- val Played time'' = preplay_step timeout (hd meths)(*FIXME*) step''
+ val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step''
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
@@ -238,7 +238,7 @@
()
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val play_outcomes = map3 preplay_step timeouts succ_meths succs'
+ val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
(* ensure none of the modified successors timed out *)
val true = forall (fn Played _ => true) play_outcomes
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
@@ -11,7 +11,7 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step
+ val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data -> isar_step -> isar_step
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
isar_proof
end;
@@ -25,8 +25,8 @@
val slack = seconds 0.1
-fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies {preplay_step, set_preplay_outcomes, preplay_outcome, ...}
+fun minimize_isar_step_dependencies _ (_ : isar_preplay_data) (step as Let _) = step
+ | minimize_isar_step_dependencies ctxt {set_preplay_outcomes, preplay_outcome, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
(case Lazy.force (preplay_outcome l meth) of
Played time =>
@@ -36,7 +36,8 @@
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
- (case preplay_step (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of
+ (case preplay_isar_step ctxt (Time.+ (time, slack)) meth
+ (mk_step (min_facts @ facts)) of
Played time => minimize_facts mk_step time min_facts facts
| _ => minimize_facts mk_step time (f :: min_facts) facts)
--- 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
@@ -16,12 +16,12 @@
val trace : bool Config.T
type isar_preplay_data =
- {preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
- set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
+ {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
overall_preplay_outcome: isar_proof -> play_outcome}
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
+ val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
val preplay_data_of_isar_proof : Proof.context -> Time.time -> isar_proof -> isar_preplay_data
end;
@@ -116,47 +116,49 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step ctxt timeout meth
- (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
- let
- val goal =
- (case xs of
- [] => t
- | _ =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
- (cf. "~~/src/Pure/Isar/obtain.ML") *)
- let
- (* FIXME: generate fresh name *)
- val thesis = Free ("thesis_preplay", HOLogic.boolT)
- val thesis_prop = HOLogic.mk_Trueprop thesis
- val frees = map Free xs
+fun raw_preplay_step ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+ let
+ val goal =
+ (case xs of
+ [] => t
+ | _ =>
+ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (cf. "~~/src/Pure/Isar/obtain.ML") *)
+ let
+ (* FIXME: generate fresh name *)
+ val thesis = Free ("thesis_preplay", HOLogic.boolT)
+ val thesis_prop = HOLogic.mk_Trueprop thesis
+ 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))
- in
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
- Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
- end)
+ (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+ in
+ (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+ Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
+ end)
- val facts =
- resolve_fact_names ctxt fact_names
- |>> append (map (thm_of_proof ctxt) subproofs)
+ val facts =
+ resolve_fact_names ctxt fact_names
+ |>> append (map (thm_of_proof ctxt) subproofs)
- fun prove () =
- Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method ctxt facts meth))
- handle ERROR msg => error ("Preplay error: " ^ msg)
+ fun prove () =
+ Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
+ HEADGOAL (tac_of_method ctxt facts meth))
+ handle ERROR msg => error ("Preplay error: " ^ msg)
- val play_outcome = take_time timeout prove ()
- in
- (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
- play_outcome)
- end
+ val play_outcome = take_time timeout prove ()
+ in
+ (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+ play_outcome)
+ end
+
+fun preplay_isar_step ctxt timeout meth =
+ try (raw_preplay_step ctxt timeout meth)
+ #> the_default Play_Failed
type isar_preplay_data =
{set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
- preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
fun time_of_play (Played time) = time
@@ -173,10 +175,6 @@
avoid repeated calculation. *)
fun preplay_data_of_isar_proof ctxt preplay_timeout proof =
let
- fun preplay_step timeout meth =
- try (raw_preplay_step ctxt timeout meth)
- #> the_default Play_Failed
-
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
fun set_preplay_outcomes l meths_outcomes =
@@ -200,14 +198,13 @@
fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay_step preplay_timeout meth step))) meths)
+ (meth, Lazy.lazy (fn () => preplay_isar_step ctxt preplay_timeout meth step))) meths)
(!preplay_tab)
| reset_preplay_outcomes _ = ()
val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
in
- {preplay_step = preplay_step,
- set_preplay_outcomes = set_preplay_outcomes,
+ {set_preplay_outcomes = set_preplay_outcomes,
preplay_outcome = preplay_outcome,
overall_preplay_outcome = overall_preplay_outcome}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
@@ -11,7 +11,7 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof
+ val try0_isar_proof : Proof.context -> Time.time -> isar_preplay_data -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
@@ -27,9 +27,9 @@
val slack = seconds 0.05
-fun try0_step _ _ (step as Let _) = step
- | try0_step preplay_timeout
- ({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data)
+fun try0_step _ _ _ (step as Let _) = step
+ | try0_step ctxt preplay_timeout
+ ({set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data)
(step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
let
val timeout =
@@ -38,7 +38,7 @@
| _ => preplay_timeout)
fun try_method meth =
- (case preplay_step timeout meth step of
+ (case preplay_isar_step ctxt timeout meth step of
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
in
@@ -49,6 +49,6 @@
| NONE => step)
end
-val try0_isar_proof = map_isar_steps oo try0_step
+val try0_isar_proof = map_isar_steps ooo try0_step
end;