viewcvs.cgi/misc/bool.ml

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
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) &&
          (X.equal x1 x2) && (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 (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


(*
  let rec hash = function
    | True -> 1
    | False -> 2
    | Split (x, p,i,n) -> 
        (X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
*)
  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


  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) ->
        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
          and n = diff (aux p) (atom x) in
          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

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

  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


(* Invariant:
   - no ``subsumption'
*)

  let rec simplify a l =
    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 ->
        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
        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 ->
        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
        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 equal a b then a *)
    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) ->
          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 =
(*    if equal a b then a *)
    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) ->
          let c = X.compare x1 x2 in
          if c = 0 then
(*          split x1 
              (p1 ** (p2 ++ i2) ++ (p2 ** i1))
              (i1 ** i2)
              (n1 ** (n2 ++ i2) ++ (n2 ** i1))
*)
            split x1 
              ((p1 ++ i1) ** (p2 ++ i2))
              False
              ((n1 ++ i1) ** (n2 ++ i2))
          else if c < 0 then
            split x1 (p1 ** b) (i1 ** b) (n1 ** b)
          else
            split x2 (p2 ** a) (i2 ** a) (n2 ** a)

  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 =  
(*    if equal a b then False *)
    if a == b then False
    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
            split x1 (p1 // b) (i1 // b) (n1 // b)
(*          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 = ( // )

  let diff x y =
(*    let d = diff x y in
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
      dump x dump y dump d;  *)
    diff x y
end
1	module type ARG =
2	sig
3	type 'a t
4	val dump: Format.formatter -> 'a t -> unit
5
6	val equal: 'a t -> 'a t -> bool
7	val hash: 'a t -> int
8	val compare: 'a t -> 'a t -> int
9	end
10
11	module type S =
12	sig
13	type 'a elem
14	type 'a t
15
16	val dump: Format.formatter -> 'a t -> unit
17
18	val equal : 'a t -> 'a t -> bool
19	val compare: 'a t -> 'a t -> int
20	val hash: 'a t -> int
21
22	val get: 'a t -> ('a elem list * 'a elem list) list
23
24	val empty : 'a t
25	val full : 'a t
26	val cup : 'a t -> 'a t -> 'a t
27	val cap : 'a t -> 'a t -> 'a t
28	val diff : 'a t -> 'a t -> 'a t
29	val atom : 'a elem -> 'a t
30
31	val iter: ('a elem-> unit) -> 'a t -> unit
32
33	val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
34	-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
35	atom:('a elem -> 'b) -> 'a t -> 'b
36
37	val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
38	(Format.formatter -> unit) list
39	end
40
41	module Make(X : ARG) =
42	struct
43	type 'a elem = 'a X.t
44	type 'a t =
45	\| True
46	\| False
47	\| Split of int * 'a elem * 'a t * 'a t * 'a t
48
49	let rec equal a b =
50	(a == b) \|\|
51	match (a,b) with
52	\| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
53	(h1 == h2) &&
54	(X.equal x1 x2) && (equal p1 p2) & (equal i1 i2) &&
55	(equal n1 n2)
56	\| _ -> false
57
58	let rec compare a b =
59	if (a == b) then 0
60	else match (a,b) with
61	\| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
62	if h1 < h2 then -1 else if h1 > h2 then 1
63	else let c = X.compare x1 x2 in if c <> 0 then c
64	else let c = compare p1 p2 in if c <> 0 then c
65	else let c = compare i1 i2 in if c <> 0 then c
66	else compare n1 n2
67	\| True,_ -> -1
68	\| _, True -> 1
69	\| False,_ -> -1
70	\| _,False -> 1
71
72
73	(*
74	let rec hash = function
75	\| True -> 1
76	\| False -> 2
77	\| Split (x, p,i,n) ->
78	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
79	*)
80	let rec hash = function
81	\| True -> 1
82	\| False -> 0
83	\| Split(h, _,_,_,_) -> h
84
85	let compute_hash x p i n =
86	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
87
88	let atom x =
89	let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
90	Split (h, x,True,False,False)
91
92
93	let rec iter f = function
94	\| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
95	\| _ -> ()
96
97	(* TODO: precompute hash value for Split node to have fast equality... *)
98
99	let rec dump ppf = function
100	\| True -> Format.fprintf ppf "+"
101	\| False -> Format.fprintf ppf "-"
102	\| Split (_,x, p,i,n) ->
103	Format.fprintf ppf "%a(@[%a,%a,%a@])"
104	X.dump x dump p dump i dump n
105
106
107	let rec print f ppf = function
108	\| True -> Format.fprintf ppf "Any"
109	\| False -> Format.fprintf ppf "Empty"
110	\| Split (_, x, p,i, n) ->
111	let flag = ref false in
112	let b () = if !flag then Format.fprintf ppf " \| " else flag := true in
113	(match p with
114	\| True -> b(); Format.fprintf ppf "%a" f x
115	\| False -> ()
116	\| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
117	(match i with
118	\| True -> assert false;
119	\| False -> ()
120	\| _ -> b(); print f ppf i);
121	(match n with
122	\| True -> b (); Format.fprintf ppf "@[~%a@]" f x
123	\| False -> ()
124	\| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
125
126	let print a f = function
127	\| True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
128	\| False -> []
129	\| c -> [ fun ppf -> print f ppf c ]
130
131
132	let rec get accu pos neg = function
133	\| True -> (pos,neg) :: accu
134	\| False -> accu
135	\| Split (_,x, p,i,n) ->
136	let accu = get accu (x::pos) neg p in
137	let accu = get accu pos (x::neg) n in
138	let accu = get accu pos neg i in
139	accu
140
141	let get x = get [] [] [] x
142
143	let compute ~empty ~full ~cup ~cap ~diff ~atom b =
144	let rec aux = function
145	\| True -> full
146	\| False -> empty
147	\| Split(_,x, p,i,n) ->
148	let p = cap (atom x) (aux p)
149	and i = aux i
150	and n = diff (aux p) (atom x) in
151	cup (cup p i) n
152	in
153	aux b
154
155	(* Invariant: correct hash value *)
156
157	let split x pos ign neg =
158	Split (compute_hash x pos ign neg, x, pos, ign, neg)
159
160	let empty = False
161	let full = True
162
163	(* Invariants:
164	Split (x, pos,ign,neg) ==> (ign <> True);
165	(pos <> False or neg <> False)
166	*)
167
168	let split x pos ign neg =
169	if ign = True then True
170	else if (pos = False) && (neg = False) then ign
171	else split x pos ign neg
172
173
174	(* Invariant:
175	- no ``subsumption'
176	*)
177
178	let rec simplify a l =
179	if (a = False) then False else simpl_aux1 a [] l
180	and simpl_aux1 a accu = function
181	\| [] ->
182	if accu = [] then a else
183	(match a with
184	\| True -> True
185	\| False -> assert false
186	\| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
187	\| False :: l -> simpl_aux1 a accu l
188	\| True :: l -> False
189	\| b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
190	and simpl_aux2 x p i n ap ai an = function
191	\| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
192	\| (Split (_,x2,p2,i2,n2) as b) :: l ->
193	let c = X.compare x2 x in
194	if c < 0 then
195	simpl_aux3 x p i n ap ai an l i2
196	else if c > 0 then
197	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
198	else
199	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
200	\| _ -> assert false
201	and simpl_aux3 x p i n ap ai an l = function
202	\| False -> simpl_aux2 x p i n ap ai an l
203	\| True -> assert false
204	\| Split (_,x2,p2,i2,n2) as b ->
205	let c = X.compare x2 x in
206	if c < 0 then
207	simpl_aux3 x p i n ap ai an l i2
208	else if c > 0 then
209	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
210	else
211	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
212
213	let split x p i n =
214	split x (simplify p [i]) i (simplify n [i])
215
216	let rec ( ++ ) a b =
217	(* if equal a b then a *)
218	if a == b then a
219	else match (a,b) with
220	\| True, _ \| _, True -> True
221	\| False, a \| a, False -> a
222	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
223	let c = X.compare x1 x2 in
224	if c = 0 then
225	split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
226	else if c < 0 then
227	split x1 p1 (i1 ++ b) n1
228	else
229	split x2 p2 (i2 ++ a) n2
230
231	(* Pseudo-Invariant:
232	- pos <> neg
233	*)
234
235	let split x pos ign neg =
236	if equal pos neg then (neg ++ ign) else split x pos ign neg
237
238	(* seems better not to make ++ and this split mutually recursive;
239	is the invariant still inforced ? *)
240
241	let rec ( ** ) a b =
242	(* if equal a b then a *)
243	if a == b then a
244	else match (a,b) with
245	\| True, a \| a, True -> a
246	\| False, _ \| _, False -> False
247	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
248	let c = X.compare x1 x2 in
249	if c = 0 then
250	(* split x1
251	(p1 (p2 ++ i2) ++ (p2 i1))
252	(i1 ** i2)
253	(n1 (n2 ++ i2) ++ (n2 i1))
254	*)
255	split x1
256	((p1 ++ i1) ** (p2 ++ i2))
257	False
258	((n1 ++ i1) ** (n2 ++ i2))
259	else if c < 0 then
260	split x1 (p1 b) (i1 b) (n1 ** b)
261	else
262	split x2 (p2 a) (i2 a) (n2 ** a)
263
264	let rec neg = function
265	\| True -> False
266	\| False -> True
267	(* \| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
268	\| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
269	\| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n) *)
270	\| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
271
272	let rec ( // ) a b =
273	(* if equal a b then False *)
274	if a == b then False
275	else match (a,b) with
276	\| False,_ \| _, True -> False
277	\| a, False -> a
278	\| True, b -> neg b
279	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
280	let c = X.compare x1 x2 in
281	if c = 0 then
282	split x1
283	((p1 ++ i1) // (p2 ++ i2))
284	False
285	((n1 ++ i1) // (n2 ++ i2))
286	else if c < 0 then
287	split x1 (p1 // b) (i1 // b) (n1 // b)
288	(* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *)
289	else
290	split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
291
292
293	let cup = ( ++ )
294	let cap = ( ** )
295	let diff = ( // )
296
297	let diff x y =
298	(* let d = diff x y in
299	Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
300	dump x dump y dump d; *)
301	diff x y
302	end