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 (***********************************************************************)
18 include FiniteCofinite_sig
20 module type HConsBuilder =
21 functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
23 module Builder (HCB : HConsBuilder) (E : Ptset.S) :
24 S with type elt = E.elt and type set = E.t =
27 type node = Finite of E.t | CoFinite of E.t
29 module Node = HCB(struct
34 | CoFinite s1, CoFinite s2 -> E.equal s1 s2
35 | (Finite _| CoFinite _), _ -> false
38 | Finite s -> HASHINT2 (PRIME1, E.hash s)
39 | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
42 let empty = make (Finite E.empty)
43 let any = make (CoFinite E.empty)
44 let finite x = make (Finite x)
45 let cofinite x = make (CoFinite x)
47 let is_empty t = match t.node with
48 | Finite s -> E.is_empty s
51 let is_any t = match t.node with
52 | CoFinite s -> E.is_empty s
55 let is_finite t = match t.node with
59 let kind t = match t.node with
61 | CoFinite _ -> `Cofinite
63 let mem x t = match t.node with
64 | Finite s -> E.mem x s
65 | CoFinite s -> not (E.mem x s)
67 let singleton x = finite (E.singleton x)
69 let add e t = match t.node with
70 | Finite s -> finite (E.add e s)
71 | CoFinite s -> cofinite (E.remove e s)
73 let remove e t = match t.node with
74 | Finite s -> finite (E.remove e s)
75 | CoFinite s -> cofinite (E.add e s)
77 let union s t = match s.node, t.node with
78 | Finite s, Finite t -> finite (E.union s t)
79 | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
80 | Finite s, CoFinite t -> cofinite (E.diff t s)
81 | CoFinite s, Finite t-> cofinite (E.diff s t)
83 let inter s t = match s.node, t.node with
84 | Finite s, Finite t -> finite (E.inter s t)
85 | CoFinite s, CoFinite t -> cofinite (E.union s t)
86 | Finite s, CoFinite t -> finite (E.diff s t)
87 | CoFinite s, Finite t-> finite (E.diff t s)
89 let diff s t = match s.node, t.node with
90 | Finite s, Finite t -> finite (E.diff s t)
91 | Finite s, CoFinite t -> finite(E.inter s t)
92 | CoFinite s, Finite t -> cofinite(E.union t s)
93 | CoFinite s, CoFinite t -> finite (E.diff t s)
95 let complement t = match t.node with
96 | Finite s -> cofinite s
97 | CoFinite s -> finite s
99 let compare s t = match s.node, t.node with
100 | Finite s , Finite t -> E.compare s t
101 | CoFinite s , CoFinite t -> E.compare t s
102 | Finite _, CoFinite _ -> -1
103 | CoFinite _, Finite _ -> 1
105 let subset s t = match s.node, t.node with
106 | Finite s , Finite t -> E.subset s t
107 | CoFinite s , CoFinite t -> E.subset t s
108 | Finite s, CoFinite t -> E.is_empty (E.inter s t)
109 | CoFinite _, Finite _ -> false
111 (* given a list l of type t list,
112 returns two sets (f,c) where :
113 - f is the union of all the finite sets of l
114 - c is the union of all the cofinite sets of l
115 - f and c are disjoint
116 Invariant : cup f c = List.fold_left cup empty l
117 We treat the CoFinite part explicitely :
122 let rec next_finite_cofinite facc cacc = function
123 | [] -> finite facc, cofinite (E.diff cacc facc)
124 | { node = Finite s; _ } ::r ->
125 next_finite_cofinite (E.union s facc) cacc r
126 | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
127 next_finite_cofinite facc cacc r
128 | { node = CoFinite s; _ } ::r ->
129 next_finite_cofinite facc (E.inter cacc s) r
131 let rec first_cofinite facc = function
133 | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
134 | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
136 first_cofinite E.empty l
138 let exn = FiniteCofinite_sig.InfiniteSet
140 let fold f t a = match t.node with
141 | Finite s -> E.fold f s a
142 | CoFinite _ -> raise exn
144 let fold_left f t a = match t.node with
145 | Finite s -> E.fold_left f s a
146 | CoFinite _ -> raise exn
148 let fold_right f t a = match t.node with
149 | Finite s -> E.fold_right f s a
150 | CoFinite _ -> raise exn
152 let iter f t = match t.node with
153 | Finite t -> E.iter f t
154 | CoFinite _ -> raise exn
156 let for_all f t = match t.node with
157 | Finite s -> E.for_all f s
158 | CoFinite _ -> raise exn
160 let exists f t = match t.node with
161 | Finite s -> E.exists f s
162 | CoFinite _ -> raise exn
164 let filter f t = match t.node with
165 | Finite s -> finite (E.filter f s)
166 | CoFinite _ -> raise exn
168 let partition f t = match t.node with
169 | Finite s -> let a,b = E.partition f s in finite a,finite b
170 | CoFinite _ -> raise exn
172 let cardinal t = match t.node with
173 | Finite s -> E.cardinal s
174 | CoFinite _ -> raise exn
176 let elements t = match t.node with
177 | Finite s -> E.elements s
178 | CoFinite _ -> raise exn
181 finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
183 let choose t = match t.node with
184 Finite s -> E.choose s
185 | CoFinite _ -> raise exn
187 let is_singleton t = match t.node with
188 | Finite s -> E.is_singleton s
189 | CoFinite _ -> false
191 let intersect s t = match s.node, t.node with
192 | Finite s, Finite t -> E.intersect s t
193 | CoFinite s, Finite t -> not (E.subset t s)
194 | Finite s, CoFinite t -> not (E.subset s t)
195 | CoFinite _ , CoFinite _ -> true
197 let split x s = match s.node with
199 let s1, b, s2 = E.split x s in
200 finite s1, b, finite s2
202 | CoFinite _ -> raise exn
204 let min_elt s = match s.node with
205 | Finite s -> E.min_elt s
206 | CoFinite _ -> raise exn
208 let max_elt s = match s.node with
209 | Finite s -> E.min_elt s
210 | CoFinite _ -> raise exn
212 let positive t = match t.node with
214 | CoFinite _ -> E.empty
216 let negative t = match t.node with
218 | Finite _ -> E.empty
220 let inj_positive t = finite t
221 let inj_negative t = cofinite t
224 module Make = Builder(Hcons.Make)
225 module Weak = Builder(Hcons.Weak)