src/common/atom.ml

   1 (* Adapted from Pottier's PP compiler *)
   2
   3 (* A universe is a record, whose address defines the identity of the
   4    universe. The integer counter [next] holds the number of the next
   5    fresh atom. The [name] field holds the name of the universe. *)
   6
   7 type universe = {
   8     mutable next: int;
   9     name: string
  10   }
  11
  12 let new_universe name = {
  13   next = 0;
  14   name = name
  15 }
  16
  17 (* An atom is a pair of a universe and an integer. The latter defines
  18    the atom's identity within its universe. *)
  19
  20 type t =
  21    universe * int
  22
  23 let fresh u =
  24    let id = u.next in
  25    u.next <- id + 1;
  26    u, id
  27
  28 let equal (u1, id1) (u2, id2) =
  29   assert (u1 == u2);
  30   ((id1 : int) = (id2 : int))
  31
  32 let compare (u1, id1) (u2, id2) =
  33   assert (u1 == u2);
  34   compare (id1 : int) (id2 : int)
  35
  36 let flex_compare (u1, id1) (u2, id2) =
  37   if String.compare u1.name u2.name = 0 then Pervasives.compare id1 id2
  38   else String.compare u1.name u2.name
  39
  40 let flex_equal l1 l2 = flex_compare l1 l2 = 0
  41
  42 let universe_of (u, _) = u
  43
  44 let same_universe (u1, _) (u2, _) = u1 = u2
  45
  46 let ends_with_a_digit s =
  47   let n = String.length s in
  48   n > 0 && s.[n-1] >= '0' && s.[n-1] <= '9'
  49
  50 (* This function is injective, that is, [u] and [id] can be recovered
  51    out of [print (u, id)]. *)
  52
  53 let print (u, id) =
  54   Printf.sprintf "%s%s%d" u.name (if ends_with_a_digit u.name then "_" else "") id
  55
  56 (* Added by Nicolas Ayache: more flexible maps and sets where atoms
  57    from different universes can coexist. *)
  58
  59 type label_t = t
  60
  61 module OrderedLabel = struct
  62   type t = label_t
  63   let compare = flex_compare
  64 end
  65
  66 module FlexSet = Set.Make (OrderedLabel)
  67
  68 module FlexMap = Map.Make (OrderedLabel)
  69
  70
  71 module OrderedInt = struct
  72   type t = int
  73   let compare x1 x2 = x1 - x2
  74 end
  75
  76 (* We internally rely upon Objective Caml's integer sets and maps. *)
  77
  78 module ISet = Set.Make (OrderedInt)
  79 module IMap = Map.Make (OrderedInt)
  80
  81 (* Sets. *)
  82
  83 module Set = struct
  84
  85   (* A set is either empty or a pair of a universe and a (possibly
  86      empty) internal set. The fact that we do not require the empty
  87      set to be explicitly associated with a universe means that
  88      [empty] can be a constant, as opposed to an operation that
  89      expects a universe as a parameter. *)
  90
  91   type elt =
  92       t
  93
  94   type t =
  95     | E
  96     | U of universe * ISet.t
  97
  98   let empty =
  99     E
 100
 101   let is_empty = function
 102     | E ->
 103         true
 104     | U (_, s) ->
 105         ISet.is_empty s
 106
 107   let mem (u1, x) = function
 108     | E ->
 109         false
 110     | U (u2, s) ->
 111         assert (u1 == u2);
 112         (u1 = u2) && (ISet.mem x s)
 113
 114   let add (u1, x) = function
 115     | E ->
 116         U (u1, ISet.singleton x)
 117     | U (u2, s) ->
 118         assert (u1 == u2);
 119         U (u1, ISet.add x s)
 120
 121   let remove (u1, x) = function
 122     | E ->
 123         E
 124     | U (u2, s) ->
 125         assert (u1 == u2);
 126         (* set can become empty but retains its universe *)
 127         U (u1, ISet.remove x s)
 128
 129   let singleton x =
 130     add x empty
 131
 132   let couple x1 x2 =
 133     add x1 (singleton x2)
 134
 135   let of_list xs =
 136     List.fold_right add xs empty
 137
 138   let union s1 s2 =
 139     match s1, s2 with
 140     | E, s
 141     | s, E ->
 142         s
 143     | U (u1, s1), U (u2, s2) ->
 144         assert (u1 == u2);
 145         U (u1, ISet.union s1 s2)
 146
 147   let inter s1 s2 =
 148     match s1, s2 with
 149     | E, s
 150     | s, E ->
 151         E
 152     | U (u1, s1), U (u2, s2) ->
 153         assert (u1 == u2);
 154         U (u1, ISet.inter s1 s2)
 155
 156   let disjoint s1 s2 =
 157     is_empty (inter s1 s2)
 158
 159   let diff s1 s2 =
 160     match s1, s2 with
 161     | E, _ ->
 162         E
 163     | s, E ->
 164         s
 165     | U (u1, s1), U (u2, s2) ->
 166         assert (u1 == u2);
 167         U (u1, ISet.diff s1 s2)
 168
 169   let iter f = function
 170     | E ->
 171         ()
 172     | U (u, s) ->
 173         ISet.iter (fun x -> f (u, x)) s
 174
 175   let fold f s accu =
 176     match s with
 177     | E ->
 178         accu
 179     | U (u, s) ->
 180         ISet.fold (fun x accu -> f (u, x) accu) s accu
 181
 182   let choose = function
 183     | E ->
 184         raise Not_found
 185     | U (u, s) ->
 186         u, ISet.choose s
 187
 188   let equal s1 s2 =
 189     match s1, s2 with
 190     | E, s
 191     | s, E ->
 192         is_empty s
 193     | U (u1, s1), U (u2, s2) ->
 194         assert (u1 == u2);
 195         ISet.equal s1 s2
 196
 197   let cardinal = function
 198     | E ->
 199         0
 200     | U (_, s) ->
 201         ISet.cardinal s
 202
 203   let elements = function
 204     | E ->
 205         []
 206     | U (u, s) ->
 207         List.map (fun x -> (u, x)) (ISet.elements s)
 208
 209   let filter p = function
 210     | E ->
 211         E
 212     | U (u, s) ->
 213         U (u, ISet.filter (fun x -> p (u, x)) s)
 214
 215   let pick s =
 216     let x = choose s in
 217     let s = remove x s in
 218     x, s
 219
 220   let rec exhaust s accu f =
 221     if is_empty s then
 222       accu
 223     else
 224       let x, s = pick s in
 225       let s', accu = f x accu in
 226       exhaust (union s s') accu f
 227
 228   open Print
 229
 230   let print s =
 231     seplist comma (fun () x -> print x) () (elements s)
 232
 233 end
 234
 235 (* Maps. *)
 236
 237 module Map = struct
 238
 239   (* A map is either empty or a pair of a universe and a (possibly
 240      empty) internal map. The fact that we do not require the empty
 241      map to be explicitly associated with a universe means that
 242      [empty] can be a constant, as opposed to an operation that
 243      expects a universe as a parameter. *)
 244
 245   type key =
 246       t
 247
 248   type 'a t =
 249     | E
 250     | U of universe * 'a IMap.t
 251
 252   let empty =
 253     E
 254
 255   let is_empty = function
 256     | E ->
 257         true
 258     | U (_, m) ->
 259         IMap.is_empty m
 260
 261   let mem (u1, x) = function
 262     | E ->
 263         false
 264     | U (u2, m) ->
 265         assert (u1 == u2);
 266         IMap.mem x m
 267
 268   let add (u1, x) d = function
 269     | E ->
 270         U (u1, IMap.add x d IMap.empty)
 271     | U (u2, m) ->
 272         assert (u1 == u2);
 273         U (u1, IMap.add x d m)
 274
 275   let remove (u1, x) = function
 276     | E ->
 277         E
 278     | U (u2, m) ->
 279         assert (u1 == u2);
 280         U (u1, IMap.remove x m)
 281
 282   let singleton x d =
 283     add x d empty
 284
 285   let find (u1, x) = function
 286     | E ->
 287         raise Not_found
 288     | U (u2, m) ->
 289         assert (u1 == u2);
 290         IMap.find x m
 291
 292   let iter f = function
 293     | E ->
 294         ()
 295     | U (u, m) ->
 296         IMap.iter (fun x d -> f (u, x) d) m
 297
 298   let fold f m accu =
 299     match m with
 300     | E ->
 301         accu
 302     | U (u, m) ->
 303         IMap.fold (fun x d accu -> f (u, x) d accu) m accu
 304
 305   let map f = function
 306     | E ->
 307         E
 308     | U (u, m) ->
 309         U (u, IMap.map f m)
 310
 311   let mapi f = function
 312     | E ->
 313         E
 314     | U (u, m) ->
 315         U (u, IMap.mapi (fun x d -> f (u, x) d) m)
 316
 317   let domain = function
 318     | E ->
 319         Set.E
 320     | U (u, m) ->
 321         Set.U (u, IMap.fold (fun x _ s ->
 322                     ISet.add x s
 323                   ) m ISet.empty
 324               )
 325
 326   let lift f = function
 327     | Set.E ->
 328         E
 329     | Set.U (u, s) ->
 330         U (u, ISet.fold (fun x m ->
 331                 IMap.add x (f (u, x)) m
 332               ) s IMap.empty
 333           )
 334
 335
 336   let generator u =
 337     let m = ref empty in
 338     let generate d =
 339       let label = fresh u in
 340       m := add label d !m;
 341       label
 342     in
 343     m, generate
 344
 345   let addm m1 m2 =
 346     fold add m1 m2
 347
 348   let restrict p m =
 349     fold (fun x d m ->
 350       if p x then
 351         add x d m
 352       else
 353         m
 354     ) m empty
 355
 356 end
 357
 358 (* An imperative interface to maps. *)
 359
 360 module ImperativeMap = struct
 361
 362   type key =
 363       Map.key
 364
 365   type 'data t =
 366       'data Map.t ref
 367
 368   let create () =
 369     ref Map.empty
 370
 371   let clear t =
 372     t := Map.empty
 373
 374   let add k d t =
 375     t := Map.add k d !t
 376
 377   let find k t =
 378     Map.find k !t
 379
 380   let iter f t =
 381     Map.iter f !t
 382
 383 end
 384
 385 (* Maps of atoms to sets of atoms. *)
 386
 387 module SetMap = SetMap.MakeHomo(Set)(Map)