replacing whd_betaiotaevar_preserving_vm_cast

by nf_betaiotaevar_preserving_vm_cast.


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

1 files changed, 114 insertions, 40 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f6859bc19..6616b2f0a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -338,46 +338,6 @@ let local_whd_state_gen flags =
   in 
   whrec
 
-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))
 
 (* 1. Beta Reduction Functions *)
 
@@ -485,6 +445,120 @@ let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
 let nf_betadeltaiota env sigma =
   clos_norm_flags Closure.betadeltaiota env sigma
 
+
+(* Attention reduire un beta-redexe avec un argument qui n'est pas 
+   une variable, peut changer enormement le temps de conversion lors
+   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
+
+
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
   whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t))