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

  val trivially_disjoint: 'a t -> 'a t -> bool
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 -> 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 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

  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;  
    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
*)
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
40	val trivially_disjoint: 'a t -> 'a t -> bool
41	end
42
43	module Make(X : ARG) =
44	struct
45	type 'a elem = 'a X.t
46	type 'a t =
47	\| True
48	\| False
49	\| Split of int * 'a elem * 'a t * 'a t * 'a t
50
51	let rec equal a b =
52	(a == b) \|\|
53	match (a,b) with
54	\| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
55	(h1 == h2) &&
56	(equal p1 p2) && (equal i1 i2) &&
57	(equal n1 n2) && (X.equal x1 x2)
58	\| _ -> false
59
60	(* Idea: add a mutable "unique" identifier and set it to
61	the minimum of the two when egality ... *)
62
63
64	let rec compare a b =
65	if (a == b) then 0
66	else match (a,b) with
67	\| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
68	if h1 < h2 then -1 else if h1 > h2 then 1
69	else let c = X.compare x1 x2 in if c <> 0 then c
70	else let c = compare p1 p2 in if c <> 0 then c
71	else let c = compare i1 i2 in if c <> 0 then c
72	else compare n1 n2
73	\| True,_ -> -1
74	\| _, True -> 1
75	\| False,_ -> -1
76	\| _,False -> 1
77
78
79	let rec hash = function
80	\| True -> 1
81	\| False -> 0
82	\| Split(h, _,_,_,_) -> h
83
84	let compute_hash x p i n =
85	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
86
87	let atom x =
88	let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
89	Split (h, x,True,False,False)
90
91
92	let rec iter f = function
93	\| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
94	\| _ -> ()
95
96	(* TODO: precompute hash value for Split node to have fast equality... *)
97
98	let rec dump ppf = function
99	\| True -> Format.fprintf ppf "+"
100	\| False -> Format.fprintf ppf "-"
101	\| Split (_,x, p,i,n) ->
102	Format.fprintf ppf "%a(@[%a,%a,%a@])"
103	X.dump x dump p dump i dump n
104
105
106	let rec print f ppf = function
107	\| True -> Format.fprintf ppf "Any"
108	\| False -> Format.fprintf ppf "Empty"
109	\| Split (_, x, p,i, n) ->
110	let flag = ref false in
111	let b () = if !flag then Format.fprintf ppf " \| " else flag := true in
112	(match p with
113	\| True -> b(); Format.fprintf ppf "%a" f x
114	\| False -> ()
115	\| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
116	(match i with
117	\| True -> assert false;
118	\| False -> ()
119	\| _ -> b(); print f ppf i);
120	(match n with
121	\| True -> b (); Format.fprintf ppf "@[~%a@]" f x
122	\| False -> ()
123	\| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
124
125	let print a f = function
126	\| True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
127	\| False -> []
128	\| c -> [ fun ppf -> print f ppf c ]
129
130
131	let rec get accu pos neg = function
132	\| True -> (pos,neg) :: accu
133	\| False -> accu
134	\| Split (_,x, p,i,n) ->
135	(OPT: can avoid creating this list cell when pos or neg =False )
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	(*
179	let rec simplify a b =
180	if equal a b then False
181	else match (a,b) with
182	\| False,_ \| _, True -> False
183	\| a, False -> a
184	\| True, _ -> True
185	\| Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
186	let c = X.compare x1 x2 in
187	if c = 0 then
188	let p1' = simplify (simplify p1 i2) p2
189	and i1' = simplify i1 i2
190	and n1' = simplify (simplify n1 i2) n2 in
191	if (p1 != p1') \|\| (n1 != n1') \|\| (i1 != i1')
192	then split x1 p1' i1' n1'
193	else a
194	else if c > 0 then
195	simplify a i2
196	else
197	let p1' = simplify p1 b
198	and i1' = simplify i1 b
199	and n1' = simplify n1 b in
200	if (p1 != p1') \|\| (n1 != n1') \|\| (i1 != i1')
201	then split x1 p1' i1' n1'
202	else a
203	*)
204
205
206	let rec simplify a l =
207	if (a = False) then False else simpl_aux1 a [] l
208	and simpl_aux1 a accu = function
209	\| [] ->
210	if accu = [] then a else
211	(match a with
212	\| True -> True
213	\| False -> assert false
214	\| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
215	\| False :: l -> simpl_aux1 a accu l
216	\| True :: l -> False
217	\| b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
218	and simpl_aux2 x p i n ap ai an = function
219	\| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
220	\| (Split (_,x2,p2,i2,n2) as b) :: l ->
221	let c = X.compare x2 x in
222	if c < 0 then
223	simpl_aux3 x p i n ap ai an l i2
224	else if c > 0 then
225	simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
226	else
227	simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
228	\| _ -> assert false
229	and simpl_aux3 x p i n ap ai an l = function
230	\| False -> simpl_aux2 x p i n ap ai an l
231	\| True -> assert false
232	\| Split (_,x2,p2,i2,n2) as b ->
233	let c = X.compare x2 x in
234	if c < 0 then
235	simpl_aux3 x p i n ap ai an l i2
236	else if c > 0 then
237	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	split x (simplify p [i]) i (simplify n [i])
245
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	split x1
286	((p1 ++ i1) ** (p2 ++ i2))
287	False
288	((n1 ++ i1) ** (n2 ++ i2))
289	else if c < 0 then
290	split x1 (p1 b) (i1 b) (n1 ** b)
291	else
292	split x2 (p2 a) (i2 a) (n2 ** a)
293
294	let rec trivially_disjoint a b =
295	if a == b then a = False
296	else match (a,b) with
297	\| True, a \| a, True -> a = False
298	\| False, _ \| _, False -> true
299	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
300	let c = X.compare x1 x2 in
301	if c = 0 then
302	(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
303	trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
304	trivially_disjoint (n1 ++ i1) (n2 ++ i2)
305	else if c < 0 then
306	trivially_disjoint p1 b &&
307	trivially_disjoint i1 b &&
308	trivially_disjoint n1 b
309	else
310	trivially_disjoint p2 a &&
311	trivially_disjoint i2 a &&
312	trivially_disjoint n2 a
313
314	let rec neg = function
315	\| True -> False
316	\| False -> True
317	(* \| Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
318	\| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
319	\| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n) *)
320	\| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
321
322	let rec ( // ) a b =
323	(* if equal a b then False *)
324	if a == b then False
325	else match (a,b) with
326	\| False,_ \| _, True -> False
327	\| a, False -> a
328	\| True, b -> neg b
329	\| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
330	let c = X.compare x1 x2 in
331	if c = 0 then
332	split x1
333	((p1 ++ i1) // (p2 ++ i2))
334	False
335	((n1 ++ i1) // (n2 ++ i2))
336	else if c < 0 then
337	split x1 (p1 // b) (i1 // b) (n1 // b)
338	(* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *)
339	else
340	split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
341
342
343	let cup = ( ++ )
344	let cap = ( ** )
345	let diff = ( // )
346
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	dump x dump y dump d;
352	d
353
354	let cap x y =
355	let d = cap x y in
356	Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
357	dump x dump y dump d;
358	d
359	*)
360	end