commons/seti.ml

   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