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