author | berghofe |
Thu, 07 Oct 1999 11:36:39 +0200 | |
changeset 7765 | fa28bac7903c |
child 7783 | 9ace4017ead8 |
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 |
|
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; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
67 |
val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
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; |