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