helm/ocaml/cic/cicUniv.ml

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