1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (*****************************************************************************)
30 (* Enrico Tassi <tassi@cs.unibo.it> *)
33 (* This module implements the aciclic graph of universes. *)
35 (*****************************************************************************)
39 (*****************************************************************************)
40 (** switch implementation **)
41 (*****************************************************************************)
43 let fast_implementation = ref true ;;
45 (*****************************************************************************)
47 (*****************************************************************************)
51 (*****************************************************************************)
52 (** Types and default values **)
53 (*****************************************************************************)
55 type universe = int * UriManager.uri option
57 module UniverseType = struct
59 let compare = Pervasives.compare
62 module SOF = Set.Make(UniverseType)
74 module MAL = Map.Make(UniverseType)
76 type arc_type = GE | GT | EQ
78 type bag = entry MAL.t
89 let empty_bag = MAL.empty
91 let are_set_eq s1 s2 =
94 let are_entry_eq v1 v2 =
95 (are_set_eq v1.gt_closure v2.gt_closure ) &&
96 (are_set_eq v1.ge_closure v2.ge_closure ) &&
97 (are_set_eq v1.eq_closure v2.eq_closure ) &&
98 (*(are_set_eq v1.in_gegt_of v2.in_gegt_of ) &&*)
99 (are_set_eq v1.one_s_ge v2.one_s_ge ) &&
100 (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
101 (are_set_eq v1.one_s_eq v2.one_s_eq )
103 let are_ugraph_eq = MAL.equal are_entry_eq
105 (*****************************************************************************)
106 (** Pretty printings **)
107 (*****************************************************************************)
109 let string_of_universe (i,u) =
112 "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
113 | None -> "(" ^ (string_of_int i) ^ ",None)"
115 let string_of_universe_set l =
116 SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
118 let string_of_node n =
120 "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^
121 "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^
122 "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^
123 "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
125 let string_of_arc (a,u,v) =
126 (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
128 let string_of_mal m =
131 rc := !rc ^ sprintf "%s --> %s" (string_of_universe k)
132 (string_of_node v)) m;
135 let string_of_bag b =
138 (*****************************************************************************)
140 (*****************************************************************************)
141 let time_spent = ref 0.0;;
142 let partial = ref 0.0 ;;
144 let reset_spent_time () = time_spent := 0.0;;
145 let get_spent_time () = !time_spent ;;
146 let begin_spending () = ()
147 (*assert (!partial = 0.0);*)
148 (* partial := Unix.gettimeofday () *)
151 let end_spending () = ()
153 assert (!partial > 0.0);
154 let interval = (Unix.gettimeofday ()) -. !partial in
156 time_spent := !time_spent +. interval
161 (*****************************************************************************)
163 (*****************************************************************************)
170 Not_found -> empty_entry
172 (* FIXME: May be faster if we make it by hand *)
173 let merge_closures f nodes m =
174 SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
177 (*****************************************************************************)
178 (** _fats implementation **)
179 (*****************************************************************************)
181 let rec closure_of_fast ru m =
182 let eq_c = closure_eq_fast ru m in
183 let ge_c = closure_ge_fast ru m in
184 let gt_c = closure_gt_fast ru m in
189 in_gegt_of = ru.in_gegt_of;
190 one_s_eq = ru.one_s_eq;
191 one_s_ge = ru.one_s_ge;
192 one_s_gt = ru.one_s_gt
195 and closure_eq_fast ru m =
197 let j = ru.one_s_eq in
198 let _Uj = merge_closures (fun x -> x.eq_closure) j m in
199 let one_step_eq = ru.one_s_eq in
200 (SOF.union one_step_eq _Uj)
204 and closure_ge_fast ru m =
206 let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
207 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
213 and closure_gt_fast ru m =
215 let j = ru.one_s_gt in
216 let k = ru.one_s_ge in
217 let l = ru.one_s_eq in
218 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
219 let _Uk = merge_closures (fun x -> x.gt_closure) k m in
220 let _Ul = merge_closures (fun x -> x.gt_closure) l m in
221 let one_step_gt = ru.one_s_gt in
222 (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
226 and print_rec_status u ru =
227 print_endline ("Aggiusto " ^ (string_of_universe u) ^
228 "e ottengo questa chiusura\n " ^ (string_of_node ru))
230 and adjust_fast_aux u m =
232 let gt_c = closure_gt_fast ru m in
233 let ge_c = closure_ge_fast ru m in
234 let eq_c = closure_eq_fast ru m in
235 let changed_eq = not (are_set_eq eq_c ru.eq_closure) in
237 (not (are_set_eq gt_c ru.gt_closure)) ||
238 (not (are_set_eq ge_c ru.ge_closure))
240 if ((not changed_gegt) && (not changed_eq)) then
248 in_gegt_of = ru.in_gegt_of;
249 one_s_eq = ru.one_s_eq;
250 one_s_ge = ru.one_s_ge;
251 one_s_gt = ru.one_s_gt}
253 let m = MAL.add u ru' m in
255 SOF.fold (fun x m -> adjust_fast_aux x m)
256 (SOF.union ru'.eq_closure ru'.in_gegt_of) m
261 m (*adjust_fast u m*)
265 and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
266 and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
268 and adjust_fast x y = adjust_fast_aux x y
270 and add_gt_arc_fast u v m =
272 if SOF.mem v ru.gt_closure then m else
273 let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
274 let m' = MAL.add u ru' m in
275 let rv = repr v m' in
276 let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
277 let m'' = MAL.add v rv' m' in
280 and add_ge_arc_fast u v m =
282 if SOF.mem v ru.ge_closure then m else
283 let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
284 let m' = MAL.add u ru' m in
285 let rv = repr v m' in
286 let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
287 let m'' = MAL.add v rv' m' in
290 and add_eq_arc_fast u v m =
292 if SOF.mem v ru.eq_closure then m else
294 let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
295 (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
296 let m' = MAL.add u ru' m in
297 let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
298 (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
299 let m'' = MAL.add v rv' m' in
300 adjust_fast v (*(adjust_fast u*) m'' (* ) *)
304 (*****************************************************************************)
305 (** safe implementation **)
306 (*****************************************************************************)
311 let j = ru.one_s_eq in
312 let _Uj = merge_closures (fun x -> x.eq_closure) j m in
313 let one_step_eq = ru.one_s_eq in
314 (SOF.union one_step_eq _Uj)
317 let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
318 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
323 let j = ru.one_s_gt in
324 let k = ru.one_s_ge in
325 let l = ru.one_s_eq in
326 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
327 let _Uk = merge_closures (fun x -> x.gt_closure) k m in
328 let _Ul = merge_closures (fun x -> x.gt_closure) l m in
329 let one_step_gt = ru.one_s_gt in
330 (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
336 in_gegt_of = ru.in_gegt_of;
337 one_s_eq = ru.one_s_eq;
338 one_s_ge = ru.one_s_ge;
339 one_s_gt = ru.one_s_gt
342 let rec simple_adjust m =
344 MAL.mapi (fun x _ -> closure_of x m) m
346 if not (are_ugraph_eq m m') then(
351 let add_eq_arc u v m =
354 let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
355 let m' = MAL.add u ru' m in
356 let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
357 let m'' = MAL.add v rv' m' in
360 let add_ge_arc u v m =
362 let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
363 let m' = MAL.add u ru' m in
366 let add_gt_arc u v m =
368 let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
369 let m' = MAL.add u ru' m in
373 (*****************************************************************************)
374 (** Outhern interface, that chooses between _fast and safe **)
375 (*****************************************************************************)
378 given the 2 nodes plus the current bag, adds the arc, recomputes the
379 closures and returns the new map
381 let add_eq fast u v b =
383 add_eq_arc_fast u v b
388 given the 2 nodes plus the current bag, adds the arc, recomputes the
389 closures and returns the new map
391 let add_ge fast u v b =
393 add_ge_arc_fast u v b
397 given the 2 nodes plus the current bag, adds the arc, recomputes the
398 closures and returns the new map
400 let add_gt fast u v b =
402 add_gt_arc_fast u v b
407 (*****************************************************************************)
408 (** Other real code **)
409 (*****************************************************************************)
411 exception UniverseInconsistency of string Lazy.t
413 let error arc node1 closure_type node2 closure =
416 ("\n ===== Universe Inconsistency detected =====\n\n" ^
418 "\t" ^ (string_of_arc arc) ^ "\n" ^
420 "\t" ^ (string_of_universe node1) ^ "\n" ^
421 " is in the " ^ closure_type ^ " closure\n" ^
422 "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^
424 "\t" ^ (string_of_universe node2) ^ "\n\n" ^
425 " ===== Universe Inconsistency detected =====\n") in
426 prerr_endline (Lazy.force s);
427 raise (UniverseInconsistency s)
430 let fill_empty_nodes_with_uri (g, already_contained,o) l uri =
431 let fill_empty_universe u =
433 (i,None) -> (i,Some uri)
434 | (i,Some _) as u -> u
436 let fill_empty_set s =
437 SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
439 let fill_empty_entry e = {
440 eq_closure = (fill_empty_set e.eq_closure) ;
441 ge_closure = (fill_empty_set e.ge_closure) ;
442 gt_closure = (fill_empty_set e.gt_closure) ;
443 in_gegt_of = (fill_empty_set e.in_gegt_of) ;
444 one_s_eq = (fill_empty_set e.one_s_eq) ;
445 one_s_ge = (fill_empty_set e.one_s_ge) ;
446 one_s_gt = (fill_empty_set e.one_s_gt) ;
451 MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
453 let l' = List.map fill_empty_universe l in
454 (m', already_contained,o),l'
457 (*****************************************************************************)
458 (** World interface **)
459 (*****************************************************************************)
461 type universe_graph = bag * UriManager.UriSet.t * bool
462 (* the graph , the cache of already merged ugraphs, oblivion? *)
464 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
465 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
467 let current_index_anon = ref (-1)
468 let current_index_named = ref (-1)
470 let restart_numbering () = current_index_named := (-1)
472 let fresh ?uri ?id () =
476 current_index_anon := !current_index_anon + 1;
478 | None, Some _ -> assert false
480 current_index_named := !current_index_named + 1;
482 | Some _, Some id -> id
486 let name_universe u uri =
488 | (i, None) -> (i, Some uri)
489 | (i, Some ouri) when UriManager.eq ouri uri -> u
491 (* inside obj living at uri 'uri' should live only
492 * universes with uri None. Call Unshare.unshare ~fresh_univs:true
493 * if you want to reuse a Type in another object *)
494 prerr_endline ("Offending universe: " ^ string_of_universe u^
495 " found inside object " ^ UriManager.string_of_uri uri);
499 let print_ugraph (g, _, o) =
500 if o then prerr_endline "oblivion universe" else
501 prerr_endline (string_of_bag g)
503 let add_eq ?(fast=(!fast_implementation)) u v b =
504 (* should we check to no add twice the same?? *)
507 if SOF.mem v ru.gt_closure then
508 error ("EQ",u,v) v "GT" u ru.gt_closure
512 if SOF.mem u rv.gt_closure then
513 error ("EQ",u,v) u "GT" v rv.gt_closure
518 let add_ge ?(fast=(!fast_implementation)) u v b =
519 (* should we check to no add twice the same?? *)
522 if SOF.mem u rv.gt_closure then
523 error ("GE",u,v) u "GT" v rv.gt_closure
527 let add_gt ?(fast=(!fast_implementation)) u v b =
528 (* should we check to no add twice the same?? *)
530 FIXME : check the thesis... no need to check GT and EQ closure since the
531 GE is a superset of both
537 error ("GT",u,v) u "==" v SOF.empty
540 (*if SOF.mem u rv.gt_closure then
541 error ("GT",u,v) u "GT" v rv.gt_closure
544 if SOF.mem u rv.ge_closure then
545 error ("GT",u,v) u "GE" v rv.ge_closure
548 if SOF.mem u rv.eq_closure then
549 error ("GT",u,v) u "EQ" v rv.eq_closure
555 (*****************************************************************************)
556 (** START: Decomment this for performance comparisons **)
557 (*****************************************************************************)
559 let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
560 if oblivion then (b,already_contained,oblivion) else
561 (*prerr_endline "add_eq";*)
563 let rc = add_eq ~fast u v b in
565 rc,already_contained,false)
567 let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
568 if oblivion then (b,already_contained,oblivion) else
569 (* prerr_endline "add_ge"; *)
571 let rc = add_ge ~fast u v b in
573 rc,already_contained,false)
575 let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
576 if oblivion then (b,already_contained,oblivion) else
577 (* prerr_endline "add_gt"; *)
579 let rc = add_gt ~fast u v b in
581 rc,already_contained,false)
584 let profiler_eq = HExtlib.profile "CicUniv.add_eq"
585 let profiler_ge = HExtlib.profile "CicUniv.add_ge"
586 let profiler_gt = HExtlib.profile "CicUniv.add_gt"
587 let add_gt ?fast u v b =
588 profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) ()
589 let add_ge ?fast u v b =
590 profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
591 let add_eq ?fast u v b =
592 profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
596 let rank = ref MAL.empty;;
598 let do_rank (b,_,_ as ugraph) =
599 (* print_ugraph ugraph; *)
600 let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
604 let rec aux k seen = function
606 | x::tl when SOF.mem x seen -> aux k seen tl
608 (* prerr_endline (String.make k '.' ^ string_of_universe x); *)
609 let seen = SOF.add x seen in
610 let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
611 let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in
612 let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
613 let t4, seen = aux k seen tl in
615 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
618 let rank, _ = aux 0 SOF.empty [u] in
625 prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
631 (* if the universe is not in the graph it means there are
632 * no contraints on it! thus it can be freely set to Type0 *)
635 (*****************************************************************************)
636 (** END: Decomment this for performance comparisons **)
637 (*****************************************************************************)
639 (* TODO: uncomment l to gain a small speedup *)
640 let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
641 let merge_brutal (u,a,_) v =
642 (* prerr_endline ("merging graph: "^UriManager.string_of_uri
643 * uri_of_increment); *)
650 let m = add_gt k u x in m)
651 (SOF.union v.one_s_gt v.gt_closure)
654 let m = add_ge k u x in m)
655 (SOF.union v.one_s_ge v.ge_closure)
658 let m = add_eq k u x in m)
659 (SOF.union v.one_s_eq v.eq_closure) x)))
662 let base, already_contained, oblivion = base_ugraph in
663 let inc,_,oblivion2 = increment in
666 else if oblivion2 then
668 else if MAL.is_empty base then
672 UriManager.UriSet.mem uri_of_increment already_contained
676 (fun (x,_,_) -> x) (merge_brutal increment base_ugraph),
678 List.fold_right UriManager.UriSet.add
679 (List.map (fun (_,x) -> HExtlib.unopt x) l)
681 (UriManager.UriSet.add uri_of_increment already_contained), false
683 (* profiling code; WARNING: the time spent during profiling can be
684 greater than the profiled time
685 let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
686 let merge_ugraphs ~base_ugraph ~increment =
687 profiler_merge.HExtlib.profile
688 (fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
691 (*****************************************************************************)
692 (** Xml sesialization and parsing **)
693 (*****************************************************************************)
695 let xml_of_universe name u =
699 None,"id",(string_of_int i) ;
700 None,"uri",(UriManager.string_of_uri u)]
702 raise (Failure "we can serialize only universes with uri")
706 List.map (xml_of_universe "node") (SOF.elements s)
708 List.fold_left (fun s x -> [< s ; x >] ) [<>] l
710 let xml_of_entry_content e =
711 let stream_of_field f name =
712 let eq_c = xml_of_set f in
714 Xml.xml_nempty name [] eq_c
719 (stream_of_field e.eq_closure "eq_closure");
720 (stream_of_field e.gt_closure "gt_closure");
721 (stream_of_field e.ge_closure "ge_closure");
722 (stream_of_field e.in_gegt_of "in_gegt_of");
723 (stream_of_field e.one_s_eq "one_s_eq");
724 (stream_of_field e.one_s_gt "one_s_gt");
725 (stream_of_field e.one_s_ge "one_s_ge")
728 let xml_of_entry u e =
734 raise (Failure "we can serialize only universes (entry) with uri")
736 let ent = Xml.xml_nempty "entry" [
737 None,"id",(string_of_int i) ;
738 None,"uri",(UriManager.string_of_uri u'')] in
739 let content = xml_of_entry_content e in
742 let write_xml_of_ugraph filename (m,_,_) l =
745 Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
746 Xml.xml_nempty "ugraph" []
747 ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ;
749 (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>]
751 Xml.pp ~gzip:true tokens (Some filename)
756 let rec clean_ugraph m already_contained f =
758 MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
759 let m'' = MAL.fold (fun k v x ->
761 eq_closure = SOF.filter f v.eq_closure;
762 ge_closure = SOF.filter f v.ge_closure;
763 gt_closure = SOF.filter f v.gt_closure;
764 in_gegt_of = SOF.filter f v.in_gegt_of;
765 one_s_eq = SOF.filter f v.one_s_eq;
766 one_s_ge = SOF.filter f v.one_s_ge;
767 one_s_gt = SOF.filter f v.one_s_gt
769 MAL.add k v' x ) m' MAL.empty in
771 MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
773 k::l end else l) m'' []
777 m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
780 (fun k v x -> if v <> empty_entry then MAL.add k v x else x)
784 let clean_ugraph (m,a,o) l =
786 let m, a = clean_ugraph m a (fun u -> List.mem u l) in
791 "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
792 | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
793 | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
794 | "in_gegt_of" -> (fun e u->{e with in_gegt_of =SOF.add u e.in_gegt_of})
795 | "one_s_ge" -> (fun e u->{e with one_s_ge =SOF.add u e.one_s_ge})
796 | "one_s_gt" -> (fun e u->{e with one_s_gt =SOF.add u e.one_s_gt})
797 | "one_s_eq" -> (fun e u->{e with one_s_eq =SOF.add u e.one_s_eq})
798 | s -> raise (Failure ("unsupported tag " ^ s))
802 let module XPP = XmlPushParser in
803 let current_node = ref (0,None) in
804 let current_entry = ref empty_entry in
805 let current_assign = ref (assigner_of "in_gegt_of") in
806 { XPP.default_callbacks with
807 XPP.end_element = Some( fun name ->
810 m := MAL.add !current_node !current_entry !m;
811 current_entry := empty_entry
814 XPP.start_element = Some( fun name attlist ->
818 let id = List.assoc "id" attlist in
819 let uri = List.assoc "uri" attlist in
820 current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
822 let id = int_of_string (List.assoc "id" attlist) in
823 let uri = List.assoc "uri" attlist in
824 current_entry := !current_assign !current_entry
825 (id,Some (UriManager.uri_of_string uri))
827 let id = int_of_string (List.assoc "id" attlist) in
828 let uri = List.assoc "uri" attlist in
829 l := (id,Some (UriManager.uri_of_string uri)) :: !l
830 | s -> current_assign := assigner_of s
835 let ugraph_and_univlist_of_xml filename =
836 let module XPP = XmlPushParser in
837 let result_map = ref MAL.empty in
838 let result_list = ref [] in
839 let cb = cb_factory result_map result_list in
840 let xml_parser = XPP.create_parser cb in
841 let xml_source = `Gzip_file filename in
842 (try XPP.parse xml_parser xml_source
843 with (XPP.Parse_error err) as exn -> raise exn);
844 (!result_map,UriManager.UriSet.empty,false), !result_list
847 (*****************************************************************************)
848 (** the main, only for testing **)
849 (*****************************************************************************)
853 type arc = Ge | Gt | Eq ;;
855 let randomize_actionlist n m =
856 let ge_percent = 0.7 in
857 let gt_percent = 0.15 in
859 let node1 = Random.int m in
860 let node2 = Random.int m in
862 let r = Random.float 1.0 in
863 if r < ge_percent then
865 else (if r < (ge_percent +. gt_percent) then
875 | n -> (random_step ())::(aux (n-1))
879 let print_action_list l =
880 let string_of_step (op,node1,node2) =
885 "," ^ (string_of_int node1) ^ "," ^ (string_of_int node2)
891 ";" ^ (string_of_step a) ^ (aux tl)
894 let l_body = (String.length body) - 1 in
895 prerr_endline ("[" ^ (String.sub body 1 l_body))
898 let d_print_endline = if debug then print_endline else ignore
899 let d_print_ugraph = if debug then print_ugraph else ignore
902 (if Array.length Sys.argv < 2 then
903 prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
905 let max_edges = int_of_string Sys.argv.(1) in
906 let max_nodes = int_of_string Sys.argv.(2) in
907 let action_listR = randomize_actionlist max_edges max_nodes in
909 let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
910 let action_list = action_listR in
912 print_action_list action_list;
913 let prform_step ?(fast=false) (t,u,v) g =
925 let g' = f ~fast (u,None) (v,None) g in
926 (*print_ugraph g' ;*)
929 let fail = ref false in
930 let time1 = Unix.gettimeofday () in
931 let n_safe = ref 0 in
934 d_print_endline "SAFE";
937 n_safe := !n_safe + 1;
939 ) empty_ugraph action_list
941 UniverseInconsistency s -> fail:=true;empty_bag
943 let time2 = Unix.gettimeofday () in
944 d_print_ugraph g_safe;
945 let time3 = Unix.gettimeofday () in
946 let n_test = ref 0 in
949 d_print_endline "FAST";
952 n_test := !n_test + 1;
953 prform_step ~fast:true e g
954 ) empty_ugraph action_list
956 UniverseInconsistency s -> empty_bag
958 let time4 = Unix.gettimeofday () in
959 d_print_ugraph g_test;
960 if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
965 if e = Eq then s+1 else s
971 if e = Gt then s+1 else s
974 let num_ge = max_edges - num_gt - num_eq in
975 let time_fast = (time4 -. time3) in
976 let time_safe = (time2 -. time1) in
977 let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
978 let fail = if !fail then 1 else 0 in
981 "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d"
982 fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
987 print_endline "FAIL";
1000 i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
1002 let recons_entry entry =
1003 let recons_set set =
1004 SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
1007 eq_closure = recons_set entry.eq_closure;
1008 ge_closure = recons_set entry.ge_closure;
1009 gt_closure = recons_set entry.gt_closure;
1010 in_gegt_of = recons_set entry.in_gegt_of;
1011 one_s_eq = recons_set entry.one_s_eq;
1012 one_s_ge = recons_set entry.one_s_ge;
1013 one_s_gt = recons_set entry.one_s_gt;
1016 let recons_graph (graph,uriset,o) =
1018 (fun universe entry map ->
1019 MAL.add (recons_univ universe) (recons_entry entry) map)
1022 UriManager.UriSet.fold
1024 UriManager.UriSet.add
1025 (UriManager.uri_of_string (UriManager.string_of_uri u)) acc)
1026 uriset UriManager.UriSet.empty, o
1031 raise (UniverseInconsistency (lazy "This universe graph has a hole"))
1034 let assert_univs_have_uri (graph,_,_) univlist =
1036 SOF.iter (fun u -> assert_univ u) s
1038 let assert_entry e =
1039 assert_set e.eq_closure;
1040 assert_set e.ge_closure;
1041 assert_set e.gt_closure;
1042 assert_set e.in_gegt_of;
1043 assert_set e.one_s_eq;
1044 assert_set e.one_s_ge;
1045 assert_set e.one_s_gt;
1047 MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
1048 List.iter assert_univ univlist
1052 | (id1, Some uri1),(id2, Some uri2) ->
1053 id1 = id2 && UriManager.eq uri1 uri2
1054 | (id1, None),(id2, None) -> id1 = id2
1057 let compare (id1, uri1) (id2, uri2) =
1058 let cmp = id1 - id2 in
1060 match uri1,uri2 with
1063 | None, Some _ -> ~-1
1064 | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
1068 let is_anon = function (_,None) -> true | _ -> false