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 cd958a8f62074aa5ba4ac76fb023043b2478587e..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
@@ -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
@@ -94,4 +116,35 @@ let target_of t =
     CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
   with Invalid_argument _ -> assert false (* t must be a coercion *)
     
+let generate_dot_file () =
+  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 =
+    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,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
+  
 (* EOF *)