src/Pure/Thy/thm_deps.ML
author wenzelm
Wed, 16 Apr 2008 21:53:05 +0200
changeset 26697 3b9eede40608
parent 26185 e53165319347
child 26699 6c7e4d858bae
permissions -rw-r--r--
removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;
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 enable: unit -> unit
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    11
  val disable: unit -> unit
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    12
  val thm_deps: thm list -> unit
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    13
  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
    14
end;
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
structure ThmDeps: THM_DEPS =
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    17
struct
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    18
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    19
(* thm_deps *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    20
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    21
fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ());
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    22
fun disable () = proofs := 0;
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    23
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    24
local
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    25
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    26
open Proofterm;
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    27
21646
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 20854
diff changeset
    28
fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 20854
diff changeset
    29
  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 20854
diff changeset
    30
  | dest_thm_axm _ = ("", MinProof ([], [], []));
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    31
17020
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    32
fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    33
  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    34
  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    35
  | make_deps_graph (prf % _) = make_deps_graph prf
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    36
  | make_deps_graph (MinProof (thms, axms, _)) =
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    37
      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    38
      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    39
  | make_deps_graph prf = (fn p as (gra, parents) =>
21646
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 20854
diff changeset
    40
      let val (name, prf') = dest_thm_axm prf
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    41
      in
21646
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 20854
diff changeset
    42
        if name <> "" then
16894
40f80823b451 Inttab.defined;
wenzelm
parents: 16268
diff changeset
    43
          if not (Symtab.defined gra name) then
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    44
            let
17020
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    45
              val (gra', parents') = make_deps_graph prf' (gra, []);
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21646
diff changeset
    46
              val prefx = #1 (Library.split_last (NameSpace.explode name));
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    47
              val session =
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    48
                (case prefx of
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    49
                  (x :: _) =>
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    50
                    (case ThyInfo.lookup_theory x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    51
                      SOME thy =>
24562
fc3cf01e8af1 Present.session_name;
wenzelm
parents: 21858
diff changeset
    52
                        let val name = Present.session_name thy
16268
d978482479d3 File.isatool, File.shell_path;
wenzelm
parents: 15570
diff changeset
    53
                        in if name = "" then [] else [name] end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    54
                    | NONE => [])
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    55
                 | _ => ["global"]);
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    56
            in
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20578
diff changeset
    57
              if member (op =) parents' name then (gra', parents union parents')
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17224
diff changeset
    58
              else (Symtab.update (name,
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    59
                {name = Sign.base_name name, ID = name,
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    60
                 dir = space_implode "/" (session @ prefx),
17224
a78339014063 curried_lookup/update;
wenzelm
parents: 17020
diff changeset
    61
                 unfold = false, path = "", parents = parents'}) gra',
20854
f9cf9e62d11c insert replacing ins ins_int ins_string
haftmann
parents: 20664
diff changeset
    62
               insert (op =) name parents)
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    63
            end
20854
f9cf9e62d11c insert replacing ins ins_int ins_string
haftmann
parents: 20664
diff changeset
    64
          else (gra, insert (op =) name parents)
11530
b6e21f6cfacd Adapted to new proof terms.
berghofe
parents: 9502
diff changeset
    65
        else
17020
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    66
          make_deps_graph prf' (gra, parents)
f3014afac46f Adapted to new argument format of MinProof constructor.
berghofe
parents: 16894
diff changeset
    67
      end);
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    68
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    69
in
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    70
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    71
fun thm_deps thms =
20578
f26c8408a675 Present.display_graph;
wenzelm
parents: 18799
diff changeset
    72
  Present.display_graph
26138
dc578de1d3e9 thm_deps: sort result;
wenzelm
parents: 24562
diff changeset
    73
    (map snd (sort_wrt fst (Symtab.dest (fst
dc578de1d3e9 thm_deps: sort result;
wenzelm
parents: 24562
diff changeset
    74
      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
    75
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    76
end;
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    77
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    78
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    79
(* unused_thms *)
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    80
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    81
fun unused_thms (base_thys, thys) =
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    82
  let
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    83
    fun add_fact (name, ths) =
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    84
      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    85
      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    86
    val thms = sort_wrt #1 (fold (Facts.fold_static add_fact o PureThy.facts_of) thys []);
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    87
    val tab = fold Proofterm.thms_of_proof
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    88
      (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    89
    fun is_unused (name, th) = case Symtab.lookup tab name of
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    90
        NONE => true
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    91
      | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    92
    (* groups containing at least one used theorem *)
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    93
    val grps = fold (fn p as (_, thm) => if is_unused p then I else
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    94
      case PureThy.get_group thm of
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    95
        NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    96
    val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
    97
      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    98
        andalso is_unused p
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
    99
      then
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   100
        (case PureThy.get_group thm of
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   101
           NONE => (p :: thms, grps')
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   102
         | SOME grp =>
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   103
             (* do not output theorem if another theorem in group has been used *)
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
   104
             if Symtab.defined grps grp then q
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   105
             (* output at most one unused theorem per group *)
26697
3b9eede40608 removed obsolete BASIC_THM_DEPS;
wenzelm
parents: 26185
diff changeset
   106
             else if Symtab.defined grps' grp then q
26185
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   107
             else (p :: thms, Symtab.update (grp, ()) grps'))
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   108
      else q) thms ([], Symtab.empty)
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   109
  in rev thms' end;
e53165319347 Added function for finding unused theorems.
berghofe
parents: 26138
diff changeset
   110
7765
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
   111
end;
fa28bac7903c New function thm_deps for visualizing dependencies of theorems.
berghofe
parents:
diff changeset
   112