bool.ml 9.46 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
module type ARG =
sig
    type 'a t
    val dump: Format.formatter -> 'a t -> unit

    val equal: 'a t -> 'a t -> bool
    val hash: 'a t -> int
    val compare: 'a t -> 'a t -> int
end

module type S =
sig
  type 'a elem
  type 'a t

  val dump: Format.formatter -> 'a t -> unit

  val equal : 'a t -> 'a t -> bool
  val compare: 'a t -> 'a t -> int
  val hash: 'a t -> int

  val get: 'a t -> ('a elem list * 'a elem list) list

  val empty : 'a t
  val full  : 'a t
  val cup   : 'a t -> 'a t -> 'a t
  val cap   : 'a t -> 'a t -> 'a t
  val diff  : 'a t -> 'a t -> 'a t
  val atom  : 'a elem -> 'a t

  val iter: ('a elem-> unit) -> 'a t -> unit

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

  val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
    (Format.formatter -> unit) list
39 40

  val trivially_disjoint: 'a t -> 'a t -> bool
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
end

module Make(X : ARG) =
struct
  type 'a elem = 'a X.t
  type 'a t =
    | True
    | False
    | Split of int * 'a elem * 'a t * 'a t * 'a t

  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) &&
56 57
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
58 59
      | _ -> false

60 61 62 63
(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)


64 65 66 67 68 69 70 71 72 73 74 75 76
  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
77 78


79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
  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)

  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
    Split (h, x,True,False,False)


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

(* TODO: precompute hash value for Split node to have fast equality... *)

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

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

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

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


174 175
(* Invariant:
   - no ``subsumption'
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 202
  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
203 204 205
*)


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

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

246 247

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

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

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

347
(*
348
  let diff x y =
349
    let d = diff x y in
350
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
351 352 353 354 355 356 357 358 359
      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
*)
360
end