author | blanchet |
Mon, 03 Feb 2014 19:32:02 +0100 | |
changeset 55294 | 6f77310a0907 |
parent 55287 | ffa306239316 |
child 55295 | b18f65f77fcd |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML |
54712 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
50923 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
||
54763 | 5 |
Preplaying of Isar proofs. |
50923 | 6 |
*) |
7 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
8 |
signature SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 9 |
sig |
55287 | 10 |
type play_outcome = Sledgehammer_Proof_Methods.play_outcome |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
11 |
type proof_method = Sledgehammer_Isar_Proof.proof_method |
55212 | 12 |
type isar_step = Sledgehammer_Isar_Proof.isar_step |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
13 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
14 |
type label = Sledgehammer_Isar_Proof.label |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
15 |
|
55212 | 16 |
val trace : bool Config.T |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
17 |
|
55260 | 18 |
type isar_preplay_data |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
19 |
|
55256 | 20 |
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
21 |
val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step -> |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
22 |
play_outcome |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
23 |
val preplay_isar_step : Proof.context -> Time.time -> isar_step -> |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
24 |
(proof_method * play_outcome) list |
55264 | 25 |
val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
26 |
isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit |
55272 | 27 |
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome |
55266 | 28 |
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> |
55260 | 29 |
play_outcome Lazy.lazy |
55266 | 30 |
val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method |
55260 | 31 |
val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome |
54504 | 32 |
end; |
50923 | 33 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
34 |
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 35 |
struct |
36 |
||
55257 | 37 |
open ATP_Proof_Reconstruct |
50923 | 38 |
open Sledgehammer_Util |
55287 | 39 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
40 |
open Sledgehammer_Isar_Proof |
50923 | 41 |
|
54763 | 42 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
50924 | 43 |
|
55256 | 44 |
fun enrich_context_with_local_facts proof ctxt = |
45 |
let |
|
46 |
val thy = Proof_Context.theory_of ctxt |
|
47 |
||
48 |
fun enrich_with_fact l t = |
|
49 |
Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
|
50 |
||
51 |
val enrich_with_assms = fold (uncurry enrich_with_fact) |
|
52 |
||
53 |
fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
|
54 |
enrich_with_assms assms #> fold enrich_with_step isar_steps |
|
55 |
and enrich_with_step (Let _) = I |
|
55280 | 56 |
| enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) = |
55256 | 57 |
enrich_with_fact l t #> fold enrich_with_proof subproofs |
58 |
in |
|
59 |
enrich_with_proof proof ctxt |
|
60 |
end |
|
61 |
||
55260 | 62 |
fun preplay_trace ctxt assmsp concl outcome = |
51879 | 63 |
let |
64 |
val ctxt = ctxt |> Config.put show_markup true |
|
55194 | 65 |
val assms = op @ assmsp |
55260 | 66 |
val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") |
55251 | 67 |
val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) |
68 |
val concl = Syntax.pretty_term ctxt concl |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
69 |
in |
55251 | 70 |
tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
71 |
end |
51879 | 72 |
|
50923 | 73 |
fun take_time timeout tac arg = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
74 |
let val timing = Timing.start () in |
54828 | 75 |
(TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
76 |
handle TimeLimit.TimeOut => Play_Timed_Out timeout |
|
50923 | 77 |
end |
78 |
||
79 |
fun resolve_fact_names ctxt names = |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
80 |
(names |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
81 |
|>> map string_of_label |
55194 | 82 |
|> pairself (maps (thms_of_name ctxt))) |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
83 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 84 |
|
54700 | 85 |
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
50923 | 86 |
let |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
87 |
val thy = Proof_Context.theory_of ctxt |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
88 |
|
54700 | 89 |
val concl = |
90 |
(case try List.last steps of |
|
55280 | 91 |
SOME (Prove (_, [], _, t, _, _, _)) => t |
54700 | 92 |
| _ => raise Fail "preplay error: malformed subproof") |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
93 |
|
51178 | 94 |
val var_idx = maxidx_of_term concl + 1 |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
95 |
fun var_of_free (x, T) = Var ((x, var_idx), T) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
96 |
val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees |
51178 | 97 |
in |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
98 |
Logic.list_implies (assms |> map snd, concl) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
99 |
|> subst_free subst |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
100 |
|> Skip_Proof.make_thm thy |
51178 | 101 |
end |
102 |
||
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
103 |
(* main function for preplaying Isar steps; may throw exceptions *) |
55280 | 104 |
fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) = |
55258 | 105 |
let |
106 |
val goal = |
|
107 |
(case xs of |
|
108 |
[] => t |
|
109 |
| _ => |
|
110 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
111 |
(cf. "~~/src/Pure/Isar/obtain.ML") *) |
|
112 |
let |
|
55294 | 113 |
val frees = map Free xs |
114 |
val thesis = |
|
115 |
Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) |
|
55258 | 116 |
val thesis_prop = HOLogic.mk_Trueprop thesis |
50923 | 117 |
|
55258 | 118 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
119 |
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
120 |
in |
|
121 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
122 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
123 |
end) |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
124 |
|
55258 | 125 |
val facts = |
126 |
resolve_fact_names ctxt fact_names |
|
127 |
|>> append (map (thm_of_proof ctxt) subproofs) |
|
55194 | 128 |
|
55258 | 129 |
fun prove () = |
130 |
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
|
55285 | 131 |
HEADGOAL (tac_of_proof_method ctxt facts meth)) |
55258 | 132 |
handle ERROR msg => error ("Preplay error: " ^ msg) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
133 |
|
55258 | 134 |
val play_outcome = take_time timeout prove () |
135 |
in |
|
136 |
(if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
|
137 |
play_outcome) |
|
138 |
end |
|
139 |
||
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
140 |
fun preplay_isar_step_for_method ctxt timeout meth = |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
141 |
try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
142 |
|
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
143 |
fun preplay_isar_step ctxt timeout step = |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
144 |
let |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
145 |
fun try_method meth = |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
146 |
(case preplay_isar_step_for_method ctxt timeout meth step of |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
147 |
outcome as Played _ => SOME (meth, outcome) |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
148 |
| _ => NONE) |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
149 |
|
55279 | 150 |
val meths = proof_methods_of_isar_step step |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
151 |
in |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
152 |
the_list (Par_List.get_some try_method meths) |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
153 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|
55260 | 155 |
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
156 |
|
55256 | 157 |
fun time_of_play (Played time) = time |
158 |
| time_of_play (Play_Timed_Out time) = time |
|
50923 | 159 |
|
55260 | 160 |
fun add_preplay_outcomes Play_Failed _ = Play_Failed |
161 |
| add_preplay_outcomes _ Play_Failed = Play_Failed |
|
162 |
| add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2)) |
|
163 |
| add_preplay_outcomes play1 play2 = |
|
55256 | 164 |
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) |
54827 | 165 |
|
55264 | 166 |
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data |
55280 | 167 |
(step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 = |
55264 | 168 |
let |
55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
169 |
fun lazy_preplay meth = |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
170 |
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step) |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
171 |
val meths_outcomes = meths_outcomes0 |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
172 |
|> map (apsnd Lazy.value) |
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55275
diff
changeset
|
173 |
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths |
55264 | 174 |
in |
175 |
preplay_data := Canonical_Label_Tab.map_default (l, []) |
|
176 |
(fold (AList.update (op =)) meths_outcomes) (!preplay_data) |
|
177 |
end |
|
178 |
| set_preplay_outcomes_of_isar_step _ _ _ _ _ = () |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
179 |
|
55269 | 180 |
fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played |
181 |
||
55275 | 182 |
fun get_best_method_outcome force = |
183 |
tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *) |
|
184 |
#> map (apsnd force) |
|
185 |
#> sort (play_outcome_ord o pairself snd) |
|
186 |
#> hd |
|
187 |
||
55272 | 188 |
fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = |
55269 | 189 |
let |
55275 | 190 |
val meths_outcomes as (meth1, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l) |
55269 | 191 |
in |
55275 | 192 |
if forall (not o Lazy.is_finished o snd) meths_outcomes then |
193 |
(case Lazy.force outcome1 of |
|
194 |
outcome as Played _ => outcome |
|
195 |
| _ => snd (get_best_method_outcome Lazy.force meths_outcomes)) |
|
196 |
else |
|
197 |
(case get_best_method_outcome peek_at_outcome meths_outcomes of |
|
198 |
(_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes) |
|
199 |
| (_, outcome) => outcome) |
|
55269 | 200 |
end |
201 |
||
55268 | 202 |
fun preplay_outcome_of_isar_step_for_method preplay_data l = |
203 |
the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l)) |
|
55252 | 204 |
|
55268 | 205 |
fun fastest_method_of_isar_step preplay_data = |
55269 | 206 |
the o Canonical_Label_Tab.lookup preplay_data |
55275 | 207 |
#> get_best_method_outcome Lazy.force |
208 |
#> fst |
|
55266 | 209 |
|
55280 | 210 |
fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) = |
55266 | 211 |
Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths)) |
55260 | 212 |
| forced_outcome_of_step _ _ = Played Time.zeroTime |
55252 | 213 |
|
55260 | 214 |
fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = |
215 |
fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps |
|
216 |
(Played Time.zeroTime) |
|
50923 | 217 |
|
54504 | 218 |
end; |