author | blanchet |
Fri, 31 Jan 2014 16:26:43 +0100 | |
changeset 55213 | dcb36a2540bc |
parent 55212 | 5832470d956e |
child 55219 | 6fe9fd75f9d7 |
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 |
55212 | 11 |
type isar_step = Sledgehammer_Isar_Proof.isar_step |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
12 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
13 |
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
|
14 |
|
55212 | 15 |
val trace : bool Config.T |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
16 |
|
55213 | 17 |
type isar_preplay_data = |
54828 | 18 |
{get_preplay_outcome: label -> play_outcome, |
19 |
set_preplay_outcome: label -> play_outcome -> unit, |
|
20 |
preplay_quietly: Time.time -> isar_step -> play_outcome, |
|
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 |
|
55213 | 23 |
val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time -> |
24 |
isar_proof -> isar_preplay_data |
|
54504 | 25 |
end; |
50923 | 26 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
27 |
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
50923 | 28 |
struct |
29 |
||
30 |
open Sledgehammer_Util |
|
54828 | 31 |
open Sledgehammer_Reconstructor |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
32 |
open Sledgehammer_Isar_Proof |
50923 | 33 |
|
54763 | 34 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
50924 | 35 |
|
55194 | 36 |
fun preplay_trace ctxt assmsp concl result = |
51879 | 37 |
let |
38 |
val ctxt = ctxt |> Config.put show_markup true |
|
55194 | 39 |
val assms = op @ assmsp |
54828 | 40 |
val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str |
51879 | 41 |
val nr_of_assms = length assms |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
42 |
val assms = assms |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
43 |
|> map (Display.pretty_thm ctxt) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
44 |
|> (fn [] => Pretty.str "" |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
45 |
| [a] => a |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
46 |
| assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *) |
51879 | 47 |
val concl = concl |> Syntax.pretty_term ctxt |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
48 |
val trace_list = [] |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
49 |
|> cons concl |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
50 |
|> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>") |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
51 |
|> cons assms |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
52 |
|> cons time |
53761
4d34e267fba9
use configuration mechanism for low-level tracing
blanchet
parents:
53664
diff
changeset
|
53 |
val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
54 |
in |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
55 |
tracing (Pretty.string_of pretty_trace) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
56 |
end |
51879 | 57 |
|
50923 | 58 |
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
|
59 |
let val timing = Timing.start () in |
54828 | 60 |
(TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
61 |
handle TimeLimit.TimeOut => Play_Timed_Out timeout |
|
50923 | 62 |
end |
63 |
||
64 |
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
|
65 |
(names |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
66 |
|>> map string_of_label |
55194 | 67 |
|> 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
|
68 |
handle ERROR msg => error ("preplay error: " ^ msg) |
50923 | 69 |
|
54700 | 70 |
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
50923 | 71 |
let |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
72 |
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
|
73 |
|
54700 | 74 |
val concl = |
75 |
(case try List.last steps of |
|
76 |
SOME (Prove (_, [], _, t, _, _)) => t |
|
77 |
| _ => 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
|
78 |
|
51178 | 79 |
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
|
80 |
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
|
81 |
val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees |
51178 | 82 |
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
|
83 |
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
|
84 |
|> subst_free subst |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
85 |
|> Skip_Proof.make_thm thy |
51178 | 86 |
end |
87 |
||
55194 | 88 |
fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) = |
89 |
Method.insert_tac local_facts THEN' |
|
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
90 |
(case meth of |
55194 | 91 |
Meson_Method => Meson.meson_tac ctxt global_facts |
92 |
| Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
93 |
| _ => |
55194 | 94 |
Method.insert_tac global_facts THEN' |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
95 |
(case meth of |
55194 | 96 |
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
|
97 |
| Simp_Size_Method => |
16511f84913c
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet
parents:
54831
diff
changeset
|
98 |
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) |
54765 | 99 |
| Auto_Method => K (Clasimp.auto_tac ctxt) |
100 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt |
|
101 |
| Force_Method => Clasimp.force_tac ctxt |
|
102 |
| Arith_Method => Arith_Data.arith_tac ctxt |
|
103 |
| Blast_Method => blast_tac ctxt |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
104 |
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method")) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52575
diff
changeset
|
105 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
106 |
(* main function for preplaying Isar steps; may throw exceptions *) |
54828 | 107 |
fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime |
53761
4d34e267fba9
use configuration mechanism for low-level tracing
blanchet
parents:
53664
diff
changeset
|
108 |
| preplay_raw debug type_enc lam_trans ctxt timeout |
54799 | 109 |
(Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
110 |
let |
54763 | 111 |
val goal = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
112 |
(case xs of |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
113 |
[] => t |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
114 |
| _ => |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
115 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
116 |
(cf. "~~/src/Pure/Isar/obtain.ML") *) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
117 |
let |
54813 | 118 |
(* FIXME: generate fresh name *) |
119 |
val thesis = Free ("thesis", HOLogic.boolT) |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
120 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
54813 | 121 |
val frees = map Free xs |
50923 | 122 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
123 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
124 |
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
125 |
in |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
126 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
50923 | 127 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
128 |
end) |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
129 |
|
55194 | 130 |
val facts = |
131 |
resolve_fact_names ctxt fact_names |
|
132 |
|>> append (map (thm_of_proof ctxt) subproofs) |
|
133 |
||
55170 | 134 |
val ctxt' = ctxt |> silence_reconstructors debug |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
135 |
|
54817 | 136 |
fun prove () = |
137 |
Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} => |
|
138 |
HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts)) |
|
139 |
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
|
140 |
|
54828 | 141 |
val play_outcome = take_time timeout prove () |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
142 |
in |
54828 | 143 |
(if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
144 |
play_outcome) |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
145 |
end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
146 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
147 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
148 |
(*** proof preplay interface ***) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
149 |
|
55213 | 150 |
type isar_preplay_data = |
54828 | 151 |
{get_preplay_outcome: label -> play_outcome, |
152 |
set_preplay_outcome: label -> play_outcome -> unit, |
|
153 |
preplay_quietly: Time.time -> isar_step -> play_outcome, |
|
54831 | 154 |
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
|
155 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
156 |
fun enrich_context_with_local_facts proof ctxt = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
val thy = Proof_Context.theory_of ctxt |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
159 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
160 |
fun enrich_with_fact l t = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
161 |
Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
162 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
163 |
val enrich_with_assms = fold (uncurry enrich_with_fact) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
164 |
|
54700 | 165 |
fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
166 |
enrich_with_assms assms #> fold enrich_with_step isar_steps |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
167 |
and enrich_with_step (Let _) = I |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
168 |
| enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
169 |
enrich_with_fact l t #> fold enrich_with_proof subproofs |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
170 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
171 |
enrich_with_proof proof ctxt |
50923 | 172 |
end |
173 |
||
54828 | 174 |
fun merge_preplay_outcomes _ Play_Failed = Play_Failed |
175 |
| merge_preplay_outcomes Play_Failed _ = Play_Failed |
|
54831 | 176 |
| merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) = |
177 |
Play_Timed_Out (Time.+ (t1, t2)) |
|
54828 | 178 |
| merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2)) |
179 |
| merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2)) |
|
180 |
| merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2)) |
|
54827 | 181 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
182 |
(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
183 |
to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
184 |
calculation. |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
185 |
|
54763 | 186 |
Precondition: The proof must be labeled canonically; cf. |
55213 | 187 |
"Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *) |
188 |
fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
189 |
if not do_preplay then |
54828 | 190 |
(* the "dont_preplay" option pretends that everything works just fine *) |
191 |
{get_preplay_outcome = K (Played Time.zeroTime), |
|
192 |
set_preplay_outcome = K (K ()), |
|
193 |
preplay_quietly = K (K (Played Time.zeroTime)), |
|
55213 | 194 |
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
195 |
else |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
196 |
let |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54712
diff
changeset
|
197 |
val ctxt = enrich_context_with_local_facts proof ctxt |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
198 |
|
52627 | 199 |
fun preplay quietly timeout step = |
54828 | 200 |
preplay_raw debug type_enc lam_trans ctxt timeout step |
52626 | 201 |
handle exn => |
55212 | 202 |
if Exn.is_interrupt exn then |
203 |
reraise exn |
|
204 |
else |
|
205 |
(if not quietly andalso debug then |
|
206 |
warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn) |
|
207 |
else |
|
208 |
(); |
|
209 |
Play_Failed) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
210 |
|
52626 | 211 |
(* preplay steps treating exceptions like timeouts *) |
54827 | 212 |
fun preplay_quietly timeout = preplay true timeout |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
213 |
|
52626 | 214 |
val preplay_tab = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
215 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
216 |
fun add_step_to_tab step tab = |
54763 | 217 |
(case label_of_step step of |
54831 | 218 |
NONE => tab |
219 |
| SOME l => |
|
55212 | 220 |
Canonical_Label_Tab.update_new |
54831 | 221 |
(l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab) |
55212 | 222 |
handle Canonical_Label_Tab.DUP _ => |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
223 |
raise Fail "Sledgehammer_Isar_Preplay: preplay time table" |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
224 |
in |
55212 | 225 |
Canonical_Label_Tab.empty |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
226 |
|> fold_isar_steps add_step_to_tab (steps_of_proof proof) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
227 |
|> Unsynchronized.ref |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
228 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
229 |
|
54828 | 230 |
fun get_preplay_outcome l = |
55212 | 231 |
Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
232 |
handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table" |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
233 |
|
54828 | 234 |
fun set_preplay_outcome l result = |
55212 | 235 |
preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab) |
52626 | 236 |
|
54763 | 237 |
val result_of_step = |
54828 | 238 |
try (label_of_step #> the #> get_preplay_outcome) |
239 |
#> the_default (Played Time.zeroTime) |
|
54763 | 240 |
|
54831 | 241 |
fun overall_preplay_outcome (Proof (_, _, steps)) = |
54828 | 242 |
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
243 |
in |
54828 | 244 |
{get_preplay_outcome = get_preplay_outcome, |
245 |
set_preplay_outcome = set_preplay_outcome, |
|
54712 | 246 |
preplay_quietly = preplay_quietly, |
54831 | 247 |
overall_preplay_outcome = overall_preplay_outcome} |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
248 |
end |
50923 | 249 |
|
54504 | 250 |
end; |