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