X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=9dfd6613d458016f25f0b520bd488f461acfe4e7;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=17301e4d6bb4cbb81ef8498a3ccf69e6daf37c93;hpb=e79fd328fe626dbd8c76183c36f721119e9fb668;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 17301e4d6..9dfd6613d 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -136,7 +136,7 @@ let source_of t =
 ;;
 
 let generate_dot_file () =
-  let l = CoercDb.to_list () in
+  let l = CoercDb.to_list (CoercDb.dump ()) in
   let module Pp = GraphvizPp.Dot in
   let buf = Buffer.create 10240 in
   let fmt = Format.formatter_of_buffer buf in
@@ -263,7 +263,7 @@ let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
 
 (* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_to carr = 
-  let l = CoercDb.to_list () in
+  let l = CoercDb.to_list (CoercDb.dump ()) in
   let splat_coercion_to carr (src,tgt,cl) =
     if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
   in
@@ -273,7 +273,7 @@ let get_coercions_to carr =
 
 (* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_from carr = 
-  let l = CoercDb.to_list () in
+  let l = CoercDb.to_list (CoercDb.dump ()) in
   let splat_coercion_from carr (src,tgt,cl) =
     if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
   in
@@ -304,10 +304,16 @@ let lb (c,_,_) =
 
 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements 
  * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
-let rec min acc = function
+let rec min acc skipped = function
   | c::tl -> 
-    if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
-  | [] -> acc
+    if List.exists (lb c) (tl@acc) 
+    then min acc (c::skipped) tl else min (c::acc) skipped tl
+  | [] -> acc, skipped
+;;
+
+
+let sort l = 
+  let low, high = min [] [] l in low @ high
 ;;
 
 let meets metasenv subst context (grow_left,left) (grow_right,right) =
@@ -321,12 +327,12 @@ let meets metasenv subst context (grow_left,left) (grow_right,right) =
   in
   List.map 
     (fun (c,uo1,uo2) -> 
-      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
+      let metasenv, uo1 = saturate metasenv uo1 in
+      let metasenv, uo2 = saturate metasenv uo2 in
       c,metasenv, uo1, uo2)
-    (min [] (intersect (grow left) (grow right)))
+    (sort (intersect 
+      (if grow_left then grow left else [left,None]) 
+      (if grow_right then grow right else [right,None])))
 ;;
 
 (* EOF *)