2bfe70c63e703721acf98efad34afdb4558d9d95
[tatoo.git] / src / utils / finiteCofinite.ml
1 (***********************************************************************)
2 (*                                                                     *)
3 (*                               TAToo                                 *)
4 (*                                                                     *)
5 (*                     Kim Nguyen, LRI UMR8623                         *)
6 (*                   Universit√© Paris-Sud & CNRS                       *)
7 (*                                                                     *)
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   *)
12 (*  ../LICENSE.                                                        *)
13 (*                                                                     *)
14 (***********************************************************************)
15
16 (*
17   Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
18 *)
19
20 INCLUDE "utils.ml"
21
22 include FiniteCofinite_sig
23
24 module type HConsBuilder =
25   functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
26
27 module Builder (HCB : HConsBuilder) (E : Ptset.S) :
28   S with type elt = E.elt and type set = E.t =
29 struct
30   type elt = E.elt
31   type node = Finite of E.t | CoFinite of E.t
32   type set = E.t
33   module Node = HCB(struct
34     type t = node
35     let equal a b =
36       match a, b with
37         Finite s1, Finite s2
38       | CoFinite s1, CoFinite s2 -> E.equal s1 s2
39       | (Finite _| CoFinite _), _ -> false
40
41     let hash = function
42       | Finite s -> HASHINT2 (PRIME1, E.hash s)
43       | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
44   end)
45   include Node
46   let empty = make (Finite E.empty)
47   let any = make (CoFinite E.empty)
48   let finite x = make (Finite x)
49   let cofinite x = make (CoFinite x)
50
51   let is_empty t =  match t.node with
52     | Finite s -> E.is_empty s
53     | CoFinite _  -> false
54
55   let is_any t = match t.node with
56     | CoFinite s -> E.is_empty s
57     | Finite _  -> false
58
59   let is_finite t = match t.node with
60     | Finite _ -> true
61     | CoFinite _ -> false
62
63   let kind t = match t.node with
64     | Finite _ -> `Finite
65     | CoFinite _  -> `Cofinite
66
67   let mem x t = match t.node with
68     | Finite s -> E.mem x s
69     | CoFinite s -> not (E.mem x s)
70
71   let singleton x = finite (E.singleton x)
72
73   let add e t = match t.node with
74     | Finite s -> finite (E.add e s)
75     | CoFinite s -> cofinite (E.remove e s)
76
77   let remove e t = match t.node with
78     | Finite s -> finite (E.remove e s)
79     | CoFinite s -> cofinite (E.add e s)
80
81   let union s t = match s.node, t.node with
82     | Finite s, Finite t -> finite (E.union s t)
83     | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
84     | Finite s, CoFinite t -> cofinite (E.diff t s)
85     | CoFinite s, Finite t-> cofinite (E.diff s t)
86
87   let inter s t = match s.node, t.node with
88     | Finite s, Finite t -> finite (E.inter s t)
89     | CoFinite s, CoFinite t -> cofinite (E.union s t)
90     | Finite s, CoFinite t -> finite (E.diff s t)
91     | CoFinite s, Finite t-> finite (E.diff t s)
92
93   let diff s t = match s.node, t.node with
94     | Finite s, Finite t -> finite (E.diff s t)
95     | Finite s, CoFinite t -> finite(E.inter s t)
96     | CoFinite s, Finite t -> cofinite(E.union t s)
97     | CoFinite s, CoFinite t -> finite (E.diff t s)
98
99   let complement t = match t.node with
100     | Finite s -> cofinite s
101     | CoFinite s -> finite s
102
103   let compare s t = match s.node, t.node with
104     | Finite s , Finite t -> E.compare s t
105     | CoFinite s , CoFinite t -> E.compare t s
106     | Finite _, CoFinite _ -> -1
107     | CoFinite _, Finite _ -> 1
108
109   let subset s t = match s.node, t.node with
110     | Finite s , Finite t -> E.subset s t
111     | CoFinite s , CoFinite t -> E.subset t s
112     | Finite s, CoFinite t -> E.is_empty (E.inter s t)
113     | CoFinite _, Finite _ -> false
114
115   (* given a  list l of type t list,
116      returns two sets (f,c) where :
117      - f is the union of all the finite sets of l
118      - c is the union of all the cofinite sets of l
119      - f and c are disjoint
120      Invariant : cup f c = List.fold_left cup empty l
121      We treat the CoFinite part explicitely :
122   *)
123
124   let kind_split l =
125
126     let rec next_finite_cofinite facc cacc = function
127       | [] -> finite facc, cofinite (E.diff cacc facc)
128       | { node = Finite s; _ } ::r ->
129         next_finite_cofinite (E.union s facc) cacc r
130       | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
131         next_finite_cofinite facc cacc r
132       | { node = CoFinite s; _ } ::r ->
133         next_finite_cofinite facc (E.inter cacc s) r
134     in
135     let rec first_cofinite facc = function
136       | [] -> empty,empty
137       | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
138       | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
139     in
140       first_cofinite E.empty l
141
142   let exn = FiniteCofinite_sig.InfiniteSet
143
144   let fold f t a = match t.node with
145     | Finite s -> E.fold f s a
146     | CoFinite _ -> raise exn
147
148   let iter f t = match t.node with
149     | Finite t -> E.iter f t
150     | CoFinite _ -> raise exn
151
152   let for_all f t = match t.node with
153     | Finite s -> E.for_all f s
154     | CoFinite _ -> raise exn
155
156   let exists f t = match t.node with
157     | Finite s -> E.exists f s
158     | CoFinite _ -> raise exn
159
160   let filter f t = match t.node with
161     | Finite s -> finite (E.filter f s)
162     | CoFinite _ -> raise exn
163
164   let partition f t = match t.node with
165     | Finite s -> let a,b = E.partition f s in finite a,finite b
166     | CoFinite _ -> raise exn
167
168   let cardinal t = match t.node with
169     | Finite s -> E.cardinal s
170     | CoFinite _ -> raise exn
171
172   let elements t = match t.node with
173     | Finite s -> E.elements s
174     | CoFinite _ -> raise exn
175
176   let from_list l =
177     finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
178
179   let choose t = match t.node with
180       Finite s -> E.choose s
181     | CoFinite _ -> raise exn
182
183   let is_singleton t = match t.node with
184     | Finite s -> E.is_singleton s
185     | CoFinite _ -> false
186
187   let intersect s t = match s.node, t.node with
188     | Finite s, Finite t -> E.intersect s t
189     | CoFinite s, Finite t -> not (E.subset t s)
190     | Finite s, CoFinite t -> not (E.subset s t)
191     | CoFinite _ , CoFinite _ -> true
192
193   let split x s = match s.node with
194     | Finite s ->
195       let s1, b, s2 = E.split x s in
196       finite s1, b, finite s2
197
198     | CoFinite _ -> raise exn
199
200   let min_elt s = match s.node with
201     | Finite s -> E.min_elt s
202     | CoFinite _ -> raise exn
203
204   let max_elt s = match s.node with
205     | Finite s -> E.min_elt s
206     | CoFinite _ -> raise exn
207
208   let positive t = match t.node with
209       | Finite x -> x
210       | CoFinite _ -> E.empty
211
212   let negative t = match t.node with
213       | CoFinite x -> x
214       | Finite _ -> E.empty
215
216   let inj_positive t = finite t
217   let inj_negative t = cofinite t
218 end
219
220 module Make = Builder(Hcons.Make)
221 module Weak = Builder(Hcons.Weak)