diff options
Diffstat (limited to 'lib/gmap.ml')
| -rw-r--r-- | lib/gmap.ml | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/lib/gmap.ml b/lib/gmap.ml new file mode 100644 index 00000000..e5d41034 --- /dev/null +++ b/lib/gmap.ml @@ -0,0 +1,125 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id: gmap.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *) + +(* Maps using the generic comparison function of ocaml. Code borrowed from + the ocaml standard library. *) + + type ('a,'b) t = + Empty + | Node of ('a,'b) t * 'a * 'b * ('a,'b) t * int + + let empty = Empty + + 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) as t -> + 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 merge t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) -> + bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2) + + let rec remove x = function + Empty -> + Empty + | Node(l, v, d, r, h) as t -> + 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) + + 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 [] + |