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 c8a8660b3bade7c485670c89087291f5a222944d..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)
 
 
@@ -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)
@@ -474,33 +476,38 @@ let add_eq u v b =
 let rank = ref MAL.empty;;
 
 let do_rank (b,_,_) =
-(*         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 k seen = function
-           | [] -> 0, seen
-           | 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 (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 keys = 
+     MAL.fold 
+       (fun k v acc -> 
+          SOF.union acc (SOF.union (SOF.singleton k) 
+            (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
+       b SOF.empty 
    in
-   rank := fall keys;
+   let keys = SOF.elements keys in
+   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
+   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 
      (fun k v -> 
-       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+       if not (List.mem v !res) then res := v::!res;
+       resk := k :: !resk) !rank;
+   !res, !resk
 ;;
 
 let get_rank u =