1(*  Title:      Pure/thm_deps.ML
2    Author:     Stefan Berghofer, TU Muenchen
3    Author:     Makarius
4
5Dependencies of theorems wrt. internal derivation.
6*)
7
8signature THM_DEPS =
9sig
10  val all_oracles: thm list -> Proofterm.oracle list
11  val has_skip_proof: thm list -> bool
12  val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
13  val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
14  val pretty_thm_deps: theory -> thm list -> Pretty.T
15  val unused_thms_cmd: theory list * theory list -> (string * thm) list
16end;
17
18structure Thm_Deps: THM_DEPS =
19struct
20
21(* oracles *)
22
23fun all_oracles thms =
24  let
25    fun collect (PBody {oracles, thms, ...}) =
26      (if null oracles then I else apfst (cons oracles)) #>
27      (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
28        if Inttab.defined seen i then (res, seen)
29        else
30          let val body = Future.join (Proofterm.thm_node_body thm_node)
31          in collect body (res, Inttab.update (i, ()) seen) end));
32    val bodies = map Thm.proof_body_of thms;
33  in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
34
35fun has_skip_proof thms =
36  all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
37
38fun pretty_thm_oracles ctxt thms =
39  let
40    val thy = Proof_Context.theory_of ctxt;
41    fun prt_ora (name, pos) = Thm.pretty_oracle ctxt name :: Pretty.here pos;
42    fun prt_oracle (ora, NONE) = prt_ora ora
43      | prt_oracle (ora, SOME prop) =
44          prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
45    val oracles =
46      (case try all_oracles thms of
47        SOME oracles => oracles
48      | NONE => error "Malformed proofs")
49  in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;
50
51
52(* thm_deps *)
53
54fun thm_deps thy =
55  let
56    val lookup = Global_Theory.lookup_thm_id thy;
57    fun deps (i, thm_node) res =
58      if Inttab.defined res i then res
59      else
60        let val thm_id = Proofterm.thm_id (i, thm_node) in
61          (case lookup thm_id of
62            SOME thm_name =>
63              Inttab.update (i, SOME (thm_id, thm_name)) res
64          | NONE =>
65              Inttab.update (i, NONE) res
66              |> fold deps (Proofterm.thm_node_thms thm_node))
67        end;
68  in
69    fn thms =>
70      (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, [])
71      |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
72  end;
73
74fun pretty_thm_deps thy thms =
75  let
76    val ctxt = Proof_Context.init_global thy;
77    val deps =
78      (case try (thm_deps thy) thms of
79        SOME deps => deps
80      | NONE => error "Malformed proofs");
81    val items =
82      map #2 deps
83      |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
84      |> sort_by (#2 o #1)
85      |> map (fn ((marks, xname), i) =>
86          Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]);
87  in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
88
89
90(* unused_thms_cmd *)
91
92fun unused_thms_cmd (base_thys, thys) =
93  let
94    fun add_fact transfer space (name, ths) =
95      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
96      else
97        let val {concealed, group, ...} = Name_Space.the_entry space name in
98          fold_rev (transfer #> (fn th =>
99            (case Thm.derivation_name th of
100              "" => I
101            | a => cons (a, (th, concealed, group))))) ths
102        end;
103    fun add_facts thy =
104      let
105        val transfer = Global_Theory.transfer_theories thy;
106        val facts = Global_Theory.facts_of thy;
107      in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end;
108
109    val new_thms =
110      fold add_facts thys []
111      |> sort_distinct (string_ord o apply2 #1);
112
113    val used =
114      Proofterm.fold_body_thms
115        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
116        (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
117        Symtab.empty;
118
119    fun is_unused a = not (Symtab.defined used a);
120
121    (*groups containing at least one used theorem*)
122    val used_groups = fold (fn (a, (_, _, group)) =>
123      if is_unused a then I
124      else
125        (case group of
126          NONE => I
127        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
128
129    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
130      if not concealed andalso
131        (* FIXME replace by robust treatment of thm groups *)
132        Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
133      then
134        (case group of
135           NONE => ((a, th) :: thms, seen_groups)
136         | SOME grp =>
137             if Inttab.defined used_groups grp orelse
138               Inttab.defined seen_groups grp then q
139             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
140      else q) new_thms ([], Inttab.empty);
141  in rev thms' end;
142
143end;
144