--- a/src/Pure/ROOT.ML Sat Aug 17 11:02:09 2019 +0200
+++ b/src/Pure/ROOT.ML Sat Aug 17 11:13:16 2019 +0200
@@ -309,6 +309,7 @@
ML_file "PIDE/resources.ML";
ML_file "Thy/present.ML";
ML_file "Thy/thy_info.ML";
+ML_file "Thy/thm_deps.ML";
ML_file "Thy/export_theory.ML";
ML_file "Thy/sessions.ML";
ML_file "PIDE/session.ML";
@@ -341,7 +342,6 @@
ML_file "Tools/print_operation.ML";
ML_file "Tools/rail.ML";
ML_file "Tools/rule_insts.ML";
-ML_file "Tools/thm_deps.ML";
ML_file "Tools/thy_deps.ML";
ML_file "Tools/class_deps.ML";
ML_file "Tools/find_theorems.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thm_deps.ML Sat Aug 17 11:13:16 2019 +0200
@@ -0,0 +1,105 @@
+(* Title: Pure/Thy/thm_deps.ML
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Makarius
+
+Dependencies of theorems wrt. internal derivation.
+*)
+
+signature THM_DEPS =
+sig
+ val thm_deps: theory -> thm list -> unit
+ val unused_thms: theory list * theory list -> (string * thm) list
+end;
+
+structure Thm_Deps: THM_DEPS =
+struct
+
+(* thm_deps *)
+
+fun thm_deps thy thms =
+ let
+ fun make_node name directory =
+ Graph_Display.session_node
+ {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
+ fun add_dep {name = "", ...} = I
+ | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
+ let
+ val prefix = #1 (split_last (Long_Name.explode name));
+ val session =
+ (case prefix of
+ a :: _ =>
+ (case try (Context.get_theory {long = false} thy) a of
+ SOME thy =>
+ (case Present.theory_qualifier thy of
+ "" => []
+ | session => [session])
+ | NONE => [])
+ | _ => ["global"]);
+ val node = make_node name (space_implode "/" (session @ prefix));
+ val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
+ in Symtab.update (name, (node, deps)) end;
+ val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
+ val entries1 =
+ Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
+ if Symtab.defined tab d then tab
+ else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
+ in
+ Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
+ |> Graph_Display.display_graph_old
+ end;
+
+
+(* unused_thms *)
+
+fun unused_thms (base_thys, thys) =
+ let
+ fun add_fact transfer space (name, ths) =
+ if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
+ else
+ let val {concealed, group, ...} = Name_Space.the_entry space name in
+ fold_rev (fn th =>
+ (case Thm.derivation_name th of
+ "" => I
+ | a => cons (a, (transfer th, concealed, group)))) ths
+ end;
+ fun add_facts thy =
+ let
+ val transfer = Global_Theory.transfer_theories thy;
+ val facts = Global_Theory.facts_of thy;
+ in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;
+
+ val new_thms =
+ fold add_facts thys []
+ |> sort_distinct (string_ord o apply2 #1);
+
+ val used =
+ Proofterm.fold_body_thms
+ (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
+ (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+ Symtab.empty;
+
+ fun is_unused a = not (Symtab.defined used a);
+
+ (*groups containing at least one used theorem*)
+ val used_groups = fold (fn (a, (_, _, group)) =>
+ if is_unused a then I
+ else
+ (case group of
+ NONE => I
+ | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
+
+ val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
+ if not concealed andalso
+ (* FIXME replace by robust treatment of thm groups *)
+ Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
+ then
+ (case group of
+ NONE => ((a, th) :: thms, seen_groups)
+ | SOME grp =>
+ if Inttab.defined used_groups grp orelse
+ Inttab.defined seen_groups grp then q
+ else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
+ else q) new_thms ([], Inttab.empty);
+ in rev thms' end;
+
+end;
--- a/src/Pure/Tools/thm_deps.ML Sat Aug 17 11:02:09 2019 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-(* Title: Pure/Tools/thm_deps.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Visualize dependencies of theorems.
-*)
-
-signature THM_DEPS =
-sig
- val thm_deps: theory -> thm list -> unit
- val unused_thms: theory list * theory list -> (string * thm) list
-end;
-
-structure Thm_Deps: THM_DEPS =
-struct
-
-(* thm_deps *)
-
-fun thm_deps thy thms =
- let
- fun make_node name directory =
- Graph_Display.session_node
- {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
- fun add_dep {name = "", ...} = I
- | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
- let
- val prefix = #1 (split_last (Long_Name.explode name));
- val session =
- (case prefix of
- a :: _ =>
- (case try (Context.get_theory {long = false} thy) a of
- SOME thy =>
- (case Present.theory_qualifier thy of
- "" => []
- | session => [session])
- | NONE => [])
- | _ => ["global"]);
- val node = make_node name (space_implode "/" (session @ prefix));
- val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
- in Symtab.update (name, (node, deps)) end;
- val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
- val entries1 =
- Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
- if Symtab.defined tab d then tab
- else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
- in
- Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
- |> Graph_Display.display_graph_old
- end;
-
-
-(* unused_thms *)
-
-fun unused_thms (base_thys, thys) =
- let
- fun add_fact transfer space (name, ths) =
- if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
- else
- let val {concealed, group, ...} = Name_Space.the_entry space name in
- fold_rev (fn th =>
- (case Thm.derivation_name th of
- "" => I
- | a => cons (a, (transfer th, concealed, group)))) ths
- end;
- fun add_facts thy =
- let
- val transfer = Global_Theory.transfer_theories thy;
- val facts = Global_Theory.facts_of thy;
- in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;
-
- val new_thms =
- fold add_facts thys []
- |> sort_distinct (string_ord o apply2 #1);
-
- val used =
- Proofterm.fold_body_thms
- (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
- (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
- Symtab.empty;
-
- fun is_unused a = not (Symtab.defined used a);
-
- (*groups containing at least one used theorem*)
- val used_groups = fold (fn (a, (_, _, group)) =>
- if is_unused a then I
- else
- (case group of
- NONE => I
- | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
-
- val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
- if not concealed andalso
- (* FIXME replace by robust treatment of thm groups *)
- Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
- then
- (case group of
- NONE => ((a, th) :: thms, seen_groups)
- | SOME grp =>
- if Inttab.defined used_groups grp orelse
- Inttab.defined seen_groups grp then q
- else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
- else q) new_thms ([], Inttab.empty);
- in rev thms' end;
-
-end;