suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls

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

9 files changed, 54 insertions, 47 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4a7649a79c..c096008db2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -171,8 +171,8 @@ let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
 
 exception Induc
 
-let extract_mrectype env sigma t =
-  let (t,l) = whd_stack env sigma t [] in
+let extract_mrectype t =
+  let (t,l) = whd_stack t [] in
   match t with
     | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
     | _ -> raise Induc
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b7501dd642..b603fbf1ee 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -128,17 +128,24 @@ val make_arity : env -> 'a evar_map -> bool -> inductive_family ->
 val build_branch_type : env -> bool -> constr -> constructor_summary -> constr 
 
 
-(*s [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+(*s Extracting an inductive type from a constructions *)
+
+exception Induc
+
+(* [extract_mrectype c] assumes [c] is syntactically an inductive type
+   applied to arguments then it returns its components; if not an
+   inductive type, it raises [Induc] *)
+val extract_mrectype  : constr -> inductive * constr list
+
+(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_mrectype], [find_minductype] and [find_mcoinductype]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
    They raise [Induc] if not convertible to a recursive type. *)
 
-exception Induc
 val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
 val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
 val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
-val extract_mrectype  : env -> 'a evar_map -> constr -> inductive * constr list
 
 val lookup_mind_specif : inductive -> env -> inductive_instance
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index de61b72e97..4361a1bf39 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,8 +20,11 @@ type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
 type 'a reduction_function = 'a contextual_reduction_function
 type local_reduction_function = constr -> constr
 
-type 'a stack_reduction_function = 
+type 'a contextual_stack_reduction_function = 
     env -> 'a evar_map -> constr -> constr list -> constr * constr list
+type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type local_stack_reduction_function = 
+    constr -> constr list -> constr * constr list
 
 (*************************************)
 (*** Reduction Functions Operators ***)
@@ -31,15 +34,19 @@ let rec under_casts f env sigma = function
   | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f env sigma c, t)
   | c              -> f env sigma c
 
-let rec whd_stack env sigma x stack =
+let rec local_under_casts f = function
+  | DOP2(Cast,c,t) -> DOP2(Cast,local_under_casts f c, t)
+  | c              -> f c
+
+let rec whd_stack x stack =
   match x with
-    | DOPN(AppL,cl)  -> whd_stack env sigma cl.(0) (array_app_tl cl stack)
-    | DOP2(Cast,c,_) -> whd_stack env sigma c stack
+    | DOPN(AppL,cl)  -> whd_stack cl.(0) (array_app_tl cl stack)
+    | DOP2(Cast,c,_) -> whd_stack c stack
     | _              -> (x,stack)
 	  
 let stack_reduction_of_reduction red_fun env sigma x stack =
   let t = red_fun env sigma (applistc x stack) in
-  whd_stack env sigma t []
+  whd_stack t []
 
 let strong whdfun env sigma = 
   let rec strongrec t = match whdfun env sigma t with
@@ -291,7 +298,7 @@ let rec stacklam recfun env t stack =
 let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l
 
 
-let whd_beta_stack_gen = 
+let whd_beta_stack = 
   let rec whrec x stack = match x with
     | DOP2(Lambda,c1,DLAM(name,c2)) ->
 	(match stack with
@@ -304,10 +311,7 @@ let whd_beta_stack_gen =
   in 
   whrec
 
-let whd_beta_gen x = applist (whd_beta_stack_gen x [])
-
-let whd_beta_stack env sigma = whd_beta_stack_gen 
-let whd_beta env sigma = whd_beta_gen
+let whd_beta x = applist (whd_beta_stack x [])
 
 (* 2. Delta Reduction *)
 		   
@@ -542,7 +546,7 @@ let reduce_fix whfun fix stack =
                                      --------------------
 qui coute cher dans whd_betadeltaiota *)
 
-let whd_betaiota_stack_gen = 
+let whd_betaiota_stack = 
   let rec whrec x stack =
     match x with
       | DOP2(Cast,c,_) -> whrec c stack
@@ -567,11 +571,7 @@ let whd_betaiota_stack_gen =
   in 
   whrec    
 
-let whd_betaiota_gen x = applist (whd_betaiota_stack_gen x [])
-
-let whd_betaiota_stack env sigma = whd_betaiota_stack_gen 
-let whd_betaiota env sigma = whd_betaiota_gen
-
+let whd_betaiota x = applist (whd_betaiota_stack x [])
 
 let whd_betaiotaevar_stack env sigma = 
   let rec whrec x stack =
@@ -970,7 +970,7 @@ let plain_instance s c =
     
 (* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
 let instance s c = 
-  if s = [] then c else strong whd_betaiota () () (plain_instance s c)
+  if s = [] then c else local_strong whd_betaiota (plain_instance s c)
 
 
 (* pseudo-reduction rule:
@@ -1080,7 +1080,7 @@ let compute_consteval env sigma c =
 (* One step of approximation *)
 
 let rec apprec env sigma c stack =
-  let (t,stack) = whd_betaiota_stack env sigma c stack in
+  let (t,stack) = whd_betaiota_stack c stack in
   match t with
     | DOPN(MutCase _,_) ->
         let (ci,p,d,lf) = destCase t in
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a1c5421998..9be27fb7cc 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -20,14 +20,19 @@ type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
 type 'a reduction_function = 'a contextual_reduction_function
 type local_reduction_function = constr -> constr
 
-type 'a stack_reduction_function = 
+type 'a contextual_stack_reduction_function = 
     env -> 'a evar_map -> constr -> constr list -> constr * constr list
+type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type local_stack_reduction_function = 
+    constr -> constr list -> constr * constr list
 
-val whd_stack : 'a stack_reduction_function
+val whd_stack : local_stack_reduction_function
 
 (*s Reduction Function Operators *)
 
-val under_casts : 'a reduction_function -> 'a reduction_function
+val local_under_casts : local_reduction_function -> local_reduction_function
+val under_casts :
+  'a contextual_reduction_function -> 'a contextual_reduction_function
 val strong : 'a reduction_function -> 'a reduction_function
 val local_strong : local_reduction_function -> local_reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
@@ -52,13 +57,13 @@ val cbv_betaiota : 'a reduction_function
 val cbv_betadeltaiota : 'a reduction_function
 
 (* 3. lazy strategy, weak head reduction *)
-val whd_beta : 'a reduction_function
-val whd_betaiota : 'a reduction_function
-val whd_betadeltaiota : 'a reduction_function
+val whd_beta : local_reduction_function
+val whd_betaiota : local_reduction_function
+val whd_betadeltaiota : 'a contextual_reduction_function
 
-val whd_beta_stack : 'a stack_reduction_function
-val whd_betaiota_stack : 'a stack_reduction_function
-val whd_betadeltaiota_stack : 'a stack_reduction_function
+val whd_beta_stack : local_stack_reduction_function
+val whd_betaiota_stack : local_stack_reduction_function
+val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
 
 
 (*s Head normal forms *)
diff --git a/library/indrec.ml b/library/indrec.ml
index b684226d53..e1609b25aa 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -169,15 +169,13 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
              | None -> 
 		 lambda_name env
 		   (n,t,process_constr (i+1) cprest 
-		      (applist(whd_beta_stack env sigma (lift 1 f) 
-				 [(Rel 1)])) rest)
+		      (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) rest)
              | Some(_,f_0) -> 
 		 let nF = lift (i+1+decF) f_0 in
 		 let arg = process_pos nF (lift 1 t) in 
                  lambda_name env
 		   (n,t,process_constr (i+1) cprest 
-		      (applist(whd_beta_stack env sigma (lift 1 f) 
-				 [(Rel 1); arg])) 
+		      (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
 		      rest))
       | [] -> f
   in 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c4b757034e..1c5615b25e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -97,7 +97,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
-      whd_beta env sigma (applist (pop deffix,realargs@[c]))
+      whd_beta (applist (pop deffix,realargs@[c]))
     else
       let typPfix = 
 	it_prod_name env
@@ -106,11 +106,9 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 			     (List.map (lift nar) params)
 			     (rel_list 0 nar))),
 	      (if dep then 
-		 applist (whd_beta_stack env sigma 
-			    (lift (nar+1) p) (rel_list 0 (nar+1)))
+		 applist (whd_beta_stack (lift (nar+1) p) (rel_list 0 (nar+1)))
 	       else 
-		 applist (whd_beta_stack env sigma 
-			    (lift (nar+1) p) (rel_list 1 nar)))))
+		 applist (whd_beta_stack (lift (nar+1) p) (rel_list 1 nar)))))
           lnames 
       in
       let fix = DOPN(Fix([|nar|],0),
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 86eb8113ec..955767cefb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -791,7 +791,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       in
       (bindings,dFLT)
     else
-      let (a,p) = match whd_stack env sigma (whd_beta env sigma ty) [] with
+      let (a,p) = match whd_beta_stack ty [] with
 	| (_,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausale_forme: should be a sigma type" in
       let mv = new_meta() in
@@ -1200,7 +1200,8 @@ let subst_tuple_term env sigma dep_pair b =
   strong (fun _ _ -> 
 	    compose (whd_betaiota env sigma)
 	      (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) 
-    env sigma*) whd_betaiota env sigma app_B
+    env sigma *)
+  (* whd_betaiota *) app_B
     
 (* |- (P e2)
      BY RevSubstInConcl (eq T e1 e2)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 587890ca5f..e5a657e697 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -132,9 +132,7 @@ let make_inv_predicate env sigma ind id status concl =
 		abstract_list_all env sigma p concl (realargs@[VAR id])
 	  in
 	  let hyps,_ = decompose_lam pred in
-	  let c3 =
-	    whd_beta env sigma
-	      (applist (pred,rel_list nrealargs (nrealargs +1))) 
+	  let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) 
 	  in
 	  (hyps,c3)
   in
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 52b4e288c0..23b939b3cd 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1703,7 +1703,7 @@ let tauto_of_cci_fmla gls cciterm =
 	| _ -> assert false
     else FPred cciterm
   in 
-  tradrec (whd_betaiota (pf_env gls) (project gls) cciterm)   
+  tradrec (whd_betaiota cciterm)   
 
 (*-- Retorna una lista de todas las variables proposicionales que
   aparescan en una lista de formulasS --*)