author | wenzelm |
Sat, 15 Nov 2008 21:31:36 +0100 | |
changeset 28810 | e915ab11fe52 |
parent 27865 | 27a8ad9612a3 |
child 28814 | 463c9e9111ae |
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 |
|
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
8 |
signature THM_DEPS = |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
9 |
sig |
26697 | 10 |
val thm_deps: thm list -> unit |
11 |
val unused_thms: theory list * theory list -> (string * thm) list |
|
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
12 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
13 |
|
26697 | 14 |
structure ThmDeps: THM_DEPS = |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
15 |
struct |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
16 |
|
26697 | 17 |
(* thm_deps *) |
18 |
||
28810 | 19 |
fun add_dep ((name, _, _), PBody {thms = thms', ...}) = |
20 |
name <> "" ? |
|
21 |
Graph.new_node (name, ()) #> |
|
22 |
fold (fn (_, ((name', _, _), _)) => name <> "" ? Graph.add_edge (name', name)) thms'; |
|
26697 | 23 |
|
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
24 |
fun thm_deps thms = |
28810 | 25 |
let |
26 |
val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_of thms) Graph.empty; |
|
27 |
fun add_entry (name, (_, (preds, _))) = |
|
28 |
let |
|
29 |
val prefix = #1 (Library.split_last (NameSpace.explode name)); |
|
30 |
val session = |
|
31 |
(case prefix of |
|
32 |
a :: _ => |
|
33 |
(case ThyInfo.lookup_theory a of |
|
34 |
SOME thy => |
|
35 |
(case Present.session_name thy of |
|
36 |
"" => [] |
|
37 |
| session => [session]) |
|
38 |
| NONE => []) |
|
39 |
| _ => ["global"]); |
|
40 |
val entry = |
|
41 |
{name = Sign.base_name name, |
|
42 |
ID = name, |
|
43 |
dir = space_implode "/" (session @ prefix), |
|
44 |
unfold = false, |
|
45 |
path = "", |
|
46 |
parents = preds}; |
|
47 |
in cons entry end; |
|
48 |
in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end; |
|
26697 | 49 |
|
50 |
||
51 |
(* unused_thms *) |
|
52 |
||
53 |
fun unused_thms (base_thys, thys) = |
|
26185 | 54 |
let |
26697 | 55 |
fun add_fact (name, ths) = |
56 |
if exists (fn thy => PureThy.defined_fact thy name) base_thys then I |
|
57 |
else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths; |
|
26699 | 58 |
val thms = |
59 |
fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] |
|
60 |
|> sort_distinct (string_ord o pairself #1); |
|
28810 | 61 |
|
62 |
val tab = Proofterm.fold_body_thms |
|
63 |
(fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
|
26697 | 64 |
(map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty; |
28810 | 65 |
fun is_unused (name, th) = |
66 |
not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
|
67 |
||
26185 | 68 |
(* groups containing at least one used theorem *) |
69 |
val grps = fold (fn p as (_, thm) => if is_unused p then I else |
|
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset
|
70 |
case Thm.get_group thm of |
26185 | 71 |
NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; |
72 |
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => |
|
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset
|
73 |
if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) |
26185 | 74 |
andalso is_unused p |
75 |
then |
|
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26699
diff
changeset
|
76 |
(case Thm.get_group thm of |
26185 | 77 |
NONE => (p :: thms, grps') |
78 |
| SOME grp => |
|
79 |
(* do not output theorem if another theorem in group has been used *) |
|
26697 | 80 |
if Symtab.defined grps grp then q |
26185 | 81 |
(* output at most one unused theorem per group *) |
26697 | 82 |
else if Symtab.defined grps' grp then q |
26185 | 83 |
else (p :: thms, Symtab.update (grp, ()) grps')) |
84 |
else q) thms ([], Symtab.empty) |
|
85 |
in rev thms' end; |
|
86 |
||
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
87 |
end; |
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
88 |