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