X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=d3ae5c960f5169531f952b43bcbf86d15d1b930d;hb=c59d5065faea77ce41431e273a3331f4d152fbfa;hp=b7783095414d47d56a38fe65679c8ba322353088;hpb=bc2834b671b7e7554159a284f13e52d93debfd03;p=helm.git diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index b77830954..d3ae5c960 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -143,16 +143,18 @@ let partial = ref 0.0 ;; let reset_spent_time () = time_spent := 0.0;; let get_spent_time () = !time_spent ;; -let begin_spending () = +let begin_spending () = () (*assert (!partial = 0.0);*) - partial := Unix.gettimeofday () +(* partial := Unix.gettimeofday () *) ;; -let end_spending () = +let end_spending () = () +(* assert (!partial > 0.0); let interval = (Unix.gettimeofday ()) -. !partial in partial := 0.0; time_spent := !time_spent +. interval +*) ;; @@ -225,7 +227,7 @@ 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 u m = let ru = repr u m in let gt_c = closure_gt_fast ru m in let ge_c = closure_ge_fast ru m in @@ -250,7 +252,7 @@ and adjust_fast u m = in let m = MAL.add u ru' m in let m = - SOF.fold (fun x m -> adjust_fast x 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 @@ -258,9 +260,16 @@ and adjust_fast u m = in m (*adjust_fast u m*) 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 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 +279,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 +289,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 *) @@ -397,24 +408,26 @@ let add_gt fast 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 +451,18 @@ 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 let current_index_anon = ref (-1) let current_index_named = ref (-1) @@ -472,9 +486,17 @@ let fresh ?uri ?id () = let name_universe u uri = match u with | (i, None) -> (i, Some 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 +;; -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 = @@ -533,27 +555,31 @@ 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) = +let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (*prerr_endline "add_eq";*) - begin_spending (); + (begin_spending (); let rc = add_eq ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) -let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) = +let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (* prerr_endline "add_ge"; *) - begin_spending (); + (begin_spending (); let rc = add_ge ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) -let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = +let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (* prerr_endline "add_gt"; *) - begin_spending (); + (begin_spending (); let rc = add_gt ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) +(* 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" @@ -563,13 +589,56 @@ 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) () +*) + +(* ugly *) +let rank = ref MAL.empty;; + +let do_rank (b,_,_) = + + let keys = MAL.fold (fun k _ acc -> k::acc) b [] in + let fall = + List.fold_left + (fun acc u -> + let rec aux seen = function + | [] -> 0, seen + | x::tl when SOF.mem x seen -> aux seen tl + | x::tl -> + let seen = SOF.add x seen in + let t1, seen = aux seen (SOF.elements (repr x b).one_s_eq) in + let t2, seen = aux seen (SOF.elements (repr x b).one_s_ge) in + let t3, seen = aux seen (SOF.elements (repr x b).one_s_gt) in + let t4, seen = aux seen tl in + max (max t1 t2) + (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4), + seen + in + let rank, _ = aux SOF.empty [u] in + MAL.add u rank acc) + MAL.empty + in + rank := fall keys; + MAL.iter + (fun k v -> + prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank +;; + +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 ( @@ -586,22 +655,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 @@ -659,7 +737,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,7 +751,7 @@ let write_xml_of_ugraph filename (m,_) l = let univno = fst -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 -> @@ -694,15 +772,17 @@ let rec clean_ugraph (m,already_contained) f = in if 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 (List.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 m, a = clean_ugraph m a (fun u -> List.mem u l) in + m, a, o let assigner_of = function @@ -759,7 +839,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 (*****************************************************************************) @@ -931,7 +1011,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) @@ -941,14 +1021,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 @@ -981,5 +1062,7 @@ let compare (id1, uri1) (id2, uri2) = | Some uri1, Some uri2 -> UriManager.compare uri1 uri2 else cmp + +let is_anon = function (_,None) -> true | _ -> false (* EOF *)