author  wenzelm 
Sat, 20 Aug 2011 19:21:03 +0200  
changeset 44333  cc53ce50f738 
parent 44331  aa9c1e9ef2ce 
child 49561  26fc70e983c2 
permissions  rwrr 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thm_deps.ML 
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"]); 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

34 
val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

35 
val entry = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

36 
{name = Long_Name.base_name name, 
28826
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

37 
ID = name, 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

38 
dir = space_implode "/" (session @ prefix), 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

39 
unfold = false, 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

40 
path = "", 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

41 
parents = parents}; 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

42 
in cons entry end; 
44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

43 
val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; 
28826
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

44 
in Present.display_graph (sort_wrt #ID deps) end; 
26697  45 

46 

47 
(* unused_thms *) 

48 

49 
fun unused_thms (base_thys, thys) = 

26185  50 
let 
33170  51 
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 globalonly;
wenzelm
parents:
37870
diff
changeset

52 
if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I 
33170  53 
else 
54 
let val {concealed, group, ...} = Name_Space.the_entry space name in 

55 
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

56 
(case Thm.derivation_name th of 
33170  57 
"" => I 
58 
 a => cons (a, (th, concealed, group)))) ths 

59 
end; 

60 
fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; 

61 

33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

62 
val new_thms = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37870
diff
changeset

63 
fold (add_facts o Global_Theory.facts_of) thys [] 
26699  64 
> sort_distinct (string_ord o pairself #1); 
28810  65 

33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

66 
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

67 
Proofterm.fold_body_thms 
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset

68 
(fn (a, _, _) => a <> "" ? Symtab.update (a, ())) 
44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

69 
(map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) 
44331  70 
Symtab.empty; 
33170  71 

41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset

72 
fun is_unused a = not (Symtab.defined used a); 
28810  73 

26185  74 
(* 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

75 
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

76 
if is_unused a then I 
33170  77 
else 
78 
(case group of 

79 
NONE => I 

33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

80 
 SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; 
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

81 

6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

82 
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 oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

83 
if not concealed andalso 
42473  84 
(* FIXME replace by robust treatment of thm groups *) 
85 
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

86 
is_unused a 
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

87 
then 
33170  88 
(case group of 
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

89 
NONE => ((a, th) :: thms, seen_groups) 
26185  90 
 SOME grp => 
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

91 
if Inttab.defined used_groups grp orelse 
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

92 
Inttab.defined seen_groups grp then q 
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

93 
else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) 
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
wenzelm
parents:
33642
diff
changeset

94 
else q) new_thms ([], Inttab.empty); 
26185  95 
in rev thms' end; 
96 

7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

97 
end; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

98 