for graph display, prefer graph data structure over list with dependencies;
authorwenzelm
Wed Dec 31 14:15:52 2014 +0100 (2014-12-31)
changeset 592082486d625878b
parent 59207 6b030dc97a4f
child 59209 8521841f277b
for graph display, prefer graph data structure over list with dependencies;
pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes
src/Pure/General/graph_display.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/present.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/thm_deps.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:13:11 2014 +0100
     1.2 +++ b/src/Pure/General/graph_display.ML	Wed Dec 31 14:15:52 2014 +0100
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  signature GRAPH_DISPLAY =
     1.6  sig
     1.7 -  type node =
     1.8 -   {name: string, ident: string, directory: string, unfold: bool,
     1.9 -    path: string, parents: string list, content: Pretty.T list}
    1.10 -  type graph = node list
    1.11 +  type node
    1.12 +  val content_node: string -> Pretty.T list -> node
    1.13 +  val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
    1.14 +  type graph = string list * node Graph.T
    1.15    val write_graph_browser: Path.T -> graph -> unit
    1.16    val browserN: string
    1.17    val graphviewN: string
    1.18 @@ -20,13 +20,19 @@
    1.19  structure Graph_Display: GRAPH_DISPLAY =
    1.20  struct
    1.21  
    1.22 -(* external graph representation *)
    1.23 +(* abstract graph representation *)
    1.24 +
    1.25 +type node = {name: string, content: Pretty.T list,
    1.26 +  unfold: bool, directory: string, path: string};
    1.27  
    1.28 -type node =
    1.29 - {name: string, ident: string, directory: string, unfold: bool,
    1.30 -  path: string, parents: string list, content: Pretty.T list};
    1.31 +type graph = string list * node Graph.T;
    1.32 +  (*partial explicit order in left argument*)
    1.33  
    1.34 -type graph = node list;
    1.35 +fun content_node name content =
    1.36 +  {name = name, content = content, unfold = true, directory = "", path = ""};
    1.37 +
    1.38 +fun session_node {name: string, unfold: bool, directory: string, path: string} =
    1.39 +  {name = name, content = [], unfold = unfold, directory = directory, path = path};
    1.40  
    1.41  
    1.42  (* print modes *)
    1.43 @@ -43,20 +49,21 @@
    1.44  
    1.45  (* encode graph *)
    1.46  
    1.47 -fun encode_browser (graph: graph) =
    1.48 -  cat_lines (map (fn {name, ident, directory, unfold, path, parents, ...} =>
    1.49 -    "\"" ^ name ^ "\" \"" ^ ident ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
    1.50 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    1.51 +fun encode_browser ((keys, gr) : graph) =
    1.52 +  fold_rev (update (op =)) (Graph.keys gr) keys
    1.53 +  |> map (fn key => case Graph.get_node gr key of {name, unfold, content, directory, path} =>
    1.54 +    "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
    1.55 +    path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;")
    1.56 +  |> cat_lines;
    1.57  
    1.58  fun write_graph_browser path graph = File.write path (encode_browser graph);
    1.59  
    1.60  
    1.61  val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
    1.62  
    1.63 -fun encode_graphview (graph: graph) =
    1.64 -  Graph.empty
    1.65 -  |> fold (fn {ident, name, content, ...} => Graph.new_node (ident, (name, content))) graph
    1.66 -  |> fold (fn {ident = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.67 +fun encode_graphview ((_, gr): graph) =
    1.68 +  gr
    1.69 +  |> Graph.map (fn _ => fn {name, content, ...} => (name, content))
    1.70    |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
    1.71  
    1.72  
    1.73 @@ -80,4 +87,3 @@
    1.74      in () end;
    1.75  
    1.76  end;
    1.77 -
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:15:52 2014 +0100
     2.3 @@ -275,25 +275,26 @@
     2.4      val thy = Toplevel.theory_of state;
     2.5      val thy_session = Present.session_name thy;
     2.6  
     2.7 -    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
     2.8 +    val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node =>
     2.9        let
    2.10          val name = Context.theory_name node;
    2.11          val parents = map Context.theory_name (Theory.parents_of node);
    2.12          val session = Present.session_name node;
    2.13          val unfold = (session = thy_session);
    2.14        in
    2.15 -       {name = name, ident = name, parents = parents, directory = session,
    2.16 -        unfold = unfold, path = "", content = []}
    2.17 +       ((name, Graph_Display.session_node
    2.18 +         {name = name, directory = session, unfold = unfold, path = ""}), parents)
    2.19        end);
    2.20 -  in Graph_Display.display_graph graph end);
    2.21 +  in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end);
    2.22  
    2.23  val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    2.24    let
    2.25      val thy = Toplevel.theory_of state;
    2.26 -    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    2.27 -     {name = Locale.extern thy name, ident = name, parents = parents,
    2.28 -      directory = "", unfold = true, path = "", content = [body]});
    2.29 -  in Graph_Display.display_graph graph end);
    2.30 +    val gr = Locale.pretty_locale_deps thy
    2.31 +      |> map (fn {name, parents, body} => ((name,
    2.32 +          Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    2.33 +      |> Graph.make;
    2.34 +  in Graph_Display.display_graph ([], gr) end);
    2.35  
    2.36  
    2.37  (* print theorems, terms, types etc. *)
     3.1 --- a/src/Pure/Thy/present.ML	Wed Dec 31 14:13:11 2014 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:15:52 2014 +0100
     3.3 @@ -76,6 +76,9 @@
     3.4    end;
     3.5  
     3.6  (*retrieve graph data from initial collection of theories*)
     3.7 +type browser_node = {name: string, ident: string, parents: string list,
     3.8 +  unfold: bool, directory: string, path: string}
     3.9 +
    3.10  fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
    3.11    let
    3.12      val {chapter, name = session_name} = Browser_Info.get thy;
    3.13 @@ -84,18 +87,17 @@
    3.14        (case theory_link (curr_chapter, curr_session) thy of
    3.15          NONE => ""
    3.16        | SOME p => Path.implode p);
    3.17 -    val entry =
    3.18 +    val graph_entry =
    3.19       {name = thy_name,
    3.20        ident = ID_of [chapter, session_name] thy_name,
    3.21        directory = session_name,
    3.22        path = path,
    3.23        unfold = false,
    3.24 -      parents = map ID_of_thy (Theory.parents_of thy),
    3.25 -      content = []};
    3.26 -  in (0, entry) end);
    3.27 +      parents = map ID_of_thy (Theory.parents_of thy)};
    3.28 +  in (0, graph_entry) end);
    3.29  
    3.30 -fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) =
    3.31 -  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr;
    3.32 +fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) =
    3.33 +  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph;
    3.34  
    3.35  
    3.36  
    3.37 @@ -118,7 +120,7 @@
    3.38   {theories: theory_info Symtab.table,
    3.39    tex_index: (int * string) list,
    3.40    html_index: (int * string) list,
    3.41 -  graph: (int * Graph_Display.node) list};
    3.42 +  graph: (int * browser_node) list};
    3.43  
    3.44  fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
    3.45    {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
    3.46 @@ -276,6 +278,14 @@
    3.47  
    3.48  (* finish session -- output all generated text *)
    3.49  
    3.50 +fun finalize_graph (nodes : (int * browser_node) list) =
    3.51 +  nodes
    3.52 +  |> map (fn (_, {ident, parents, name, unfold, directory, path}) =>
    3.53 +      ((ident, Graph_Display.session_node
    3.54 +        {name = name, unfold = unfold, directory = directory, path = path}), parents))
    3.55 +  |> Graph.make
    3.56 +  |> pair (map (#ident o snd) (sort (int_ord o apply2 fst) (rev nodes)));
    3.57 +
    3.58  fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
    3.59  fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
    3.60  
    3.61 @@ -298,10 +308,10 @@
    3.62      fun finish_html (a, {html_source, ...}: theory_info) =
    3.63        File.write (Path.append session_prefix (html_path a)) html_source;
    3.64  
    3.65 -    val sorted_graph = sorted_index graph;
    3.66 +    val graph' = finalize_graph graph;
    3.67      val opt_graphs =
    3.68        if doc_graph andalso not (null documents) then
    3.69 -        SOME (isabelle_browser sorted_graph)
    3.70 +        SOME (isabelle_browser graph')
    3.71        else NONE;
    3.72  
    3.73      val _ =
    3.74 @@ -310,7 +320,7 @@
    3.75          File.write_buffer (Path.append session_prefix index_path)
    3.76            (index_buffer html_index |> Buffer.add HTML.end_document);
    3.77          (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
    3.78 -        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
    3.79 +        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) graph';
    3.80          Isabelle_System.isabelle_tool "browser" "-b";
    3.81          Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    3.82          List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
    3.83 @@ -387,8 +397,7 @@
    3.84          directory = session_name,
    3.85          unfold = true,
    3.86          path = Path.implode (html_path name),
    3.87 -        parents = map ID_of_thy parents,
    3.88 -        content = []};
    3.89 +        parents = map ID_of_thy parents};
    3.90      in
    3.91        init_theory_info name (make_theory_info ("", html_source));
    3.92        add_graph_entry (update_time, graph_entry);
     4.1 --- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:13:11 2014 +0100
     4.2 +++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:15:52 2014 +0100
     4.3 @@ -24,14 +24,11 @@
     4.4        SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
     4.5      val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
     4.6        (le_super andf sub_le) (K NONE) original_algebra;
     4.7 -    val classes = Sorts.classes_of algebra;
     4.8 -    fun entry (c, (i, (_, cs))) =
     4.9 -      (i, {name = Name_Space.extern ctxt space c, ident = c, parents = Graph.Keys.dest cs,
    4.10 -            directory = "", unfold = true, path = "", content = []});
    4.11 -    val graph =
    4.12 -      Graph.fold (cons o entry) classes []
    4.13 -      |> sort (int_ord o apply2 #1) |> map #2;
    4.14 -  in Graph_Display.display_graph graph end;
    4.15 +    val gr =
    4.16 +      Sorts.classes_of algebra
    4.17 +      |> Graph.map (fn c => fn _ =>
    4.18 +        Graph_Display.content_node (Name_Space.extern ctxt space c) [])
    4.19 +  in Graph_Display.display_graph ([], gr) end;
    4.20  
    4.21  val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
    4.22  val visualize_cmd = gen_visualize Syntax.read_sort;
     5.1 --- a/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:13:11 2014 +0100
     5.2 +++ b/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:15:52 2014 +0100
     5.3 @@ -31,18 +31,15 @@
     5.4                        | session => [session])
     5.5                    | NONE => [])
     5.6                 | _ => ["global"]);
     5.7 +            val directory = space_implode "/" (session @ prefix);
     5.8              val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
     5.9 -            val entry =
    5.10 -              {name = Long_Name.base_name name,
    5.11 -               ident = name,
    5.12 -               directory = space_implode "/" (session @ prefix),
    5.13 -               unfold = false,
    5.14 -               path = "",
    5.15 -               parents = parents,
    5.16 -               content = []};
    5.17 -          in cons entry end;
    5.18 -    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    5.19 -  in Graph_Display.display_graph (sort_wrt #ident deps) end;
    5.20 +          in
    5.21 +            cons ((name, Graph_Display.session_node
    5.22 +              {name = Long_Name.base_name name, directory = directory,
    5.23 +                unfold = false, path = ""}), parents)
    5.24 +          end;
    5.25 +    val gr = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    5.26 +  in Graph_Display.display_graph (sort_wrt I (map (fst o fst) gr), Graph.make gr) end;
    5.27  
    5.28  val _ =
    5.29    Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
     6.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:13:11 2014 +0100
     6.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:15:52 2014 +0100
     6.3 @@ -911,25 +911,28 @@
     6.4  
     6.5  fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
     6.6  
     6.7 +fun join_strong_conn gr =
     6.8 +  let
     6.9 +    val xss = Graph.strong_conn gr;
    6.10 +    val xss_zs = map (fn xs => (xs, commas xs)) xss;
    6.11 +    val z_for = the o AList.lookup (op =) (maps (fn (xs, z) => map (fn x => (x, z)) xs) xss_zs);
    6.12 +    val succs = map (fn (xs, z) => (z, (map z_for o maps (Graph.immediate_succs gr)) xs)) xss_zs;
    6.13 +  in
    6.14 +    Graph.empty
    6.15 +    |> fold (fn (xs, z) => Graph.new_node (z, map (Graph.get_node gr) xs)) xss_zs
    6.16 +    |> fold (fn (z, succs) => fold (fn w => Graph.add_edge (z, w)) succs) succs
    6.17 +  end;
    6.18 +
    6.19  fun code_deps ctxt consts =
    6.20    let
    6.21      val thy = Proof_Context.theory_of ctxt;
    6.22 -    val eqngr = code_depgr ctxt consts;
    6.23 -    val constss = Graph.strong_conn eqngr;
    6.24 -    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
    6.25 -      Symtab.update (const, consts)) consts) constss;
    6.26 -    fun succs consts = consts
    6.27 -      |> maps (Graph.immediate_succs eqngr)
    6.28 -      |> subtract (op =) consts
    6.29 -      |> map (the o Symtab.lookup mapping)
    6.30 -      |> distinct (op =);
    6.31 -    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
    6.32 -    fun namify consts = map (Code.string_of_const thy) consts
    6.33 -      |> commas;
    6.34 -    val graph = map (fn (consts, constss) =>
    6.35 -      { name = namify consts, ident = namify consts, directory = "", unfold = true,
    6.36 -        path = "", parents = map namify constss, content = [] }) conn;
    6.37 -  in Graph_Display.display_graph graph end;
    6.38 +    val namify = commas o map (Code.string_of_const thy);
    6.39 +    val gr =
    6.40 +      code_depgr ctxt consts
    6.41 +      |> Graph.map (fn c => fn _ => c)
    6.42 +      |> join_strong_conn 
    6.43 +      |> Graph.map (fn _ => fn cs => Graph_Display.content_node (namify cs) [])
    6.44 +  in Graph_Display.display_graph ([], gr) end;
    6.45  
    6.46  local
    6.47