author | wenzelm |
Fri, 27 Jan 2006 19:03:02 +0100 | |
changeset 18799 | f137c5e971f5 |
parent 17412 | e26cb20ef0cc |
child 20578 | f26c8408a675 |
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 |
|
7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
8 |
signature BASIC_THM_DEPS = |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
9 |
sig |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
10 |
val thm_deps : thm list -> unit |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
11 |
end; |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
12 |
|
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
13 |
signature THM_DEPS = |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
14 |
sig |
7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
15 |
include BASIC_THM_DEPS |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
16 |
val enable : unit -> unit |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
17 |
val disable : unit -> unit |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
18 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
19 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
20 |
structure ThmDeps : THM_DEPS = |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
21 |
struct |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
22 |
|
11530 | 23 |
open Proofterm; |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
24 |
|
11543
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11530
diff
changeset
|
25 |
fun enable () = if ! proofs = 0 then proofs := 1 else (); |
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11530
diff
changeset
|
26 |
fun disable () = proofs := 0; |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
27 |
|
11530 | 28 |
fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) |
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
29 |
| dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], [])) |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
30 |
| dest_thm_axm _ = (("", []), MinProof ([], [], [])); |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
31 |
|
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
32 |
fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
33 |
| make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
34 |
| make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2 |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
35 |
| make_deps_graph (prf % _) = make_deps_graph prf |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
36 |
| make_deps_graph (MinProof (thms, axms, _)) = |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
37 |
fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
38 |
fold (make_deps_graph o Proofterm.proof_of_min_axm) axms |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
39 |
| make_deps_graph prf = (fn p as (gra, parents) => |
11530 | 40 |
let val ((name, tags), prf') = dest_thm_axm prf |
41 |
in |
|
18799 | 42 |
if name <> "" andalso not (PureThy.has_internal tags) then |
16894 | 43 |
if not (Symtab.defined gra name) then |
11530 | 44 |
let |
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
45 |
val (gra', parents') = make_deps_graph prf' (gra, []); |
11530 | 46 |
val prefx = #1 (Library.split_last (NameSpace.unpack name)); |
47 |
val session = |
|
48 |
(case prefx of |
|
49 |
(x :: _) => |
|
50 |
(case ThyInfo.lookup_theory x of |
|
15531 | 51 |
SOME thy => |
11530 | 52 |
let val name = #name (Present.get_info thy) |
16268 | 53 |
in if name = "" then [] else [name] end |
15531 | 54 |
| NONE => []) |
11530 | 55 |
| _ => ["global"]); |
56 |
in |
|
12239
ee360f910ec8
Now handles different theorems with same name more gracefully.
berghofe
parents:
11819
diff
changeset
|
57 |
if name mem parents' then (gra', parents union parents') |
17412 | 58 |
else (Symtab.update (name, |
11530 | 59 |
{name = Sign.base_name name, ID = name, |
60 |
dir = space_implode "/" (session @ prefx), |
|
17224 | 61 |
unfold = false, path = "", parents = parents'}) gra', |
11530 | 62 |
name ins parents) |
63 |
end |
|
64 |
else (gra, name ins parents) |
|
65 |
else |
|
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
66 |
make_deps_graph prf' (gra, parents) |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
67 |
end); |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
68 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
69 |
fun thm_deps thms = |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
70 |
let |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
71 |
val _ = writeln "Generating graph ..."; |
17020
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
72 |
val gra = map snd (Symtab.dest (fst |
f3014afac46f
Adapted to new argument format of MinProof constructor.
berghofe
parents:
16894
diff
changeset
|
73 |
(fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))); |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
74 |
val path = File.tmp_path (Path.unpack "theorems.graph"); |
9450 | 75 |
val _ = Present.write_graph gra path; |
16268 | 76 |
val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &"); |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
77 |
in () end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
78 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
79 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
80 |
|
7785
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
81 |
structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps; |
c06825c396e8
Added functions for enabling and disabling derivations.
berghofe
parents:
7783
diff
changeset
|
82 |
open BasicThmDeps; |