(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** Generic hash-consing. *)
(** {6 Hashconsing functorial interface} *)
type'a f = 'a -> int * 'a (** Type of hashconsing function for ['a]. The returned int is the hash. *)
module type HashconsedType = sig (** {6 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. *)
val hashcons : t f (** The actual hashconsing function. It should be compatible with [eq], that is
[eq x (snd @@ hashcons f x) = true]. It also returns the hash. *)
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. It should be compatible with the hash returned by [hashcons], ie [eq x y] implies [fst @@ hashcons x = fst @@ hashcons y].
*) end
module type HashconsedRecType = sig type t
val hashcons : t f -> t f (** Hashcons the given constructor, calling the provided function on children. *)
val eq : t -> t -> bool end
module type S = sig type t (** Type of objects to hashcons. *)
type table (** Type of hashconsing tables *)
val generate : unit -> table (** This create a hashtable of the hashconsed objects. *)
val hcons : table -> t f (** Perform the hashconsing of the given object within the table, and returns the hash. *)
val stats : table -> Hashset.statistics (** Recover statistics of the hashconsing table. *) end
module Make (X : HashconsedType) : (S withtype t = X.t) (** Create a new hashconsing, given canonicalization functions. *)
module MakeRec (X : HashconsedRecType) : (S withtype t = X.t) (** Create a new hashconsing, given canonicalization functions.
[hashcons] will get the resulting [hcons] as first argument. *)
(** {6 Wrappers} *)
(** 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]. *)
(** {6 Hashconsing of usual structures} *)
module type HashedType = sig type t val hcons : t f end
module Hlist (D:HashedType) : (S withtype 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. *)
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
