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

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


  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) ->
        (*OPT: can avoid creating this list cell when pos or neg =False *)
        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 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
(*
  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	(equal p1 p2) && (equal i1 i2) &&
55	(equal n1 n2) && (X.equal x1 x2)
56	\| _ -> false
57
58	(* Idea: add a mutable "unique" identifier and set it to
59	the minimum of the two when egality ... *)
60
61
62	let rec compare a b =
63	if (a == b) then 0
64	else match (a,b) with
65	\| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
66	if h1 < h2 then -1 else if h1 > h2 then 1
67	else let c = X.compare x1 x2 in if c <> 0 then c
68	else let c = compare p1 p2 in if c <> 0 then c
69	else let c = compare i1 i2 in if c <> 0 then c
70	else compare n1 n2
71	\| True,_ -> -1
72	\| _, True -> 1
73	\| False,_ -> -1
74	\| _,False -> 1
75
76
77	(*
78	let rec hash = function
79	\| True -> 1
80	\| False -> 2
81	\| Split (x, p,i,n) ->
82	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
83	*)
84	let rec hash = function
85	\| True -> 1
86	\| False -> 0
87	\| Split(h, _,_,_,_) -> h
88
89	let compute_hash x p i n =
90	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
91
92	let atom x =
93	let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
94	Split (h, x,True,False,False)
95
96
97	let rec iter f = function
98	\| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
99	\| _ -> ()
100
101	(* TODO: precompute hash value for Split node to have fast equality... *)
102
103	let rec dump ppf = function
104	\| True -> Format.fprintf ppf "+"
105	\| False -> Format.fprintf ppf "-"
106	\| Split (_,x, p,i,n) ->
107	Format.fprintf ppf "%a(@[%a,%a,%a@])"
108	X.dump x dump p dump i dump n
109
110
111	let rec print f ppf = function
112	\| True -> Format.fprintf ppf "Any"
113	\| False -> Format.fprintf ppf "Empty"
114	\| Split (_, x, p,i, n) ->
115	let flag = ref false in
116	let b () = if !flag then Format.fprintf ppf " \| " else flag := true in
117	(match p with
118	\| True -> b(); Format.fprintf ppf "%a" f x
119	\| False -> ()
120	\| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
121	(match i with
122	\| True -> assert false;
123	\| False -> ()
124	\| _ -> b(); print f ppf i);
125	(match n with
126	\| True -> b (); Format.fprintf ppf "@[~%a@]" f x
127	\| False -> ()
128	\| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
129
130	let print a f = function
131	\| True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
132	\| False -> []
133	\| c -> [ fun ppf -> print f ppf c ]
134
135
136	let rec get accu pos neg = function
137	\| True -> (pos,neg) :: accu
138	\| False -> accu
139	\| Split (_,x, p,i,n) ->
140	(OPT: can avoid creating this list cell when pos or neg =False )
141	let accu = get accu (x::pos) neg p in
142	let accu = get accu pos (x::neg) n in
143	let accu = get accu pos neg i in
144	accu
145
146	let get x = get [] [] [] x
147
148	let compute ~empty ~full ~cup ~cap ~diff ~atom b =
149	let rec aux = function
150	\| True -> full
151	\| False -> empty
152	\| Split(_,x, p,i,n) ->
153	let p = cap (atom x) (aux p)
154	and i = aux i
155	and n = diff (aux p) (atom x) in
156	cup (cup p i) n
157	in
158	aux b
159
160	(* Invariant: correct hash value *)
161
162	let split x pos ign neg =
163	Split (compute_hash x pos ign neg, x, pos, ign, neg)
164
165	let empty = False
166	let full = True
167
168	(* Invariants:
169	Split (x, pos,ign,neg) ==> (ign <> True);
170	(pos <> False or neg <> False)
171	*)
172
173	let split x pos ign neg =
174	if ign = True then True
175	else if (pos = False) && (neg = False) then ign
176	else split x pos ign neg
177
178
179	(* Invariant:
180	- no ``subsumption'
181	*)
182
183	let rec simplify a b =
184	if equal a b then False
185	else match (a,b) with
186	\| False,_ \| _, True -> False
187	\| a, False -> a
188	\| True, _ -> True
189	\| Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
190	let c = X.compare x1 x2 in
191	if c = 0 then
192	let p1' = simplify (simplify p1 i2) p2
193	and i1' = simplify i1 i2
194	and n1' = simplify (simplify n1 i2) n2 in
195	if (p1 != p1') \|\| (n1 != n1') \|\| (i1 != i1')
196	then split x1 p1' i1' n1'
197	else a
198	else if c > 0 then
199	simplify a i2
200	else
201	let p1' = simplify p1 b
202	and i1' = simplify i1 b
203	and n1' = simplify n1 b in
204	if (p1 != p1') \|\| (n1 != n1') \|\| (i1 != i1')
205	then split x1 p1' i1' n1'
206	else a
207	(*
208	let rec simplify a l =
209	if (a = False) then False else simpl_aux1 a [] l
210	and simpl_aux1 a accu = function
211	\| [] ->
212	if accu = [] then a else
213	(match a with
214	\| True -> True
215	\| False -> assert false
216	\| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
217	\| False :: l -> simpl_aux1 a accu l
218	\| True :: l -> False
219	\| b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
220	and simpl_aux2 x p i n ap ai an = function
221	\| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
222	\| (Split (_,x2,p2,i2,n2) as b) :: l ->
223	let c = X.compare x2 x in
224	if c < 0 then
225	simpl_aux3 x p i n ap ai an l i2
226	else if c > 0 then
227	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
228	else
229	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
230	\| _ -> assert false
231	and simpl_aux3 x p i n ap ai an l = function
232	\| False -> simpl_aux2 x p i n ap ai an l
233	\| True -> assert false
234	\| Split (_,x2,p2,i2,n2) as b ->
235	let c = X.compare x2 x in
236	if c < 0 then
237	simpl_aux3 x p i n ap ai an l i2
238	else if c > 0 then
239	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
240	else
241	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
242	*)
243
244	let split x p i n =
245	split x (simplify p i) i (simplify n i)
246
247	let rec ( ++ ) a b =
248	(* if equal a b then a *)
249	if a == b then a
250	else match (a,b) with
251	\| True, _ \| _, True -> True
252	\| False, a \| a, False -> a
253	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
254	let c = X.compare x1 x2 in
255	if c = 0 then
256	split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
257	else if c < 0 then
258	split x1 p1 (i1 ++ b) n1
259	else
260	split x2 p2 (i2 ++ a) n2
261
262	(* Pseudo-Invariant:
263	- pos <> neg
264	*)
265
266	let split x pos ign neg =
267	if equal pos neg then (neg ++ ign) else split x pos ign neg
268
269	(* seems better not to make ++ and this split mutually recursive;
270	is the invariant still inforced ? *)
271
272	let rec ( ** ) a b =
273	(* if equal a b then a *)
274	if a == b then a
275	else match (a,b) with
276	\| True, a \| a, True -> a
277	\| False, _ \| _, False -> False
278	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
279	let c = X.compare x1 x2 in
280	if c = 0 then
281	(* split x1
282	(p1 (p2 ++ i2) ++ (p2 i1))
283	(i1 ** i2)
284	(n1 (n2 ++ i2) ++ (n2 i1))
285	*)
286	split x1
287	((p1 ++ i1) ** (p2 ++ i2))
288	False
289	((n1 ++ i1) ** (n2 ++ i2))
290	else if c < 0 then
291	split x1 (p1 b) (i1 b) (n1 ** b)
292	else
293	split x2 (p2 a) (i2 a) (n2 ** a)
294
295	let rec neg = function
296	\| True -> False
297	\| False -> True
298	(* \| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
299	\| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
300	\| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n) *)
301	\| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
302
303	let rec ( // ) a b =
304	(* if equal a b then False *)
305	if a == b then False
306	else match (a,b) with
307	\| False,_ \| _, True -> False
308	\| a, False -> a
309	\| True, b -> neg b
310	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
311	let c = X.compare x1 x2 in
312	if c = 0 then
313	split x1
314	((p1 ++ i1) // (p2 ++ i2))
315	False
316	((n1 ++ i1) // (n2 ++ i2))
317	else if c < 0 then
318	split x1 (p1 // b) (i1 // b) (n1 // b)
319	(* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *)
320	else
321	split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
322
323
324	let cup = ( ++ )
325	let cap = ( ** )
326	let diff = ( // )
327
328	let diff x y =
329	(* let d = diff x y in
330	Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
331	dump x dump y dump d; *)
332	diff x y
333	end