viewcvs.cgi/types/boolean.ml

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 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) =
  (SList.subset p2 p1) && (SList.subset n2 n1)

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