X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercGraph.ml;h=40d6281252c58de143736f3e6aaaa9248c13d570;hb=5c21228da6a5c6e09789788ae82b3c3317cd6149;hp=62a89b0a71ea36ed8b5ad3b48912a1c7af8616a9;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index 62a89b0a7..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
@@ -38,34 +38,56 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
+  let arity_of con =
+    try
+      let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+      let rec count_pi = function
+        | Cic.Prod (_,_,t) -> 1 + count_pi t
+        | _ -> 0
+      in
+      count_pi ty
+    with Invalid_argument _ -> assert false (* all coercions have an uri *)
+  in
+  let rec mk_implicits = function
+    | 0 -> [] 
+    | n -> Cic.Implicit None :: mk_implicits (n-1)
+  in
   try 
     let l = 
       CoercDb.find_coercion 
-        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
+        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
+    let uri =
+     match l with
+     | [] -> 
+         debug_print 
+           (lazy 
+             (sprintf ":-( coercion non trovata da %s a %s" 
+               (CoercDb.name_of_carr src) 
+               (CoercDb.name_of_carr tgt)));
+         None
+     | _::_ -> 
+         debug_print (lazy (
+           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
+             (List.length l)
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)));
+         Some l
     in
-    match l with
-    | [] -> 
-        debug_print 
-          (lazy 
-            (sprintf ":-( coercion non trovata da %s a %s" 
-              (CoercDb.name_of_carr src) 
-              (CoercDb.name_of_carr tgt)));
-        NoCoercion
-    | [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)));
-        SomeCoercion (CicUtil.term_of_uri u)
-    | u::_ -> 
-        debug_print (lazy (
-          sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
-            (List.length l)
-            (CoercDb.name_of_carr src) 
-            (CoercDb.name_of_carr tgt)
-            (UriManager.name_of_uri u)));
-        SomeCoercion (CicUtil.term_of_uri u)
+     (match uri with
+         None -> NoCoercion
+       | 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 newtl)
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -95,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 *)