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