src/Pure/Thy/thm_deps.ML
changeset 28810 e915ab11fe52
parent 27865 27a8ad9612a3
child 28814 463c9e9111ae
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat Nov 15 21:31:35 2008 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Nov 15 21:31:36 2008 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  signature THM_DEPS =
     1.6  sig
     1.7 -  val enable: unit -> unit
     1.8 -  val disable: unit -> unit
     1.9    val thm_deps: thm list -> unit
    1.10    val unused_thms: theory list * theory list -> (string * thm) list
    1.11  end;
    1.12 @@ -18,62 +16,36 @@
    1.13  
    1.14  (* thm_deps *)
    1.15  
    1.16 -fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ());
    1.17 -fun disable () = proofs := 0;
    1.18 -
    1.19 -local
    1.20 -
    1.21 -open Proofterm;
    1.22 -
    1.23 -fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
    1.24 -  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
    1.25 -  | dest_thm_axm _ = ("", MinProof ([], [], []));
    1.26 -
    1.27 -fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
    1.28 -  | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
    1.29 -  | make_deps_graph (prf1 %% prf2) = make_deps_graph prf1 #> make_deps_graph prf2
    1.30 -  | make_deps_graph (prf % _) = make_deps_graph prf
    1.31 -  | make_deps_graph (MinProof (thms, axms, _)) =
    1.32 -      fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
    1.33 -      fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
    1.34 -  | make_deps_graph prf = (fn p as (gra, parents) =>
    1.35 -      let val (name, prf') = dest_thm_axm prf
    1.36 -      in
    1.37 -        if name <> "" then
    1.38 -          if not (Symtab.defined gra name) then
    1.39 -            let
    1.40 -              val (gra', parents') = make_deps_graph prf' (gra, []);
    1.41 -              val prefx = #1 (Library.split_last (NameSpace.explode name));
    1.42 -              val session =
    1.43 -                (case prefx of
    1.44 -                  (x :: _) =>
    1.45 -                    (case ThyInfo.lookup_theory x of
    1.46 -                      SOME thy =>
    1.47 -                        let val name = Present.session_name thy
    1.48 -                        in if name = "" then [] else [name] end
    1.49 -                    | NONE => [])
    1.50 -                 | _ => ["global"]);
    1.51 -            in
    1.52 -              if member (op =) parents' name then (gra', parents union parents')
    1.53 -              else (Symtab.update (name,
    1.54 -                {name = Sign.base_name name, ID = name,
    1.55 -                 dir = space_implode "/" (session @ prefx),
    1.56 -                 unfold = false, path = "", parents = parents'}) gra',
    1.57 -               insert (op =) name parents)
    1.58 -            end
    1.59 -          else (gra, insert (op =) name parents)
    1.60 -        else
    1.61 -          make_deps_graph prf' (gra, parents)
    1.62 -      end);
    1.63 -
    1.64 -in
    1.65 +fun add_dep ((name, _, _), PBody {thms = thms', ...}) =
    1.66 +  name <> "" ?
    1.67 +    Graph.new_node (name, ()) #>
    1.68 +    fold (fn (_, ((name', _, _), _)) => name <> "" ? Graph.add_edge (name', name)) thms';
    1.69  
    1.70  fun thm_deps thms =
    1.71 -  Present.display_graph
    1.72 -    (map snd (sort_wrt fst (Symtab.dest (fst
    1.73 -      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
    1.74 -
    1.75 -end;
    1.76 +  let
    1.77 +    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_of thms) Graph.empty;
    1.78 +    fun add_entry (name, (_, (preds, _))) =
    1.79 +      let
    1.80 +        val prefix = #1 (Library.split_last (NameSpace.explode name));
    1.81 +        val session =
    1.82 +          (case prefix of
    1.83 +            a :: _ =>
    1.84 +              (case ThyInfo.lookup_theory a of
    1.85 +                SOME thy =>
    1.86 +                  (case Present.session_name thy of
    1.87 +                    "" => []
    1.88 +                  | session => [session])
    1.89 +              | NONE => [])
    1.90 +           | _ => ["global"]);
    1.91 +        val entry =
    1.92 +          {name = Sign.base_name name,
    1.93 +           ID = name,
    1.94 +           dir = space_implode "/" (session @ prefix),
    1.95 +           unfold = false,
    1.96 +           path = "",
    1.97 +           parents = preds};
    1.98 +      in cons entry end;
    1.99 +  in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end;
   1.100  
   1.101  
   1.102  (* unused_thms *)
   1.103 @@ -86,11 +58,13 @@
   1.104      val thms =
   1.105        fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
   1.106        |> sort_distinct (string_ord o pairself #1);
   1.107 -    val tab = fold Proofterm.thms_of_proof
   1.108 +
   1.109 +    val tab = Proofterm.fold_body_thms
   1.110 +      (fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
   1.111        (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
   1.112 -    fun is_unused (name, th) = case Symtab.lookup tab name of
   1.113 -        NONE => true
   1.114 -      | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
   1.115 +    fun is_unused (name, th) =
   1.116 +      not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
   1.117 +
   1.118      (* groups containing at least one used theorem *)
   1.119      val grps = fold (fn p as (_, thm) => if is_unused p then I else
   1.120        case Thm.get_group thm of