author | blanchet |
Mon, 03 Feb 2014 14:35:19 +0100 | |
changeset 55284 | bd27ac6ad1c3 |
parent 55282 | d4a033f07800 |
child 55285 | e88ad20035f4 |
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_proof.ML |
50263 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Basic data structures for representing and basic methods |
|
6 |
for dealing with Isar proof texts. |
|
7 |
*) |
|
8 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
9 |
signature SLEDGEHAMMER_ISAR_PROOF = |
50259 | 10 |
sig |
51239 | 11 |
type label = string * int |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54767
diff
changeset
|
12 |
type facts = label list * string list (* local and global facts *) |
50268 | 13 |
|
51178 | 14 |
datatype isar_qualifier = Show | Then |
50268 | 15 |
|
55218 | 16 |
datatype proof_method = |
55257 | 17 |
Metis_Method of string option * string option | |
55284 | 18 |
Meson_Method | |
19 |
SMT_Method | |
|
55257 | 20 |
Simp_Method | |
21 |
Simp_Size_Method | |
|
22 |
Auto_Method | |
|
23 |
Fastforce_Method | |
|
24 |
Force_Method | |
|
25 |
Arith_Method | |
|
26 |
Blast_Method | |
|
27 |
Algebra_Method |
|
55218 | 28 |
|
52454 | 29 |
datatype isar_proof = |
54700 | 30 |
Proof of (string * typ) list * (label * term) list * isar_step list |
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
|
31 |
and isar_step = |
50268 | 32 |
Let of term * term | |
55280 | 33 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list |
34 |
* facts * proof_method list |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
35 |
|
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
|
36 |
val no_label : label |
50268 | 37 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
38 |
val label_ord : label * label -> order |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
39 |
val string_of_label : label -> string |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
40 |
|
55222 | 41 |
val string_of_proof_method : proof_method -> string |
42 |
||
55260 | 43 |
val steps_of_isar_proof : isar_proof -> isar_step list |
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
|
44 |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
45 |
val label_of_isar_step : isar_step -> label option |
55279 | 46 |
val facts_of_isar_step : isar_step -> facts |
47 |
val proof_methods_of_isar_step : isar_step -> proof_method list |
|
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
|
48 |
|
54765 | 49 |
val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
55212 | 50 |
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
51 |
val add_isar_steps : isar_step list -> int -> int |
|
52454 | 52 |
|
55212 | 53 |
structure Canonical_Label_Tab : TABLE |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
54 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
55 |
val canonical_label_ord : (label * label) -> order |
55220 | 56 |
|
57 |
val chain_isar_proof : isar_proof -> isar_proof |
|
58 |
val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof |
|
55213 | 59 |
val relabel_isar_proof_canonically : isar_proof -> isar_proof |
55282 | 60 |
val relabel_isar_proof_nicely : isar_proof -> isar_proof |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
61 |
|
55257 | 62 |
val string_of_isar_proof : Proof.context -> int -> int -> |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
63 |
(label -> proof_method list -> string) -> isar_proof -> string |
54504 | 64 |
end; |
50259 | 65 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
66 |
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = |
50259 | 67 |
struct |
68 |
||
55211 | 69 |
open ATP_Util |
70 |
open ATP_Proof |
|
71 |
open ATP_Problem_Generate |
|
72 |
open ATP_Proof_Reconstruct |
|
73 |
open Sledgehammer_Util |
|
74 |
open Sledgehammer_Reconstructor |
|
75 |
open Sledgehammer_Isar_Annotate |
|
76 |
||
50259 | 77 |
type label = string * int |
54534 | 78 |
type facts = label list * string list (* local and global facts *) |
50259 | 79 |
|
51178 | 80 |
datatype isar_qualifier = Show | Then |
50259 | 81 |
|
55218 | 82 |
datatype proof_method = |
55257 | 83 |
Metis_Method of string option * string option | |
55284 | 84 |
Meson_Method | |
85 |
SMT_Method | |
|
55257 | 86 |
Simp_Method | |
87 |
Simp_Size_Method | |
|
88 |
Auto_Method | |
|
89 |
Fastforce_Method | |
|
90 |
Force_Method | |
|
91 |
Arith_Method | |
|
92 |
Blast_Method | |
|
93 |
Algebra_Method |
|
55218 | 94 |
|
52454 | 95 |
datatype isar_proof = |
54700 | 96 |
Proof of (string * typ) list * (label * term) list * isar_step list |
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
|
97 |
and isar_step = |
50259 | 98 |
Let of term * term | |
55280 | 99 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list |
100 |
* facts * proof_method list |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
101 |
|
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
|
102 |
val no_label = ("", ~1) |
50259 | 103 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
104 |
val label_ord = pairself swap #> prod_ord int_ord fast_string_ord |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
105 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
106 |
fun string_of_label (s, num) = s ^ string_of_int num |
50259 | 107 |
|
55222 | 108 |
fun string_of_proof_method meth = |
55218 | 109 |
(case meth of |
55257 | 110 |
Metis_Method (NONE, NONE) => "metis" |
111 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
|
112 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
|
55284 | 113 |
| Meson_Method => "meson" |
114 |
| SMT_Method => "smt" |
|
55218 | 115 |
| Simp_Method => "simp" |
55257 | 116 |
| Simp_Size_Method => "simp add: size_ne_size_imp_ne" |
55218 | 117 |
| Auto_Method => "auto" |
118 |
| Fastforce_Method => "fastforce" |
|
119 |
| Force_Method => "force" |
|
120 |
| Arith_Method => "arith" |
|
121 |
| Blast_Method => "blast" |
|
55219 | 122 |
| Algebra_Method => "algebra") |
55218 | 123 |
|
55260 | 124 |
fun steps_of_isar_proof (Proof (_, _, steps)) = steps |
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
|
125 |
|
55280 | 126 |
fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
127 |
| label_of_isar_step _ = NONE |
51178 | 128 |
|
55281 | 129 |
fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _)) = subs |
130 |
| subproofs_of_isar_step _ = [] |
|
52454 | 131 |
|
55280 | 132 |
fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts |
55279 | 133 |
| facts_of_isar_step _ = ([], []) |
134 |
||
55280 | 135 |
fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths |
55279 | 136 |
| proof_methods_of_isar_step _ = [] |
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
|
137 |
|
55212 | 138 |
fun fold_isar_step f step = |
55281 | 139 |
fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step |
55212 | 140 |
and fold_isar_steps f = fold (fold_isar_step f) |
52454 | 141 |
|
54765 | 142 |
fun map_isar_steps f = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
143 |
let |
55212 | 144 |
fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps) |
145 |
and map_step (step as Let _) = f step |
|
55281 | 146 |
| map_step (Prove (qs, xs, l, t, subs, facts, meths)) = |
147 |
f (Prove (qs, xs, l, t, map map_proof subs, facts, meths)) |
|
55212 | 148 |
in map_proof end |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
149 |
|
55212 | 150 |
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
151 |
|
55211 | 152 |
(* canonical proof labels: 1, 2, 3, ... in post traversal order *) |
52557 | 153 |
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|
55212 | 155 |
structure Canonical_Label_Tab = Table( |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
156 |
type key = label |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
val ord = canonical_label_ord) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
|
55220 | 159 |
fun chain_qs_lfs NONE lfs = ([], lfs) |
160 |
| chain_qs_lfs (SOME l0) lfs = |
|
161 |
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) |
|
55281 | 162 |
fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) = |
55220 | 163 |
let val (qs', lfs) = chain_qs_lfs lbl lfs in |
55281 | 164 |
Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths) |
55220 | 165 |
end |
166 |
| chain_isar_step _ step = step |
|
167 |
and chain_isar_steps _ [] = [] |
|
168 |
| chain_isar_steps (prev as SOME _) (i :: is) = |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
169 |
chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
170 |
| chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is |
55220 | 171 |
and chain_isar_proof (Proof (fix, assms, steps)) = |
172 |
Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps) |
|
173 |
||
174 |
fun kill_useless_labels_in_isar_proof proof = |
|
175 |
let |
|
176 |
val used_ls = |
|
55279 | 177 |
fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] |
55220 | 178 |
|
179 |
fun kill_label l = if member (op =) used_ls l then l else no_label |
|
180 |
||
55281 | 181 |
fun kill_step (Prove (qs, xs, l, t, subs, facts, meths)) = |
182 |
Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths) |
|
55220 | 183 |
| kill_step step = step |
184 |
and kill_proof (Proof (fix, assms, steps)) = |
|
185 |
Proof (fix, map (apfst kill_label) assms, map kill_step steps) |
|
186 |
in |
|
187 |
kill_proof proof |
|
188 |
end |
|
189 |
||
55213 | 190 |
fun relabel_isar_proof_canonically proof = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
192 |
fun next_label l (next, subst) = |
54534 | 193 |
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
194 |
|
55281 | 195 |
fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) = |
54534 | 196 |
let |
55281 | 197 |
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs |
198 |
val ((subs', l'), accum') = accum |
|
199 |
|> fold_map relabel_proof subs |
|
200 |
||>> next_label l |
|
54534 | 201 |
in |
55281 | 202 |
(Prove (qs, fix, l', t, subs', (lfs', gfs), meths), accum') |
54534 | 203 |
end |
55281 | 204 |
| relabel_step step accum = (step, accum) |
205 |
and relabel_proof (Proof (fix, assms, steps)) = |
|
206 |
fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms |
|
207 |
##>> fold_map relabel_step steps |
|
208 |
#>> (fn (assms, steps) => Proof (fix, assms, steps)) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
209 |
in |
55279 | 210 |
fst (relabel_proof proof (0, [])) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
211 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
212 |
|
55220 | 213 |
val assume_prefix = "a" |
214 |
val have_prefix = "f" |
|
215 |
||
55282 | 216 |
val relabel_isar_proof_nicely = |
55220 | 217 |
let |
55281 | 218 |
fun next_label depth prefix l (accum as (next, subst)) = |
55220 | 219 |
if l = no_label then |
55281 | 220 |
(l, accum) |
55220 | 221 |
else |
222 |
let val l' = (replicate_string (depth + 1) prefix, next) in |
|
55281 | 223 |
(l', (next + 1, (l, l') :: subst)) |
55220 | 224 |
end |
225 |
||
55281 | 226 |
fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) = |
55220 | 227 |
let |
55281 | 228 |
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs |
229 |
val (l', accum' as (next', subst')) = next_label depth have_prefix l accum |
|
230 |
val subs' = map (relabel_proof subst' (depth + 1)) subs |
|
55220 | 231 |
in |
55281 | 232 |
(Prove (qs, xs, l', t, subs', (lfs', gfs), meths), accum') |
55220 | 233 |
end |
55281 | 234 |
| relabel_step _ step accum = (step, accum) |
55220 | 235 |
and relabel_proof subst depth (Proof (fix, assms, steps)) = |
55281 | 236 |
(1, subst) |
237 |
|> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms |
|
238 |
||>> fold_map (relabel_step depth) steps |
|
239 |
|> (fn ((assms, steps), _) => Proof (fix, assms, steps)) |
|
55220 | 240 |
in |
241 |
relabel_proof [] 0 |
|
242 |
end |
|
243 |
||
55211 | 244 |
val indent_size = 2 |
245 |
||
55257 | 246 |
fun string_of_isar_proof ctxt i n comment_of proof = |
55211 | 247 |
let |
248 |
(* Make sure only type constraints inserted by the type annotation code are printed. *) |
|
249 |
val ctxt = |
|
250 |
ctxt |> Config.put show_markup false |
|
251 |
|> Config.put Printer.show_type_emphasis false |
|
252 |
|> Config.put show_types false |
|
253 |
|> Config.put show_sorts false |
|
254 |
|> Config.put show_consts false |
|
255 |
||
256 |
val register_fixes = map Free #> fold Variable.auto_fixes |
|
257 |
||
55216 | 258 |
fun add_str s' = apfst (suffix s') |
55211 | 259 |
|
260 |
fun of_indent ind = replicate_string (ind * indent_size) " " |
|
261 |
fun of_moreover ind = of_indent ind ^ "moreover\n" |
|
262 |
fun of_label l = if l = no_label then "" else string_of_label l ^ ": " |
|
263 |
||
264 |
fun of_obtain qs nr = |
|
265 |
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " |
|
266 |
else if nr = 1 orelse member (op =) qs Then then "then " |
|
267 |
else "") ^ "obtain" |
|
268 |
||
269 |
fun of_show_have qs = if member (op =) qs Show then "show" else "have" |
|
270 |
fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" |
|
271 |
||
272 |
fun of_have qs nr = |
|
273 |
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs |
|
274 |
else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs |
|
275 |
else of_show_have qs |
|
276 |
||
277 |
fun add_term term (s, ctxt) = |
|
278 |
(s ^ (term |
|
279 |
|> singleton (Syntax.uncheck_terms ctxt) |
|
55213 | 280 |
|> annotate_types_in_term ctxt |
55211 | 281 |
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |
282 |
|> simplify_spaces |
|
283 |
|> maybe_quote), |
|
284 |
ctxt |> Variable.auto_fixes term) |
|
285 |
||
286 |
fun with_facts none _ [] [] = none |
|
287 |
| with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss)) |
|
288 |
||
289 |
val using_facts = with_facts "" (enclose "using " " ") |
|
55257 | 290 |
|
291 |
fun maybe_paren s = s |> String.isSubstring " " s ? enclose "(" ")" |
|
292 |
fun by_facts meth ls ss = |
|
293 |
"by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss |
|
294 |
||
295 |
fun is_direct_method (Metis_Method _) = true |
|
296 |
| is_direct_method Meson_Method = true |
|
55284 | 297 |
| is_direct_method SMT_Method = true |
55257 | 298 |
| is_direct_method _ = false |
55211 | 299 |
|
300 |
(* Local facts are always passed via "using", which affects "meson" and "metis". This is |
|
301 |
arguably stylistically superior, because it emphasises the structure of the proof. It is also |
|
302 |
more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" |
|
303 |
and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) |
|
55257 | 304 |
fun of_method ls ss meth = |
55281 | 305 |
let val direct = is_direct_method meth in |
306 |
using_facts ls (if direct then [] else ss) ^ |
|
307 |
by_facts (string_of_proof_method meth) [] (if direct then ss else []) |
|
308 |
end |
|
55211 | 309 |
|
310 |
fun of_free (s, T) = |
|
311 |
maybe_quote s ^ " :: " ^ |
|
312 |
maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) |
|
313 |
||
314 |
fun add_frees xs (s, ctxt) = |
|
315 |
(s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) |
|
316 |
||
317 |
fun add_fix _ [] = I |
|
55281 | 318 |
| add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n" |
55211 | 319 |
|
320 |
fun add_assm ind (l, t) = |
|
55281 | 321 |
add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n" |
55211 | 322 |
|
323 |
fun of_subproof ind ctxt proof = |
|
324 |
let |
|
325 |
val ind = ind + 1 |
|
326 |
val s = of_proof ind ctxt proof |
|
327 |
val prefix = "{ " |
|
328 |
val suffix = " }" |
|
329 |
in |
|
330 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
|
331 |
String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ |
|
332 |
suffix ^ "\n" |
|
333 |
end |
|
334 |
and of_subproofs _ _ _ [] = "" |
|
55281 | 335 |
| of_subproofs ind ctxt qs subs = |
55211 | 336 |
(if member (op =) qs Then then of_moreover ind else "") ^ |
55281 | 337 |
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs) |
338 |
and add_step_pre ind qs subs (s, ctxt) = |
|
339 |
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt) |
|
55211 | 340 |
and add_step ind (Let (t1, t2)) = |
55216 | 341 |
add_str (of_indent ind ^ "let ") |
55281 | 342 |
#> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n" |
343 |
| add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _)) = |
|
344 |
add_step_pre ind qs subs |
|
55211 | 345 |
#> (case xs of |
55281 | 346 |
[] => add_str (of_have qs (length subs) ^ " ") |
347 |
| _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ") |
|
55217 | 348 |
#> add_str (of_label l) |
349 |
#> add_term t |
|
350 |
#> add_str (" " ^ |
|
55218 | 351 |
of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
352 |
(case comment_of l meths of |
55222 | 353 |
"" => "" |
354 |
| comment => " (* " ^ comment ^ " *)") ^ "\n") |
|
55211 | 355 |
and add_steps ind = fold (add_step ind) |
356 |
and of_proof ind ctxt (Proof (xs, assms, steps)) = |
|
55281 | 357 |
("", ctxt) |
358 |
|> add_fix ind xs |
|
359 |
|> fold (add_assm ind) assms |
|
360 |
|> add_steps ind steps |
|
361 |
|> fst |
|
55211 | 362 |
in |
363 |
(* One-step Metis proofs are pointless; better use the one-liner directly. *) |
|
364 |
(case proof of |
|
365 |
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) |
|
55280 | 366 |
| Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _)]) => "" |
55211 | 367 |
| _ => |
368 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
|
369 |
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ |
|
370 |
of_indent 0 ^ (if n <> 1 then "next" else "qed")) |
|
371 |
end |
|
372 |
||
54504 | 373 |
end; |