author | wenzelm |
Thu, 31 Oct 2019 14:29:29 +0100 | |
changeset 70974 | 3ee90f831805 |
parent 70895 | 2a318149b01b |
child 70975 | 19818f99b4ae |
permissions | -rw-r--r-- |
70893 | 1 |
(* Title: Pure/thm_deps.ML |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer, TU Muenchen |
70556 | 3 |
Author: Makarius |
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
4 |
|
70556 | 5 |
Dependencies of theorems wrt. internal derivation. |
7765
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 |
70557 | 10 |
val all_oracles: thm list -> Proofterm.oracle list |
70566
fb3d06d7dd05
more thorough check, using full dependency graph of finished proofs;
wenzelm
parents:
70560
diff
changeset
|
11 |
val has_skip_proof: thm list -> bool |
70560 | 12 |
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
70605 | 13 |
val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list |
14 |
val pretty_thm_deps: theory -> thm list -> Pretty.T |
|
70974 | 15 |
val proof_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} -> |
16 |
thm list -> Proofterm.thm_id list |
|
70570 | 17 |
val unused_thms_cmd: theory list * theory list -> (string * thm) list |
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 |
|
33391 | 20 |
structure Thm_Deps: THM_DEPS = |
7765
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 |
|
70557 | 23 |
(* oracles *) |
24 |
||
25 |
fun all_oracles thms = |
|
70588 | 26 |
let |
27 |
fun collect (PBody {oracles, thms, ...}) = |
|
28 |
(if null oracles then I else apfst (cons oracles)) #> |
|
29 |
(tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) => |
|
30 |
if Inttab.defined seen i then (res, seen) |
|
31 |
else |
|
32 |
let val body = Future.join (Proofterm.thm_node_body thm_node) |
|
33 |
in collect body (res, Inttab.update (i, ()) seen) end)); |
|
34 |
val bodies = map Thm.proof_body_of thms; |
|
35 |
in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; |
|
70557 | 36 |
|
70566
fb3d06d7dd05
more thorough check, using full dependency graph of finished proofs;
wenzelm
parents:
70560
diff
changeset
|
37 |
fun has_skip_proof thms = |
fb3d06d7dd05
more thorough check, using full dependency graph of finished proofs;
wenzelm
parents:
70560
diff
changeset
|
38 |
all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>); |
fb3d06d7dd05
more thorough check, using full dependency graph of finished proofs;
wenzelm
parents:
70560
diff
changeset
|
39 |
|
70560 | 40 |
fun pretty_thm_oracles ctxt thms = |
41 |
let |
|
70567 | 42 |
val thy = Proof_Context.theory_of ctxt; |
70560 | 43 |
fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
44 |
| prt_oracle (name, SOME prop) = |
|
70567 | 45 |
[Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, |
46 |
Syntax.pretty_term_global thy prop]; |
|
70560 | 47 |
in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; |
48 |
||
70557 | 49 |
|
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
50 |
(* thm_deps *) |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
51 |
|
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
52 |
fun thm_deps thy = |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
53 |
let |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
54 |
val lookup = Global_Theory.lookup_thm_id thy; |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
55 |
fun deps (i, thm_node) res = |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
56 |
if Inttab.defined res i then res |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
57 |
else |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
58 |
let val thm_id = Proofterm.thm_id (i, thm_node) in |
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
59 |
(case lookup thm_id of |
70602
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
60 |
SOME thm_name => |
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
61 |
Inttab.update (i, SOME (thm_id, thm_name)) res |
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
62 |
| NONE => |
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
63 |
Inttab.update (i, NONE) res |
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
64 |
|> fold deps (Proofterm.thm_node_thms thm_node)) |
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
65 |
end; |
70596 | 66 |
in |
70605 | 67 |
fn thms => |
68 |
(fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, []) |
|
70602
b85a12c2e2bf
proper graph traversal: avoid multiple visit of unnamed nodes;
wenzelm
parents:
70596
diff
changeset
|
69 |
|-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) |
70596 | 70 |
end; |
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70588
diff
changeset
|
71 |
|
70605 | 72 |
fun pretty_thm_deps thy thms = |
28810 | 73 |
let |
70605 | 74 |
val ctxt = Proof_Context.init_global thy; |
75 |
val items = |
|
76 |
map #2 (thm_deps thy thms) |
|
77 |
|> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) |
|
78 |
|> sort_by (#2 o #1) |
|
79 |
|> map (fn ((marks, xname), i) => |
|
80 |
Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
|
81 |
in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
|
26697 | 82 |
|
83 |
||
70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
84 |
(* proof boxes: undefined PThm nodes *) |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
85 |
|
70974 | 86 |
fun proof_boxes {included, excluded} thms = |
70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
87 |
let |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
88 |
fun boxes (i, thm_node) res = |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
89 |
let val thm_id = Proofterm.thm_id (i, thm_node) in |
70974 | 90 |
if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id)) |
91 |
then res |
|
70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
92 |
else |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
93 |
Inttab.update (i, thm_id) res |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
94 |
|> fold boxes (Proofterm.thm_node_thms thm_node) |
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
95 |
end; |
70974 | 96 |
in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end; |
70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
97 |
|
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70893
diff
changeset
|
98 |
|
70570 | 99 |
(* unused_thms_cmd *) |
26697 | 100 |
|
70570 | 101 |
fun unused_thms_cmd (base_thys, thys) = |
26185 | 102 |
let |
61507 | 103 |
fun add_fact transfer space (name, ths) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37870
diff
changeset
|
104 |
if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I |
33170 | 105 |
else |
106 |
let val {concealed, group, ...} = Name_Space.the_entry space name in |
|
107 |
fold_rev (fn th => |
|
36744
6e1f3d609a68
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents:
33769
diff
changeset
|
108 |
(case Thm.derivation_name th of |
33170 | 109 |
"" => I |
61507 | 110 |
| a => cons (a, (transfer th, concealed, group)))) ths |
33170 | 111 |
end; |
61507 | 112 |
fun add_facts thy = |
113 |
let |
|
114 |
val transfer = Global_Theory.transfer_theories thy; |
|
115 |
val facts = Global_Theory.facts_of thy; |
|
116 |
in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; |
|
33170 | 117 |
|
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
118 |
val new_thms = |
61507 | 119 |
fold add_facts thys [] |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
120 |
|> sort_distinct (string_ord o apply2 #1); |
28810 | 121 |
|
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
122 |
val used = |
32810
f3466a5645fa
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
wenzelm
parents:
32726
diff
changeset
|
123 |
Proofterm.fold_body_thms |
64572 | 124 |
(fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) |
70830 | 125 |
(map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
44331 | 126 |
Symtab.empty; |
33170 | 127 |
|
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
128 |
fun is_unused a = not (Symtab.defined used a); |
28810 | 129 |
|
57934
5e500c0e7eca
tuned signature -- prefer self-contained user-space tool;
wenzelm
parents:
49561
diff
changeset
|
130 |
(*groups containing at least one used theorem*) |
41565
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
131 |
val used_groups = fold (fn (a, (_, _, group)) => |
9718c32f9c4e
unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents:
41489
diff
changeset
|
132 |
if is_unused a then I |
33170 | 133 |
else |
134 |
(case group of |
|
135 |
NONE => I |
|
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
136 |
| SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
137 |
|
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
138 |
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
139 |
if not concealed andalso |
42473 | 140 |
(* FIXME replace by robust treatment of thm groups *) |
61336 | 141 |
Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
142 |
then |
33170 | 143 |
(case group of |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
144 |
NONE => ((a, th) :: thms, seen_groups) |
26185 | 145 |
| SOME grp => |
33769
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
146 |
if Inttab.defined used_groups grp orelse |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
147 |
Inttab.defined seen_groups grp then q |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
148 |
else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) |
6d8630fab26a
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents:
33642
diff
changeset
|
149 |
else q) new_thms ([], Inttab.empty); |
26185 | 150 |
in rev thms' end; |
151 |
||
7765
fa28bac7903c
New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff
changeset
|
152 |
end; |