X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fhcons.ml;h=6a40b06b1dd326c2b02bef712e87be51ad141fd7;hb=6b66008811639324be623a42037b60e02056772c;hp=d421d03a30c2a5484e0bd821ebf61de75ba1e0ce;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git diff --git a/src/hcons.ml b/src/hcons.ml index d421d03..6a40b06 100644 --- a/src/hcons.ml +++ b/src/hcons.ml @@ -13,45 +13,27 @@ (* *) (***********************************************************************) -module type Abstract = - sig - type data - type t - val make : data -> t - val node : t -> data - val hash : t -> int - val uid : t -> Uid.t - val equal : t -> t -> bool - val init : unit -> unit - end +(* + Time-stamp: +*) -type 'a node = { id : Uid.t; - key : int; - node : 'a } -module type S = -sig - type data - type t = private { id : Uid.t; - key : int; - node : data } - include Abstract with type data := data and type t := t -end +include Sigs.HCONS module type TableBuilder = functor - (H : Sigs.HashedType) -> - Sigs.HashSet with type data = H.t + (H : Sigs.AUX.HashedType) -> + Sigs.AUX.HashSet with type data = H.t -module Builder (TB : TableBuilder) (H : Sigs.HashedType) = +module Builder (TB : TableBuilder) (H : Sigs.AUX.HashedType) = struct type data = H.t type t = { id : Uid.t; - key : int; + 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.key + let hash t = t.hash let equal t1 t2 = t1 == t2 module HN = struct @@ -68,7 +50,7 @@ struct uid_make := Uid.make_maker () let make x = - let cell = { id = Uid.dummy; key = H.hash x; node = x } in + let cell = { id = Uid.dummy; hash = H.hash x; node = x } in try T.find pool cell with @@ -88,9 +70,14 @@ struct 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 equal x y = x == y + let init () = () end