author | blanchet |
Sun, 02 Feb 2014 20:53:51 +0100 | |
changeset 55258 | 8cc42c1f9bb5 |
parent 55257 | abfd7b90bba2 |
child 55260 | ada3ae6458d4 |
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 |
54828 | 10 |
type play_outcome = Sledgehammer_Reconstructor.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 |
|
55213 | 18 |
type isar_preplay_data = |
55258 | 19 |
{set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, |
55243 | 20 |
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
54831 | 21 |
overall_preplay_outcome: isar_proof -> play_outcome} |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
22 |
|
55256 | 23 |
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context |
55258 | 24 |
val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome |
55257 | 25 |
val preplay_data_of_isar_proof : Proof.context -> Time.time -> isar_proof -> isar_preplay_data |
54504 | 26 |
end; |
50923 | 27 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
28 |
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 29 |
struct |
30 |
||
55257 | 31 |
open ATP_Proof_Reconstruct |
50923 | 32 |
open Sledgehammer_Util |
54828 | 33 |
open Sledgehammer_Reconstructor |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
34 |
open Sledgehammer_Isar_Proof |
50923 | 35 |
|
54763 | 36 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
50924 | 37 |
|
55256 | 38 |
fun enrich_context_with_local_facts proof ctxt = |
39 |
let |
|
40 |
val thy = Proof_Context.theory_of ctxt |
|
41 |
||
42 |
fun enrich_with_fact l t = |
|
43 |
Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
|
44 |
||
45 |
val enrich_with_assms = fold (uncurry enrich_with_fact) |
|
46 |
||
47 |
fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
|
48 |
enrich_with_assms assms #> fold enrich_with_step isar_steps |
|
49 |
and enrich_with_step (Let _) = I |
|
50 |
| enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
|
51 |
enrich_with_fact l t #> fold enrich_with_proof subproofs |
|
52 |
in |
|
53 |
enrich_with_proof proof ctxt |
|
54 |
end |
|
55 |
||
55194 | 56 |
fun preplay_trace ctxt assmsp concl result = |
51879 | 57 |
let |
58 |
val ctxt = ctxt |> Config.put show_markup true |
|
55194 | 59 |
val assms = op @ assmsp |
55251 | 60 |
val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]") |
61 |
val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) |
|
62 |
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
|
63 |
in |
55251 | 64 |
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
|
65 |
end |
51879 | 66 |
|
50923 | 67 |
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
|
68 |
let val timing = Timing.start () in |
54828 | 69 |
(TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
70 |
handle TimeLimit.TimeOut => Play_Timed_Out timeout |
|
50923 | 71 |
end |
72 |
||
73 |
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
|
74 |
(names |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
75 |
|>> map string_of_label |
55194 | 76 |
|> 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
|
77 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 78 |
|
54700 | 79 |
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
50923 | 80 |
let |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
81 |
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
|
82 |
|
54700 | 83 |
val concl = |
84 |
(case try List.last steps of |
|
85 |
SOME (Prove (_, [], _, t, _, _)) => t |
|
86 |
| _ => 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
|
87 |
|
51178 | 88 |
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
|
89 |
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
|
90 |
val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees |
51178 | 91 |
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
|
92 |
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
|
93 |
|> subst_free subst |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
94 |
|> Skip_Proof.make_thm thy |
51178 | 95 |
end |
96 |
||
55257 | 97 |
fun tac_of_method ctxt (local_facts, global_facts) meth = |
55194 | 98 |
Method.insert_tac local_facts THEN' |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
99 |
(case meth of |
55194 | 100 |
Meson_Method => Meson.meson_tac ctxt global_facts |
55257 | 101 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
102 |
Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] |
|
103 |
(the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
104 |
| _ => |
55194 | 105 |
Method.insert_tac global_facts THEN' |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
106 |
(case meth of |
55194 | 107 |
Simp_Method => Simplifier.asm_full_simp_tac ctxt |
54838
16511f84913c
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet
parents:
54831
diff
changeset
|
108 |
| Simp_Size_Method => |
16511f84913c
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet
parents:
54831
diff
changeset
|
109 |
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) |
54765 | 110 |
| Auto_Method => K (Clasimp.auto_tac ctxt) |
111 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt |
|
112 |
| Force_Method => Clasimp.force_tac ctxt |
|
113 |
| Arith_Method => Arith_Data.arith_tac ctxt |
|
114 |
| Blast_Method => blast_tac ctxt |
|
55219 | 115 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
116 |
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method")) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
117 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
118 |
(* main function for preplaying Isar steps; may throw exceptions *) |
55258 | 119 |
fun raw_preplay_step ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) = |
120 |
let |
|
121 |
val goal = |
|
122 |
(case xs of |
|
123 |
[] => t |
|
124 |
| _ => |
|
125 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
126 |
(cf. "~~/src/Pure/Isar/obtain.ML") *) |
|
127 |
let |
|
128 |
(* FIXME: generate fresh name *) |
|
129 |
val thesis = Free ("thesis_preplay", HOLogic.boolT) |
|
130 |
val thesis_prop = HOLogic.mk_Trueprop thesis |
|
131 |
val frees = map Free xs |
|
50923 | 132 |
|
55258 | 133 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
134 |
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
135 |
in |
|
136 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
137 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
138 |
end) |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
139 |
|
55258 | 140 |
val facts = |
141 |
resolve_fact_names ctxt fact_names |
|
142 |
|>> append (map (thm_of_proof ctxt) subproofs) |
|
55194 | 143 |
|
55258 | 144 |
fun prove () = |
145 |
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
|
146 |
HEADGOAL (tac_of_method ctxt facts meth)) |
|
147 |
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
|
148 |
|
55258 | 149 |
val play_outcome = take_time timeout prove () |
150 |
in |
|
151 |
(if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
|
152 |
play_outcome) |
|
153 |
end |
|
154 |
||
155 |
fun preplay_isar_step ctxt timeout meth = |
|
156 |
try (raw_preplay_step ctxt timeout meth) |
|
157 |
#> the_default Play_Failed |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
|
55213 | 159 |
type isar_preplay_data = |
55252 | 160 |
{set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit, |
55243 | 161 |
preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy, |
54831 | 162 |
overall_preplay_outcome: isar_proof -> play_outcome} |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
163 |
|
55256 | 164 |
fun time_of_play (Played time) = time |
165 |
| time_of_play (Play_Timed_Out time) = time |
|
50923 | 166 |
|
55256 | 167 |
fun merge_preplay_outcomes Play_Failed _ = Play_Failed |
168 |
| merge_preplay_outcomes _ Play_Failed = Play_Failed |
|
169 |
| merge_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2)) |
|
170 |
| merge_preplay_outcomes play1 play2 = |
|
171 |
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) |
|
54827 | 172 |
|
55256 | 173 |
(* Given a (canonically labeled) proof, produces an imperative preplay interface with a shared table |
174 |
mapping from labels to preplay results. The preplay results are caluclated lazily and cached to |
|
175 |
avoid repeated calculation. *) |
|
55257 | 176 |
fun preplay_data_of_isar_proof ctxt preplay_timeout proof = |
55253 | 177 |
let |
178 |
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty |
|
179 |
||
180 |
fun set_preplay_outcomes l meths_outcomes = |
|
181 |
preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes) |
|
182 |
(!preplay_tab) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
183 |
|
55253 | 184 |
fun preplay_outcome l meth = |
185 |
(case Canonical_Label_Tab.lookup (!preplay_tab) l of |
|
186 |
SOME meths_outcomes => |
|
187 |
(case AList.lookup (op =) meths_outcomes meth of |
|
188 |
SOME outcome => outcome |
|
189 |
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") |
|
190 |
| NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
|
55253 | 192 |
fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) = |
193 |
Lazy.force (preplay_outcome l meth) |
|
194 |
| result_of_step _ = Played Time.zeroTime |
|
54763 | 195 |
|
55253 | 196 |
fun overall_preplay_outcome (Proof (_, _, steps)) = |
197 |
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) |
|
55252 | 198 |
|
55253 | 199 |
fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = |
200 |
preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => |
|
55258 | 201 |
(meth, Lazy.lazy (fn () => preplay_isar_step ctxt preplay_timeout meth step))) meths) |
55253 | 202 |
(!preplay_tab) |
203 |
| reset_preplay_outcomes _ = () |
|
55252 | 204 |
|
55253 | 205 |
val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () |
206 |
in |
|
55258 | 207 |
{set_preplay_outcomes = set_preplay_outcomes, |
55253 | 208 |
preplay_outcome = preplay_outcome, |
209 |
overall_preplay_outcome = overall_preplay_outcome} |
|
210 |
end |
|
50923 | 211 |
|
54504 | 212 |
end; |