24 |
24 |
25 fun enable () = if ! proofs = 0 then proofs := 1 else (); |
25 fun enable () = if ! proofs = 0 then proofs := 1 else (); |
26 fun disable () = proofs := 0; |
26 fun disable () = proofs := 0; |
27 |
27 |
28 fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) |
28 fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) |
29 | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof []) |
29 | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], [])) |
30 | dest_thm_axm _ = (("", []), MinProof []); |
30 | dest_thm_axm _ = (("", []), MinProof ([], [], [])); |
31 |
31 |
32 fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf) |
32 fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf |
33 | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf) |
33 | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf |
34 | make_deps_graph (p, prf1 %% prf2) = |
34 | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2 |
35 make_deps_graph (make_deps_graph (p, prf1), prf2) |
35 | make_deps_graph (prf % _) = make_deps_graph prf |
36 | make_deps_graph (p, prf % _) = make_deps_graph (p, prf) |
36 | make_deps_graph (MinProof (thms, axms, _)) = |
37 | make_deps_graph (p, MinProof prfs) = Library.foldl make_deps_graph (p, prfs) |
37 fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> |
38 | make_deps_graph (p as (gra, parents), prf) = |
38 fold (make_deps_graph o Proofterm.proof_of_min_axm) axms |
|
39 | make_deps_graph prf = (fn p as (gra, parents) => |
39 let val ((name, tags), prf') = dest_thm_axm prf |
40 let val ((name, tags), prf') = dest_thm_axm prf |
40 in |
41 in |
41 if name <> "" andalso not (Drule.has_internal tags) then |
42 if name <> "" andalso not (Drule.has_internal tags) then |
42 if not (Symtab.defined gra name) then |
43 if not (Symtab.defined gra name) then |
43 let |
44 let |
44 val (gra', parents') = make_deps_graph ((gra, []), prf'); |
45 val (gra', parents') = make_deps_graph prf' (gra, []); |
45 val prefx = #1 (Library.split_last (NameSpace.unpack name)); |
46 val prefx = #1 (Library.split_last (NameSpace.unpack name)); |
46 val session = |
47 val session = |
47 (case prefx of |
48 (case prefx of |
48 (x :: _) => |
49 (x :: _) => |
49 (case ThyInfo.lookup_theory x of |
50 (case ThyInfo.lookup_theory x of |
60 unfold = false, path = "", parents = parents'}), gra'), |
61 unfold = false, path = "", parents = parents'}), gra'), |
61 name ins parents) |
62 name ins parents) |
62 end |
63 end |
63 else (gra, name ins parents) |
64 else (gra, name ins parents) |
64 else |
65 else |
65 make_deps_graph ((gra, parents), prf') |
66 make_deps_graph prf' (gra, parents) |
66 end; |
67 end); |
67 |
68 |
68 fun thm_deps thms = |
69 fun thm_deps thms = |
69 let |
70 let |
70 val _ = writeln "Generating graph ..."; |
71 val _ = writeln "Generating graph ..."; |
71 val gra = map snd (Symtab.dest (fst (Library.foldl make_deps_graph ((Symtab.empty, []), |
72 val gra = map snd (Symtab.dest (fst |
72 map Thm.proof_of thms)))); |
73 (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))); |
73 val path = File.tmp_path (Path.unpack "theorems.graph"); |
74 val path = File.tmp_path (Path.unpack "theorems.graph"); |
74 val _ = Present.write_graph gra path; |
75 val _ = Present.write_graph gra path; |
75 val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &"); |
76 val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &"); |
76 in () end; |
77 in () end; |
77 |
78 |