More commands documented.

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

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index 62a89b0a71ea36ed8b5ad3b48912a1c7af8616a9..6d7a670efc688d641f2927ce62e03af1600f6076 100644 (file)
--- 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
@@ -104,10 +126,14 @@ let generate_dot_file () =
   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 
+    (fun acc (src,tgt,cl) -> 
+      List.fold_left 
+        (fun acc c ->
+          acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
+          CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
+          "\"];\n")
+        acc cl)
+      "" l 
   in
   preamble ^ data ^ conclusion