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

6 files changed, 33 insertions, 26 deletions

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)