filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
authorwenzelm
Mon Apr 27 15:53:11 2015 +0200 (2015-04-27)
changeset 60203add72fdadd0b
parent 60202 a95023a21725
child 60204 137b3fc46bb3
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
clarified
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sat Apr 25 20:49:26 2015 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 27 15:53:11 2015 +0200
     1.3 @@ -924,16 +924,18 @@
     1.4  
     1.5  fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
     1.6  
     1.7 -fun join_strong_conn gr =
     1.8 +fun coalesce_strong_conn gr =
     1.9    let
    1.10      val xss = Graph.strong_conn gr;
    1.11 -    val xss_zs = map (fn xs => (xs, commas xs)) xss;
    1.12 -    val z_for = the o AList.lookup (op =) (maps (fn (xs, z) => map (fn x => (x, z)) xs) xss_zs);
    1.13 -    val succs = map (fn (xs, z) => (z, (map z_for o maps (Graph.immediate_succs gr)) xs)) xss_zs;
    1.14 +    val xss_ys = map (fn xs => (xs, commas xs)) xss;
    1.15 +    val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys);
    1.16 +    fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs
    1.17 +      |> subtract (op =) xs
    1.18 +      |> map y_for
    1.19 +      |> distinct (op =);
    1.20 +    val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
    1.21    in
    1.22 -    Graph.empty
    1.23 -    |> fold (fn (xs, z) => Graph.new_node (z, map (Graph.get_node gr) xs)) xss_zs
    1.24 -    |> fold (fn (z, succs) => fold (fn w => Graph.add_edge (z, w)) succs) succs
    1.25 +    map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys
    1.26    end;
    1.27  
    1.28  fun code_deps ctxt consts =
    1.29 @@ -943,10 +945,9 @@
    1.30    in
    1.31      code_depgr ctxt consts
    1.32      |> Graph.map (fn c => fn _ => c)
    1.33 -    |> join_strong_conn
    1.34 -    |> Graph.dest
    1.35 -    |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
    1.36 -    |> Graph_Display.display_graph_old
    1.37 +    |> coalesce_strong_conn
    1.38 +    |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps))
    1.39 +    |> Graph_Display.display_graph
    1.40    end;
    1.41  
    1.42  local