# HG changeset patch # User wenzelm # Date 1408006120 -7200 # Node ID 5e500c0e7ecae7da717465779dd8d0bd408b1609 # Parent 4e2cbff02f2359d7983510602b75438c43464d18 tuned signature -- prefer self-contained user-space tool; diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/Isar/isar_cmd.ML --- 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. *) diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/Isar/isar_syn.ML --- 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) **) diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/Pure.thy --- 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" diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/ROOT --- 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" diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/ROOT.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"; diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/Thy/thm_deps.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; - diff -r 4e2cbff02f23 -r 5e500c0e7eca src/Pure/Tools/thm_deps.ML --- /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; +