src/Pure/Thy/thm_deps.ML
author wenzelm
Mon, 17 Nov 2008 21:28:46 +0100
changeset 28826 3b460b6eadae
parent 28817 c8cc94a470d4
child 29606 fedb8be05f24
permissions -rw-r--r--
simplified thm_deps -- no need to build a graph datastructure;
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
    ID:         $Id$
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     4
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     5
Visualize dependencies of theorems.
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
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     8
signature THM_DEPS =
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
     9
sig
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    10
  val thm_deps: thm list -> unit
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    11
  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
    12
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    13
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    14
structure ThmDeps: THM_DEPS =
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    15
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    16
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    17
(* thm_deps *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    18
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    19
fun thm_deps thms =
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    20
  let
28826
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    21
    fun add_dep ("", _, _) = I
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    22
      | add_dep (name, _, PBody {thms = thms', ...}) =
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    23
          let
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    24
            val prefix = #1 (Library.split_last (NameSpace.explode name));
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    25
            val session =
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    26
              (case prefix of
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    27
                a :: _ =>
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    28
                  (case ThyInfo.lookup_theory a of
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    29
                    SOME thy =>
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    30
                      (case Present.session_name thy of
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    31
                        "" => []
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    32
                      | session => [session])
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    33
                  | NONE => [])
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    34
               | _ => ["global"]);
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    35
            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
    36
            val entry =
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    37
              {name = Sign.base_name name,
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    38
               ID = name,
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    39
               dir = space_implode "/" (session @ prefix),
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    40
               unfold = false,
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    41
               path = "",
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    42
               parents = parents};
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    43
          in cons entry end;
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    44
    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
3b460b6eadae simplified thm_deps -- no need to build a graph datastructure;
wenzelm
parents: 28817
diff changeset
    45
  in Present.display_graph (sort_wrt #ID deps) end;
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    46
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    47
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    48
(* unused_thms *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    49
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    50
fun unused_thms (base_thys, thys) =
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    51
  let
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    52
    fun add_fact (name, ths) =
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    53
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    54
      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
26699
6c7e4d858bae unused_thms: sort_distinct;
wenzelm
parents: 26697
diff changeset
    55
    val thms =
6c7e4d858bae unused_thms: sort_distinct;
wenzelm
parents: 26697
diff changeset
    56
      fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
6c7e4d858bae unused_thms: sort_distinct;
wenzelm
parents: 26697
diff changeset
    57
      |> sort_distinct (string_ord o pairself #1);
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    58
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    59
    val tab = Proofterm.fold_body_thms
28817
c8cc94a470d4 proof_body/pthm: removed redundant types field;
wenzelm
parents: 28814
diff changeset
    60
      (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28810
diff changeset
    61
      (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
28810
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    62
    fun is_unused (name, th) =
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    63
      not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
e915ab11fe52 retrieve thm deps from proof_body;
wenzelm
parents: 27865
diff changeset
    64
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    65
    (* groups containing at least one used theorem *)
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    66
    val grps = fold (fn p as (_, thm) => if is_unused p then I else
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26699
diff changeset
    67
      case Thm.get_group thm of
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    68
        NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    69
    val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26699
diff changeset
    70
      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    71
        andalso is_unused p
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    72
      then
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26699
diff changeset
    73
        (case Thm.get_group thm of
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    74
           NONE => (p :: thms, grps')
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    75
         | SOME grp =>
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    76
             (* do not output theorem if another theorem in group has been used *)
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    77
             if Symtab.defined grps grp then q
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    78
             (* output at most one unused theorem per group *)
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    79
             else if Symtab.defined grps' grp then q
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    80
             else (p :: thms, Symtab.update (grp, ()) grps'))
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    81
      else q) thms ([], Symtab.empty)
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    82
  in rev thms' end;
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    83
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    84
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    85