Source file Store.ml

(***************************************************************************)
(*                                                                         *)
(*                                 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 should be thought of as a
     mutable object. Some stores support a cheap [copy] operation, because the
     underlying data structure allows it: for instance, a store implemented as
     a reference to a persistent map supports cheap copies. Some stores do not
     support [copy] at all: for instance, a store implemented using primitive
     references does not support copies. *)
  type 'a store

  (* We choose an API where stores are mutable, so an operation that updates
     the store does not need to return a new store. The API includes a [copy]
     operation; this allows to simulate a persistent store by a mutable store
     that supports cheap copies. A store that is fundamentally not persistent
     can choose to not implement [copy]. *)

  (* 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

  (**[copy s] returns a copy of the store [s]. Every reference that is valid
     in the store [s] is also valid in the new store, and has the same content
     in both stores. The two stores are independent of one another: updating
     one of them does not affect the other. When supported, [copy] is cheap:
     it can be expected to run in constant time. However, some stores does not
     support [copy]; in that case, an unspecified exception is raised. *)
  val copy: 'a store -> '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 updates the store in place and returns the
     newly-created reference. *)
  val make: 'a store -> 'a -> 'a rref

  (**[get s x] reads the current content of the reference [x] in the store
     [s]. It may update the store in place, and returns the current content of
     the reference. *)
  val get:  'a store -> 'a rref -> 'a

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

  (**[eq s x y] determines whether the references [x] and [y] are the same
     reference. It may update the store in place, and returns a Boolean
     result. The references [x] and [y] must belong to the store [s]. *)
  val eq: 'a store -> 'a rref -> 'a rref -> bool

end