Source file `cSet.ml`

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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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 type ExtS =
sig
  include CSig.SetS
  module List : sig
    val union : t list -> t
  end
end

module SetExt (M : Set.OrderedType) :
sig
  type set = Set.Make(M).t
  module List : sig
    val union : set list -> set
  end
end =
struct
  module S = Set.Make(M)
  type set = S.t

  module List = struct
    let union = List.fold_left S.union S.empty
  end
end

module Make(M : Set.OrderedType) =
struct
  include Set.Make(M)
  include SetExt(M)
end

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