]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicUniv.ml
uses Map.equal to compare universes
[helm.git] / helm / ocaml / cic / cicUniv.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*****************************************************************************)
27 (*                                                                           *)
28 (*                               PROJECT HELM                                *)
29 (*                                                                           *)
30 (*                      Enrico Tassi <tassi@cs.unibo.it>                     *)
31 (*                                 23/04/2004                                *)
32 (*                                                                           *)
33 (* This module implements the aciclic graph of universes.                    *)
34 (*                                                                           *)
35 (*****************************************************************************)
36
37 (*****************************************************************************)
38 (** switch implementation                                                   **)
39 (*****************************************************************************)
40
41 let fast_implementation = ref false ;;
42
43 (*****************************************************************************)
44 (** open                                                                    **)
45 (*****************************************************************************)
46
47 open Printf
48
49 (*****************************************************************************)
50 (** Types and default values                                                **)
51 (*****************************************************************************)
52
53 type universe = int * UriManager.uri option 
54     
55 module UniverseType = struct
56   type t = universe
57   let compare = Pervasives.compare
58 end
59   
60 module SOF = Set.Make(UniverseType)
61   
62 type entry = {
63   eq_closure : SOF.t;
64   ge_closure : SOF.t;
65   gt_closure : SOF.t;
66   in_gegt_of   : SOF.t;
67   one_s_eq   : SOF.t;
68   one_s_ge   : SOF.t;
69   one_s_gt   : SOF.t;
70 }
71     
72 module MAL = Map.Make(UniverseType)
73   
74 type arc_type = GE | GT | EQ
75     
76 type bag = entry MAL.t 
77     
78 let empty_entry = {
79   eq_closure=SOF.empty;
80   ge_closure=SOF.empty;
81   gt_closure=SOF.empty;
82   in_gegt_of=SOF.empty;
83   one_s_eq=SOF.empty;
84   one_s_ge=SOF.empty;
85   one_s_gt=SOF.empty;
86 }
87 let empty_bag = MAL.empty
88
89 let are_set_eq s1 s2 = 
90   SOF.equal s1 s2
91
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 )
100
101 let are_ugraph_eq = MAL.equal are_entry_eq
102
103 (*****************************************************************************)
104 (** Pretty printings                                                        **)
105 (*****************************************************************************)
106
107 let string_of_universe (i,u) = 
108   match u with
109       Some u ->
110         "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
111     | None -> "(" ^ (string_of_int i) ^ ",None)"
112
113 let string_of_universe_set l = 
114   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
115
116 let string_of_node n =
117   "{"^
118   "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ 
119   "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ 
120   "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ 
121   "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
122
123 let string_of_arc (a,u,v) = 
124   (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
125   
126 let string_of_mal m =
127   let rc = ref "" in
128   MAL.iter (fun k v ->  
129     rc := !rc ^ sprintf "%s --> %s" (string_of_universe k) 
130               (string_of_node v)) m;
131   !rc
132
133 let string_of_bag b = 
134   string_of_mal b
135
136 (*****************************************************************************)
137 (** Helpers                                                                 **)
138 (*****************************************************************************)
139
140 (* find the repr *)
141 let repr u m =
142   try 
143     MAL.find u m
144   with
145     Not_found -> empty_entry
146     
147 (* FIXME: May be faster if we make it by hand *)
148 let merge_closures f nodes m =  
149   SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
150
151 (*****************************************************************************)
152 (** Benchmarking                                                            **)
153 (*****************************************************************************)
154 let time_spent = ref 0.0;;
155 let partial = ref 0.0 ;;
156
157 let reset_spent_time () = time_spent := 0.0;;
158 let get_spent_time () = !time_spent ;;
159 let begin_spending () =
160   (*assert (!partial = 0.0);*)
161   partial := Unix.gettimeofday ()
162 ;;
163
164 let end_spending () =
165   assert (!partial > 0.0);
166   let interval = (Unix.gettimeofday ()) -. !partial in
167     partial := 0.0;
168     time_spent := !time_spent +. interval
169 ;;
170   
171 \f
172 (*****************************************************************************)
173 (** _fats implementation                                                    **)
174 (*****************************************************************************)
175
176 let rec closure_of_fast ru m =
177   let eq_c = closure_eq_fast ru m in
178   let ge_c = closure_ge_fast ru m in
179   let gt_c = closure_gt_fast ru m in
180     {
181       eq_closure = eq_c;
182       ge_closure = ge_c;
183       gt_closure = gt_c;
184       in_gegt_of = ru.in_gegt_of;
185       one_s_eq = ru.one_s_eq;
186       one_s_ge = ru.one_s_ge;
187       one_s_gt = ru.one_s_gt
188     }
189       
190 and closure_eq_fast ru m = 
191   let eq_c =
192     let j = ru.one_s_eq in
193     let _Uj = merge_closures (fun x -> x.eq_closure) j m in
194     let one_step_eq = ru.one_s_eq in
195       (SOF.union one_step_eq _Uj)
196   in
197     eq_c
198       
199 and closure_ge_fast ru m =
200   let ge_c = 
201     let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
202     let _Uj = merge_closures (fun x -> x.ge_closure) j m in
203     let _Ux = j in
204       (SOF.union _Uj _Ux)
205   in
206     ge_c
207       
208 and closure_gt_fast ru m =
209   let gt_c =
210     let j = ru.one_s_gt in
211     let k = ru.one_s_ge in
212     let l = ru.one_s_eq in
213     let _Uj = merge_closures (fun x -> x.ge_closure) j m in
214     let _Uk = merge_closures (fun x -> x.gt_closure) k m in
215     let _Ul = merge_closures (fun x -> x.gt_closure) l m in
216     let one_step_gt = ru.one_s_gt in
217       (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
218   in
219     gt_c
220       
221 and print_rec_status u ru =
222   print_endline ("Aggiusto " ^ (string_of_universe u) ^ 
223                  "e ottengo questa chiusura\n " ^ (string_of_node ru))
224
225 and adjust_fast u m =
226   let ru = repr u m in
227   let gt_c = closure_gt_fast ru m in
228   let ge_c = closure_ge_fast ru m in
229   let eq_c = closure_eq_fast ru m in
230   let changed_eq = not (are_set_eq eq_c ru.eq_closure) in
231   let changed_gegt = 
232     (not (are_set_eq gt_c ru.gt_closure)) || 
233     (not (are_set_eq ge_c ru.ge_closure))
234   in
235     if ((not changed_gegt) &&  (not changed_eq)) then
236       m
237     else
238       begin
239         let ru' = {
240           eq_closure = eq_c;
241           ge_closure = ge_c;
242           gt_closure = gt_c;
243           in_gegt_of = ru.in_gegt_of;
244           one_s_eq = ru.one_s_eq;
245           one_s_ge = ru.one_s_ge;
246           one_s_gt = ru.one_s_gt}
247         in
248         let m = MAL.add u ru' m in
249         let m =
250             SOF.fold (fun x m -> adjust_fast  x m) 
251               (SOF.union ru'.eq_closure ru'.in_gegt_of) m
252               (* TESI: 
253                    ru'.in_gegt_of m 
254               *)
255         in
256           m (*adjust_fast  u m*)
257       end
258         
259 and add_gt_arc_fast u v m =
260   let ru = repr u m in
261   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
262   let m' = MAL.add u ru' m in
263   let rv = repr v m' in
264   let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
265   let m'' = MAL.add v rv' m' in
266     adjust_fast u m''
267       
268 and add_ge_arc_fast u v m =
269   let ru = repr u m in
270   let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
271   let m' = MAL.add u ru' m in
272   let rv = repr v m' in
273   let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
274   let m'' = MAL.add v rv' m' in
275     adjust_fast u m''
276
277 and add_eq_arc_fast u v m =
278   let ru = repr u m in
279   let rv = repr v m in 
280   let ru' = {ru  with one_s_eq = SOF.add v ru.one_s_eq} in
281   (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
282   let m' = MAL.add u ru' m in
283   let rv' = {rv  with one_s_eq = SOF.add u rv.one_s_eq} in
284   (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
285   let m'' = MAL.add v rv' m' in
286     adjust_fast v (*(adjust_fast u*) m'' (* ) *)
287 ;;
288
289 \f
290 (*****************************************************************************)
291 (** safe implementation                                                     **)
292 (*****************************************************************************)
293
294 let closure_of u m =
295   let ru = repr u m in
296   let eq_c =
297     let j = ru.one_s_eq in
298     let _Uj = merge_closures (fun x -> x.eq_closure) j m in
299     let one_step_eq = ru.one_s_eq in
300             (SOF.union one_step_eq _Uj)
301   in
302   let ge_c = 
303     let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
304     let _Uj = merge_closures (fun x -> x.ge_closure) j m in
305     let _Ux = j in
306       (SOF.union _Uj _Ux)
307   in
308   let gt_c =
309     let j = ru.one_s_gt in
310     let k = ru.one_s_ge in
311     let l = ru.one_s_eq in
312     let _Uj = merge_closures (fun x -> x.ge_closure) j m in
313     let _Uk = merge_closures (fun x -> x.gt_closure) k m in
314     let _Ul = merge_closures (fun x -> x.gt_closure) l m in
315     let one_step_gt = ru.one_s_gt in
316       (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
317   in
318     {
319       eq_closure = eq_c;
320       ge_closure = ge_c;
321       gt_closure = gt_c;
322       in_gegt_of = ru.in_gegt_of;
323       one_s_eq = ru.one_s_eq;
324       one_s_ge = ru.one_s_ge;
325       one_s_gt = ru.one_s_gt
326     }
327
328 let rec simple_adjust m =
329   let m' = 
330     MAL.mapi (fun x _ -> closure_of x m) m
331   in
332     if not (are_ugraph_eq m  m') then(
333       simple_adjust m')
334     else
335       m'
336
337 let add_eq_arc u v m =
338   let ru = repr u m in
339   let rv = repr v m in
340   let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
341   let m' = MAL.add u ru' m in
342   let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
343   let m'' = MAL.add v rv' m' in
344     simple_adjust m''
345
346 let add_ge_arc u v m =
347   let ru = repr u m in
348   let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
349   let m' = MAL.add u ru' m in
350     simple_adjust m'
351
352 let add_gt_arc u v m =
353   let ru = repr u m in
354   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
355   let m' = MAL.add u ru' m in
356     simple_adjust m'
357
358 \f
359 (*****************************************************************************)
360 (** Outhern interface, that chooses between _fast and safe                  **)
361 (*****************************************************************************)
362
363 (*                                                                            
364     given the 2 nodes plus the current bag, adds the arc, recomputes the 
365     closures and returns the new map
366 *) 
367 let add_eq fast u v b =
368   if fast then
369     add_eq_arc_fast u v b
370   else
371     add_eq_arc u v b
372
373 (*                                                                            
374     given the 2 nodes plus the current bag, adds the arc, recomputes the 
375     closures and returns the new map
376 *) 
377 let add_ge fast u v b =
378   if fast then
379     add_ge_arc_fast u v b
380   else
381     add_ge_arc u v b
382 (*                                                                            
383     given the 2 nodes plus the current bag, adds the arc, recomputes the 
384     closures and returns the new map
385 *)                                                                            
386 let add_gt fast u v b =
387   if fast then
388     add_gt_arc_fast u v b
389   else
390     add_gt_arc u v b
391
392
393 (*****************************************************************************)
394 (** Other real code                                                         **)
395 (*****************************************************************************)
396
397 exception UniverseInconsistency of string 
398
399 let error arc node1 closure_type node2 closure =
400   let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
401    "   Unable to add\n" ^ 
402    "\t" ^ (string_of_arc arc) ^ "\n" ^
403    "   cause\n" ^ 
404    "\t" ^ (string_of_universe node1) ^ "\n" ^
405    "   is in the " ^ closure_type ^ " closure\n" ^
406    "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
407    "   of\n" ^ 
408    "\t" ^ (string_of_universe node2) ^ "\n\n" ^
409    "  ===== Universe Inconsistency detected =====\n" in
410   prerr_endline s;
411   raise (UniverseInconsistency s)
412
413
414 let fill_empty_nodes_with_uri g uri =
415   let fill_empty_universe u =
416     match u with
417         (i,None) -> (i,Some uri)
418       | (i,Some _) as u -> u
419   in
420   let fill_empty_set s =
421     SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty 
422   in
423   let fill_empty_entry e = {
424     eq_closure = (fill_empty_set e.eq_closure) ;
425     ge_closure = (fill_empty_set e.ge_closure) ;
426     gt_closure = (fill_empty_set e.gt_closure) ;
427     in_gegt_of = (fill_empty_set e.in_gegt_of) ;
428     one_s_eq = (fill_empty_set e.one_s_eq) ;
429     one_s_ge = (fill_empty_set e.one_s_ge) ;
430     one_s_gt = (fill_empty_set e.one_s_gt) ;
431   } in  
432   let m = g in
433   let m' = MAL.fold (
434     fun k v m -> 
435       MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
436   in
437     m'
438
439
440 (*****************************************************************************)
441 (** World interface                                                         **)
442 (*****************************************************************************)
443
444 type universe_graph = bag
445
446 let empty_ugraph = empty_bag
447
448 let current_index_anon = ref (-1)
449 let current_index_named = ref (-1)
450
451 let restart_numbering () = current_index_named := (-1) 
452
453 let fresh ?uri () =
454   let i =
455     match uri with
456     | None -> 
457         current_index_anon := !current_index_anon + 1;
458         !current_index_anon
459     | Some _ -> 
460         current_index_named := !current_index_named + 1;
461         !current_index_named
462   in
463   (i,uri)
464
465 let print_ugraph g = 
466   prerr_endline (string_of_bag g)
467
468 let add_eq ?(fast=(!fast_implementation)) u v b =
469   (* should we check to no add twice the same?? *)
470   let m = b in
471   let ru = repr u m in
472   if SOF.mem v ru.gt_closure then
473     error ("EQ",u,v) v "GT" u ru.gt_closure
474   else
475     begin
476     let rv = repr v m in
477     if SOF.mem u rv.gt_closure then
478       error ("EQ",u,v) u "GT" v rv.gt_closure
479     else
480       add_eq fast u v b
481     end
482
483 let add_ge ?(fast=(!fast_implementation)) u v b =
484   (* should we check to no add twice the same?? *)
485   let m = b in
486   let rv = repr v m in
487   if SOF.mem u rv.gt_closure then
488     error ("GE",u,v) u "GT" v rv.gt_closure
489   else
490     add_ge fast u v b
491   
492 let add_gt ?(fast=(!fast_implementation)) u v b =
493   (* should we check to no add twice the same?? *)
494   (* 
495      FIXME : check the thesis... no need to check GT and EQ closure since the 
496      GE is a superset of both 
497   *)
498   let m = b in
499   let rv = repr v m in
500
501   if u = v then
502     error ("GT",u,v) u "==" v SOF.empty
503   else
504   
505   (*if SOF.mem u rv.gt_closure then
506     error ("GT",u,v) u "GT" v rv.gt_closure
507   else
508     begin*)
509       if SOF.mem u rv.ge_closure then
510         error ("GT",u,v) u "GE" v rv.ge_closure
511       else
512 (*        begin
513           if SOF.mem u rv.eq_closure then
514             error ("GT",u,v) u "EQ" v rv.eq_closure
515           else*)
516             add_gt fast u v b
517 (*        end
518     end*)
519
520 (*****************************************************************************)
521 (** START: Decomment this for performance comparisons                       **)
522 (*****************************************************************************)
523
524 let add_eq ?(fast=(!fast_implementation))  u v b =
525   begin_spending ();
526   let rc = add_eq ~fast u v b in
527     end_spending();
528     rc
529
530 let add_ge ?(fast=(!fast_implementation)) u v b =
531   begin_spending ();
532   let rc = add_ge ~fast u v b in
533  end_spending();
534     rc
535     
536 let add_gt ?(fast=(!fast_implementation)) u v b =
537   begin_spending ();
538   let rc = add_gt ~fast u v b in
539     end_spending();
540     rc
541
542 (*****************************************************************************)
543 (** END: Decomment this for performance comparisons                         **)
544 (*****************************************************************************)
545
546 let merge_ugraphs u v =
547   (* this sucks *)
548   let merge_brutal u v =
549     if u = empty_bag then v 
550     else if v = empty_bag then u 
551     else
552       let m1 = u in 
553       let m2 = v in 
554         MAL.fold (
555           fun k v x -> 
556             (SOF.fold (
557                fun u x -> 
558                  let m = add_gt k u x in m) v.one_s_gt 
559                (SOF.fold (
560                   fun u x -> 
561                     let m = add_ge k u x in m) v.one_s_ge
562                   (SOF.fold (
563                      fun u x -> 
564                        let m = add_eq k u x in m) v.one_s_eq x)))
565         ) m1 m2
566   in
567     merge_brutal u v
568
569
570 (*****************************************************************************)
571 (** Xml sesialization and parsing                                           **)
572 (*****************************************************************************)
573
574 let xml_of_set s =
575   let l = 
576     List.map (
577       function 
578           (i,Some u) -> 
579             Xml.xml_empty "node" [
580               None,"id",(string_of_int i) ;
581               None,"uri",(UriManager.string_of_uri u)]
582         | (_,None) -> 
583             raise (Failure "we can serialize only universes with uri")
584     ) (SOF.elements s) 
585   in
586     List.fold_left (fun s x -> [< s ; x >] ) [<>] l
587       
588 let xml_of_entry_content e =
589   let stream_of_field f name =
590     let eq_c = xml_of_set f in
591     if eq_c != [<>] then
592       Xml.xml_nempty name [] eq_c
593     else
594       [<>]
595   in
596   [<
597     (stream_of_field e.eq_closure "eq_closure");
598     (stream_of_field e.gt_closure "gt_closure");
599     (stream_of_field e.ge_closure "ge_closure");
600     (stream_of_field e.in_gegt_of "in_gegt_of");
601     (stream_of_field e.one_s_eq "one_s_eq");
602     (stream_of_field e.one_s_gt "one_s_gt");
603     (stream_of_field e.one_s_ge "one_s_ge")
604   >]
605
606 let xml_of_entry u e =
607   let (i,u') = u in
608   let u'' = 
609     match u' with 
610         Some x -> x 
611       | None -> 
612           raise (Failure "we can serialize only universes (entry) with uri")
613   in
614   let ent = Xml.xml_nempty "entry" [
615     None,"id",(string_of_int i) ; 
616     None,"uri",(UriManager.string_of_uri u'')] in
617   let content = xml_of_entry_content e in
618   ent content
619
620 let write_xml_of_ugraph filename m =
621     let o = open_out filename in
622     output_string o "<?xml version=\"1.0\" encoding=\"iso-8859-1\" ?>\n";
623     Xml.pp_to_outchan (
624       Xml.xml_nempty "ugraph" [] (
625       MAL.fold (
626         fun k v s -> [< s ; (xml_of_entry k v) >])
627       m [<>])) o;
628     close_out o
629  
630 let rec clean_ugraph m f =
631   let m' = 
632     MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
633   let m'' =  MAL.fold (fun k v x -> 
634     let v' = {
635       eq_closure = SOF.filter f v.eq_closure;
636       ge_closure = SOF.filter f v.ge_closure;
637       gt_closure = SOF.filter f v.gt_closure;
638       in_gegt_of = SOF.filter f v.in_gegt_of;
639       one_s_eq = SOF.filter f v.one_s_eq;
640       one_s_ge = SOF.filter f v.one_s_ge;
641       one_s_gt = SOF.filter f v.one_s_gt
642     } in 
643     MAL.add k v' x ) m' MAL.empty in
644   let e_l = 
645     MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' []
646   in
647     if e_l != [] then
648       clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
649     else
650       m''
651
652 let clean_ugraph g l =
653   clean_ugraph g (fun u -> List.mem u l)
654
655 let assigner_of = 
656   function
657     "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
658   | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
659   | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
660   | "in_gegt_of"   -> (fun e u->{e with in_gegt_of  =SOF.add u e.in_gegt_of})
661   | "one_s_ge"   -> (fun e u->{e with one_s_ge  =SOF.add u e.one_s_ge})
662   | "one_s_gt"   -> (fun e u->{e with one_s_gt  =SOF.add u e.one_s_gt})
663   | "one_s_eq"   -> (fun e u->{e with one_s_eq  =SOF.add u e.one_s_eq})
664   | s -> raise (Failure ("unsupported tag " ^ s))
665 ;;
666
667 let cb_factory m = 
668   let module XPP = XmlPushParser in
669   let current_node = ref (0,None) in
670   let current_entry = ref empty_entry in
671   let current_assign = ref (assigner_of "in_ge_of") in
672   { XPP.default_callbacks with
673     XPP.end_element = Some( fun name ->
674       match name with
675       | "entry" -> 
676           m := MAL.add !current_node !current_entry !m;
677           current_entry := empty_entry
678       | _ -> ()
679     );
680     XPP.start_element = Some( fun name attlist ->
681       match name with
682       | "entry" -> 
683           let id = List.assoc "id" attlist in      
684           let uri = List.assoc "uri" attlist in
685           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
686       | "node" -> 
687           let id = int_of_string (List.assoc "id" attlist) in
688           let uri = List.assoc "uri" attlist in        
689             current_entry := !current_assign !current_entry 
690               (id,Some (UriManager.uri_of_string uri))
691       | s -> current_assign := assigner_of s
692     )
693   }
694 ;; 
695
696 (* alternative implementation *)
697 let mapl = [
698   ("ge_closure",0);("gt_closure",1);("eq_closure",2);
699   ("in_gegt_of",  3);
700   ("one_s_ge",  4);("one_s_gt",  5);("one_s_eq",  6)]
701 ;;
702
703 let assigner_of' s = List.assoc s mapl ;;
704
705 let entry_of_array a = { 
706   ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
707   in_gegt_of   = a.(3); 
708   one_s_ge   = a.(4); one_s_gt   = a.(5); one_s_eq   = a.(6)}
709 ;;
710
711 let cb_factory' m = 
712   let module XPP = XmlPushParser in
713   let current_node = ref (0,None) in
714   let current_entry = Array.create 7 SOF.empty in
715   let current_assign = ref 0 in
716   { XPP.default_callbacks with
717     XPP.start_element = Some( fun name attlist ->
718       match name with
719       | "entry" -> 
720           let id = List.assoc "id" attlist in      
721           let uri = List.assoc "uri" attlist in
722           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
723       | "node" -> 
724           let id = int_of_string (List.assoc "id" attlist) in
725           let uri = List.assoc "uri" attlist in        
726           current_entry.(!current_assign) <- 
727             SOF.add (id,Some (UriManager.uri_of_string uri)) 
728               current_entry.(!current_assign) 
729       | s -> current_assign := assigner_of' s
730     );
731     XPP.end_element = Some( fun name -> 
732       match name with
733       | "entry" -> 
734           m := MAL.add !current_node (entry_of_array current_entry) !m;
735           Array.fill current_entry 0 7 SOF.empty 
736       | _ -> ()
737     );
738   }
739 ;;
740
741      
742 let ugraph_of_xml filename =
743   let module XPP = XmlPushParser in
744   let result = ref MAL.empty in
745   let cb = cb_factory result in
746 (*let cb = cb_factory' result in*)
747   let xml_parser = XPP.create_parser cb in
748   let xml_source = `Gzip_file filename in
749   (try XPP.parse xml_parser xml_source
750    with (XPP.Parse_error err) as exn -> raise exn);
751   !result
752
753 \f
754 (*****************************************************************************)
755 (** the main, only for testing                                              **)
756 (*****************************************************************************)
757
758 (* 
759
760 type arc = Ge | Gt | Eq ;;
761
762 let randomize_actionlist n m =
763   let ge_percent = 0.7 in
764   let gt_percent = 0.15 in
765   let random_step () =
766     let node1 = Random.int m in
767     let node2 = Random.int m in
768     let op = 
769       let r = Random.float 1.0 in
770         if r < ge_percent then 
771           Ge 
772         else (if r < (ge_percent +. gt_percent) then 
773           Gt 
774         else 
775           Eq) 
776     in
777       op,node1,node2      
778   in
779   let rec aux n =
780     match n with 
781         0 -> []
782       | n -> (random_step ())::(aux (n-1))
783   in
784     aux n
785
786 let print_action_list l =
787   let string_of_step (op,node1,node2) =
788     (match op with
789          Ge -> "Ge"
790        | Gt -> "Gt"
791        | Eq -> "Eq") ^ 
792     "," ^ (string_of_int node1) ^ ","   ^ (string_of_int node2) 
793   in
794   let rec aux l =
795     match l with 
796         [] -> "]"
797       | a::tl ->
798           ";" ^ (string_of_step a) ^ (aux tl)
799   in
800   let body = aux l in
801   let l_body = (String.length body) - 1 in
802     prerr_endline ("[" ^ (String.sub body 1 l_body))
803   
804 let debug = false
805 let d_print_endline = if debug then print_endline else ignore 
806 let d_print_ugraph = if debug then print_ugraph else ignore
807
808 let _ = 
809   (if Array.length Sys.argv < 2 then
810     prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
811   Random.self_init ();
812   let max_edges = int_of_string Sys.argv.(1) in
813   let max_nodes = int_of_string Sys.argv.(2) in
814   let action_listR = randomize_actionlist max_edges max_nodes in
815
816   let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
817   let action_list = action_listR in
818   
819   print_action_list action_list;
820   let prform_step ?(fast=false) (t,u,v) g =
821     let f,str = 
822       match t with
823           Ge -> add_ge,">="
824         | Gt -> add_gt,">"
825         | Eq -> add_eq,"="
826     in
827       d_print_endline (
828         "Aggiungo " ^ 
829         (string_of_int u) ^
830         " " ^ str ^ " " ^ 
831         (string_of_int v));
832       let g' = f ~fast (u,None) (v,None) g in
833         (*print_ugraph g' ;*)
834         g'
835   in
836   let fail = ref false in
837   let time1 = Unix.gettimeofday () in
838   let n_safe = ref 0 in
839   let g_safe =  
840     try 
841       d_print_endline "SAFE";
842       List.fold_left (
843         fun g e -> 
844           n_safe := !n_safe + 1;
845           prform_step e g
846       ) empty_ugraph action_list
847     with
848         UniverseInconsistency s -> fail:=true;empty_bag
849   in
850   let time2 = Unix.gettimeofday () in
851   d_print_ugraph g_safe;
852   let time3 = Unix.gettimeofday () in
853   let n_test = ref 0 in
854   let g_test = 
855     try
856       d_print_endline "FAST";
857       List.fold_left (
858         fun g e ->
859           n_test := !n_test + 1;
860           prform_step ~fast:true e g
861       ) empty_ugraph action_list
862     with
863         UniverseInconsistency s -> empty_bag
864   in
865   let time4 = Unix.gettimeofday () in
866   d_print_ugraph g_test;
867     if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
868       begin
869         let num_eq = 
870           List.fold_left (
871             fun s (e,_,_) -> 
872               if e = Eq then s+1 else s 
873           ) 0 action_list 
874         in
875         let num_gt = 
876           List.fold_left (
877             fun s (e,_,_) ->
878               if e = Gt then s+1 else s
879           ) 0 action_list
880         in
881         let num_ge = max_edges - num_gt - num_eq in
882         let time_fast = (time4 -. time3) in
883         let time_safe = (time2 -. time1) in
884         let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
885         let fail = if !fail then 1 else 0 in
886           print_endline 
887             (sprintf 
888                "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
889                fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
890           exit 0
891       end
892     else
893       begin
894         print_endline "FAIL";
895         print_ugraph g_safe;
896         print_ugraph g_test;
897         exit 1
898       end
899 ;;
900
901  *)
902
903 let recons_univ u =
904   match u with
905   | i, None -> u
906   | i, Some uri ->
907       i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
908
909 let recons_entry entry =
910   let recons_set set =
911     SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
912   in
913   {
914     eq_closure = recons_set entry.eq_closure;
915     ge_closure = recons_set entry.ge_closure;
916     gt_closure = recons_set entry.gt_closure;
917     in_gegt_of = recons_set entry.in_gegt_of;
918     one_s_eq = recons_set entry.one_s_eq;
919     one_s_ge = recons_set entry.one_s_ge;
920     one_s_gt = recons_set entry.one_s_gt;
921   }
922
923 let recons_graph graph =
924   MAL.fold
925     (fun universe entry map ->
926       MAL.add (recons_univ universe) (recons_entry entry) map)
927     graph MAL.empty
928
929 let assert_univ u =
930     match u with 
931     | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
932     | _ -> ()
933     
934 let assert_univs_have_uri graph =
935   let assert_set s =
936     SOF.iter (fun u -> assert_univ u) s
937   in
938   let assert_entry e =
939     assert_set e.eq_closure;
940     assert_set e.ge_closure;
941     assert_set e.gt_closure;
942     assert_set e.in_gegt_of;
943     assert_set e.one_s_eq;
944     assert_set e.one_s_ge;
945     assert_set e.one_s_gt;
946   in
947   MAL.iter (fun k v -> assert_univ k; assert_entry v)graph 
948   
949     
950 (* EOF *)