package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Generic hashconsing signature

Given an equivalence relation eq, a hashconsing function is a function that associates the same canonical element to two elements related by eq. Usually, the element chosen is canonical w.r.t. physical equality (==), so as to reduce memory consumption and enhance efficiency of equality tests.

In order to ensure canonicality, we need a way to remember the element associated to a class of equivalence; this is done using the table type generated by the Make functor.

type t

Type of objects to hashcons.

type u

Type of hashcons functions for the sub-structures contained in t. Usually a tuple of functions.

val hashcons : u -> t -> t

The actual hashconsing function, using its fist argument to recursively hashcons substructures. It should be compatible with eq, that is eq x (hashcons f x) = true.

val eq : t -> t -> bool

A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the hashcons function, but it should be insensible to shallow copy of the compared object.

val hash : t -> int

A hash function passed to the underlying hashtable structure. hash should be compatible with eq, i.e. if eq x y = true then hash x = hash y.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct