Bug fixed in insertion of parametric coercions.

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

diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml
index cd958a8f62074aa5ba4ac76fb023043b2478587e..06d7a12d3ea3a5e250ae595dc747d906e75b0857 100644 (file)
--- a/components/library/coercGraph.ml
+++ b/components/library/coercGraph.ml
@@ -38,34 +38,61 @@ 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
+     | [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" 
+             (List.length l)
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)
+             (UriManager.name_of_uri u)));
+         Some u
     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 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)
+          in
+           SomeCoercion newt)
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -94,4 +121,21 @@ 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 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
+  
 (* EOF *)