Source file `HashCons.ml`

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
(******************************************************************************)
(*                                                                            *)
(*                                    Fix                                     *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Library General Public License version 2, with a         *)
(*  special exception on linking, as described in the file LICENSE.           *)
(*                                                                            *)
(******************************************************************************)

open Sigs

(* The interface that we expose is not fully safe: it is possible, by applying
   the functor [Make] twice, to construct two instances of the hash-consing
   service that produce hash-consed values of *compatible* type [M.key cell]. *)

(* To achieve greater safety, one might wish to make the functor [Make]
   generative, so that each application of [Make] creates a fresh abstract
   type [t] which is convertible (in one direction only) into [M.key cell].
   However, that would render [Make] impossible to use in situations where the
   user wishes to hash-cons a type of trees. Indeed, the user needs to first
   define a (concrete, recursive) type of trees, then create an instance of
   the hash-consing service. If [Make] produces an abstract type, then the
   type definition and the functor application must be mutually recursive,
   which is not permitted. *)

type 'data cell =
  { id: int; data: 'data }

let id x =
  x.id

let data x =
  x.data

let equal x y =
  x.id = y.id
    (* We could also use physical equality, saving two reads. *)

let compare x y =
  compare x.id y.id
    (* To compare two cells, we compare their unique identifiers. *)

let hash x =
  Hashtbl.hash x.id
    (* To hash a cell, we hash its unique identifier. *)
    (* We could also return [x.id] without hashing it. *)

module type SERVICE = sig
  type data
  val make: data -> data cell
end

(* Creating a fresh hash-consing service is a simple matter of:
   1- creating a new gensym;
   2- memoizing the function [fun data -> { id = gensym(); data }]. *)

module Make (M : MEMOIZER) = struct

  type data =
    M.key

  let gensym =
    Gensym.make()

  let make =
    M.memoize (fun data -> { id = gensym(); data })

end

module ForHashedType
  (T : HashedType)
     = Make(Memoize.ForHashedType(T))

(* Hash-consing is a situation where a weak hash table can be used. Indeed, a
   hash-consing service based on a weak hash table can forget about a datum
   only if the user himself has forgotten about it. Thus, at different points
   in time, a datum *can* receive distinct IDs; but the user *can never* catch
   us red-handed, that is, can never at a given instant hold two pieces of
   data that are logically equal yet have distinct IDs. Thus, our
   constant-time implementation of [equal] remains correct. *)

module ForHashedTypeWeak
  (T : HashedType)
     = Make(Memoize.Make(Glue.WeakHashTablesAsImperativeMaps(T)))