Re: [isabelle] RC-1 – ad 8bd5999133d4 – »code_deps needs cycles«



Am 22.04.2015 um 15:46 schrieb Makarius:
> On Tue, 21 Apr 2015, Florian Haftmann wrote:
> 
>> This should not be the case.  Have you an example at hand where this did
>> fail with the new graph browser?
> 
> code_deps List.map

The problem should be resolved by the first attached patch.  The old
graph browser by accident accepted (and effectively ignored) recursive
dependencies.

The second patch adda actual content to the nodes.

I am a little uncertain how critical these patches are for the upcoming
release.  The fact that code_deps seems to be used rarely is both an
argument for as well as against including them.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent 6640d2ddf6de95c57d8e3c59a51135bbe22b374d
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
clarified

diff -r 6640d2ddf6de src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Apr 23 22:40:41 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun Apr 26 11:35:07 2015 +0200
@@ -924,16 +924,18 @@
 
 fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
 
-fun join_strong_conn gr =
+fun coalesce_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;
+    val xss_ys = map (fn xs => (xs, commas xs)) xss;
+    val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys);
+    fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs
+      |> subtract (op =) xs
+      |> map y_for
+      |> distinct (op =);
+    val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
   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
+    map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys
   end;
 
 fun code_deps ctxt consts =
@@ -943,10 +945,9 @@
   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_old
+    |> coalesce_strong_conn
+    |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps))
+    |> Graph_Display.display_graph
   end;
 
 local
# HG changeset patch
# Parent 93cc5c17433878ef212a68d309564da9c8df8fc9
code equations as displayable content in code dependency graph

diff -r 93cc5c174338 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Apr 26 11:35:07 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun Apr 26 17:12:42 2015 +0200
@@ -935,18 +935,21 @@
       |> distinct (op =);
     val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
   in
-    map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys
+    map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys
   end;
 
 fun code_deps ctxt consts =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val namify = commas o map (Code.string_of_const thy);
+    fun mk_entry ((name, consts), (ps, deps)) =
+      let
+        val label = commas (map (Code.string_of_const thy) consts);
+      in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end;
   in
     code_depgr ctxt consts
-    |> Graph.map (fn c => fn _ => c)
+    |> Graph.map (K (Code.pretty_cert thy o snd))
     |> coalesce_strong_conn
-    |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps))
+    |> map mk_entry
     |> Graph_Display.display_graph
   end;
 

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.