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