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