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 (*
  38
  39    todo:
  40      - in add_eq there is probably no need of add_gt, simple @ the gt lists
  41      - the problem of duplicates in the 1steg gt/ge list if two of them are
  42        add_eq may be "fixed" in some ways:
  43         - lazy, do nothing on add_eq and eventually update the ge list
  44           on closure
  45         - add a check_duplicates_after_eq function called by add_eq
  46         - do something like rmap, add a list of canonical that point to us
  47           so when we collapse we have the list of the canonical we may update
  48      - don't use failure but another exception
  49
  50 *)
  51
  52 (* ************************************************************************** *)
  53 (*  TYPES                                                                     *)
  54 (* ************************************************************************** *)
  55 type universe = int
  56
  57 type canonical_repr = {
  58         mutable ge:universe list;
  59         mutable gt:universe list;
  60         (* since we collapse we may need the reverse map *)
  61         mutable eq:universe list;
  62         (* the canonical representer *)
  63         u:universe
  64 }
  65
  66 module UniverseType = struct
  67   type t = universe
  68   let compare = Pervasives.compare
  69 end
  70
  71 module MapUC = Map.Make(UniverseType)
  72
  73 (* ************************************************************************** *)
  74 (*  Globals                                                                   *)
  75 (* ************************************************************************** *)
  76
  77 let map = ref MapUC.empty
  78 let used = ref (-1)
  79
  80 (* ************************************************************************** *)
  81 (*  Helpers                                                                   *)
  82 (* ************************************************************************** *)
  83
  84 (* create a canonical for [u] *)
  85 let mk_canonical u =
  86   {u = u ; gt = [] ; ge = [] ; eq = [u] }
  87
  88 (* give a new universe *)
  89 let fresh () =
  90   used := !used + 1;
  91   map := MapUC.add !used (mk_canonical !used) !map;
  92   !used
  93
  94 let reset () =
  95   map := MapUC.empty;
  96   used := -1
  97
  98 (* ************************************************************************** *)
  99 (*   Pretty printing                                                          *)
 100 (* ************************************************************************** *)
 101 (* pp *)
 102 let string_of_universe = string_of_int
 103
 104 (* pp *)
 105 let canonical_to_string c =
 106   let s_gt =
 107     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in
 108   let s_ge =
 109     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in
 110   let s_eq =
 111     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in
 112   let s_u = (string_of_universe c.u) in
 113   "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}"
 114
 115 (* print the content of map *)
 116 let print_map () =
 117   MapUC.iter (fun u c ->
 118    prerr_endline
 119     (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c)))
 120   !map;
 121   prerr_endline ""
 122
 123 (* ************************************************************************** *)
 124 (*  The way we fail                                                           *)
 125 (* ************************************************************************** *)
 126 (* we are doing bad *)
 127 let error s =
 128   (*prerr_endline " ======= Universe Inconsistency =========";
 129   print_map ();*)
 130   prerr_endline (" " ^ s ^ "\n");
 131   failwith s
 132
 133 (* ************************************************************************** *)
 134 (*  The real code                                                             *)
 135 (* ************************************************************************** *)
 136 (* <--------> *)
 137
 138 (* the canonical representer of the [u] equaliti class *)
 139 let repr u =
 140   try
 141     MapUC.find u !map
 142   with
 143     Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u))
 144
 145 (* all the nodes we can ifer in the ge list of u *)
 146 let close_ge u =
 147   let repr_u = repr u in
 148   let rec close_ge_aux tofollow bag =
 149     match tofollow with
 150       [] -> bag
 151     | v::tl -> let repr_v = repr v in
 152                if List.mem repr_v bag then (* avoid loops *)
 153                  (close_ge_aux tl bag )
 154                else
 155                  (close_ge_aux (tl @ repr_v.ge) (repr_v::bag))
 156                  (* we assume that v==u -> v \notin (repr u).ge *)
 157   in
 158   close_ge_aux repr_u.ge []
 159
 160 (* all the nodes we can ifer in the gt list of u,
 161    we must follow bot gt and ge arcs, but we must put in bag only
 162    the nodes that have a gt in theys path
 163 *)
 164 let close_gt u =
 165   let repr_u = repr u in
 166   let rec close_gt_aux bag todo inspected =
 167     (*print_all bag todo;Unix.sleep 1;*)
 168     match todo with
 169       [],[] -> bag
 170     | [],p::may -> let repr_p = repr p in
 171                    if List.mem repr_p.u inspected then (* avoid loops *)
 172                      close_gt_aux bag ([],may) inspected
 173                    else
 174                      close_gt_aux bag (repr_p.gt,repr_p.ge @ may)
 175                       (repr_p.u::inspected)
 176     | s::secure,may -> let repr_s = repr s in
 177                        if List.mem repr_s.u inspected then (* avoid loops *)
 178                          if List.mem repr_s bag then
 179                            close_gt_aux bag (secure,may) inspected
 180                          else
 181                            (* even if we ave already inspected the node, now
 182                               it is in the secure list so we want it in the bag
 183                            *)
 184                            close_gt_aux (repr_s::bag) (secure,may) inspected
 185                        else
 186                          close_gt_aux ((repr_s)::bag)
 187                           (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected)
 188   in
 189   close_gt_aux [] (repr_u.gt,repr_u.ge) []
 190
 191 (* when we add an eq we have to change the mapping of u to c*)
 192 let remap u c =
 193   let repr_u = repr u in
 194   List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq;
 195   List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq
 196
 197 (* we suspect that u and v are connected by a == implyed by two >= *)
 198 let rec collapse u v =
 199   let repr_u = repr u in
 200   let repr_v = repr v in
 201   let ge_v = close_ge v in
 202   let ge_u = close_ge u in
 203   if List.mem repr_u ge_v && List.mem repr_v ge_u then
 204     add_eq u v
 205
 206 (* we have to add u == v *)
 207 and add_eq u v =
 208   let repr_u = repr u in
 209   let repr_v = repr v in
 210   (* if we already have u == v then do nothing *)
 211   if repr_u = repr_v then
 212     ()
 213   else
 214     (* if we already have v > u then fail *)
 215     let gt_v = close_gt v in
 216     if List.mem repr_u gt_v then
 217       error ("Asking for " ^ (string_of_universe u) ^ " == " ^
 218             (string_of_universe v) ^ " but " ^
 219             (string_of_universe v) ^ " > " ^ (string_of_universe u))
 220     else
 221       (* if we already have u > v then fail *)
 222       let gt_u = close_gt u in
 223       if List.mem repr_v gt_u then
 224         error ("Asking for " ^ (string_of_universe u) ^ " == " ^
 225               (string_of_universe v) ^ " but " ^
 226               (string_of_universe u) ^ " > " ^ (string_of_universe v))
 227       else
 228         (* add the inherited > constraints *)
 229         List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt;
 230         (* add the inherited >= constraints *)
 231         (* close_ge assumes that v==u -> v \notin (repr u).ge *)
 232         repr_u.ge <- List.filter (fun x -> x <> u && x <> v)
 233          (repr_v.ge @ repr_u.ge);
 234         (* mege the eq list, we assume they are disjuncted *)
 235         repr_u.eq <- repr_u.eq @ repr_v.eq;
 236         (* we have to remap all node represented by repr_v to repr_u *)
 237         remap v repr_u;
 238         (* FIXME: not sure this is what we have to do
 239                   think more to the list of suspected cicles
 240         *)
 241         List.iter (fun x -> collapse u x) repr_u.ge
 242
 243 (* we have to add u >= v *)
 244 and add_ge u v =
 245   let repr_u = repr u in
 246   let repr_v = repr v in
 247   (* if we already have u == v then do nothing *)
 248   if repr_u = repr_v then
 249     ()
 250   else
 251     (* if we already have v > u then fail *)
 252     let gt = close_gt v in
 253     if List.memq repr_u gt then
 254       error ("Asking for " ^ (string_of_universe u) ^ " >= " ^
 255             (string_of_universe v) ^ " but " ^
 256             (string_of_universe v) ^ " > " ^ (string_of_universe u))
 257     else
 258       (* it is now safe to add u >= v *)
 259       repr_u.ge <- v::repr_u.ge;
 260       (* but we may have introduced a cicle *)
 261       collapse u v (* FIXME: not sure it is from u to v, think more. *)
 262
 263 (* we have to add u > v *)
 264 and add_gt u v =
 265   let repr_u = repr u in
 266   let repr_v = repr v in
 267   (* if we already have u == v then fail *)
 268   if repr_u = repr_v then
 269     error ("Asking for " ^ (string_of_universe u) ^ " > " ^
 270           (string_of_universe v) ^ " but " ^
 271           (string_of_universe u) ^ " == " ^ (string_of_universe v))
 272   else
 273     (* if we already have u > v do nothing *)
 274     let gt_u = close_gt u in
 275     if List.memq repr_v gt_u then
 276       ()
 277     else
 278       (* if we already have v > u then fail *)
 279       let gt = close_gt v in
 280       if List.memq repr_u gt then
 281         error ("Asking for " ^ (string_of_universe u) ^ " > " ^
 282               (string_of_universe v) ^ " but " ^
 283               (string_of_universe v) ^ " > " ^ (string_of_universe u))
 284       else
 285         (* if we already have v >= u then fail *)
 286         let ge = close_ge v in
 287         if List.memq repr_u ge then
 288           error ("Asking for " ^ (string_of_universe u) ^ " > " ^
 289                 (string_of_universe v) ^ " but " ^
 290                 (string_of_universe v) ^ " >= " ^ (string_of_universe u))
 291         else
 292           (* it is safe to add u > v *)
 293           repr_u.gt <- v::repr_u.gt
 294
 295 let add_gt u v =
 296   try
 297     add_gt u v; true
 298   with
 299     exn -> false
 300
 301 let add_ge u v =
 302   try
 303     add_ge u v; true
 304   with
 305     exn -> false
 306
 307 let add_eq u v =
 308   try
 309     add_eq u v; true
 310   with
 311     exn -> false
 312
 313 (* <--------> *)
 314
 315 (* ************************************************************************** *)
 316 (*  To make tests                                                             *)
 317 (* ************************************************************************** *)
 318
 319 (*
 320 let check_status_eq l =
 321   let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in
 322   let repr_u = repr (List.hd l) in
 323   let rec check_status_eq_aux c =
 324     match c with
 325       [] -> print_endline (" Result check_status_eq["^s^"] = OK");true
 326     | u::tl -> if repr u != repr_u then
 327                  (print_endline (" Result check_status_eq["^s^"] = FAILED");
 328                  print_endline ((string_of_universe u) ^ " != " ^
 329                   (string_of_universe repr_u.u));
 330                  print_map ();false)
 331                else
 332                  check_status_eq_aux tl
 333   in
 334   check_status_eq_aux (List.tl l)
 335 *)
 336
 337 (* ************************************************************************** *)
 338 (*  Fake implementation                                                       *)
 339 (* ************************************************************************** *)
 340
 341 (* <--------> *
 342 let add_ge u v = true
 343 let add_gt u v = true
 344 let add_eq u v = true
 345 * <--------> *)