|
1 (* Title: Pure/thm_deps.ML |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 Author: Makarius |
|
4 |
|
5 Dependencies of theorems wrt. internal derivation. |
|
6 *) |
|
7 |
|
8 signature THM_DEPS = |
|
9 sig |
|
10 val all_oracles: thm list -> Proofterm.oracle list |
|
11 val has_skip_proof: thm list -> bool |
|
12 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
|
13 val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list |
|
14 val pretty_thm_deps: theory -> thm list -> Pretty.T |
|
15 val unused_thms_cmd: theory list * theory list -> (string * thm) list |
|
16 end; |
|
17 |
|
18 structure Thm_Deps: THM_DEPS = |
|
19 struct |
|
20 |
|
21 (* oracles *) |
|
22 |
|
23 fun all_oracles thms = |
|
24 let |
|
25 fun collect (PBody {oracles, thms, ...}) = |
|
26 (if null oracles then I else apfst (cons oracles)) #> |
|
27 (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) => |
|
28 if Inttab.defined seen i then (res, seen) |
|
29 else |
|
30 let val body = Future.join (Proofterm.thm_node_body thm_node) |
|
31 in collect body (res, Inttab.update (i, ()) seen) end)); |
|
32 val bodies = map Thm.proof_body_of thms; |
|
33 in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; |
|
34 |
|
35 fun has_skip_proof thms = |
|
36 all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>); |
|
37 |
|
38 fun pretty_thm_oracles ctxt thms = |
|
39 let |
|
40 val thy = Proof_Context.theory_of ctxt; |
|
41 fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
|
42 | prt_oracle (name, SOME prop) = |
|
43 [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, |
|
44 Syntax.pretty_term_global thy prop]; |
|
45 in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; |
|
46 |
|
47 |
|
48 (* thm_deps *) |
|
49 |
|
50 fun thm_deps thy = |
|
51 let |
|
52 val lookup = Global_Theory.lookup_thm_id thy; |
|
53 fun deps (i, thm_node) res = |
|
54 if Inttab.defined res i then res |
|
55 else |
|
56 let val thm_id = Proofterm.thm_id (i, thm_node) in |
|
57 (case lookup thm_id of |
|
58 SOME thm_name => |
|
59 Inttab.update (i, SOME (thm_id, thm_name)) res |
|
60 | NONE => |
|
61 Inttab.update (i, NONE) res |
|
62 |> fold deps (Proofterm.thm_node_thms thm_node)) |
|
63 end; |
|
64 in |
|
65 fn thms => |
|
66 (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, []) |
|
67 |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) |
|
68 end; |
|
69 |
|
70 fun pretty_thm_deps thy thms = |
|
71 let |
|
72 val ctxt = Proof_Context.init_global thy; |
|
73 val items = |
|
74 map #2 (thm_deps thy thms) |
|
75 |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) |
|
76 |> sort_by (#2 o #1) |
|
77 |> map (fn ((marks, xname), i) => |
|
78 Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
|
79 in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
|
80 |
|
81 |
|
82 (* unused_thms_cmd *) |
|
83 |
|
84 fun unused_thms_cmd (base_thys, thys) = |
|
85 let |
|
86 fun add_fact transfer space (name, ths) = |
|
87 if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I |
|
88 else |
|
89 let val {concealed, group, ...} = Name_Space.the_entry space name in |
|
90 fold_rev (fn th => |
|
91 (case Thm.derivation_name th of |
|
92 "" => I |
|
93 | a => cons (a, (transfer th, concealed, group)))) ths |
|
94 end; |
|
95 fun add_facts thy = |
|
96 let |
|
97 val transfer = Global_Theory.transfer_theories thy; |
|
98 val facts = Global_Theory.facts_of thy; |
|
99 in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; |
|
100 |
|
101 val new_thms = |
|
102 fold add_facts thys [] |
|
103 |> sort_distinct (string_ord o apply2 #1); |
|
104 |
|
105 val used = |
|
106 Proofterm.fold_body_thms |
|
107 (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) |
|
108 (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
|
109 Symtab.empty; |
|
110 |
|
111 fun is_unused a = not (Symtab.defined used a); |
|
112 |
|
113 (*groups containing at least one used theorem*) |
|
114 val used_groups = fold (fn (a, (_, _, group)) => |
|
115 if is_unused a then I |
|
116 else |
|
117 (case group of |
|
118 NONE => I |
|
119 | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; |
|
120 |
|
121 val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => |
|
122 if not concealed andalso |
|
123 (* FIXME replace by robust treatment of thm groups *) |
|
124 Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a |
|
125 then |
|
126 (case group of |
|
127 NONE => ((a, th) :: thms, seen_groups) |
|
128 | SOME grp => |
|
129 if Inttab.defined used_groups grp orelse |
|
130 Inttab.defined seen_groups grp then q |
|
131 else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) |
|
132 else q) new_thms ([], Inttab.empty); |
|
133 in rev thms' end; |
|
134 |
|
135 end; |