--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
+*)
+
+include Hcons_sig
+
+module type TableBuilder =
+ functor
+ (H : Common_sig.HashedType) ->
+ Common_sig.HashSet with type data = H.t
+
+module Builder (TB : TableBuilder) (H : Common_sig.HashedType) =
+struct
+ type data = H.t
+ type t = { id : Uid.t;
+ hash : int;
+ node : data }
+ let uid_make = ref (Uid.make_maker())
+ let node t = t.node
+ let uid t = t.id
+ let hash t = t.hash
+ let equal t1 t2 = t1 == t2
+ module HN =
+ struct
+ type _t = t
+ type t = _t
+ let hash = hash
+ let equal x y = x == y || H.equal x.node y.node
+ end
+ module T = TB(HN)
+
+ let pool = T.create 101
+ let init () =
+ T.clear pool;
+ uid_make := Uid.make_maker ()
+ let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
+
+ let make x =
+ let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
+ try
+ T.find pool cell
+ with
+ | Not_found ->
+ let cell = { cell with id = !uid_make(); } in
+ T.add pool cell;
+ cell
+end
+
+module Make = Builder (Misc.HashSet)
+module Weak = Builder (Weak.Make)
+
+module PosInt =
+struct
+ type data = int
+ type t = int
+ let make v =
+ if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
+ else v
+
+ let node v = v
+
+ let hash v = v
+
+ let uid v = Uid.of_int v
+ let dummy _ = ~-1
+ let equal x y = x == y
+
+ let init () = ()
+end