helm/ocaml/cic/cicUniv.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                      Enrico Tassi <tassi@cs.unibo.it>                      *)
  31 (*                                 23/04/2004                                 *)
  32 (*                                                                            *)
  33 (* This module implements the aciclic graph of universes.                     *)
  34 (*                                                                            *)
  35 (******************************************************************************)
  36
  37 open Printf
  38
  39 (******************************************************************************)
  40 (** Types and default values                                                 **)
  41 (******************************************************************************)
  42
  43 type universe = int
  44
  45 module UniverseType = struct
  46   type t = universe
  47   let compare = Pervasives.compare
  48 end
  49
  50 module SOF = Set.Make(UniverseType)
  51
  52 type entry = {
  53         eq_closure : SOF.t;
  54         ge_closure : SOF.t;
  55         gt_closure : SOF.t;
  56         in_eq_of   : SOF.t;
  57         in_ge_of   : SOF.t;
  58         in_gt_of   : SOF.t;
  59         one_s_eq   : SOF.t;
  60         one_s_ge   : SOF.t;
  61         one_s_gt   : SOF.t;
  62 }
  63
  64 module MAL = Map.Make(UniverseType)
  65
  66 type arc_type = GE | GT | EQ
  67
  68 type arc = arc_type * universe * universe
  69
  70 type bag = entry MAL.t * (arc list)
  71
  72 let empty_entry = {
  73         eq_closure=SOF.empty;
  74         ge_closure=SOF.empty;
  75         gt_closure=SOF.empty;
  76         in_eq_of=SOF.empty;
  77         in_ge_of=SOF.empty;
  78         in_gt_of=SOF.empty;
  79         one_s_eq=SOF.empty;
  80         one_s_ge=SOF.empty;
  81         one_s_gt=SOF.empty;
  82 }
  83
  84 let empty_bag = (MAL.empty, [])
  85
  86 let env_bag = ref empty_bag
  87
  88 (******************************************************************************)
  89 (** Pretty printings                                                         **)
  90 (******************************************************************************)
  91
  92 let string_of_universe u = string_of_int u
  93
  94 let string_of_arc_type u =
  95   match u with
  96     EQ -> "EQ"
  97   | GT -> "GT"
  98   | GE -> "EQ"
  99
 100 let string_of_arc u =
 101   let atype,a,b = u in
 102   (string_of_arc_type atype) ^ " " ^
 103    (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; "
 104 ;;
 105
 106 let string_of_universe_set l =
 107   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
 108
 109 let string_of_arc_list l =
 110   List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l
 111
 112 let string_of_node n =
 113   "{"^
 114   "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^
 115   "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^
 116   "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^
 117   "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^
 118   "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^
 119   "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n"
 120
 121 let string_of_mal m =
 122   let rc = ref "" in
 123   MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m;
 124   !rc
 125
 126 let string_of_bag b =
 127   let (m,l) = b in
 128   let s_m = string_of_mal m in
 129   let s_l = string_of_arc_list l in
 130    s_m ^"["^s_l^"]"
 131
 132 (******************************************************************************)
 133 (** Helpers                                                                  **)
 134 (******************************************************************************)
 135
 136 (*
 137     we need to merge the 2 graphs... here the code
 138 *)
 139 let repr u m =
 140   try
 141     MAL.find u m
 142   with
 143     Not_found ->
 144       try
 145         let m',_ = !env_bag in
 146         MAL.find u m'
 147       with
 148         Not_found -> empty_entry
 149
 150 (*
 151     FIXME: May be faster if we make it by hand
 152 *)
 153 let merge_closures f nodes m =
 154   SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
 155
 156 (******************************************************************************)
 157 (** Real stuff GT                                                            **)
 158 (******************************************************************************)
 159
 160 (*
 161     todo is the SOF of nodes that needs to be recomputed,
 162     m is the MAL map, s is the already touched nodes
 163 *)
 164 let rec redo_gt_closure todo m s =
 165   if SOF.is_empty todo then m
 166   else
 167     begin
 168     (* we choose the node to recompute *)
 169     let u = SOF.choose todo in
 170     if not (SOF.mem u s) then
 171       let ru = repr u m in
 172       let ru' = {ru with gt_closure =
 173        (* the new gt closure is the gt-closures + ge-closures + eq-closures
 174           of the one step gt-connected nodes *)
 175        SOF.union ru.one_s_gt (merge_closures
 176         (fun x -> SOF.union x.eq_closure
 177          (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in
 178       let m' = MAL.add u ru' m in
 179       let s' = SOF.add u s in
 180       redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s'
 181     else
 182       (* if already done go next. FIXME: think if it is right
 183          maybe we should check if we changed something or not *)
 184       redo_gt_closure (SOF.remove u todo) m s
 185     end
 186
 187 (*
 188     calculates the closures of u and adjusts the in_*_of of v, then
 189     starts redo_*_closure to adjust the colure of nodew thet have
 190     (clusure u) in theyr closures
 191 *)
 192 let add_gt_arc u v m =
 193   let ru = repr u m in
 194   let rv = repr v m in
 195   let ru' = {
 196     (* new node: we add the v gt-closure and v to our gt-closure *)
 197     eq_closure = ru.eq_closure;
 198     ge_closure = ru.ge_closure;
 199     gt_closure = SOF.add v
 200      (SOF.union ru.gt_closure
 201       (SOF.union rv.ge_closure
 202        (SOF.union rv.eq_closure rv.gt_closure)));
 203     in_eq_of = ru.in_eq_of;
 204     in_ge_of = ru.in_ge_of;
 205     in_gt_of = ru.in_gt_of;
 206     one_s_eq = ru.one_s_eq;
 207     one_s_ge = ru.one_s_ge;
 208     one_s_gt = SOF.add v ru.one_s_gt;
 209   } in
 210   (* may add the sanity check *)
 211   let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in
 212   let m' = MAL.add u ru' m in
 213   let m'' = MAL.add v rv' m' in
 214   redo_gt_closure ru'.in_gt_of m'' SOF.empty
 215
 216 (*
 217     given the 2 nodes plus the current bag, adds the arc, recomputes the
 218     closures and returns the new map
 219 *)
 220 let add_gt u v b =
 221   let m,l = b in
 222   let m' = add_gt_arc u v m in
 223   let l' = (GT,u,v)::l in
 224   (m',l')
 225
 226 (******************************************************************************)
 227 (** Real stuff GE                                                            **)
 228 (******************************************************************************)
 229
 230 (*
 231     todo is the SOF of nodes that needs to be recomputed,
 232     m is the MAL map, s is the already touched nodes
 233 *)
 234 let rec redo_ge_closure todo m s =
 235   if SOF.is_empty todo then m,s
 236   else
 237     begin
 238     let u = SOF.choose todo in
 239     if not (SOF.mem u s) then
 240       begin
 241         let ru = repr u m in
 242         (* the ge-closure is recomputed as the ge-closures of
 243            ge connected nodes plus theys eq-closure *)
 244         let ru' = {ru with ge_closure = merge_closures
 245           (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in
 246         let m' = MAL.add u ru' m in
 247         let s' = SOF.add u s in
 248         redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s'
 249       end
 250     else
 251       redo_ge_closure (SOF.remove u todo) m s
 252     end
 253
 254 (*
 255     calculates the closures of u and adjusts the in_*_of of v, then
 256     starts redo_*_closure to adjust the colure of nodew thet have
 257     (clusure u) in theyr closures
 258 *)
 259 let add_ge_arc u v m =
 260   let ru = repr u m in
 261    let rv = repr v m in
 262   let ru' = {
 263     eq_closure = ru.eq_closure;
 264     ge_closure = SOF.add v
 265      (SOF.union ru.ge_closure
 266       (SOF.union rv.eq_closure rv.ge_closure));
 267     gt_closure = ru.gt_closure;
 268     in_eq_of = ru.in_eq_of;
 269     in_ge_of = ru.in_ge_of;
 270     in_gt_of = ru.in_gt_of;
 271     one_s_eq = ru.one_s_eq;
 272     one_s_ge = SOF.add v ru.one_s_ge;
 273     one_s_gt = ru.one_s_gt;
 274   } in
 275   let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in
 276   let m' = MAL.add u ru' m in
 277   let m'' = MAL.add v rv' m' in
 278   let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
 279   (* closing ge may provoke aome changes in gt-closures *)
 280   redo_gt_closure (SOF.union ru'.in_gt_of
 281    (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of))
 282     td SOF.empty )) m''' SOF.empty
 283
 284 (*
 285     given the 2 nodes plus the current bag, adds the arc, recomputes the
 286     closures and returns the new map
 287 *)
 288 let add_ge u v b =
 289   let m,l = b in
 290   let m' = add_ge_arc u v m in
 291   let l' = (GE,u,v)::l in
 292   (m',l')
 293
 294 (******************************************************************************)
 295 (** Real stuff EQ                                                            **)
 296 (******************************************************************************)
 297
 298 let rec redo_eq_closure todo m s =
 299   if SOF.is_empty todo then m,s
 300   else begin
 301     let u = SOF.choose todo in
 302     if not (SOF.mem  u s) then
 303       begin
 304         let ru = repr u m in
 305         let eq_closure = merge_closures
 306           (fun x -> x.eq_closure) ru.one_s_eq m in
 307         let ru' = {ru with eq_closure = eq_closure
 308         ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
 309         let m' = MAL.add u ru' m in
 310         let s' = SOF.add u s in
 311         redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
 312       end
 313     else
 314       redo_eq_closure (SOF.remove u todo) m s
 315   end
 316
 317 (*
 318     calculates the closures of u and adjusts the in_*_of of v, then
 319     starts redo_*_closure to adjust the colure of nodew thet have
 320     (clusure u) in theyr closures
 321 *)
 322 let add_eq_arc u v m =
 323   let ru = repr u m in
 324   let rv = repr v m in
 325   (* since eq is symmetric we have to chage more *)
 326   let eq_closure = SOF.add u (SOF.add v
 327      (SOF.union ru.eq_closure rv.eq_closure)) in
 328   let ru' = {
 329     eq_closure = eq_closure;
 330     ge_closure = SOF.union ru.ge_closure rv.ge_closure;
 331     gt_closure = SOF.union ru.gt_closure rv.gt_closure;
 332     in_eq_of = eq_closure;
 333     in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
 334     in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
 335     one_s_eq = eq_closure;
 336     one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
 337     one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
 338   } in
 339   (* this is a collapse *)
 340   let rv' = ru' in
 341   let m' = MAL.add u ru' m in
 342   let m'' = MAL.add v rv' m' in
 343   let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
 344   (* redoing a eq may change some ge and some gt *)
 345   let m'''',td' = redo_ge_closure
 346    (SOF.union ru'.in_ge_of
 347     (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of))
 348     td SOF.empty)) m''' SOF.empty in
 349   redo_gt_closure (SOF.union ru'.in_gt_of
 350    (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of))
 351     td' SOF.empty)) m'''' SOF.empty
 352
 353 (*
 354     given the 2 nodes plus the current bag, adds the arc, recomputes the
 355     closures and returns the new map
 356 *)
 357 let add_eq u v b =
 358   let m,l = b in
 359   let m' = add_eq_arc u v m in
 360   let l' = (EQ,u,v)::l in
 361   (m',l')
 362
 363 (******************************************************************************)
 364 (** Oyther real code                                                         **)
 365 (******************************************************************************)
 366
 367 exception UniverseInconsistency of string
 368
 369 let error arc node1 closure_type node2 closure =
 370   let s = "  ===== Universe Inconsistency detected =====\n\n" ^
 371    "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^
 372    (string_of_universe node1) ^ " is in the " ^
 373    (string_of_arc_type closure_type) ^ " closure {" ^
 374    (string_of_universe_set closure) ^ "} of " ^
 375    (string_of_universe node2) ^ "\n\n" ^
 376    "  ===== Universe Inconsistency detected =====\n" in
 377   prerr_endline s;
 378   raise (UniverseInconsistency s)
 379
 380 (*
 381     we merge the env_bag with b
 382 *)
 383 let qed b =
 384   let m,l = b in
 385   let m',l' = !env_bag in
 386   let m'' = ref m' in
 387   MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
 388   let l'' = l @ l' in
 389   env_bag := (!m'',l'')
 390
 391 let add_eq u v b =
 392   (* should we check to no add twice the same?? *)
 393   let m,_ = b in
 394   let ru = repr u m in
 395   if SOF.mem v ru.gt_closure then
 396     error (EQ,u,v) v GT u ru.gt_closure
 397   else
 398     begin
 399     let rv = repr v m in
 400     if SOF.mem u rv.gt_closure then
 401       error (EQ,u,v) u GT v rv.gt_closure
 402     else
 403       add_eq u v b
 404     end
 405
 406 let add_ge u v b =
 407   (* should we check to no add twice the same?? *)
 408   let m,_ = b in
 409   let rv = repr v m in
 410   if SOF.mem u rv.gt_closure then
 411     error (GE,u,v) u GT v rv.gt_closure
 412   else
 413     add_ge u v b
 414
 415 let add_gt u v b =
 416   (* should we check to no add twice the same?? *)
 417   let m,_ = b in
 418   let rv = repr v m in
 419   if SOF.mem u rv.gt_closure then
 420     error (GT,u,v) u GT v rv.gt_closure
 421   else
 422     begin
 423       if SOF.mem u rv.ge_closure then
 424         error (GT,u,v) u GE v rv.ge_closure
 425       else
 426         begin
 427           if SOF.mem u rv.eq_closure then
 428             error (GT,u,v) u EQ v rv.eq_closure
 429           else
 430             add_gt u v b
 431         end
 432     end
 433
 434
 435
 436 (******************************************************************************)
 437 (** World interface                                                          **)
 438 (******************************************************************************)
 439
 440 type universe_graph = bag
 441
 442 let work_bag = ref empty_bag
 443 let current_index = ref (-1)
 444
 445 let get_working () = !work_bag
 446 let get_global  () = !env_bag
 447 let set_working b = work_bag := b
 448
 449 let fresh () =
 450   current_index := !current_index + 1;
 451   !current_index
 452
 453 let qed () =
 454   qed !work_bag
 455
 456 let print_global_graph () =
 457   let s = string_of_bag !env_bag in
 458   prerr_endline s
 459
 460 let print_working_graph () =
 461   let s = string_of_bag !work_bag in
 462   prerr_endline s
 463
 464 type history_ticket = int
 465
 466 let get_history_ticket b =
 467   let m,l = b in
 468   List.length l
 469
 470 let redo_history t b b'=
 471   let rec get_history l n =
 472     if n == 0 then
 473       []
 474     else
 475       begin
 476       match l with
 477         [] -> failwith "erroer, lista piu' corta della history"
 478       | h::tl -> h::(get_history tl (n - 1))
 479       end
 480   in
 481   let rec redo_commands l b =
 482     match l with
 483       [] -> b
 484     | (GE,u,v)::tl -> redo_commands tl (add_ge u v b)
 485     | (GT,u,v)::tl -> redo_commands tl (add_gt u v b)
 486     | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b)
 487   in
 488   let (m,l) = b in
 489   let todo = List.rev (get_history l ((List.length l) - t)) in
 490   try
 491     redo_commands todo b'
 492   with
 493     UniverseInconsistency s -> failwith s
 494   (*| _ -> failwith "Unexpected exception"*)
 495
 496 let add_gt u v =
 497   try
 498     work_bag := add_gt u v !work_bag; true
 499   with
 500     UniverseInconsistency s -> false
 501   (*| _ -> failwith "Unexpected exception"*)
 502
 503 let add_ge u v =
 504   try
 505     work_bag := add_ge u v !work_bag;true
 506   with
 507     UniverseInconsistency s -> false
 508   (*| _ -> failwith "Unexpected exception"*)
 509
 510 let add_eq u v =
 511   try
 512     work_bag := add_eq u v !work_bag;true
 513   with
 514     UniverseInconsistency s -> false
 515   (*| _ -> failwith "Unexpected exception"*)
 516
 517 let saved_data = ref (empty_bag,0)
 518
 519 let directly_to_env_begin () =
 520   saved_data := (!work_bag, get_history_ticket !env_bag);
 521   work_bag := empty_bag
 522
 523 let directly_to_env_end () =
 524   qed ();
 525   let (b,t) = !saved_data in
 526   work_bag := redo_history t !env_bag b
 527
 528 let reset_working () = work_bag := empty_bag
 529
 530 (******************************************************************************)
 531 (** Fake implementatoin                                                      **)
 532 (******************************************************************************)
 533
 534 let reset_working = function _ -> ()
 535 let directly_to_env_end = function _ -> ()
 536 let directly_to_env_begin = function _ -> ()
 537 let add_eq = fun _ _ -> true
 538 let add_ge = fun _ _ -> true
 539 let add_gt = fun _ _ -> true
 540 let get_working = function a -> empty_bag
 541 let set_working = function a -> ()