]> matita.cs.unibo.it Git - helm.git/commitdiff
ranking hopefully fixed
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Dec 2008 20:37:27 +0000 (20:37 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Dec 2008 20:37:27 +0000 (20:37 +0000)
helm/software/components/cic/cicUniv.ml

index 3074f2a78778143141bcb79dd516df2f69af1110..fc01328ab1d0fbdfbc697372fa1e6f4685e00849 100644 (file)
@@ -484,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