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
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
16

17
    Look in src/core/term.ml for usage examples. *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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. *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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]. *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48 49

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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. *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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