Source file `Store.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
(***************************************************************************)
(*                                                                         *)
(*                                 UnionFind                               *)
(*                                                                         *)
(*                       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.        *)
(***************************************************************************)

(**The signature {!STORE} describes an implementation of first-class stores. *)
module type STORE = sig

  (**A store can be thought of as a region of memory in which objects, known
     as references, can be dynamically allocated, read, and written. Stores
     are homogeneous: all references in a store of type ['a store] have the
     content type, namely ['a]. In general, a store may be persistent or
     mutable, depending on which data structure is used to implement it. *)
  type 'a store

  (* We restrict our attention to homogeneous stores, because this is
     simpler and allows a wider range of implementations. *)

  (**[new_store()] creates an empty store. *)
  val new_store: unit -> 'a store

  (**A reference of type ['a rref] can be thought of as (a pointer to) an
     object that exists in some store. *)
  type 'a rref

  (* The type parameter ['a] in ['a rref] could be considered redundant, as it
     is not really necessary that both [store] and [rref] be parameterized.
     However, one can think of instances where ['a store] is a phantom type
     and ['a rref] really depends on ['a] AND of instances where the converse
     holds. *)

  (* For regularity, each of the four operations below takes a store as a
     parameter and returns a store as a result. One might think that [eq]
     does not need a store parameter, and that [get] and [eq] do not need a
     store result. However, in some implementations where the store is
     self-organizing, this may be necessary, so we bite the bullet and pay
     the cost in runtime and verbosity. *)

  (**[make s v] creates a fresh reference in the store [s] and sets its
     content to [v]. It returns a pair of an updated store and the
     newly-created reference. *)
  val make: 'a store -> 'a -> 'a store * 'a rref

  (**[get s x] reads the current content of the reference [x] in the store
     [s]. It returns a pair of a possibly-updated store and the current
     content of the reference. *)
  val get:  'a store -> 'a rref -> 'a store * 'a

  (**[set s x v] updates the store [s] so as to set the content of the
     reference [x] to [v]. It returns an updated store. *)
  val set:  'a store -> 'a rref -> 'a -> 'a store

  (**[eq s x y] determines whether the references [x] and [y] are the same
     reference. It returns a pair of a possibly-updated store and a Boolean
     result. The references [x] and [y] must belong to the store [s]. *)
  val eq: 'a store -> 'a rref -> 'a rref -> 'a store * bool

end