# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID 8cc42c1f9bb53039dfcf207f73aaa8a354c9534d # Parent abfd7b90bba2e59ec8b24bba05a639bd10bf777e more data structure rationalization diff -r abfd7b90bba2 -r 8cc42c1f9bb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r abfd7b90bba2 -r 8cc42c1f9bb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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 diff -r abfd7b90bba2 -r 8cc42c1f9bb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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) diff -r abfd7b90bba2 -r 8cc42c1f9bb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r abfd7b90bba2 -r 8cc42c1f9bb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- 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;