package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module HashconsSource

Generic hash-consing.

Hashconsing functorial interface
Sourcetype 'a f = 'a -> int * 'a

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

Sourcemodule type HashconsedType = sig ... end
Sourcemodule type HashconsedRecType = sig ... end
Sourcemodule type S = sig ... end
Sourcemodule Make (X : HashconsedType) : S with type t = X.t

Create a new hashconsing, given canonicalization functions.

Sourcemodule 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.

Wrappers

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

Sourceval 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.

Hashconsing of usual structures
Sourcemodule type HashedType = sig ... end
Sourcemodule Hlist (D : HashedType) : S with type t = D.t list

Hashconsing of lists.

Sourceval 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.