Data.Graph.Indexed.Util.DisjointSet

Definitions

record DisjointSet : Type -> Nat -> Type

  A simple [disjoint set](https://en.wikipedia.org/wiki/Disjoint-set_data_structure)
  implementation.
  
  This allows us to efficiently partition the values from 0 to `k-1`
  into disjoint sets. Operations like `root`, `size`, and `union`
  are de-facto amortized O(1).

Totality: total
Visibility: export
Constructor: 

DSF : MArray s k (DSNode k) -> DisjointSet s k

Projection: 

.arr : DisjointSet s k -> MArray s k (DSNode k)

ds : (k : Nat) -> F1 s (DisjointSet s k)

  Allocates a fresh `DisjointSet` data type with all
  values from `0` to `k-1` in their own partition.

Totality: total
Visibility: export

root : DisjointSet s k -> Fin k -> F1 s (Fin k)

  Returns the current root node of `x`, used for identifying
  the partition, to which `x` currently belongs.

Totality: total
Visibility: export

size : DisjointSet s k -> Fin k -> F1 s Nat

  Returns the size of the partition `x` currently belongs to.

Totality: total
Visibility: export

samePartition : DisjointSet s k -> Fin k -> Fin k -> F1 s Bool

  Returns `True` if `x` and `y` belong to the same partition,
  `False` otherwise.

Totality: total
Visibility: export

union : DisjointSet s k -> Fin k -> Fin k -> F1' s

  Computes the set union of the partitions of `x` and `y`.

Totality: total
Visibility: export

sets : DisjointSet s k -> F1 s (List (List (Fin k)))

Totality: total
Visibility: export