author  wenzelm 
Thu, 05 Mar 2009 12:08:00 +0100  
changeset 30280  eb98b49ef835 
parent 29606  fedb8be05f24 
child 30364  577edc39b501 
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 
26697  9 
val thm_deps: thm list > unit 
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 

26697  13 
structure ThmDeps: 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 

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

18 
fun thm_deps 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 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

23 
val prefix = #1 (Library.split_last (NameSpace.explode name)); 
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 :: _ => 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

27 
(case ThyInfo.lookup_theory a of 
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 = 
30280  36 
{name = NameSpace.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; 
3b460b6eadae
simplified thm_deps  no need to build a graph datastructure;
wenzelm
parents:
28817
diff
changeset

43 
val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) []; 
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 
26697  51 
fun add_fact (name, ths) = 
52 
if exists (fn thy => PureThy.defined_fact thy name) base_thys then I 

53 
else fold_rev (fn th => (case Thm.get_name th of "" => I  a => cons (a, th))) ths; 

26699  54 
val thms = 
55 
fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] 

56 
> sort_distinct (string_ord o pairself #1); 

28810  57 

58 
val tab = Proofterm.fold_body_thms 

28817  59 
(fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) 
28814  60 
(map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; 
28810  61 
fun is_unused (name, th) = 
62 
not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); 

63 

26185  64 
(* groups containing at least one used theorem *) 
65 
val grps = fold (fn p as (_, thm) => if is_unused p then I else 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

66 
case Thm.get_group thm of 
26185  67 
NONE => I  SOME grp => Symtab.update (grp, ())) thms Symtab.empty; 
68 
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

69 
if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) 
26185  70 
andalso is_unused p 
71 
then 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset

72 
(case Thm.get_group thm of 
26185  73 
NONE => (p :: thms, grps') 
74 
 SOME grp => 

75 
(* do not output theorem if another theorem in group has been used *) 

26697  76 
if Symtab.defined grps grp then q 
26185  77 
(* output at most one unused theorem per group *) 
26697  78 
else if Symtab.defined grps' grp then q 
26185  79 
else (p :: thms, Symtab.update (grp, ()) grps')) 
80 
else q) thms ([], Symtab.empty) 

81 
in rev thms' end; 

82 

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

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

84 