22 Trust_Playable of reconstructor * Time.time option| |
22 Trust_Playable of reconstructor * Time.time option| |
23 Failed_to_Preplay |
23 Failed_to_Preplay |
24 |
24 |
25 type minimize_command = string list -> string |
25 type minimize_command = string list -> string |
26 type one_line_params = |
26 type one_line_params = |
27 preplay * string * (string * locality) list * minimize_command * thm * int |
27 preplay * string * (string * locality) list * minimize_command * int * int |
28 type isar_params = |
28 type isar_params = |
29 bool * bool * int * type_system * string Symtab.table * int list list |
29 bool * bool * int * type_system * string Symtab.table * int list list |
30 * int * (string * locality) list vector * int Symtab.table * string proof |
30 * int * (string * locality) list vector * int Symtab.table * string proof |
|
31 * thm |
31 val repair_conjecture_shape_and_fact_names : |
32 val repair_conjecture_shape_and_fact_names : |
32 type_system -> string -> int list list -> int |
33 type_system -> string -> int list list -> int |
33 -> (string * locality) list vector -> int list |
34 -> (string * locality) list vector -> int list |
34 -> int list list * int * (string * locality) list vector * int list |
35 -> int list list * int * (string * locality) list vector * int list |
35 val used_facts_in_atp_proof : |
36 val used_facts_in_atp_proof : |
37 -> string proof -> (string * locality) list |
38 -> string proof -> (string * locality) list |
38 val used_facts_in_unsound_atp_proof : |
39 val used_facts_in_unsound_atp_proof : |
39 Proof.context -> type_system -> int list list -> int |
40 Proof.context -> type_system -> int list list -> int |
40 -> (string * locality) list vector -> 'a proof -> string list option |
41 -> (string * locality) list vector -> 'a proof -> string list option |
41 val uses_typed_helpers : int list -> 'a proof -> bool |
42 val uses_typed_helpers : int list -> 'a proof -> bool |
42 val reconstructor_name : reconstructor -> string |
|
43 val reconstructor_settings : reconstructor -> string |
|
44 val apply_on_subgoal : string -> int -> int -> string |
|
45 val command_call : string -> string list -> string |
|
46 val try_command_line : string -> (bool * Time.time) option -> string -> string |
|
47 val minimize_line : ('a list -> string) -> 'a list -> string |
|
48 val split_used_facts : |
|
49 (string * locality) list |
|
50 -> (string * locality) list * (string * locality) list |
|
51 val one_line_proof_text : one_line_params -> string |
43 val one_line_proof_text : one_line_params -> string |
52 val isar_proof_text : |
44 val isar_proof_text : |
53 Proof.context -> isar_params -> one_line_params -> string |
45 Proof.context -> isar_params -> one_line_params -> string |
54 val proof_text : |
46 val proof_text : |
55 Proof.context -> bool -> isar_params -> one_line_params -> string |
47 Proof.context -> bool -> isar_params -> one_line_params -> string |
75 Trust_Playable of reconstructor * Time.time option | |
67 Trust_Playable of reconstructor * Time.time option | |
76 Failed_to_Preplay |
68 Failed_to_Preplay |
77 |
69 |
78 type minimize_command = string list -> string |
70 type minimize_command = string list -> string |
79 type one_line_params = |
71 type one_line_params = |
80 preplay * string * (string * locality) list * minimize_command * thm * int |
72 preplay * string * (string * locality) list * minimize_command * int * int |
81 type isar_params = |
73 type isar_params = |
82 bool * bool * int * type_system * string Symtab.table * int list list * int |
74 bool * bool * int * type_system * string Symtab.table * int list list * int |
83 * (string * locality) list vector * int Symtab.table * string proof |
75 * (string * locality) list vector * int Symtab.table * string proof * thm |
84 |
76 |
85 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
77 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
86 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
78 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
87 |
79 |
88 val is_typed_helper_name = |
80 val is_typed_helper_name = |
289 val split_used_facts = |
281 val split_used_facts = |
290 List.partition (curry (op =) Chained o snd) |
282 List.partition (curry (op =) Chained o snd) |
291 #> pairself (sort_distinct (string_ord o pairself fst)) |
283 #> pairself (sort_distinct (string_ord o pairself fst)) |
292 |
284 |
293 fun one_line_proof_text (preplay, banner, used_facts, minimize_command, |
285 fun one_line_proof_text (preplay, banner, used_facts, minimize_command, |
294 goal, i) = |
286 subgoal, subgoal_count) = |
295 let |
287 let |
296 val (chained, extra) = split_used_facts used_facts |
288 val (chained, extra) = split_used_facts used_facts |
297 val (reconstructor, ext_time) = |
289 val (reconstructor, ext_time) = |
298 case preplay of |
290 case preplay of |
299 Preplayed (reconstructor, time) => |
291 Preplayed (reconstructor, time) => |
303 case time of |
295 case time of |
304 NONE => NONE |
296 NONE => NONE |
305 | SOME time => |
297 | SOME time => |
306 if time = Time.zeroTime then NONE else SOME (true, time)) |
298 if time = Time.zeroTime then NONE else SOME (true, time)) |
307 | Failed_to_Preplay => (NONE, NONE) |
299 | Failed_to_Preplay => (NONE, NONE) |
308 val n = Logic.count_prems (prop_of goal) |
|
309 val try_line = |
300 val try_line = |
310 case reconstructor of |
301 case reconstructor of |
311 SOME r => reconstructor_command r i n ([], map fst extra) |
302 SOME r => ([], map fst extra) |
|
303 |> reconstructor_command r subgoal subgoal_count |
312 |> try_command_line banner ext_time |
304 |> try_command_line banner ext_time |
313 | NONE => "Proof reconstruction failed." |
305 | NONE => "Proof reconstruction failed." |
314 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
306 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
315 |
307 |
316 (** Hard-core proof reconstruction: structured Isar proofs **) |
308 (** Hard-core proof reconstruction: structured Isar proofs **) |
1052 (if n <> 1 then "next" else "qed") |
1044 (if n <> 1 then "next" else "qed") |
1053 in do_proof end |
1045 in do_proof end |
1054 |
1046 |
1055 fun isar_proof_text ctxt |
1047 fun isar_proof_text ctxt |
1056 (debug, full_types, isar_shrink_factor, type_sys, pool, |
1048 (debug, full_types, isar_shrink_factor, type_sys, pool, |
1057 conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof) |
1049 conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal) |
1058 (one_line_params as (_, _, _, _, goal, i)) = |
1050 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
1059 let |
1051 let |
1060 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
1052 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal |
1061 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
1053 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
1062 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
1054 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
1063 val n = Logic.count_prems (prop_of goal) |
|
1064 val one_line_proof = one_line_proof_text one_line_params |
1055 val one_line_proof = one_line_proof_text one_line_params |
1065 fun isar_proof_for () = |
1056 fun isar_proof_for () = |
1066 case atp_proof |
1057 case atp_proof |
1067 |> isar_proof_from_atp_proof pool ctxt type_sys tfrees |
1058 |> isar_proof_from_atp_proof pool ctxt type_sys tfrees |
1068 isar_shrink_factor conjecture_shape facts_offset |
1059 isar_shrink_factor conjecture_shape facts_offset |
1070 |> redirect_proof hyp_ts concl_t |
1061 |> redirect_proof hyp_ts concl_t |
1071 |> kill_duplicate_assumptions_in_proof |
1062 |> kill_duplicate_assumptions_in_proof |
1072 |> then_chain_proof |
1063 |> then_chain_proof |
1073 |> kill_useless_labels_in_proof |
1064 |> kill_useless_labels_in_proof |
1074 |> relabel_proof |
1065 |> relabel_proof |
1075 |> string_for_proof ctxt full_types i n of |
1066 |> string_for_proof ctxt full_types subgoal subgoal_count of |
1076 "" => "\nNo structured proof available (proof too short)." |
1067 "" => "\nNo structured proof available (proof too short)." |
1077 | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof |
1068 | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof |
1078 val isar_proof = |
1069 val isar_proof = |
1079 if debug then |
1070 if debug then |
1080 isar_proof_for () |
1071 isar_proof_for () |