author  berghofe 
Thu, 28 Feb 2008 17:34:15 +0100  
changeset 26185  e53165319347 
parent 26138  dc578de1d3e9 
child 26697  3b9eede40608 
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 
ID: $Id$ 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

3 
Author: Stefan Berghofer, TU Muenchen 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

4 

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

5 
Visualize dependencies of theorems. 
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 

7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

8 
signature BASIC_THM_DEPS = 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

9 
sig 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

10 
val thm_deps : thm list > unit 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

11 
end; 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

12 

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

13 
signature THM_DEPS = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

14 
sig 
7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

15 
include BASIC_THM_DEPS 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

16 
val enable : unit > unit 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

17 
val disable : unit > unit 
26185  18 
val unused_thms : theory list option * theory list > (string * thm) list 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

20 

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

21 
structure ThmDeps : THM_DEPS = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

23 

11530  24 
open Proofterm; 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

25 

11543
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11530
diff
changeset

26 
fun enable () = if ! proofs = 0 then proofs := 1 else (); 
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11530
diff
changeset

27 
fun disable () = proofs := 0; 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

28 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20854
diff
changeset

29 
fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20854
diff
changeset

30 
 dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], [])) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20854
diff
changeset

31 
 dest_thm_axm _ = ("", MinProof ([], [], [])); 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

32 

17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

33 
fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

34 
 make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

35 
 make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

36 
 make_deps_graph (prf % _) = make_deps_graph prf 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

37 
 make_deps_graph (MinProof (thms, axms, _)) = 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

38 
fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

39 
fold (make_deps_graph o Proofterm.proof_of_min_axm) axms 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

40 
 make_deps_graph prf = (fn p as (gra, parents) => 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20854
diff
changeset

41 
let val (name, prf') = dest_thm_axm prf 
11530  42 
in 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20854
diff
changeset

43 
if name <> "" then 
16894  44 
if not (Symtab.defined gra name) then 
11530  45 
let 
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

46 
val (gra', parents') = make_deps_graph prf' (gra, []); 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21646
diff
changeset

47 
val prefx = #1 (Library.split_last (NameSpace.explode name)); 
11530  48 
val session = 
49 
(case prefx of 

50 
(x :: _) => 

51 
(case ThyInfo.lookup_theory x of 

15531  52 
SOME thy => 
24562  53 
let val name = Present.session_name thy 
16268  54 
in if name = "" then [] else [name] end 
15531  55 
 NONE => []) 
11530  56 
 _ => ["global"]); 
57 
in 

20664  58 
if member (op =) parents' name then (gra', parents union parents') 
17412  59 
else (Symtab.update (name, 
11530  60 
{name = Sign.base_name name, ID = name, 
61 
dir = space_implode "/" (session @ prefx), 

17224  62 
unfold = false, path = "", parents = parents'}) gra', 
20854  63 
insert (op =) name parents) 
11530  64 
end 
20854  65 
else (gra, insert (op =) name parents) 
11530  66 
else 
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

67 
make_deps_graph prf' (gra, parents) 
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset

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

69 

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

70 
fun thm_deps thms = 
20578  71 
Present.display_graph 
26138  72 
(map snd (sort_wrt fst (Symtab.dest (fst 
73 
(fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))))); 

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

74 

26185  75 
fun unused_thms (opt_thys1, thys2) = 
76 
let 

77 
val thys = case opt_thys1 of 

78 
NONE => thys2 

79 
 SOME thys1 => 

80 
thys2 > 

81 
fold (curry (gen_union Theory.eq_thy)) (map Context.ancestors_of thys2) > 

82 
fold (subtract Theory.eq_thy) (thys1 :: map Context.ancestors_of thys1); 

83 
val thms = maps PureThy.thms_of thys; 

84 
val tab = fold Proofterm.thms_of_proof 

85 
(map (Proofterm.strip_thm o proof_of o snd) thms) Symtab.empty; 

86 
fun is_unused (s, thm) = case Symtab.lookup tab s of 

87 
NONE => true 

88 
 SOME ps => not (prop_of thm mem map fst ps); 

89 
(* groups containing at least one used theorem *) 

90 
val grps = fold (fn p as (_, thm) => if is_unused p then I else 

91 
case PureThy.get_group thm of 

92 
NONE => I  SOME grp => Symtab.update (grp, ())) thms Symtab.empty; 

93 
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => 

94 
if PureThy.get_kind thm mem [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] 

95 
andalso is_unused p 

96 
then 

97 
(case PureThy.get_group thm of 

98 
NONE => (p :: thms, grps') 

99 
 SOME grp => 

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

101 
if is_some (Symtab.lookup grps grp) then q 

102 
(* output at most one unused theorem per group *) 

103 
else if is_some (Symtab.lookup grps' grp) then q 

104 
else (p :: thms, Symtab.update (grp, ()) grps')) 

105 
else q) thms ([], Symtab.empty) 

106 
in rev thms' end; 

107 

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

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

109 

7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

110 
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps; 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

111 
open BasicThmDeps; 