# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID ada3ae6458d4d85ca86467aeeec4e3147ded8db8 # Parent 7f2930d9bb2c4d3e6d8182340b2421405afae612 more data structure rationalization diff -r 7f2930d9bb2c -r ada3ae6458d4 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 @@ -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 diff -r 7f2930d9bb2c -r ada3ae6458d4 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,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 diff -r 7f2930d9bb2c -r ada3ae6458d4 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,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 *)) diff -r 7f2930d9bb2c -r ada3ae6458d4 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 @@ -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; diff -r 7f2930d9bb2c -r ada3ae6458d4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r 7f2930d9bb2c -r ada3ae6458d4 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,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