]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicUniv.ml
incomplete proof completed
[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
102 (* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *)
103 (*
104   let are_ugraph_eq308 g h =
105     MAL.equal are_entry_eq g h
106 *)
107 let are_ugraph_eq307 g h = 
108   try
109     MAL.fold (
110       fun k v b -> 
111         if not b then 
112           raise (Failure "Different") 
113         else
114           try
115             let k_h = MAL.find k h in
116             are_entry_eq v k_h
117           with Not_found -> true
118         ) g true
119     with 
120       Failure "Different" -> false
121
122 let are_ugraph_eq = are_ugraph_eq307
123
124 (*****************************************************************************)
125 (** Pretty printings                                                        **)
126 (*****************************************************************************)
127
128 let string_of_universe (i,u) = 
129   match u with
130       Some u ->
131         "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
132     | None -> "(" ^ (string_of_int i) ^ ",None)"
133
134 let string_of_universe_set l = 
135   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
136
137 let string_of_node n =
138   "{"^
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"
143
144 let string_of_arc (a,u,v) = 
145   (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
146   
147 let string_of_mal m =
148   let rc = ref "" in
149   MAL.iter (fun k v ->  
150     rc := !rc ^ sprintf "%s --> %s" (string_of_universe k) 
151               (string_of_node v)) m;
152   !rc
153
154 let string_of_bag b = 
155   string_of_mal b
156
157 (*****************************************************************************)
158 (** Helpers                                                                 **)
159 (*****************************************************************************)
160
161 (* find the repr *)
162 let repr u m =
163   try 
164     MAL.find u m
165   with
166     Not_found -> empty_entry
167     
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
171
172 (*****************************************************************************)
173 (** Benchmarking                                                            **)
174 (*****************************************************************************)
175 let time_spent = ref 0.0;;
176 let partial = ref 0.0 ;;
177
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 ()
183 ;;
184
185 let end_spending () =
186   assert (!partial > 0.0);
187   let interval = (Unix.gettimeofday ()) -. !partial in
188     partial := 0.0;
189     time_spent := !time_spent +. interval
190 ;;
191   
192 \f
193 (*****************************************************************************)
194 (** _fats implementation                                                    **)
195 (*****************************************************************************)
196
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
201     {
202       eq_closure = eq_c;
203       ge_closure = ge_c;
204       gt_closure = gt_c;
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
209     }
210       
211 and closure_eq_fast ru m = 
212   let eq_c =
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)
217   in
218     eq_c
219       
220 and closure_ge_fast ru m =
221   let ge_c = 
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
224     let _Ux = j in
225       (SOF.union _Uj _Ux)
226   in
227     ge_c
228       
229 and closure_gt_fast ru m =
230   let gt_c =
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)
239   in
240     gt_c
241       
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))
245
246 and adjust_fast u m =
247   let ru = repr u m in
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
252   let changed_gegt = 
253     (not (are_set_eq gt_c ru.gt_closure)) || 
254     (not (are_set_eq ge_c ru.ge_closure))
255   in
256     if ((not changed_gegt) &&  (not changed_eq)) then
257       m
258     else
259       begin
260         let ru' = {
261           eq_closure = eq_c;
262           ge_closure = ge_c;
263           gt_closure = gt_c;
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}
268         in
269         let m = MAL.add u ru' m in
270         let m =
271             SOF.fold (fun x m -> adjust_fast  x m) 
272               (SOF.union ru'.eq_closure ru'.in_gegt_of) m
273               (* TESI: 
274                    ru'.in_gegt_of m 
275               *)
276         in
277           m (*adjust_fast  u m*)
278       end
279         
280 and add_gt_arc_fast u v m =
281   let ru = repr u m in
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
287     adjust_fast u m''
288       
289 and add_ge_arc_fast u v m =
290   let ru = repr u m in
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
296     adjust_fast u m''
297
298 and add_eq_arc_fast u v m =
299   let ru = repr u m in
300   let rv = repr v m in 
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'' (* ) *)
308 ;;
309
310 \f
311 (*****************************************************************************)
312 (** safe implementation                                                     **)
313 (*****************************************************************************)
314
315 let closure_of u m =
316   let ru = repr u m in
317   let eq_c =
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)
322   in
323   let ge_c = 
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
326     let _Ux = j in
327       (SOF.union _Uj _Ux)
328   in
329   let gt_c =
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)
338   in
339     {
340       eq_closure = eq_c;
341       ge_closure = ge_c;
342       gt_closure = gt_c;
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
347     }
348
349 let rec simple_adjust m =
350   let m' = 
351     MAL.mapi (fun x _ -> closure_of x m) m
352   in
353     if not (are_ugraph_eq m  m') then(
354       simple_adjust m')
355     else
356       m'
357
358 let add_eq_arc u v m =
359   let ru = repr u m in
360   let rv = repr v m in
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
365     simple_adjust m''
366
367 let add_ge_arc u v m =
368   let ru = repr u m in
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
371     simple_adjust m'
372
373 let add_gt_arc u v m =
374   let ru = repr u m in
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
377     simple_adjust m'
378
379 \f
380 (*****************************************************************************)
381 (** Outhern interface, that chooses between _fast and safe                  **)
382 (*****************************************************************************)
383
384 (*                                                                            
385     given the 2 nodes plus the current bag, adds the arc, recomputes the 
386     closures and returns the new map
387 *) 
388 let add_eq fast u v b =
389   if fast then
390     add_eq_arc_fast u v b
391   else
392     add_eq_arc u v b
393
394 (*                                                                            
395     given the 2 nodes plus the current bag, adds the arc, recomputes the 
396     closures and returns the new map
397 *) 
398 let add_ge fast u v b =
399   if fast then
400     add_ge_arc_fast u v b
401   else
402     add_ge_arc u v b
403 (*                                                                            
404     given the 2 nodes plus the current bag, adds the arc, recomputes the 
405     closures and returns the new map
406 *)                                                                            
407 let add_gt fast u v b =
408   if fast then
409     add_gt_arc_fast u v b
410   else
411     add_gt_arc u v b
412
413
414 (*****************************************************************************)
415 (** Other real code                                                         **)
416 (*****************************************************************************)
417
418 exception UniverseInconsistency of string 
419
420 let error arc node1 closure_type node2 closure =
421   let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
422    "   Unable to add\n" ^ 
423    "\t" ^ (string_of_arc arc) ^ "\n" ^
424    "   cause\n" ^ 
425    "\t" ^ (string_of_universe node1) ^ "\n" ^
426    "   is in the " ^ closure_type ^ " closure\n" ^
427    "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
428    "   of\n" ^ 
429    "\t" ^ (string_of_universe node2) ^ "\n\n" ^
430    "  ===== Universe Inconsistency detected =====\n" in
431   prerr_endline s;
432   raise (UniverseInconsistency s)
433
434
435 let fill_empty_nodes_with_uri g uri =
436   let fill_empty_universe u =
437     match u with
438         (i,None) -> (i,Some uri)
439       | (i,Some _) as u -> u
440   in
441   let fill_empty_set s =
442     SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty 
443   in
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) ;
452   } in  
453   let m = g in
454   let m' = MAL.fold (
455     fun k v m -> 
456       MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
457   in
458     m'
459
460
461 (*****************************************************************************)
462 (** World interface                                                         **)
463 (*****************************************************************************)
464
465 type universe_graph = bag
466
467 let empty_ugraph = empty_bag
468
469 let current_index_anon = ref (-1)
470 let current_index_named = ref (-1)
471
472 let restart_numbering () = current_index_named := (-1) 
473
474 let fresh ?uri () =
475   let i =
476     match uri with
477     | None -> 
478         current_index_anon := !current_index_anon + 1;
479         !current_index_anon
480     | Some _ -> 
481         current_index_named := !current_index_named + 1;
482         !current_index_named
483   in
484   (i,uri)
485
486 let print_ugraph g = 
487   prerr_endline (string_of_bag g)
488
489 let add_eq ?(fast=(!fast_implementation)) u v b =
490   (* should we check to no add twice the same?? *)
491   let m = b in
492   let ru = repr u m in
493   if SOF.mem v ru.gt_closure then
494     error ("EQ",u,v) v "GT" u ru.gt_closure
495   else
496     begin
497     let rv = repr v m in
498     if SOF.mem u rv.gt_closure then
499       error ("EQ",u,v) u "GT" v rv.gt_closure
500     else
501       add_eq fast u v b
502     end
503
504 let add_ge ?(fast=(!fast_implementation)) u v b =
505   (* should we check to no add twice the same?? *)
506   let m = b in
507   let rv = repr v m in
508   if SOF.mem u rv.gt_closure then
509     error ("GE",u,v) u "GT" v rv.gt_closure
510   else
511     add_ge fast u v b
512   
513 let add_gt ?(fast=(!fast_implementation)) u v b =
514   (* should we check to no add twice the same?? *)
515   (* 
516      FIXME : check the thesis... no need to check GT and EQ closure since the 
517      GE is a superset of both 
518   *)
519   let m = b in
520   let rv = repr v m in
521
522   if u = v then
523     error ("GT",u,v) u "==" v SOF.empty
524   else
525   
526   (*if SOF.mem u rv.gt_closure then
527     error ("GT",u,v) u "GT" v rv.gt_closure
528   else
529     begin*)
530       if SOF.mem u rv.ge_closure then
531         error ("GT",u,v) u "GE" v rv.ge_closure
532       else
533 (*        begin
534           if SOF.mem u rv.eq_closure then
535             error ("GT",u,v) u "EQ" v rv.eq_closure
536           else*)
537             add_gt fast u v b
538 (*        end
539     end*)
540
541 (*****************************************************************************)
542 (** START: Decomment this for performance comparisons                       **)
543 (*****************************************************************************)
544
545 let add_eq ?(fast=(!fast_implementation))  u v b =
546   begin_spending ();
547   let rc = add_eq ~fast u v b in
548     end_spending();
549     rc
550
551 let add_ge ?(fast=(!fast_implementation)) u v b =
552   begin_spending ();
553   let rc = add_ge ~fast u v b in
554  end_spending();
555     rc
556     
557 let add_gt ?(fast=(!fast_implementation)) u v b =
558   begin_spending ();
559   let rc = add_gt ~fast u v b in
560     end_spending();
561     rc
562
563 (*****************************************************************************)
564 (** END: Decomment this for performance comparisons                         **)
565 (*****************************************************************************)
566
567 let merge_ugraphs u v =
568   (* this sucks *)
569   let merge_brutal u v =
570     if u = empty_bag then v 
571     else if v = empty_bag then u 
572     else
573       let m1 = u in 
574       let m2 = v in 
575         MAL.fold (
576           fun k v x -> 
577             (SOF.fold (
578                fun u x -> 
579                  let m = add_gt k u x in m) v.one_s_gt 
580                (SOF.fold (
581                   fun u x -> 
582                     let m = add_ge k u x in m) v.one_s_ge
583                   (SOF.fold (
584                      fun u x -> 
585                        let m = add_eq k u x in m) v.one_s_eq x)))
586         ) m1 m2
587   in
588     merge_brutal u v
589
590
591 (*****************************************************************************)
592 (** Xml sesialization and parsing                                           **)
593 (*****************************************************************************)
594
595 let xml_of_set s =
596   let l = 
597     List.map (
598       function 
599           (i,Some u) -> 
600             Xml.xml_empty "node" [
601               None,"id",(string_of_int i) ;
602               None,"uri",(UriManager.string_of_uri u)]
603         | (_,None) -> 
604             raise (Failure "we can serialize only universes with uri")
605     ) (SOF.elements s) 
606   in
607     List.fold_left (fun s x -> [< s ; x >] ) [<>] l
608       
609 let xml_of_entry_content e =
610   let stream_of_field f name =
611     let eq_c = xml_of_set f in
612     if eq_c != [<>] then
613       Xml.xml_nempty name [] eq_c
614     else
615       [<>]
616   in
617   [<
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")
625   >]
626
627 let xml_of_entry u e =
628   let (i,u') = u in
629   let u'' = 
630     match u' with 
631         Some x -> x 
632       | None -> 
633           raise (Failure "we can serialize only universes (entry) with uri")
634   in
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
639   ent content
640
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";
644     Xml.pp_to_outchan (
645       Xml.xml_nempty "ugraph" [] (
646       MAL.fold (
647         fun k v s -> [< s ; (xml_of_entry k v) >])
648       m [<>])) o;
649     close_out o
650  
651 let rec clean_ugraph m f =
652   let m' = 
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 -> 
655     let v' = {
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
663     } in 
664     MAL.add k v' x ) m' MAL.empty in
665   let e_l = 
666     MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' []
667   in
668     if e_l != [] then
669       clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
670     else
671       m''
672
673 let clean_ugraph g l =
674   clean_ugraph g (fun u -> List.mem u l)
675
676 let assigner_of = 
677   function
678     "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
679   | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
680   | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
681   | "in_gegt_of"   -> (fun e u->{e with in_gegt_of  =SOF.add u e.in_gegt_of})
682   | "one_s_ge"   -> (fun e u->{e with one_s_ge  =SOF.add u e.one_s_ge})
683   | "one_s_gt"   -> (fun e u->{e with one_s_gt  =SOF.add u e.one_s_gt})
684   | "one_s_eq"   -> (fun e u->{e with one_s_eq  =SOF.add u e.one_s_eq})
685   | s -> raise (Failure ("unsupported tag " ^ s))
686 ;;
687
688 let cb_factory m = 
689   let module XPP = XmlPushParser in
690   let current_node = ref (0,None) in
691   let current_entry = ref empty_entry in
692   let current_assign = ref (assigner_of "in_ge_of") in
693   { XPP.default_callbacks with
694     XPP.end_element = Some( fun name ->
695       match name with
696       | "entry" -> 
697           m := MAL.add !current_node !current_entry !m;
698           current_entry := empty_entry
699       | _ -> ()
700     );
701     XPP.start_element = Some( fun name attlist ->
702       match name with
703       | "entry" -> 
704           let id = List.assoc "id" attlist in      
705           let uri = List.assoc "uri" attlist in
706           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
707       | "node" -> 
708           let id = int_of_string (List.assoc "id" attlist) in
709           let uri = List.assoc "uri" attlist in        
710             current_entry := !current_assign !current_entry 
711               (id,Some (UriManager.uri_of_string uri))
712       | s -> current_assign := assigner_of s
713     )
714   }
715 ;; 
716
717 (* alternative implementation *)
718 let mapl = [
719   ("ge_closure",0);("gt_closure",1);("eq_closure",2);
720   ("in_gegt_of",  3);
721   ("one_s_ge",  4);("one_s_gt",  5);("one_s_eq",  6)]
722 ;;
723
724 let assigner_of' s = List.assoc s mapl ;;
725
726 let entry_of_array a = { 
727   ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
728   in_gegt_of   = a.(3); 
729   one_s_ge   = a.(4); one_s_gt   = a.(5); one_s_eq   = a.(6)}
730 ;;
731
732 let cb_factory' m = 
733   let module XPP = XmlPushParser in
734   let current_node = ref (0,None) in
735   let current_entry = Array.create 7 SOF.empty in
736   let current_assign = ref 0 in
737   { XPP.default_callbacks with
738     XPP.start_element = Some( fun name attlist ->
739       match name with
740       | "entry" -> 
741           let id = List.assoc "id" attlist in      
742           let uri = List.assoc "uri" attlist in
743           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
744       | "node" -> 
745           let id = int_of_string (List.assoc "id" attlist) in
746           let uri = List.assoc "uri" attlist in        
747           current_entry.(!current_assign) <- 
748             SOF.add (id,Some (UriManager.uri_of_string uri)) 
749               current_entry.(!current_assign) 
750       | s -> current_assign := assigner_of' s
751     );
752     XPP.end_element = Some( fun name -> 
753       match name with
754       | "entry" -> 
755           m := MAL.add !current_node (entry_of_array current_entry) !m;
756           Array.fill current_entry 0 7 SOF.empty 
757       | _ -> ()
758     );
759   }
760 ;;
761
762      
763 let ugraph_of_xml filename =
764   let module XPP = XmlPushParser in
765   let result = ref MAL.empty in
766   let cb = cb_factory result in
767 (*let cb = cb_factory' result in*)
768   let xml_parser = XPP.create_parser cb in
769   let xml_source = `Gzip_file filename in
770   (try XPP.parse xml_parser xml_source
771    with (XPP.Parse_error err) as exn -> raise exn);
772   !result
773
774 \f
775 (*****************************************************************************)
776 (** the main, only for testing                                              **)
777 (*****************************************************************************)
778
779 (* 
780
781 type arc = Ge | Gt | Eq ;;
782
783 let randomize_actionlist n m =
784   let ge_percent = 0.7 in
785   let gt_percent = 0.15 in
786   let random_step () =
787     let node1 = Random.int m in
788     let node2 = Random.int m in
789     let op = 
790       let r = Random.float 1.0 in
791         if r < ge_percent then 
792           Ge 
793         else (if r < (ge_percent +. gt_percent) then 
794           Gt 
795         else 
796           Eq) 
797     in
798       op,node1,node2      
799   in
800   let rec aux n =
801     match n with 
802         0 -> []
803       | n -> (random_step ())::(aux (n-1))
804   in
805     aux n
806
807 let print_action_list l =
808   let string_of_step (op,node1,node2) =
809     (match op with
810          Ge -> "Ge"
811        | Gt -> "Gt"
812        | Eq -> "Eq") ^ 
813     "," ^ (string_of_int node1) ^ ","   ^ (string_of_int node2) 
814   in
815   let rec aux l =
816     match l with 
817         [] -> "]"
818       | a::tl ->
819           ";" ^ (string_of_step a) ^ (aux tl)
820   in
821   let body = aux l in
822   let l_body = (String.length body) - 1 in
823     prerr_endline ("[" ^ (String.sub body 1 l_body))
824   
825 let debug = false
826 let d_print_endline = if debug then print_endline else ignore 
827 let d_print_ugraph = if debug then print_ugraph else ignore
828
829 let _ = 
830   (if Array.length Sys.argv < 2 then
831     prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
832   Random.self_init ();
833   let max_edges = int_of_string Sys.argv.(1) in
834   let max_nodes = int_of_string Sys.argv.(2) in
835   let action_listR = randomize_actionlist max_edges max_nodes in
836
837   let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
838   let action_list = action_listR in
839   
840   print_action_list action_list;
841   let prform_step ?(fast=false) (t,u,v) g =
842     let f,str = 
843       match t with
844           Ge -> add_ge,">="
845         | Gt -> add_gt,">"
846         | Eq -> add_eq,"="
847     in
848       d_print_endline (
849         "Aggiungo " ^ 
850         (string_of_int u) ^
851         " " ^ str ^ " " ^ 
852         (string_of_int v));
853       let g' = f ~fast (u,None) (v,None) g in
854         (*print_ugraph g' ;*)
855         g'
856   in
857   let fail = ref false in
858   let time1 = Unix.gettimeofday () in
859   let n_safe = ref 0 in
860   let g_safe =  
861     try 
862       d_print_endline "SAFE";
863       List.fold_left (
864         fun g e -> 
865           n_safe := !n_safe + 1;
866           prform_step e g
867       ) empty_ugraph action_list
868     with
869         UniverseInconsistency s -> fail:=true;empty_bag
870   in
871   let time2 = Unix.gettimeofday () in
872   d_print_ugraph g_safe;
873   let time3 = Unix.gettimeofday () in
874   let n_test = ref 0 in
875   let g_test = 
876     try
877       d_print_endline "FAST";
878       List.fold_left (
879         fun g e ->
880           n_test := !n_test + 1;
881           prform_step ~fast:true e g
882       ) empty_ugraph action_list
883     with
884         UniverseInconsistency s -> empty_bag
885   in
886   let time4 = Unix.gettimeofday () in
887   d_print_ugraph g_test;
888     if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
889       begin
890         let num_eq = 
891           List.fold_left (
892             fun s (e,_,_) -> 
893               if e = Eq then s+1 else s 
894           ) 0 action_list 
895         in
896         let num_gt = 
897           List.fold_left (
898             fun s (e,_,_) ->
899               if e = Gt then s+1 else s
900           ) 0 action_list
901         in
902         let num_ge = max_edges - num_gt - num_eq in
903         let time_fast = (time4 -. time3) in
904         let time_safe = (time2 -. time1) in
905         let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
906         let fail = if !fail then 1 else 0 in
907           print_endline 
908             (sprintf 
909                "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
910                fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
911           exit 0
912       end
913     else
914       begin
915         print_endline "FAIL";
916         print_ugraph g_safe;
917         print_ugraph g_test;
918         exit 1
919       end
920 ;;
921
922  *)
923
924 let recons_univ u =
925   match u with
926   | i, None -> u
927   | i, Some uri ->
928       i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
929
930 let recons_entry entry =
931   let recons_set set =
932     SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
933   in
934   {
935     eq_closure = recons_set entry.eq_closure;
936     ge_closure = recons_set entry.ge_closure;
937     gt_closure = recons_set entry.gt_closure;
938     in_gegt_of = recons_set entry.in_gegt_of;
939     one_s_eq = recons_set entry.one_s_eq;
940     one_s_ge = recons_set entry.one_s_ge;
941     one_s_gt = recons_set entry.one_s_gt;
942   }
943
944 let recons_graph graph =
945   MAL.fold
946     (fun universe entry map ->
947       MAL.add (recons_univ universe) (recons_entry entry) map)
948     graph MAL.empty
949
950 let assert_univ u =
951     match u with 
952     | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
953     | _ -> ()
954     
955 let assert_univs_have_uri graph =
956   let assert_set s =
957     SOF.iter (fun u -> assert_univ u) s
958   in
959   let assert_entry e =
960     assert_set e.eq_closure;
961     assert_set e.ge_closure;
962     assert_set e.gt_closure;
963     assert_set e.in_gegt_of;
964     assert_set e.one_s_eq;
965     assert_set e.one_s_ge;
966     assert_set e.one_s_gt;
967   in
968   MAL.iter (fun k v -> assert_univ k; assert_entry v)graph 
969   
970     
971 (* EOF *)