hashcons.mli 2.67 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

12
(** Hash tables for hash consing
Francois Bobot's avatar
Francois Bobot committed
13

14 15
    Hash consing tables are using weak pointers, so that values that are no
    more referenced from anywhere else can be erased by the GC.
16

17
    Look in src/core/term.ml for usage examples. *)
18

19 20 21 22 23
(** Values to be hash-consed must implement signature [HashedType] below.
    Type [t] is the type of values to be hash-consed.
    The user must provide an equality and a hash function over type [t],
    as well as a function [tag] to build a new value of type [t] from
    an old one and a unique integer tag. *)
24 25 26 27

module type HashedType =
  sig
    type t
28 29 30
    val equal : t -> t -> bool
    val hash : t -> int
    val tag : int -> t -> t
31 32 33 34 35 36
  end

module type S =
  sig
    type t

37
    val hashcons : t -> t
38 39 40 41 42 43 44 45 46 47
      (** [hashcons n] hash-cons value [n] i.e. returns any existing
          value in the table equal to [n], if any; otherwise, creates
          a new value with function [tag], stores it in the table and
          returns it. *)

    val unique : t -> t
      (** [unique n] registers the new value [n] without hash-consing.
          This should be used in case where the value is guaranteed to
          be unique, i.e. not equal to any other value, old or future.
          Unique values are not visited by [iter]. *)
48 49

    val iter : (t -> unit) -> unit
50 51
      (** [iter f] iterates [f] over all elements of the table. *)

52 53
    val stats : unit -> int * int * int * int * int * int
      (** Return statistics on the table.  The numbers are, in order:
54 55 56
          table length, number of entries, sum of bucket lengths,
          smallest bucket length, median bucket length, biggest
          bucket length. *)
57 58
  end

59
module Make(H : HashedType) : (S with type t = H.t)
60 61 62 63 64 65 66 67


(* helpers *)

val combine : int -> int -> int
val combine2 : int -> int -> int -> int
val combine3 : int -> int -> int -> int -> int
val combine_list : ('a -> int) -> int -> 'a list -> int
68 69
val combine_option : ('a -> int) -> 'a option -> int
val combine_pair : ('a -> int) -> ('b -> int) -> 'a * 'b -> int