|
1 (* Title: Pure/Thy/thm_deps.ML |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
|
4 |
|
5 Visualize dependencies of theorems. |
|
6 *) |
|
7 |
|
8 signature THM_DEPS = |
|
9 sig |
|
10 val thm_deps: thm list -> unit |
|
11 end; |
|
12 |
|
13 structure ThmDeps : THM_DEPS = |
|
14 struct |
|
15 |
|
16 fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"] |
|
17 else |
|
18 (case #session (Present.get_info thy) of |
|
19 [x] => [x, "base"] |
|
20 | xs => xs); |
|
21 |
|
22 fun put_graph gr path = |
|
23 File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
24 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
25 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
|
26 |
|
27 fun is_thm_axm (Theorem _) = true |
|
28 | is_thm_axm (Axiom _) = true |
|
29 | is_thm_axm _ = false; |
|
30 |
|
31 fun get_name (Theorem (s, _)) = s |
|
32 | get_name (Axiom (s, _)) = s |
|
33 | get_name _ = ""; |
|
34 |
|
35 fun make_deps_graph ((gra, parents), Join (ta, ders)) = |
|
36 let |
|
37 val name = get_name ta; |
|
38 in |
|
39 if is_thm_axm ta then |
|
40 if is_none (Symtab.lookup (gra, name)) then |
|
41 let |
|
42 val (gra', parents') = foldl make_deps_graph ((gra, []), ders); |
|
43 val prefx = rev (tl (rev (NameSpace.unpack name))); |
|
44 val session = (case prefx of |
|
45 (x :: _) => (case ThyInfo.lookup_theory x of |
|
46 (Some thy) => get_sess thy |
|
47 | None => []) |
|
48 | _ => ["global"]) |
|
49 in |
|
50 (Symtab.update_new ((name, |
|
51 {name = Sign.base_name name, ID = name, |
|
52 dir = space_implode "/" (session @ prefx), |
|
53 unfold = false, path = "", parents = parents'}), gra'), name ins parents) |
|
54 end |
|
55 else (gra, name ins parents) |
|
56 else |
|
57 foldl make_deps_graph ((gra, parents), ders) |
|
58 end; |
|
59 |
|
60 fun thm_deps thms = |
|
61 let |
|
62 val _ = writeln "Generating graph ..."; |
|
63 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |
|
64 map (#der o rep_thm) thms)))); |
|
65 val path = File.tmp_path (Path.unpack "theorems.graph"); |
|
66 val _ = put_graph gra path; |
|
67 val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
|
68 in () end; |
|
69 |
|
70 end; |
|
71 |
|
72 open ThmDeps; |