--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100
@@ -135,10 +135,8 @@
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
- val (_, ctxt) =
- params
- |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
- |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
+ val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
+ val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
val do_preplay = preplay_timeout <> Time.zeroTime
val try0_isar = try0_isar andalso do_preplay
@@ -283,19 +281,14 @@
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
- val preplay_ctxt = ctxt
+ val ctxt = ctxt
|> enrich_context_with_local_facts canonical_isar_proof
|> silence_reconstructors debug
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
- fun init_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)
- | init_preplay_outcomes _ = ()
-
- val _ = fold_isar_steps (K o init_preplay_outcomes)
+ val _ = fold_isar_steps (fn meth =>
+ K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
(steps_of_isar_proof canonical_isar_proof) ()
fun str_of_preplay_outcome outcome =
@@ -316,12 +309,12 @@
val (play_outcome, isar_proof) =
canonical_isar_proof
|> tap (trace_isar_proof "Original")
- |> compress_isar_proof preplay_ctxt compress_isar preplay_data
+ |> compress_isar_proof ctxt compress_isar preplay_data
|> tap (trace_isar_proof "Compressed")
- |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
+ |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
|> tap (trace_isar_proof "Tried0")
|> postprocess_isar_proof_remove_unreferenced_steps
- (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
+ (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `(preplay_outcome_of_isar_proof (!preplay_data))
||> chain_isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
@@ -137,11 +137,16 @@
end
(* elimination of trivial, one-step subproofs *)
- fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
+ fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (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)))
+ let
+ val subproofs = List.revAppend (nontriv_subs, subs)
+ val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
+ in
+ set_preplay_outcomes_of_isar_step ctxt time preplay_data step
+ [(meth, Lazy.value (Played time))];
+ step
+ end
else
(case subs of
(sub as Proof (_, assms, sub_steps)) :: subs =>
@@ -166,11 +171,11 @@
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
+ elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
end
handle Bind =>
- elim_subproofs' time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
- | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
+ elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
+ | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
fun elim_subproofs (step as Let _) = step
| elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
@@ -179,7 +184,7 @@
step
else
(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 []
+ Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
| _ => step)
fun compress_top_level steps =
@@ -210,25 +215,22 @@
|> fold_index add_cand) []
end
- fun try_eliminate (i, l, _) succ_lbls steps =
+ fun try_eliminate (i, l, _) labels steps =
let
val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
- val succs = collect_successors steps' succ_lbls
- val succ_methss = map (snd o the o byline_of_isar_step) succs
- val succ_meths = map hd succ_methss (* FIXME *)
+ val succs = collect_successors steps' labels
+ val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
(* only touch steps that can be preplayed successfully *)
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_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
+ val times0 = map2 ((fn Played time => time) o Lazy.force oo
+ preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths
+ val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
+ val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
(* FIXME: debugging *)
val _ =
@@ -241,19 +243,20 @@
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
+ val times = map (fn Played time => time) play_outcomes
val (steps1, _ :: steps2) = chop i steps
(* replace successors with their modified versions *)
val steps2 = update_steps steps2 succs'
val succ_meths_outcomess =
- map2 (fn meth :: meths => fn outcome => (meth, Lazy.value outcome) ::
- map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
+ map2 (fn meth => fn outcome => [(meth, Lazy.value outcome)]) succ_meths
+ play_outcomes
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 (set_preplay_outcomes_of_isar_step preplay_data) succ_lbls succ_meths_outcomess;
- map (replace_successor l succ_lbls) lfs;
+ map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
+ succs succ_meths_outcomess;
+ map (replace_successor l labels) lfs;
(* removing the step would mess up the indices; replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100
@@ -43,9 +43,12 @@
val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+
+ val step' = mk_step_lfs_gfs min_lfs min_gfs
in
- set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))];
- mk_step_lfs_gfs min_lfs min_gfs
+ set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
+ [(meth, Lazy.value (Played time))];
+ step'
end
| _ => step (* don't touch steps that time out or fail *))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
@@ -19,7 +19,8 @@
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 set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
+ val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
+ isar_preplay_data Unsynchronized.ref -> isar_step ->
(proof_method * play_outcome Lazy.lazy) list -> unit
val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
play_outcome Lazy.lazy
@@ -167,9 +168,17 @@
| add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
-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 set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
+ (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
+ let
+ fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
+ val meths_outcomes =
+ fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
+ in
+ preplay_data := Canonical_Label_Tab.map_default (l, [])
+ (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
+ end
+ | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
fun preplay_outcome_of_isar_step preplay_data l meth =
(case Canonical_Label_Tab.lookup preplay_data l of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Mon Feb 03 10:14:18 2014 +0100
@@ -45,8 +45,11 @@
(* FIXME: create variant after success *)
(case Par_List.get_some try_method meths of
SOME (meth', outcome) =>
- (set_preplay_outcomes_of_isar_step preplay_data l [(meth', Lazy.value outcome)];
- step_with_method meth' step)
+ let val step' = step_with_method meth' step in
+ (set_preplay_outcomes_of_isar_step ctxt timeout preplay_data step'
+ [(meth', Lazy.value outcome)];
+ step')
+ end
| NONE => step)
end