author  wenzelm 
Wed, 02 Aug 2000 19:40:14 +0200  
changeset 9502  50ec59aff389 
parent 9450  c97dba47e504 
child 11530  b6e21f6cfacd 
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 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

19 

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

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

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

22 

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

23 
fun enable () = Thm.keep_derivs := ThmDeriv; 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

24 
fun disable () = Thm.keep_derivs := MinDeriv; 
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset

25 

9450  26 
fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags; 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

27 

9450  28 
fun is_thm_axm (Theorem x) = not (is_internal x) 
29 
 is_thm_axm (Axiom x) = not (is_internal x) 

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

30 
 is_thm_axm _ = false; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

31 

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

32 
fun get_name (Theorem (s, _)) = s 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

33 
 get_name (Axiom (s, _)) = s 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

34 
 get_name _ = ""; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

35 

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

36 
fun make_deps_graph ((gra, parents), Join (ta, ders)) = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

38 
val name = get_name ta; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

40 
if is_thm_axm ta then 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

41 
if is_none (Symtab.lookup (gra, name)) then 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

43 
val (gra', parents') = foldl make_deps_graph ((gra, []), ders); 
9450  44 
val prefx = #1 (Library.split_last (NameSpace.unpack name)); 
45 
val session = 

46 
(case prefx of 

47 
(x :: _) => 

48 
(case ThyInfo.lookup_theory x of 

49 
Some thy => 

50 
let val name = #name (Present.get_info thy) 

51 
in if name = "" then [] else [name] end 

52 
 None => []) 

53 
 _ => ["global"]); 

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

54 
in 
7786  55 
(Symtab.update ((name, 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

56 
{name = Sign.base_name name, ID = name, 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

57 
dir = space_implode "/" (session @ prefx), 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

58 
unfold = false, path = "", parents = parents'}), gra'), name ins parents) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

60 
else (gra, name ins parents) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

62 
foldl make_deps_graph ((gra, parents), ders) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

64 

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

65 
fun thm_deps thms = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

67 
val _ = writeln "Generating graph ..."; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

68 
val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), 
9502  69 
map (#2 o #der o Thm.rep_thm) thms)))); 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

70 
val path = File.tmp_path (Path.unpack "theorems.graph"); 
9450  71 
val _ = Present.write_graph gra path; 
7853  72 
val _ = system ("$ISATOOL browser d " ^ Path.pack (Path.expand path) ^ " &"); 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

73 
in () end; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

74 

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

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

76 

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

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

78 
open BasicThmDeps; 