removed obsolete BASIC_THM_DEPS;
authorwenzelm
Wed Apr 16 21:53:05 2008 +0200 (2008-04-16)
changeset 266973b9eede40608
parent 26696 1cd71fb32831
child 26698 ca558202ffa5
removed obsolete BASIC_THM_DEPS;
unused_thms: simplified signature, use proper PureThy.facts_of;
misc tuning;
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Apr 16 21:53:04 2008 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Apr 16 21:53:05 2008 +0200
     1.3 @@ -5,27 +5,26 @@
     1.4  Visualize dependencies of theorems.
     1.5  *)
     1.6  
     1.7 -signature BASIC_THM_DEPS =
     1.8 -sig
     1.9 -  val thm_deps : thm list -> unit
    1.10 -end;
    1.11 -
    1.12  signature THM_DEPS =
    1.13  sig
    1.14 -  include BASIC_THM_DEPS
    1.15 -  val enable : unit -> unit
    1.16 -  val disable : unit -> unit
    1.17 -  val unused_thms : theory list option * theory list -> (string * thm) list
    1.18 +  val enable: unit -> unit
    1.19 +  val disable: unit -> unit
    1.20 +  val thm_deps: thm list -> unit
    1.21 +  val unused_thms: theory list * theory list -> (string * thm) list
    1.22  end;
    1.23  
    1.24 -structure ThmDeps : THM_DEPS =
    1.25 +structure ThmDeps: THM_DEPS =
    1.26  struct
    1.27  
    1.28 +(* thm_deps *)
    1.29 +
    1.30 +fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ());
    1.31 +fun disable () = proofs := 0;
    1.32 +
    1.33 +local
    1.34 +
    1.35  open Proofterm;
    1.36  
    1.37 -fun enable () = if ! proofs = 0 then proofs := 1 else ();
    1.38 -fun disable () = proofs := 0;
    1.39 -
    1.40  fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
    1.41    | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
    1.42    | dest_thm_axm _ = ("", MinProof ([], [], []));
    1.43 @@ -67,45 +66,47 @@
    1.44            make_deps_graph prf' (gra, parents)
    1.45        end);
    1.46  
    1.47 +in
    1.48 +
    1.49  fun thm_deps thms =
    1.50    Present.display_graph
    1.51      (map snd (sort_wrt fst (Symtab.dest (fst
    1.52        (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
    1.53  
    1.54 -fun unused_thms (opt_thys1, thys2) =
    1.55 +end;
    1.56 +
    1.57 +
    1.58 +(* unused_thms *)
    1.59 +
    1.60 +fun unused_thms (base_thys, thys) =
    1.61    let
    1.62 -    val thys = case opt_thys1 of
    1.63 -        NONE => thys2
    1.64 -      | SOME thys1 =>
    1.65 -          thys2 |>
    1.66 -          fold (curry (gen_union Theory.eq_thy)) (map Context.ancestors_of thys2) |>
    1.67 -          fold (subtract Theory.eq_thy) (thys1 :: map Context.ancestors_of thys1);
    1.68 -    val thms = maps PureThy.thms_of thys;
    1.69 +    fun add_fact (name, ths) =
    1.70 +      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
    1.71 +      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
    1.72 +    val thms = sort_wrt #1 (fold (Facts.fold_static add_fact o PureThy.facts_of) thys []);
    1.73      val tab = fold Proofterm.thms_of_proof
    1.74 -      (map (Proofterm.strip_thm o proof_of o snd) thms) Symtab.empty;
    1.75 -    fun is_unused (s, thm) = case Symtab.lookup tab s of
    1.76 +      (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
    1.77 +    fun is_unused (name, th) = case Symtab.lookup tab name of
    1.78          NONE => true
    1.79 -      | SOME ps => not (prop_of thm mem map fst ps);
    1.80 +      | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
    1.81      (* groups containing at least one used theorem *)
    1.82      val grps = fold (fn p as (_, thm) => if is_unused p then I else
    1.83        case PureThy.get_group thm of
    1.84          NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
    1.85      val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
    1.86 -      if PureThy.get_kind thm mem [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
    1.87 +      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
    1.88          andalso is_unused p
    1.89        then
    1.90          (case PureThy.get_group thm of
    1.91             NONE => (p :: thms, grps')
    1.92           | SOME grp =>
    1.93               (* do not output theorem if another theorem in group has been used *)
    1.94 -             if is_some (Symtab.lookup grps grp) then q
    1.95 +             if Symtab.defined grps grp then q
    1.96               (* output at most one unused theorem per group *)
    1.97 -             else if is_some (Symtab.lookup grps' grp) then q
    1.98 +             else if Symtab.defined grps' grp then q
    1.99               else (p :: thms, Symtab.update (grp, ()) grps'))
   1.100        else q) thms ([], Symtab.empty)
   1.101    in rev thms' end;
   1.102  
   1.103  end;
   1.104  
   1.105 -structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
   1.106 -open BasicThmDeps;