modules Bij, Gmapl, Stock

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@125 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 108 insertions, 4 deletions

diff --git a/lib/bij.ml b/lib/bij.ml
new file mode 100644
index 0000000000..cd0acbabbb
--- /dev/null
+++ b/lib/bij.ml
@@ -0,0 +1,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
+
+
diff --git a/lib/bij.mli b/lib/bij.mli
new file mode 100644
index 0000000000..65bae1eec2
--- /dev/null
+++ b/lib/bij.mli
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+(* Bijections. *)
+
+type ('a,'b) t
+
+val empty : ('a,'b) t
+val map : ('a,'b) t -> 'a -> 'b
+val pam : ('a,'b) t -> 'b -> 'a
+val dom : ('a,'b) t -> 'a list
+val rng : ('a,'b) t -> 'b list
+val in_dom : ('a,'b) t -> 'a -> bool
+val in_rng : ('a,'b) t -> 'b -> bool
+val app : ('a -> 'b -> unit) -> ('a,'b) t -> unit
+val to_list : ('a,'b) t -> ('a * 'b) list
+
+val add : ('a,'b) t -> 'a * 'b -> ('a,'b) t
+val remove : ('a,'b) t -> 'a -> ('a,'b) t
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
new file mode 100644
index 0000000000..6295c4099c
--- /dev/null
+++ b/lib/gmapl.ml
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+open Util
+
+type ('a,'b) t = ('a,'b list) Gmap.t
+
+let empty = Gmap.empty
+let mem = Gmap.mem
+let iter = Gmap.iter
+let map = Gmap.map
+let fold = Gmap.fold
+
+let add x y m =
+  try
+    let l = Gmap.find x m in
+    Gmap.add x (if List.mem y l then l else y::l) m
+  with Not_found ->
+    Gmap.add x [y] m
+
+let find x m =
+  try Gmap.find x m with Not_found -> []
+
+let remove x y m =
+  let l = Gmap.find x m in
+  Gmap.add x (if List.mem y l then list_subtract l [y] else l) m
+
+  
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
new file mode 100644
index 0000000000..27b465f83d
--- /dev/null
+++ b/lib/gmapl.mli
@@ -0,0 +1,16 @@
+
+(* $Id$ *)
+
+(* Maps from ['a] to lists of ['b]. *)
+
+type ('a,'b) t = ('a,'b list) Gmap.t
+
+val empty : ('a,'b) t
+val mem :  'a -> ('a,'b) t -> bool
+val iter : ('a -> 'b list -> unit) -> ('a,'b) t -> unit
+val map : ('b list -> 'c list) -> ('a,'b) t -> ('a,'c) t
+val fold : ('a -> 'b list -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
+
+val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
+val find : 'a -> ('a,'b) t -> 'b list
+val remove : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/util.ml b/lib/util.ml
index 30f1cbeb65..bb50238860 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -91,10 +91,6 @@ let list_assign l n e =
   in 
   assrec [] (l,n)
 
-let rec list_distinct = function
-  | h::t -> (not (List.mem h t)) && list_distinct t
-  | [] -> true
-
 let list_map_i f = 
   let rec map_i_rec i = function
     | [] -> [] 
@@ -154,6 +150,15 @@ let rec list_distinct = function
   | h::t -> (not (List.mem h t)) && list_distinct t
   | _ -> true
 
+let list_subset l1 l2 =
+  let t2 = Hashtbl.create 151 in
+  List.iter (fun x -> Hashtbl.add t2 x ()) l2;
+  let rec look = function
+    | [] -> true
+    | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
+  in 
+  look l1
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index a40a24ba41..3975cdfc6e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -46,6 +46,7 @@ val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
 val list_distinct : 'a list -> bool
+val list_subset : 'a list -> 'a list -> bool
 
 (*s Arrays. *)