Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)

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

2 files changed, 20 insertions, 9 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4832cdd8a4..5c0a4fa634 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -219,13 +219,11 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
   substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
 
 let fix_recarg ((recindices,bodynum),_) stack =
-  if 0 <= bodynum & bodynum < Array.length recindices then
-    let recargnum = Array.get recindices bodynum in
-    (try 
-       Some (recargnum, stack_nth stack recargnum)
-     with Not_found ->
-       None)
-  else 
+  assert (0 <= bodynum & bodynum < Array.length recindices);
+  let recargnum = Array.get recindices bodynum in
+  try 
+    Some (recargnum, stack_nth stack recargnum)
+  with Not_found ->
     None
 
 type fix_reduction_result = NotReducible | Reduced of state
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index abbd47b8b1..16bd2b9c74 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -408,14 +408,27 @@ let internal_red_product env sigma c =
   let simpfun = clos_norm_flags (UNIFORM,betaiotazeta_red) env sigma in
   let rec redrec env x =
     match kind_of_term x with
-      | IsApp (f,l) -> simpfun (appvect (redrec env f, l))
+      | IsApp (f,l) -> 
+          (match kind_of_term f with
+             | IsFix fix ->
+                 let stack = append_stack l empty_stack in
+                 (match fix_recarg fix stack with
+                    | None -> raise Redelimination
+                    | Some (recargnum,recarg) ->
+                        let recarg' = redrec env recarg in
+                        let stack' = stack_assign stack recargnum recarg' in
+                        simpfun (app_stack (f,stack')))
+             | _ -> simpfun (appvect (redrec env f, l)))
       | IsCast (c,_) -> redrec env c
       | IsProd (x,a,b) -> mkProd (x, a, redrec (push_rel_assum (x,a) env) b)
       | IsLetIn (x,a,b,t) -> redrec env (subst1 a t)
+      | IsMutCase (ci,p,d,lf) -> simpfun (mkMutCase (ci,p,redrec env d,lf))
       | _ when isEvalRef x -> 
+          (* TO DO: re-fold fixpoints after expansion *)
+          (* to get true one-step reductions *)
 	  (match reference_opt_value sigma env (destEvalRef x) with
 	     | None -> raise Redelimination
-	     | Some c -> simpfun c)
+	     | Some c -> c)
       | _ -> raise Redelimination
   in redrec env c