(** Types and default values **)
(*****************************************************************************)
+
type universe = int * UriManager.uri option
-
+
+let eq u1 u2 =
+ match u1,u2 with
+ | (id1, Some uri1),(id2, Some uri2) ->
+ id1 = id2 && UriManager.eq uri1 uri2
+ | (id1, None),(id2, None) -> id1 = id2
+ | _ -> false
+
+let compare (id1, uri1) (id2, uri2) =
+ let cmp = id1 - id2 in
+ if cmp = 0 then
+ match uri1,uri2 with
+ | None, None -> 0
+ | Some _, None -> 1
+ | None, Some _ -> ~-1
+ | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+ else
+ cmp
+
module UniverseType = struct
type t = universe
- let compare (n1,u1) (n2,u2) =
- let ndiff = n1 - n2 in
- if ndiff <> 0 then ndiff
- else
- match u1,u2 with
- None, None -> 0
- | Some u1, Some u2 -> UriManager.compare u1 u2
- | None, Some _ -> 1
- | Some _, None -> -1
+ let compare = compare
end
module SOF = Set.Make(UniverseType)
print_endline ("Aggiusto " ^ (string_of_universe u) ^
"e ottengo questa chiusura\n " ^ (string_of_node ru))
-and adjust_fast_aux u m =
+and adjust_fast_aux adjusted u m =
+ if SOF.mem u adjusted then m, adjusted else
+ let adjusted = SOF.add u adjusted in
let ru = repr u m in
let gt_c = closure_gt_fast ru m in
let ge_c = closure_ge_fast ru m in
(not (are_set_eq ge_c ru.ge_closure))
in
if ((not changed_gegt) && (not changed_eq)) then
- m
+ m, adjusted
else
begin
let ru' = {
one_s_gt = ru.one_s_gt}
in
let m = MAL.add u ru' m in
- let m =
- SOF.fold (fun x m -> adjust_fast_aux x m)
- (SOF.union ru'.eq_closure ru'.in_gegt_of) m
- (* TESI:
- ru'.in_gegt_of m
- *)
+ let m, adjusted =
+ SOF.fold (fun x (m,adjusted) -> MAL.add x ru' m, SOF.add x adjusted)
+ (SOF.diff ru'.eq_closure adjusted)
+ (m,adjusted)
+ in
+ let m, adjusted =
+ SOF.fold (fun x (m,adjusted) -> adjust_fast_aux adjusted x m)
+ (SOF.diff ru'.in_gegt_of adjusted)
+ (m,adjusted)
in
- m (*adjust_fast u m*)
+ m, adjusted
end
(*
and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
*)
-and adjust_fast x y = adjust_fast_aux x y
+and adjust_fast x y =
+ fst(adjust_fast_aux SOF.empty x y)
and add_gt_arc_fast u v m =
let ru = repr u m in
" 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)
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)
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 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
+ 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
- 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
(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 =
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 =
let e_l =
MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
begin
- k::l end else l) m'' []
+ SOF.add k l end else l) m'' SOF.empty
in
- if e_l != [] then
+ if not (SOF.is_empty e_l) then
clean_ugraph
- m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
+ m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
else
MAL.fold
(fun k v x -> if v <> empty_entry then MAL.add k v x else x)
let clean_ugraph (m,a,o) l =
assert(not o);
- let m, a = clean_ugraph m a (fun u -> List.mem u l) in
+ let l = List.fold_right SOF.add l SOF.empty in
+ let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
m, a, o
let assigner_of =
MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
List.iter assert_univ univlist
-let eq u1 u2 =
- match u1,u2 with
- | (id1, Some uri1),(id2, Some uri2) ->
- id1 = id2 && UriManager.eq uri1 uri2
- | (id1, None),(id2, None) -> id1 = id2
- | _ -> false
-
-let compare (id1, uri1) (id2, uri2) =
- let cmp = id1 - id2 in
- if cmp = 0 then
- match uri1,uri2 with
- | None, None -> 0
- | Some _, None -> 1
- | None, Some _ -> ~-1
- | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
- else
- cmp
-
let is_anon = function (_,None) -> true | _ -> false
(* EOF *)
projects / helm.git / blobdiff