In "simpl c" and "change c with d", c can be a pattern.

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

8 files changed, 42 insertions, 29 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f1da217a6..d46fd226e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -658,7 +658,8 @@ let rec subst_rawconstr subst raw =
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
   | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
-      TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw
+      TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) ->
+      raw
 
   | RCast (loc,r1,k) ->
       (match k with
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7b8c62360..105672564 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -92,6 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with
 open Evd
 
 let pattern_of_constr sigma t =
+  let ctx = ref [] in
   let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -106,9 +107,11 @@ let pattern_of_constr sigma t =
     | App (f,a) ->
         (match 
           match kind_of_term f with
-            Evar (evk,args) ->
+            Evar (evk,args as ev) ->
               (match snd (Evd.evar_source evk sigma) with
-                  MatchingVar (true,n) -> Some n
+                  MatchingVar (true,id) ->
+                    ctx := (id,None,existential_type sigma ev)::!ctx;
+                    Some id
                 | _ -> None)
             | _ -> None
           with
@@ -117,9 +120,11 @@ let pattern_of_constr sigma t =
     | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind sp        -> PRef (canonical_gr (IndRef sp))
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
-    | Evar (evk,ctxt) ->
+    | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
-          | MatchingVar (b,n) -> assert (not b); PMeta (Some n)
+          | MatchingVar (b,id) ->
+              ctx := (id,None,existential_type sigma ev)::!ctx;
+              assert (not b); PMeta (Some id)
           | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
@@ -129,8 +134,11 @@ let pattern_of_constr sigma t =
 	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
-    | CoFix f -> PCoFix f
-  in pattern_of_constr t
+    | CoFix f -> PCoFix f in
+  let p = pattern_of_constr t in
+  (* side-effect *)
+  (* Warning: the order of dependencies in ctx is not ensured *)
+  (!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -167,7 +175,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr Evd.empty t
+	 snd (pattern_of_constr Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 0e87025fc..e7460377b 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern
+val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
 
 (* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b40476c97..e847894a5 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -11,6 +11,9 @@ Typing
 Evarutil
 Term_dnet
 Recordops
+Rawterm
+Pattern
+Matching
 Tacred
 Evarconv
 Typeclasses_errors
@@ -19,11 +22,8 @@ Classops
 Coercion
 Unification
 Clenv
-Rawterm
-Pattern
 Detyping
 Indrec
 Cases
 Pretyping
-Matching
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 727ac117c..16421b2a7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -344,10 +344,10 @@ let no_occurrences_expr = (true,[])
 
 type 'a with_occurrences = occurrences_expr * 'a
 
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a with_occurrences option
+  | Simpl of 'c with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
   | Unfold of 'b with_occurrences list
@@ -356,8 +356,8 @@ type ('a,'b) red_expr_gen =
   | ExtraRedExpr of string
   | CbvVm
 
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a,'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 5cf227440..ac4f0dec6 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -155,10 +155,10 @@ val no_occurrences_expr : occurrences_expr
 
 type 'a with_occurrences = occurrences_expr * 'a
 
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a with_occurrences option
+  | Simpl of 'c with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
   | Unfold of 'b with_occurrences list
@@ -167,8 +167,8 @@ type ('a,'b) red_expr_gen =
   | ExtraRedExpr of string
   | CbvVm
 
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a,'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7079b937b..a103c49b6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,8 @@ open Closure
 open Reductionops
 open Cbv
 open Rawterm
+open Pattern
+open Matching
 
 (* Errors *)
 
@@ -733,10 +735,10 @@ let simpl env sigma c = strong whd_simpl env sigma c
 
 (* Reduction at specific subterms *)
 
-let is_head c t =
+let matches_head c t =
   match kind_of_term t with
-    | App (f,_) -> f = c
-    | _ -> false
+    | App (f,_) -> matches c f
+    | _ -> raise PatternMatchingFailure
 
 let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
   let maxocc = List.fold_right max locs 0 in
@@ -744,22 +746,23 @@ let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
   let rec traverse (env,c as envc) t =
     if nowhere_except_in & (!pos > maxocc) then t
     else
-    if (not byhead & eq_constr c t) or (byhead & is_head c t) then
+    try
+      let subst = if byhead then matches_head c t else matches c t in
       let ok =
 	if nowhere_except_in then List.mem !pos locs
 	else not (List.mem !pos locs) in
       incr pos;
       if ok then
-	f env sigma t
+	f subst env sigma t
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)
         let (f,l) = destApp t in
 	mkApp (f, array_map_left (traverse envc) l)
       else
 	t
-    else
+    with PatternMatchingFailure ->
       map_constr_with_binders_left_to_right
-	(fun d (env,c) -> (push_rel d env,lift 1 c))
+	(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
         traverse envc t
   in
   let t' = traverse (env,c) t in
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 80eca2bcc..2bba87a75 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -17,6 +17,7 @@ open Reductionops
 open Closure
 open Rawterm
 open Termops
+open Pattern
 (*i*)
 
 type reduction_tactic_error =
@@ -92,5 +93,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-val contextually : bool -> occurrences * constr -> reduction_function
-  -> reduction_function
+val contextually : bool -> occurrences * constr_pattern ->
+  (patvar_map -> reduction_function) -> reduction_function