Module `LabeledValued.PersistentArray`

Persistent array based labeled union-find lattice with values.

Parameters

module Config : Parameters.PERSISTENT_ARRAY_CONFIG

module Node : Parameters.NODE

module Relation : Parameters.GROUP

module Value : 
  Parameters.RELATIONAL_VALUE
    with type node = Node.t
     and type relation = Relation.t

Signature

include Sig.LABELED_UNION_FIND_LATTICE
  with type node = Node.t
  with type relation = Relation.t

type node = Node.t

The type of union-find nodes i.e. the elements of the partition set

type relation = Relation.t

The type of relations between nodes. These relations have a group structure.

type t

The type of the persistent labeled union-find (PUF) data-structure

Union-find operations

val make : int -> t

Create a new union-find, see UNION_FIND_LATTICE.make

val find : t -> node -> node * relation

find uf x returns:

the reprensentative of x
the relation between x and its representative It performs both the 'find' and 'get_value' operations from the paper.

val add_relation : t -> node -> node -> relation -> (t, relation) Stdlib.result

add_relation uf x y r returns a new persistent union-find, where the relation x --(r)--> y was added.

This is the union operation of classical union find, only this time it takes the new relation as an extra argument.

This fails if x and y were already related by a different relation in uf. In that case, that other relation is returned.

val check_related : t -> node -> node -> relation option

check_related uf x y checks if x and y are in the same relational class in uf. If so, the relation between them is returned. Otherwise, None is returned.

Lattice operations

val incl : t -> t -> bool

incl uf_a uf_b is lattice inclusion, uf_a <= uf_b, i.e. forall x y, if check_related uf_b x y then check_related uf_a x y

val join : t -> t -> t

join uf_a uf_b is the least upper-bound of uf_a and uf_b, i.e. forall x y, check_related (join uf_a uf_b) x y iff check_related uf_b x y and check_related uf_a x y

val meet : t -> t -> t * (node * relation * node) list

meet uf_a uf_b is a pair meet, extra_rel:

meet is (one of) the greatest lower bound of uf_a and uf_b. It contains all relations of uf_a and some of the relations of uf_b. (All nodes that are related in uf_b are still related, but their relation might be changed, as all relations may not be preserved)
extra_rel is a minimal list of relations from uf_b that could not be preserved. For example, if uf_a contains x --(r)--> y and uf_b contains x --(r')--> y with r != r', r' will either be in the list, or a transitive/symmetric consequence of relations that are in the list.

Testing and debugging

val copy : t -> t

To compare persistent union-find with non-persistent version, we need an explicit copy operation. This is Fun.id for all persistent versions.

val check_invariants : t -> string option

check_invariants uf is used in testing, to assert that the data-structures internal invariants, if any, are still true after complex operations.

Returns None if they hold, Some error_msg otherwise.

val pretty : Stdlib.Format.formatter -> t -> unit

pretty-printer

type value = Value.t

The type of values assigned to relational classes. Relation act as group actions on values: given a ('a, 'b) relation, we can transform a 'a value into a 'b value

val get_value : t -> node -> value option

get_value uf x returns the value attached to x, if it exists.

val set_value : intersect:bool -> t -> node -> value -> t

set_value ~intersect uf n v returns a new union-find, where the value attached to the class of n is now v. If intersect is true, this value will be combined with the previous value (should one exists) via Parameters.VALUE.meet.

Module LabeledValued.PersistentArray