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

1 files changed, 11 insertions, 0 deletions

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 ()