improved coercions support:

[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 06d7a12d3ea3a5e250ae595dc747d906e75b0857..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
@@ -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
@@ -131,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