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 (*****************************************************************************)
37 (*****************************************************************************)
38 (** switch implementation **)
39 (*****************************************************************************)
41 let fast_implementation = ref false ;;
43 (*****************************************************************************)
45 (*****************************************************************************)
49 (*****************************************************************************)
50 (** Types and default values **)
51 (*****************************************************************************)
53 type universe = int * UriManager.uri option
55 module UniverseType = struct
57 let compare = Pervasives.compare
60 module SOF = Set.Make(UniverseType)
72 module MAL = Map.Make(UniverseType)
74 type arc_type = GE | GT | EQ
76 type bag = entry MAL.t
87 let empty_bag = MAL.empty
89 let are_set_eq s1 s2 =
92 let are_entry_eq v1 v2 =
93 (are_set_eq v1.gt_closure v2.gt_closure ) &&
94 (are_set_eq v1.ge_closure v2.ge_closure ) &&
95 (are_set_eq v1.eq_closure v2.eq_closure ) &&
96 (*(are_set_eq v1.in_gegt_of v2.in_gegt_of ) &&*)
97 (are_set_eq v1.one_s_ge v2.one_s_ge ) &&
98 (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
99 (are_set_eq v1.one_s_eq v2.one_s_eq )
102 (* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *)
104 let are_ugraph_eq308 g h =
105 MAL.equal are_entry_eq g h
107 let are_ugraph_eq307 g h =
112 raise (Failure "Different")
115 let k_h = MAL.find k h in
117 with Not_found -> true
120 Failure "Different" -> false
122 let are_ugraph_eq = are_ugraph_eq307
124 (*****************************************************************************)
125 (** Pretty printings **)
126 (*****************************************************************************)
128 let string_of_universe (i,u) =
131 "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
132 | None -> "(" ^ (string_of_int i) ^ ",None)"
134 let string_of_universe_set l =
135 SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
137 let string_of_node n =
139 "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^
140 "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^
141 "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^
142 "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
144 let string_of_arc (a,u,v) =
145 (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
147 let string_of_mal m =
150 rc := !rc ^ sprintf "%s --> %s" (string_of_universe k)
151 (string_of_node v)) m;
154 let string_of_bag b =
157 (*****************************************************************************)
159 (*****************************************************************************)
166 Not_found -> empty_entry
168 (* FIXME: May be faster if we make it by hand *)
169 let merge_closures f nodes m =
170 SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
172 (*****************************************************************************)
174 (*****************************************************************************)
175 let time_spent = ref 0.0;;
176 let partial = ref 0.0 ;;
178 let reset_spent_time () = time_spent := 0.0;;
179 let get_spent_time () = !time_spent ;;
180 let begin_spending () =
181 (*assert (!partial = 0.0);*)
182 partial := Unix.gettimeofday ()
185 let end_spending () =
186 assert (!partial > 0.0);
187 let interval = (Unix.gettimeofday ()) -. !partial in
189 time_spent := !time_spent +. interval
193 (*****************************************************************************)
194 (** _fats implementation **)
195 (*****************************************************************************)
197 let rec closure_of_fast ru m =
198 let eq_c = closure_eq_fast ru m in
199 let ge_c = closure_ge_fast ru m in
200 let gt_c = closure_gt_fast ru m in
205 in_gegt_of = ru.in_gegt_of;
206 one_s_eq = ru.one_s_eq;
207 one_s_ge = ru.one_s_ge;
208 one_s_gt = ru.one_s_gt
211 and closure_eq_fast ru m =
213 let j = ru.one_s_eq in
214 let _Uj = merge_closures (fun x -> x.eq_closure) j m in
215 let one_step_eq = ru.one_s_eq in
216 (SOF.union one_step_eq _Uj)
220 and closure_ge_fast ru m =
222 let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
223 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
229 and closure_gt_fast ru m =
231 let j = ru.one_s_gt in
232 let k = ru.one_s_ge in
233 let l = ru.one_s_eq in
234 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
235 let _Uk = merge_closures (fun x -> x.gt_closure) k m in
236 let _Ul = merge_closures (fun x -> x.gt_closure) l m in
237 let one_step_gt = ru.one_s_gt in
238 (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
242 and print_rec_status u ru =
243 print_endline ("Aggiusto " ^ (string_of_universe u) ^
244 "e ottengo questa chiusura\n " ^ (string_of_node ru))
246 and adjust_fast u m =
248 let gt_c = closure_gt_fast ru m in
249 let ge_c = closure_ge_fast ru m in
250 let eq_c = closure_eq_fast ru m in
251 let changed_eq = not (are_set_eq eq_c ru.eq_closure) in
253 (not (are_set_eq gt_c ru.gt_closure)) ||
254 (not (are_set_eq ge_c ru.ge_closure))
256 if ((not changed_gegt) && (not changed_eq)) then
264 in_gegt_of = ru.in_gegt_of;
265 one_s_eq = ru.one_s_eq;
266 one_s_ge = ru.one_s_ge;
267 one_s_gt = ru.one_s_gt}
269 let m = MAL.add u ru' m in
271 SOF.fold (fun x m -> adjust_fast x m)
272 (SOF.union ru'.eq_closure ru'.in_gegt_of) m
277 m (*adjust_fast u m*)
280 and add_gt_arc_fast u v m =
282 let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
283 let m' = MAL.add u ru' m in
284 let rv = repr v m' in
285 let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
286 let m'' = MAL.add v rv' m' in
289 and add_ge_arc_fast u v m =
291 let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
292 let m' = MAL.add u ru' m in
293 let rv = repr v m' in
294 let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
295 let m'' = MAL.add v rv' m' in
298 and add_eq_arc_fast u v m =
301 let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
302 (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
303 let m' = MAL.add u ru' m in
304 let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
305 (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
306 let m'' = MAL.add v rv' m' in
307 adjust_fast v (*(adjust_fast u*) m'' (* ) *)
311 (*****************************************************************************)
312 (** safe implementation **)
313 (*****************************************************************************)
318 let j = ru.one_s_eq in
319 let _Uj = merge_closures (fun x -> x.eq_closure) j m in
320 let one_step_eq = ru.one_s_eq in
321 (SOF.union one_step_eq _Uj)
324 let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
325 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
330 let j = ru.one_s_gt in
331 let k = ru.one_s_ge in
332 let l = ru.one_s_eq in
333 let _Uj = merge_closures (fun x -> x.ge_closure) j m in
334 let _Uk = merge_closures (fun x -> x.gt_closure) k m in
335 let _Ul = merge_closures (fun x -> x.gt_closure) l m in
336 let one_step_gt = ru.one_s_gt in
337 (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
343 in_gegt_of = ru.in_gegt_of;
344 one_s_eq = ru.one_s_eq;
345 one_s_ge = ru.one_s_ge;
346 one_s_gt = ru.one_s_gt
349 let rec simple_adjust m =
351 MAL.mapi (fun x _ -> closure_of x m) m
353 if not (are_ugraph_eq m m') then(
358 let add_eq_arc u v m =
361 let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
362 let m' = MAL.add u ru' m in
363 let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
364 let m'' = MAL.add v rv' m' in
367 let add_ge_arc u v m =
369 let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
370 let m' = MAL.add u ru' m in
373 let add_gt_arc u v m =
375 let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
376 let m' = MAL.add u ru' m in
380 (*****************************************************************************)
381 (** Outhern interface, that chooses between _fast and safe **)
382 (*****************************************************************************)
385 given the 2 nodes plus the current bag, adds the arc, recomputes the
386 closures and returns the new map
388 let add_eq fast u v b =
390 add_eq_arc_fast u v b
395 given the 2 nodes plus the current bag, adds the arc, recomputes the
396 closures and returns the new map
398 let add_ge fast u v b =
400 add_ge_arc_fast u v b
404 given the 2 nodes plus the current bag, adds the arc, recomputes the
405 closures and returns the new map
407 let add_gt fast u v b =
409 add_gt_arc_fast u v b
414 (*****************************************************************************)
415 (** Other real code **)
416 (*****************************************************************************)
418 exception UniverseInconsistency of string
420 let error arc node1 closure_type node2 closure =
421 let s = "\n ===== Universe Inconsistency detected =====\n\n" ^
423 "\t" ^ (string_of_arc arc) ^ "\n" ^
425 "\t" ^ (string_of_universe node1) ^ "\n" ^
426 " is in the " ^ closure_type ^ " closure\n" ^
427 "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^
429 "\t" ^ (string_of_universe node2) ^ "\n\n" ^
430 " ===== Universe Inconsistency detected =====\n" in
432 raise (UniverseInconsistency s)
435 let fill_empty_nodes_with_uri g uri =
436 let fill_empty_universe u =
438 (i,None) -> (i,Some uri)
439 | (i,Some _) as u -> u
441 let fill_empty_set s =
442 SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
444 let fill_empty_entry e = {
445 eq_closure = (fill_empty_set e.eq_closure) ;
446 ge_closure = (fill_empty_set e.ge_closure) ;
447 gt_closure = (fill_empty_set e.gt_closure) ;
448 in_gegt_of = (fill_empty_set e.in_gegt_of) ;
449 one_s_eq = (fill_empty_set e.one_s_eq) ;
450 one_s_ge = (fill_empty_set e.one_s_ge) ;
451 one_s_gt = (fill_empty_set e.one_s_gt) ;
456 MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
461 (*****************************************************************************)
462 (** World interface **)
463 (*****************************************************************************)
465 type universe_graph = bag
467 let empty_ugraph = empty_bag
469 let current_index_anon = ref (-1)
470 let current_index_named = ref (-1)
472 let restart_numbering () = current_index_named := (-1)
478 current_index_anon := !current_index_anon + 1;
481 current_index_named := !current_index_named + 1;
487 prerr_endline (string_of_bag g)
489 let add_eq ?(fast=(!fast_implementation)) u v b =
490 (* should we check to no add twice the same?? *)
493 if SOF.mem v ru.gt_closure then
494 error ("EQ",u,v) v "GT" u ru.gt_closure
498 if SOF.mem u rv.gt_closure then
499 error ("EQ",u,v) u "GT" v rv.gt_closure
504 let add_ge ?(fast=(!fast_implementation)) u v b =
505 (* should we check to no add twice the same?? *)
508 if SOF.mem u rv.gt_closure then
509 error ("GE",u,v) u "GT" v rv.gt_closure
513 let add_gt ?(fast=(!fast_implementation)) u v b =
514 (* should we check to no add twice the same?? *)
516 FIXME : check the thesis... no need to check GT and EQ closure since the
517 GE is a superset of both
523 error ("GT",u,v) u "==" v SOF.empty
526 (*if SOF.mem u rv.gt_closure then
527 error ("GT",u,v) u "GT" v rv.gt_closure
530 if SOF.mem u rv.ge_closure then
531 error ("GT",u,v) u "GE" v rv.ge_closure
534 if SOF.mem u rv.eq_closure then
535 error ("GT",u,v) u "EQ" v rv.eq_closure
541 (*****************************************************************************)
542 (** START: Decomment this for performance comparisons **)
543 (*****************************************************************************)
545 let add_eq ?(fast=(!fast_implementation)) u v b =
547 let rc = add_eq ~fast u v b in
551 let add_ge ?(fast=(!fast_implementation)) u v b =
553 let rc = add_ge ~fast u v b in
557 let add_gt ?(fast=(!fast_implementation)) u v b =
559 let rc = add_gt ~fast u v b in
563 (*****************************************************************************)
564 (** END: Decomment this for performance comparisons **)
565 (*****************************************************************************)
567 let merge_ugraphs u v =
569 let merge_brutal u v =
570 if u = empty_bag then v
571 else if v = empty_bag then u
579 let m = add_gt k u x in m) v.one_s_gt
582 let m = add_ge k u x in m) v.one_s_ge
585 let m = add_eq k u x in m) v.one_s_eq x)))
591 (*****************************************************************************)
592 (** Xml sesialization and parsing **)
593 (*****************************************************************************)
600 Xml.xml_empty "node" [
601 None,"id",(string_of_int i) ;
602 None,"uri",(UriManager.string_of_uri u)]
604 raise (Failure "we can serialize only universes with uri")
607 List.fold_left (fun s x -> [< s ; x >] ) [<>] l
609 let xml_of_entry_content e =
610 let stream_of_field f name =
611 let eq_c = xml_of_set f in
613 Xml.xml_nempty name [] eq_c
618 (stream_of_field e.eq_closure "eq_closure");
619 (stream_of_field e.gt_closure "gt_closure");
620 (stream_of_field e.ge_closure "ge_closure");
621 (stream_of_field e.in_gegt_of "in_gegt_of");
622 (stream_of_field e.one_s_eq "one_s_eq");
623 (stream_of_field e.one_s_gt "one_s_gt");
624 (stream_of_field e.one_s_ge "one_s_ge")
627 let xml_of_entry u e =
633 raise (Failure "we can serialize only universes (entry) with uri")
635 let ent = Xml.xml_nempty "entry" [
636 None,"id",(string_of_int i) ;
637 None,"uri",(UriManager.string_of_uri u'')] in
638 let content = xml_of_entry_content e in
641 let write_xml_of_ugraph filename m =
642 let o = open_out filename in
643 output_string o "<?xml version=\"1.0\" encoding=\"iso-8859-1\" ?>\n";
645 Xml.xml_nempty "ugraph" [] (
647 fun k v s -> [< s ; (xml_of_entry k v) >])
651 let rec clean_ugraph m f =
653 MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
654 let m'' = MAL.fold (fun k v x ->
656 eq_closure = SOF.filter f v.eq_closure;
657 ge_closure = SOF.filter f v.ge_closure;
658 gt_closure = SOF.filter f v.gt_closure;
659 in_gegt_of = SOF.filter f v.in_gegt_of;
660 one_s_eq = SOF.filter f v.one_s_eq;
661 one_s_ge = SOF.filter f v.one_s_ge;
662 one_s_gt = SOF.filter f v.one_s_gt
664 MAL.add k v' x ) m' MAL.empty in
666 MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' []
669 clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
673 let clean_ugraph g l =
674 clean_ugraph g (fun u -> List.mem u l)
680 "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
681 | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
682 | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
683 | "in_gegt_of" -> (fun e u->{e with in_gegt_of =SOF.add u e.in_gegt_of})
684 | "one_s_ge" -> (fun e u->{e with one_s_ge =SOF.add u e.one_s_ge})
685 | "one_s_gt" -> (fun e u->{e with one_s_gt =SOF.add u e.one_s_gt})
686 | "one_s_eq" -> (fun e u->{e with one_s_eq =SOF.add u e.one_s_eq})
687 | s -> raise (Failure ("unsupported tag " ^ s))
691 let current_node = ref (0,None) in
692 let current_entry = ref empty_entry in
693 let current_assign = ref (assigner_of "in_ge_of") in
695 | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
696 | E_start_tag ("entry",attlist,_,_) ->
697 let id = List.assoc "id" attlist in
698 let uri = List.assoc "uri" attlist in
699 current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
700 | E_start_tag ("node",attlist,_,_) ->
701 let id = int_of_string (List.assoc "id" attlist) in
702 let uri = List.assoc "uri" attlist in
703 current_entry := !current_assign !current_entry
704 (id,Some (UriManager.uri_of_string uri))
705 | E_start_tag (s,_,_,_) ->
706 current_assign := assigner_of s
707 | E_end_tag ("entry",_) ->
708 m := MAL.add !current_node !current_entry !m;
709 current_entry := empty_entry
713 (* alternative implementation *)
715 ("ge_closure",0);("gt_closure",1);("eq_closure",2);
717 ("one_s_ge", 4);("one_s_gt", 5);("one_s_eq", 6)]
720 let assigner_of' s = List.assoc s mapl ;;
722 let entry_of_array a = {
723 ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
725 one_s_ge = a.(4); one_s_gt = a.(5); one_s_eq = a.(6)}
729 let current_node = ref (0,None) in
730 let current_entry = Array.create 7 SOF.empty in
731 let current_assign = ref 0 in
733 | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
734 | E_start_tag ("entry",attlist,_,_) ->
735 let id = List.assoc "id" attlist in
736 let uri = List.assoc "uri" attlist in
737 current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
738 | E_start_tag ("node",attlist,_,_) ->
739 let id = int_of_string (List.assoc "id" attlist) in
740 let uri = List.assoc "uri" attlist in
741 current_entry.(!current_assign) <-
742 SOF.add (id,Some (UriManager.uri_of_string uri))
743 current_entry.(!current_assign)
744 | E_start_tag (s,_,_,_) ->
745 current_assign := assigner_of' s
746 | E_end_tag ("entry",_) ->
747 m := MAL.add !current_node (entry_of_array current_entry) !m;
748 Array.fill current_entry 0 7 SOF.empty
753 let ugraph_of_xml filename =
754 let module PX = Pxp_ev_parser in
755 let module NE = Netconversion in
756 let config = default_config in
757 let entry = `Entry_document [] in
758 let encoding = `Enc_iso88591 in
759 let source = from_file ~system_encoding:encoding filename in
761 PX.create_entity_manager ~is_document:true config source in
762 let result = ref MAL.empty in
763 let cb = cb_factory result in
764 (*let cb = cb_factory' result in*)
765 PX.process_entity config entry entity_manager cb;
769 (*****************************************************************************)
770 (** the main, only for testing **)
771 (*****************************************************************************)
775 type arc = Ge | Gt | Eq ;;
777 let randomize_actionlist n m =
778 let ge_percent = 0.7 in
779 let gt_percent = 0.15 in
781 let node1 = Random.int m in
782 let node2 = Random.int m in
784 let r = Random.float 1.0 in
785 if r < ge_percent then
787 else (if r < (ge_percent +. gt_percent) then
797 | n -> (random_step ())::(aux (n-1))
801 let print_action_list l =
802 let string_of_step (op,node1,node2) =
807 "," ^ (string_of_int node1) ^ "," ^ (string_of_int node2)
813 ";" ^ (string_of_step a) ^ (aux tl)
816 let l_body = (String.length body) - 1 in
817 prerr_endline ("[" ^ (String.sub body 1 l_body))
820 let d_print_endline = if debug then print_endline else ignore
821 let d_print_ugraph = if debug then print_ugraph else ignore
824 (if Array.length Sys.argv < 2 then
825 prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
827 let max_edges = int_of_string Sys.argv.(1) in
828 let max_nodes = int_of_string Sys.argv.(2) in
829 let action_listR = randomize_actionlist max_edges max_nodes in
831 let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
832 let action_list = action_listR in
834 print_action_list action_list;
835 let prform_step ?(fast=false) (t,u,v) g =
847 let g' = f ~fast (u,None) (v,None) g in
848 (*print_ugraph g' ;*)
851 let fail = ref false in
852 let time1 = Unix.gettimeofday () in
853 let n_safe = ref 0 in
856 d_print_endline "SAFE";
859 n_safe := !n_safe + 1;
861 ) empty_ugraph action_list
863 UniverseInconsistency s -> fail:=true;empty_bag
865 let time2 = Unix.gettimeofday () in
866 d_print_ugraph g_safe;
867 let time3 = Unix.gettimeofday () in
868 let n_test = ref 0 in
871 d_print_endline "FAST";
874 n_test := !n_test + 1;
875 prform_step ~fast:true e g
876 ) empty_ugraph action_list
878 UniverseInconsistency s -> empty_bag
880 let time4 = Unix.gettimeofday () in
881 d_print_ugraph g_test;
882 if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
887 if e = Eq then s+1 else s
893 if e = Gt then s+1 else s
896 let num_ge = max_edges - num_gt - num_eq in
897 let time_fast = (time4 -. time3) in
898 let time_safe = (time2 -. time1) in
899 let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
900 let fail = if !fail then 1 else 0 in
903 "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d"
904 fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
909 print_endline "FAIL";
922 i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
924 let recons_entry entry =
926 SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
929 eq_closure = recons_set entry.eq_closure;
930 ge_closure = recons_set entry.ge_closure;
931 gt_closure = recons_set entry.gt_closure;
932 in_gegt_of = recons_set entry.in_gegt_of;
933 one_s_eq = recons_set entry.one_s_eq;
934 one_s_ge = recons_set entry.one_s_ge;
935 one_s_gt = recons_set entry.one_s_gt;
938 let recons_graph graph =
940 (fun universe entry map ->
941 MAL.add (recons_univ universe) (recons_entry entry) map)
946 | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
949 let assert_univs_have_uri graph =
951 SOF.iter (fun u -> assert_univ u) s
954 assert_set e.eq_closure;
955 assert_set e.ge_closure;
956 assert_set e.gt_closure;
957 assert_set e.in_gegt_of;
958 assert_set e.one_s_eq;
959 assert_set e.one_s_ge;
960 assert_set e.one_s_gt;
962 MAL.iter (fun k v -> assert_univ k; assert_entry v)graph