X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=58dc5cd6cfc82af8641150ba34168d5281716f4a;hb=281f0c7b4fc0d5b97025625af2ecff85edebbb5c;hp=03088410f59e3804a3ad527581fb8baef8f19751;hpb=25bc159057b95f144495872b55115a1762561d69;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 03088410f..58dc5cd6c 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -317,7 +317,7 @@ let error arc node1 closure_type node2 closure =
      "   of\n" ^ 
      "\t" ^ (string_of_universe node2) ^ "\n\n" ^
      "  ===== Universe Inconsistency detected =====\n") in
-  prerr_endline (Lazy.force s);
+(*   prerr_endline (Lazy.force s); *)
   raise (UniverseInconsistency s)
 
 
@@ -357,6 +357,8 @@ type universe_graph = bag * UriManager.UriSet.t * bool
 
 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph   
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)
@@ -482,27 +484,23 @@ let do_rank (b,_,_) =
        b SOF.empty 
    in
    let keys = SOF.elements keys in
-   let fall =
-     List.fold_left 
-       (fun acc u ->
-         let rec aux k seen = function
-           | [] -> 0, seen
-           | x::tl when SOF.mem x seen -> aux k seen tl
-           | x::tl ->
-               let seen = SOF.add x seen in
-               let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
-               let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in
-               let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
-               let t4, seen = aux k seen tl in
-               max (max t1 t2) 
-                 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
-               seen 
-         in
-         let rank, _ = aux 0 SOF.empty [u] in
-         MAL.add u rank acc) 
-       MAL.empty
+   let rec aux cache l =
+      match l with
+      | [] -> -1,cache
+      | x::tl when List.mem_assoc x cache ->
+          let height = List.assoc x cache in
+          let rest, cache = aux cache tl in
+          max rest height, cache
+      | x::tl -> 
+          let sons = SOF.elements (repr x b).gt_closure in
+          let height,cache = aux cache sons in
+          let height = height + 1 in
+          let cache = (x,height) :: cache in
+          let rest, cache = aux cache tl in
+          max height rest, cache
    in
-   rank := fall keys;
+   let _, cache = aux [] keys in
+   rank := List.fold_left (fun m (k,v) -> MAL.add k v m) MAL.empty cache;
    let res = ref [] in
    let resk = ref [] in
    MAL.iter