1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
17 include Sigs.FINITECOFINITE
19 module type HConsBuilder =
20 functor (H : Sigs.AUX.HashedType) -> Hcons.S with type data = H.t
22 module Builder (HCB : HConsBuilder) (E : Ptset.S) :
23 S with type elt = E.elt and type set = E.t =
26 type node = Finite of E.t | CoFinite of E.t
28 module Node = HCB(struct
32 Finite (s1), Finite (s2)
33 | CoFinite (s1), CoFinite (s2) -> E.equal s1 s2
37 | Finite s -> HASHINT2 (PRIME1, E.hash s)
38 | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
41 let empty = make (Finite E.empty)
42 let any = make (CoFinite E.empty)
43 let finite x = make (Finite x)
44 let cofinite x = make (CoFinite x)
46 let is_empty = function
47 | { node = Finite s } when E.is_empty s -> true
51 | { node = CoFinite s } when E.is_empty s -> true
54 let is_finite t = match t.node with
55 | Finite _ -> true | _ -> false
57 let kind t = match t.node with
61 let mem x t = match t.node with
62 | Finite s -> E.mem x s
63 | CoFinite s -> not (E.mem x s)
65 let singleton x = finite (E.singleton x)
67 let add e t = match t.node with
68 | Finite s -> finite (E.add e s)
69 | CoFinite s -> cofinite (E.remove e s)
71 let remove e t = match t.node with
72 | Finite s -> finite (E.remove e s)
73 | CoFinite s -> cofinite (E.add e s)
75 let union s t = match s.node, t.node with
76 | Finite s, Finite t -> finite (E.union s t)
77 | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
78 | Finite s, CoFinite t -> cofinite (E.diff t s)
79 | CoFinite s, Finite t-> cofinite (E.diff s t)
81 let inter s t = match s.node, t.node with
82 | Finite s, Finite t -> finite (E.inter s t)
83 | CoFinite s, CoFinite t -> cofinite (E.union s t)
84 | Finite s, CoFinite t -> finite (E.diff s t)
85 | CoFinite s, Finite t-> finite (E.diff t s)
87 let diff s t = match s.node, t.node with
88 | Finite s, Finite t -> finite (E.diff s t)
89 | Finite s, CoFinite t -> finite(E.inter s t)
90 | CoFinite s, Finite t -> cofinite(E.union t s)
91 | CoFinite s, CoFinite t -> finite (E.diff t s)
93 let complement t = match t.node with
94 | Finite s -> cofinite s
95 | CoFinite s -> finite s
97 let compare s t = match s.node, t.node with
98 | Finite s , Finite t -> E.compare s t
99 | CoFinite s , CoFinite t -> E.compare t s
100 | Finite _, CoFinite _ -> -1
101 | CoFinite _, Finite _ -> 1
103 let subset s t = match s.node, t.node with
104 | Finite s , Finite t -> E.subset s t
105 | CoFinite s , CoFinite t -> E.subset t s
106 | Finite s, CoFinite t -> E.is_empty (E.inter s t)
107 | CoFinite _, Finite _ -> false
109 (* given a list l of type t list,
110 returns two sets (f,c) where :
111 - f is the union of all the finite sets of l
112 - c is the union of all the cofinite sets of l
113 - f and c are disjoint
114 Invariant : cup f c = List.fold_left cup empty l
115 We treat the CoFinite part explicitely :
120 let rec next_finite_cofinite facc cacc = function
121 | [] -> finite facc, cofinite (E.diff cacc facc)
122 | { node = Finite s } ::r ->
123 next_finite_cofinite (E.union s facc) cacc r
124 | { node = CoFinite _ } ::r when E.is_empty cacc ->
125 next_finite_cofinite facc cacc r
126 | { node = CoFinite s } ::r ->
127 next_finite_cofinite facc (E.inter cacc s) r
129 let rec first_cofinite facc = function
131 | { node = Finite s } :: r-> first_cofinite (E.union s facc) r
132 | { node = CoFinite s } :: r -> next_finite_cofinite facc s r
134 first_cofinite E.empty l
136 let exn = Sigs.FINITECOFINITE.InfiniteSet
138 let fold f t a = match t.node with
139 | Finite s -> E.fold f s a
140 | CoFinite _ -> raise exn
142 let iter f t = match t.node with
143 | Finite t -> E.iter f t
144 | CoFinite _ -> raise exn
146 let for_all f t = match t.node with
147 | Finite s -> E.for_all f s
148 | CoFinite _ -> raise exn
150 let exists f t = match t.node with
151 | Finite s -> E.exists f s
152 | CoFinite _ -> raise exn
154 let filter f t = match t.node with
155 | Finite s -> finite (E.filter f s)
156 | CoFinite _ -> raise exn
158 let partition f t = match t.node with
159 | Finite s -> let a,b = E.partition f s in finite a,finite b
160 | CoFinite _ -> raise exn
162 let cardinal t = match t.node with
163 | Finite s -> E.cardinal s
164 | CoFinite _ -> raise exn
166 let elements t = match t.node with
167 | Finite s -> E.elements s
168 | CoFinite _ -> raise exn
171 finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
173 let choose t = match t.node with
174 Finite s -> E.choose s
177 let is_singleton t = match t.node with
178 | Finite s -> E.is_singleton s
181 let intersect s t = match s.node, t.node with
182 | Finite s, Finite t -> E.intersect s t
183 | CoFinite s, Finite t -> not (E.subset t s)
184 | Finite s, CoFinite t -> not (E.subset s t)
185 | CoFinite s, CoFinite t -> true
187 let split x s = match s.node with
189 let s1, b, s2 = E.split x s in
190 finite s1, b, finite s2
194 let min_elt s = match s.node with
195 | Finite s -> E.min_elt s
198 let max_elt s = match s.node with
199 | Finite s -> E.min_elt s
212 let inj_positive t = finite t
213 let inj_negative t = cofinite t
216 module Make = Builder(Hcons.Make)
217 module Weak = Builder(Hcons.Weak)