Module UnionFind.StoredSource

The mutable state of the union-find data structure is tracked in a store that is provided by the Store library. Every operation on the union-find data structure requires a store as a parameter. With a given instance of the union-find data structure, a single store must be used throughout. It is up to the user to ensure that this constraint is respected. Naturally, two independent instances of the union-find data structure can use two distinct stores.

'a rref is the type of elements, or references. Like the type 'a ref of ordinary references, this type supports the operations of creating a new reference, reading a reference, writing a reference, and testing whether two references are the same. Unlike ordinary references, this type also supports a form of merging: union merges two references, making them "the same reference".

This type is defined as an alias for 'a content Store.Ref.t, where Store.Ref.t is the type of stored references, and 'a content is an abstract type of meta-data required by the union-find machinery.

By revealing this information, we advertise the fact that union-find is implemented on top of the Store library. In particular, the state of the union-find data structure can be captured and restored by capturing and restoring the underlying store.

make s v creates a fresh reference and sets its content to v.

get s x returns the current content of the reference x.

set s x v sets the content of the reference x to v.

eq s x y determines whether the references x and y are "the same reference". At any point in time, eq is an equivalence relation on references: it is reflexive, symmetric, and transitive. When two references x and y are merged by invoking union s x y, they become the same reference: eq s x y becomes true, and remains forever true.

If eq s x y is true, then union s x y has no observable effect. Otherwise, union s x y merges the references x and y. In either case, after the call eq s x y is true.

union s x y returns a reference z such that eq s x z and eq s y z and is_representative s z are true.

The content of the reference that is returned is unchanged. The content of the reference that is not returned is lost.

If eq s x y is true initially, then merge f s x y has no observable effect. Otherwise, merge s f x y merges the references x and y and sets the content of the reference to f vx vy, where vx and vy are the initial contents of the references x and y. The function f is not allowed to access the union-find data structure. Under this restriction, merge s f x y is equivalent to:

  if eq s x y then
    find s x
  else
    let vx, vy = get s x, get s y in
    let v = f vx vy in
    let z = union s x y in
    set s z v;
    z

find s x returns a representative element of x's equivalence class. This element is chosen in an unspecified but deterministic manner, so two calls to find s x must return the same result, provided no calls to union take place in between. eq s x y is equivalent to find s x == find s y.

is_representative s x determines whether x is the representative element of its equivalence class. It is equivalent to find s x == x.