Ajout Simpl et Change sur des sous-termes

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

4 files changed, 42 insertions, 19 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 7fd10ef23f..9354035497 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -250,15 +250,17 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+type 'a occurrences = int list * 'a
+
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl
+  | Simpl of 'a occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of (int list * 'b) list
+  | Unfold of 'b occurrences list
   | Fold of 'a list
-  | Pattern of (int list * 'a) list
+  | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
 type 'a or_metanum = AN of 'a | MetaNum of int located
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d1c480ef72..3c2241682b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -106,15 +106,17 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+type 'a occurrences = int list * 'a
+
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl
+  | Simpl of 'a occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of (int list * 'b) list
+  | Unfold of 'b occurrences list
   | Fold of 'a list
-  | Pattern of (int list * 'a) list
+  | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
 type 'a or_metanum = AN of 'a | MetaNum of int located
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 26a627d178..7613cd6df7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -595,6 +595,34 @@ let whd_nf env sigma c =
 
 let nf env sigma c = strong whd_nf env sigma c
 
+let contextually (locs,c) f env sigma t =
+  let maxocc = List.fold_right max locs 0 in
+  let pos = ref 1 in
+  let check = ref true in
+  let except = List.exists (fun n -> n<0) locs in
+  if except & (List.exists (fun n -> n>=0) locs) 
+  then error "mixing of positive and negative occurences"
+  else
+   let rec traverse (env,c as envc) t =
+    if locs <> [] & (not except) & (!pos > maxocc) then t
+    else
+    if eq_constr c t then
+      let r =
+	if except then 
+	  if List.mem (- !pos) locs then t else f env sigma t
+	else 
+	  if locs = [] or List.mem !pos locs then f env sigma t else t
+      in incr pos; r
+    else
+      map_constr_with_binders_left_to_right
+	(fun d (env,c) -> (push_rel d env,lift 1 c))
+        traverse envc t
+  in
+  let t' = traverse (env,c) t in
+  if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then
+    errorlabstrm "contextually" (str "Too few occurences");
+  t'
+
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
@@ -804,7 +832,8 @@ let declare_red_expr s f =
 let reduction_of_redexp = function
   | Red internal -> if internal then internal_red_product else red_product
   | Hnf -> hnf_constr
-  | Simpl -> nf
+  | Simpl (Some lp) -> contextually lp nf
+  | Simpl None -> nf
   | Cbv f -> cbv_norm_flags (make_flag f)
   | Lazy f -> clos_norm_flags (make_flag f)
   | Unfold ubinds -> unfoldn ubinds
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index d41161efb1..9d76b655c7 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,6 +15,7 @@ open Environ
 open Evd
 open Reductionops
 open Closure
+open Rawterm
 (*i*)
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
@@ -60,20 +61,9 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
    returns [I] and [t'] or fails with a user error *)
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
-open Rawterm
-(*
-type red_expr =
-  | Red of bool    (* raise Redelimination if true otherwise UserError *)
-  | Hnf
-  | Simpl
-  | Cbv of Closure.RedFlags.reds
-  | Lazy of Closure.RedFlags.reds
-  | Unfold of (int list * evaluable_global_reference) list
-  | Fold of constr list
-  | Pattern of (int list * constr * constr) list
-*)
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
+val contextually : constr occurrences -> reduction_function->reduction_function
 val reduction_of_redexp : red_expr -> reduction_function
 
 val declare_red_expr : string -> reduction_function -> unit