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