# HG changeset patch # User wenzelm # Date 1566563571 -7200 # Node ID 048cf2096186fe0c17e7419d7e662da73f10d885 # Parent 8088cf2576f31bdb6182d171ff0e06494c490639 clarified 'thm_deps' command; diff -r 8088cf2576f3 -r 048cf2096186 NEWS --- a/NEWS Fri Aug 23 13:32:27 2019 +0200 +++ b/NEWS Fri Aug 23 14:32:51 2019 +0200 @@ -23,6 +23,10 @@ * Command 'thm_oracles' prints all oracles used in given theorems, covering the full graph of transitive dependencies. +* Command 'thm_deps' prints immediate theorem dependencies of the given +facts. The former graph visualization has been discontinued, because it +was hardly usable. + *** Isar *** diff -r 8088cf2576f3 -r 048cf2096186 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Aug 23 13:32:27 2019 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Aug 23 14:32:51 2019 +0200 @@ -589,8 +589,9 @@ matches against subtypes. The criterion \name: p\ and the prefix ``\-\'' function as described for @{command "find_theorems"}. - \<^descr> @{command "thm_deps"}~\a\<^sub>1 \ a\<^sub>n\ visualizes dependencies of facts, using - Isabelle's graph browser tool (see also @{cite "isabelle-system"}). + \<^descr> @{command "thm_deps"}~\thms\ prints immediate theorem dependencies, i.e.\ + the union of all theorems that are used directly to prove the argument + facts, without going deeper into the dependency graph. \<^descr> @{command "unused_thms"}~\A\<^sub>1 \ A\<^sub>m - B\<^sub>1 \ B\<^sub>n\ displays all theorems that are proved in theories \B\<^sub>1 \ B\<^sub>n\ or their parents but not in \A\<^sub>1 \ diff -r 8088cf2576f3 -r 048cf2096186 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri Aug 23 13:32:27 2019 +0200 +++ b/src/Pure/Pure.thy Fri Aug 23 14:32:51 2019 +0200 @@ -1301,13 +1301,14 @@ val _ = - Outer_Syntax.command \<^command_keyword>\thm_deps\ "visualize theorem dependencies" + Outer_Syntax.command \<^command_keyword>\thm_deps\ + "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; - in Thm_Deps.thm_deps_cmd thy (Attrib.eval_thms ctxt args) end))); + in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ diff -r 8088cf2576f3 -r 048cf2096186 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Fri Aug 23 13:32:27 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Fri Aug 23 14:32:51 2019 +0200 @@ -259,7 +259,7 @@ fun encode_thm raw_thm = let - val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm); + val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm raw_thm; val raw_proof = if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else Proofterm.MinProof; diff -r 8088cf2576f3 -r 048cf2096186 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Fri Aug 23 13:32:27 2019 +0200 +++ b/src/Pure/Thy/thm_deps.ML Fri Aug 23 14:32:51 2019 +0200 @@ -10,8 +10,8 @@ val all_oracles: thm list -> Proofterm.oracle list val has_skip_proof: thm list -> bool val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T - val thm_deps: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) list - val thm_deps_cmd: theory -> thm list -> unit + val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list + val pretty_thm_deps: theory -> thm list -> Pretty.T val unused_thms_cmd: theory list * theory list -> (string * thm) list end; @@ -62,45 +62,21 @@ |> fold deps (Proofterm.thm_node_thms thm_node)) end; in - fn thm => - (fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty, []) + fn thms => + (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, []) |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) end; - -(* thm_deps_cmd *) - -fun thm_deps_cmd thy thms = +fun pretty_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; + val ctxt = Proof_Context.init_global thy; + val items = + map #2 (thm_deps thy thms) + |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) + |> sort_by (#2 o #1) + |> map (fn ((marks, xname), i) => + Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); + in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; (* unused_thms_cmd *)