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