author | wenzelm |
Wed, 31 Jan 2001 22:16:22 +0100 | |
changeset 11012 | 8eb472444705 |
parent 9502 | 50ec59aff389 |
child 11530 | b6e21f6cfacd |
permissions | -rw-r--r-- |
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; |