1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
module type OrderedType =
sig
type t
val compare : t -> t -> int
end
module type S = Set.S
module Make(M : OrderedType)= Set.Make(M)
module type HashedType =
sig
type t
val hash : t -> int
end
module Hashcons(M : OrderedType)(H : HashedType with type t = M.t) =
struct
module Set = Make(M)
type set = Set.t
type _set =
| SEmpty
| SNode of set * M.t * set * int
let set_prj : set -> _set = Obj.magic
let set_inj : _set -> set = Obj.magic
let rec spine s accu = match set_prj s with
| SEmpty -> accu
| SNode (l, v, r, _) -> spine l ((v, r) :: accu)
let rec umap f s = match set_prj s with
| SEmpty -> set_inj SEmpty
| SNode (l, v, r, h) ->
let l' = umap f l in
let r' = umap f r in
let v' = f v in
set_inj (SNode (l', v', r', h))
let rec eqeq s1 s2 = match s1, s2 with
| [], [] -> true
| (v1, r1) :: s1, (v2, r2) :: s2 ->
v1 == v2 && eqeq (spine r1 s1) (spine r2 s2)
| _ -> false
module Hashed =
struct
open Hashset.Combine
type t = set
type u = M.t -> M.t
let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0
let hashcons = umap
end
include Hashcons.Make(Hashed)
end
|