author | wenzelm |
Wed, 31 Dec 2014 20:42:45 +0100 | |
changeset 59210 | 8658b4290aed |
parent 59208 | 2486d625878b |
child 59936 | b8ffc3dc9e24 |
permissions | -rw-r--r-- |
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
1 |
(* Title: Pure/Tools/thm_deps.ML |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer, TU Muenchen |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
3 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
4 |
Visualize dependencies of theorems. |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
5 |
*) |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
6 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
7 |
signature THM_DEPS = |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
8 |
sig |
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37216
diff
changeset
|
9 |
val thm_deps: theory -> thm list -> unit |
26697 | 10 |
val unused_thms: theory list * theory list -> (string * thm) list |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
11 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
12 |
|
33391 | 13 |
structure Thm_Deps: THM_DEPS = |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
14 |
struct |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
15 |
|
26697 | 16 |
(* thm_deps *) |
17 |
||
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37216
diff
changeset
|
18 |
fun thm_deps thy thms = |
28810 | 19 |
let |
28826
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
20 |
fun add_dep ("", _, _) = I |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
21 |
| add_dep (name, _, PBody {thms = thms', ...}) = |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
22 |
let |
41489
8e2b8649507d
standardized split_last/last_elem towards List.last;
wenzelm
parents:
39557
diff
changeset
|
23 |
val prefix = #1 (split_last (Long_Name.explode name)); |
28826
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
24 |
val session = |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
25 |
(case prefix of |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
26 |
a :: _ => |
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37216
diff
changeset
|
27 |
(case try (Context.get_theory thy) a of |
28826
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
28 |
SOME thy => |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
29 |
(case Present.session_name thy of |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
30 |
"" => [] |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
31 |
| session => [session]) |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
32 |
| NONE => []) |
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
33 |
| _ => ["global"]); |
59208
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
34 |
val directory = space_implode "/" (session @ prefix); |
28826
3b460b6eadae
simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset
|
35 |
val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); |
59208
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
36 |
in |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
37 |
cons ((name, Graph_Display.session_node |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
38 |
{name = Long_Name.base_name name, directory = directory, |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
39 |
unfold = false, path = ""}), parents) |
2486d625878b
for graph display, prefer graph data structure over list with dependencies;
wenzelm
parents:
59207
diff
changeset
|
40 |
end; |
59210
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
41 |
in |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
42 |
Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [] |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
43 |
|> Graph_Display.display_graph |
8658b4290aed
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
wenzelm
parents:
59208
diff
changeset
|
44 |
end; |
26697 | 45 |
|
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
46 |
val _ = |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58028
diff
changeset
|
47 |
Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies" |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
57934
diff
changeset
|
48 |
(Parse.xthms1 >> (fn args => |
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
49 |
Toplevel.unknown_theory o Toplevel.keep (fn state => |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
50 |
thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args)))); |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
51 |
|
26697 | 52 |
|
53 |
(* unused_thms *) |
|
54 |
||
55 |
fun unused_thms (base_thys, thys) = |
|
26185 | 56 |
let |
33170 | 57 |
fun add_fact space (name, ths) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37870
diff
changeset
|
58 |
if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I |
33170 | 59 |
else |
60 |
let val {concealed, group, ...} = Name_Space.the_entry space name in |
|
61 |
fold_rev (fn th => |
|
36744
6e1f3d609a68
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents:
33769
diff
changeset
|
62 |
(case Thm.derivation_name th of |
33170 | 63 |
"" => I |
64 |
| a => cons (a, (th, concealed, group)))) ths |
|
65 |
end; |
|
66 |
fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; |
|
67 |
||
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
68 |
val new_thms = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37870
diff
changeset
|
69 |
fold (add_facts o Global_Theory.facts_of) thys [] |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
70 |
|> sort_distinct (string_ord o apply2 #1); |
28810 | 71 |
|
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
72 |
val used = |
32810
f3466a5645fa
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
wenzelm
parents:
32726
diff
changeset
|
73 |
Proofterm.fold_body_thms |
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
74 |
(fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset
|
75 |
(map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
44331 | 76 |
Symtab.empty; |
33170 | 77 |
|
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
78 |
fun is_unused a = not (Symtab.defined used a); |
28810 | 79 |
|
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
80 |
(*groups containing at least one used theorem*) |
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
81 |
val used_groups = fold (fn (a, (_, _, group)) => |
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
82 |
if is_unused a then I |
33170 | 83 |
else |
84 |
(case group of |
|
85 |
NONE => I |
|
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
86 |
| SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
87 |
|
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
88 |
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
89 |
if not concealed andalso |
42473 | 90 |
(* FIXME replace by robust treatment of thm groups *) |
91 |
member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso |
|
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
92 |
is_unused a |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
93 |
then |
33170 | 94 |
(case group of |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
95 |
NONE => ((a, th) :: thms, seen_groups) |
26185 | 96 |
| SOME grp => |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
97 |
if Inttab.defined used_groups grp orelse |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
98 |
Inttab.defined seen_groups grp then q |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
99 |
else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
100 |
else q) new_thms ([], Inttab.empty); |
26185 | 101 |
in rev thms' end; |
102 |
||
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
103 |
val _ = |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58028
diff
changeset
|
104 |
Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems" |
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
105 |
(Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) -- |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
106 |
Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range => |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
107 |
Toplevel.keep (fn state => |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
108 |
let |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
109 |
val thy = Toplevel.theory_of state; |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
110 |
val ctxt = Toplevel.context_of state; |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
111 |
fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
112 |
val get_theory = Context.get_theory thy; |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
113 |
in |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
114 |
unused_thms |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
115 |
(case opt_range of |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
116 |
NONE => (Theory.parents_of thy, [thy]) |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
117 |
| SOME (xs, NONE) => (map get_theory xs, [thy]) |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
118 |
| SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys)) |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
119 |
|> map pretty_thm |> Pretty.writeln_chunks |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
120 |
end))); |
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
121 |
|
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
122 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
123 |