author  wenzelm 
Tue, 27 Aug 2002 11:06:20 +0200  
changeset 13530  4813fdc0ef17 
parent 12239  ee360f910ec8 
child 14981  e73f8140af78 
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 
11819  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
7765
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 
Visualize dependencies of theorems. 
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 

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

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

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

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

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

13 

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

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

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

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

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

18 
val disable : unit > unit 
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 

11530  29 
fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) 
30 
 dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof []) 

31 
 dest_thm_axm _ = (("", []), MinProof []); 

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

32 

11530  33 
fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf) 
34 
 make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf) 

11612  35 
 make_deps_graph (p, prf1 %% prf2) = 
11530  36 
make_deps_graph (make_deps_graph (p, prf1), prf2) 
11612  37 
 make_deps_graph (p, prf % _) = make_deps_graph (p, prf) 
11530  38 
 make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs) 
39 
 make_deps_graph (p as (gra, parents), prf) = 

40 
let val ((name, tags), prf') = dest_thm_axm prf 

41 
in 

42 
if name <> "" andalso not (Drule.has_internal tags) then 

43 
if is_none (Symtab.lookup (gra, name)) then 

44 
let 

45 
val (gra', parents') = make_deps_graph ((gra, []), prf'); 

46 
val prefx = #1 (Library.split_last (NameSpace.unpack name)); 

47 
val session = 

48 
(case prefx of 

49 
(x :: _) => 

50 
(case ThyInfo.lookup_theory x of 

51 
Some thy => 

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

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

54 
 None => []) 

55 
 _ => ["global"]); 

56 
in 

12239
ee360f910ec8
Now handles different theorems with same name more gracefully.
berghofe
parents:
11819
diff
changeset

57 
if name mem parents' then (gra', parents union parents') 
ee360f910ec8
Now handles different theorems with same name more gracefully.
berghofe
parents:
11819
diff
changeset

58 
else (Symtab.update ((name, 
11530  59 
{name = Sign.base_name name, ID = name, 
60 
dir = space_implode "/" (session @ prefx), 

61 
unfold = false, path = "", parents = parents'}), gra'), 

62 
name ins parents) 

63 
end 

64 
else (gra, name ins parents) 

65 
else 

66 
make_deps_graph ((gra, parents), prf') 

67 
end; 

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

68 

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

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

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

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

72 
val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), 
13530  73 
map Thm.proof_of thms)))); 
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset

74 
val path = File.tmp_path (Path.unpack "theorems.graph"); 
9450  75 
val _ = Present.write_graph gra path; 
7853  76 
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

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

78 

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

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

80 

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

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

82 
open BasicThmDeps; 