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

8 files changed, 36 insertions, 9 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 98fb467c8..41338c1cc 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -250,7 +250,7 @@ let ref_value_cache info ref =
             | None -> raise Not_found
             | Some t -> lift n t
             end
-	| VarKey id -> List.assoc_f Id.equal id info.i_vars
+	| VarKey id -> Id.List.assoc id info.i_vars
 	| ConstKey cst -> constant_value info.i_env cst
     in
     let v = info.i_repr info body in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9d2580ce4..50c052abb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -239,6 +239,14 @@ let typecheck_inductive env mie =
 
   let inds = Array.of_list inds in
   let arities = Array.of_list arity_list in
+  let has_some_univ u = function
+    | Some v when Universe.equal u v -> true
+    | _ -> false
+  in
+  let remove_some_univ u = function
+    | Some v when Universe.equal u v -> None
+    | x -> x
+  in
   let fold l (_, b, p) = match b with
   | None ->
     (* Parameter contributes to polymorphism only if explicit Type *)
@@ -247,8 +255,8 @@ let typecheck_inductive env mie =
     (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
     begin match kind_of_term c with
     | Sort (Type u) ->
-      if List.mem (Some u) l then
-        None :: List.map (function Some v when Universe.equal u v -> None | x -> x) l
+      if List.exists (has_some_univ u) l then
+        None :: List.map (remove_some_univ u) l
       else
         Some u :: l
     | _ ->
diff --git a/kernel/names.ml b/kernel/names.ml
index c505017f6..d02e0ce07 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -64,6 +64,8 @@ struct
 
   module Pred = Predicate.Make(Self)
 
+  module List = String.List
+
   let hcons = String.hcons
 
 end
diff --git a/kernel/names.mli b/kernel/names.mli
index 417e35aaa..16d0ae5d0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,6 +46,9 @@ sig
   module Pred : Predicate.S with type elt = t
   (** Predicates over identifiers. *)
 
+  module List : List.MonoS with type elt = t
+  (** Operations over lists of identifiers. *)
+
   val hcons : t -> t
   (** Hashconsing of identifiers. *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d656eceb6..fd8844e00 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -615,14 +615,14 @@ let get_rel env id i =
     List.nth env.env_rel (i-1)
   else 
     let i = i - env.env_bound in
-    try List.assoc_f Int.equal i !(env.env_urel)
+    try Int.List.assoc i !(env.env_urel)
     with Not_found ->
       let local = MLlocal (fresh_lname id) in
       env.env_urel := (i,local) :: !(env.env_urel);
       local
 
 let get_var env id =
-  try List.assoc_f Id.equal id !(env.env_named)
+  try Id.List.assoc id !(env.env_named)
   with Not_found ->
     let local = MLlocal (fresh_lname (Name id)) in
     env.env_named := (id, local)::!(env.env_named);
@@ -1501,18 +1501,20 @@ let compile_constant env prefix ~interactive con body =
 
 let loaded_native_files = ref ([] : string list)
 
+let is_loaded_native_file s = String.List.mem s !loaded_native_files
+
 let register_native_file s =
-  if not (List.mem s !loaded_native_files) then
+  if not (is_loaded_native_file s) then
     loaded_native_files := s :: !loaded_native_files
 
 let is_code_loaded ~interactive name =
   match !name with
   | NotLinked -> false
   | LinkedInteractive (s,_) ->
-      if (interactive && List.mem s !loaded_native_files) then true
+      if (interactive && is_loaded_native_file s) then true
       else (name := NotLinked; false)
   | Linked (s,_) ->
-      if List.mem s !loaded_native_files then true
+      if is_loaded_native_file s then true
       else (name := NotLinked; false)
 
 let param_name = Name (id_of_string "params")
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 04deade92..03f1cd265 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -59,6 +59,11 @@ let hash = function
   let h = Universe.hash u in
   combinesmall 2 h
 
+module List = struct
+  let mem = List.memq
+  let intersect l l' = CList.intersect family_equal l l'
+end
+
 module Hsorts =
   Hashcons.Make(
     struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index b64e92fba..2750145f1 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -30,3 +30,8 @@ val family : t -> family
 val hcons : t -> t
 
 val family_equal : family -> family -> bool
+
+module List : sig
+  val mem : family -> family list -> bool
+  val intersect : family list -> family list -> family list
+end
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9b5c42f56..7f5c71c70 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -950,10 +950,12 @@ let no_upper_constraints u cst =
 
 (* Is u mentionned in v (or equals to v) ? *)
 
+let level_list_mem u l = List.mem_f UniverseLevel.equal u l
+
 let univ_depends u v =
   match u, v with
     | Atom u, Atom v -> UniverseLevel.equal u v
-    | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
+    | Atom u, Max (gel,gtl) -> level_list_mem u gel || level_list_mem u gtl
     | _ -> anomaly (Pp.str "univ_depends given a non-atomic 1st arg")
 
 (* Pretty-printing *)