helm/software/components/cic/cicUniv.ml

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