1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
fun enable () = Thm.keep_derivs := ThmDeriv;
fun disable () = Thm.keep_derivs := MinDeriv;
enable();
fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
else
(case #session (Present.get_info thy) of
[x] => [x, "base"]
| xs => xs);
fun put_graph gr path =
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
fun is_thm_axm (Theorem _) = true
| is_thm_axm (Axiom _) = true
| is_thm_axm _ = false;
fun get_name (Theorem (s, _)) = s
| get_name (Axiom (s, _)) = s
| get_name _ = "";
fun make_deps_graph ((gra, parents), Join (ta, ders)) =
let
val name = get_name ta;
in
if is_thm_axm ta then
if is_none (Symtab.lookup (gra, name)) then
let
val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
val prefx = rev (tl (rev (NameSpace.unpack name)));
val session = (case prefx of
(x :: _) => (case ThyInfo.lookup_theory x of
(Some thy) => get_sess thy
| None => [])
| _ => ["global"])
in
(Symtab.update ((name,
{name = Sign.base_name name, ID = name,
dir = space_implode "/" (session @ prefx),
unfold = false, path = "", parents = parents'}), gra'), name ins parents)
end
else (gra, name ins parents)
else
foldl make_deps_graph ((gra, parents), ders)
end;
fun thm_deps thms =
let
val _ = writeln "Generating graph ...";
val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
map (#der o rep_thm) thms))));
val path = File.tmp_path (Path.unpack "theorems.graph");
val _ = put_graph gra path;
val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
in () end;
fun new_thm_deps thms =
let
val header = "Proof General, the theorem dependencies are: \"";
val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
map (#der o rep_thm) thms))));
val deps = foldl (op@) ([],(map #parents gra))
val msg = header ^ (space_implode " " deps) ^ "\""
in writeln msg end;
val old_qed = qed;
fun qed s =
let val _ = old_qed s
val proved_thm = thm s
in new_thm_deps [proved_thm] end;
|
