# HG changeset patch # User wenzelm # Date 1420054965 -3600 # Node ID 8658b4290aedd593ba11495afb6ac12c77098c2f # Parent 8521841f277b950a7f263f8b890cca299bfd3f2b clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned; diff -r 8521841f277b -r 8658b4290aed src/Pure/General/graph_display.ML --- a/src/Pure/General/graph_display.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Pure/General/graph_display.ML Wed Dec 31 20:42:45 2014 +0100 @@ -9,7 +9,10 @@ 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 + type entry = (string * node) * string list + val eq_entry: entry * entry -> bool + type graph = entry list + val sort_graph: graph -> graph val write_graph_browser: Path.T -> graph -> unit val browserN: string val graphviewN: string @@ -20,19 +23,44 @@ structure Graph_Display: GRAPH_DISPLAY = struct -(* abstract graph representation *) +(* type node *) -type node = {name: string, content: Pretty.T list, - unfold: bool, directory: string, path: string}; - -type graph = string list * node Graph.T; - (*partial explicit order in left argument*) +datatype node = + Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string}; fun content_node name content = - {name = name, content = content, unfold = true, directory = "", path = ""}; + Node {name = name, content = content, unfold = true, directory = "", path = ""}; + +fun session_node {name, unfold, directory, path} = + Node {name = name, content = [], unfold = unfold, directory = directory, path = path}; + + +(* type graph *) + +type entry = (string * node) * string list; +val eq_entry: entry * entry -> bool = op = o apply2 (#1 o #1); + +type graph = entry list; + +structure Aux_Graph = + Graph(type key = string * string val ord = prod_ord string_ord string_ord); -fun session_node {name: string, unfold: bool, directory: string, path: string} = - {name = name, content = [], unfold = unfold, directory = directory, path = path}; +fun sort_graph (graph: graph) = + let + val ident_names = + fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident))) + graph Symtab.empty; + val the_key = the o Symtab.lookup ident_names; + val G = + Aux_Graph.empty + |> fold (fn ((ident, node), _) => Aux_Graph.new_node (the_key ident, node)) graph + |> fold (fn ((ident, _), parents) => + fold (fn parent => Aux_Graph.add_edge (the_key parent, the_key ident)) parents) graph + in + Aux_Graph.topological_order G |> map (fn key => + let val (_, (node, (preds, _))) = Aux_Graph.get_entry G key + in ((#2 key, node), map #2 (Aux_Graph.Keys.dest preds)) end) + end; (* print modes *) @@ -49,41 +77,43 @@ (* encode 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} => +val encode_browser = + map (fn ((key, Node {name, unfold, content, directory, path}), parents) => "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^ - path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;") - |> cat_lines; + path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") + #> cat_lines; -fun write_graph_browser path graph = File.write path (encode_browser graph); +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_node (Node {name, content, ...}) = + (name, content) |> + let open XML.Encode + in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end; -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; +val encode_graph = + let open XML.Encode in list (pair (pair string encode_node) (list string)) end; (* display graph *) -fun display_graph graph = - if print_mode_active active_graphN then - let - val (markup, body) = - if is_browser () then (Markup.browserN, encode_browser graph) - else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph)); - val ((bg1, bg2), en) = - YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); - in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end - else - let - val _ = writeln "Displaying graph ..."; - val path = Isabelle_System.create_tmp_path "graph" ""; - val _ = write_graph_browser path graph; - val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); - in () end; +val display_graph = + sort_graph #> (fn graph => + if print_mode_active active_graphN then + let + val (markup, body) = + if is_browser () then (Markup.browserN, encode_browser graph) + else (Markup.graphviewN, YXML.string_of_body (encode_graph graph)); + val ((bg1, bg2), en) = + YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); + in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end + else + let + val _ = writeln "Displaying graph ..."; + val path = Isabelle_System.create_tmp_path "graph" ""; + val _ = write_graph_browser path graph; + val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); + in () end); end; diff -r 8521841f277b -r 8658b4290aed src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Dec 31 20:42:45 2014 +0100 @@ -274,27 +274,29 @@ let val thy = Toplevel.theory_of state; val thy_session = Present.session_name thy; - - 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, Graph_Display.session_node - {name = name, directory = session, unfold = unfold, path = ""}), parents) - end); - in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end); + in + Theory.nodes_of thy + |> map (fn thy_node => + let + val name = Context.theory_name thy_node; + val parents = map Context.theory_name (Theory.parents_of thy_node); + val session = Present.session_name thy_node; + val node = + Graph_Display.session_node + {name = name, directory = session, unfold = session = thy_session, path = ""}; + in ((name, node), parents) end) + |> Graph_Display.display_graph + end); val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; - 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); + in + Locale.pretty_locale_deps thy + |> map (fn {name, parents, body} => + ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) + |> Graph_Display.display_graph + end); (* print theorems, terms, types etc. *) diff -r 8521841f277b -r 8658b4290aed src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Pure/Thy/present.ML Wed Dec 31 20:42:45 2014 +0100 @@ -75,29 +75,20 @@ else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link]) 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 => +fun init_graph_entry session thy = let - val {chapter, name = session_name} = Browser_Info.get thy; - val thy_name = Context.theory_name thy; - val path = - (case theory_link (curr_chapter, curr_session) thy of - NONE => "" - | SOME p => Path.implode p); - val graph_entry = - {name = thy_name, - ident = ident_of [chapter, session_name] thy_name, - directory = session_name, - path = path, - unfold = false, - parents = map ident_of_thy (Theory.parents_of thy)}; - in (0, graph_entry) end); - -fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) = - (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph; + val ident = ident_of_thy thy; + val parents = map ident_of_thy (Theory.parents_of thy); + val node = + Graph_Display.session_node + {name = Context.theory_name thy, + unfold = false, + directory = session_name thy, + path = + (case theory_link session thy of + NONE => "" + | SOME p => Path.implode p)}; + in ((ident, node), parents) end; @@ -120,7 +111,7 @@ {theories: theory_info Symtab.table, tex_index: (int * string) list, html_index: (int * string) list, - graph: (int * browser_node) list}; + graph: Graph_Display.graph}; fun make_browser_info (theories, tex_index, html_index, graph) : browser_info = {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph}; @@ -128,7 +119,7 @@ val empty_browser_info = make_browser_info (Symtab.empty, [], [], []); fun init_browser_info session thys = - make_browser_info (Symtab.empty, [], [], init_graph session thys); + make_browser_info (Symtab.empty, [], [], map (init_graph_entry session) thys); fun map_browser_info f {theories, tex_index, html_index, graph} = make_browser_info (f (theories, tex_index, html_index, graph)); @@ -161,7 +152,7 @@ fun add_graph_entry entry = change_browser_info (fn (theories, tex_index, html_index, graph) => - (theories, tex_index, html_index, ins_graph_entry entry graph)); + (theories, tex_index, html_index, update Graph_Display.eq_entry entry graph)); @@ -278,14 +269,6 @@ (* 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; @@ -308,10 +291,10 @@ fun finish_html (a, {html_source, ...}: theory_info) = File.write (Path.append session_prefix (html_path a)) html_source; - val graph' = finalize_graph graph; + val sorted_graph = Graph_Display.sort_graph graph; val opt_graphs = if doc_graph andalso not (null documents) then - SOME (isabelle_browser graph') + SOME (isabelle_browser sorted_graph) else NONE; val _ = @@ -320,7 +303,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) graph'; + Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_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) @@ -392,15 +375,16 @@ val html_source = HTML.theory name parent_specs (mk_text ()); val graph_entry = - {name = name, - ident = ident_of [chapter, session_name] name, - directory = session_name, - unfold = true, - path = Path.implode (html_path name), - parents = map ident_of_thy parents}; + ((ident_of [chapter, session_name] name, + Graph_Display.session_node + {name = name, + directory = session_name, + unfold = true, + path = Path.implode (html_path name)}), + map ident_of_thy parents); in init_theory_info name (make_theory_info ("", html_source)); - add_graph_entry (update_time, graph_entry); + add_graph_entry graph_entry; add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); add_tex_index (update_time, Latex.theory_entry name); Browser_Info.put {chapter = chapter, name = session_name} thy diff -r 8521841f277b -r 8658b4290aed src/Pure/Tools/class_deps.ML --- a/src/Pure/Tools/class_deps.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Pure/Tools/class_deps.ML Wed Dec 31 20:42:45 2014 +0100 @@ -6,11 +6,11 @@ signature CLASS_DEPS = sig - val visualize: Proof.context -> sort -> sort option -> unit - val visualize_cmd: Proof.context -> string -> string option -> unit + val class_deps: Proof.context -> sort -> sort option -> unit + val class_deps_cmd: Proof.context -> string -> string option -> unit end; -structure Class_deps: CLASS_DEPS = +structure Class_Deps: CLASS_DEPS = struct fun gen_visualize prep_sort ctxt raw_super raw_sub = @@ -19,23 +19,28 @@ val sub = Option.map (prep_sort ctxt) raw_sub; val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); fun le_super class = Sorts.sort_le original_algebra ([class], super); - val sub_le = case sub of - NONE => K true | - 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 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 sub_le = + (case sub of + NONE => K true + | 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; + in + Sorts.classes_of algebra + |> Graph.dest + |> map (fn ((c, _), ds) => + ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds)) + |> Graph_Display.display_graph + end; -val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); -val visualize_cmd = gen_visualize Syntax.read_sort; +val class_deps = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); +val class_deps_cmd = gen_visualize Syntax.read_sort; val _ = Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" - ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) => - ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub)))); + ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (super, sub) => + (Toplevel.unknown_theory o + Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub)))); end; diff -r 8521841f277b -r 8658b4290aed src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Pure/Tools/thm_deps.ML Wed Dec 31 20:42:45 2014 +0100 @@ -38,8 +38,10 @@ {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; + in + Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [] + |> Graph_Display.display_graph + end; val _ = Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies" diff -r 8521841f277b -r 8658b4290aed src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Dec 31 14:28:04 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Wed Dec 31 20:42:45 2014 +0100 @@ -927,12 +927,14 @@ let val thy = Proof_Context.theory_of ctxt; 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; + in + code_depgr ctxt consts + |> Graph.map (fn c => fn _ => c) + |> join_strong_conn + |> Graph.dest + |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds)) + |> Graph_Display.display_graph + end; local @@ -953,7 +955,7 @@ "visualize dependencies of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.unknown_context o - Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs))); + Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); end;