From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 23 Jul 2008 11:41:37 +0000 (+0000)
Subject: better ranking interface
X-Git-Tag: make_still_working~4885
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=25bc159057b95f144495872b55115a1762561d69;p=helm.git

better ranking interface
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index cf6b6eeff..03088410f 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -504,11 +504,12 @@ let do_rank (b,_,_) =
    in
    rank := fall keys;
    let res = ref [] in
+   let resk = ref [] in
    MAL.iter 
      (fun k v -> 
-        if not (List.mem v !res) then res := v::!res;
-       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank;
-   !res 
+       if not (List.mem v !res) then res := v::!res;
+       resk := k :: !resk) !rank;
+   !res, !resk
 ;;
 
 let get_rank u = 
diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index b53e50691..fa7f544c0 100644
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -72,7 +72,7 @@ val add_ge:
 val add_gt: 
   universe -> universe -> universe_graph -> universe_graph
 
-val do_rank: universe_graph -> int list
+val do_rank: universe_graph -> int list * universe list
 val get_rank: universe -> int
 
 (*
diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index a51d97722..467d61147 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -142,7 +142,10 @@ let _ =
        try load_graph u with exn -> ())
     roots_alluris;
   prerr_endline "finished....";
-  let lll = List.sort compare (CicUniv.do_rank (get_graph ())) in
+  let lll,uuu = List.sort compare (CicUniv.do_rank (get_graph ())) in
+  List.iter (fun k -> 
+    prerr_endline (string_of_universe k ^ " = " ^ string_of_int (Cicuniv.get_rank k))) uuu
+    in
   let _ = 
     try
     let rec aux = function