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	abate	271	module type ARG =
2			sig
3			type 'a t
4			val dump: Format.formatter -> 'a t -> unit
5	abate	269
6	abate	271	val equal: 'a t -> 'a t -> bool
7			val hash: 'a t -> int
8			val compare: 'a t -> 'a t -> int
9			end
10	abate	269
11	abate	271	module type S =
12			sig
13			type 'a elem
14			type 'a t
15	abate	269
16	abate	271	val dump: Format.formatter -> 'a t -> unit
17	abate	269
18	abate	271	val equal : 'a t -> 'a t -> bool
19			val compare: 'a t -> 'a t -> int
20			val hash: 'a t -> int
21	abate	269
22	abate	271	val get: 'a t -> ('a elem list * 'a elem list) list
23	abate	269
24	abate	271	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	abate	269
31	abate	271	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	abate	269	(*
74	abate	271	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	abate	269	*)
80	abate	271	let rec hash = function
81			\| True -> 1
82			\| False -> 0
83			\| Split(h, _,_,_,_) -> h
84	abate	269
85	abate	271	let compute_hash x p i n =
86			(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
87	abate	269
88	abate	271	let atom x =
89			let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
90			Split (h, x,True,False,False)
91	abate	269
92
93	abate	271	let rec iter f = function
94			\| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
95			\| _ -> ()
96	abate	269
97	abate	271	(* TODO: precompute hash value for Split node to have fast equality... *)
98	abate	269
99	abate	271	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	abate	269
106
107	abate	271	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	abate	269
157	abate	271	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	abate	269	(* Invariants:
164			Split (x, pos,ign,neg) ==> (ign <> True);
165			(pos <> False or neg <> False)
166			*)
167
168	abate	271	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	abate	269
173
174	abate	271	(* Invariant:
175			- no ``subsumption'
176			*)
177	abate	269
178	abate	271	let rec simplify a l =
179			if (a = False) then False else simpl_aux1 a [] l
180			and simpl_aux1 a accu = function
181	abate	269	\| [] ->
182			if accu = [] then a else
183	abate	271	(match a with
184			\| True -> True
185			\| False -> assert false
186			\| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
187	abate	269	\| 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	abate	271	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	abate	269
216	abate	271	let rec ( ++ ) a b =
217	abate	272	(* if equal a b then a *)
218			if a == b then a
219	abate	271	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	abate	269
231	abate	271	(* Pseudo-Invariant:
232			- pos <> neg
233			*)
234	abate	269
235	abate	271	let split x pos ign neg =
236			if equal pos neg then (neg ++ ign) else split x pos ign neg
237	abate	269
238	abate	271	(* seems better not to make ++ and this split mutually recursive;
239			is the invariant still inforced ? *)
240	abate	269
241	abate	271	let rec ( ** ) a b =
242	abate	272	(* if equal a b then a *)
243			if a == b then a
244	abate	271	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	abate	269
264	abate	271	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	abate	272	(* if equal a b then False *)
274	abate	271	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