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 36 37 38 39
  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) &&
40 41
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
42 43
      | _ -> false

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


48 49 50 51 52 53 54 55 56 57 58 59 60
  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
61 62


63 64 65 66 67 68 69 70
  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)

71 72 73 74 75 76 77 78

  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) | _ -> ());
79
	X.check x; check p; check i; check n
80

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

  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
99 100


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
  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) ->
130
	(*OPT: can avoid creating this list cell when pos or neg =False *)
131 132 133 134 135 136 137 138 139 140 141 142 143 144
	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
145
	  and n = diff (aux n) (atom x) in
146 147 148 149 150 151 152 153 154
	  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)

155 156 157 158

    


159 160
  let empty = False
  let full = True
161 162 163 164 165 166

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

167 168 169 170
  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
171 172


173 174
(* Invariant:
   - no ``subsumption'
175
*)
176

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
  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
202 203 204
*)


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

	  
    
242
  let split x p i n = 
243 244
    split x (simplify p [i]) i (simplify n [i])

245 246

  let rec ( ++ ) a b =
247 248
(*    if equal a b then a *)
    if a == b then a  
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
    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 =
272 273
    (*    if equal a b then a *)
    if a == b then a
274 275 276 277 278 279 280 281 282
    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)
283
	      (n1 ** (n2 ++ i2) ++ (n2 ** i1))  *)
284 285 286
	    split x1 
	      ((p1 ++ i1) ** (p2 ++ i2))
	      False
287
	      ((n1 ++ i1) ** (n2 ++ i2)) 
288 289 290 291 292
	  else if c < 0 then
	    split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	  else
	    split x2 (p2 ** a) (i2 ** a) (n2 ** a)

293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
  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

313 314 315 316 317 318 319 320 321
  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 =  
322 323
(*    if equal a b then False  *)
    if a == b then False 
324 325 326 327 328 329 330 331 332 333 334 335
    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
336
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
337 338 339 340 341 342 343 344 345
(*	    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 = ( // )

346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
 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);
363
	  if (c < 0) then 
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
	    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! *)
  
381
(*
382
  let diff x y =
383
    let d = diff x y in
384
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
385 386 387 388 389 390 391 392 393
      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
*)
394
end