src/utilities/unionFind.ml

   1 (* Pasted from Pottier's PP compiler *)
   2
   3 (** This module implements a simple and efficient union/find algorithm.
   4     See Robert E. Tarjan, ``Efficiency of a Good But Not Linear Set
   5     Union Algorithm'', JACM 22(2), 1975. *)
   6
   7 (** The abstraction defined by this module is a set of points,
   8     partitioned into equivalence classes. With each equivalence class,
   9     a piece of information, of abstract type ['a], is associated; we
  10     call it a descriptor.
  11
  12     A point is implemented as a cell, whose (mutable) contents consist
  13     of a single link to either information about the equivalence class,
  14     or another point. Thus, points form a graph, which must be acyclic,
  15     and whose connected components are the equivalence classes. In
  16     every equivalence class, exactly one point has no outgoing edge,
  17     and carries information about the class instead. It is the class's
  18     representative element.
  19
  20     Information about a class consists of an integer weight (the number
  21     of elements in the class) and of the class's descriptor. *)
  22 type 'a point = {
  23     mutable link: 'a link
  24   }
  25
  26 and 'a link =
  27   | Info of 'a info
  28   | Link of 'a point
  29
  30 and 'a info = {
  31     mutable weight: int;
  32     mutable descriptor: 'a
  33   }
  34
  35 (** [fresh desc] creates a fresh point and returns it. It forms an
  36     equivalence class of its own, whose descriptor is [desc]. *)
  37 let fresh desc = {
  38   link = Info { weight = 1; descriptor = desc }
  39 }
  40
  41 (** [repr point] returns the representative element of [point]'s
  42     equivalence class. It is found by starting at [point] and following
  43     the links. For efficiency, the function performs path compression
  44     at the same time. *)
  45 let rec repr point =
  46   match point.link with
  47   | Link point' ->
  48       let point'' = repr point' in
  49       if point'' != point' then
  50
  51         (* [point''] is [point']'s representative element. Because we
  52            just invoked [repr point'], [point'.link] must be [Link
  53            point'']. We write this value into [point.link], thus
  54            performing path compression. Note that this function never
  55            performs memory allocation. *)
  56
  57         point.link <- point'.link;
  58       point''
  59   | Info _ ->
  60       point
  61
  62 (** [find point] returns the descriptor associated with [point]'s
  63     equivalence class. *)
  64 let rec find point =
  65
  66   (* By not calling [repr] immediately, we optimize the common cases
  67      where the path starting at [point] has length 0 or 1, at the
  68      expense of the general case. *)
  69
  70   match point.link with
  71   | Info info
  72   | Link { link = Info info } ->
  73       info.descriptor
  74   | Link { link = Link _ } ->
  75       find (repr point)
  76
  77 let rec change point v =
  78   match point.link with
  79   | Info info
  80   | Link { link = Info info } ->
  81       info.descriptor <- v
  82   | Link { link = Link _ } ->
  83       change (repr point) v
  84
  85 (** [union point1 point2] merges the equivalence classes associated
  86     with [point1] and [point2] (which must be distinct) into a single
  87     class whose descriptor is that originally associated with [point2].
  88
  89     The fact that [point1] and [point2] do not originally belong to the
  90     same class guarantees that we do not create a cycle in the graph.
  91
  92     The weights are used to determine whether [point1] should be made
  93     to point to [point2], or vice-versa. By making the representative
  94     of the smaller class point to that of the larger class, we
  95     guarantee that paths remain of logarithmic length (not accounting
  96     for path compression, which makes them yet smaller). *)
  97 let union point1 point2 =
  98   let point1 = repr point1
  99   and point2 = repr point2 in
 100   assert (point1 != point2);
 101   match point1.link, point2.link with
 102   | Info info1, Info info2 ->
 103       let weight1 = info1.weight
 104       and weight2 = info2.weight in
 105       if weight1 >= weight2 then begin
 106         point2.link <- Link point1;
 107         info1.weight <- weight1 + weight2;
 108         info1.descriptor <- info2.descriptor
 109       end
 110       else begin
 111         point1.link <- Link point2;
 112         info2.weight <- weight1 + weight2
 113       end
 114   | _, _ ->
 115       assert false (* [repr] guarantees that [link] matches [Info _]. *)
 116
 117 (** [equivalent point1 point2] tells whether [point1] and [point2]
 118     belong to the same equivalence class. *)
 119 let equivalent point1 point2 =
 120   repr point1 == repr point2
 121
 122 (** [eunion point1 point2] is identical to [union], except it does
 123     nothing if [point1] and [point2] are already equivalent. *)
 124 let eunion point1 point2 =
 125   if not (equivalent point1 point2) then
 126     union point1 point2
 127
 128 (** [redundant] maps all members of an equivalence class, but one, to
 129     [true]. *)
 130 let redundant = function
 131   | { link = Link _ } ->
 132       true
 133   | { link = Info _ } ->
 134       false
 135