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 ->
  50       (Interv (newi, j))::(if newi =|= z then xs else (Exact z)::xs)
  51   | (Interv (i', j'))::xs ->
  52       if newi =|= j'
  53       then (Interv (i', j))::xs  (* merge *)
  54       else (Interv (newi, j))::(Interv (i', j'))::xs
  55
  56
  57 (* the only possible merges are when x = i-1, otherwise, the job is done before *)
  58 let rec (add2: int -> seti -> seti) = fun x -> function
  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
  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
  64
  65   | (Exact i)::xs when i =|= x   -> (Exact i)::xs
  66   | (Interv (i,j)::xs) when x <= j && x >= i -> (Interv (i,j))::xs
  67   | other ->
  68 (*         let _ = log "Cache miss" in *)
  69       let _ = count2 () in
  70       (match other with
  71       |       (Exact i)::xs when x =|= i-1 -> pack x i xs
  72       |       (Exact i)::xs when x < i-1 -> (Exact i)::add x xs
  73
  74       |       (Interv (i,j)::xs) when x =|= i-1 -> pack x j xs
  75       |       (Interv (i,j)::xs) when x < i-1 -> (Interv (i,j))::add x xs
  76       |       _ -> raise Impossible
  77       )
  78 and add x y = let _ = count5 () in add2 x y
  79
  80
  81 let rec tolist2 = function
  82   | [] -> []
  83   | (Exact i)::xs -> i::tolist2 xs
  84   | (Interv (i,j))::xs -> enum i j @ tolist2 xs
  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
  93   | Interv (i,j) when i =|= j -> Exact i
  94   | y -> y
  95 let exactize2 x y = if x =|= y then Exact x else Interv (x,y)
  96
  97
  98 let rec (remove: int -> seti -> seti) = fun x xs ->
  99   match xs with
 100   | [] -> [] (*  pb, not in  *)
 101   | (Exact z)::zs ->
 102       (match x <=> z with
 103       | Equal -> zs
 104       | Sup -> xs  (*  pb, not in *)
 105       | Inf -> (Exact z)::remove x zs
 106       )
 107   | (Interv (i,j)::zs) ->
 108       if x > j then xs (*  pb not in *)
 109       else
 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
 114             | _ when x =|= i -> [exactize2 (i+1) j]
 115             | _ when x =|= j -> [exactize2 i (j-1)]
 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
 129
 130 let rec mem e = function
 131   | [] -> false
 132   | (Exact x)::xs ->
 133       (match e <=> x with
 134       | Equal -> true
 135       | Sup -> false
 136       | Inf -> mem e xs
 137       )
 138   | (Interv (i,j)::xs) ->
 139       if e > j then false
 140       else
 141         if e >= i && e <= j then true
 142       else mem e xs
 143
 144 let iter f xs = xs +> List.iter
 145   (function
 146   | Exact i -> f i
 147   | Interv (i, j) -> for k = i to j do f k done
 148   )
 149
 150 let is_empty xs = xs =*= []
 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
 155
 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
 161
 162 (*****************************************************************************)
 163 (*  TODO: could return corresponding osetb ? *)
 164 let rec inter xs ys =
 165   let rec aux = fun xs ys ->
 166     match (xs, ys) with
 167     | (_, []) -> []
 168     | ([],_)  -> []
 169     | (x::xs, y::ys) ->
 170         (match (x, y) with
 171         | (Interv (i1, j1), Interv (i2, j2)) ->
 172             (match i1 <=> i2 with
 173             | Equal ->
 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                 )
 185             | Inf ->
 186                 if j1 < i2 then aux xs (y::ys) (* need order ? *)
 187                   (*  [    ] *)
 188                   (*         [ ] *)
 189                 else
 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))
 208
 209 let union xs ys =
 210   let rec aux = fun xs ys ->
 211     match (xs, ys) with
 212     | (vs, []) -> vs
 213     | ([],vs)  -> vs
 214     | (x::xs, y::ys) ->
 215         (match (x, y) with
 216         | (Interv (i1, j1), Interv (i2, j2)) ->
 217             (match i1 <=> i2 with
 218             | Equal ->
 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                 )
 230             | Inf ->
 231                 if j1 < i2 then Interv (i1, j1):: aux xs (y::ys)
 232                   (*  [    ] *)
 233                   (*         [ ] *)
 234                 else
 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
 258 let diff xs ys =
 259   let rec aux = fun xs ys ->
 260     match (xs, ys) with
 261     | (vs, []) -> vs
 262     | ([],vs)  -> []
 263     | (x::xs, y::ys) ->
 264         (match (x, y) with
 265         | (Interv (i1, j1), Interv (i2, j2)) ->
 266             (match i1 <=> i2 with
 267             | Equal ->
 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                 )
 279             | Inf ->
 280                 if j1 < i2 then Interv (i1, j1):: aux xs (y::ys)
 281                   (*  [    ] *)
 282                   (*         [ ] *)
 283                 else
 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                   )
 295             | Sup ->
 296                 if j2 < i1 then aux (x::xs) ys
 297                   (*       [    ] *)
 298                   (*  [ ] *)
 299                 else
 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]) *)
 320
 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
 330 let patch2 xs = xs +> List.map (fun e ->
 331   match e with
 332   | Interv (i,j) when i > j && i =|= j+1 ->
 333       let _ = pr2 (sprintf "i = %d, j = %d" i j) in
 334       Exact i
 335   | e -> e
 336 )
 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
 343           then (min, acc)
 344           else (i, (Exact i)::acc)
 345       | Interv (i,j) ->
 346           (j, (Interv (i,j)::acc))
 347     ) (min, [])
 348   in
 349   aux min_int (List.rev xs) +> snd
 350
 351