author | blanchet |
Thu, 30 Jan 2014 15:01:40 +0100 | |
changeset 55184 | 6e2295db4cf8 |
parent 55183 | 17ec4a29ef71 |
child 55186 | fafdf2424c57 |
permissions | -rw-r--r-- |
49883 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
49914 | 5 |
Isar proof reconstruction from ATP proofs. |
49883 | 6 |
*) |
7 |
||
52374 | 8 |
signature SLEDGEHAMMER_RECONSTRUCT = |
49883 | 9 |
sig |
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54770
diff
changeset
|
10 |
type atp_step_name = ATP_Proof.atp_step_name |
54495 | 11 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset
|
12 |
type 'a atp_proof = 'a ATP_Proof.atp_proof |
49914 | 13 |
type stature = ATP_Problem_Generate.stature |
54495 | 14 |
type one_line_params = Sledgehammer_Reconstructor.one_line_params |
49914 | 15 |
|
16 |
type isar_params = |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
17 |
bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm |
49914 | 18 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
19 |
val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int -> |
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
20 |
one_line_params -> string |
49883 | 21 |
end; |
22 |
||
54751 | 23 |
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT = |
49883 | 24 |
struct |
25 |
||
26 |
open ATP_Util |
|
49914 | 27 |
open ATP_Problem |
49883 | 28 |
open ATP_Proof |
29 |
open ATP_Problem_Generate |
|
30 |
open ATP_Proof_Reconstruct |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
31 |
open Sledgehammer_Util |
52555 | 32 |
open Sledgehammer_Reconstructor |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50262
diff
changeset
|
33 |
open Sledgehammer_Proof |
50258 | 34 |
open Sledgehammer_Annotate |
52555 | 35 |
open Sledgehammer_Print |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset
|
36 |
open Sledgehammer_Preplay |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51129
diff
changeset
|
37 |
open Sledgehammer_Compress |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52556
diff
changeset
|
38 |
open Sledgehammer_Try0 |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
52592
diff
changeset
|
39 |
open Sledgehammer_Minimize_Isar |
49914 | 40 |
|
41 |
structure String_Redirect = ATP_Proof_Redirect( |
|
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset
|
42 |
type key = atp_step_name |
49914 | 43 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
44 |
val string_of = fst) |
|
45 |
||
49883 | 46 |
open String_Redirect |
47 |
||
54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset
|
48 |
val e_skolemize_rules = ["skolemize", "shift_quantors"] |
54836 | 49 |
val spass_pirate_datatype_rule = "DT" |
54746 | 50 |
val vampire_skolemisation_rule = "skolemisation" |
51 |
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
|
54753 | 52 |
val z3_skolemize_rule = "sk" |
53 |
val z3_th_lemma_rule = "th-lemma" |
|
54746 | 54 |
|
54772 | 55 |
val skolemize_rules = |
56 |
e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] |
|
54746 | 57 |
|
54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset
|
58 |
val is_skolemize_rule = member (op =) skolemize_rules |
54755 | 59 |
val is_arith_rule = String.isPrefix z3_th_lemma_rule |
54836 | 60 |
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule |
54755 | 61 |
|
54501 | 62 |
fun raw_label_of_num num = (num, 0) |
49914 | 63 |
|
54501 | 64 |
fun label_of_clause [(num, _)] = raw_label_of_num num |
65 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
|
50005 | 66 |
|
54505 | 67 |
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) |
68 |
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) |
|
49914 | 69 |
|
54758 | 70 |
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) |
71 |
fun is_only_type_information t = t aconv @{prop True} |
|
72 |
||
73 |
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in |
|
54759 | 74 |
type information. *) |
54799 | 75 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
54770 | 76 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
77 |
definitions. *) |
|
54700 | 78 |
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse |
54755 | 79 |
role = Hypothesis orelse is_arith_rule rule then |
54746 | 80 |
line :: lines |
54505 | 81 |
else if role = Axiom then |
49914 | 82 |
(* Facts are not proof lines. *) |
54507 | 83 |
lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, [])) |
49914 | 84 |
else |
85 |
map (replace_dependencies_in_line (name, [])) lines |
|
54755 | 86 |
| add_line_pass1 line lines = line :: lines |
49914 | 87 |
|
54758 | 88 |
(* Recursively delete empty lines (type information) from the proof. |
89 |
(FIXME: needed? And why is "delete_dependency" so complicated?) *) |
|
54755 | 90 |
fun add_line_pass2 (line as (name, _, t, _, [])) lines = |
54507 | 91 |
if is_only_type_information t then delete_dependency name lines else line :: lines |
54755 | 92 |
| add_line_pass2 line lines = line :: lines |
49914 | 93 |
and delete_dependency name lines = |
54755 | 94 |
fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) [] |
49914 | 95 |
|
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54770
diff
changeset
|
96 |
fun add_lines_pass3 res [] = rev res |
54799 | 97 |
| add_lines_pass3 res ((name, role, t, rule, deps) :: lines) = |
55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
98 |
let |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
99 |
val is_last_line = null lines |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
100 |
|
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
101 |
fun looks_interesting () = |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
102 |
not (is_only_type_information t) andalso null (Term.add_tvars t []) |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
103 |
andalso length deps >= 2 andalso not (can the_single lines) |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
104 |
|
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
105 |
fun is_skolemizing_line (_, _, _, rule', deps') = |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
106 |
is_skolemize_rule rule' andalso member (op =) deps' name |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
107 |
fun is_before_skolemize_rule () = exists is_skolemizing_line lines |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
108 |
in |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
109 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
110 |
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
111 |
is_before_skolemize_rule () then |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
112 |
add_lines_pass3 ((name, role, t, rule, deps) :: res) lines |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
113 |
else |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
114 |
add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines) |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
115 |
end |
49914 | 116 |
|
52454 | 117 |
val add_labels_of_proof = |
54700 | 118 |
steps_of_proof |
119 |
#> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I)) |
|
49914 | 120 |
|
121 |
fun kill_useless_labels_in_proof proof = |
|
122 |
let |
|
51178 | 123 |
val used_ls = add_labels_of_proof proof [] |
54758 | 124 |
|
54700 | 125 |
fun kill_label l = if member (op =) used_ls l then l else no_label |
126 |
fun kill_assms assms = map (apfst kill_label) assms |
|
54758 | 127 |
|
54700 | 128 |
fun kill_step (Prove (qs, xs, l, t, subproofs, by)) = |
129 |
Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by) |
|
130 |
| kill_step step = step |
|
131 |
and kill_proof (Proof (fix, assms, steps)) = |
|
132 |
Proof (fix, kill_assms assms, map kill_step steps) |
|
133 |
in |
|
134 |
kill_proof proof |
|
135 |
end |
|
49914 | 136 |
|
54501 | 137 |
val assume_prefix = "a" |
138 |
val have_prefix = "f" |
|
139 |
||
49914 | 140 |
val relabel_proof = |
141 |
let |
|
54758 | 142 |
fun fresh_label depth prefix (accum as (l, subst, next)) = |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
143 |
if l = no_label then |
54758 | 144 |
accum |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
145 |
else |
54758 | 146 |
let val l' = (replicate_string (depth + 1) prefix, next) 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
|
147 |
(l', (l, l') :: subst, next + 1) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
148 |
end |
54700 | 149 |
|
150 |
fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) |
|
151 |
||
152 |
fun relabel_assm depth (l, t) (subst, next) = |
|
54507 | 153 |
let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix 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
|
154 |
((l, t), (subst, next)) |
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
|
155 |
end |
54700 | 156 |
|
157 |
fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst |
|
158 |
||
159 |
fun relabel_steps _ _ _ [] = [] |
|
160 |
| relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
161 |
let |
54507 | 162 |
val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix |
54700 | 163 |
val sub = relabel_proofs subst depth sub |
54759 | 164 |
val by = apfst (relabel_facts subst) by |
54700 | 165 |
in |
166 |
Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps |
|
167 |
end |
|
168 |
| relabel_steps subst depth next (step :: steps) = |
|
169 |
step :: relabel_steps subst depth next steps |
|
170 |
and relabel_proof subst depth (Proof (fix, assms, steps)) = |
|
171 |
let val (assms, subst) = relabel_assms subst depth assms in |
|
172 |
Proof (fix, assms, relabel_steps subst depth 1 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
|
173 |
end |
54700 | 174 |
and relabel_proofs subst depth = map (relabel_proof subst (depth + 1)) |
175 |
in |
|
176 |
relabel_proof [] 0 |
|
177 |
end |
|
49914 | 178 |
|
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset
|
179 |
val chain_direct_proof = |
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset
|
180 |
let |
54700 | 181 |
fun chain_qs_lfs NONE lfs = ([], lfs) |
182 |
| chain_qs_lfs (SOME l0) lfs = |
|
183 |
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
184 |
fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) = |
54700 | 185 |
let val (qs', lfs) = chain_qs_lfs lbl lfs in |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
186 |
Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss)) |
54700 | 187 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
188 |
| chain_step _ step = 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
|
189 |
and chain_steps _ [] = [] |
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
|
190 |
| chain_steps (prev as SOME _) (i :: is) = |
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
|
191 |
chain_step prev i :: chain_steps (label_of_step i) is |
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
|
192 |
| chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is |
54700 | 193 |
and chain_proof (Proof (fix, assms, steps)) = |
194 |
Proof (fix, assms, chain_steps (try (List.last #> fst) assms) 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
|
195 |
and chain_proofs proofs = map (chain_proof) proofs |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
196 |
in |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
197 |
chain_proof |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
198 |
end |
49883 | 199 |
|
49914 | 200 |
type isar_params = |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
201 |
bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm |
49914 | 202 |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
203 |
val arith_methodss = |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
204 |
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
205 |
Metis_Method], [Meson_Method]] |
54838
16511f84913c
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet
parents:
54836
diff
changeset
|
206 |
val datatype_methodss = [[Simp_Size_Method, Simp_Method]] |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
207 |
val metislike_methodss = |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
208 |
[[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method, |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
209 |
Force_Method], [Meson_Method]] |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
210 |
val rewrite_methodss = |
54801 | 211 |
[[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]] |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
212 |
val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]] |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
213 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
214 |
fun isar_proof_text ctxt debug isar_proofs isar_params |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
215 |
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
49883 | 216 |
let |
217 |
fun isar_proof_of () = |
|
218 |
let |
|
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
219 |
val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar, |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
220 |
try0_isar, atp_proof, goal) = try isar_params () |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
221 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
222 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
223 |
val (_, ctxt) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
224 |
params |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
225 |
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
226 |
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
227 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
228 |
val do_preplay = preplay_timeout <> Time.zeroTime |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
229 |
val try0_isar = try0_isar andalso do_preplay |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
230 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
231 |
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
232 |
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
233 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
234 |
fun get_role keep_role ((num, _), role, t, rule, _) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
235 |
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
236 |
|
49883 | 237 |
val atp_proof = |
238 |
atp_proof |
|
54755 | 239 |
|> rpair [] |-> fold_rev add_line_pass1 |
240 |
|> rpair [] |-> fold_rev add_line_pass2 |
|
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)
blanchet
parents:
54770
diff
changeset
|
241 |
|> add_lines_pass3 [] |
54700 | 242 |
|
54535
59737a43e044
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents:
54507
diff
changeset
|
243 |
val conjs = |
54700 | 244 |
map_filter (fn (name, role, _, _, _) => |
245 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
246 |
atp_proof |
|
54751 | 247 |
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof |
54700 | 248 |
val lems = |
249 |
map_filter (get_role (curry (op =) Lemma)) atp_proof |
|
54751 | 250 |
|> map (fn ((l, t), rule) => |
54753 | 251 |
let |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
252 |
val (skos, methss) = |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
253 |
if is_skolemize_rule rule then (skolems_of t, skolem_methodss) |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
254 |
else if is_arith_rule rule then ([], arith_methodss) |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
255 |
else ([], rewrite_methodss) |
54753 | 256 |
in |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
257 |
Prove ([], skos, l, t, [], (([], []), methss)) |
54753 | 258 |
end) |
54700 | 259 |
|
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
260 |
val bot = atp_proof |> List.last |> #1 |
54700 | 261 |
|
51145 | 262 |
val refute_graph = |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
263 |
atp_proof |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
264 |
|> map (fn (name, _, _, _, from) => (from, name)) |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
265 |
|> make_refute_graph bot |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
266 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
54700 | 267 |
|
51145 | 268 |
val axioms = axioms_of_refute_graph refute_graph conjs |
54700 | 269 |
|
51145 | 270 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
51156 | 271 |
val is_clause_tainted = exists (member (op =) tainted) |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
272 |
val steps = |
49883 | 273 |
Symtab.empty |
51201 | 274 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
54758 | 275 |
Symtab.update_new (s, (rule, t |
276 |
|> (if is_clause_tainted [name] then |
|
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
277 |
HOLogic.dest_Trueprop |
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
278 |
#> role <> Conjecture ? s_not |
54758 | 279 |
#> fold exists_of (map Var (Term.add_vars t [])) |
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
280 |
#> HOLogic.mk_Trueprop |
54758 | 281 |
else |
282 |
I)))) |
|
283 |
atp_proof |
|
54700 | 284 |
|
54755 | 285 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
54700 | 286 |
|
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54756
diff
changeset
|
287 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form |
50016 | 288 |
| prop_of_clause names = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
289 |
let |
54758 | 290 |
val lits = map (HOLogic.dest_Trueprop o snd) |
291 |
(map_filter (Symtab.lookup steps o fst) names) |
|
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
292 |
in |
54754 | 293 |
(case List.partition (can HOLogic.dest_not) lits of |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
294 |
(negs as _ :: _, pos as _ :: _) => |
54507 | 295 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
54754 | 296 |
| _ => fold (curry s_disj) lits @{term False}) |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
297 |
end |
50016 | 298 |
|> HOLogic.mk_Trueprop |> close_form |
54700 | 299 |
|
55169 | 300 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show |
54700 | 301 |
|
302 |
fun isar_steps outer predecessor accum [] = |
|
303 |
accum |
|
304 |
|> (if tainted = [] then |
|
305 |
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
306 |
((the_list predecessor, []), metislike_methodss))) |
54700 | 307 |
else |
308 |
I) |
|
309 |
|> rev |
|
54755 | 310 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
54700 | 311 |
let |
312 |
val l = label_of_clause c |
|
313 |
val t = prop_of_clause c |
|
54755 | 314 |
val rule = rule_of_clause_id id |
315 |
val skolem = is_skolemize_rule rule |
|
316 |
||
54700 | 317 |
fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by) |
318 |
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs |
|
54755 | 319 |
|
320 |
val deps = fold add_fact_of_dependencies gamma no_facts |
|
54836 | 321 |
val methss = |
322 |
if is_arith_rule rule then arith_methodss |
|
323 |
else if is_datatype_rule rule then datatype_methodss |
|
324 |
else metislike_methodss |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
325 |
val by = (deps, methss) |
54700 | 326 |
in |
327 |
if is_clause_tainted c then |
|
54712 | 328 |
(case gamma of |
54700 | 329 |
[g] => |
54755 | 330 |
if skolem andalso is_clause_tainted g then |
54751 | 331 |
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
332 |
isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] [] |
54700 | 333 |
end |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
334 |
else |
54700 | 335 |
do_rest l (prove [] by) |
54712 | 336 |
| _ => do_rest l (prove [] by)) |
54700 | 337 |
else |
54765 | 338 |
do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) |
54700 | 339 |
end |
340 |
| isar_steps outer predecessor accum (Cases cases :: infs) = |
|
341 |
let |
|
342 |
fun isar_case (c, infs) = |
|
343 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] infs |
|
344 |
val c = succedent_of_cases cases |
|
345 |
val l = label_of_clause c |
|
346 |
val t = prop_of_clause c |
|
347 |
val step = |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
348 |
Prove (maybe_show outer c [], [], l, t, |
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
349 |
map isar_case (filter_out (null o snd) cases), |
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
350 |
((the_list predecessor, []), metislike_methodss)) |
54700 | 351 |
in |
352 |
isar_steps outer (SOME l) (step :: accum) infs |
|
353 |
end |
|
354 |
and isar_proof outer fix assms lems infs = |
|
355 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
|
356 |
||
54831 | 357 |
val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) = |
51145 | 358 |
refute_graph |
54699 | 359 |
(* |
54751 | 360 |
|> tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
54699 | 361 |
*) |
51031
63d71b247323
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents:
51026
diff
changeset
|
362 |
|> redirect_graph axioms tainted bot |
54699 | 363 |
(* |
54751 | 364 |
|> tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
54699 | 365 |
*) |
54754 | 366 |
|> isar_proof true params assms lems |
54712 | 367 |
|> postprocess_remove_unreferenced_steps I |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset
|
368 |
|> relabel_proof_canonically |
54500 | 369 |
|> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay |
53761
4d34e267fba9
use configuration mechanism for low-level tracing
blanchet
parents:
53586
diff
changeset
|
370 |
preplay_timeout) |
54754 | 371 |
|
54828 | 372 |
val (play_outcome, isar_proof) = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset
|
373 |
isar_proof |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
374 |
|> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) |
53762 | 375 |
preplay_interface |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
376 |
|> try0_isar ? try0 preplay_timeout preplay_interface |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
377 |
|> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface) |
54831 | 378 |
|> `overall_preplay_outcome |
54758 | 379 |
||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof) |
54754 | 380 |
|
54500 | 381 |
val isar_text = |
382 |
string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof |
|
49883 | 383 |
in |
54754 | 384 |
(case isar_text of |
49883 | 385 |
"" => |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
386 |
if isar_proofs = SOME true then |
50671 | 387 |
"\nNo structured proof available (proof too simple)." |
49883 | 388 |
else |
389 |
"" |
|
390 |
| _ => |
|
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
391 |
let |
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
392 |
val msg = |
51203 | 393 |
(if verbose then |
54828 | 394 |
let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in |
395 |
[string_of_int num_steps ^ " step" ^ plural_s num_steps] |
|
396 |
end |
|
51203 | 397 |
else |
398 |
[]) @ |
|
54828 | 399 |
(if do_preplay then [string_of_play_outcome play_outcome] else []) |
50277 | 400 |
in |
54507 | 401 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
402 |
Active.sendback_markup [Markup.padding_command] isar_text |
|
54754 | 403 |
end) |
49883 | 404 |
end |
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
405 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
406 |
val one_line_proof = one_line_proof_text 0 one_line_params |
49883 | 407 |
val isar_proof = |
408 |
if debug then |
|
409 |
isar_proof_of () |
|
54754 | 410 |
else |
411 |
(case try isar_proof_of () of |
|
412 |
SOME s => s |
|
413 |
| NONE => |
|
414 |
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") |
|
49883 | 415 |
in one_line_proof ^ isar_proof end |
416 |
||
54824 | 417 |
fun isar_proof_would_be_a_good_idea (reconstr, play) = |
418 |
(case play of |
|
419 |
Played _ => reconstr = SMT |
|
54823 | 420 |
| Play_Timed_Out _ => true |
54824 | 421 |
| Play_Failed => true |
422 |
| Not_Played => false) |
|
51187
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
423 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
424 |
fun proof_text ctxt debug isar_proofs isar_params num_chained |
49883 | 425 |
(one_line_params as (preplay, _, _, _, _, _)) = |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
426 |
(if isar_proofs = SOME true orelse |
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
427 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
428 |
isar_proof_text ctxt debug isar_proofs isar_params |
49883 | 429 |
else |
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
430 |
one_line_proof_text num_chained) one_line_params |
49883 | 431 |
|
432 |
end; |