Removing more association lists in Constrintern.

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

7 files changed, 65 insertions, 45 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 363f43fd7..ece2a4518 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -799,14 +799,16 @@ let find_remaining_scopes pl1 pl2 ref =
   in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
       simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
 
+let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
+
 let product_of_cases_patterns ids idspl =
   List.fold_right (fun (ids,pl) (ids',ptaill) ->
-    (ids@ids',
+    (ids @ ids',
      (* Cartesian prod of the or-pats for the nth arg and the tail args *)
      List.flatten (
        List.map (fun (subst,p) ->
-	 List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
-    idspl (ids,[[],[]])
+	 List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
+    idspl (ids,[Id.Map.empty,[]])
 
 (* @return the first variable that occurs twice in a pattern
 
@@ -896,10 +898,13 @@ let find_constructor loc add_params ref =
     |IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.")
     |_ -> anomaly (Pp.str "unexpected global_reference in pattern")) ref in
   cstr, (function (ind,_ as c) -> match add_params with
-    |Some nb_args -> let nb = if Int.equal nb_args (Inductiveops.constructor_nrealhyps c)
-      then fst (Inductiveops.inductive_nargs ind)
-      else Inductiveops.inductive_nparams ind in
-		     Util.List.make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
+    |Some nb_args ->
+      let nb =
+        if Int.equal nb_args (Inductiveops.constructor_nrealhyps c)
+          then fst (Inductiveops.inductive_nargs ind)
+          else Inductiveops.inductive_nparams ind
+      in
+      List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
     |None -> []) cstr
 
 let find_pattern_variable = function
@@ -998,21 +1003,31 @@ let sort_fields mode loc l completer =
 
 (** {6 Manage multiple aliases} *)
 
+type alias = {
+  alias_ids : Id.t list;
+  alias_map : Id.t Id.Map.t;
+}
+
+let empty_alias = {
+  alias_ids = [];
+  alias_map = Id.Map.empty;
+}
+
   (* [merge_aliases] returns the sets of all aliases encountered at this
      point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,asubst as _aliases) id =
-  let ans = ids @ [id] in
-  let subst = match ids with
-  | [] -> asubst
-  | id' :: _ -> (id, id') :: asubst
+let merge_aliases aliases id =
+  let alias_ids = aliases.alias_ids @ [id] in
+  let alias_map = match aliases.alias_ids with
+  | [] -> aliases.alias_map
+  | id' :: _ -> Id.Map.add id id' aliases.alias_map
   in
-  (ans, subst)
+  { alias_ids; alias_map; }
 
-let alias_of = function
-  | ([],_) -> Anonymous
-  | (id::_,_) -> Name id
+let alias_of als = match als.alias_ids with
+| [] -> Anonymous
+| id :: _ -> Name id
 
-let message_redundant_alias (id1,id2) =
+let message_redundant_alias id1 id2 =
   msg_warning
     (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
 
@@ -1169,10 +1184,10 @@ let drop_notations_pattern looked_for =
     | t -> error_invalid_pattern_notation loc
   in in_pat true
 
-let rec intern_pat genv (ids,asubst as aliases) pat =
+let rec intern_pat genv aliases pat =
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
-    let idslpl2 = List.map (intern_pat genv ([],[])) pl2 in
-    let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
+    let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
+    let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
@@ -1193,10 +1208,11 @@ let rec intern_pat genv (ids,asubst as aliases) pat =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
     | RCPatAtom (loc, Some id) ->
-      let ids,asubst = merge_aliases aliases id in
-      (ids,[asubst, PatVar (loc,alias_of (ids,asubst))])
+      let aliases = merge_aliases aliases id in
+      (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
     | RCPatAtom (loc, None) ->
-      (ids,[asubst, PatVar (loc,alias_of aliases)])
+      let { alias_ids = ids; alias_map = asubst; } = aliases in
+      (ids, [asubst, PatVar (loc, alias_of aliases)])
     | RCPatOr (loc, pl) ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
@@ -1221,8 +1237,8 @@ let intern_ind_pattern genv env pat =
 	|_ -> error_bad_inductive_type loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
-      let idslpl1 = List.rev_map (intern_pat genv ([],[])) expl_pl in
-      let idslpl2 = List.map (intern_pat genv ([],[])) pl2 in
+      let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
+      let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
       (with_letin,
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
 	 |_,[_,pl] ->
@@ -1519,7 +1535,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern env n (loc,pl) =
     let idsl_pll =
-      List.map (intern_cases_pattern globalenv {env with tmp_scope = None} ([],[])) pl in
+      List.map (intern_cases_pattern globalenv {env with tmp_scope = None} empty_alias) pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns [] idsl_pll
 
@@ -1540,7 +1556,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
-      List.iter message_redundant_alias asubst;
+      Id.Map.iter message_redundant_alias asubst;
       let rhs' = intern {env with ids = env_ids} rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
@@ -1691,7 +1707,7 @@ let intern_pattern globalenv patt =
   try
     intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false;
 				    tmp_scope = None; scopes = [];
-				    impls = empty_internalization_env} ([],[]) patt
+				    impls = empty_internalization_env} empty_alias patt
   with
       InternalizationError (loc,e) ->
 	user_err_loc (loc,"internalize",explain_internalization_error e)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 5535b6c84..a4f3e057f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -83,8 +83,7 @@ val intern_gen : typing_constraint -> evar_map -> env ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-  Names.Id.t list *
-    ((Names.Id.t * Names.Id.t) list * cases_pattern) list
+  Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 54049ac5b..43c79bd49 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -251,8 +251,8 @@ let map_constr_expr_with_binders g f e = function
 (* Used in constrintern *)
 let rec replace_vars_constr_expr l = function
   | CRef (Ident (loc,id)) as x ->
-      (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
-  | c -> map_constr_expr_with_binders List.remove_assoc
+      (try CRef (Ident (loc,Id.Map.find id l)) with Not_found -> x)
+  | c -> map_constr_expr_with_binders Id.Map.remove
            replace_vars_constr_expr l c
 
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 356189643..f042de00f 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -21,7 +21,7 @@ val oldfashion_patterns : bool ref
 (** Utilities on constr_expr *)
 
 val replace_vars_constr_expr :
-  (Id.t * Id.t) list -> constr_expr -> constr_expr
+  Id.t Id.Map.t -> constr_expr -> constr_expr
 
 val free_vars_of_constr_expr : constr_expr -> Id.Set.t
 val occur_var_constr_expr : Id.t -> constr_expr -> bool
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 04c8c3064..52fb935d4 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -278,7 +278,7 @@ let rec bind_primary_aliases map pat =
 	  List.fold_left bind_primary_aliases map1 lpat
 
 let bind_secondary_aliases map subst =
-  List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst
+  Id.Map.fold (fun ids (idp : Id.t) map -> (ids,List.assoc idp map)::map) subst map
 
 let bind_aliases patvars subst patt =
   let map = bind_primary_aliases [] patt in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d1fa16c0a..993f3d5fb 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -491,11 +491,12 @@ let map_option f = function
 open Constrexpr
 open Topconstr
 
-let make_assoc = List.fold_left2 (fun l a b ->
-match a, b with
-  |(_,Name na), (_, Name id) -> (na, id)::l
-  |_,_ -> l
-)
+let make_assoc assoc l1 l2 =
+  let fold assoc a b = match a, b with
+  | (_, Name na), (_, Name id) -> Id.Map.add na id assoc
+  | _, _ -> assoc
+  in
+  List.fold_left2 fold assoc l1 l2
 
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
@@ -514,16 +515,20 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
-	      let old_nal',new_nal' = List.chop lnal nal' in 
-	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' 
+	      let old_nal',new_nal' = List.chop lnal nal' in
+	      let nassoc = make_assoc assoc old_nal' nal in
+	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
+	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if new_nal' = [] && rest = []
 		 then  typ' 
 		 else if new_nal' = [] 
 		 then CProdN(Loc.ghost,rest,typ')
 		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
-	      let captured_nal,non_captured_nal = List.chop lnal' nal in 
-	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
+	      let captured_nal,non_captured_nal = List.chop lnal' nal in
+	      let nassoc = make_assoc assoc nal' captured_nal in
+	      let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
+	      rebuild_nal ((assum :: aux), nassoc)
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
 
@@ -537,7 +542,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
      
-      let new_bl',new_ret_type,_ = rebuild_bl ([],[]) bl fix_typ in 
+      let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in 
       (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
     )
       fixpoint_exprl constr_expr_typel 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 39f91b795..b389ca790 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -309,7 +309,7 @@ let split_lambda = function
 let rename na na' t c =
   match (na,na') with
     | (_,Name id), (_,Name id') ->
-      (na',t,Topconstr.replace_vars_constr_expr [id,id'] c)
+      (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c)
     | (_,Name id), (_,Anonymous) -> (na,t,c)
     | _ -> (na',t,c)