Module `Terms.UnionFind`

Union find structure: some terms points to their parents through the set of relations, allowing for accurate representation of relations in the group and storing fewer independent terms.

type 'a t = 'a t

type ('a, 'b) relation = ('a, 'b) Relation.t

type 'a node_through_relation =

| NodeThoughRelation : 'b t * ('a, 'b) relation -> 'a node_through_relation

Existential wrapper for returning the representative

val find_representative : 'a t -> 'a node_through_relation

Find the representative of a node, and the associated relation

val check_related : 'a t -> 'b t -> ('a, 'b) relation option

check_related a b returns the relation between a and b if they are in the same class.

val union : 
  'a t ->
  'b t ->
  ('a, 'b) relation ->
  (unit, ('a, 'b) relation) Stdlib.result

union m n r adds the m--(r)-->n relation to the union find returns Ok () on success, Error rel if m and n are already related via another relation rel and r != rel.

Module Terms.UnionFind

Module `Terms.UnionFind`