ported the instantiate-left-params-to-calculate-rec-args patch from the old to the...

[helm.git] / helm / software / components / cic / cicUniv.ml

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index fe9f01d532af2c65866fb1b9a34d6cf223ed76dd..8570c0c15c28f4a11f7818fca9d78a0076251538 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -47,18 +47,28 @@ open Printf
 (*****************************************************************************)
 
 type universe = int * UriManager.uri option 
-    
+
+let eq u1 u2 = 
+  match u1,u2 with
+  | (id1, Some uri1),(id2, Some uri2) -> 
+      id1 = id2 && UriManager.eq uri1 uri2
+  | (id1, None),(id2, None) -> id1 = id2
+  | _ -> false
+  
+let compare (id1, uri1) (id2, uri2) = 
+  let cmp = id1 - id2 in
+  if cmp = 0 then
+    match uri1,uri2 with
+    | None, None -> 0 
+    | Some _, None -> 1
+    | None, Some _ -> ~-1
+    | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+  else
+    cmp
+
 module UniverseType = struct
   type t = universe
-  let compare (n1,u1) (n2,u2) =
-   let ndiff = n1 - n2 in
-    if ndiff <> 0 then ndiff
-    else
-     match u1,u2 with
-        None, None -> 0
-      | Some u1, Some u2 -> UriManager.compare u1 u2
-      | None, Some _ -> 1
-      | Some _, None -> -1
+  let compare = compare
 end
   
 module SOF = Set.Make(UniverseType)
@@ -638,11 +648,11 @@ let rec clean_ugraph m already_contained f =
   let e_l = 
     MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
       begin
-      k::l end else l) m'' []
+      SOF.add k l end else l) m'' SOF.empty
   in
-    if e_l != [] then
+    if not (SOF.is_empty e_l) then
       clean_ugraph 
-        m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
+        m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
     else
       MAL.fold 
         (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
@@ -651,7 +661,8 @@ let rec clean_ugraph m already_contained f =
 
 let clean_ugraph (m,a,o) l =
   assert(not o);
-  let m, a = clean_ugraph m a (fun u -> List.mem u l) in
+  let l = List.fold_right SOF.add l SOF.empty in
+  let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
   m, a, o
 
 let assigner_of = 
@@ -915,24 +926,6 @@ let assert_univs_have_uri (graph,_,_) univlist =
   MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
   List.iter assert_univ univlist
   
-let eq u1 u2 = 
-  match u1,u2 with
-  | (id1, Some uri1),(id2, Some uri2) -> 
-      id1 = id2 && UriManager.eq uri1 uri2
-  | (id1, None),(id2, None) -> id1 = id2
-  | _ -> false
-  
-let compare (id1, uri1) (id2, uri2) = 
-  let cmp = id1 - id2 in
-  if cmp = 0 then
-    match uri1,uri2 with
-    | None, None -> 0 
-    | Some _, None -> 1
-    | None, Some _ -> ~-1
-    | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
-  else
-    cmp
-
 let is_anon = function (_,None) -> true | _ -> false
   
 (* EOF *)