author  wenzelm 
Thu, 17 Apr 2008 11:40:00 +0200  
changeset 26699  6c7e4d858bae 
parent 26697  3b9eede40608 
child 27865  27a8ad9612a3 
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 

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

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

9 
sig 
26697  10 
val enable: unit > unit 
11 
val disable: unit > unit 

12 
val thm_deps: thm list > unit 

13 
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

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

15 

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

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

18 

26697  19 
(* thm_deps *) 
20 

21 
fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ()); 

22 
fun disable () = proofs := 0; 

23 

24 
local 

25 

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

27 

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

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

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

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

31 

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

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

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

34 
 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

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

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

37 
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

38 
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

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

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

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

45 
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

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

49 
(x :: _) => 

50 
(case ThyInfo.lookup_theory x of 

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

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

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

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

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

68 

26697  69 
in 
70 

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

71 
fun thm_deps thms = 
20578  72 
Present.display_graph 
26138  73 
(map snd (sort_wrt fst (Symtab.dest (fst 
74 
(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

75 

26697  76 
end; 
77 

78 

79 
(* unused_thms *) 

80 

81 
fun unused_thms (base_thys, thys) = 

26185  82 
let 
26697  83 
fun add_fact (name, ths) = 
84 
if exists (fn thy => PureThy.defined_fact thy name) base_thys then I 

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

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

88 
> sort_distinct (string_ord o pairself #1); 

26185  89 
val tab = fold Proofterm.thms_of_proof 
26697  90 
(map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty; 
91 
fun is_unused (name, th) = case Symtab.lookup tab name of 

26185  92 
NONE => true 
26697  93 
 SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th)); 
26185  94 
(* groups containing at least one used theorem *) 
95 
val grps = fold (fn p as (_, thm) => if is_unused p then I else 

96 
case PureThy.get_group thm of 

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

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

26697  99 
if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm) 
26185  100 
andalso is_unused p 
101 
then 

102 
(case PureThy.get_group thm of 

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

104 
 SOME grp => 

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

26697  106 
if Symtab.defined grps grp then q 
26185  107 
(* output at most one unused theorem per group *) 
26697  108 
else if Symtab.defined grps' grp then q 
26185  109 
else (p :: thms, Symtab.update (grp, ()) grps')) 
110 
else q) thms ([], Symtab.empty) 

111 
in rev thms' end; 

112 

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

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

114 