# HG changeset patch # User wenzelm # Date 1420031752 -3600 # Node ID 2486d625878b98b734eb95405ce9752a551d5e37 # Parent 6b030dc97a4f493492932bf5d2216bb7f60a4c8f for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes diff -r 6b030dc97a4f -r 2486d625878b src/Pure/General/graph_display.ML --- a/src/Pure/General/graph_display.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Pure/General/graph_display.ML Wed Dec 31 14:15:52 2014 +0100 @@ -6,10 +6,10 @@ signature GRAPH_DISPLAY = sig - type node = - {name: string, ident: string, directory: string, unfold: bool, - path: string, parents: string list, content: Pretty.T list} - type graph = node list + type node + val content_node: string -> Pretty.T list -> node + val session_node: {name: string, unfold: bool, directory: string, path: string} -> node + type graph = string list * node Graph.T val write_graph_browser: Path.T -> graph -> unit val browserN: string val graphviewN: string @@ -20,13 +20,19 @@ structure Graph_Display: GRAPH_DISPLAY = struct -(* external graph representation *) +(* abstract graph representation *) + +type node = {name: string, content: Pretty.T list, + unfold: bool, directory: string, path: string}; -type node = - {name: string, ident: string, directory: string, unfold: bool, - path: string, parents: string list, content: Pretty.T list}; +type graph = string list * node Graph.T; + (*partial explicit order in left argument*) -type graph = node list; +fun content_node name content = + {name = name, content = content, unfold = true, directory = "", path = ""}; + +fun session_node {name: string, unfold: bool, directory: string, path: string} = + {name = name, content = [], unfold = unfold, directory = directory, path = path}; (* print modes *) @@ -43,20 +49,21 @@ (* encode graph *) -fun encode_browser (graph: graph) = - cat_lines (map (fn {name, ident, directory, unfold, path, parents, ...} => - "\"" ^ name ^ "\" \"" ^ ident ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^ - path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph); +fun encode_browser ((keys, gr) : graph) = + fold_rev (update (op =)) (Graph.keys gr) keys + |> map (fn key => case Graph.get_node gr key of {name, unfold, content, directory, path} => + "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^ + path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;") + |> cat_lines; fun write_graph_browser path graph = File.write path (encode_browser graph); val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; -fun encode_graphview (graph: graph) = - Graph.empty - |> fold (fn {ident, name, content, ...} => Graph.new_node (ident, (name, content))) graph - |> fold (fn {ident = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph +fun encode_graphview ((_, gr): graph) = + gr + |> Graph.map (fn _ => fn {name, content, ...} => (name, content)) |> let open XML.Encode in Graph.encode string (pair string encode_content) end; @@ -80,4 +87,3 @@ in () end; end; - diff -r 6b030dc97a4f -r 2486d625878b src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Dec 31 14:15:52 2014 +0100 @@ -275,25 +275,26 @@ val thy = Toplevel.theory_of state; val thy_session = Present.session_name thy; - val graph = rev (Theory.nodes_of thy) |> map (fn node => + val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node => let val name = Context.theory_name node; val parents = map Context.theory_name (Theory.parents_of node); val session = Present.session_name node; val unfold = (session = thy_session); in - {name = name, ident = name, parents = parents, directory = session, - unfold = unfold, path = "", content = []} + ((name, Graph_Display.session_node + {name = name, directory = session, unfold = unfold, path = ""}), parents) end); - in Graph_Display.display_graph graph end); + in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end); val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; - val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => - {name = Locale.extern thy name, ident = name, parents = parents, - directory = "", unfold = true, path = "", content = [body]}); - in Graph_Display.display_graph graph end); + val gr = Locale.pretty_locale_deps thy + |> map (fn {name, parents, body} => ((name, + Graph_Display.content_node (Locale.extern thy name) [body]), parents)) + |> Graph.make; + in Graph_Display.display_graph ([], gr) end); (* print theorems, terms, types etc. *) diff -r 6b030dc97a4f -r 2486d625878b src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Pure/Thy/present.ML Wed Dec 31 14:15:52 2014 +0100 @@ -76,6 +76,9 @@ end; (*retrieve graph data from initial collection of theories*) +type browser_node = {name: string, ident: string, parents: string list, + unfold: bool, directory: string, path: string} + fun init_graph (curr_chapter, curr_session) = rev o map (fn thy => let val {chapter, name = session_name} = Browser_Info.get thy; @@ -84,18 +87,17 @@ (case theory_link (curr_chapter, curr_session) thy of NONE => "" | SOME p => Path.implode p); - val entry = + val graph_entry = {name = thy_name, ident = ID_of [chapter, session_name] thy_name, directory = session_name, path = path, unfold = false, - parents = map ID_of_thy (Theory.parents_of thy), - content = []}; - in (0, entry) end); + parents = map ID_of_thy (Theory.parents_of thy)}; + in (0, graph_entry) end); -fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) = - (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr; +fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) = + (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph; @@ -118,7 +120,7 @@ {theories: theory_info Symtab.table, tex_index: (int * string) list, html_index: (int * string) list, - graph: (int * Graph_Display.node) list}; + graph: (int * browser_node) list}; fun make_browser_info (theories, tex_index, html_index, graph) : browser_info = {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph}; @@ -276,6 +278,14 @@ (* finish session -- output all generated text *) +fun finalize_graph (nodes : (int * browser_node) list) = + nodes + |> map (fn (_, {ident, parents, name, unfold, directory, path}) => + ((ident, Graph_Display.session_node + {name = name, unfold = unfold, directory = directory, path = path}), parents)) + |> Graph.make + |> pair (map (#ident o snd) (sort (int_ord o apply2 fst) (rev nodes))); + fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; @@ -298,10 +308,10 @@ fun finish_html (a, {html_source, ...}: theory_info) = File.write (Path.append session_prefix (html_path a)) html_source; - val sorted_graph = sorted_index graph; + val graph' = finalize_graph graph; val opt_graphs = if doc_graph andalso not (null documents) then - SOME (isabelle_browser sorted_graph) + SOME (isabelle_browser graph') else NONE; val _ = @@ -310,7 +320,7 @@ File.write_buffer (Path.append session_prefix index_path) (index_buffer html_index |> Buffer.add HTML.end_document); (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); - Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph; + Graph_Display.write_graph_browser (Path.append session_prefix graph_path) graph'; Isabelle_System.isabelle_tool "browser" "-b"; Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt) @@ -387,8 +397,7 @@ directory = session_name, unfold = true, path = Path.implode (html_path name), - parents = map ID_of_thy parents, - content = []}; + parents = map ID_of_thy parents}; in init_theory_info name (make_theory_info ("", html_source)); add_graph_entry (update_time, graph_entry); diff -r 6b030dc97a4f -r 2486d625878b src/Pure/Tools/class_deps.ML --- a/src/Pure/Tools/class_deps.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Pure/Tools/class_deps.ML Wed Dec 31 14:15:52 2014 +0100 @@ -24,14 +24,11 @@ SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]); val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt) (le_super andf sub_le) (K NONE) original_algebra; - val classes = Sorts.classes_of algebra; - fun entry (c, (i, (_, cs))) = - (i, {name = Name_Space.extern ctxt space c, ident = c, parents = Graph.Keys.dest cs, - directory = "", unfold = true, path = "", content = []}); - val graph = - Graph.fold (cons o entry) classes [] - |> sort (int_ord o apply2 #1) |> map #2; - in Graph_Display.display_graph graph end; + val gr = + Sorts.classes_of algebra + |> Graph.map (fn c => fn _ => + Graph_Display.content_node (Name_Space.extern ctxt space c) []) + in Graph_Display.display_graph ([], gr) end; val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); val visualize_cmd = gen_visualize Syntax.read_sort; diff -r 6b030dc97a4f -r 2486d625878b src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Pure/Tools/thm_deps.ML Wed Dec 31 14:15:52 2014 +0100 @@ -31,18 +31,15 @@ | session => [session]) | NONE => []) | _ => ["global"]); + val directory = space_implode "/" (session @ prefix); val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); - val entry = - {name = Long_Name.base_name name, - ident = name, - directory = space_implode "/" (session @ prefix), - unfold = false, - path = "", - parents = parents, - content = []}; - in cons entry end; - val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; - in Graph_Display.display_graph (sort_wrt #ident deps) end; + in + cons ((name, Graph_Display.session_node + {name = Long_Name.base_name name, directory = directory, + unfold = false, path = ""}), parents) + end; + val gr = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; + in Graph_Display.display_graph (sort_wrt I (map (fst o fst) gr), Graph.make gr) end; val _ = Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies" diff -r 6b030dc97a4f -r 2486d625878b src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Dec 31 14:13:11 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Wed Dec 31 14:15:52 2014 +0100 @@ -911,25 +911,28 @@ fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt; +fun join_strong_conn gr = + let + val xss = Graph.strong_conn gr; + val xss_zs = map (fn xs => (xs, commas xs)) xss; + val z_for = the o AList.lookup (op =) (maps (fn (xs, z) => map (fn x => (x, z)) xs) xss_zs); + val succs = map (fn (xs, z) => (z, (map z_for o maps (Graph.immediate_succs gr)) xs)) xss_zs; + in + Graph.empty + |> fold (fn (xs, z) => Graph.new_node (z, map (Graph.get_node gr) xs)) xss_zs + |> fold (fn (z, succs) => fold (fn w => Graph.add_edge (z, w)) succs) succs + end; + fun code_deps ctxt consts = let val thy = Proof_Context.theory_of ctxt; - val eqngr = code_depgr ctxt consts; - val constss = Graph.strong_conn eqngr; - val mapping = Symtab.empty |> fold (fn consts => fold (fn const => - Symtab.update (const, consts)) consts) constss; - fun succs consts = consts - |> maps (Graph.immediate_succs eqngr) - |> subtract (op =) consts - |> map (the o Symtab.lookup mapping) - |> distinct (op =); - val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; - fun namify consts = map (Code.string_of_const thy) consts - |> commas; - val graph = map (fn (consts, constss) => - { name = namify consts, ident = namify consts, directory = "", unfold = true, - path = "", parents = map namify constss, content = [] }) conn; - in Graph_Display.display_graph graph end; + val namify = commas o map (Code.string_of_const thy); + val gr = + code_depgr ctxt consts + |> Graph.map (fn c => fn _ => c) + |> join_strong_conn + |> Graph.map (fn _ => fn cs => Graph_Display.content_node (namify cs) []) + in Graph_Display.display_graph ([], gr) end; local