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