Coercions graph is printed between real types and not approximated ones

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 0b0db09d9b26153f7905909a26766955bc0404f6..17301e4d6bb4cbb81ef8498a3ccf69e6daf37c93 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -142,7 +142,7 @@ let generate_dot_file () =
   let fmt = Format.formatter_of_buffer buf in
   Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
     ~edge_attrs:["fontsize", "10"] fmt;
-  if l <> [] then
+  if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
     Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
     color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n" 
        ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
@@ -154,41 +154,75 @@ let generate_dot_file () =
            (fun (src,tgt,ul) -> 
             let src_name = CoercDb.string_of_carr src in
             let tgt_name = CoercDb.string_of_carr tgt in
-            let names = List.map (fun (u,_,_) -> UriManager.name_of_uri u) ul in
+            let names = 
+              List.map (fun (u,_,_) -> 
+                UriManager.name_of_uri u ^ 
+                  (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+                  | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+                    when List.exists ((=) (`Flavour `Variant)) attrs -> "*"
+                  | _ -> "")
+              ) ul 
+            in
             "<TR><TD>"  ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
-              String.concat "," names ^ "</TD>")
+            String.concat ",&nbsp;" names ^ "</TD>")
          (List.sort (fun (x,y,_) (x1,y1,_) -> 
              let rc = compare x x1 in
              if rc = 0 then compare y y1 else rc) l))
        ^ "</TR></TABLE></FONT>")
-      (String.concat ";"
-        (List.flatten (List.map (fun (s,t,_) -> 
-            let src_name = CoercDb.string_of_carr s in
-            let tgt_name = CoercDb.string_of_carr t in
-            [ "\""^src_name^"\""; "\""^tgt_name^"\"" ]
-          ) l)));
-  let pp_description carr =
-    match carr with
-    | CoercDb.Uri uri ->
-        Pp.node (CoercDb.string_of_carr carr)
-          ~attrs:["href", UriManager.string_of_uri uri] fmt 
-    | _ -> ()
+       (String.concat ";" ["Type"]);
+  let type_uri u = 
+    let ty, _ = 
+      CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+      CicUniv.oblivion_ugraph
+    in
+      ty
+  in
+  let deref_coercion u =
+   match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+   | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+     when List.exists ((=) (`Flavour `Variant)) attrs ->
+       UriManager.name_of_uri u'
+   | Cic.Constant (_,Some t,_,_,_), _ when
+       let rec is_id = function 
+         | Cic.Lambda (_,_,t) -> is_id t
+         | Cic.Rel _ -> true
+         | _ -> false
+         in is_id t -> "ID"
+   | _ -> UriManager.name_of_uri u
   in
   List.iter
     (fun (src, tgt, ul) ->
-      let src_name = CoercDb.string_of_carr src in
-      let tgt_name = CoercDb.string_of_carr tgt in
-      pp_description src;
-      pp_description tgt;
       List.iter
-        (fun (u,saturations,_) ->
+        (fun (u,saturations,cpos) ->
+          let ty = type_uri u in
+          let src_name, tgt_name = 
+            let rec aux ctx cpos t =
+              match cpos, t with
+              | 0,Cic.Prod (_,src,tgt) ->
+                  CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx)
+              | 0,t -> CicPp.pp t ctx, Cic.Implicit None, []
+              | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt
+              | _ -> assert false
+            in
+            let ssrc, rest, ctx = aux [] cpos ty in
+            let stgt, rest, _ = aux ctx saturations rest in
+            let stgt = 
+              if rest <> Cic.Implicit None then
+                match tgt with 
+                | CoercDb.Fun _ -> CoercDb.string_of_carr tgt
+                | _ -> assert false
+              else
+                stgt
+            in
+            ssrc, stgt
+          in
+          Pp.node src_name fmt;
+          Pp.node tgt_name fmt;
           Pp.edge src_name tgt_name
             ~attrs:[ "label",
-                     (UriManager.name_of_uri u ^
-                      if saturations = 0 then
-                       ""
-                      else
-                       "(" ^ string_of_int saturations ^ ")");
+                 (deref_coercion u ^
+                  if saturations = 0 then ""
+                  else "(" ^ string_of_int saturations ^ ")");
               "href", UriManager.string_of_uri u ]
             fmt)
         ul)