src/Pure/Thy/thm_deps.ML
author wenzelm
Thu Apr 17 11:40:00 2008 +0200 (2008-04-17)
changeset 26699 6c7e4d858bae
parent 26697 3b9eede40608
child 27865 27a8ad9612a3
permissions -rw-r--r--
unused_thms: sort_distinct;
berghofe@7765
     1
(*  Title:      Pure/Thy/thm_deps.ML
berghofe@7765
     2
    ID:         $Id$
berghofe@7765
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@7765
     4
berghofe@7765
     5
Visualize dependencies of theorems.
berghofe@7765
     6
*)
berghofe@7765
     7
berghofe@7765
     8
signature THM_DEPS =
berghofe@7765
     9
sig
wenzelm@26697
    10
  val enable: unit -> unit
wenzelm@26697
    11
  val disable: unit -> unit
wenzelm@26697
    12
  val thm_deps: thm list -> unit
wenzelm@26697
    13
  val unused_thms: theory list * theory list -> (string * thm) list
berghofe@7765
    14
end;
berghofe@7765
    15
wenzelm@26697
    16
structure ThmDeps: THM_DEPS =
berghofe@7765
    17
struct
berghofe@7765
    18
wenzelm@26697
    19
(* thm_deps *)
wenzelm@26697
    20
wenzelm@26697
    21
fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ());
wenzelm@26697
    22
fun disable () = proofs := 0;
wenzelm@26697
    23
wenzelm@26697
    24
local
wenzelm@26697
    25
berghofe@11530
    26
open Proofterm;
berghofe@7765
    27
wenzelm@21646
    28
fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
wenzelm@21646
    29
  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
wenzelm@21646
    30
  | dest_thm_axm _ = ("", MinProof ([], [], []));
berghofe@7765
    31
berghofe@17020
    32
fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
berghofe@17020
    33
  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
berghofe@17020
    34
  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
berghofe@17020
    35
  | make_deps_graph (prf % _) = make_deps_graph prf
berghofe@17020
    36
  | make_deps_graph (MinProof (thms, axms, _)) =
berghofe@17020
    37
      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
berghofe@17020
    38
      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
berghofe@17020
    39
  | make_deps_graph prf = (fn p as (gra, parents) =>
wenzelm@21646
    40
      let val (name, prf') = dest_thm_axm prf
berghofe@11530
    41
      in
wenzelm@21646
    42
        if name <> "" then
wenzelm@16894
    43
          if not (Symtab.defined gra name) then
berghofe@11530
    44
            let
berghofe@17020
    45
              val (gra', parents') = make_deps_graph prf' (gra, []);
wenzelm@21858
    46
              val prefx = #1 (Library.split_last (NameSpace.explode name));
berghofe@11530
    47
              val session =
berghofe@11530
    48
                (case prefx of
berghofe@11530
    49
                  (x :: _) =>
berghofe@11530
    50
                    (case ThyInfo.lookup_theory x of
skalberg@15531
    51
                      SOME thy =>
wenzelm@24562
    52
                        let val name = Present.session_name thy
wenzelm@16268
    53
                        in if name = "" then [] else [name] end
skalberg@15531
    54
                    | NONE => [])
berghofe@11530
    55
                 | _ => ["global"]);
berghofe@11530
    56
            in
wenzelm@20664
    57
              if member (op =) parents' name then (gra', parents union parents')
wenzelm@17412
    58
              else (Symtab.update (name,
berghofe@11530
    59
                {name = Sign.base_name name, ID = name,
berghofe@11530
    60
                 dir = space_implode "/" (session @ prefx),
wenzelm@17224
    61
                 unfold = false, path = "", parents = parents'}) gra',
haftmann@20854
    62
               insert (op =) name parents)
berghofe@11530
    63
            end
haftmann@20854
    64
          else (gra, insert (op =) name parents)
berghofe@11530
    65
        else
berghofe@17020
    66
          make_deps_graph prf' (gra, parents)
berghofe@17020
    67
      end);
berghofe@7765
    68
wenzelm@26697
    69
in
wenzelm@26697
    70
berghofe@7765
    71
fun thm_deps thms =
wenzelm@20578
    72
  Present.display_graph
wenzelm@26138
    73
    (map snd (sort_wrt fst (Symtab.dest (fst
wenzelm@26138
    74
      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
berghofe@7765
    75
wenzelm@26697
    76
end;
wenzelm@26697
    77
wenzelm@26697
    78
wenzelm@26697
    79
(* unused_thms *)
wenzelm@26697
    80
wenzelm@26697
    81
fun unused_thms (base_thys, thys) =
berghofe@26185
    82
  let
wenzelm@26697
    83
    fun add_fact (name, ths) =
wenzelm@26697
    84
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
wenzelm@26697
    85
      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
wenzelm@26699
    86
    val thms =
wenzelm@26699
    87
      fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
wenzelm@26699
    88
      |> sort_distinct (string_ord o pairself #1);
berghofe@26185
    89
    val tab = fold Proofterm.thms_of_proof
wenzelm@26697
    90
      (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
wenzelm@26697
    91
    fun is_unused (name, th) = case Symtab.lookup tab name of
berghofe@26185
    92
        NONE => true
wenzelm@26697
    93
      | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
berghofe@26185
    94
    (* groups containing at least one used theorem *)
berghofe@26185
    95
    val grps = fold (fn p as (_, thm) => if is_unused p then I else
berghofe@26185
    96
      case PureThy.get_group thm of
berghofe@26185
    97
        NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
berghofe@26185
    98
    val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
wenzelm@26697
    99
      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
berghofe@26185
   100
        andalso is_unused p
berghofe@26185
   101
      then
berghofe@26185
   102
        (case PureThy.get_group thm of
berghofe@26185
   103
           NONE => (p :: thms, grps')
berghofe@26185
   104
         | SOME grp =>
berghofe@26185
   105
             (* do not output theorem if another theorem in group has been used *)
wenzelm@26697
   106
             if Symtab.defined grps grp then q
berghofe@26185
   107
             (* output at most one unused theorem per group *)
wenzelm@26697
   108
             else if Symtab.defined grps' grp then q
berghofe@26185
   109
             else (p :: thms, Symtab.update (grp, ()) grps'))
berghofe@26185
   110
      else q) thms ([], Symtab.empty)
berghofe@26185
   111
  in rev thms' end;
berghofe@26185
   112
berghofe@7765
   113
end;
berghofe@7765
   114