1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Maps using the generic comparison function of ocaml. Code borrowed from
the ocaml standard library (Copyright 1996, INRIA). *)
type ('a,'b) t =
Empty
| Node of ('a,'b) t * 'a * 'b * ('a,'b) t * int
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let height = function
Empty -> 0
| Node(_,_,_,_,h) -> h
let create l x d r =
let hl = height l and hr = height r in
Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
let bal l x d r =
let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
if hl > hr + 2 then begin
match l with
Empty -> invalid_arg "Map.bal"
| Node(ll, lv, ld, lr, _) ->
if height ll >= height lr then
create ll lv ld (create lr x d r)
else begin
match lr with
Empty -> invalid_arg "Map.bal"
| Node(lrl, lrv, lrd, lrr, _)->
create (create ll lv ld lrl) lrv lrd (create lrr x d r)
end
end else if hr > hl + 2 then begin
match r with
Empty -> invalid_arg "Map.bal"
| Node(rl, rv, rd, rr, _) ->
if height rr >= height rl then
create (create l x d rl) rv rd rr
else begin
match rl with
Empty -> invalid_arg "Map.bal"
| Node(rll, rlv, rld, rlr, _) ->
create (create l x d rll) rlv rld (create rlr rv rd rr)
end
end else
Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
let rec add x data = function
Empty ->
Node(Empty, x, data, Empty, 1)
| Node(l, v, d, r, h) ->
let c = Pervasives.compare x v in
if c = 0 then
Node(l, x, data, r, h)
else if c < 0 then
bal (add x data l) v d r
else
bal l v d (add x data r)
let rec find x = function
Empty ->
raise Not_found
| Node(l, v, d, r, _) ->
let c = Pervasives.compare x v in
if c = 0 then d
else find x (if c < 0 then l else r)
let rec mem x = function
Empty ->
false
| Node(l, v, d, r, _) ->
let c = Pervasives.compare x v in
c = 0 || mem x (if c < 0 then l else r)
let rec min_binding = function
Empty -> raise Not_found
| Node(Empty, x, d, r, _) -> (x, d)
| Node(l, x, d, r, _) -> min_binding l
let rec remove_min_binding = function
Empty -> invalid_arg "Map.remove_min_elt"
| Node(Empty, x, d, r, _) -> r
| Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
let merge t1 t2 =
match (t1, t2) with
(Empty, t) -> t
| (t, Empty) -> t
| (_, _) ->
let (x, d) = min_binding t2 in
bal t1 x d (remove_min_binding t2)
let rec remove x = function
Empty ->
Empty
| Node(l, v, d, r, h) ->
let c = Pervasives.compare x v in
if c = 0 then
merge l r
else if c < 0 then
bal (remove x l) v d r
else
bal l v d (remove x r)
let rec iter f = function
Empty -> ()
| Node(l, v, d, r, _) ->
iter f l; f v d; iter f r
let rec map f = function
Empty -> Empty
| Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
(* Maintien de fold_right par compatibilit (chang en fold_left dans
ocaml-3.09.0) *)
let rec fold f m accu =
match m with
Empty -> accu
| Node(l, v, d, r, _) ->
fold f l (f v d (fold f r accu))
(* Added with respect to ocaml standard library. *)
let dom m = fold (fun x _ acc -> x::acc) m []
let rng m = fold (fun _ y acc -> y::acc) m []
let to_list m = fold (fun x y acc -> (x,y)::acc) m []
|