From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 13 Jul 2006 09:39:51 +0000 (+0000)
Subject: use the graphviz pretty printer to generate graphviz markup for the coercions graph
X-Git-Tag: 0.4.95@7852~1206
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=619389e0395c49045cd5e1eb97099fb2c87b139d;p=helm.git

use the graphviz pretty printer to generate graphviz markup for the coercions graph
---

diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml
index d3adfdb5f..6f31cbd46 100644
--- a/components/library/coercGraph.ml
+++ b/components/library/coercGraph.ml
@@ -117,34 +117,34 @@ let target_of t =
   with Invalid_argument _ -> assert false (* t must be a coercion *)
     
 let generate_dot_file () =
+  let module Pp = GraphvizPp.Dot in
+  let buf = Buffer.create 10240 in
+  let fmt = Format.formatter_of_buffer buf in
+  Pp.header fmt;
+  Pp.node "node" ~attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] fmt;
+  Pp.node "edge" ~attrs:["fontsize", "10"] fmt;
   let l = CoercDb.to_list () in
-  let preamble = "
-    digraph g {
-      node [fontsize=9, width=.4, height=.4];
-      edge [fontsize=10]; 
-      \n" 
-  in
-  let conclusion = " } \n" in
-  let node_dsc carr =
+  let pp_description carr =
     match CoercDb.uri_of_carr carr with
-    | None -> ""
+    | None -> ()
     | Some uri ->
-        sprintf "%s [href=\"%s\"]"
-          (CoercDb.name_of_carr carr) (UriManager.string_of_uri uri) in
-  let data = List.fold_left 
-    (fun acc (src,tgt,cl) -> 
-      List.fold_left 
-        (fun acc c ->
-          let src_name = CoercDb.name_of_carr src in
-          let tgt_name = CoercDb.name_of_carr tgt in
-          acc ^ src_name ^ " -> "
-            ^ tgt_name ^ " [label=\"" ^ UriManager.name_of_uri c
-            ^ "\",href=\"" ^ UriManager.string_of_uri c
-            ^ "\"];\n"
-            ^ node_dsc src ^ node_dsc tgt)
-        acc cl)
-      "" l 
-  in
-  preamble ^ data ^ conclusion
-  
+        Pp.node (CoercDb.name_of_carr carr)
+          ~attrs:["href", UriManager.string_of_uri uri] fmt in
+  List.iter
+    (fun (src, tgt, cl) ->
+      let src_name = CoercDb.name_of_carr src in
+      let tgt_name = CoercDb.name_of_carr tgt in
+      pp_description src;
+      pp_description tgt;
+      List.iter
+        (fun c ->
+          Pp.edge src_name tgt_name
+            ~attrs:[ "label", UriManager.name_of_uri c;
+              "href", UriManager.string_of_uri c ]
+            fmt)
+        cl)
+    l;
+  Pp.trailer fmt;
+  Buffer.contents buf
+
 (* EOF *)
diff --git a/components/library/coercGraph.mli b/components/library/coercGraph.mli
index 691bafd4c..986ef8e47 100644
--- a/components/library/coercGraph.mli
+++ b/components/library/coercGraph.mli
@@ -39,3 +39,4 @@ val source_of: Cic.term -> Cic.term
 val target_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
+