Ajout map_constr_with_full_binders et strong pour Simpl

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

3 files changed, 39 insertions, 10 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index d496a9e49..a5f9114a8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -108,10 +108,10 @@ let stack_reduction_of_reduction red_fun env sigma s =
   let t = red_fun env sigma (app_stack s) in
   whd_stack t
 
-(* BUGGE : NE PREND PAS EN COMPTE LES DEFS LOCALES *)
-let strong whdfun env sigma = 
-  let rec strongrec t = map_constr strongrec (whdfun env sigma t) in
-  strongrec
+let strong whdfun env sigma t = 
+  let rec strongrec env t =
+    map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
+  strongrec env t
 
 let local_strong whdfun = 
   let rec strongrec t = map_constr strongrec (whdfun t) in
@@ -270,7 +270,6 @@ let reduce_fix whdfun fix stack =
 let whd_state_gen flags env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-(*
       | IsRel n when red_delta flags ->
 	  (match lookup_rel_value n env with
 	     | Some body -> whrec (lift n body, stack)
@@ -279,7 +278,6 @@ let whd_state_gen flags env sigma =
 	  (match lookup_named_value id env with
 	     | Some body -> whrec (body, stack)
 	     | None -> s)
-*)
       | IsEvar ev when red_evar flags ->
 	  (match existential_opt_value sigma ev with
 	     | Some body -> whrec (body, stack)
@@ -331,7 +329,7 @@ let whd_state_gen flags env sigma =
 let local_whd_state_gen flags = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
+      | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsApp (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
diff --git a/kernel/term.ml b/kernel/term.ml
index e29a9edcd..ff96a8e15 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -666,9 +666,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
-(* Ocaml does not guarantee Array.map is LR (even if so), then we rewrite it *)
-let array_map_left f a =
-  let l = Array.length a in
+let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *)
+  let l = Array.length a in (* (even if so), then we rewrite it *)
   if l = 0 then [||] else begin
     let r = Array.create l (f a.(0)) in
     for i = 1 to l - 1 do
@@ -714,6 +713,28 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       let tl', bl' = array_map_left_pair (f l) tl (f l') bl in
       mkCoFix (ln,(tl',lna,bl'))
 
+(* strong *)
+let map_constr_with_full_binders g f l c = match kind_of_term c with
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsCast (c,t) -> mkCast (f l c, f l t)
+  | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c)
+  | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c)
+  | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c)
+  | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
+  | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
+  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
+  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
+  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
+  | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
+  | IsFix (ln,(tl,lna,bl)) ->
+      let tll = Array.to_list tl in
+      let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in
+      mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+  | IsCoFix(ln,(tl,lna,bl)) ->
+      let tll = Array.to_list tl in
+      let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in
+      mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl))
+
 (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)
diff --git a/kernel/term.mli b/kernel/term.mli
index f909b90da..d4dbd8ce1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -631,6 +631,16 @@ val map_constr_with_named_binders :
 val map_constr_with_binders_left_to_right :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
 
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+   subterms of [c]; it carries an extra data [l] (typically a name
+   list) which is processed by [g na] (which typically cons [na] to
+   [l]) at each binder traversal (with name [na]); it is not recursive
+   and the order with which subterms are processed is not specified *)
+
+val map_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) ->
+      'a -> constr -> constr
+
 (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)