Commit | Line | Data |
---|---|---|
34e49164 C |
1 | open Common |
2 | ||
3 | (*****************************************************************************) | |
4 | (* coded for LFS *) | |
5 | ||
6 | (* todo: could take an incr/decr func in param, to make it generic | |
7 | * opti: remember the min/max (optimisation to have intersect biggest x -> x) | |
8 | * opti: avoid all those rev, and avoid the intervise | |
9 | * (but yes the algo are then more complex :) | |
10 | * opti: balanced set intervalle | |
11 | *) | |
12 | ||
13 | (*****************************************************************************) | |
14 | type seti = elt list (* last elements is in first pos, ordered reverse *) | |
15 | and elt = Exact of int | Interv of int * int | |
16 | ||
17 | (* invariant= ordered list, no incoherent interv (one elem or zero elem), | |
18 | * merged (intervalle are separated) *) | |
19 | let invariant xs = | |
20 | let rec aux min xs = | |
21 | xs +> List.fold_left (fun min e -> | |
22 | match e with | |
23 | | Exact i -> | |
24 | if i <= min then pr2 (sprintf "i = %d, min = %d" i min); | |
25 | (* todo: should be even stronger, shoud be i > min+1 *) | |
26 | assert (i > min); | |
27 | i | |
28 | | Interv (i,j) -> | |
29 | assert (i > min); | |
30 | assert (j > i); | |
31 | j | |
32 | ) min | |
33 | in | |
34 | ignore(aux min_int (List.rev xs)); | |
35 | () | |
36 | ||
37 | let string_of_seti xs = | |
38 | "[" ^ | |
39 | join "," (xs +> List.rev +> map (function | |
40 | | (Exact i) -> string_of_int i | |
41 | | (Interv (i,j)) -> Printf.sprintf "%d - %d" i j)) ^ | |
42 | "]" | |
43 | ||
44 | (*****************************************************************************) | |
45 | let empty = [] | |
46 | ||
47 | let pack newi j = function | |
48 | | [] -> [Interv (newi,j)] | |
49 | | (Exact z)::xs -> (Interv (newi, j))::(if newi = z then xs else (Exact z)::xs) | |
50 | | (Interv (i', j'))::xs -> | |
51 | if newi = j' | |
52 | then (Interv (i', j))::xs (* merge *) | |
53 | else (Interv (newi, j))::(Interv (i', j'))::xs | |
54 | ||
55 | ||
56 | (* the only possible merges are when x = i-1, otherwise, the job is done before *) | |
57 | let rec (add2: int -> seti -> seti) = fun x -> function | |
58 | | [] -> [Exact x] | |
59 | | (Exact i)::xs when x > i+1 -> (Exact x)::(Exact i)::xs | |
60 | | (Interv (i,j)::xs) when x > j+1 -> (Exact x)::(Interv (i,j))::xs | |
61 | | (Interv (i,j)::xs) when x = j+1 -> (Interv (i,x))::xs | |
62 | | (Exact i)::xs when x = i+1 -> (Interv (i,x))::xs | |
63 | ||
64 | | (Exact i)::xs when i = x -> (Exact i)::xs | |
65 | | (Interv (i,j)::xs) when x <= j && x >= i -> (Interv (i,j))::xs | |
66 | | other -> | |
67 | (* let _ = log "Cache miss" in *) | |
68 | let _ = count2 () in | |
69 | (match other with | |
70 | | (Exact i)::xs when x = i-1 -> pack x i xs | |
71 | | (Exact i)::xs when x < i-1 -> (Exact i)::add x xs | |
72 | ||
73 | | (Interv (i,j)::xs) when x = i-1 -> pack x j xs | |
74 | | (Interv (i,j)::xs) when x < i-1 -> (Interv (i,j))::add x xs | |
75 | | _ -> raise Impossible | |
76 | ) | |
77 | and add x y = let _ = count5 () in add2 x y | |
78 | ||
79 | ||
80 | let rec tolist2 = function | |
81 | | [] -> [] | |
82 | | (Exact i)::xs -> i::tolist2 xs | |
83 | | (Interv (i,j))::xs -> enum i j @ tolist2 xs | |
84 | let rec tolist xs = List.rev (tolist2 xs) | |
85 | ||
86 | let rec fromlist = function xs -> List.fold_left (fun a e -> add e a) empty xs | |
87 | ||
88 | let intervise = function | |
89 | | Exact x -> Interv (x,x) | |
90 | | y -> y | |
91 | let exactize = function | |
92 | | Interv (i,j) when i = j -> Exact i | |
93 | | y -> y | |
94 | let exactize2 x y = if x = y then Exact x else Interv (x,y) | |
95 | ||
96 | ||
97 | let rec (remove: int -> seti -> seti) = fun x xs -> | |
98 | match xs with | |
99 | | [] -> [] (* pb, not in *) | |
100 | | (Exact z)::zs -> | |
101 | (match x <=> z with | |
102 | | Equal -> zs | |
103 | | Sup -> xs (* pb, not in *) | |
104 | | Inf -> (Exact z)::remove x zs | |
105 | ) | |
106 | | (Interv (i,j)::zs) -> | |
107 | if x > j then xs (* pb not in *) | |
108 | else | |
109 | if x >= i && x <= j then | |
110 | ( | |
111 | let _ = assert (j > i) in (* otherwise can lead to construct seti such as [7,6] when removing 6 from [6,6] *) | |
112 | match () with | |
113 | | _ when x = i -> [exactize2 (i+1) j] | |
114 | | _ when x = j -> [exactize2 i (j-1)] | |
115 | | _ -> [exactize2 (x+1) j; exactize2 i (x-1)] | |
116 | ) @ zs | |
117 | else (Interv (i,j))::remove x zs | |
118 | ||
119 | (* let _ = Example (remove 635 [Interv (3, 635)] = [Interv (3, 634)]) *) | |
120 | (* let _ = Example (remove 2 [Interv (6, 7); Interv(1,4)] = [Interv (6,7); Interv (3,4); Exact 1]) *) | |
121 | (* let _ = Example (remove 6 [Interv (6, 7); Interv(1,4)] = [Exact 7; Interv (1,4)]) *) | |
122 | (* let _ = Example (remove 1 [Interv (6, 7); Interv(1,2)] = [Interv (6,7); Exact 2]) *) | |
123 | (* let _ = Example (remove 3 [Interv (1, 7)] = [Interv (4,7); Interv (1,2)]) *) | |
124 | let _ = assert_equal (remove 3 [Interv (1, 7)]) [Interv (4,7); Interv (1,2)] | |
125 | let _ = assert_equal (remove 4 [Interv (3, 4)]) [Exact (3);] | |
126 | (* let _ = example (try (ignore(remove 6 [Interv (6, 6)] = []); false) with _ -> true) *) | |
127 | ||
128 | ||
129 | let rec mem e = function | |
130 | | [] -> false | |
131 | | (Exact x)::xs -> | |
132 | (match e <=> x with | |
133 | | Equal -> true | |
134 | | Sup -> false | |
135 | | Inf -> mem e xs | |
136 | ) | |
137 | | (Interv (i,j)::xs) -> | |
138 | if e > j then false | |
139 | else | |
140 | if e >= i && e <= j then true | |
141 | else mem e xs | |
142 | ||
143 | let iter f xs = xs +> List.iter | |
144 | (function | |
145 | | Exact i -> f i | |
146 | | Interv (i, j) -> for k = i to j do f k done | |
147 | ) | |
148 | ||
149 | let is_empty xs = xs = [] | |
150 | let choose = function | |
151 | | [] -> failwith "not supposed to be called with empty set" | |
152 | | (Exact i)::xs -> i | |
153 | | (Interv (i,j))::xs -> i | |
154 | ||
155 | let elements xs = tolist xs | |
156 | let rec cardinal = function | |
157 | | [] -> 0 | |
158 | | (Exact _)::xs -> 1+cardinal xs | |
159 | | (Interv (i,j)::xs) -> (j-i) +1 + cardinal xs | |
160 | ||
161 | (*****************************************************************************) | |
162 | (* TODO: could return corresponding osetb ? *) | |
163 | let rec inter xs ys = | |
164 | let rec aux = fun xs ys -> | |
165 | match (xs, ys) with | |
166 | | (_, []) -> [] | |
167 | | ([],_) -> [] | |
168 | | (x::xs, y::ys) -> | |
169 | (match (x, y) with | |
170 | | (Interv (i1, j1), Interv (i2, j2)) -> | |
171 | (match i1 <=> i2 with | |
172 | | Equal -> | |
173 | (match j1 <=> j2 with | |
174 | | Equal -> (Interv (i1,j1))::aux xs ys | |
175 | (* [ ] *) | |
176 | (* [ ] *) | |
177 | | Inf -> (Interv (i1, j1))::aux xs ((Interv (j1+1, j2))::ys) | |
178 | (* [ ] [ TODO? could have [ so cant englobe right now, but would be better *) | |
179 | (* [ ] *) | |
180 | | Sup -> (Interv (i1, j2))::aux ((Interv (j2+1, j1))::xs) ys | |
181 | (* [ ] *) | |
182 | (* [ ] [ same *) | |
183 | ) | |
184 | | Inf -> | |
185 | if j1 < i2 then aux xs (y::ys) (* need order ? *) | |
186 | (* [ ] *) | |
187 | (* [ ] *) | |
188 | else | |
189 | (match j1 <=> j2 with | |
190 | | Equal -> (Interv (i2, j1))::aux xs ys | |
191 | (* [ ] *) | |
192 | (* [ ] *) | |
193 | | Inf -> (Interv (i2, j1))::aux xs ((Interv (j1+1, j2))::ys) | |
194 | (* [ ] [ same *) | |
195 | (* [ ] *) | |
196 | | Sup -> (Interv (i2, j2))::aux ((Interv (j2+1, j1))::xs) ys | |
197 | (* [ ] *) | |
198 | (* [ ] [ same *) | |
199 | ) | |
200 | | Sup -> aux (y::ys) (x::xs) (* can cos commutative *) | |
201 | ) | |
202 | | _ -> raise Impossible (* intervise *) | |
203 | ) | |
204 | in | |
205 | (* TODO avoid the rev rev, but aux good ? need order ? *) | |
206 | List.rev_map exactize (aux (List.rev_map intervise xs) (List.rev_map intervise ys)) | |
207 | ||
208 | let union xs ys = | |
209 | let rec aux = fun xs ys -> | |
210 | match (xs, ys) with | |
211 | | (vs, []) -> vs | |
212 | | ([],vs) -> vs | |
213 | | (x::xs, y::ys) -> | |
214 | (match (x, y) with | |
215 | | (Interv (i1, j1), Interv (i2, j2)) -> | |
216 | (match i1 <=> i2 with | |
217 | | Equal -> | |
218 | (match j1 <=> j2 with | |
219 | | Equal -> (Interv (i1,j1))::aux xs ys | |
220 | (* [ ] *) | |
221 | (* [ ] *) | |
222 | | Inf -> (Interv (i1, j1))::aux xs ((Interv (j1+1, j2))::ys) | |
223 | (* [ ] [ TODO? could have [ so cant englobe right now, but would be better *) | |
224 | (* [ ] *) | |
225 | | Sup -> (Interv (i1, j2))::aux ((Interv (j2+1, j1))::xs) ys | |
226 | (* [ ] *) | |
227 | (* [ ] [ same *) | |
228 | ) | |
229 | | Inf -> | |
230 | if j1 < i2 then Interv (i1, j1):: aux xs (y::ys) | |
231 | (* [ ] *) | |
232 | (* [ ] *) | |
233 | else | |
234 | (match j1 <=> j2 with | |
235 | | Equal -> (Interv (i1, j1))::aux xs ys | |
236 | (* [ ] *) | |
237 | (* [ ] *) | |
238 | | Inf -> (Interv (i1, j1))::aux xs ((Interv (j1+1, j2))::ys) | |
239 | (* [ ] [ same *) | |
240 | (* [ ] *) | |
241 | | Sup -> (Interv (i1, j2))::aux ((Interv (j2+1, j1))::xs) ys | |
242 | (* [ ] *) | |
243 | (* [ ] [ same *) | |
244 | ) | |
245 | | Sup -> aux (y::ys) (x::xs) (* can cos commutative *) | |
246 | ) | |
247 | | _ -> raise Impossible (* intervise *) | |
248 | ) | |
249 | in | |
250 | (* union_set (tolist xs) (tolist ys) +> fromlist *) | |
251 | List.rev_map exactize (aux (List.rev_map intervise xs) (List.rev_map intervise ys)) | |
252 | ||
253 | (* bug/feature: discovered by vlad rusu, my invariant for intervalle is | |
254 | * not very strong, should return (Interv (1,4)) *) | |
255 | (* let _ = Example (union [Interv (1, 4)] [Interv (1, 3)] = ([Exact 4; Interv (1,3)])) *) | |
256 | ||
257 | let diff xs ys = | |
258 | let rec aux = fun xs ys -> | |
259 | match (xs, ys) with | |
260 | | (vs, []) -> vs | |
261 | | ([],vs) -> [] | |
262 | | (x::xs, y::ys) -> | |
263 | (match (x, y) with | |
264 | | (Interv (i1, j1), Interv (i2, j2)) -> | |
265 | (match i1 <=> i2 with | |
266 | | Equal -> | |
267 | (match j1 <=> j2 with | |
268 | | Equal -> aux xs ys | |
269 | (* [ ] *) | |
270 | (* [ ] *) | |
271 | | Inf -> aux xs ((Interv (j1+1, j2))::ys) | |
272 | (* [ ] *) | |
273 | (* [ ] *) | |
274 | | Sup -> aux ((Interv (j2+1, j1))::xs) ys | |
275 | (* [ ] *) | |
276 | (* [ ] *) | |
277 | ) | |
278 | | Inf -> | |
279 | if j1 < i2 then Interv (i1, j1):: aux xs (y::ys) | |
280 | (* [ ] *) | |
281 | (* [ ] *) | |
282 | else | |
283 | (match j1 <=> j2 with | |
284 | | Equal -> (Interv (i1, i2-1))::aux xs ys (* -1 cos exlude [ *) | |
285 | (* [ ] *) | |
286 | (* [ ] *) | |
287 | | Inf -> (Interv (i1, i2-1))::aux xs ((Interv (j1+1, j2))::ys) | |
288 | (* [ ] *) | |
289 | (* [ ] *) | |
290 | | Sup -> (Interv (i1, i2-1))::aux ((Interv (j2+1, j1))::xs) ys | |
291 | (* [ ] *) | |
292 | (* [ ] *) | |
293 | ) | |
294 | | Sup -> | |
295 | if j2 < i1 then aux (x::xs) ys | |
296 | (* [ ] *) | |
297 | (* [ ] *) | |
298 | else | |
299 | (match j1 <=> j2 with | |
300 | | Equal -> aux xs ys | |
301 | (* [ ] *) | |
302 | (* [ ] *) | |
303 | | Inf -> aux xs ((Interv (j1+1, j2))::ys) | |
304 | (* [ ] *) | |
305 | (* [ ] *) | |
306 | | Sup -> aux ((Interv (j2+1, j1))::xs) ys | |
307 | (* [ ] *) | |
308 | (* [ ] *) | |
309 | ) | |
310 | ) | |
311 | | _ -> raise Impossible (* intervise *) | |
312 | ) | |
313 | in | |
314 | (* minus_set (tolist xs) (tolist ys) +> fromlist *) | |
315 | List.rev_map exactize (aux (List.rev_map intervise xs) (List.rev_map intervise ys)) | |
316 | ||
317 | ||
318 | (* let _ = Example (diff [Interv (3,7)] [Interv (4,5)] = [Interv (6, 7); Exact 3]) *) | |
319 | ||
320 | (*****************************************************************************) | |
321 | let rec debug = function | |
322 | | [] -> "" | |
323 | | (Exact i)::xs -> (Printf.sprintf "Exact:%d;" i) ^ (debug xs) | |
324 | | (Interv (i,j)::xs) -> (Printf.sprintf "Interv:(%d,%d);" i j) ^ debug xs | |
325 | ||
326 | (*****************************************************************************) | |
327 | (* if operation return wrong result, then may later have to patch them *) | |
328 | let patch1 xs = List.map exactize xs | |
329 | let patch2 xs = xs +> List.map (fun e -> | |
330 | match e with | |
331 | | Interv (i,j) when i > j && i = j+1 -> | |
332 | let _ = pr2 (sprintf "i = %d, j = %d" i j) in | |
333 | Exact i | |
334 | | e -> e | |
335 | ) | |
336 | let patch3 xs = | |
337 | let rec aux min xs = | |
338 | xs +> List.fold_left (fun (min,acc) e -> | |
339 | match e with | |
340 | | Exact i -> | |
341 | if i = min | |
342 | then (min, acc) | |
343 | else (i, (Exact i)::acc) | |
344 | | Interv (i,j) -> | |
345 | (j, (Interv (i,j)::acc)) | |
346 | ) (min, []) | |
347 | in | |
348 | aux min_int (List.rev xs) +> snd | |
349 | ||
350 |