tuned signature -- prefer self-contained user-space tool;
authorwenzelm
Thu Aug 14 10:48:40 2014 +0200 (2014-08-14)
changeset 579345e500c0e7eca
parent 57931 4e2cbff02f23
child 57935 c578f3a37a67
tuned signature -- prefer self-contained user-space tool;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Tools/thm_deps.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 13 22:29:43 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 10:48:40 2014 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4    val thy_deps: Toplevel.transition -> Toplevel.transition
     1.5    val locale_deps: Toplevel.transition -> Toplevel.transition
     1.6    val class_deps: Toplevel.transition -> Toplevel.transition
     1.7 -  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     1.8 -  val unused_thms: (string list * string list option) option ->
     1.9 -    Toplevel.transition -> Toplevel.transition
    1.10    val print_stmts: string list * (Facts.ref * Attrib.src list) list
    1.11      -> Toplevel.transition -> Toplevel.transition
    1.12    val print_thms: string list * (Facts.ref * Attrib.src list) list
    1.13 @@ -314,28 +311,6 @@
    1.14        |> sort (int_ord o pairself #1) |> map #2;
    1.15    in Graph_Display.display_graph gr end);
    1.16  
    1.17 -fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.18 -  Thm_Deps.thm_deps (Toplevel.theory_of state)
    1.19 -    (Attrib.eval_thms (Toplevel.context_of state) args));
    1.20 -
    1.21 -
    1.22 -(* find unused theorems *)
    1.23 -
    1.24 -fun unused_thms opt_range = Toplevel.keep (fn state =>
    1.25 -  let
    1.26 -    val thy = Toplevel.theory_of state;
    1.27 -    val ctxt = Toplevel.context_of state;
    1.28 -    fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
    1.29 -    val get_theory = Context.get_theory thy;
    1.30 -  in
    1.31 -    Thm_Deps.unused_thms
    1.32 -      (case opt_range of
    1.33 -        NONE => (Theory.parents_of thy, [thy])
    1.34 -      | SOME (xs, NONE) => (map get_theory xs, [thy])
    1.35 -      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
    1.36 -    |> map pretty_thm |> Pretty.writeln_chunks
    1.37 -  end);
    1.38 -
    1.39  
    1.40  (* print theorems, terms, types etc. *)
    1.41  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 13 22:29:43 2014 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 10:48:40 2014 +0200
     2.3 @@ -894,10 +894,6 @@
     2.4      (Scan.succeed Isar_Cmd.class_deps);
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
     2.8 -    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
     2.9 -
    2.10 -val _ =
    2.11    Outer_Syntax.improper_command @{command_spec "print_binds"}
    2.12      "print term bindings of proof context -- Proof General legacy"
    2.13      (Scan.succeed (Toplevel.unknown_context o
    2.14 @@ -956,11 +952,6 @@
    2.15      (Scan.succeed (Toplevel.unknown_theory o
    2.16        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
    2.17  
    2.18 -val _ =
    2.19 -  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
    2.20 -    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
    2.21 -       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
    2.22 -
    2.23  
    2.24  
    2.25  (** system commands (for interactive mode only) **)
     3.1 --- a/src/Pure/Pure.thy	Wed Aug 13 22:29:43 2014 +0200
     3.2 +++ b/src/Pure/Pure.thy	Thu Aug 14 10:48:40 2014 +0200
     3.3 @@ -112,6 +112,7 @@
     3.4  ML_file "Isar/calculation.ML"
     3.5  ML_file "Tools/rail.ML"
     3.6  ML_file "Tools/rule_insts.ML";
     3.7 +ML_file "Tools/thm_deps.ML";
     3.8  ML_file "Tools/find_theorems.ML"
     3.9  ML_file "Tools/find_consts.ML"
    3.10  ML_file "Tools/proof_general_pure.ML"
     4.1 --- a/src/Pure/ROOT	Wed Aug 13 22:29:43 2014 +0200
     4.2 +++ b/src/Pure/ROOT	Thu Aug 14 10:48:40 2014 +0200
     4.3 @@ -202,7 +202,6 @@
     4.4      "Thy/latex.ML"
     4.5      "Thy/present.ML"
     4.6      "Thy/term_style.ML"
     4.7 -    "Thy/thm_deps.ML"
     4.8      "Thy/thy_header.ML"
     4.9      "Thy/thy_info.ML"
    4.10      "Thy/thy_output.ML"
     5.1 --- a/src/Pure/ROOT.ML	Wed Aug 13 22:29:43 2014 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Thu Aug 14 10:48:40 2014 +0200
     5.3 @@ -310,7 +310,6 @@
     5.4  use "PIDE/document.ML";
     5.5  
     5.6  (*theory and proof operations*)
     5.7 -use "Thy/thm_deps.ML";
     5.8  use "Isar/isar_cmd.ML";
     5.9  
    5.10  use "subgoal.ML";
     6.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Aug 13 22:29:43 2014 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,99 +0,0 @@
     6.4 -(*  Title:      Pure/Thy/thm_deps.ML
     6.5 -    Author:     Stefan Berghofer, TU Muenchen
     6.6 -
     6.7 -Visualize dependencies of theorems.
     6.8 -*)
     6.9 -
    6.10 -signature THM_DEPS =
    6.11 -sig
    6.12 -  val thm_deps: theory -> thm list -> unit
    6.13 -  val unused_thms: theory list * theory list -> (string * thm) list
    6.14 -end;
    6.15 -
    6.16 -structure Thm_Deps: THM_DEPS =
    6.17 -struct
    6.18 -
    6.19 -(* thm_deps *)
    6.20 -
    6.21 -fun thm_deps thy thms =
    6.22 -  let
    6.23 -    fun add_dep ("", _, _) = I
    6.24 -      | add_dep (name, _, PBody {thms = thms', ...}) =
    6.25 -          let
    6.26 -            val prefix = #1 (split_last (Long_Name.explode name));
    6.27 -            val session =
    6.28 -              (case prefix of
    6.29 -                a :: _ =>
    6.30 -                  (case try (Context.get_theory thy) a of
    6.31 -                    SOME thy =>
    6.32 -                      (case Present.session_name thy of
    6.33 -                        "" => []
    6.34 -                      | session => [session])
    6.35 -                  | NONE => [])
    6.36 -               | _ => ["global"]);
    6.37 -            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
    6.38 -            val entry =
    6.39 -              {name = Long_Name.base_name name,
    6.40 -               ID = name,
    6.41 -               dir = space_implode "/" (session @ prefix),
    6.42 -               unfold = false,
    6.43 -               path = "",
    6.44 -               parents = parents,
    6.45 -               content = []};
    6.46 -          in cons entry end;
    6.47 -    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    6.48 -  in Graph_Display.display_graph (sort_wrt #ID deps) end;
    6.49 -
    6.50 -
    6.51 -(* unused_thms *)
    6.52 -
    6.53 -fun unused_thms (base_thys, thys) =
    6.54 -  let
    6.55 -    fun add_fact space (name, ths) =
    6.56 -      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
    6.57 -      else
    6.58 -        let val {concealed, group, ...} = Name_Space.the_entry space name in
    6.59 -          fold_rev (fn th =>
    6.60 -            (case Thm.derivation_name th of
    6.61 -              "" => I
    6.62 -            | a => cons (a, (th, concealed, group)))) ths
    6.63 -        end;
    6.64 -    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
    6.65 -
    6.66 -    val new_thms =
    6.67 -      fold (add_facts o Global_Theory.facts_of) thys []
    6.68 -      |> sort_distinct (string_ord o pairself #1);
    6.69 -
    6.70 -    val used =
    6.71 -      Proofterm.fold_body_thms
    6.72 -        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    6.73 -        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
    6.74 -        Symtab.empty;
    6.75 -
    6.76 -    fun is_unused a = not (Symtab.defined used a);
    6.77 -
    6.78 -    (* groups containing at least one used theorem *)
    6.79 -    val used_groups = fold (fn (a, (_, _, group)) =>
    6.80 -      if is_unused a then I
    6.81 -      else
    6.82 -        (case group of
    6.83 -          NONE => I
    6.84 -        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
    6.85 -
    6.86 -    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
    6.87 -      if not concealed andalso
    6.88 -        (* FIXME replace by robust treatment of thm groups *)
    6.89 -        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
    6.90 -        is_unused a
    6.91 -      then
    6.92 -        (case group of
    6.93 -           NONE => ((a, th) :: thms, seen_groups)
    6.94 -         | SOME grp =>
    6.95 -             if Inttab.defined used_groups grp orelse
    6.96 -               Inttab.defined seen_groups grp then q
    6.97 -             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
    6.98 -      else q) new_thms ([], Inttab.empty);
    6.99 -  in rev thms' end;
   6.100 -
   6.101 -end;
   6.102 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Aug 14 10:48:40 2014 +0200
     7.3 @@ -0,0 +1,124 @@
     7.4 +(*  Title:      Pure/Tools/thm_deps.ML
     7.5 +    Author:     Stefan Berghofer, TU Muenchen
     7.6 +
     7.7 +Visualize dependencies of theorems.
     7.8 +*)
     7.9 +
    7.10 +signature THM_DEPS =
    7.11 +sig
    7.12 +  val thm_deps: theory -> thm list -> unit
    7.13 +  val unused_thms: theory list * theory list -> (string * thm) list
    7.14 +end;
    7.15 +
    7.16 +structure Thm_Deps: THM_DEPS =
    7.17 +struct
    7.18 +
    7.19 +(* thm_deps *)
    7.20 +
    7.21 +fun thm_deps thy thms =
    7.22 +  let
    7.23 +    fun add_dep ("", _, _) = I
    7.24 +      | add_dep (name, _, PBody {thms = thms', ...}) =
    7.25 +          let
    7.26 +            val prefix = #1 (split_last (Long_Name.explode name));
    7.27 +            val session =
    7.28 +              (case prefix of
    7.29 +                a :: _ =>
    7.30 +                  (case try (Context.get_theory thy) a of
    7.31 +                    SOME thy =>
    7.32 +                      (case Present.session_name thy of
    7.33 +                        "" => []
    7.34 +                      | session => [session])
    7.35 +                  | NONE => [])
    7.36 +               | _ => ["global"]);
    7.37 +            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
    7.38 +            val entry =
    7.39 +              {name = Long_Name.base_name name,
    7.40 +               ID = name,
    7.41 +               dir = space_implode "/" (session @ prefix),
    7.42 +               unfold = false,
    7.43 +               path = "",
    7.44 +               parents = parents,
    7.45 +               content = []};
    7.46 +          in cons entry end;
    7.47 +    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    7.48 +  in Graph_Display.display_graph (sort_wrt #ID deps) end;
    7.49 +
    7.50 +val _ =
    7.51 +  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
    7.52 +    (Parse_Spec.xthms1 >> (fn args =>
    7.53 +      Toplevel.unknown_theory o Toplevel.keep (fn state =>
    7.54 +        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
    7.55 +
    7.56 +
    7.57 +(* unused_thms *)
    7.58 +
    7.59 +fun unused_thms (base_thys, thys) =
    7.60 +  let
    7.61 +    fun add_fact space (name, ths) =
    7.62 +      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
    7.63 +      else
    7.64 +        let val {concealed, group, ...} = Name_Space.the_entry space name in
    7.65 +          fold_rev (fn th =>
    7.66 +            (case Thm.derivation_name th of
    7.67 +              "" => I
    7.68 +            | a => cons (a, (th, concealed, group)))) ths
    7.69 +        end;
    7.70 +    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
    7.71 +
    7.72 +    val new_thms =
    7.73 +      fold (add_facts o Global_Theory.facts_of) thys []
    7.74 +      |> sort_distinct (string_ord o pairself #1);
    7.75 +
    7.76 +    val used =
    7.77 +      Proofterm.fold_body_thms
    7.78 +        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    7.79 +        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
    7.80 +        Symtab.empty;
    7.81 +
    7.82 +    fun is_unused a = not (Symtab.defined used a);
    7.83 +
    7.84 +    (*groups containing at least one used theorem*)
    7.85 +    val used_groups = fold (fn (a, (_, _, group)) =>
    7.86 +      if is_unused a then I
    7.87 +      else
    7.88 +        (case group of
    7.89 +          NONE => I
    7.90 +        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
    7.91 +
    7.92 +    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
    7.93 +      if not concealed andalso
    7.94 +        (* FIXME replace by robust treatment of thm groups *)
    7.95 +        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
    7.96 +        is_unused a
    7.97 +      then
    7.98 +        (case group of
    7.99 +           NONE => ((a, th) :: thms, seen_groups)
   7.100 +         | SOME grp =>
   7.101 +             if Inttab.defined used_groups grp orelse
   7.102 +               Inttab.defined seen_groups grp then q
   7.103 +             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
   7.104 +      else q) new_thms ([], Inttab.empty);
   7.105 +  in rev thms' end;
   7.106 +
   7.107 +val _ =
   7.108 +  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
   7.109 +    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   7.110 +       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
   7.111 +        Toplevel.keep (fn state =>
   7.112 +          let
   7.113 +            val thy = Toplevel.theory_of state;
   7.114 +            val ctxt = Toplevel.context_of state;
   7.115 +            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
   7.116 +            val get_theory = Context.get_theory thy;
   7.117 +          in
   7.118 +            unused_thms
   7.119 +              (case opt_range of
   7.120 +                NONE => (Theory.parents_of thy, [thy])
   7.121 +              | SOME (xs, NONE) => (map get_theory xs, [thy])
   7.122 +              | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
   7.123 +            |> map pretty_thm |> Pretty.writeln_chunks
   7.124 +          end)));
   7.125 +
   7.126 +end;
   7.127 +