--- 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
@@ -287,14 +287,23 @@
|> enrich_context_with_local_facts canonical_isar_proof
|> silence_reconstructors debug
- val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
- preplay_data_of_isar_proof preplay_ctxt preplay_timeout canonical_isar_proof
+ val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
+
+ fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+ set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
+ Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
+ meths)
+ | reset_preplay_outcomes _ = ()
+
+ val _ = fold_isar_steps (K o reset_preplay_outcomes)
+ (steps_of_isar_proof canonical_isar_proof) ()
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
fun str_of_meth l meth =
- string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
+ string_of_proof_method meth ^ " " ^
+ str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth)
fun comment_of l = map (str_of_meth l) #> commas
fun trace_isar_proof label proof =
@@ -314,7 +323,7 @@
|> postprocess_isar_proof_remove_unreferenced_steps
(try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
- |> `overall_preplay_outcome
+ |> `(preplay_outcome_of_isar_proof (!preplay_data))
||> chain_isar_proof
||> kill_useless_labels_in_isar_proof
||> relabel_isar_proof_finally
@@ -327,7 +336,7 @@
let
val msg =
(if verbose then
- let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
+ let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
[string_of_int num_steps ^ " step" ^ plural_s num_steps]
end
else
--- 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,8 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val compress_isar_proof : Proof.context -> real -> isar_preplay_data -> isar_proof -> isar_proof
+ val compress_isar_proof : Proof.context -> real -> isar_preplay_data Unsynchronized.ref ->
+ isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
@@ -37,7 +38,7 @@
| accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
and do_subproofs [] x = x
| do_subproofs (proof :: subproofs) x =
- (case do_steps (steps_of_proof proof) x of
+ (case do_steps (steps_of_isar_proof proof) x of
accum as ([], _) => accum
| accum => do_subproofs subproofs accum)
in
@@ -97,15 +98,14 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
-fun compress_isar_proof ctxt compress_isar
- ({preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof =
+fun compress_isar_proof ctxt compress_isar preplay_data proof =
if compress_isar <= 1.0 then
proof
else
let
val (compress_further, decrement_step_count) =
let
- val number_of_steps = add_isar_steps (steps_of_proof proof) 0
+ val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
in
@@ -120,7 +120,7 @@
val tab =
Canonical_Label_Tab.empty
- |> fold_isar_steps add_refs (steps_of_proof proof)
+ |> fold_isar_steps add_refs (steps_of_isar_proof proof)
(* "rev" should have the same effect as "sort canonical_label_ord" *)
|> Canonical_Label_Tab.map (K rev)
|> Unsynchronized.ref
@@ -139,7 +139,7 @@
(* elimination of trivial, one-step subproofs *)
fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_outcomes l ((meth, Lazy.value (Played time)) ::
+ (set_preplay_outcomes_of_isar_step preplay_data l ((meth, Lazy.value (Played time)) ::
map (rpair (Lazy.value Not_Played)(*FIXME*)) meths');
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
else
@@ -151,7 +151,7 @@
try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Played time' = Lazy.force (preplay_outcome l' meth')
+ val Played time' = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l' meth')
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -178,7 +178,7 @@
if subproofs = [] then
step
else
- (case Lazy.force (preplay_outcome l meth) of
+ (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs []
| _ => step)
@@ -220,12 +220,13 @@
val succ_meths = map hd succ_methss (* FIXME *)
(* only touch steps that can be preplayed successfully *)
- val Played time = Lazy.force (preplay_outcome l meth)
+ val Played time = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth)
val succs' = map (try_merge cand #> the) succs
val succ_times =
- map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
+ map2 ((fn Played t => t) o Lazy.force oo
+ preplay_outcome_of_isar_step (!preplay_data)) succ_lbls succ_meths
val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
val timeouts =
map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
@@ -252,7 +253,7 @@
map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_outcomes succ_lbls succ_meths_outcomess;
+ map2 (set_preplay_outcomes_of_isar_step preplay_data) succ_lbls succ_meths_outcomess;
map (replace_successor l succ_lbls) lfs;
(* removing the step would mess up the indices; replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
--- 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,8 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data -> isar_step -> isar_step
+ val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
+ isar_step -> isar_step
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
isar_proof
end;
@@ -25,10 +26,10 @@
val slack = seconds 0.1
-fun minimize_isar_step_dependencies _ (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies ctxt {set_preplay_outcomes, preplay_outcome, ...}
+fun minimize_isar_step_dependencies _ _ (step as Let _) = step
+ | minimize_isar_step_dependencies ctxt preplay_data
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
- (case Lazy.force (preplay_outcome l meth) of
+ (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
Played time =>
let
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
@@ -44,7 +45,7 @@
val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
in
- set_preplay_outcomes l [(meth, Lazy.value (Played time))];
+ set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))];
mk_step_lfs_gfs min_lfs min_gfs
end
| _ => step (* don't touch steps that time out or fail *))
--- 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
@@ -15,14 +15,15 @@
val trace : bool Config.T
- 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,
- overall_preplay_outcome: isar_proof -> play_outcome}
+ type isar_preplay_data
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
+ val set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
+ (proof_method * play_outcome Lazy.lazy) list -> unit
+ val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
+ play_outcome Lazy.lazy
+ val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
end;
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
@@ -53,11 +54,11 @@
enrich_with_proof proof ctxt
end
-fun preplay_trace ctxt assmsp concl result =
+fun preplay_trace ctxt assmsp concl outcome =
let
val ctxt = ctxt |> Config.put show_markup true
val assms = op @ assmsp
- val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]")
+ val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
@@ -153,60 +154,37 @@
end
fun preplay_isar_step ctxt timeout meth =
- try (raw_preplay_step ctxt timeout meth)
- #> the_default Play_Failed
+ 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,
- overall_preplay_outcome: isar_proof -> play_outcome}
+type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
fun time_of_play (Played time) = time
| time_of_play (Play_Timed_Out time) = time
-fun merge_preplay_outcomes Play_Failed _ = Play_Failed
- | merge_preplay_outcomes _ Play_Failed = Play_Failed
- | merge_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
- | merge_preplay_outcomes play1 play2 =
+fun add_preplay_outcomes Play_Failed _ = Play_Failed
+ | add_preplay_outcomes _ Play_Failed = Play_Failed
+ | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
+ | add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
-(* Given a (canonically labeled) proof, produces an imperative preplay interface with a shared table
- mapping from labels to preplay results. The preplay results are caluclated lazily and cached to
- avoid repeated calculation. *)
-fun preplay_data_of_isar_proof ctxt preplay_timeout proof =
- let
- 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 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 set_preplay_outcomes_of_isar_step preplay_data l meths_outcomes =
+ preplay_data := Canonical_Label_Tab.map_default (l, [])
+ (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
- 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 preplay_outcome_of_isar_step preplay_data l meth =
+ (case Canonical_Label_Tab.lookup preplay_data 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 reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
- preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay_isar_step ctxt preplay_timeout meth step))) meths)
- (!preplay_tab)
- | reset_preplay_outcomes _ = ()
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meth :: _))) =
+ Lazy.force (preplay_outcome_of_isar_step preplay_data l meth)
+ | forced_outcome_of_step _ _ = Played Time.zeroTime
- val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
- in
- {set_preplay_outcomes = set_preplay_outcomes,
- preplay_outcome = preplay_outcome,
- overall_preplay_outcome = overall_preplay_outcome}
- end
+fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
+ fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps
+ (Played Time.zeroTime)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
@@ -40,7 +40,7 @@
val string_of_proof_method : proof_method -> string
- val steps_of_proof : isar_proof -> isar_step list
+ val steps_of_isar_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
val byline_of_isar_step : isar_step -> (facts * proof_method list) option
@@ -119,7 +119,7 @@
| Meson_Method => "meson"
| Algebra_Method => "algebra")
-fun steps_of_proof (Proof (_, _, steps)) = steps
+fun steps_of_isar_proof (Proof (_, _, steps)) = steps
fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
| label_of_isar_step _ = NONE
@@ -131,7 +131,7 @@
| byline_of_isar_step _ = NONE
fun fold_isar_step f step =
- fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
+ fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
and fold_isar_steps f = fold (fold_isar_step f)
fun map_isar_steps f =
@@ -170,7 +170,7 @@
let
val used_ls =
fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
- (steps_of_proof proof) []
+ (steps_of_isar_proof proof) []
fun kill_label l = if member (op =) used_ls l then l else no_label
--- 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,8 @@
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val try0_isar_proof : Proof.context -> Time.time -> isar_preplay_data -> isar_proof -> isar_proof
+ val try0_isar_proof : Proof.context -> Time.time -> isar_preplay_data Unsynchronized.ref ->
+ isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
@@ -28,12 +29,11 @@
val slack = seconds 0.05
fun try0_step _ _ _ (step as Let _) = step
- | try0_step ctxt preplay_timeout
- ({set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data)
+ | try0_step ctxt preplay_timeout preplay_data
(step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
let
val timeout =
- (case Lazy.force (preplay_outcome l meth) of
+ (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
Played time => Time.+ (time, slack)
| _ => preplay_timeout)
@@ -45,7 +45,8 @@
(* FIXME: create variant after success *)
(case Par_List.get_some try_method meths of
SOME (meth', outcome) =>
- (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step)
+ (set_preplay_outcomes_of_isar_step preplay_data l [(meth', Lazy.value outcome)];
+ step_with_method meth' step)
| NONE => step)
end