9 signature SLEDGEHAMMER_ATP_RECONSTRUCT = |
9 signature SLEDGEHAMMER_ATP_RECONSTRUCT = |
10 sig |
10 sig |
11 type 'a proof = 'a ATP_Proof.proof |
11 type 'a proof = 'a ATP_Proof.proof |
12 type locality = Sledgehammer_Filter.locality |
12 type locality = Sledgehammer_Filter.locality |
13 type type_system = Sledgehammer_ATP_Translate.type_system |
13 type type_system = Sledgehammer_ATP_Translate.type_system |
|
14 |
|
15 datatype reconstructor = |
|
16 Metis | |
|
17 MetisFT | |
|
18 SMT of string |
|
19 |
|
20 datatype preplay = |
|
21 Preplayed of reconstructor * Time.time | |
|
22 Trust_Playable of reconstructor * Time.time option| |
|
23 Preplay_Failed |
|
24 |
14 type minimize_command = string list -> string |
25 type minimize_command = string list -> string |
15 type metis_params = |
26 type one_line_params = |
16 string * minimize_command * type_system * string proof * int |
27 preplay * string * (string * locality) list * minimize_command * thm * int |
17 * (string * locality) list vector * int list * thm * int |
|
18 type isar_params = |
28 type isar_params = |
19 bool * int * string Symtab.table * int list list * int Symtab.table |
29 bool * bool * int * type_system * string Symtab.table * int list list |
20 type text_result = string * (string * locality) list |
30 * int * (string * locality) list vector * int Symtab.table * string proof |
21 |
|
22 val repair_conjecture_shape_and_fact_names : |
31 val repair_conjecture_shape_and_fact_names : |
23 type_system -> string -> int list list -> int |
32 type_system -> string -> int list list -> int |
24 -> (string * locality) list vector -> int list |
33 -> (string * locality) list vector -> int list |
25 -> int list list * int * (string * locality) list vector * int list |
34 -> int list list * int * (string * locality) list vector * int list |
26 val used_facts_in_atp_proof : |
35 val used_facts_in_atp_proof : |
27 Proof.context -> type_system -> int -> (string * locality) list vector |
36 Proof.context -> type_system -> int -> (string * locality) list vector |
28 -> string proof -> (string * locality) list |
37 -> string proof -> (string * locality) list |
29 val used_facts_in_unsound_atp_proof : |
38 val used_facts_in_unsound_atp_proof : |
30 Proof.context -> type_system -> int list list -> int |
39 Proof.context -> type_system -> int list list -> int |
31 -> (string * locality) list vector -> string proof -> string list option |
40 -> (string * locality) list vector -> 'a proof -> string list option |
|
41 val uses_typed_helpers : int list -> 'a proof -> bool |
|
42 val reconstructor_name : reconstructor -> string |
|
43 val reconstructor_settings : reconstructor -> string |
32 val apply_on_subgoal : string -> int -> int -> string |
44 val apply_on_subgoal : string -> int -> int -> string |
33 val command_call : string -> string list -> string |
45 val command_call : string -> string list -> string |
34 val try_command_line : string -> string -> string |
46 val try_command_line : string -> (bool * Time.time) option -> string -> string |
35 val minimize_line : ('a list -> string) -> 'a list -> string |
47 val minimize_line : ('a list -> string) -> 'a list -> string |
36 val split_used_facts : |
48 val split_used_facts : |
37 (string * locality) list |
49 (string * locality) list |
38 -> (string * locality) list * (string * locality) list |
50 -> (string * locality) list * (string * locality) list |
39 val metis_proof_text : Proof.context -> metis_params -> text_result |
51 val one_line_proof_text : one_line_params -> string |
40 val isar_proof_text : |
52 val isar_proof_text : |
41 Proof.context -> isar_params -> metis_params -> text_result |
53 Proof.context -> isar_params -> one_line_params -> string |
42 val proof_text : |
54 val proof_text : |
43 Proof.context -> bool -> isar_params -> metis_params -> text_result |
55 Proof.context -> bool -> isar_params -> one_line_params -> string |
44 end; |
56 end; |
45 |
57 |
46 structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = |
58 structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = |
47 struct |
59 struct |
48 |
60 |
51 open Metis_Translate |
63 open Metis_Translate |
52 open Sledgehammer_Util |
64 open Sledgehammer_Util |
53 open Sledgehammer_Filter |
65 open Sledgehammer_Filter |
54 open Sledgehammer_ATP_Translate |
66 open Sledgehammer_ATP_Translate |
55 |
67 |
|
68 datatype reconstructor = |
|
69 Metis | |
|
70 MetisFT | |
|
71 SMT of string |
|
72 |
|
73 datatype preplay = |
|
74 Preplayed of reconstructor * Time.time | |
|
75 Trust_Playable of reconstructor * Time.time option | |
|
76 Preplay_Failed |
|
77 |
56 type minimize_command = string list -> string |
78 type minimize_command = string list -> string |
57 type metis_params = |
79 type one_line_params = |
58 string * minimize_command * type_system * string proof * int |
80 preplay * string * (string * locality) list * minimize_command * thm * int |
59 * (string * locality) list vector * int list * thm * int |
|
60 type isar_params = |
81 type isar_params = |
61 bool * int * string Symtab.table * int list list * int Symtab.table |
82 bool * bool * int * type_system * string Symtab.table * int list list * int |
62 type text_result = string * (string * locality) list |
83 * (string * locality) list vector * int Symtab.table * string proof |
63 |
84 |
64 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
85 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
65 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
86 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
66 |
87 |
67 val is_typed_helper_name = |
88 val is_typed_helper_name = |
221 SOME (map fst used_facts) |
242 SOME (map fst used_facts) |
222 else |
243 else |
223 NONE |
244 NONE |
224 end |
245 end |
225 |
246 |
|
247 fun uses_typed_helpers typed_helpers = |
|
248 exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name |
|
249 | _ => false) |
|
250 |
|
251 |
226 (** Soft-core proof reconstruction: Metis one-liner **) |
252 (** Soft-core proof reconstruction: Metis one-liner **) |
227 |
253 |
|
254 fun reconstructor_name Metis = "metis" |
|
255 | reconstructor_name MetisFT = "metisFT" |
|
256 | reconstructor_name (SMT _) = "smt" |
|
257 |
|
258 fun reconstructor_settings (SMT settings) = settings |
|
259 | reconstructor_settings _ = "" |
|
260 |
228 fun string_for_label (s, num) = s ^ string_of_int num |
261 fun string_for_label (s, num) = s ^ string_of_int num |
|
262 |
|
263 fun show_time NONE = "" |
|
264 | show_time (SOME ext_time) = " ~ " ^ string_from_ext_time ext_time |
229 |
265 |
230 fun set_settings "" = "" |
266 fun set_settings "" = "" |
231 | set_settings settings = "using [[" ^ settings ^ "]] " |
267 | set_settings settings = "using [[" ^ settings ^ "]] " |
232 fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " |
268 fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " |
233 | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " |
269 | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " |
234 | apply_on_subgoal settings i n = |
270 | apply_on_subgoal settings i n = |
235 "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n |
271 "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n |
236 fun command_call name [] = name |
272 fun command_call name [] = name |
237 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
273 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
238 fun try_command_line banner command = |
274 fun try_command_line banner time command = |
239 banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." |
275 banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "." |
240 fun using_labels [] = "" |
276 fun using_labels [] = "" |
241 | using_labels ls = |
277 | using_labels ls = |
242 "using " ^ space_implode " " (map string_for_label ls) ^ " " |
278 "using " ^ space_implode " " (map string_for_label ls) ^ " " |
243 fun metis_name full_types = if full_types then "metisFT" else "metis" |
279 fun reconstructor_command reconstructor i n (ls, ss) = |
244 fun metis_call full_types ss = command_call (metis_name full_types) ss |
280 using_labels ls ^ |
245 fun metis_command full_types i n (ls, ss) = |
281 apply_on_subgoal (reconstructor_settings reconstructor) i n ^ |
246 using_labels ls ^ apply_on_subgoal "" i n ^ metis_call full_types ss |
282 command_call (reconstructor_name reconstructor) ss |
247 fun minimize_line _ [] = "" |
283 fun minimize_line _ [] = "" |
248 | minimize_line minimize_command ss = |
284 | minimize_line minimize_command ss = |
249 case minimize_command ss of |
285 case minimize_command ss of |
250 "" => "" |
286 "" => "" |
251 | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "." |
287 | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "." |
252 |
288 |
253 val split_used_facts = |
289 val split_used_facts = |
254 List.partition (curry (op =) Chained o snd) |
290 List.partition (curry (op =) Chained o snd) |
255 #> pairself (sort_distinct (string_ord o pairself fst)) |
291 #> pairself (sort_distinct (string_ord o pairself fst)) |
256 |
292 |
257 fun uses_typed_helpers typed_helpers = |
293 fun one_line_proof_text (preplay, banner, used_facts, minimize_command, |
258 exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name |
294 goal, i) = |
259 | _ => false) |
295 let |
260 |
296 val (chained, extra) = split_used_facts used_facts |
261 fun metis_proof_text ctxt (banner, minimize_command, type_sys, atp_proof, |
297 val (reconstructor, ext_time) = |
262 facts_offset, fact_names, typed_helpers, goal, i) = |
298 case preplay of |
263 let |
299 Preplayed (reconstructor, time) => |
264 val (chained, extra) = |
300 (SOME reconstructor, (SOME (false, time))) |
265 atp_proof |> used_facts_in_atp_proof ctxt type_sys facts_offset fact_names |
301 | Trust_Playable (reconstructor, time) => |
266 |> split_used_facts |
302 (SOME reconstructor, |
267 val full_types = uses_typed_helpers typed_helpers atp_proof |
303 case time of |
|
304 NONE => NONE |
|
305 | SOME time => |
|
306 if time = Time.zeroTime then NONE else SOME (true, time)) |
|
307 | Preplay_Failed => (NONE, NONE) |
268 val n = Logic.count_prems (prop_of goal) |
308 val n = Logic.count_prems (prop_of goal) |
269 val metis = metis_command full_types i n ([], map fst extra) |
309 val try_line = |
270 in |
310 case reconstructor of |
271 (try_command_line banner metis ^ |
311 SOME r => reconstructor_command r i n ([], map fst extra) |
272 minimize_line minimize_command (map fst (extra @ chained)), |
312 |> try_command_line banner ext_time |
273 extra @ chained) |
313 | NONE => "Proof reconstruction failed." |
274 end |
314 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
275 |
315 |
276 (** Hard-core proof reconstruction: structured Isar proofs **) |
316 (** Hard-core proof reconstruction: structured Isar proofs **) |
277 |
317 |
278 (* Simple simplifications to ensure that sort annotations don't leave a trail of |
318 (* Simple simplifications to ensure that sort annotations don't leave a trail of |
279 spurious "True"s. *) |
319 spurious "True"s. *) |
974 (if member (op =) qs Then then |
1014 (if member (op =) qs Then then |
975 if member (op =) qs Show then "thus" else "hence" |
1015 if member (op =) qs Show then "thus" else "hence" |
976 else |
1016 else |
977 if member (op =) qs Show then "show" else "have") |
1017 if member (op =) qs Show then "show" else "have") |
978 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
1018 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
|
1019 val reconstructor = if full_types then MetisFT else Metis |
979 fun do_facts (ls, ss) = |
1020 fun do_facts (ls, ss) = |
980 metis_command full_types 1 1 |
1021 reconstructor_command reconstructor 1 1 |
981 (ls |> sort_distinct (prod_ord string_ord int_ord), |
1022 (ls |> sort_distinct (prod_ord string_ord int_ord), |
982 ss |> sort_distinct string_ord) |
1023 ss |> sort_distinct string_ord) |
983 and do_step ind (Fix xs) = |
1024 and do_step ind (Fix xs) = |
984 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
1025 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
985 | do_step ind (Let (t1, t2)) = |
1026 | do_step ind (Let (t1, t2)) = |
986 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
1027 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
987 | do_step ind (Assume (l, t)) = |
1028 | do_step ind (Assume (l, t)) = |
1010 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
1051 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
1011 (if n <> 1 then "next" else "qed") |
1052 (if n <> 1 then "next" else "qed") |
1012 in do_proof end |
1053 in do_proof end |
1013 |
1054 |
1014 fun isar_proof_text ctxt |
1055 fun isar_proof_text ctxt |
1015 (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) |
1056 (debug, full_types, isar_shrink_factor, type_sys, pool, |
1016 (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names, |
1057 conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof) |
1017 typed_helpers, goal, i)) = |
1058 (one_line_params as (_, _, _, _, goal, i)) = |
1018 let |
1059 let |
1019 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
1060 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
1020 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
1061 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
1021 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
1062 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
1022 val full_types = uses_typed_helpers typed_helpers atp_proof |
|
1023 val n = Logic.count_prems (prop_of goal) |
1063 val n = Logic.count_prems (prop_of goal) |
1024 val (one_line_proof, lemma_names) = metis_proof_text ctxt metis_params |
1064 val one_line_proof = one_line_proof_text one_line_params |
1025 fun isar_proof_for () = |
1065 fun isar_proof_for () = |
1026 case isar_proof_from_atp_proof pool ctxt type_sys tfrees |
1066 case atp_proof |
1027 isar_shrink_factor atp_proof conjecture_shape facts_offset |
1067 |> isar_proof_from_atp_proof pool ctxt type_sys tfrees |
1028 fact_names sym_tab params frees |
1068 isar_shrink_factor conjecture_shape facts_offset |
|
1069 fact_names sym_tab params frees |
1029 |> redirect_proof hyp_ts concl_t |
1070 |> redirect_proof hyp_ts concl_t |
1030 |> kill_duplicate_assumptions_in_proof |
1071 |> kill_duplicate_assumptions_in_proof |
1031 |> then_chain_proof |
1072 |> then_chain_proof |
1032 |> kill_useless_labels_in_proof |
1073 |> kill_useless_labels_in_proof |
1033 |> relabel_proof |
1074 |> relabel_proof |