+(* ugly *)
+let rank = ref MAL.empty;;
+
+let do_rank (b,_,_) =
+
+ let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+ let fall =
+ List.fold_left
+ (fun acc u ->
+ let rec aux seen = function
+ | [] -> 0, seen
+ | x::tl when SOF.mem x seen -> aux seen tl
+ | x::tl ->
+ 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
+ max (max t1 t2)
+ (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4),
+ seen
+ in
+ let rank, _ = aux SOF.empty [u] in
+ MAL.add u rank acc)
+ MAL.empty
+ in
+ rank := fall keys;
+ MAL.iter
+ (fun k v ->
+ prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+;;
+
+let get_rank u =
+ try MAL.find u !rank
+ with Not_found -> 0
+ (* if the universe is not in the graph it means there are
+ * no contraints on it! thus it can be freely set to Type0 *)
+;;
+