X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercGraph.ml;h=40d6281252c58de143736f3e6aaaa9248c13d570;hb=0d1ecc789c6d57a3eef47a028634d316905ef317;hp=06d7a12d3ea3a5e250ae595dc747d906e75b0857;hpb=d0bbef82f6258816b9a500a453813c1739c43806;p=helm.git

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index 06d7a12d3..40d628125 100644
--- a/helm/software/components/library/coercGraph.ml
+++ b/helm/software/components/library/coercGraph.ml
@@ -28,7 +28,7 @@
 open Printf;;
 
 type coercion_search_result = 
-  | SomeCoercion of Cic.term
+  | SomeCoercion of Cic.term list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
@@ -65,34 +65,29 @@ let look_for_coercion src tgt =
                (CoercDb.name_of_carr src) 
                (CoercDb.name_of_carr tgt)));
          None
-     | [u] -> 
+     | _::_ -> 
          debug_print (lazy (
-           sprintf ":-) TROVATA 1 coercion da %s a %s: %s" 
-             (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)
-             (UriManager.name_of_uri u)));
-         Some u
-     | u::_ -> 
-         debug_print (lazy (
-           sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
              (List.length l)
              (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)
-             (UriManager.name_of_uri u)));
-         Some u
+             (CoercDb.name_of_carr tgt)));
+         Some l
     in
      (match uri with
          None -> NoCoercion
-       | Some u ->
-          let c = CicUtil.term_of_uri u in
-          let arity = arity_of c in
-          let args = mk_implicits (arity - 1) in
-          let newt =
-           match args with
-              [] -> c
-            | _ -> Cic.Appl (c::args)
+       | Some ul ->
+          let cl = List.map CicUtil.term_of_uri ul in
+          let arityl = List.map arity_of cl in
+          let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+          let newtl =
+            List.map2 
+              (fun args c -> 
+                match args with
+                |  [] -> c
+                | _ -> Cic.Appl (c::args))
+              argsl cl
           in
-           SomeCoercion newt)
+           SomeCoercion newtl)
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -122,20 +117,33 @@ 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 ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+    ~edge_attrs:["fontsize", "10"] fmt;
   let l = CoercDb.to_list () in
-  let preamble = "
-    digraph pippo {
-      node [fontsize=9, width=.4, height=.4];
-      edge [fontsize=10]; 
-      \n" 
-  in
-  let conclusion = " } \n" in
-  let data = List.fold_left 
-    (fun acc (src,tgt,c) -> 
-      acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
-      CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
-      "\"];\n") "" l 
-  in
-  preamble ^ data ^ conclusion
-  
+  let pp_description carr =
+    match CoercDb.uri_of_carr carr with
+    | None -> ()
+    | Some uri ->
+        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 *)