author | blanchet |
Tue, 19 Nov 2013 18:38:25 +0100 | |
changeset 54504 | 096f7d452164 |
parent 54503 | b490e15a5e19 |
child 54534 | 3cad06ff414b |
permissions | -rw-r--r-- |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_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 |
||
50268 | 9 |
signature SLEDGEHAMMER_PROOF = |
50259 | 10 |
sig |
51239 | 11 |
type label = string * int |
52454 | 12 |
type facts = label list * string list (* local & global facts *) |
50268 | 13 |
|
51178 | 14 |
datatype isar_qualifier = Show | Then |
50268 | 15 |
|
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
|
16 |
datatype fix = Fix of (string * typ) list |
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
|
17 |
datatype assms = Assume of (label * term) list |
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
|
18 |
|
52454 | 19 |
datatype isar_proof = |
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
|
20 |
Proof of fix * assms * isar_step list |
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
|
21 |
and isar_step = |
50268 | 22 |
Let of term * term | |
52590 | 23 |
(* for |fix|>0, this is an obtain step; step may contain subproofs *) |
24 |
Prove of isar_qualifier list * fix * label * term * isar_proof list * byline |
|
50268 | 25 |
and byline = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
26 |
By of facts * proof_method |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
27 |
and proof_method = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
28 |
MetisM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
29 |
SimpM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
30 |
AutoM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
31 |
FastforceM | |
52629 | 32 |
ForceM | |
33 |
ArithM | |
|
34 |
BlastM |
|
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 |
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
|
37 |
val no_facts : facts |
50268 | 38 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
39 |
val label_ord : label * label -> order |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
40 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
41 |
val dummy_isar_step : isar_step |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
42 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
43 |
val string_of_label : label -> string |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
44 |
|
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
|
45 |
val fix_of_proof : isar_proof -> fix |
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
|
46 |
val assms_of_proof : isar_proof -> assms |
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
|
47 |
val steps_of_proof : isar_proof -> isar_step list |
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 |
|
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
|
49 |
val label_of_step : isar_step -> label option |
52454 | 50 |
val subproofs_of_step : isar_step -> isar_proof list option |
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
|
51 |
val byline_of_step : isar_step -> byline option |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
52 |
val proof_method_of_step : isar_step -> proof_method option |
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
|
53 |
|
52454 | 54 |
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a |
55 |
val fold_isar_steps : |
|
56 |
(isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
|
57 |
||
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
58 |
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
59 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
60 |
val map_facts_of_byline : (facts -> facts) -> byline -> byline |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
61 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
62 |
val add_proof_steps : isar_step list -> int -> int |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
63 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
64 |
(** canonical proof labels: 1, 2, 3, ... in post traversal order **) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
65 |
val canonical_label_ord : (label * label) -> order |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
66 |
val relabel_proof_canonically : isar_proof -> isar_proof |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
67 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
68 |
structure Canonical_Lbl_Tab : TABLE |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
69 |
|
54504 | 70 |
end; |
50259 | 71 |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50269
diff
changeset
|
72 |
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
50259 | 73 |
struct |
74 |
||
75 |
type label = string * int |
|
52454 | 76 |
type facts = label list * string list (* local & global facts *) |
50259 | 77 |
|
51178 | 78 |
datatype isar_qualifier = Show | Then |
50259 | 79 |
|
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
|
80 |
datatype fix = Fix of (string * typ) list |
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
|
81 |
datatype assms = Assume of (label * term) list |
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
|
82 |
|
52454 | 83 |
datatype isar_proof = |
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
|
84 |
Proof of fix * assms * isar_step list |
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
|
85 |
and isar_step = |
50259 | 86 |
Let of term * term | |
52454 | 87 |
(* for |fix|>0, this is an obtain step; step may contain subproofs *) |
88 |
Prove of isar_qualifier list * fix * label * term * isar_proof list * byline |
|
50259 | 89 |
and byline = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
90 |
By of facts * proof_method |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
91 |
and proof_method = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
92 |
MetisM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
93 |
SimpM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
94 |
AutoM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
95 |
FastforceM | |
52629 | 96 |
ForceM | |
97 |
ArithM | |
|
98 |
BlastM |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
99 |
|
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
|
100 |
val no_label = ("", ~1) |
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
|
101 |
val no_facts = ([],[]) |
50259 | 102 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
103 |
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
|
104 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
105 |
val dummy_isar_step = Let (Term.dummy, Term.dummy) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
106 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
107 |
fun string_of_label (s, num) = s ^ string_of_int num |
50259 | 108 |
|
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
|
109 |
fun fix_of_proof (Proof (fix, _, _)) = fix |
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
|
110 |
fun assms_of_proof (Proof (_, assms, _)) = assms |
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
|
111 |
fun steps_of_proof (Proof (_, _, steps)) = 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
|
112 |
|
52454 | 113 |
fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l |
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
|
114 |
| label_of_step _ = NONE |
51178 | 115 |
|
52454 | 116 |
fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs |
117 |
| subproofs_of_step _ = NONE |
|
118 |
||
119 |
fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline |
|
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
|
120 |
| byline_of_step _ = NONE |
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
|
121 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
122 |
fun proof_method_of_step (Prove (_, _, _, _, _, By(_, method))) = SOME method |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
123 |
| proof_method_of_step _ = NONE |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
124 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
125 |
fun fold_isar_steps f = fold (fold_isar_step f) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
126 |
and fold_isar_step f step s = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
127 |
fold (steps_of_proof #> fold_isar_steps f) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
128 |
(these (subproofs_of_step step)) s |
52454 | 129 |
|> f step |
130 |
||
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
131 |
fun map_isar_steps f proof = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
132 |
let |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
133 |
fun do_proof (Proof (fix, assms, steps)) = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
134 |
Proof (fix, assms, map do_step steps) |
51178 | 135 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
136 |
and do_step (step as Let _) = f step |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
137 |
| do_step (Prove (qs, xs, l, t, subproofs, by)) = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
138 |
let |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
139 |
val subproofs = map do_proof subproofs |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
140 |
val step = Prove (qs, xs, l, t, subproofs, by) |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
141 |
in |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
142 |
f step |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
143 |
end |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
144 |
in |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
145 |
do_proof proof |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
146 |
end |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
147 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
148 |
fun map_facts_of_byline f (By (facts, method)) = By (f facts, method) |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
149 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
150 |
val add_proof_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 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
152 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
153 |
(** canonical proof labels: 1, 2, 3, ... in post traversal order **) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|
52557 | 155 |
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
|
156 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
structure Canonical_Lbl_Tab = Table( |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
type key = label |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
159 |
val ord = canonical_label_ord) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
160 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
161 |
fun relabel_proof_canonically proof = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
162 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
163 |
val lbl = pair "" |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
164 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
165 |
fun next_label l (next, subst) = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
166 |
(lbl next, (next + 1, (l, lbl next) :: subst)) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
167 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
168 |
fun do_byline by (_, subst) = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
169 |
by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the))) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
170 |
handle Option.Option => |
52627 | 171 |
raise Fail "Sledgehammer_Proof: relabel_proof_canonically" |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
172 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
173 |
fun do_assm (l, t) state = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
174 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
175 |
val (l, state) = next_label l state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
176 |
in ((l, t), state) end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
177 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
178 |
fun do_proof (Proof (fix, Assume assms, steps)) state = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
179 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
180 |
val (assms, state) = fold_map do_assm assms state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
181 |
val (steps, state) = fold_map do_step steps state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
182 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
183 |
(Proof (fix, Assume assms, steps), state) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
184 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
185 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
186 |
and do_step (step as Let _) state = (step, state) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
187 |
| do_step (Prove (qs, fix, l, t, subproofs, by)) state= |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
188 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
189 |
val by = do_byline by state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
190 |
val (subproofs, state) = fold_map do_proof subproofs state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
191 |
val (l, state) = next_label l state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
192 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
193 |
(Prove (qs, fix, l, t, subproofs, by), state) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
194 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
195 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
196 |
fst (do_proof proof (0, [])) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
197 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
198 |
|
54504 | 199 |
end; |