7 *) |
7 *) |
8 |
8 |
9 signature SLEDGEHAMMER_PROOF = |
9 signature SLEDGEHAMMER_PROOF = |
10 sig |
10 sig |
11 type label = string * int |
11 type label = string * int |
|
12 val no_label : label |
12 type facts = label list * string list |
13 type facts = label list * string list |
|
14 val no_facts : facts |
13 |
15 |
14 datatype isar_qualifier = Show | Then | Ultimately |
16 datatype isar_qualifier = Show | Then |
15 |
17 |
16 datatype isar_step = |
18 datatype isar_step = |
17 Fix of (string * typ) list | |
19 Fix of (string * typ) list | |
18 Let of term * term | |
20 Let of term * term | |
19 Assume of label * term | |
21 Assume of label * term | |
20 Obtain of |
22 Obtain of |
21 isar_qualifier list * (string * typ) list * label * term * byline | |
23 isar_qualifier list * (string * typ) list * label * term * byline | |
22 Prove of isar_qualifier list * label * term * byline |
24 Prove of isar_qualifier list * label * term * byline |
23 and byline = |
25 and byline = |
24 By_Metis of facts | |
26 By_Metis of isar_step list list * facts |
25 Case_Split of isar_step list list | |
|
26 Subblock of isar_step list |
|
27 |
27 |
28 val string_for_label : label -> string |
28 val string_for_label : label -> string |
29 val metis_steps_top_level : isar_step list -> int |
29 val metis_steps_top_level : isar_step list -> int |
30 val metis_steps_total : isar_step list -> int |
30 val metis_steps_total : isar_step list -> int |
|
31 val term_of_assm : isar_step -> term |
|
32 val term_of_prove : isar_step -> term |
|
33 val split_proof : |
|
34 isar_step list -> (string * typ) list * (label * term) list * term |
31 end |
35 end |
32 |
36 |
33 structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
37 structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
34 struct |
38 struct |
35 |
39 |
36 type label = string * int |
40 type label = string * int |
|
41 val no_label = ("", ~1) |
37 type facts = label list * string list |
42 type facts = label list * string list |
|
43 val no_facts = ([],[]) |
38 |
44 |
39 datatype isar_qualifier = Show | Then | Ultimately |
45 datatype isar_qualifier = Show | Then |
40 |
46 |
41 datatype isar_step = |
47 datatype isar_step = |
42 Fix of (string * typ) list | |
48 Fix of (string * typ) list | |
43 Let of term * term | |
49 Let of term * term | |
44 Assume of label * term | |
50 Assume of label * term | |
45 Obtain of isar_qualifier list * (string * typ) list * label * term * byline | |
51 Obtain of isar_qualifier list * (string * typ) list * label * term * byline | |
46 Prove of isar_qualifier list * label * term * byline |
52 Prove of isar_qualifier list * label * term * byline |
47 and byline = |
53 and byline = |
48 By_Metis of facts | |
54 By_Metis of isar_step list list * facts |
49 Case_Split of isar_step list list | |
|
50 Subblock of isar_step list |
|
51 |
55 |
52 fun string_for_label (s, num) = s ^ string_of_int num |
56 fun string_for_label (s, num) = s ^ string_of_int num |
53 |
57 |
54 fun metis_steps_top_level proof = |
58 fun metis_steps_top_level proof = |
55 fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) |
59 fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) |
56 proof 0 |
60 proof 0 |
57 fun metis_steps_total proof = |
61 fun metis_steps_total proof = |
58 fold (fn Obtain _ => Integer.add 1 |
62 let |
59 | Prove (_, _, _, By_Metis _) => Integer.add 1 |
63 fun add_substeps subproofs i = |
60 | Prove (_, _, _, Case_Split cases) => |
64 Integer.add (fold Integer.add (map metis_steps_total subproofs) i) |
61 Integer.add (fold (Integer.add o metis_steps_total) cases 1) |
65 in |
62 | Prove (_, _, _, Subblock subproof) => |
66 fold |
63 Integer.add (metis_steps_total subproof + 1) |
67 (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 |
64 | _ => I) proof 0 |
68 | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 |
|
69 | _ => I) |
|
70 proof 0 |
|
71 end |
|
72 |
|
73 fun term_of_assm (Assume (_, t)) = t |
|
74 | term_of_assm _ = error "sledgehammer proof: unexpected constructor" |
|
75 fun term_of_prove (Prove (_, _, t, _)) = t |
|
76 | term_of_prove _ = error "sledgehammer proof: unexpected constructor" |
|
77 |
|
78 fun split_proof proof = |
|
79 let |
|
80 fun split_step step (fixes, assms, _) = |
|
81 (case step of |
|
82 Fix xs => (xs@fixes, assms, step) |
|
83 | Assume a => (fixes, a::assms, step) |
|
84 | _ => (fixes, assms, step)) |
|
85 val (fixes, assms, concl) = |
|
86 fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *) |
|
87 in |
|
88 (rev fixes, rev assms, term_of_prove concl) |
|
89 end |
65 |
90 |
66 end |
91 end |