many changes regarding coercions:

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

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 2fa2c4b0c5ca4ba216534de62d26cbebb9e02bcd..0b0db09d9b26153f7905909a26766955bc0404f6 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -91,7 +91,13 @@ let look_for_coercion_carr metasenv subst context src tgt =
   else
     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 && 
+          match t, tgt with
+          | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop 
+          | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set 
+          | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true
+          | _ -> CoercDb.eq_carr t tgt) 
     in
     pp_l "precise" l;
      (match l with
@@ -130,12 +136,37 @@ let source_of t =
 ;;
 
 let generate_dot_file () =
+  let l = CoercDb.to_list () in
   let module Pp = GraphvizPp.Dot in
   let buf = Buffer.create 10240 in
   let fmt = Format.formatter_of_buffer buf in
   Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
     ~edge_attrs:["fontsize", "10"] fmt;
-  let l = CoercDb.to_list () in
+  if 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\" >
+         <TR><TD BGCOLOR=\"gray95\">Source</TD>
+         <TD BGCOLOR=\"gray95\">Target</TD>
+         <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
+       String.concat "</TR>"   
+         (List.map 
+           (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
+            "<TR><TD>"  ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
+              String.concat "," 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 ->
@@ -166,20 +197,6 @@ let generate_dot_file () =
   Buffer.contents buf
 ;;
     
-let is_composite t =
-  try
-    let uri = 
-      match t with 
-      | Cic.Appl (he::_) -> CicUtil.uri_of_term he
-      | _ -> CicUtil.uri_of_term t
-    in
-    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
-    | Cic.Constant (_,_, _, _, attrs),_  ->
-        List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
-    | _ -> false
-  with Invalid_argument _ -> false
-;;
-
 let coerced_arg l =
   match l with
   | [] | [_] -> None
@@ -259,7 +276,7 @@ let rec min acc = function
   | [] -> acc
 ;;
 
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
   let saturate metasenv uo =
     match uo with 
     | None -> metasenv, None
@@ -270,8 +287,10 @@ let meets metasenv subst context left right =
   in
   List.map 
     (fun (c,uo1,uo2) -> 
-      let metasenv, uo1 = saturate metasenv uo1 in
-      let metasenv, uo2 = saturate metasenv uo2 in
+      let metasenv, uo1 = 
+        if grow_left then saturate metasenv uo1 else metasenv, None in
+      let metasenv, uo2 = 
+        if grow_right then saturate metasenv uo2 else metasenv, None in
       c,metasenv, uo1, uo2)
     (min [] (intersect (grow left) (grow right)))
 ;;