More monomorphic List.mem + List.assoc + ...

 To reduce the amount of syntactic noise, we now provide
 a few inner modules Int.List, Id.List, String.List, Sorts.List
 which contain some monomorphic (or semi-monomorphic) functions
 such as mem, assoc, ...

 NB: for Int.List.mem and co we reuse List.memq and so on.

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

6 files changed, 58 insertions, 0 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 140728242c..02e46092c3 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -140,6 +140,16 @@ sig
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
   val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 
+  module type MonoS = sig
+    type elt
+    val equal : elt list -> elt list -> bool
+    val mem : elt -> elt list -> bool
+    val assoc : elt -> (elt * 'a) list -> 'a
+    val mem_assoc : elt -> (elt * 'a) list -> bool
+    val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
+    val mem_assoc_sym : elt -> ('a * elt) list -> bool
+  end
+
 end
 
 include List
@@ -788,3 +798,13 @@ let rec factorize_left cmp = function
       let al,l' = partition (fun (a',_) -> cmp a a') l in
       (a,(b::List.map snd al)) :: factorize_left cmp l'
   | [] -> []
+
+module type MonoS = sig
+  type elt
+  val equal : elt list -> elt list -> bool
+  val mem : elt -> elt list -> bool
+  val assoc : elt -> (elt * 'a) list -> 'a
+  val mem_assoc : elt -> (elt * 'a) list -> bool
+  val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
+  val mem_assoc_sym : elt -> ('a * elt) list -> bool
+end
diff --git a/lib/cList.mli b/lib/cList.mli
index 6b9f2a8c2d..6af32fdd0f 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -241,6 +241,16 @@ sig
   (** Keep only those products that do not return None *)
 
   val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
+
+  module type MonoS = sig
+    type elt
+    val equal : elt list -> elt list -> bool
+    val mem : elt -> elt list -> bool
+    val assoc : elt -> (elt * 'a) list -> 'a
+    val mem_assoc : elt -> (elt * 'a) list -> bool
+    val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
+    val mem_assoc_sym : elt -> ('a * elt) list -> bool
+  end
 end
 
 include ExtS
diff --git a/lib/cString.ml b/lib/cString.ml
index 551b628342..842625aa4e 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -61,6 +61,7 @@ sig
   val is_sub : string -> string -> int -> bool
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
+  module List : CList.MonoS with type elt = t
   val hcons : string -> string
 end
 
@@ -191,4 +192,14 @@ end
 module Set = Set.Make(Self)
 module Map = CMap.Make(Self)
 
+module List = struct
+  type elt = string
+  let mem id l = List.exists (equal id) l
+  let assoc id l = CList.assoc_f equal id l
+  let remove_assoc id l = CList.remove_assoc_f equal id l
+  let mem_assoc id l = List.exists (fun (a,_) -> equal id a) l
+  let mem_assoc_sym id l = List.exists (fun (_,b) -> equal id b) l
+  let equal l l' = CList.equal equal l l'
+end
+
 let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate ()
diff --git a/lib/cString.mli b/lib/cString.mli
index d8a19c8e4c..5f36162312 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -99,6 +99,9 @@ sig
   module Map : CMap.ExtS with type key = t and module Set := Set
   (** Finite maps on [string] *)
 
+  module List : CList.MonoS with type elt = t
+  (** Association lists with [string] as keys *)
+
   val hcons : string -> string
   (** Hashconsing on [string] *)
 
diff --git a/lib/int.ml b/lib/int.ml
index 6eb4260657..b5519a5715 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -22,3 +22,10 @@ end
 
 module Set = Set.Make(Self)
 module Map = CMap.Make(Self)
+
+module List = struct
+  let mem = List.memq
+  let assoc = List.assq
+  let mem_assoc = List.mem_assq
+  let remove_assoc = List.remove_assq
+end
diff --git a/lib/int.mli b/lib/int.mli
index 956432a526..a84798950d 100644
--- a/lib/int.mli
+++ b/lib/int.mli
@@ -18,3 +18,10 @@ val hash : t -> int
 
 module Set : Set.S with type elt = t
 module Map : CMap.ExtS with type key = t and module Set := Set
+
+module List : sig
+  val mem : int -> int list -> bool
+  val assoc : int -> (int * 'a) list -> 'a
+  val mem_assoc : int -> (int * 'a) list -> bool
+  val remove_assoc : int -> (int * 'a) list -> (int * 'a) list
+end