X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=58dc5cd6cfc82af8641150ba34168d5281716f4a;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=fe9f01d532af2c65866fb1b9a34d6cf223ed76dd;hpb=0805c61933df87f5cfae63b94456a1f0518b06d0;p=helm.git diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index fe9f01d53..58dc5cd6c 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -46,19 +46,30 @@ open Printf (** 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) @@ -206,7 +217,9 @@ and print_rec_status u ru = 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 @@ -217,7 +230,7 @@ and adjust_fast_aux u m = (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' = { @@ -230,21 +243,25 @@ and adjust_fast_aux u m = 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 @@ -300,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) @@ -340,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) @@ -363,14 +382,7 @@ let fresh ?uri ?id () = 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) = @@ -464,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 + 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 = @@ -619,6 +636,9 @@ let write_xml_of_ugraph filename (m,_,_) l = 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 = @@ -638,11 +658,11 @@ 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) @@ -651,7 +671,8 @@ let rec clean_ugraph m already_contained f = 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 = @@ -915,24 +936,6 @@ let assert_univs_have_uri (graph,_,_) univlist = 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 *)