let name_universe u uri =
match u with
| (i, None) -> (i, Some uri)
- | (i, Some ouri) when UriManager.eq ouri uri -> u
- | (i, Some ouri) ->
- (* inside obj living at uri 'uri' should live only
- * universes with uri None. Call Unshare.unshare ~fresh_univs:true
- * if you want to reuse a Type in another object *)
- prerr_endline ("Offending universe: " ^ string_of_universe u^
- " found inside object " ^ UriManager.string_of_uri uri);
- assert false
+ | u -> u
;;
let print_ugraph (g, _, o) =
let rank = ref MAL.empty;;
let do_rank (b,_,_) =
-(* print_ugraph ugraph; *)
- let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+ 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
+ let keys = SOF.elements keys in
let fall =
List.fold_left
(fun acc u ->
| [] -> 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
MAL.empty
in
rank := fall keys;
+ let res = 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;
+ prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank;
+ !res
;;
let get_rank u =
Xml.pp ~gzip:true tokens (Some filename)
let univno = fst
+let univuri = function
+ | _,None -> UriManager.uri_of_string "cic:/fake.con"
+ | _,Some u -> u
let rec clean_ugraph m already_contained f =