--- a/src/Pure/Isar/isar_cmd.ML Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 14 10:48:40 2014 +0200
@@ -39,9 +39,6 @@
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
- val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
- val unused_thms: (string list * string list option) option ->
- Toplevel.transition -> Toplevel.transition
val print_stmts: string list * (Facts.ref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_thms: string list * (Facts.ref * Attrib.src list) list
@@ -314,28 +311,6 @@
|> sort (int_ord o pairself #1) |> map #2;
in Graph_Display.display_graph gr end);
-fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Toplevel.theory_of state)
- (Attrib.eval_thms (Toplevel.context_of state) args));
-
-
-(* find unused theorems *)
-
-fun unused_thms opt_range = Toplevel.keep (fn state =>
- let
- val thy = Toplevel.theory_of state;
- val ctxt = Toplevel.context_of state;
- fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
- val get_theory = Context.get_theory thy;
- in
- Thm_Deps.unused_thms
- (case opt_range of
- NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
- |> map pretty_thm |> Pretty.writeln_chunks
- end);
-
(* print theorems, terms, types etc. *)
--- a/src/Pure/Isar/isar_syn.ML Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Aug 14 10:48:40 2014 +0200
@@ -894,10 +894,6 @@
(Scan.succeed Isar_Cmd.class_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
- (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_binds"}
"print term bindings of proof context -- Proof General legacy"
(Scan.succeed (Toplevel.unknown_context o
@@ -956,11 +952,6 @@
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
-val _ =
- Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
- (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
- Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
-
(** system commands (for interactive mode only) **)
--- a/src/Pure/Pure.thy Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/Pure.thy Thu Aug 14 10:48:40 2014 +0200
@@ -112,6 +112,7 @@
ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
ML_file "Tools/rule_insts.ML";
+ML_file "Tools/thm_deps.ML";
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
ML_file "Tools/proof_general_pure.ML"
--- a/src/Pure/ROOT Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/ROOT Thu Aug 14 10:48:40 2014 +0200
@@ -202,7 +202,6 @@
"Thy/latex.ML"
"Thy/present.ML"
"Thy/term_style.ML"
- "Thy/thm_deps.ML"
"Thy/thy_header.ML"
"Thy/thy_info.ML"
"Thy/thy_output.ML"
--- a/src/Pure/ROOT.ML Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/ROOT.ML Thu Aug 14 10:48:40 2014 +0200
@@ -310,7 +310,6 @@
use "PIDE/document.ML";
(*theory and proof operations*)
-use "Thy/thm_deps.ML";
use "Isar/isar_cmd.ML";
use "subgoal.ML";
--- a/src/Pure/Thy/thm_deps.ML Wed Aug 13 22:29:43 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: Pure/Thy/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 add_dep ("", _, _) = I
- | add_dep (name, _, PBody {thms = thms', ...}) =
- let
- val prefix = #1 (split_last (Long_Name.explode name));
- val session =
- (case prefix of
- a :: _ =>
- (case try (Context.get_theory thy) a of
- SOME thy =>
- (case Present.session_name thy of
- "" => []
- | session => [session])
- | NONE => [])
- | _ => ["global"]);
- val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
- val entry =
- {name = Long_Name.base_name name,
- ID = name,
- dir = space_implode "/" (session @ prefix),
- unfold = false,
- path = "",
- parents = parents,
- content = []};
- in cons entry end;
- val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
- in Graph_Display.display_graph (sort_wrt #ID deps) end;
-
-
-(* unused_thms *)
-
-fun unused_thms (base_thys, thys) =
- let
- fun add_fact 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, (th, concealed, group)))) ths
- end;
- fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
-
- val new_thms =
- fold (add_facts o Global_Theory.facts_of) thys []
- |> sort_distinct (string_ord o pairself #1);
-
- val used =
- Proofterm.fold_body_thms
- (fn (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 *)
- member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) 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;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/thm_deps.ML Thu Aug 14 10:48:40 2014 +0200
@@ -0,0 +1,124 @@
+(* 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 add_dep ("", _, _) = I
+ | add_dep (name, _, PBody {thms = thms', ...}) =
+ let
+ val prefix = #1 (split_last (Long_Name.explode name));
+ val session =
+ (case prefix of
+ a :: _ =>
+ (case try (Context.get_theory thy) a of
+ SOME thy =>
+ (case Present.session_name thy of
+ "" => []
+ | session => [session])
+ | NONE => [])
+ | _ => ["global"]);
+ val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
+ val entry =
+ {name = Long_Name.base_name name,
+ ID = name,
+ dir = space_implode "/" (session @ prefix),
+ unfold = false,
+ path = "",
+ parents = parents,
+ content = []};
+ in cons entry end;
+ val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
+ in Graph_Display.display_graph (sort_wrt #ID deps) end;
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
+ (Parse_Spec.xthms1 >> (fn args =>
+ Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+
+
+(* unused_thms *)
+
+fun unused_thms (base_thys, thys) =
+ let
+ fun add_fact 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, (th, concealed, group)))) ths
+ end;
+ fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
+
+ val new_thms =
+ fold (add_facts o Global_Theory.facts_of) thys []
+ |> sort_distinct (string_ord o pairself #1);
+
+ val used =
+ Proofterm.fold_body_thms
+ (fn (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 *)
+ member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) 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;
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
+ (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
+ Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
+ Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
+ fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+ val get_theory = Context.get_theory thy;
+ in
+ unused_thms
+ (case opt_range of
+ NONE => (Theory.parents_of thy, [thy])
+ | SOME (xs, NONE) => (map get_theory xs, [thy])
+ | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
+ |> map pretty_thm |> Pretty.writeln_chunks
+ end)));
+
+end;
+