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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(************************************************************************)
(* * 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 with type t = X.t)
(** Create a new hashconsing, given canonicalization functions. *)
module 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. *)
(** {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 with type 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. *)
|
