blob: cd0acbabbbf20aa1f2de4b24b6b3d6b2cabdb39c (
plain)
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
|
(* $Id$ *)
type ('a,'b) t = {
f : ('a,'b) Gmap.t;
finv : ('b,'a) Gmap.t }
let empty = { f = Gmap.empty; finv = Gmap.empty }
let map b x = Gmap.find x b.f
let pam b y = Gmap.find y b.finv
let dom b = Gmap.dom b.f
let rng b = Gmap.dom b.finv
let in_dom b x = Gmap.mem x b.f
let in_rng b y = Gmap.mem y b.finv
let add b (x,y) =
if in_dom b x || in_rng b y then failwith "Bij.add";
{ f = Gmap.add x y b.f;
finv = Gmap.add y x b.finv }
let remove b x =
let y = try map b x with Not_found -> failwith "Bij.remove" in
{ f = Gmap.remove x b.f; finv = Gmap.remove y b.finv }
let app f b = Gmap.iter f b.f
let to_list b = Gmap.to_list b.f
|