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