# Contents of /misc/bool.ml

Revision 269 - (show annotations)
Tue Jul 10 17:21:03 2007 UTC (5 years, 10 months ago) by abate
File size: 5922 byte(s)
```[r2003-03-22 15:22:10 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-22 15:22:11+00:00```
 1 type 'a obj = { id : int; mutable v : 'a } 2 3 type 'a t = 4 | True 5 | False 6 | Split of 'a obj * 'a t * 'a t * 'a t 7 8 let rec equal a b = 9 (a == b) || 10 match (a,b) with 11 | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) -> 12 (x1.id = x2.id) && (equal p1 p2) & (equal i1 i2) && 13 (equal n1 n2) 14 | _ -> false 15 16 let rec compare a b = 17 if (a == b) then 0 18 else match (a,b) with 19 | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) -> 20 if x1.id < x2.id then -1 21 else if x1.id > x2.id then 1 22 else let c = compare p1 p2 in if c <> 0 then c 23 else let c = compare i1 i2 in if c <> 0 then c 24 else compare n1 n2 25 | True,_ -> -1 26 | _, True -> 1 27 | False,_ -> -1 28 | _,False -> 1 29 30 let rec hash = function 31 | True -> 1 32 | False -> 2 33 | Split (x, p,i,n) -> 34 x.id + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n) 35 36 let rec iter f = function 37 | Split (x, p,i,n) -> f x.v; iter f p; iter f i; iter f n 38 | _ -> () 39 40 (* TODO: precompute hash value for Split node to have fast equality... *) 41 42 (* 43 let rec print f ppf = function 44 | True -> Format.fprintf ppf "True" 45 | False -> Format.fprintf ppf "False" 46 | Split (x, p,i,n) -> 47 Format.fprintf ppf "%a(@[%a,%a,%a@])" 48 f x.v (print f) p (print f) i (print f) n 49 *) 50 51 52 let rec print f ppf = function 53 | True -> Format.fprintf ppf "Any" 54 | False -> Format.fprintf ppf "Empty" 55 | Split (x, p,i, n) -> 56 (* Format.fprintf ppf "{%i}" x.id; *) 57 let flag = ref false in 58 let b () = if !flag then Format.fprintf ppf " | " else flag := true in 59 (match p with 60 | True -> b(); Format.fprintf ppf "%a" f x.v 61 | False -> () 62 | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x.v (print f) p ); 63 (match i with 64 | True -> assert false; 65 | False -> () 66 | _ -> b(); print f ppf i); 67 (match n with 68 | True -> b (); Format.fprintf ppf "@[~%a@]" f x.v 69 | False -> () 70 | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x.v (print f) n) 71 72 73 74 let rec dump ppf = function 75 | True -> Format.fprintf ppf "True" 76 | False -> Format.fprintf ppf "False" 77 | Split (x, p,i,n) -> 78 Format.fprintf ppf "%i(@[%a,%a,%a@])" 79 x.id dump p dump i dump n 80 81 let rec dnf accu pos neg = function 82 | True -> (pos,neg) :: accu 83 | False -> accu 84 | Split (x, p,i,n) -> 85 let accu = dnf accu (x.v::pos) neg p in 86 let accu = dnf accu pos (x.v::neg) n in 87 let accu = dnf accu pos neg i in 88 accu 89 90 let dnf x = dnf [] [] [] x 91 92 let compute ~empty ~any ~cup ~cap ~diff ~atom b = 93 let rec aux = function 94 | True -> any 95 | False -> empty 96 | Split(x, p,i,n) -> 97 let p = cap (atom x.v) (aux p) 98 and i = aux i 99 and n = diff (aux p) (atom x.v) in 100 cup (cup p i) n 101 in 102 aux b 103 104 (* Invariants: 105 Split (x, pos,ign,neg) ==> (ign <> True); 106 (pos <> False or neg <> False) 107 108 Other meaningful invariant that could be enforced: 109 - pos <> neg 110 - no ``subsumption'' --> DONE (cf below) 111 *) 112 113 let split x pos ign neg = 114 if ign = True then True 115 else if (pos = False) && (neg = False) then ign 116 else Split (x, pos, ign, neg) 117 118 119 let ( !! ) x = Split (x, True, False, False) 120 121 let empty = False 122 let any = True 123 124 let rec simplify a l = 125 (* Format.fprintf Format.std_formatter "simplify %a <=" dump a; 126 List.iter (fun b -> Format.fprintf Format.std_formatter " %a" dump b) l; 127 Format.fprintf Format.std_formatter "@\n"; 128 *) 129 if (a = False) then False else simpl_aux1 a [] l 130 and simpl_aux1 a accu = function 131 | [] -> 132 if accu = [] then a else 133 (match a with 134 | True -> True 135 | False -> assert false 136 | Split (x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu) 137 | False :: l -> simpl_aux1 a accu l 138 | True :: l -> False 139 | b :: l -> if a == b then False else simpl_aux1 a (b::accu) l 140 and simpl_aux2 x p i n ap ai an = function 141 | [] -> split x (simplify p ap) (simplify i ai) (simplify n an) 142 | (Split (x2,p2,i2,n2) as b) :: l -> 143 if x2.id < x.id then 144 simpl_aux3 x p i n ap ai an l i2 145 else if x.id < x2.id then 146 simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l 147 else 148 simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l 149 | _ -> assert false 150 and simpl_aux3 x p i n ap ai an l = function 151 | False -> simpl_aux2 x p i n ap ai an l 152 | True -> assert false 153 | Split (x2,p2,i2,n2) as b -> 154 if x2.id < x.id then 155 simpl_aux3 x p i n ap ai an l i2 156 else if x.id < x2.id then 157 simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l 158 else 159 simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l 160 161 let split x p i n = 162 split x (simplify p [i]) i (simplify n [i]) 163 164 let rec ( ++ ) a b = 165 if a == b then a 166 else match (a,b) with 167 | True, _ | _, True -> True 168 | False, a | a, False -> a 169 | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) -> 170 if x1.id = x2.id then 171 split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2) 172 else if x1.id < x2.id then 173 split x1 p1 (i1 ++ b) n1 174 else 175 split x2 p2 (i2 ++ a) n2 176 177 178 (* TODO: optimize the cup with 3 arguments ? *) 179 180 let rec ( ** ) a b = 181 if a == b then a 182 else match (a,b) with 183 | True, a | a, True -> a 184 | False, _ | _, False -> False 185 | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) -> 186 if x1.id = x2.id then 187 split x1 188 ((p1 ** p2) ++ (p1 ** i2) ++ (p2 ** i1)) 189 (i1 ** i2) 190 ((n1 ** n2) ++ (n1 ** i2) ++ (n2 ** i1)) 191 else if x1.id < x2.id then 192 split x1 (p1 ** b) (i1 ** b) (n1 ** b) 193 else 194 split x2 (p2 ** a) (i2 ** a) (n2 ** a) 195 196 let rec ( // ) a b = 197 if a == b then False 198 else match (a,b) with 199 | False,_ | _, True -> False 200 | a, False -> a 201 | True, Split (x2, p2,i2,n2) -> 202 let i = True // i2 in 203 split x2 (i // p2) False (i // n2) 204 | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) -> 205 if x1.id = x2.id then 206 let i = i1 // i2 in 207 split x1 208 ((p1 // p2 // i2) ++ (i // p2)) 209 False 210 ((n1 // n2 // i2) ++ (i // n2)) 211 else if x1.id < x2.id then 212 split x1 (p1 // b) (i1 // b) (n1 // b) 213 else 214 let i = a // i2 in 215 split x2 (i // p2) False (i // n2)