viewcvs.cgi/types/boolean.ml

(* Optimization ideas:
    -    (A|B) & (C|D) = A | (B & (C|D))    if A <= C
*)

module type S =
sig
  type 'a elem
  type 'a t

  val equal : 'a t -> 'a t -> bool
  val compare: 'a t -> 'a t -> int
  val hash: 'a t -> int

  external get: 'a t -> ('a elem list * 'a elem list) list = "%identity"

  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 map : ('a elem-> 'b elem) -> 'a t -> 'b t
  val iter: ('a elem -> unit) -> 'a t -> unit
  val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd) 
    -> cap:('c -> 'b -> 'c) -> diff:('c -> 'b -> 'c) ->
    atom:('a elem -> 'b) -> 'a t -> 'd
  val compute_bool: ('a elem -> 'b t) -> 'a t -> 'b t
    
  val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
    (Format.formatter -> unit) list
    

  val trivially_disjoint : 'a t -> 'a t -> bool    
  val check: 'a t -> unit
end

module Make(X : SortedList.ARG) = struct
  type 'a elem = 'a X.t
  module SList = SortedList.Make_transp(X)
  module SSList = SortedList.Make_transp
    (struct
       type 'a t = 'a SList.t * 'a SList.t
       let compare (x1,y1) (x2,y2) =
         let c = SList.compare x1 x2 in if c <> 0 then c
         else SList.compare y1 y2
       let equal (x1,y1) (x2,y2) =
         (SList.equal x1 x2) && (SList.equal y1 y2)
       let hash (x,y) =
         SList.hash x + 17 * SList.hash y
     end)
  type 'a t = 'a SSList.t
  let hash = SSList.hash
  let compare = SSList.compare
  let equal = SSList.equal

  external get: 'a t -> ('a elem list * 'a elem list) list = "%identity"


let empty = [ ]
let full  = [ [],[] ]

let atom x = [ [x],[] ]

let may_remove (p1,n1) (p2,n2) =
(*  false *)
  (SList.subset p2 p1) && (SList.subset n2 n1)

(* in some cases, it is faster to avoid may_remove...
   investigate this... *)


let cup t s = 
  if t == s then t
  else match (t,s) with
    | [],s -> s
    | t,[] -> t
    | [ [], [] ], _ | _, [ [], [] ] -> full
    | _ ->
        let s=
          SSList.filter 
            (fun (p,n) -> not (SSList.exists (may_remove (p,n)) t)) s in
        let t=
          SSList.filter 
            (fun (p,n) -> not (SSList.exists (may_remove (p,n)) s)) t in 
        SSList.cup s t

(*
let clean accu t =
  let rec aux accu = function
    | (p,n) :: rem ->
        if (List.exists (may_remove (p,n)) accu)
          || (List.exists (may_remove (p,n)) rem)
        then aux accu rem
        else aux ((p,n)::accu) rem 
    | [] -> accu
  in
  SSList.from_list (aux accu t)
*)

    
let rec fold2_aux f a x = function
  | [] -> x
  | h :: t -> fold2_aux f a (f x a h) t

let rec fold2 f x l1 l2 =
  match l1 with
    | [] -> x
    | h :: t -> fold2 f (fold2_aux f h x l2) t l2

let rec should_add x = function
  | [] -> true
  | y::rem -> if may_remove x y then false else should_add x rem

let rec clean_add accu x = function
  | [] -> accu
  | y::rem -> 
      if may_remove y x then clean_add accu x rem 
      else clean_add (y::accu) x rem

let cap s t =
  if s == t then s
  else if s == full then t
  else if t == full then s
  else if (s == empty) || (t == empty) then empty
  else
    let (lines1,common,lines2) = SSList.split s t in
    let rec aux lines (p1,n1) (p2,n2) =
        if (SList.disjoint p1 n2) && (SList.disjoint p2 n1)
        then 
          let x = (SList.cup p1 p2, SList.cup n1 n2) in
          if should_add x lines then clean_add [x] x lines else lines
        else lines
    in
    SSList.from_list 
      (fold2 aux (SSList.get common) (SSList.get lines1) (SSList.get lines2))

let diff c1 c2 =
  if (c2 == full) || (c1 == c2) then empty
  else if (c1 == empty) || (c2 == empty) then c1
  else
    let c1 = SSList.diff c1 c2 in
    let line (p,n) =
      let acc = SList.fold (fun acc a -> ([], [a]) :: acc) [] p in
      let acc = SList.fold (fun acc a -> ([a], []) :: acc) acc n in
      SSList.from_list acc
    in
    SSList.fold (fun c1 l -> cap c1 (line l)) c1 c2


let rec map f t =
  let lines =
    List.fold_left
      (fun lines (p,n) ->
         let p = SList.map f p and n = SList.map f n in
         if (SList.disjoint p n) then (p,n) :: lines else lines)
      []
      t
  in
  SSList.from_list lines

let iter f t =
  SSList.iter (fun (p,n) -> SList.iter f p; SList.iter f n) t

let compute ~empty ~full ~cup ~cap ~diff ~atom t =
  let line (p,n) =
    List.fold_left (fun accu x -> diff accu (atom x)) (
      List.fold_left (fun accu x -> cap accu (atom x)) full p
    ) n in
  List.fold_left (fun accu l -> cup accu (line l)) empty t
  
let compute_bool f = 
  compute ~empty ~full ~cup ~cap ~diff ~atom:f


let print any f =
  List.map 
    (function 
         (p1::p,n) -> 
           (fun ppf ->
              Format.fprintf ppf "@[%a" f p1;
              List.iter (fun x -> Format.fprintf ppf " &@ %a" f x) p;
              List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
              Format.fprintf ppf "@]";
           )
       | ([],[]) -> 
           (fun ppf -> Format.fprintf ppf "%s" any)
       | ([],[n]) ->
           (fun ppf -> Format.fprintf ppf "@[%s \\ %a@]" any f n)
       | ([],n1::n) ->
           (fun ppf -> 
              Format.fprintf ppf "@[%s" any;
              List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
              Format.fprintf ppf "@]";
           )
    )

let trivially_disjoint a b = cap a b = []

let check b = ()
(*
  SSList.check b;
  SSList.iter 
    (fun (p,n) -> 
       SList.check p; 
       SList.check n; 
       assert (SList.disjoint p n)
    )
    b
*)

end

include Make(
  struct 
    type 'a t = 'a 
    let hash = Hashtbl.hash 
    let equal x y = x = y 
    let compare = compare 
  end)
1	(* Optimization ideas:
2	- (A\|B) & (C\|D) = A \| (B & (C\|D)) if A <= C
3	*)
4
5	module type S =
6	sig
7	type 'a elem
8	type 'a t
9
10	val equal : 'a t -> 'a t -> bool
11	val compare: 'a t -> 'a t -> int
12	val hash: 'a t -> int
13
14	external get: 'a t -> ('a elem list * 'a elem list) list = "%identity"
15
16	val empty : 'a t
17	val full : 'a t
18	val cup : 'a t -> 'a t -> 'a t
19	val cap : 'a t -> 'a t -> 'a t
20	val diff : 'a t -> 'a t -> 'a t
21	val atom : 'a elem -> 'a t
22
23	val map : ('a elem-> 'b elem) -> 'a t -> 'b t
24	val iter: ('a elem -> unit) -> 'a t -> unit
25	val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd)
26	-> cap:('c -> 'b -> 'c) -> diff:('c -> 'b -> 'c) ->
27	atom:('a elem -> 'b) -> 'a t -> 'd
28	val compute_bool: ('a elem -> 'b t) -> 'a t -> 'b t
29
30	val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
31	(Format.formatter -> unit) list
32
33
34	val trivially_disjoint : 'a t -> 'a t -> bool
35	val check: 'a t -> unit
36	end
37
38	module Make(X : SortedList.ARG) = struct
39	type 'a elem = 'a X.t
40	module SList = SortedList.Make_transp(X)
41	module SSList = SortedList.Make_transp
42	(struct
43	type 'a t = 'a SList.t * 'a SList.t
44	let compare (x1,y1) (x2,y2) =
45	let c = SList.compare x1 x2 in if c <> 0 then c
46	else SList.compare y1 y2
47	let equal (x1,y1) (x2,y2) =
48	(SList.equal x1 x2) && (SList.equal y1 y2)
49	let hash (x,y) =
50	SList.hash x + 17 * SList.hash y
51	end)
52	type 'a t = 'a SSList.t
53	let hash = SSList.hash
54	let compare = SSList.compare
55	let equal = SSList.equal
56
57	external get: 'a t -> ('a elem list * 'a elem list) list = "%identity"
58
59
60	let empty = [ ]
61	let full = [ [],[] ]
62
63	let atom x = [ [x],[] ]
64
65	let may_remove (p1,n1) (p2,n2) =
66	(* false *)
67	(SList.subset p2 p1) && (SList.subset n2 n1)
68
69	(* in some cases, it is faster to avoid may_remove...
70	investigate this... *)
71
72
73	let cup t s =
74	if t == s then t
75	else match (t,s) with
76	\| [],s -> s
77	\| t,[] -> t
78	\| [ [], [] ], _ \| _, [ [], [] ] -> full
79	\| _ ->
80	let s=
81	SSList.filter
82	(fun (p,n) -> not (SSList.exists (may_remove (p,n)) t)) s in
83	let t=
84	SSList.filter
85	(fun (p,n) -> not (SSList.exists (may_remove (p,n)) s)) t in
86	SSList.cup s t
87
88	(*
89	let clean accu t =
90	let rec aux accu = function
91	\| (p,n) :: rem ->
92	if (List.exists (may_remove (p,n)) accu)
93	\|\| (List.exists (may_remove (p,n)) rem)
94	then aux accu rem
95	else aux ((p,n)::accu) rem
96	\| [] -> accu
97	in
98	SSList.from_list (aux accu t)
99	*)
100
101
102
103	let rec fold2_aux f a x = function
104	\| [] -> x
105	\| h :: t -> fold2_aux f a (f x a h) t
106
107	let rec fold2 f x l1 l2 =
108	match l1 with
109	\| [] -> x
110	\| h :: t -> fold2 f (fold2_aux f h x l2) t l2
111
112	let rec should_add x = function
113	\| [] -> true
114	\| y::rem -> if may_remove x y then false else should_add x rem
115
116	let rec clean_add accu x = function
117	\| [] -> accu
118	\| y::rem ->
119	if may_remove y x then clean_add accu x rem
120	else clean_add (y::accu) x rem
121
122	let cap s t =
123	if s == t then s
124	else if s == full then t
125	else if t == full then s
126	else if (s == empty) \|\| (t == empty) then empty
127	else
128	let (lines1,common,lines2) = SSList.split s t in
129	let rec aux lines (p1,n1) (p2,n2) =
130	if (SList.disjoint p1 n2) && (SList.disjoint p2 n1)
131	then
132	let x = (SList.cup p1 p2, SList.cup n1 n2) in
133	if should_add x lines then clean_add [x] x lines else lines
134	else lines
135	in
136	SSList.from_list
137	(fold2 aux (SSList.get common) (SSList.get lines1) (SSList.get lines2))
138
139	let diff c1 c2 =
140	if (c2 == full) \|\| (c1 == c2) then empty
141	else if (c1 == empty) \|\| (c2 == empty) then c1
142	else
143	let c1 = SSList.diff c1 c2 in
144	let line (p,n) =
145	let acc = SList.fold (fun acc a -> ([], [a]) :: acc) [] p in
146	let acc = SList.fold (fun acc a -> ([a], []) :: acc) acc n in
147	SSList.from_list acc
148	in
149	SSList.fold (fun c1 l -> cap c1 (line l)) c1 c2
150
151
152	let rec map f t =
153	let lines =
154	List.fold_left
155	(fun lines (p,n) ->
156	let p = SList.map f p and n = SList.map f n in
157	if (SList.disjoint p n) then (p,n) :: lines else lines)
158	[]
159	t
160	in
161	SSList.from_list lines
162
163	let iter f t =
164	SSList.iter (fun (p,n) -> SList.iter f p; SList.iter f n) t
165
166	let compute ~empty ~full ~cup ~cap ~diff ~atom t =
167	let line (p,n) =
168	List.fold_left (fun accu x -> diff accu (atom x)) (
169	List.fold_left (fun accu x -> cap accu (atom x)) full p
170	) n in
171	List.fold_left (fun accu l -> cup accu (line l)) empty t
172
173	let compute_bool f =
174	compute ~empty ~full ~cup ~cap ~diff ~atom:f
175
176
177	let print any f =
178	List.map
179	(function
180	(p1::p,n) ->
181	(fun ppf ->
182	Format.fprintf ppf "@[%a" f p1;
183	List.iter (fun x -> Format.fprintf ppf " &@ %a" f x) p;
184	List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
185	Format.fprintf ppf "@]";
186	)
187	\| ([],[]) ->
188	(fun ppf -> Format.fprintf ppf "%s" any)
189	\| ([],[n]) ->
190	(fun ppf -> Format.fprintf ppf "@[%s \\ %a@]" any f n)
191	\| ([],n1::n) ->
192	(fun ppf ->
193	Format.fprintf ppf "@[%s" any;
194	List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
195	Format.fprintf ppf "@]";
196	)
197	)
198
199	let trivially_disjoint a b = cap a b = []
200
201	let check b = ()
202	(*
203	SSList.check b;
204	SSList.iter
205	(fun (p,n) ->
206	SList.check p;
207	SList.check n;
208	assert (SList.disjoint p n)
209	)
210	b
211	*)
212
213	end
214
215	include Make(
216	struct
217	type 'a t = 'a
218	let hash = Hashtbl.hash
219	let equal x y = x = y
220	let compare = compare
221	end)