tacred uses stack_reduction_function instead of state_reduction_function

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

3 files changed, 71 insertions, 78 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a62fb38552..be2d5e2b7e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -285,18 +285,6 @@ let fix_recarg ((recindices,bodynum),_) stack =
   with Not_found ->
     None
 
-type fix_reduction_result = NotReducible | Reduced of state
-
-let reduce_fix whdfun sigma fix stack =
-  match fix_recarg fix stack with
-    | None -> NotReducible
-    | Some (recargnum,recarg) ->
-        let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in
-        let stack' = stack_assign stack recargnum (zip recarg') in
-	(match kind_of_term recarg'hd with
-           | Construct _ -> Reduced (contract_fix fix, stack')
-	   | _ -> NotReducible)
-
 (* Generic reduction function *)
 
 (* Y avait un commentaire pour whd_betadeltaiota :
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d42ef24048..083834218e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -179,14 +179,8 @@ val is_arity : env ->  evar_map -> constr -> bool
 
 val whd_programs :  reduction_function
 
-(** [reduce_fix redfun fix stk] contracts [fix stk] if it is actually
-   reducible; the structural argument is reduced by [redfun] *)
-
-type fix_reduction_result = NotReducible | Reduced of state
-
+val contract_fix : fixpoint -> Term.constr
 val fix_recarg : fixpoint -> constr stack -> (int * constr) option
-val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint
-   -> constr stack -> fix_reduction_result
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
 val is_transparent : 'a tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a9d23d7f79..f2f01c3f74 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -327,7 +327,7 @@ let reference_eval sigma env = function
 let x = Name (id_of_string "x")
 
 let make_elim_fun (names,(nbfix,lv,n)) largs =
-  let lu = nfirsts_app_of_stack n largs in
+  let lu = list_firstn n largs in
   let p = List.length lv in
   let lyi = List.map fst lv in
   let la =
@@ -431,7 +431,17 @@ let substl_checking_arity env subst c =
       | _ -> map_constr nf_fix c in
   nf_fix body
 
+type fix_reduction_result = NotReducible | Reduced of (constr*constr list)
 
+let reduce_fix whdfun sigma fix stack =
+  match fix_recarg fix [Zapp stack] with
+    | None -> NotReducible
+    | Some (recargnum,recarg) ->
+        let (recarg'hd,_ as recarg') = whdfun sigma recarg in
+        let stack' = list_assign stack recargnum (applist recarg') in
+	(match kind_of_term recarg'hd with
+           | Construct _ -> Reduced (contract_fix fix, stack')
+	   | _ -> NotReducible)
 
 let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
@@ -441,16 +451,16 @@ let contract_fix_use_function env sigma f
   substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
-  match fix_recarg fix stack with
+  match fix_recarg fix [Zapp stack] with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') =
 	  if isRel recarg then
 	    (* The recarg cannot be a local def, no worry about the right env *)
-	    (recarg, empty_stack)
+	    (recarg, [])
 	  else
-	    whfun (recarg, empty_stack) in
-        let stack' = stack_assign stack recargnum (zip recarg') in
+	    whfun recarg in
+        let stack' = list_assign stack recargnum (applist recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ ->
 	       Reduced (contract_fix_use_function env sigma f fix,stack')
@@ -506,19 +516,19 @@ let special_red_case env sigma whfun (ci, p, c, lf)  =
         | Some gvalue ->
 	    if reducible_mind_case gvalue then
 	      reduce_mind_case_use_function constr env sigma
-	        {mP=p; mconstr=gvalue; mcargs=list_of_app_stack cargs;
+	        {mP=p; mconstr=gvalue; mcargs=cargs;
                 mci=ci; mlf=lf}
 	    else
-	      redrec (gvalue, cargs)
+	      redrec (applist(gvalue, cargs))
     else
       if reducible_mind_case constr then
         reduce_mind_case
-	  {mP=p; mconstr=constr; mcargs=list_of_app_stack cargs;
+	  {mP=p; mconstr=constr; mcargs=cargs;
 	  mci=ci; mlf=lf}
       else
 	raise Redelimination
   in
-  redrec (c, empty_stack)
+  redrec c
 
 (* data structure to hold the map kn -> rec_args for simpl *)
 
@@ -612,7 +622,7 @@ let dont_expose_case r =
    it fails if no redex is around *)
 
 let rec red_elim_const env sigma ref largs =
-  let nargs = stack_args_size largs in
+  let nargs = List.length largs in
   let largs, unfold_anyway, unfold_nonelim =
     match recargs ref with
     | None -> largs, false, false
@@ -620,24 +630,24 @@ let rec red_elim_const env sigma ref largs =
     | Some (x::l,_) when nargs <= List.fold_left max x l -> raise Redelimination
     | Some (l,n) ->
         List.fold_left (fun stack i ->
-          let arg = stack_nth stack i in
-          let rarg = whd_construct_state env sigma (arg, empty_stack) in
+          let arg = List.nth stack i in
+          let rarg = whd_construct_stack env sigma arg in
           match kind_of_term (fst rarg) with
-          | Construct _ -> stack_assign stack i (zip rarg)
+          | Construct _ -> list_assign stack i (applist rarg)
           | _ -> raise Redelimination)
-        largs l, n >= 0 && l =  [] && nargs >= n, 
+        largs l, n >= 0 && l =  [] && nargs >= n,
                  n >= 0 && l <> [] && nargs >= n in
   try match reference_eval sigma env ref with
     | EliminationCases n when nargs >= n ->
 	let c = reference_value sigma env ref in
-	let c', lrest = whd_betadelta_state env sigma (c,largs) in
-	let whfun = whd_simpl_state env sigma in
+	let c', lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
+	let whfun = whd_simpl_stack env sigma in
         (special_red_case env sigma whfun (destCase c'), lrest)
     | EliminationFix (min,minfxargs,infos) when nargs >= min ->
 	let c = reference_value sigma env ref in
-	let d, lrest = whd_betadelta_state env sigma (c,largs) in
+	let d, lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
-	let whfun = whd_construct_state env sigma in
+	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
            | Reduced (c,rest) -> (nf_beta sigma c, rest))
@@ -647,73 +657,74 @@ let rec red_elim_const env sigma ref largs =
 	  if ref = refgoal then
 	    (c,args)
 	  else
-	    let c', lrest = whd_betalet_state sigma (c,args) in
+	    let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
 	    descend (destEvalRef c') lrest in
 	let (_, midargs as s) = descend ref largs in
-	let d, lrest = whd_betadelta_state env sigma s in
+	let d, lrest = whd_betadelta_stack env sigma (applist s) in
 	let f = make_elim_fun refinfos midargs in
-	let whfun = whd_construct_state env sigma in
+	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value sigma env ref in
-         whd_betaiotazeta sigma (zip (c, largs)), empty_stack
+         whd_betaiotazeta sigma (applist (c, largs)), []
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
        let c = reference_value sigma env ref in
-       whd_betaiotazeta sigma (zip (c, largs)), empty_stack
+       whd_betaiotazeta sigma (applist (c, largs)), []
 
 (* reduce to whd normal form or to an applied constant that does not hide
    a reducible iota/fix/cofix redex (the "simpl" tactic) *)
 
-and whd_simpl_state env sigma s =
-  let rec redrec (x, stack as s) =
+and whd_simpl_stack env sigma =
+  let rec redrec s =
+    let (x, stack as s') = decompose_app s in
     match kind_of_term x with
       | Lambda (na,t,c) ->
-          (match decomp_stack stack with
-             | None -> s
-             | Some (a,rest) -> stacklam redrec [a] c rest)
-      | LetIn (n,b,t,c) -> stacklam redrec [b] c stack
-      | App (f,cl) -> redrec (f, append_stack_app cl stack)
-      | Cast (c,_,_) -> redrec (c, stack)
+          (match stack with
+             | [] -> s'
+             | a :: rest -> redrec (beta_applist (x,stack)))
+      | LetIn (n,b,t,c) -> redrec (applist (substl [b] c, stack))
+      | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
+      | Cast (c,_,_) -> redrec (applist(c, stack))
       | Case (ci,p,c,lf) ->
           (try
-	    redrec (special_red_case env sigma redrec (ci,p,c,lf), stack)
+	    redrec (applist(special_red_case env sigma redrec (ci,p,c,lf), stack))
 	  with
-	      Redelimination -> s)
+	      Redelimination -> s')
       | Fix fix ->
-	  (try match reduce_fix (whd_construct_state env) sigma fix stack with
-            | Reduced s' -> redrec s'
-	    | NotReducible -> s
-	  with Redelimination -> s)
+	  (try match reduce_fix (whd_construct_stack env) sigma fix stack with
+            | Reduced s' -> redrec (applist s')
+	    | NotReducible -> s'
+	  with Redelimination -> s')
       | _ when isEvalRef env x ->
 	  let ref = destEvalRef x in
           (try
-            let hd, _ as s' = redrec (red_elim_const env sigma ref stack) in
+            let hd, _ as s'' = redrec (applist(red_elim_const env sigma ref stack)) in
             let rec is_case x = match kind_of_term x with
               | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
               | App (hd, _) -> is_case hd
               | Case _ -> true
               | _ -> false in
             if dont_expose_case ref && is_case hd then raise Redelimination
-            else s'
+            else s''
            with Redelimination ->
-	     s)
-      | _ -> s
+	     s')
+      | _ -> s'
   in
-  redrec s
+  redrec
 
 (* reduce until finding an applied constructor or fail *)
 
-and whd_construct_state env sigma s =
-  let (constr, cargs as s') = whd_simpl_state env sigma s in
+and whd_construct_stack env sigma s =
+  let (constr, cargs as s') = whd_simpl_stack env sigma s in
   if reducible_mind_case constr then s'
   else if isEvalRef env constr then
     let ref = destEvalRef constr in
     match reference_opt_value sigma env ref with
       | None -> raise Redelimination
-      | Some gvalue -> whd_construct_state env sigma (gvalue, cargs)
+      | Some gvalue -> whd_construct_stack env sigma (applist(gvalue, cargs))
   else
     raise Redelimination
 
@@ -818,23 +829,23 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
 
 let whd_simpl_orelse_delta_but_fix env sigma c =
   let rec redrec s =
-    let (constr, stack as s') = whd_simpl_state env sigma s in
+    let (constr, stack as s') = whd_simpl_stack env sigma s in
     if isEvalRef env constr then
       match reference_opt_value sigma env (destEvalRef constr) with
 	| Some c ->
 	    (match kind_of_term (strip_lam c) with
-              | CoFix _ | Fix _ -> s'
-	      | _ -> redrec (c, stack))
-	| None -> s'
+              | CoFix _ | Fix _ -> s,[]
+	      | _ -> redrec (applist(c, stack)))
+	| None -> s,[]
     else s'
-  in zip (redrec (c, empty_stack))
+  in applist (redrec c)
 
 let hnf_constr = whd_simpl_orelse_delta_but_fix
 
 (* The "simpl" reduction tactic *)
 
 let whd_simpl env sigma c =
-  zip (whd_simpl_state env sigma (c, empty_stack))
+  applist (whd_simpl_stack env sigma c)
 
 let simpl env sigma c = strong whd_simpl env sigma c
 
@@ -1030,19 +1041,19 @@ let one_step_reduce env sigma c =
   let rec redrec (x, stack) =
     match kind_of_term x with
       | Lambda (n,t,c)  ->
-          (match decomp_stack stack with
-             | None      -> raise NotStepReducible
-             | Some (a,rest) -> (subst1 a c, rest))
-      | App (f,cl) -> redrec (f, append_stack_app cl stack)
+          (match stack with
+             | []        -> raise NotStepReducible
+             | a :: rest -> (subst1 a c, rest))
+      | App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
       | LetIn (_,f,_,cl) -> (subst1 f cl,stack)
       | Cast (c,_,_) -> redrec (c,stack)
       | Case (ci,p,c,lf) ->
           (try
-	     (special_red_case env sigma (whd_simpl_state env sigma)
+	     (special_red_case env sigma (whd_simpl_stack env sigma)
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_state env) sigma fix stack with
+	  (match reduce_fix (whd_construct_stack env) sigma fix stack with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
       | _ when isEvalRef env x ->
@@ -1051,12 +1062,12 @@ let one_step_reduce env sigma c =
              red_elim_const env sigma ref stack
            with Redelimination ->
 	     match reference_opt_value sigma env ref with
-	       | Some d -> d, stack
+	       | Some d -> (d, stack)
 	       | None -> raise NotStepReducible)
 
       | _ -> raise NotStepReducible
   in
-  zip (redrec (c, empty_stack))
+  applist (redrec (c,[]))
 
 let isIndRef = function IndRef _ -> true | _ -> false