1 (* Title: Pure/Thy/thm_deps.ML |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 |
|
4 Visualize dependencies of theorems. |
|
5 *) |
|
6 |
|
7 signature THM_DEPS = |
|
8 sig |
|
9 val thm_deps: theory -> thm list -> unit |
|
10 val unused_thms: theory list * theory list -> (string * thm) list |
|
11 end; |
|
12 |
|
13 structure Thm_Deps: THM_DEPS = |
|
14 struct |
|
15 |
|
16 (* thm_deps *) |
|
17 |
|
18 fun thm_deps thy thms = |
|
19 let |
|
20 fun add_dep ("", _, _) = I |
|
21 | add_dep (name, _, PBody {thms = thms', ...}) = |
|
22 let |
|
23 val prefix = #1 (split_last (Long_Name.explode name)); |
|
24 val session = |
|
25 (case prefix of |
|
26 a :: _ => |
|
27 (case try (Context.get_theory thy) a of |
|
28 SOME thy => |
|
29 (case Present.session_name thy of |
|
30 "" => [] |
|
31 | session => [session]) |
|
32 | NONE => []) |
|
33 | _ => ["global"]); |
|
34 val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); |
|
35 val entry = |
|
36 {name = Long_Name.base_name name, |
|
37 ID = name, |
|
38 dir = space_implode "/" (session @ prefix), |
|
39 unfold = false, |
|
40 path = "", |
|
41 parents = parents, |
|
42 content = []}; |
|
43 in cons entry end; |
|
44 val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; |
|
45 in Graph_Display.display_graph (sort_wrt #ID deps) end; |
|
46 |
|
47 |
|
48 (* unused_thms *) |
|
49 |
|
50 fun unused_thms (base_thys, thys) = |
|
51 let |
|
52 fun add_fact space (name, ths) = |
|
53 if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I |
|
54 else |
|
55 let val {concealed, group, ...} = Name_Space.the_entry space name in |
|
56 fold_rev (fn th => |
|
57 (case Thm.derivation_name th of |
|
58 "" => I |
|
59 | a => cons (a, (th, concealed, group)))) ths |
|
60 end; |
|
61 fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
|
62 |
|
63 val new_thms = |
|
64 fold (add_facts o Global_Theory.facts_of) thys [] |
|
65 |> sort_distinct (string_ord o pairself #1); |
|
66 |
|
67 val used = |
|
68 Proofterm.fold_body_thms |
|
69 (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
|
70 (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
|
71 Symtab.empty; |
|
72 |
|
73 fun is_unused a = not (Symtab.defined used a); |
|
74 |
|
75 (* groups containing at least one used theorem *) |
|
76 val used_groups = fold (fn (a, (_, _, group)) => |
|
77 if is_unused a then I |
|
78 else |
|
79 (case group of |
|
80 NONE => I |
|
81 | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; |
|
82 |
|
83 val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => |
|
84 if not concealed andalso |
|
85 (* FIXME replace by robust treatment of thm groups *) |
|
86 member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso |
|
87 is_unused a |
|
88 then |
|
89 (case group of |
|
90 NONE => ((a, th) :: thms, seen_groups) |
|
91 | SOME grp => |
|
92 if Inttab.defined used_groups grp orelse |
|
93 Inttab.defined seen_groups grp then q |
|
94 else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) |
|
95 else q) new_thms ([], Inttab.empty); |
|
96 in rev thms' end; |
|
97 |
|
98 end; |
|
99 |
|