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 | |
---|