blob: 17831caf99acd4e0ee2d0a49d4255dec49dcc2a1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** The following module is a specialized version of [Hashtbl] that is
a better space saver. In each cell of the internal bucketlist of a
hashtable, there are two representations of the same value. In this
implementation, there is only one.
Besides, the responsibility of computing the hash function is now
given to the caller, which makes possible the interleaving of the
hash key computation and the hash-consing. *)
module type EqType = sig
type t
val equal : t -> t -> bool
end
module type S = sig
type elt
(** Type of hashsets elements. *)
type t
(** Type of hashsets. *)
val create : int -> t
(** [create n] creates a fresh hashset with initial size [n]. *)
val repr : int -> elt -> t -> elt
(** [repr key constr set] uses [key] to look for [constr]
in the hashet [set]. If [constr] is in [set], returns the
specific representation that is stored in [set]. Otherwise,
[constr] is stored in [set] and will be used as the canonical
representation of this value in the future. *)
end
module Make (E : EqType) : S with type elt = E.t
module Combine : sig
val combine : int -> int -> int
val combinesmall : int -> int -> int
val combine3 : int -> int -> int -> int
val combine4 : int -> int -> int -> int -> int
end
|
