Replacing lists by maps in matching interpretation.

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

13 files changed, 48 insertions, 42 deletions

diff --git a/intf/pattern.mli b/intf/pattern.mli
index cec3fe87d..d0ccb2d9b 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -47,8 +47,8 @@ type constr_under_binders = Id.t list * constr
 
 (** Types of substitutions with or w/o bound variables *)
 
-type patvar_map = (patvar * constr) list
-type extended_patvar_map = (patvar * constr_under_binders) list
+type patvar_map = constr Id.Map.t
+type extended_patvar_map = constr_under_binders Id.Map.t
 
 (** {5 Patterns} *)
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 60ae0784f..998e54767 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -399,7 +399,7 @@ let quote_terms ivs lc gl =
       match l with
         | (lhs, rhs)::tail ->
             begin try
-              let s1 = matches rhs c in
+              let s1 = Id.Map.bindings (matches rhs c) in
               let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
 	      in
               Termops.subst_meta s2 lhs
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 979a7dae3..65971d6e3 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -62,12 +62,12 @@ let warn_bound_again name =
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
-    let (ids', m') = List.assoc n terms in
+    let (ids', m') = Id.Map.find n terms in
     if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
     let () = if Id.Map.mem n names then warn_bound_meta n in
-    (names, (n, x) :: terms)
+    (names, Id.Map.add n x terms)
 
 let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
 | Name id1, Name id2 ->
@@ -76,7 +76,7 @@ let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
     (names, terms)
   else
     let names = Id.Map.add id1 id2 names in
-    let () = if List.mem_assoc id1 terms then warn_bound_again id1 in
+    let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
     (names, terms)
 | _ -> subst
 
@@ -250,12 +250,11 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
       | _ -> raise PatternMatchingFailure
 
   in
-  let names, terms = sorec [] (Id.Map.empty, []) pat c in
-  (names, List.sort (fun (a, _) (b, _) -> Id.compare a b) terms)
+  sorec [] (Id.Map.empty, Id.Map.empty) pat c
 
 let matches_core_closed convert allow_partial_app pat c =
   let names, subst = matches_core convert allow_partial_app false pat c in
-  (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+  (names, Id.Map.map snd subst)
 
 let extended_matches = matches_core None true true
 
@@ -286,7 +285,7 @@ let matches_head pat c =
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
     let sigma = matches_core_closed None partial_app pat c in
-    if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
+    if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma)
     then Lazy.force next
     else mkresult sigma (mk_ctx (mkMeta special_meta)) next
   with PatternMatchingFailure -> Lazy.force next
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5e4e5eb97..d695e8a45 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -203,7 +203,7 @@ let instantiate_pattern sigma lvar c =
   let rec aux vars = function
   | PVar id as x ->
       (try
-	let ctx,c = List.assoc id lvar in
+	let ctx,c = Id.Map.find id lvar in
 	try
 	  let inst =
 	    List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in
@@ -213,7 +213,7 @@ let instantiate_pattern sigma lvar c =
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
 	  error_instantiate_pattern id (List.subtract ctx vars)
-       with Not_found (* List.assoc failed *) ->
+       with Not_found (* Map.find failed *) ->
 	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
   | c ->
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 4a4649cca..5cc4049ba 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -53,7 +53,7 @@ val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  Evd.evar_map -> (Id.t * (Id.t list * constr)) list ->
+  Evd.evar_map -> extended_patvar_map ->
   constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 31cf52eac..a8cdfd869 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -897,7 +897,7 @@ let contextually byhead (occs,c) f env sigma t =
 	else not (List.mem !pos locs) in
       incr pos;
       if ok then
-        let subst' = List.map (on_snd (traverse envc)) subst in
+        let subst' = Id.Map.map (traverse envc) subst in
 	f subst' env sigma t
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 853720877..b5586bbd9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1110,7 +1110,7 @@ let (forward_interp_tactic, extern_interp) = Hook.make ()
 let conclPattern concl pat tac gl =
   let constr_bindings =
     match pat with
-    | None -> []
+    | None -> Id.Map.empty
     | Some pat ->
 	try matches pat concl
 	with PatternMatchingFailure -> error "conclPattern" in
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 87aff97fb..e096ac449 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Names
 open Errors
 open Evar_refiner
 open Tacmach
@@ -41,7 +42,9 @@ let instantiate n (ist,rawc) ido gl =
     if n <= 0 then error "Incorrect existential variable index.";
     let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
-    let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_filtered_env evi) 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 sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index ede813cdb..d870bfa1d 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -289,7 +289,8 @@ let is_equality_type t = op2bool (match_with_equality_type t)
 let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 
 let match_arrow_pattern t =
-  match matches coq_arrow_pattern t with
+  let result = matches coq_arrow_pattern t in
+  match Id.Map.bindings result with
     | [(m1,arg);(m2,mind)] ->
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching")
@@ -373,7 +374,7 @@ let match_eq eqn eq_pat =
     try Lazy.force eq_pat
     with e when Errors.noncritical e -> raise PatternMatchingFailure
   in
-  match matches pat eqn with
+  match Id.Map.bindings (matches pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
 	assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	PolymorphicLeibnizEq (t,x,y)
@@ -420,7 +421,7 @@ let find_this_eq_data_decompose gl eqn =
 open Tacmach
 
 let match_eq_nf gls eqn eq_pat =
-  match pf_matches gls (Lazy.force eq_pat) eqn with
+  match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
@@ -440,7 +441,7 @@ let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
 let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
 
 let match_sigma ex ex_pat =
-  match matches (Lazy.force ex_pat) ex with
+  match Id.Map.bindings (matches (Lazy.force ex_pat) ex) with
     | [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	(a,p,car,cdr)
@@ -456,7 +457,7 @@ let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
 
 let match_sigma t =
-  match matches (Lazy.force coq_sig_pattern) t with
+  match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with
     | [(_,a); (_,p)] -> (a,p)
     | _ -> anomaly (Pp.str "Unexpected pattern")
 
@@ -493,7 +494,7 @@ let match_eqdec t =
     try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
     with PatternMatchingFailure ->
         false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
-  match subst with
+  match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
       eqonleft, Globnames.constr_of_global (Lazy.force op), c1, c2, typ
   | _ -> anomaly (Pp.str "Unexpected pattern")
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 761dfe6a9..c0903c2a9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -221,7 +221,7 @@ let value_of_ident id = VIntroPattern (IntroIdentifier id)
 
 let extend_values_with_bindings (ln,lm) lfun =
   let lnames = Id.Map.fold (fun id id' accu -> (id,value_of_ident id') :: accu) ln [] in
-  let lmatch = List.map (fun (id,(ids,c)) -> (id,VConstr (ids,c))) lm in
+  let lmatch = Id.Map.fold (fun id (ids,c) accu -> (id, VConstr (ids, c)) :: accu) lm [] in
   (* For compatibility, bound variables are visible only if no other
      binding of the same name exists *)
   lmatch@lfun@lnames
@@ -449,13 +449,13 @@ let extract_ltac_constr_values ist env =
   let rec aux = function
   | (id,v)::tl ->
       let (l1,l2) = aux tl in
-      (try ((id,constr_of_value env v)::l1,l2)
+      (try (Id.Map.add id (constr_of_value env v) l1,l2)
        with Not_found ->
 	 let ido = match v with
 	   | VIntroPattern (IntroIdentifier id0) -> Some id0
 	   | _ -> None in
 	 (l1,(id,ido)::l2))
-  | [] -> ([],[]) in
+  | [] -> (Id.Map.empty,[]) in
   aux ist.lfun
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
@@ -492,18 +492,21 @@ 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 ltacvars,unbndltacvars) in
+      let ltacdata = (List.map fst ltacbnd, 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.trace 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 ist.debug env c;
@@ -936,19 +939,18 @@ let equal_instances gl (ctx',c') (ctx,c) =
 (* While non-linear matching is modulo eq_constr in matches, merge of *)
 (* different instances of the same metavars is here modulo conversion... *)
 let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
-  let rec aux = function
-  | (id,c as x)::tl ->
-      if List.for_all (fun (id',c') -> not (Id.equal id' id) || equal_instances gl c' c) lcm
-      then
-	x :: aux tl
-      else
-	raise Not_coherent_metas
-  | [] -> lcm in
+  let merge id oc1 oc2 = match oc1, oc2 with
+  | None, None -> None
+  | None, Some c | Some c, None -> Some c
+  | Some c1, Some c2 ->
+    if equal_instances gl c1 c2 then Some c1
+    else raise Not_coherent_metas
+  in
   (** ppedrot: Is that even correct? *)
   let merged = Id.Map.fold Id.Map.add ln ln1 in
-  (merged, aux lm)
+  (merged, Id.Map.merge merge lcm lm)
 
-let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
+let adjust (l, lc) = (l, Id.Map.map (fun c -> [], c) lc)
 
 type 'a extended_matching_result =
     { e_ctx : 'a;
@@ -2045,5 +2047,5 @@ let tacticIn t =
 
 let _ = Hook.set Auto.extern_interp
   (fun l ->
-    let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
-    interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
+    let l = Id.Map.mapi (fun id c -> VConstr ([], c)) l in
+    interp_tactic {lfun=Id.Map.bindings l;avoid_ids=[];debug=get_debug(); trace=[]})
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 1352d7248..48ba28e11 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -40,7 +40,8 @@ and interp_sign =
     trace : ltac_trace }
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
-  Pretyping.ltac_var_map
+  Pattern.constr_under_binders Id.Map.t * (Id.Map.key * Id.t option) list
+(* should be Pretyping.ltac_var_map *)
 
 (** Tactic extensions *)
 val add_tactic :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c96ef7e3..cee98b7c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -324,7 +324,7 @@ let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
   | Some occl ->
       contextually false occl
-        (fun subst -> change_and_check Reduction.CONV (replace_vars subst t))
+        (fun subst -> change_and_check Reduction.CONV (replace_vars (Id.Map.bindings subst) t))
 
 let change_in_concl occl t =
   reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index afd04f8b9..4de5f3cc2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1080,12 +1080,12 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
 	   let unboundvars = List.map_filter filter unboundvars in
 	   quote (pr_glob_constr_env (Global.env()) c) ++
-	     (if not (List.is_empty unboundvars) || not (List.is_empty vars) then
+	     (if not (List.is_empty unboundvars) || not (Id.Map.is_empty vars) then
 		strbrk " (with " ++
 		  prlist_with_sep pr_comma
 		  (fun (id,c) ->
 		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-		  (List.rev vars @ unboundvars) ++ str ")"
+		  (List.rev (Id.Map.bindings vars) @ unboundvars) ++ str ")"
 	      else mt())) ++
       (if Int.equal n 2 then str " (repeated twice)"
        else if n>2 then str " (repeated "++int n++str" times)"