generate dot files with attributes on nodes (instead of only edges), and added genera...

[helm.git] / components / library / coercGraph.ml

diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml
index 06d7a12d3ea3a5e250ae595dc747d906e75b0857..d3adfdb5f6566dcb1156ce7f26be64cf664d5a11 100644 (file)
--- a/components/library/coercGraph.ml
+++ b/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
@@ -124,17 +119,31 @@ let target_of t =
 let generate_dot_file () =
   let l = CoercDb.to_list () in
   let preamble = "
-    digraph pippo {
+    digraph g {
       node [fontsize=9, width=.4, height=.4];
       edge [fontsize=10]; 
       \n" 
   in
   let conclusion = " } \n" in
+  let node_dsc carr =
+    match CoercDb.uri_of_carr carr with
+    | 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,c) -> 
-      acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
-      CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
-      "\"];\n") "" l 
+    (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