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