# HG changeset patch # User wenzelm # Date 1566033196 -7200 # Node ID 038ed9b76c2b6e4caced755244889eafbe9127e7 # Parent c1fde53e5e8212b202f4e5c5e19bebef53247679 clarified modules; diff -r c1fde53e5e82 -r 038ed9b76c2b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Aug 17 11:02:09 2019 +0200 +++ b/src/Pure/ROOT.ML Sat Aug 17 11:13:16 2019 +0200 @@ -309,6 +309,7 @@ ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; +ML_file "Thy/thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; @@ -341,7 +342,6 @@ ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; -ML_file "Tools/thm_deps.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; diff -r c1fde53e5e82 -r 038ed9b76c2b src/Pure/Thy/thm_deps.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/thm_deps.ML Sat Aug 17 11:13:16 2019 +0200 @@ -0,0 +1,105 @@ +(* Title: Pure/Thy/thm_deps.ML + Author: Stefan Berghofer, TU Muenchen + Author: Makarius + +Dependencies of theorems wrt. internal derivation. +*) + +signature THM_DEPS = +sig + val thm_deps: theory -> thm list -> unit + val unused_thms: theory list * theory list -> (string * thm) list +end; + +structure Thm_Deps: THM_DEPS = +struct + +(* thm_deps *) + +fun thm_deps thy thms = + let + fun make_node name directory = + Graph_Display.session_node + {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""}; + fun add_dep {name = "", ...} = I + | add_dep {name = name, body = PBody {thms = thms', ...}, ...} = + let + val prefix = #1 (split_last (Long_Name.explode name)); + val session = + (case prefix of + a :: _ => + (case try (Context.get_theory {long = false} thy) a of + SOME thy => + (case Present.theory_qualifier thy of + "" => [] + | session => [session]) + | NONE => []) + | _ => ["global"]); + val node = make_node name (space_implode "/" (session @ prefix)); + val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms'); + in Symtab.update (name, (node, deps)) end; + val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty; + val entries1 = + Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab => + if Symtab.defined tab d then tab + else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0; + in + Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 [] + |> Graph_Display.display_graph_old + end; + + +(* unused_thms *) + +fun unused_thms (base_thys, thys) = + let + fun add_fact transfer space (name, ths) = + if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I + else + let val {concealed, group, ...} = Name_Space.the_entry space name in + fold_rev (fn th => + (case Thm.derivation_name th of + "" => I + | a => cons (a, (transfer th, concealed, group)))) ths + end; + fun add_facts thy = + let + val transfer = Global_Theory.transfer_theories thy; + val facts = Global_Theory.facts_of thy; + in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; + + val new_thms = + fold add_facts thys [] + |> sort_distinct (string_ord o apply2 #1); + + val used = + Proofterm.fold_body_thms + (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) + (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) + Symtab.empty; + + fun is_unused a = not (Symtab.defined used a); + + (*groups containing at least one used theorem*) + val used_groups = fold (fn (a, (_, _, group)) => + if is_unused a then I + else + (case group of + NONE => I + | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; + + val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => + if not concealed andalso + (* FIXME replace by robust treatment of thm groups *) + Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a + then + (case group of + NONE => ((a, th) :: thms, seen_groups) + | SOME grp => + if Inttab.defined used_groups grp orelse + Inttab.defined seen_groups grp then q + else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) + else q) new_thms ([], Inttab.empty); + in rev thms' end; + +end; diff -r c1fde53e5e82 -r 038ed9b76c2b src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Sat Aug 17 11:02:09 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -(* Title: Pure/Tools/thm_deps.ML - Author: Stefan Berghofer, TU Muenchen - -Visualize dependencies of theorems. -*) - -signature THM_DEPS = -sig - val thm_deps: theory -> thm list -> unit - val unused_thms: theory list * theory list -> (string * thm) list -end; - -structure Thm_Deps: THM_DEPS = -struct - -(* thm_deps *) - -fun thm_deps thy thms = - let - fun make_node name directory = - Graph_Display.session_node - {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""}; - fun add_dep {name = "", ...} = I - | add_dep {name = name, body = PBody {thms = thms', ...}, ...} = - let - val prefix = #1 (split_last (Long_Name.explode name)); - val session = - (case prefix of - a :: _ => - (case try (Context.get_theory {long = false} thy) a of - SOME thy => - (case Present.theory_qualifier thy of - "" => [] - | session => [session]) - | NONE => []) - | _ => ["global"]); - val node = make_node name (space_implode "/" (session @ prefix)); - val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms'); - in Symtab.update (name, (node, deps)) end; - val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty; - val entries1 = - Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab => - if Symtab.defined tab d then tab - else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0; - in - Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 [] - |> Graph_Display.display_graph_old - end; - - -(* unused_thms *) - -fun unused_thms (base_thys, thys) = - let - fun add_fact transfer space (name, ths) = - if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I - else - let val {concealed, group, ...} = Name_Space.the_entry space name in - fold_rev (fn th => - (case Thm.derivation_name th of - "" => I - | a => cons (a, (transfer th, concealed, group)))) ths - end; - fun add_facts thy = - let - val transfer = Global_Theory.transfer_theories thy; - val facts = Global_Theory.facts_of thy; - in Facts.fold_static (add_fact transfer (Facts.space_of facts)) facts end; - - val new_thms = - fold add_facts thys [] - |> sort_distinct (string_ord o apply2 #1); - - val used = - Proofterm.fold_body_thms - (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) - (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) - Symtab.empty; - - fun is_unused a = not (Symtab.defined used a); - - (*groups containing at least one used theorem*) - val used_groups = fold (fn (a, (_, _, group)) => - if is_unused a then I - else - (case group of - NONE => I - | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; - - val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => - if not concealed andalso - (* FIXME replace by robust treatment of thm groups *) - Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a - then - (case group of - NONE => ((a, th) :: thms, seen_groups) - | SOME grp => - if Inttab.defined used_groups grp orelse - Inttab.defined seen_groups grp then q - else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) - else q) new_thms ([], Inttab.empty); - in rev thms' end; - -end;