src/Pure/Thy/thm_deps.ML
author berghofe
Sat, 15 Jan 2011 12:47:52 +0100
changeset 41565 9718c32f9c4e
parent 41489 8e2b8649507d
child 42473 aca720fb3936
permissions -rw-r--r--
unused_thms no longer compares propositions, since this is no longer needed and did not work properly any longer after the addition of class constraints to propositions.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thm_deps.ML
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     3
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     4
Visualize dependencies of theorems.
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     5
*)
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
signature THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     8
sig
37870
dd9cfc512b7f thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents: 37216
diff changeset
     9
  val thm_deps: theory -> thm list -> unit
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    10
  val unused_thms: theory list * theory list -> (string * thm) list
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    11
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    12
33391
91b9da2a7b44 structure Thm_Deps;
wenzelm
parents: 33170
diff changeset
    13
structure Thm_Deps: THM_DEPS =
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    14
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    15
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    16
(* thm_deps *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    17
37870
dd9cfc512b7f thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents: 37216
diff changeset
    18
fun thm_deps thy thms =
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    19
  let
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    20
    fun add_dep ("", _, _) = I
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    21
      | add_dep (name, _, PBody {thms = thms', ...}) =
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    22
          let
41489
8e2b8649507d standardized split_last/last_elem towards List.last;
wenzelm
parents: 39557
diff changeset
    23
            val prefix = #1 (split_last (Long_Name.explode name));
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    24
            val session =
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    25
              (case prefix of
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    26
                a :: _ =>
37870
dd9cfc512b7f thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents: 37216
diff changeset
    27
                  (case try (Context.get_theory thy) a of
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    28
                    SOME thy =>
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    29
                      (case Present.session_name thy of
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    30
                        "" => []
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    31
                      | session => [session])
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    32
                  | NONE => [])
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    33
               | _ => ["global"]);
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    34
            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    35
            val entry =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
    36
              {name = Long_Name.base_name name,
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    37
               ID = name,
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    38
               dir = space_implode "/" (session @ prefix),
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    39
               unfold = false,
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    40
               path = "",
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    41
               parents = parents};
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    42
          in cons entry end;
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
    43
    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    44
  in Present.display_graph (sort_wrt #ID deps) end;
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    45
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    46
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    47
(* unused_thms *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    48
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    49
fun unused_thms (base_thys, thys) =
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    50
  let
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    51
    fun add_fact 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
    52
      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    53
      else
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    54
        let val {concealed, group, ...} = Name_Space.the_entry space name in
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    55
          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
    56
            (case Thm.derivation_name th of
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    57
              "" => I
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    58
            | a => cons (a, (th, concealed, group)))) ths
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    59
        end;
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    60
    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    61
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    62
    val new_thms =
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
    63
      fold (add_facts o Global_Theory.facts_of) thys []
26699
6c7e4d858bae unused_thms: sort_distinct;
wenzelm
parents: 26697
diff changeset
    64
      |> sort_distinct (string_ord o pairself #1);
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    65
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    66
    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
    67
      Proofterm.fold_body_thms
41565
9718c32f9c4e unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents: 41489
diff changeset
    68
        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    69
        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    70
41565
9718c32f9c4e unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents: 41489
diff changeset
    71
    fun is_unused a = not (Symtab.defined used a);
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    72
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    73
    (* 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
    74
    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
    75
      if is_unused a then I
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    76
      else
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    77
        (case group of
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    78
          NONE => I
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    79
        | 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
    80
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    81
    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
    82
      if not concealed andalso
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    83
        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.get_kind th) andalso
41565
9718c32f9c4e unused_thms no longer compares propositions, since this is no longer needed
berghofe
parents: 41489
diff changeset
    84
        is_unused a
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    85
      then
33170
dd6d8d1f70d2 maintain group via name space, not tags;
wenzelm
parents: 32810
diff changeset
    86
        (case group of
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    87
           NONE => ((a, th) :: thms, seen_groups)
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    88
         | SOME grp =>
33769
6d8630fab26a unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
wenzelm
parents: 33642
diff changeset
    89
             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
    90
               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
    91
             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
    92
      else q) new_thms ([], Inttab.empty);
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    93
  in rev thms' end;
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    94
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    95
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    96