From: Stefano Zacchiroli 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 +