Hashcons (rocq-runtime.Hashcons)

type 'a f = 'a -> int * 'a

Type of hashconsing function for 'a. The returned int is the hash.

module type HashconsedType = sig ... end

module type HashconsedRecType = sig ... end

module type S = sig ... end

module Make (X : HashconsedType) : S with type t = X.t

Create a new hashconsing, given canonicalization functions.

module MakeRec (X : HashconsedRecType) : S with type t = X.t

Create a new hashconsing, given canonicalization functions. hashcons will get the resulting hcons as first argument.

These are intended to be used together with instances of the Make functor.

val simple_hcons : ('u -> 'tab) -> ('tab -> 't -> 'v) -> 'u -> 't -> 'v

Typically used as let hcons = simple_hcons H.generate H.hcons () where H is of type S.

module type HashedType = sig ... end

module Hlist (D : HashedType) : S with type t = D.t list

Hashconsing of lists.

val hashcons_array : 'v f -> 'v array f

Helper for array hashconsing. Shares the elements producing a new array if needed, does not mutate the array, does not share the array itself.