package acgtk

  1. Overview
  2. Docs

This module implements a UnionFind data structure. The S parameter is used to try different implementations of indexed data structure, in particular eventually persistent arrays as described in "A Persistent Union-Find Data Structure" (Sylvain Conchon and Jean-Chrisophe Filliâtre

Parameters

module Value : sig ... end

Signature

type t

The type of the indexed data structure

type content =
  1. | Value of Value.value
  2. | Constr of int * int list

The type of the values (content) that are indexed. It is either an actual value of type 'a or a link to another indexed value. If a content at an index i points to i, it is meant that to be a variable.

exception Union_Failure

Exception raised when a the union of to indexed value can not happen. It should be raised by the union function when it amounts to make the union between to actual values Value a and Value b and a != b.

create l returns the corresponding indexed storage data structure where each value (or link) is indexed by its position in l (starting at 1

val empty : t
val generate_new_var : t -> int * t
val generate_new_constr : t -> (int * int list) -> int * t

generate_new_constr h (c,var_args) returns a pair (j,h') where h' is h updated with a new index j that contains a Constr(c,var_args) value. var_args is a list of already defined indexed of h (not checked here).

val extract : ?start:int -> int -> t -> content list

extract ~start:s i t returns a list of the i first elements of t starting from position s (default is 1, first position). It is ensured that the results only contain the values of representatives (i.e it follows the Link_to links until the value of the representative before returning it).

val find : int -> t -> (int * content) * t

find i h returns not only the index of the representative and the values it indexes, but also the storage data structure, so that the find algorithm can modify it, in particular with path compression. If the returned content is a Link_to j then j=i.

val union : int -> int -> t -> t

union i j h returns a new indexed storage data structure where values indexed by i and j have been unified (ie one of the two is now linked to the index of the representative of the other. It fails and raises the Union_Failure exception if both i and j representatives index actual values Value a and Value b and a != b.

val instantiate : int -> Value.value -> Value.t -> t -> t

instantiate i t h returns a new indexed storage data structure where the value indexed by i and t have been unified. It fails and raises the Union_Failure exception if i's representative indexes an actual values Value a such that a differs from t.

val cyclic : int -> t -> bool * t

cyclic i h returns a pair (b,h') where b is true if h has a cycle (following the Link_to links) containing i and false otherwise, and where h' contains the same information as h (possibly differently stored, for instance using path compression while checking h cyclicity.

val copy : t -> t
val to_string : t -> string
val log_content : Logs.level -> t -> unit