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