src/Pure/Thy/thm_deps.ML
author wenzelm
Mon Nov 02 21:05:47 2009 +0100 (2009-11-02)
changeset 33391 91b9da2a7b44
parent 33170 dd6d8d1f70d2
child 33642 d983509dbf31
permissions -rw-r--r--
structure Thm_Deps;
berghofe@7765
     1
(*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@7765
     3
berghofe@7765
     4
Visualize dependencies of theorems.
berghofe@7765
     5
*)
berghofe@7765
     6
berghofe@7765
     7
signature THM_DEPS =
berghofe@7765
     8
sig
wenzelm@26697
     9
  val thm_deps: thm list -> unit
wenzelm@26697
    10
  val unused_thms: theory list * theory list -> (string * thm) list
berghofe@7765
    11
end;
berghofe@7765
    12
wenzelm@33391
    13
structure Thm_Deps: THM_DEPS =
berghofe@7765
    14
struct
berghofe@7765
    15
wenzelm@26697
    16
(* thm_deps *)
wenzelm@26697
    17
berghofe@7765
    18
fun thm_deps thms =
wenzelm@28810
    19
  let
wenzelm@28826
    20
    fun add_dep ("", _, _) = I
wenzelm@28826
    21
      | add_dep (name, _, PBody {thms = thms', ...}) =
wenzelm@28826
    22
          let
wenzelm@30364
    23
            val prefix = #1 (Library.split_last (Long_Name.explode name));
wenzelm@28826
    24
            val session =
wenzelm@28826
    25
              (case prefix of
wenzelm@28826
    26
                a :: _ =>
wenzelm@28826
    27
                  (case ThyInfo.lookup_theory a of
wenzelm@28826
    28
                    SOME thy =>
wenzelm@28826
    29
                      (case Present.session_name thy of
wenzelm@28826
    30
                        "" => []
wenzelm@28826
    31
                      | session => [session])
wenzelm@28826
    32
                  | NONE => [])
wenzelm@28826
    33
               | _ => ["global"]);
wenzelm@28826
    34
            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
wenzelm@28826
    35
            val entry =
wenzelm@30364
    36
              {name = Long_Name.base_name name,
wenzelm@28826
    37
               ID = name,
wenzelm@28826
    38
               dir = space_implode "/" (session @ prefix),
wenzelm@28826
    39
               unfold = false,
wenzelm@28826
    40
               path = "",
wenzelm@28826
    41
               parents = parents};
wenzelm@28826
    42
          in cons entry end;
wenzelm@32810
    43
    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
wenzelm@28826
    44
  in Present.display_graph (sort_wrt #ID deps) end;
wenzelm@26697
    45
wenzelm@26697
    46
wenzelm@26697
    47
(* unused_thms *)
wenzelm@26697
    48
wenzelm@26697
    49
fun unused_thms (base_thys, thys) =
berghofe@26185
    50
  let
wenzelm@33170
    51
    fun add_fact space (name, ths) =
wenzelm@26697
    52
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
wenzelm@33170
    53
      else
wenzelm@33170
    54
        let val {concealed, group, ...} = Name_Space.the_entry space name in
wenzelm@33170
    55
          fold_rev (fn th =>
wenzelm@33170
    56
            (case Thm.get_name th of
wenzelm@33170
    57
              "" => I
wenzelm@33170
    58
            | a => cons (a, (th, concealed, group)))) ths
wenzelm@33170
    59
        end;
wenzelm@33170
    60
    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
wenzelm@33170
    61
wenzelm@26699
    62
    val thms =
wenzelm@33170
    63
      fold (add_facts o PureThy.facts_of) thys []
wenzelm@26699
    64
      |> sort_distinct (string_ord o pairself #1);
wenzelm@28810
    65
wenzelm@32810
    66
    val tab =
wenzelm@32810
    67
      Proofterm.fold_body_thms
wenzelm@33170
    68
        (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop))
wenzelm@33170
    69
        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) thms) Symtab.empty;
wenzelm@33170
    70
wenzelm@33170
    71
    fun is_unused (a, th) =
wenzelm@33170
    72
      not (member (op aconv) (Symtab.lookup_list tab a) (Thm.prop_of th));
wenzelm@28810
    73
berghofe@26185
    74
    (* groups containing at least one used theorem *)
wenzelm@33170
    75
    val used_groups = fold (fn (a, (th, _, group)) =>
wenzelm@33170
    76
      if is_unused (a, th) then I
wenzelm@33170
    77
      else
wenzelm@33170
    78
        (case group of
wenzelm@33170
    79
          NONE => I
wenzelm@33170
    80
        | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
wenzelm@33170
    81
    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
wenzelm@33170
    82
      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
wenzelm@33170
    83
        (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
berghofe@26185
    84
      then
wenzelm@33170
    85
        (case group of
wenzelm@33170
    86
           NONE => ((a, th) :: thms, grps')
berghofe@26185
    87
         | SOME grp =>
berghofe@26185
    88
             (* do not output theorem if another theorem in group has been used *)
wenzelm@33170
    89
             if Inttab.defined used_groups grp then q
berghofe@26185
    90
             (* output at most one unused theorem per group *)
wenzelm@33170
    91
             else if Inttab.defined grps' grp then q
wenzelm@33170
    92
             else ((a, th) :: thms, Inttab.update (grp, ()) grps'))
wenzelm@33170
    93
      else q) thms ([], Inttab.empty)
berghofe@26185
    94
  in rev thms' end;
berghofe@26185
    95
berghofe@7765
    96
end;
berghofe@7765
    97