From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 19 Apr 2008 16:27:28 +0000 (+0000)
Subject: ranking function fixed: when graphs are collapsed one step links are not updated... 
X-Git-Tag: make_still_working~5313
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ed731db1107673f11de9b56a376bee41b4cf0be;p=helm.git

ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk)
thus you can not rely on them, just use the closures!
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 699af7847..2bfbc92a3 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -595,26 +595,27 @@ let add_eq ?fast u v b =
 (* ugly *)
 let rank = ref MAL.empty;;
 
-let do_rank (b,_,_) =
-  
+let do_rank (b,_,_ as ugraph) =
+(*         print_ugraph ugraph; *)
    let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
    let fall =
      List.fold_left 
        (fun acc u ->
-         let rec aux seen = function
+         let rec aux k seen = function
            | [] -> 0, seen
-           | x::tl when SOF.mem x seen -> aux seen tl
+           | x::tl when SOF.mem x seen -> aux k seen tl
            | x::tl ->
+(*                prerr_endline (String.make k '.' ^ string_of_universe x); *)
                let seen = SOF.add x seen in
-               let t1, seen = aux seen (SOF.elements (repr x b).one_s_eq) in
-               let t2, seen = aux seen (SOF.elements (repr x b).one_s_ge) in
-               let t3, seen = aux seen (SOF.elements (repr x b).one_s_gt) in
-               let t4, seen = aux seen tl 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).one_s_gt then 0 else t3+1) t4),
+                 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
                seen 
          in
-         let rank, _ = aux SOF.empty [u] in
+         let rank, _ = aux 0 SOF.empty [u] in
          MAL.add u rank acc) 
        MAL.empty
    in