parameter sintax added to axiom statement

[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 3074f2a78778143141bcb79dd516df2f69af1110..58dc5cd6cfc82af8641150ba34168d5281716f4a 100644 (file)
--- 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)
 
 
@@ -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