author  wenzelm 
Thu, 07 Oct 1999 14:32:18 +0200  
changeset 7783  9ace4017ead8 
parent 7765  fa28bac7903c 
child 7785  c06825c396e8 
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 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

10 
val thm_deps: thm list > unit 
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 

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

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

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

16 
fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"] 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

18 
(case #session (Present.get_info thy) of 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

19 
[x] => [x, "base"] 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

20 
 xs => xs); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

21 

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

22 
fun put_graph gr path = 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

23 
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

24 
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

25 
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

26 

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

27 
fun is_thm_axm (Theorem _) = true 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

28 
 is_thm_axm (Axiom _) = true 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

30 

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

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

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

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

34 

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

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

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

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

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

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

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

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

42 
val (gra', parents') = foldl make_deps_graph ((gra, []), ders); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

43 
val prefx = rev (tl (rev (NameSpace.unpack name))); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

44 
val session = (case prefx of 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

45 
(x :: _) => (case ThyInfo.lookup_theory x of 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

46 
(Some thy) => get_sess thy 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

47 
 None => []) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

48 
 _ => ["global"]) 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

50 
(Symtab.update_new ((name, 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

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

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

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

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

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

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

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

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

59 

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

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

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

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

63 
val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

64 
map (#der o rep_thm) thms)))); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

65 
val path = File.tmp_path (Path.unpack "theorems.graph"); 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

66 
val _ = put_graph gra path; 
7783  67 
val _ = execute ("$ISATOOL browser d " ^ Path.pack (Path.expand path) ^ " &"); 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

68 
in () end; 
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 
end; 
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

71 

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

72 
open ThmDeps; 