extracted/untrusted/pmap.ml

   1 (* Copied from OCaml's Map to make it polymorphic *)
   2
   3     type ('k,'a) map =
   4         Empty
   5       | Node of ('k,'a) map * 'k * 'a * ('k,'a) map * int
   6
   7     let empty = Empty
   8
   9     let height = function
  10         Empty -> 0
  11       | Node(_,_,_,_,h) -> h
  12
  13     let rec find x = function
  14         Empty ->
  15           raise Not_found
  16       | Node(l, v, d, r, _) ->
  17           let c = compare x v in
  18           if c = 0 then d
  19           else find x (if c < 0 then l else r)
  20
  21     let create l x d r =
  22       let hl = height l and hr = height r in
  23       Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
  24
  25     let bal l x d r =
  26       let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
  27       let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
  28       if hl > hr + 2 then begin
  29         match l with
  30           Empty -> invalid_arg "Map.bal"
  31         | Node(ll, lv, ld, lr, _) ->
  32             if height ll >= height lr then
  33               create ll lv ld (create lr x d r)
  34             else begin
  35               match lr with
  36                 Empty -> invalid_arg "Map.bal"
  37               | Node(lrl, lrv, lrd, lrr, _)->
  38                   create (create ll lv ld lrl) lrv lrd (create lrr x d r)
  39             end
  40       end else if hr > hl + 2 then begin
  41         match r with
  42           Empty -> invalid_arg "Map.bal"
  43         | Node(rl, rv, rd, rr, _) ->
  44             if height rr >= height rl then
  45               create (create l x d rl) rv rd rr
  46             else begin
  47               match rl with
  48                 Empty -> invalid_arg "Map.bal"
  49               | Node(rll, rlv, rld, rlr, _) ->
  50                   create (create l x d rll) rlv rld (create rlr rv rd rr)
  51             end
  52       end else
  53         Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
  54
  55     let rec add x data = function
  56         Empty ->
  57           Node(Empty, x, data, Empty, 1)
  58       | Node(l, v, d, r, h) ->
  59           let c = compare x v in
  60           if c = 0 then
  61             Node(l, x, data, r, h)
  62           else if c < 0 then
  63             bal (add x data l) v d r
  64           else
  65             bal l v d (add x data r)
  66
  67     let rec min_binding = function
  68         Empty -> raise Not_found
  69       | Node(Empty, x, d, r, _) -> (x, d)
  70       | Node(l, x, d, r, _) -> min_binding l
  71
  72     let rec remove_min_binding = function
  73         Empty -> invalid_arg "Map.remove_min_elt"
  74       | Node(Empty, x, d, r, _) -> r
  75       | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
  76
  77     let merge t1 t2 =
  78       match (t1, t2) with
  79         (Empty, t) -> t
  80       | (t, Empty) -> t
  81       | (_, _) ->
  82           let (x, d) = min_binding t2 in
  83           bal t1 x d (remove_min_binding t2)
  84
  85     let rec remove x = function
  86         Empty ->
  87           Empty
  88       | Node(l, v, d, r, h) ->
  89           let c = compare x v in
  90           if c = 0 then
  91             merge l r
  92           else if c < 0 then
  93             bal (remove x l) v d r
  94           else
  95             bal l v d (remove x r)
  96
  97     let rec fold f m accu =
  98       match m with
  99         Empty -> accu
 100       | Node(l, v, d, r, _) ->
 101           fold f r (f v d (fold f l accu))
 102
 103 (* Copied from atom.ml *)
 104
 105 let restrict p m =
 106     fold (fun x d m ->
 107       if p x then
 108         add x d m
 109       else
 110         m
 111     ) m empty