bool.ml 5.78 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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
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
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
type 'a obj = { id : int; mutable v : 'a }

type 'a t =
  | True
  | False
  | Split of 'a obj * 'a t * 'a t * 'a t

let rec equal a b =
  (a == b) ||
  match (a,b) with
    | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
	(x1.id = x2.id) && (equal p1 p2) & (equal i1 i2) &&
	(equal n1 n2)
    | _ -> false

let rec compare a b =
  if (a == b) then 0 
  else match (a,b) with
    | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
	if x1.id < x2.id then -1 
	else if x1.id > x2.id then 1
	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

let rec hash = function
  | True -> 1
  | False -> 2
  | Split (x, p,i,n) -> 
      x.id + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)

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

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

(*
let rec print f ppf = function
  | True -> Format.fprintf ppf "True"
  | False -> Format.fprintf ppf "False"
  | Split (x, p,i,n) -> 
      Format.fprintf ppf "%a(@[%a,%a,%a@])" 
	f x.v (print f) p (print f) i (print f) n
*)


let rec print f ppf = function
  | True -> Format.fprintf ppf "Any"
  | False -> Format.fprintf ppf "Empty"
  | Split (x, p,i, n) ->
(*      Format.fprintf ppf "{%i}" x.id; *)
      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.v
	 | False -> ()
	 | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x.v (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.v
	 | False -> ()
	 | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x.v (print f) n)



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

let rec dnf accu pos neg = function
  | True -> (pos,neg) :: accu
  | False -> accu
  | Split (x, p,i,n) ->
      let accu = dnf accu (x.v::pos) neg p in
      let accu = dnf accu pos (x.v::neg) n in
      let accu = dnf accu pos neg i in
      accu

let dnf x = dnf [] [] [] x

let compute ~empty ~any ~cup ~cap ~diff ~atom b =
  let rec aux = function
    | True -> any
    | False -> empty
    | Split(x, p,i,n) ->
	let p = cap (atom x.v) (aux p)
	and i = aux i
	and n = diff (aux p) (atom x.v) in
	cup (cup p i) n
  in
  aux b

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

   Other meaningful invariant that could be enforced:
   - pos <> neg
   - no ``subsumption''   --> DONE (cf below)
*)

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)


let ( !! ) x = Split (x, True, False, False)

let empty = False
let any = True

let rec simplify a l =
(*  Format.fprintf Format.std_formatter "simplify %a <=" dump a;
  List.iter (fun b ->  Format.fprintf Format.std_formatter " %a" dump b) l;
  Format.fprintf Format.std_formatter "@\n";
*)
  if (a = False) then False else simpl_aux1 a [] l
and simpl_aux1 a accu = function
    | [] -> 
	if accu = [] then a else
	(match a with
	   | True -> True
	   | False -> assert false
	   | Split (x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
    | False :: l -> simpl_aux1 a accu l
    | True :: l -> False
    | b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
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 ->
      if x2.id < x.id then 
	simpl_aux3 x p i n ap ai an l i2
      else if x.id < x2.id then 
	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
      else
	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 ->
      if x2.id < x.id then 
	simpl_aux3 x p i n ap ai an l i2
      else if x.id < x2.id then 
	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
      else
	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l

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

let rec ( ++ ) a b =
  if a == b then a 
  else match (a,b) with
    | True, _ | _, True -> True
    | False, a | a, False -> a
    | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
	if x1.id = x2.id then
	  split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
	else if x1.id < x2.id then
	  split x1 p1 (i1 ++ b) n1
	else
	  split x2 p2 (i2 ++ a) n2


(* TODO: optimize the cup with 3 arguments ? *)

let rec ( ** ) a b =
  if a == b then a
  else match (a,b) with
    | True, a | a, True -> a
    | False, _ | _, False -> False
    | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
	if x1.id = x2.id then
	  split x1 
	    ((p1 ** p2) ++ (p1 ** i2) ++ (p2 ** i1))
	    (i1 ** i2)
	    ((n1 ** n2) ++ (n1 ** i2) ++ (n2 ** i1))
	else if x1.id < x2.id then
	  split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else
	  split x2 (p2 ** a) (i2 ** a) (n2 ** a)

let rec ( // ) a b =  
  if a == b then False
  else match (a,b) with
    | False,_ | _, True -> False
    | a, False -> a
    | True, Split (x2, p2,i2,n2) ->
      	let i = True // i2 in
      	split x2 (i // p2) False (i // n2)
    | Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
      	if x1.id = x2.id then
	  let i = i1 // i2 in
	  split x1
	    ((p1 // p2 // i2) ++ (i // p2))
	    False
	    ((n1 // n2 // i2) ++ (i // n2))
	else if x1.id < x2.id then
	  split x1 (p1 // b) (i1 // b) (n1 // b)
	else
	  let i = a // i2 in
	  split x2 (i // p2) False (i // n2)