18 end; |
18 end; |
19 |
19 |
20 structure ThmDeps : THM_DEPS = |
20 structure ThmDeps : THM_DEPS = |
21 struct |
21 struct |
22 |
22 |
23 fun enable () = Thm.keep_derivs := ThmDeriv; |
23 open Proofterm; |
24 fun disable () = Thm.keep_derivs := MinDeriv; |
|
25 |
24 |
26 fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags; |
25 fun enable () = keep_derivs := ThmDeriv; |
|
26 fun disable () = keep_derivs := MinDeriv; |
27 |
27 |
28 fun is_thm_axm (Theorem x) = not (is_internal x) |
28 fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) |
29 | is_thm_axm (Axiom x) = not (is_internal x) |
29 | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof []) |
30 | is_thm_axm _ = false; |
30 | dest_thm_axm _ = (("", []), MinProof []); |
31 |
31 |
32 fun get_name (Theorem (s, _)) = s |
32 fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf) |
33 | get_name (Axiom (s, _)) = s |
33 | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf) |
34 | get_name _ = ""; |
34 | make_deps_graph (p, prf1 % prf2) = |
35 |
35 make_deps_graph (make_deps_graph (p, prf1), prf2) |
36 fun make_deps_graph ((gra, parents), Join (ta, ders)) = |
36 | make_deps_graph (p, prf %% _) = make_deps_graph (p, prf) |
37 let |
37 | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs) |
38 val name = get_name ta; |
38 | make_deps_graph (p as (gra, parents), prf) = |
39 in |
39 let val ((name, tags), prf') = dest_thm_axm prf |
40 if is_thm_axm ta then |
40 in |
41 if is_none (Symtab.lookup (gra, name)) then |
41 if name <> "" andalso not (Drule.has_internal tags) then |
42 let |
42 if is_none (Symtab.lookup (gra, name)) then |
43 val (gra', parents') = foldl make_deps_graph ((gra, []), ders); |
43 let |
44 val prefx = #1 (Library.split_last (NameSpace.unpack name)); |
44 val (gra', parents') = make_deps_graph ((gra, []), prf'); |
45 val session = |
45 val prefx = #1 (Library.split_last (NameSpace.unpack name)); |
46 (case prefx of |
46 val session = |
47 (x :: _) => |
47 (case prefx of |
48 (case ThyInfo.lookup_theory x of |
48 (x :: _) => |
49 Some thy => |
49 (case ThyInfo.lookup_theory x of |
50 let val name = #name (Present.get_info thy) |
50 Some thy => |
51 in if name = "" then [] else [name] end |
51 let val name = #name (Present.get_info thy) |
52 | None => []) |
52 in if name = "" then [] else [name] end |
53 | _ => ["global"]); |
53 | None => []) |
54 in |
54 | _ => ["global"]); |
55 (Symtab.update ((name, |
55 in |
56 {name = Sign.base_name name, ID = name, |
56 (Symtab.update ((name, |
57 dir = space_implode "/" (session @ prefx), |
57 {name = Sign.base_name name, ID = name, |
58 unfold = false, path = "", parents = parents'}), gra'), name ins parents) |
58 dir = space_implode "/" (session @ prefx), |
59 end |
59 unfold = false, path = "", parents = parents'}), gra'), |
60 else (gra, name ins parents) |
60 name ins parents) |
61 else |
61 end |
62 foldl make_deps_graph ((gra, parents), ders) |
62 else (gra, name ins parents) |
63 end; |
63 else |
|
64 make_deps_graph ((gra, parents), prf') |
|
65 end; |
64 |
66 |
65 fun thm_deps thms = |
67 fun thm_deps thms = |
66 let |
68 let |
67 val _ = writeln "Generating graph ..."; |
69 val _ = writeln "Generating graph ..."; |
68 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |
70 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |