X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=58dc5cd6cfc82af8641150ba34168d5281716f4a;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=0d75caf898cec408590e0f82a59aaf22bfa4b085;hpb=d0212d7627d3e135c224ffaa30b03ee1969a4578;p=helm.git diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index 0d75caf89..58dc5cd6c 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -36,12 +36,6 @@ (* $Id$ *) -(*****************************************************************************) -(** switch implementation **) -(*****************************************************************************) - -let fast_implementation = ref true ;; - (*****************************************************************************) (** open **) (*****************************************************************************) @@ -52,11 +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 = Pervasives.compare + let compare = compare end module SOF = Set.Make(UniverseType) @@ -135,27 +148,6 @@ let string_of_mal m = let string_of_bag b = string_of_mal b -(*****************************************************************************) -(** Benchmarking **) -(*****************************************************************************) -let time_spent = ref 0.0;; -let partial = ref 0.0 ;; - -let reset_spent_time () = time_spent := 0.0;; -let get_spent_time () = !time_spent ;; -let begin_spending () = - (*assert (!partial = 0.0);*) - partial := Unix.gettimeofday () -;; - -let end_spending () = - assert (!partial > 0.0); - let interval = (Unix.gettimeofday ()) -. !partial in - partial := 0.0; - time_spent := !time_spent +. interval -;; - - (*****************************************************************************) (** Helpers **) (*****************************************************************************) @@ -225,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 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 @@ -236,7 +230,7 @@ and adjust_fast 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' = { @@ -249,18 +243,29 @@ and adjust_fast 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 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 = + fst(adjust_fast_aux SOF.empty x y) and add_gt_arc_fast u v m = let ru = repr u m in + if SOF.mem v ru.gt_closure then m else let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in let m' = MAL.add u ru' m in let rv = repr v m' in @@ -270,6 +275,7 @@ and add_gt_arc_fast u v m = and add_ge_arc_fast u v m = let ru = repr u m in + if SOF.mem v ru.ge_closure then m else let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in let m' = MAL.add u ru' m in let rv = repr v m' in @@ -279,6 +285,7 @@ and add_ge_arc_fast u v m = and add_eq_arc_fast u v m = let ru = repr u m in + if SOF.mem v ru.eq_closure then m else let rv = repr v m in let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *) @@ -290,131 +297,31 @@ and add_eq_arc_fast u v m = ;; -(*****************************************************************************) -(** safe implementation **) -(*****************************************************************************) - -let closure_of u m = - let ru = repr u m in - let eq_c = - let j = ru.one_s_eq in - let _Uj = merge_closures (fun x -> x.eq_closure) j m in - let one_step_eq = ru.one_s_eq in - (SOF.union one_step_eq _Uj) - in - let ge_c = - let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in - let _Uj = merge_closures (fun x -> x.ge_closure) j m in - let _Ux = j in - (SOF.union _Uj _Ux) - in - let gt_c = - let j = ru.one_s_gt in - let k = ru.one_s_ge in - let l = ru.one_s_eq in - let _Uj = merge_closures (fun x -> x.ge_closure) j m in - let _Uk = merge_closures (fun x -> x.gt_closure) k m in - let _Ul = merge_closures (fun x -> x.gt_closure) l m in - let one_step_gt = ru.one_s_gt in - (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj) - in - { - eq_closure = eq_c; - ge_closure = ge_c; - gt_closure = gt_c; - in_gegt_of = ru.in_gegt_of; - one_s_eq = ru.one_s_eq; - one_s_ge = ru.one_s_ge; - one_s_gt = ru.one_s_gt - } - -let rec simple_adjust m = - let m' = - MAL.mapi (fun x _ -> closure_of x m) m - in - if not (are_ugraph_eq m m') then( - simple_adjust m') - else - m' - -let add_eq_arc u v m = - let ru = repr u m in - let rv = repr v m in - let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in - let m' = MAL.add u ru' m in - let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in - let m'' = MAL.add v rv' m' in - simple_adjust m'' - -let add_ge_arc u v m = - let ru = repr u m in - let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in - let m' = MAL.add u ru' m in - simple_adjust m' - -let add_gt_arc u v m = - let ru = repr u m in - let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in - let m' = MAL.add u ru' m in - simple_adjust m' - - -(*****************************************************************************) -(** Outhern interface, that chooses between _fast and safe **) -(*****************************************************************************) - -(* - given the 2 nodes plus the current bag, adds the arc, recomputes the - closures and returns the new map -*) -let add_eq fast u v b = - if fast then - add_eq_arc_fast u v b - else - add_eq_arc u v b - -(* - given the 2 nodes plus the current bag, adds the arc, recomputes the - closures and returns the new map -*) -let add_ge fast u v b = - if fast then - add_ge_arc_fast u v b - else - add_ge_arc u v b -(* - given the 2 nodes plus the current bag, adds the arc, recomputes the - closures and returns the new map -*) -let add_gt fast u v b = - if fast then - add_gt_arc_fast u v b - else - add_gt_arc u v b - (*****************************************************************************) (** Other real code **) (*****************************************************************************) -exception UniverseInconsistency of string +exception UniverseInconsistency of string Lazy.t let error arc node1 closure_type node2 closure = - let s = "\n ===== Universe Inconsistency detected =====\n\n" ^ - " Unable to add\n" ^ - "\t" ^ (string_of_arc arc) ^ "\n" ^ - " cause\n" ^ - "\t" ^ (string_of_universe node1) ^ "\n" ^ - " is in the " ^ closure_type ^ " closure\n" ^ - "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ - " of\n" ^ - "\t" ^ (string_of_universe node2) ^ "\n\n" ^ - " ===== Universe Inconsistency detected =====\n" in - prerr_endline s; + let s = + lazy + ("\n ===== Universe Inconsistency detected =====\n\n" ^ + " Unable to add\n" ^ + "\t" ^ (string_of_arc arc) ^ "\n" ^ + " cause\n" ^ + "\t" ^ (string_of_universe node1) ^ "\n" ^ + " is in the " ^ closure_type ^ " closure\n" ^ + "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ + " of\n" ^ + "\t" ^ (string_of_universe node2) ^ "\n\n" ^ + " ===== Universe Inconsistency detected =====\n") in +(* prerr_endline (Lazy.force s); *) raise (UniverseInconsistency s) -let fill_empty_nodes_with_uri (g, already_contained) l uri = +let fill_empty_nodes_with_uri (g, already_contained,o) l uri = let fill_empty_universe u = match u with (i,None) -> (i,Some uri) @@ -438,17 +345,20 @@ let fill_empty_nodes_with_uri (g, already_contained) l uri = MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty in let l' = List.map fill_empty_universe l in - (m', already_contained),l' + (m', already_contained,o),l' (*****************************************************************************) (** World interface **) (*****************************************************************************) -type universe_graph = bag * UriManager.UriSet.t -(* the graph , the cache of already merged ugraphs *) +type universe_graph = bag * UriManager.UriSet.t * bool +(* the graph , the cache of already merged ugraphs, oblivion? *) -let empty_ugraph = empty_bag, UriManager.UriSet.empty +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) @@ -472,12 +382,14 @@ let fresh ?uri ?id () = let name_universe u uri = match u with | (i, None) -> (i, Some uri) - | _ -> u + | u -> u +;; -let print_ugraph (g, _) = +let print_ugraph (g, _, o) = + if o then prerr_endline "oblivion universe" else prerr_endline (string_of_bag g) -let add_eq ?(fast=(!fast_implementation)) u v b = +let add_eq u v b = (* should we check to no add twice the same?? *) let m = b in let ru = repr u m in @@ -489,19 +401,19 @@ let add_eq ?(fast=(!fast_implementation)) u v b = if SOF.mem u rv.gt_closure then error ("EQ",u,v) u "GT" v rv.gt_closure else - add_eq fast u v b + add_eq_arc_fast u v b end -let add_ge ?(fast=(!fast_implementation)) u v b = +let add_ge u v b = (* should we check to no add twice the same?? *) let m = b in let rv = repr v m in if SOF.mem u rv.gt_closure then error ("GE",u,v) u "GT" v rv.gt_closure else - add_ge fast u v b + add_ge_arc_fast u v b -let add_gt ?(fast=(!fast_implementation)) u v b = +let add_gt u v b = (* should we check to no add twice the same?? *) (* FIXME : check the thesis... no need to check GT and EQ closure since the @@ -525,7 +437,7 @@ let add_gt ?(fast=(!fast_implementation)) u v b = if SOF.mem u rv.eq_closure then error ("GT",u,v) u "EQ" v rv.eq_closure else*) - add_gt fast u v b + add_gt_arc_fast u v b (* end end*) @@ -533,45 +445,87 @@ let add_gt ?(fast=(!fast_implementation)) u v b = (** START: Decomment this for performance comparisons **) (*****************************************************************************) -let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained) = - (*prerr_endline "add_eq";*) - begin_spending (); - let rc = add_eq ~fast u v b in - end_spending (); - rc,already_contained - -let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) = -(* prerr_endline "add_ge"; *) - begin_spending (); - let rc = add_ge ~fast u v b in - end_spending (); - rc,already_contained +let add_eq u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else + let rc = add_eq u v b in + rc,already_contained,false + +let add_ge u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else + let rc = add_ge u v b in + rc,already_contained,false -let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = -(* prerr_endline "add_gt"; *) - begin_spending (); - let rc = add_gt ~fast u v b in - end_spending (); - rc,already_contained +let add_gt u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else + let rc = add_gt u v b in + rc,already_contained,false -(* profiling code +(* profiling code *) let profiler_eq = HExtlib.profile "CicUniv.add_eq" let profiler_ge = HExtlib.profile "CicUniv.add_ge" let profiler_gt = HExtlib.profile "CicUniv.add_gt" -let add_gt ?fast u v b = - profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) () -let add_ge ?fast u v b = - profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) () -let add_eq ?fast u v b = - profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) () -*) +let add_gt u v b = + profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) () +let add_ge u v b = + profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) () +let add_eq u v b = + profiler_eq.HExtlib.profile (fun _ -> add_eq u v b) () + + +(* ugly *) +let rank = ref MAL.empty;; + +let do_rank (b,_,_) = + 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 + 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 -> + if not (List.mem v !res) then res := v::!res; + resk := k :: !resk) !rank; + !res, !resk +;; + +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 *) +;; (*****************************************************************************) (** END: Decomment this for performance comparisons **) (*****************************************************************************) -let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = - let merge_brutal (u,_) v = +(* TODO: uncomment l to gain a small speedup *) +let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) = + let merge_brutal (u,a,_) v = +(* prerr_endline ("merging graph: "^UriManager.string_of_uri + * uri_of_increment); *) let m1 = u in let m2 = v in MAL.fold ( @@ -588,22 +542,31 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = fun u x -> let m = add_eq k u x in m) (SOF.union v.one_s_eq v.eq_closure) x))) - ) m1 m2 + ) m1 m2 in - let base, already_contained = base_ugraph in - if MAL.is_empty base then + let base, already_contained, oblivion = base_ugraph in + let inc,_,oblivion2 = increment in + if oblivion then + base_ugraph + else if oblivion2 then + increment + else if MAL.is_empty base then increment else if - MAL.is_empty (fst increment) || + MAL.is_empty inc || UriManager.UriSet.mem uri_of_increment already_contained then base_ugraph - else - fst (merge_brutal increment base_ugraph), - UriManager.UriSet.add uri_of_increment already_contained + else + (fun (x,_,_) -> x) (merge_brutal increment base_ugraph), +(* + List.fold_right UriManager.UriSet.add + (List.map (fun (_,x) -> HExtlib.unopt x) l) +*) + (UriManager.UriSet.add uri_of_increment already_contained), false (* profiling code; WARNING: the time spent during profiling can be - greater than the profiled time + greater than the profiled time let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs" let merge_ugraphs ~base_ugraph ~increment = profiler_merge.HExtlib.profile @@ -661,7 +624,7 @@ let xml_of_entry u e = let content = xml_of_entry_content e in ent content -let write_xml_of_ugraph filename (m,_) l = +let write_xml_of_ugraph filename (m,_,_) l = let tokens = [< Xml.xml_cdata "\n"; @@ -673,9 +636,12 @@ 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 = +let rec clean_ugraph m already_contained f = let m' = MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in let m'' = MAL.fold (fun k v x -> @@ -692,19 +658,22 @@ 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) m'' MAL.empty, already_contained -let clean_ugraph g l = - clean_ugraph g (fun u -> List.mem u l) +let clean_ugraph (m,a,o) l = + assert(not o); + 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 = function @@ -761,7 +730,7 @@ let ugraph_and_univlist_of_xml filename = let xml_source = `Gzip_file filename in (try XPP.parse xml_parser xml_source with (XPP.Parse_error err) as exn -> raise exn); - (!result_map,UriManager.UriSet.empty), !result_list + (!result_map,UriManager.UriSet.empty,false), !result_list (*****************************************************************************) @@ -933,7 +902,7 @@ let recons_entry entry = one_s_gt = recons_set entry.one_s_gt; } -let recons_graph (graph,uriset) = +let recons_graph (graph,uriset,o) = MAL.fold (fun universe entry map -> MAL.add (recons_univ universe) (recons_entry entry) map) @@ -943,14 +912,15 @@ let recons_graph (graph,uriset) = (fun u acc -> UriManager.UriSet.add (UriManager.uri_of_string (UriManager.string_of_uri u)) acc) - uriset UriManager.UriSet.empty + uriset UriManager.UriSet.empty, o let assert_univ u = match u with - | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") + | (_,None) -> + raise (UniverseInconsistency (lazy "This universe graph has a hole")) | _ -> () -let assert_univs_have_uri (graph,_) univlist = +let assert_univs_have_uri (graph,_,_) univlist = let assert_set s = SOF.iter (fun u -> assert_univ u) s in @@ -966,22 +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 *)