aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/bij.ml
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