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

5 files changed, 47 insertions, 56 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2c44d6da3..8337e96f0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -364,7 +364,7 @@ let reset_hidden_inductive_implicit_test env =
 
 let check_hidden_implicit_parameters id impls =
   if Id.Map.exists (fun _ -> function
-    | (Inductive indparams,_,_,_) -> List.mem id indparams
+    | (Inductive indparams,_,_,_) -> Id.List.mem id indparams
     | _ -> false) impls
   then
     errorlabstrm "" (strbrk "A parameter of an inductive type " ++
@@ -456,7 +456,8 @@ let intern_generalization intern env lvar loc bk ak c =
           | None -> false
           | Some sc -> String.equal sc Notation.type_scope
           in
-          is_type_scope || List.mem Notation.type_scope env.scopes
+          is_type_scope ||
+          String.List.mem Notation.type_scope env.scopes
       in
 	if pi then
 	  (fun (id, loc') acc ->
@@ -812,10 +813,10 @@ let product_of_cases_patterns ids idspl =
 
 (* @return the first variable that occurs twice in a pattern
 
-naive n2 algo *)
+naive n^2 algo *)
 let rec has_duplicate = function
   | [] -> None
-  | x::l -> if List.mem x l then (Some x) else has_duplicate l
+  | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs =
  Loc.merge (fst (List.hd lhs)) (fst (List.last lhs))
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 734b330e7..4d4fe9117 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -83,7 +83,7 @@ let ungeneralizable loc id =
 
 let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let found loc id bdvars l =
-    if List.mem id l then l
+    if Id.List.mem id l then l
     else if is_freevar bdvars (Global.env ()) id
     then
       if find_generalizable_ident id then id :: l
@@ -124,7 +124,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
   let rec vars bound vs = function
     | GVar (loc,id) ->
 	if is_freevar bound (Global.env ()) id then
-	  if List.mem_assoc id vs then vs
+	  if Id.List.mem_assoc id vs then vs
 	  else (id, loc) :: vs
 	else vs
     | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
@@ -219,9 +219,8 @@ let combine_params avoid fn applied needed =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (Name id, _, _)) :: need
-        when List.mem_assoc_f Id.equal id named ->
-	  aux (List.assoc_f Id.equal id named :: ids) avoid app need
+      | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named ->
+	  aux (Id.List.assoc id named :: ids) avoid app need
 
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
diff --git a/interp/notation.ml b/interp/notation.ml
index b661c33c6..5fa6346f0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -121,7 +121,7 @@ let scope_stack = ref []
 let current_scopes () = !scope_stack
 
 let scope_is_open_in_scopes sc l =
-  List.mem (Scope sc) l
+  List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l
 
 let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 
@@ -841,19 +841,18 @@ let browse_notation strict ntn map =
     if String.contains ntn ' ' then String.equal ntn ntn'
     else
       let toks = decompose_notation_key ntn' in
-      let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
-      if strict then match trms with
-      | [Terminal ntn'] -> String.equal ntn ntn'
-      | _ -> false
-      else
-        List.mem (Terminal ntn) trms in
+      let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
+      let trms = List.map_filter get_terminals toks in
+      if strict then String.List.equal [ntn] trms
+      else String.List.mem ntn trms
+  in
   let l =
     String.Map.fold
       (fun scope_name sc ->
 	String.Map.fold (fun ntn ((_,r),df) l ->
 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
-  List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l
+  List.sort (fun x y -> String.compare (fst x) (fst y)) l
 
 let global_reference_of_notation test (ntn,(sc,c,_)) =
   match c with
@@ -917,20 +916,20 @@ let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
   String.Map.fold
     (fun ntn ((_,r),(_,df)) (l,known as acc) ->
-      if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+      if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
 
 let collect_notations stack =
   fst (List.fold_left
     (fun (all,knownntn as acc) -> function
       | Scope scope ->
-	  if List.mem_assoc scope all then acc
+	  if String.List.mem_assoc scope all then acc
 	  else
 	    let (l,knownntn) =
 	      collect_notation_in_scope scope (find_scope scope) knownntn in
 	    ((scope,l)::all,knownntn)
       | SingleNotation ntn ->
-	  if List.mem ntn knownntn then (all,knownntn)
+	  if String.List.mem ntn knownntn then (all,knownntn)
 	  else
 	    let ((_,r),(_,df)) =
 	      String.Map.find ntn (find_scope default_scope).notations in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 50cbcd605..d469f36fa 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -22,14 +22,6 @@ open Decl_kinds
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders     *)
 
-module IdList = struct
-  let assoc id l = List.assoc_f Id.equal id l
-  let remove_assoc id l = List.remove_assoc_f Id.equal id l
-  let mem id l = List.exists (Id.equal id) l
-  let mem_assoc id l = List.exists (fun (a,_) -> Id.equal id a) l
-  let rev_mem_assoc id l = List.exists (fun (_,b) -> Id.equal id b) l
-end
-
 let name_to_ident = function
   | Anonymous -> Errors.error "This expression should be a simple identifier."
   | Name id -> id
@@ -45,15 +37,15 @@ let rec cases_pattern_fold_map loc g e = function
       e', PatCstr (loc,cstr,patl',na')
 
 let rec subst_glob_vars l = function
-  | GVar (_,id) as r -> (try IdList.assoc id l with Not_found -> r)
+  | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
   | GProd (loc,Name id,bk,t,c) ->
       let id =
-	try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id
+	try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
 	with Not_found -> id in
       GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
   | GLambda (loc,Name id,bk,t,c) ->
       let id =
-	try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id
+	try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
 	with Not_found -> id in
       GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
   | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
@@ -313,18 +305,18 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
   let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
   let vars = Id.Map.filter (fun y _ -> not (Id.Set.mem y useless_vars)) vars in
   let check_recvar x =
-    if IdList.mem x found then
+    if Id.List.mem x found then
       errorlabstrm "" (pr_id x ++
 	strbrk " should only be used in the recursive part of a pattern.") in
   let check (x, y) = check_recvar x; check_recvar y in
   let () = List.iter check foundrec in
   let () = List.iter check foundrecbinding in
   let check_bound x =
-    if not (IdList.mem x found) then
-      if IdList.mem_assoc x foundrec ||
-         IdList.mem_assoc x foundrecbinding ||
-         IdList.rev_mem_assoc x foundrec ||
-         IdList.rev_mem_assoc x foundrecbinding
+    if not (Id.List.mem x found) then
+      if Id.List.mem_assoc x foundrec ||
+         Id.List.mem_assoc x foundrecbinding ||
+         Id.List.mem_assoc_sym x foundrec ||
+         Id.List.mem_assoc_sym x foundrecbinding
       then
 	error
           (Id.to_string x ^
@@ -526,11 +518,11 @@ let add_env alp (sigma,sigmalist,sigmabinders) var v =
 
 let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
   try
-    let v' = IdList.assoc var sigma in
+    let v' = Id.List.assoc var sigma in
     match v, v' with
     | GHole _, _ -> fullsigma
     | _, GHole _ ->
-      add_env alp (IdList.remove_assoc var sigma,sigmalist,sigmabinders) var v
+      add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v
     | _, _ ->
         if Pervasives.(=) v v' then fullsigma (** FIXME *)
         else raise No_match
@@ -558,7 +550,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (_,Name id2) when IdList.mem id2 (fst metas) ->
+  | (_,Name id2) when Id.List.mem id2 (fst metas) ->
       let rhs = match na1 with
       | Name id1 -> GVar (Loc.ghost,id1)
       | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in
@@ -589,15 +581,15 @@ let rec match_iterated_binders islambda decls = function
   | b -> (decls,b)
 
 let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
-  (IdList.remove_assoc x sigmavar,sigmalist,sigmabinders)
+  (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders)
 
 let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
   let rec aux sigma acc rest =
     try
       let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
-      let rest = IdList.assoc ldots_var (pi1 sigma) in
+      let rest = Id.List.assoc ldots_var (pi1 sigma) in
       let b =
-        match IdList.assoc x (pi3 sigma) with [b] -> b | _ ->assert false
+        match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false
       in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
       aux sigma (b::acc) rest
@@ -610,8 +602,8 @@ let match_alist match_fun metas sigma rest x iter termin lassoc =
   let rec aux sigma acc rest =
     try
       let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
-      let rest = IdList.assoc ldots_var (pi1 sigma) in
-      let t = IdList.assoc x (pi1 sigma) in
+      let rest = Id.List.assoc ldots_var (pi1 sigma) in
+      let t = Id.List.assoc x (pi1 sigma) in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
@@ -635,7 +627,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   match (a1,a2) with
 
   (* Matching notation variable *)
-  | r1, NVar id2 when IdList.mem id2 tmetas -> bind_env alp sigma id2 r1
+  | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
   | r1, NList (x,_,iter,termin,lassoc) ->
@@ -656,10 +648,10 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when IdList.mem id blmetas ->
+  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas ->
       match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
   | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
-      when IdList.mem id blmetas && na != Anonymous ->
+      when Id.List.mem id blmetas && na != Anonymous ->
       match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
 
   (* Matching compositionally *)
@@ -773,7 +765,7 @@ let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find x =
-    try IdList.assoc x terms
+    try Id.List.assoc x terms
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
@@ -783,9 +775,9 @@ let match_notation_constr u c (metas,pat) =
     | NtnTypeConstr ->
        ((find x, scl)::terms',termlists',binders')
     | NtnTypeConstrList ->
-       (terms',(IdList.assoc x termlists,scl)::termlists',binders')
+       (terms',(Id.List.assoc x termlists,scl)::termlists',binders')
     | NtnTypeBinderList ->
-       (terms',termlists',(IdList.assoc x binders,scl)::binders'))
+       (terms',termlists',(Id.List.assoc x binders,scl)::binders'))
     metas ([],[],[])
 
 (* Matching cases pattern *)
@@ -796,7 +788,7 @@ let add_patterns_for_params ind l =
 
 let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
-    let vvar = IdList.assoc var sigma in
+    let vvar = Id.List.assoc var sigma in
     if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *)
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
@@ -804,7 +796,7 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
 
 let rec match_cases_pattern metas sigma a1 a2 =
  match (a1,a2) with
-  | r1, NVar id2 when IdList.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
+  | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
   | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
   | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
       sigma,(0,add_patterns_for_params (fst r1) largs)
@@ -846,8 +838,8 @@ let match_ind_pattern metas sigma ind pats a2 =
 let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
-      | NtnTypeConstr -> ((IdList.assoc x terms, scl)::terms',termlists')
-      | NtnTypeConstrList -> (terms',(IdList.assoc x termlists,scl)::termlists')
+      | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
+      | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
       | NtnTypeBinderList -> assert false)
     metas ([],[])
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 832af5331..7c9db3ef7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -141,7 +141,7 @@ let fold_constr_expr_with_binders g f n acc = function
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-  | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Id.Set.add id l
+  | CRef (Ident (_,id)) -> if Id.List.mem id bdvars then l else Id.Set.add id l
   | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
   in aux [] Id.Set.empty c