package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.clib/Hashcons/index.html

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.