1(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML 2 Author: Steffen Juilf Smolka, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 5Preplaying of Isar proofs. 6*) 7 8signature SLEDGEHAMMER_ISAR_PREPLAY = 9sig 10 type play_outcome = Sledgehammer_Proof_Methods.play_outcome 11 type proof_method = Sledgehammer_Proof_Methods.proof_method 12 type isar_step = Sledgehammer_Isar_Proof.isar_step 13 type isar_proof = Sledgehammer_Isar_Proof.isar_proof 14 type label = Sledgehammer_Isar_Proof.label 15 16 val trace : bool Config.T 17 18 type isar_preplay_data 19 20 val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome 21 val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context 22 val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method -> 23 isar_step -> play_outcome 24 val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list -> 25 isar_step -> (proof_method * play_outcome) list 26 val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> 27 isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit 28 val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome 29 val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> 30 play_outcome Lazy.lazy 31 val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method 32 val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome 33end; 34 35structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = 36struct 37 38open ATP_Proof_Reconstruct 39open Sledgehammer_Util 40open Sledgehammer_Proof_Methods 41open Sledgehammer_Isar_Proof 42 43val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_preplay_trace\<close> (K false) 44 45fun peek_at_outcome outcome = 46 if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime 47 48fun par_list_map_filter_with_timeout _ _ _ _ [] = [] 49 | par_list_map_filter_with_timeout get_time min_timeout timeout0 f xs = 50 let 51 val next_timeout = Unsynchronized.ref timeout0 52 53 fun apply_f x = 54 let val timeout = !next_timeout in 55 if timeout <= min_timeout then 56 NONE 57 else 58 let val y = f timeout x in 59 (case get_time y of 60 SOME time => next_timeout := time 61 | _ => ()); 62 SOME y 63 end 64 end 65 in 66 map_filter I (Par_List.map apply_f xs) 67 end 68 69fun enrich_context_with_local_facts proof ctxt = 70 let 71 val thy = Proof_Context.theory_of ctxt 72 73 fun enrich_with_fact l t = 74 Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) 75 76 val enrich_with_assms = fold (uncurry enrich_with_fact) 77 78 fun enrich_with_proof (Proof (_, assms, isar_steps)) = 79 enrich_with_assms assms #> fold enrich_with_step isar_steps 80 and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) = 81 enrich_with_fact l t #> fold enrich_with_proof subproofs 82 | enrich_with_step _ = I 83 in 84 enrich_with_proof proof ctxt 85 end 86 87fun preplay_trace ctxt assmsp concl outcome = 88 let 89 val ctxt = ctxt |> Config.put show_markup true 90 val assms = op @ assmsp 91 val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") 92 val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) 93 val concl = Syntax.pretty_term ctxt concl 94 in 95 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) 96 end 97 98fun take_time timeout tac arg = 99 let val timing = Timing.start () in 100 (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing))) 101 handle Timeout.TIMEOUT _ => Play_Timed_Out timeout 102 end 103 104fun resolve_fact_names ctxt names = 105 (names 106 |>> map string_of_label 107 |> apply2 (maps (thms_of_name ctxt))) 108 handle ERROR msg => error ("preplay error: " ^ msg) 109 110fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = 111 let 112 val thy = Proof_Context.theory_of ctxt 113 114 val concl = 115 (case try List.last steps of 116 SOME (Prove (_, [], _, t, _, _, _, _)) => t 117 | _ => raise Fail "preplay error: malformed subproof") 118 119 val var_idx = maxidx_of_term concl + 1 120 fun var_of_free (x, T) = Var ((x, var_idx), T) 121 val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees 122 in 123 Logic.list_implies (assms |> map snd, concl) 124 |> subst_free subst 125 |> Skip_Proof.make_thm thy 126 end 127 128(* may throw exceptions *) 129fun raw_preplay_step_for_method ctxt chained timeout meth 130 (Prove (_, xs, _, t, subproofs, facts, _, _)) = 131 let 132 val goal = 133 (case xs of 134 [] => t 135 | _ => 136 (* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis 137 (cf. "~~/src/Pure/Isar/obtain.ML") *) 138 let 139 val frees = map Free xs 140 val thesis = 141 Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) 142 val thesis_prop = HOLogic.mk_Trueprop thesis 143 144 (* !!x1...xn. t ==> thesis *) 145 val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) 146 in 147 (* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *) 148 Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) 149 end) 150 151 val assmsp = 152 resolve_fact_names ctxt facts 153 |>> append (map (thm_of_proof ctxt) subproofs) 154 |>> append chained 155 156 fun prove () = 157 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => 158 HEADGOAL (tac_of_proof_method ctxt assmsp meth)) 159 handle ERROR msg => error ("Preplay error: " ^ msg) 160 161 val play_outcome = take_time timeout prove () 162 in 163 if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); 164 play_outcome 165 end 166 167fun preplay_isar_step_for_method ctxt chained timeout meth = 168 try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed 169 170val min_preplay_timeout = seconds 0.002 171 172fun preplay_isar_step ctxt chained timeout0 hopeless step = 173 let 174 fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step) 175 fun get_time (_, Played time) = SOME time 176 | get_time _ = NONE 177 178 val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless 179 in 180 par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths 181 |> sort (play_outcome_ord o apply2 snd) 182 end 183 184type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table 185 186fun time_of_play (Played time) = time 187 | time_of_play (Play_Timed_Out time) = time 188 189fun add_preplay_outcomes Play_Failed _ = Play_Failed 190 | add_preplay_outcomes _ Play_Failed = Play_Failed 191 | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2) 192 | add_preplay_outcomes play1 play2 = 193 Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2))) 194 195fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data 196 (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = 197 let 198 fun lazy_preplay meth = 199 Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step) 200 val meths_outcomes = meths_outcomes0 201 |> map (apsnd Lazy.value) 202 |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths 203 in 204 preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) 205 (!preplay_data) 206 end 207 | set_preplay_outcomes_of_isar_step _ _ _ _ _ = () 208 209fun get_best_method_outcome force = 210 tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *) 211 #> map (apsnd force) 212 #> sort (play_outcome_ord o apply2 snd) 213 #> hd 214 215fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = 216 let 217 val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l) 218 in 219 if forall (not o Lazy.is_finished o snd) meths_outcomes then 220 (case Lazy.force outcome1 of 221 outcome as Played _ => outcome 222 | _ => snd (get_best_method_outcome Lazy.force meths_outcomes)) 223 else 224 let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in 225 if outcome = Play_Timed_Out Time.zeroTime then 226 snd (get_best_method_outcome Lazy.force meths_outcomes) 227 else 228 outcome 229 end 230 end 231 232fun preplay_outcome_of_isar_step_for_method preplay_data l = 233 AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l)) 234 #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime)) 235 236fun fastest_method_of_isar_step preplay_data = 237 the o Canonical_Label_Tab.lookup preplay_data 238 #> get_best_method_outcome Lazy.force 239 #> fst 240 241fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) = 242 Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths)) 243 | forced_outcome_of_step _ _ = Played Time.zeroTime 244 245fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = 246 fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps 247 (Played Time.zeroTime) 248 249end; 250