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