Reverting nf_betaiotaevar_preserving_vm_cast

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

1 files changed, 43 insertions, 107 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6616b2f0af..20b48a01ae 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -451,113 +451,49 @@ let nf_betadeltaiota env sigma =
    du type checking :
      (fun x => x + x) M
 *)
-let nf_betaiotaevar_preserving_vm_cast env sigma t = 
-  let push decl (env,subst) = 
-    (Environ.push_rel decl env, Esubst.subs_lift subst) in
-  let cons decl v (env, subst) = (push_rel decl env, Esubst.subs_cons (v,subst)) in
-
-  let app_stack t (f, stack) = 
-    let t' = app_stack (f,stack) in
-    match kind_of_term t, kind_of_term t' with
-      | App(f,args), App(f',args') when f == f' && array_for_all2 (==) args args' -> t
-      | _ -> t'
-  in
-  let rec whrec (env, subst as es) (t, stack as s) =
-    match kind_of_term t with
-      | Rel i -> 
-	  let t' = 
-	    match Esubst.expand_rel i subst with
-	      | Inl (k,e) -> lift k e
-	      | Inr (k,None) -> mkRel k
-	      | Inr (k, Some p) -> lift (k-p) (mkRel p) (*??????? == mkRel k !  Julien *)
-                           (* Est correct ??? *)
-	  in
-	  if t = t' then s else t', stack
-      | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> s
-      | Evar (e,al) -> 
-	  let al' = Array.map (norm es) al in
-	  begin match existential_opt_value sigma (e,al') with
-	    | Some body -> whrec (env,Esubst.ESID 0) (body, stack) (**** ????? ****)
-	    | None ->
-		if array_for_all2 (==) al al' then s else (mkEvar (e, al'), stack)
-	  end
-      | Cast (c,VMcast,t) ->
-	  let c' = norm es c in
-	  let t' = norm es t in 
-	  if c == c' && t == t' then s
-	  else (mkCast(c',VMcast,t'),stack)
-      | Cast (c,DEFAULTcast,_) ->
-	  whrec es (c, stack)
-
-      | Prod (na,t,c) ->
-	  let t' = norm es t in
-	  let c' = norm (push (na, None, t') es) c in
-	  if t==t' && c==c' then s else (mkProd (na, t', c'), stack)
-
-      | Lambda (na,t,c) ->
-          begin match decomp_stack stack with
-            | Some (a,m) -> 
-		begin match kind_of_term a with
-		  | Rel i when not (evaluable_rel i env) ->
-                      whrec (cons (na,None,t) a es) (c, m)
-		  | Var id when  not (evaluable_named id env)->
-                      whrec (cons (na,None,t) a es) (c, m)
-		  | _ -> 
-		      let t' = norm es t in
-		      let c' = norm (push (na, None, t') es) c in
-		      if t == t' && c == c' then s
-		      else mkLambda (na, t', c'), stack
-		end
-            | _ -> 
-		let t' = norm es t in 
-		let c' =  norm (push (na, None, t') es) c  in 
-		if t == t' && c == c' then s 
-		else mkLambda(na,t',c'),stack
-		
-	  end
-      | LetIn (na,b,t,c) ->
-	  let b' = norm es b in
-	  let t' = norm es t in
-	  let c' = norm (push (na, Some b', t') es) c in
-	  if b==b' && t==t' && c==c' then s 
-	  else mkLetIn (na, b', t', c'), stack
-
-      | App (f,cl)  -> 
-          let cl' = Array.map (norm es) cl in
-          whrec es (f, append_stack cl' stack)
-
-      | Case (ci,p,d,lf) ->
-          let (c,cargs) = whrec es (d, empty_stack) in
-          if reducible_mind_case c then
-            whrec es (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else     
-	    let p' = norm es p in
-	    let d' = app_stack d (c,cargs) in 
-	    let lf' = Array.map (norm es) lf in
-	    if p==p' && d==d' && array_for_all2 (==) lf lf' then s 
-	    else (mkCase (ci, p', d', lf'), stack)
-      | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = Array.map (norm es) tl in
-	  let es' =
-            array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl' in
-	  let bl' = Array.map (norm es') bl in
-	  if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
-	  then s
-	  else (mkFix (ln,(lna,tl',bl')), stack)
-      | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = Array.map (norm es) tl in
-	  let es' =
-            array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl in
-	  let bl' = Array.map (norm es') bl in
-	  if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
-	  then s
-	  else (mkCoFix (ln,(lna,tl',bl')), stack)
-
-  and norm es t = app_stack t (whrec es (t,empty_stack)) in
-  norm (env, Esubst.ESID 0) t
-
+let rec whd_betaiotaevar_preserving_vm_cast env sigma t = 	 
+   let rec stacklam_var subst t stack = 	 
+     match (decomp_stack stack,kind_of_term t) with 	 
+     | Some (h,stacktl), Lambda (_,_,c) -> 	 
+         begin match kind_of_term h with 	 
+         | Rel i when not (evaluable_rel i env) -> 	 
+             stacklam_var (h::subst) c stacktl 	 
+         | Var id when  not (evaluable_named id env)-> 	 
+             stacklam_var (h::subst) c stacktl 	 
+         | _ -> whrec (substl subst t, stack) 	 
+         end 	 
+     | _ -> whrec (substl subst t, stack) 	 
+   and whrec (x, stack as s) = 	 
+     match kind_of_term x with 	 
+       | Evar ev -> 	 
+           (match existential_opt_value sigma ev with 	 
+              | Some body -> whrec (body, stack) 	 
+              | None -> s) 	 
+       | Cast (c,VMcast,t) -> 	 
+           let c = app_stack (whrec (c,empty_stack)) in 	 
+           let t = app_stack (whrec (t,empty_stack)) in 	 
+           (mkCast(c,VMcast,t),stack) 	 
+       | Cast (c,DEFAULTcast,_) -> 	 
+           whrec (c, stack) 	 
+       | App (f,cl)  -> whrec (f, append_stack cl stack) 	 
+       | Lambda (na,t,c) -> 	 
+           (match decomp_stack stack with 	 
+            | Some (a,m) -> stacklam_var [a] c m 	 
+            | _ -> s) 	 
+       | Case (ci,p,d,lf) -> 	 
+           let (c,cargs) = whrec (d, empty_stack) in 	 
+           if reducible_mind_case c then 	 
+             whrec (reduce_mind_case 	 
+                      {mP=p; mconstr=c; mcargs=list_of_stack cargs; 	 
+                       mci=ci; mlf=lf}, stack) 	 
+           else 	 
+             (mkCase (ci, p, app_stack (c,cargs), lf), stack) 	 
+       | x -> s 	 
+   in 	 
+   app_stack (whrec (t,empty_stack))
+
+let nf_betaiotaevar_preserving_vm_cast = 
+  strong whd_betaiotaevar_preserving_vm_cast
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =