acgtk

Abstract Categorial Grammar development toolkit
Library acgtkLib.datalogLib
Module DatalogLib . Datalog . Datalog . UF
type 'a t

The type of the indexed data structure

type 'a content =
| Value of 'a

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.

val create : 'a content list -> 'a t

create l returns the corresponding indexed storage data structure where each value (or link) is indexed by its position in l (starting at 1). d is a data that may or may not be used to fill at init the indexed data structure.

val extract : ?start:int -> int -> 'a t -> 'a 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 -> 'a t -> (int * 'a content) * 'a 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 -> 'a t -> 'a 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 -> 'a -> 'a t -> 'a 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 -> 'a t -> bool * 'a 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 : 'a t -> 'a t
val to_string : 'a t -> string
val log_content : Logs.level -> 'a t -> unit