Generalizing the use of maps instead of lists in the interpretation

of tactics.

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

12 files changed, 44 insertions, 41 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6eed1d0ed3..87efaca199 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -635,7 +635,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   else
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
   try
-    match List.assoc id unbndltacvars with
+    match Id.Map.find id unbndltacvars with
       | None -> user_err_loc (loc,"intern_var",
 	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
@@ -1662,8 +1662,12 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
+type ltac_sign = Id.t list * unbound_ltac_var_map
+
+let empty_ltac_sign = ([], Id.Map.empty)
+
 let intern_gen kind sigma env
-               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
                c =
   let tmp_scope = scope_of_type_kind kind in
   internalize sigma env {ids = extract_ids env; unb = false;
@@ -1742,9 +1746,7 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
 
 (* Miscellaneous *)
 
-type ltac_sign = Id.t list * unbound_ltac_var_map
-
-let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
+let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
             ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
@@ -1755,7 +1757,7 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
   let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
   let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
-    false (([],[]),vl) a in
+    false (empty_ltac_sign, vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = notation_constr_of_glob_constr vars recvars c in
   (* Splits variables into those that are binding, bound, or both *)
@@ -1784,7 +1786,7 @@ let my_intern_constr sigma env lvar acc c =
 
 let intern_context global_level sigma env impl_env binders =
   try
-  let lvar = (([],[]), []) in
+  let lvar = (empty_ltac_sign, []) in
   let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2a0bbd7b78..44fd838319 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
-    ~allow_patvar:false  ~ltacvars:([],[]) c
+    ~allow_patvar:false  ~ltacvars:([],Id.Map.empty) c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0af88d1dc3..4c51cffe1e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,8 +45,8 @@ open Pattern
 open Misctypes
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type var_map = (Id.t * constr_under_binders) list
-type unbound_ltac_var_map = (Id.t * Id.t option) list
+type var_map = constr_under_binders Id.Map.t
+type unbound_ltac_var_map = Id.t option Id.Map.t
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
@@ -243,7 +243,7 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id =
   with Not_found ->
     (* Check if [id] is an ltac variable *)
     try
-      let (ids,c) = List.assoc id lvar in
+      let (ids,c) = Id.Map.find id lvar in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
 	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
@@ -255,7 +255,7 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id =
       with Not_found ->
 	(* [id] not found, build nice error message if [id] yet known from ltac *)
 	try
-	  match List.assoc id unbndltacvars with
+	  match Id.Map.find id unbndltacvars with
 	  | None -> user_err_loc (loc,"",
 				  str "Variable " ++ pr_id id ++ str " should be bound to a term.")
 	  | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
@@ -783,6 +783,8 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
+let empty_lvar : ltac_var_map = (Id.Map.empty, Id.Map.empty)
+
 let on_judgment f j =
   let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
   let (c,_,t) = destCast (f c) in
@@ -790,12 +792,12 @@ let on_judgment f j =
 
 let understand_judgment sigma env c =
   let evdref = ref sigma in
-  let j = pretype empty_tycon env evdref ([],[]) c in
+  let j = pretype empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     snd (process_inference_flags all_and_fail_flags env sigma (!evdref,c))) j
 
 let understand_judgment_tcc evdref env c =
-  let j = pretype empty_tycon env evdref ([],[]) c in
+  let j = pretype empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
@@ -806,13 +808,13 @@ let understand
     ?(flags=all_and_fail_flags)
     ?(expected_type=WithoutTypeConstraint)
     sigma env c =
-  snd (ise_pretype_gen flags sigma env ([],[]) expected_type c)
+  snd (ise_pretype_gen flags sigma env empty_lvar expected_type c)
 
 let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c =
-  ise_pretype_gen flags sigma env ([],[]) expected_type c
+  ise_pretype_gen flags sigma env empty_lvar expected_type c
 
 let understand_tcc_evars ?(flags=all_no_fail_flags) evdref env ?(expected_type=WithoutTypeConstraint) c =
-  let sigma, c = ise_pretype_gen flags !evdref env ([],[]) expected_type c in
+  let sigma, c = ise_pretype_gen flags !evdref env empty_lvar expected_type c in
   evdref := sigma;
   c
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index df65f10f33..8a0b1f8862 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -28,8 +28,8 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type var_map = (Id.t * Pattern.constr_under_binders) list
-type unbound_ltac_var_map = (Id.t * Id.t option) list
+type var_map = Pattern.constr_under_binders Id.Map.t
+type unbound_ltac_var_map = Id.t option Id.Map.t
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0e317e68e5..efed7f63de 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -64,5 +64,6 @@ let instantiate_pf_com evk com sigma =
   let evi = Evd.find sigma evk in
   let env = Evd.evar_filtered_env evi in
   let rawc = Constrintern.intern_constr sigma env com in
-  let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
+  let ltac_vars = (Id.Map.empty, Id.Map.empty) in
+  let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
   sigma'
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 609c7782d7..737cea68c4 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -53,8 +53,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr *
-      (extended_patvar_map * (Id.t * Id.t option) list)
+  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 33e1f29c59..f7cd8ad87d 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -80,8 +80,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr *
-      (extended_patvar_map * (Id.t * Id.t option) list)
+  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index e096ac4498..64f8e208eb 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -43,8 +43,7 @@ let instantiate n (ist,rawc) ido gl =
     let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
     let filtered = Evd.evar_filtered_env evi in
-    let (bvars, uvars) = Tacinterp.extract_ltac_constr_values ist filtered in
-    let ltac_vars = (Id.Map.bindings bvars, uvars) in
+    let ltac_vars = Tacinterp.extract_ltac_constr_values ist filtered in
     let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 3e008657fe..cfb96b488f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -302,8 +302,9 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
+  let ltacvars = (fst lfun, Id.Map.empty) in
   let c' =
-    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
+    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
   in
   (c',if !strict_check then None else Some c)
 
@@ -440,11 +441,11 @@ let intern_hyp_location ist ((occs,id),hl) =
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
-      let ltacvars = (lfun,[]) in
+      let ltacvars = (lfun, Id.Map.empty) in
       let (metas,pc) = intern_constr_pattern ist ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
-      let ltacvars = (lfun,[]) in
+      let ltacvars = (lfun, Id.Map.empty) in
       let (metas,pc) = intern_constr_pattern ist ltacvars pc in
       None, metas, Term pc
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e0fe2cde41..852348e71e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -399,7 +399,7 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
 
 (* Extract the constr list from lfun *)
 let extract_ltac_constr_values ist env =
-  let fold (id, v) (vars1, vars2) =
+  let fold (vars1, vars2) (id, v) =
     try
       let c = coerce_to_constr env v in
       (Id.Map.add id c vars1, vars2)
@@ -412,9 +412,9 @@ let extract_ltac_constr_values ist env =
           | _ -> None
         else None
       in
-      (vars1, (id, ido) :: vars2)
+      (vars1, Id.Map.add id ido vars2)
   in
-  List.fold_right fold ist.lfun (Id.Map.empty, [])
+  List.fold_left fold (Id.Map.empty, Id.Map.empty) ist.lfun
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
 let rec intropattern_ids (loc,pat) = match pat with
@@ -459,21 +459,20 @@ let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
-  let ltacbnd = Id.Map.bindings ltacvars in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
   | Some c ->
-      let ltacdata = (List.map fst ltacbnd, unbndltacvars) in
+      let fold id _ accu = id :: accu in
+      let ltacvars = Id.Map.fold fold ltacvars [] in
+      let ltacdata = (ltacvars, unbndltacvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
   let (evd,c) =
-    (** FIXME: we should propagate the use of Id.Map.t everywhere *)
-    let vars = (ltacbnd, unbndltacvars) in
     catch_error trace (understand_ltac flags sigma env vars kind) c
   in
   db_constr (curr_debug ist) env c;
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 6affc21a47..32880fd771 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -45,8 +45,7 @@ val f_avoid_ids : Id.t list TacStore.field
 val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
-  Pattern.constr_under_binders Id.Map.t * (Id.Map.key * Id.t option) list
-(* should be Pretyping.ltac_var_map *)
+  Pretyping.ltac_var_map
 
 (** Tactic extensions *)
 val add_tactic :
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4de5f3cc22..66eda3e80c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1076,9 +1076,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	   quote (Pptactic.pr_glob_tactic (Global.env())
 		    (Tacexpr.TacAtom (Loc.ghost,te)))
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
-	   let filter =
-	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
-	   let unboundvars = List.map_filter filter unboundvars in
+          let fold id v accu = match v with
+          | None -> accu
+          | Some id' -> (id, ([], mkVar id')) :: accu
+          in
+          let unboundvars = Id.Map.fold fold unboundvars [] in
 	   quote (pr_glob_constr_env (Global.env()) c) ++
 	     (if not (List.is_empty unboundvars) || not (Id.Map.is_empty vars) then
 		strbrk " (with " ++