bool.ml 10.5 KB
Newer Older
1
2
module type S =
sig
3
4
  type elem
  include Custom.T
5

6
  val get: t -> (elem list * elem list) list
7

8
9
10
11
12
13
  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t
14

15
  val iter: (elem-> unit) -> t -> unit
16
17
18

  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) 
    -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
19
    atom:(elem -> 'b) -> t -> 'b
20

21
  val print: string -> (Format.formatter -> elem -> unit) -> t ->
22
    (Format.formatter -> unit) list
23

24
  val trivially_disjoint: t -> t -> bool
25
26
end

27
module Make(X : Custom.T) =
28
struct
29
30
  type elem = X.t
  type t =
31
32
    | True
    | False
33
    | Split of int * elem * t * t * t
34

35
  include Custom.Dummy
36
37
38
39
40
41

  let rec equal a b =
    (a == b) ||
    match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
	  (h1 == h2) &&
42
43
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
44
45
      | _ -> false

46
47
48
49
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)


50
51
52
53
54
55
56
57
58
59
60
61
62
  let rec compare a b =
    if (a == b) then 0 
    else match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
	  if h1 < h2 then -1 else if h1 > h2 then 1 
	  else let c = X.compare x1 x2 in if c <> 0 then c
	  else let c = compare p1 p2 in if c <> 0 then c
	  else let c = compare i1 i2 in if c <> 0 then c 
	  else compare n1 n2
      | True,_  -> -1
      | _, True -> 1
      | False,_ -> -1
      | _,False -> 1
63
64


65
66
67
68
69
70
71
72
  let rec hash = function
    | True -> 1
    | False -> 0
    | Split(h, _,_,_,_) -> h

  let compute_hash x p i n = 
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)

73
74
75
76
77
78
79
80
81
82

  let rec check = function
    | True | False -> ()
    | Split (h,x,p,i,n) ->
	assert (h = compute_hash x p i n);
	(match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match i with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	check p; check i; check n

83
84
85
  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
    Split (h, x,True,False,False)
86
87
88
89
 
  let neg_atom x =
    let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
    Split (h, x,False,False,True)
90
91
92
93
94
95
96
97
98
99
100

  let rec iter f = function
    | Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
    | _ -> ()

  let rec dump ppf = function
    | True -> Format.fprintf ppf "+"
    | False -> Format.fprintf ppf "-"
    | Split (_,x, p,i,n) -> 
	Format.fprintf ppf "%a(@[%a,%a,%a@])" 
	X.dump x dump p dump i dump n
101
102


103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
  let rec print f ppf = function
    | True -> Format.fprintf ppf "Any"
    | False -> Format.fprintf ppf "Empty"
    | Split (_, x, p,i, n) ->
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
	(match p with 
	   | True -> b(); Format.fprintf ppf "%a" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
	(match i with 
	   | True -> assert false;
	   | False -> ()
	   | _ -> b(); print f ppf i);
	(match n with 
	   | True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
	
  let print a f = function
    | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | False -> []
    | c -> [ fun ppf -> print f ppf c ]
	
	
  let rec get accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x, p,i,n) ->
132
	(*OPT: can avoid creating this list cell when pos or neg =False *)
133
134
135
136
137
138
139
140
141
142
143
144
145
146
	let accu = get accu (x::pos) neg p in
	let accu = get accu pos (x::neg) n in
	let accu = get accu pos neg i in
	accu
	  
  let get x = get [] [] [] x
		
  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | True -> full
      | False -> empty
      | Split(_,x, p,i,n) ->
	  let p = cap (atom x) (aux p)
	  and i = aux i
147
	  and n = diff (aux n) (atom x) in
148
149
150
151
152
153
154
155
156
	  cup (cup p i) n
    in
    aux b
      
(* Invariant: correct hash value *)

  let split x pos ign neg =
    Split (compute_hash x pos ign neg, x, pos, ign, neg)

157
158
159
160

    


161
162
  let empty = False
  let full = True
163
164
165
166
167
168

(* Invariants:
     Split (x, pos,ign,neg) ==>  (ign <> True);   
     (pos <> False or neg <> False)
*)

169
170
171
172
  let split x pos ign neg =
    if ign = True then True 
    else if (pos = False) && (neg = False) then ign
    else split x pos ign neg
173
174


175
176
(* Invariant:
   - no ``subsumption'
177
*)
178

179
(*
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
  let rec simplify a b =
    if equal a b then False 
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, _ -> True
      | Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    let p1' = simplify (simplify p1 i2) p2 
	    and i1' = simplify i1 i2
	    and n1' = simplify (simplify n1 i2) n2 in
	    if (p1 != p1') || (n1 != n1') || (i1 != i1') 
	    then split x1 p1' i1' n1'
	    else a
	  else if c > 0 then
	    simplify a i2
	  else
	    let p1' = simplify p1 b 
	    and i1' = simplify i1 b
	    and n1' = simplify n1 b in
	    if (p1 != p1') || (n1 != n1') || (i1 != i1') 
	    then split x1 p1' i1' n1'
	    else a
204
205
206
*)


207
208
209
  let rec simplify a l =
    if (a = False) then False else simpl_aux1 a [] l
  and simpl_aux1 a accu = function
210
211
    | [] -> 
	if accu = [] then a else
212
213
214
215
	  (match a with
	     | True -> True
	     | False -> assert false
	     | Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
216
217
218
    | False :: l -> simpl_aux1 a accu l
    | True :: l -> False
    | b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
219
220
221
222
223
224
225
226
  and simpl_aux2 x p i n ap ai an = function
    | [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
    | (Split (_,x2,p2,i2,n2) as b) :: l ->
	let c = X.compare x2 x in
	if c < 0 then 
	  simpl_aux3 x p i n ap ai an l i2
	else if c > 0 then 
	  simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
227
	else
228
229
230
231
232
233
234
235
236
237
238
	  simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
    | _ -> assert false
  and simpl_aux3 x p i n ap ai an l = function
    | False -> simpl_aux2 x p i n ap ai an l
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
	let c = X.compare x2 x in
	if c < 0 then 
	  simpl_aux3 x p i n ap ai an l i2
	else if c > 0 then 
	  simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
239
	else
240
	  simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
241
242
243

	  
    
244
  let split x p i n = 
245
246
    split x (simplify p [i]) i (simplify n [i])

247
248

  let rec ( ++ ) a b =
249
250
(*    if equal a b then a *)
    if a == b then a  
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
    else match (a,b) with
      | True, _ | _, True -> True
      | False, a | a, False -> a
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
	  else if c < 0 then
	    split x1 p1 (i1 ++ b) n1
	  else
	    split x2 p2 (i2 ++ a) n2

(* Pseudo-Invariant:
   - pos <> neg
*)

  let split x pos ign neg =
    if equal pos neg then (neg ++ ign) else split x pos ign neg

(* seems better not to make ++ and this split mutually recursive;
   is the invariant still inforced ? *)

  let rec ( ** ) a b =
274
275
    (*    if equal a b then a *)
    if a == b then a
276
277
278
279
280
281
282
283
284
    else match (a,b) with
      | True, a | a, True -> a
      | False, _ | _, False -> False
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
(*	    split x1 
	      (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	      (i1 ** i2)
285
	      (n1 ** (n2 ++ i2) ++ (n2 ** i1))  *)
286
287
288
	    split x1 
	      ((p1 ++ i1) ** (p2 ++ i2))
	      False
289
	      ((n1 ++ i1) ** (n2 ++ i2)) 
290
291
292
293
294
	  else if c < 0 then
	    split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	  else
	    split x2 (p2 ** a) (i2 ** a) (n2 ** a)

295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
  let rec trivially_disjoint a b =
    if a == b then a = False
    else match (a,b) with
      | True, a | a, True -> a = False
      | False, _ | _, False -> true
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
	    trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
	    trivially_disjoint (n1 ++ i1) (n2 ++ i2)
	  else if c < 0 then
	    trivially_disjoint p1 b &&
	    trivially_disjoint i1 b &&
	    trivially_disjoint n1 b
	  else
	    trivially_disjoint p2 a &&
	    trivially_disjoint i2 a &&
	    trivially_disjoint n2 a

315
316
317
318
319
320
321
322
323
  let rec neg = function
    | True -> False
    | False -> True
(*    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
    | Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False 
    | Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)  *)
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
	      
  let rec ( // ) a b =  
324
325
(*    if equal a b then False  *)
    if a == b then False 
326
327
328
329
330
331
332
333
334
335
336
337
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    split x1
	      ((p1 ++ i1) // (p2 ++ i2))
	      False
	      ((n1 ++ i1) // (n2 ++ i2))
	  else if c < 0 then
338
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
339
340
341
342
343
344
345
346
347
(*	    split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b)  *)
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
	      

  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
 let rec serialize t = function
    | (True | False) as b -> 
	Serialize.Put.bool t true; Serialize.Put.bool t (b = True)
    | Split (_,x,p,i,n) ->
	Serialize.Put.bool t false;
	X.serialize t x;
	serialize t p;
	serialize t i;
	serialize t n

  let rec cap_atom x pos a = (* Assume that x does not appear in a *)
    match a with
      | False -> False
      | True -> if pos then atom x else neg_atom x
      | Split (_,y,p,i,n) ->
	  let c = X.compare x y in
	  assert (c <> 0);
	  if x < y then 
	    if pos then split x a False False
	    else split x False False a
	  else split y (cap_atom x pos p) (cap_atom x pos i) (cap_atom x pos n)


    
  let rec deserialize t =
    if Serialize.Get.bool t then
      if Serialize.Get.bool t then True else False
    else
      let x = X.deserialize t in
      let p = deserialize t in
      let i = deserialize t in
      let n = deserialize t in
      (cap_atom x true p) ++ i ++ (cap_atom x false n)
      (* split x p i n is not ok, because order of keys might have changed! *)
  
383
(*
384
  let diff x y =
385
    let d = diff x y in
386
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
387
388
389
390
391
392
393
394
395
      dump x dump y dump d;  
    d

  let cap x y =
    let d = cap x y in
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
      dump x dump y dump d;  
    d
*)
396
end