Déplacement du type stack de Reduction vers Closure et utilisation pour accélérer la réduction dans Closure

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

4 files changed, 238 insertions, 196 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 08b0cd065..e61f94939 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -412,10 +412,10 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
  *    (APP (l,(APP ...))) forbidden
  *)
 
-type stack =
+type cbv_stack =
   | TOP
-  | APP of cbv_value list * stack
-  | CASE of constr * constr array * case_info * cbv_value subs * stack
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
 (* Adds an application list. Collapse APPs! *)
 let stack_app appl stack =
@@ -717,6 +717,83 @@ let cbv_norm infos constr =
 
 (**** End of call by value ****)
 
+(**********************************************************************)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
+
+type 'a stack =
+  | EmptyStack
+  | ConsStack of 'a array * int * 'a stack
+
+let empty_stack = EmptyStack
+
+let decomp_stack = function
+  | EmptyStack -> None
+  | ConsStack (v, n, s) ->
+      Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s)))
+
+let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s)
+
+let rec app_stack = function
+  | f, EmptyStack -> f
+  | f, ConsStack (v, n, s) -> 
+      let args = if n=0 then v else Array.sub v n (Array.length v - n) in
+      app_stack (appvect (f, args), s)
+
+let rec list_of_stack = function
+  | EmptyStack -> []
+  | ConsStack (v, n, s) ->
+      let args = if n=0 then v else  Array.sub v n (Array.length v - n) in
+      Array.fold_right (fun a l -> a::l) args (list_of_stack s)
+
+let array_of_stack s =
+  let rec stackrec = function
+  | EmptyStack -> []
+  | ConsStack (v, n, s) ->
+      let args = if n=0 then v else  Array.sub v n (Array.length v - n) in
+      args :: (stackrec s)
+  in Array.concat (stackrec s)
+
+let rec stack_assign s p c = match s with
+  | EmptyStack -> EmptyStack
+  | ConsStack (v, n, s) ->
+      let q = Array.length v - n in 
+      if p >= q then
+	ConsStack (v, n, stack_assign s (p-q) c)
+      else
+	let v' = Array.sub v n q in
+	v'.(p) <- c;
+	ConsStack (v', 0, s)
+
+let rec stack_tail p s =
+  if p = 0 then s else
+    match s with
+      | EmptyStack -> failwith "stack_shop"
+      | ConsStack (v, n, s) ->
+	  let q = Array.length v - n in
+	  if p >= q then stack_tail (p-q) s
+	  else ConsStack (v, n+p, s)
+
+let rec stack_nth s p = match s with
+  | EmptyStack -> raise Not_found
+  | ConsStack (v, n, s) ->
+      let q = Array.length v - n in
+      if p >= q then stack_nth s (p-q)
+      else v.(p+n)
+
+let rec stack_args_size = function
+  | EmptyStack -> 0
+  | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s
+
+
+(* Version avec listes
+type stack = constr list
+
+let decomp_stack = function
+  | [] -> None
+  | v :: s -> Some (v,s)
+
+let append_stack v s = v@s
+*)
 
 (* Lazy reduction: the one used in kernel operations *)
 
@@ -999,11 +1076,12 @@ let rec strip_frterm n v stack =
   match v.term with
     | FLIFT (k,f) -> strip_frterm (k+n) f stack
     | FApp (f,args) ->
-        strip_frterm n f ((Array.map (lift_freeze n) args)::stack)
+        strip_frterm n f
+	  (append_stack (Array.map (lift_freeze n) args) stack)
     | FCast (f,_) -> (strip_frterm n f stack)
-    | _ -> (n, v, Array.concat stack)
+    | _ -> (n, v, stack)
 
-let strip_freeze v = strip_frterm 0 v []
+let strip_freeze v = strip_frterm 0 v empty_stack
 
 
 (* Same as contract_fixp, but producing a freeze *)
@@ -1038,9 +1116,9 @@ let copy_case ci p ft bl =
 
 (* Check if the case argument enables iota-reduction *)
 type case_status =
-  | CONSTRUCTOR of int * fconstr array
+  | CONSTRUCTOR of int * fconstr stack
   | COFIX of int * int * (fconstr array * name list * fconstr array) *
-      fconstr array * constr array * freeze subs
+      fconstr stack * constr array * freeze subs
   | IRREDUCTIBLE
 
 
@@ -1048,14 +1126,14 @@ let constr_or_cofix env v =
   let (lft_hd, head, appl) = strip_freeze v in
   match head.term with
     | FConstruct ((indsp,i),_) ->
-        let args = snd (array_chop (mindsp_nparams env indsp) appl) in
+        let args = stack_tail (mindsp_nparams env indsp) appl in
         CONSTRUCTOR (i, args)
     | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env)
     | _ -> IRREDUCTIBLE
 
-let fix_reducible env unf_fun n appl =
-  if n < Array.length appl & n >= 0 (* e.g for Acc_rec: n = -2 *) then
-    let v = unf_fun appl.(n) in
+let fix_reducible env unf_fun n stack =
+  if n < stack_args_size stack & n >= 0 (* e.g for Acc_rec: n = -2 *) then
+    let v = unf_fun (stack_nth stack n) in
     match constr_or_cofix env v with
       | CONSTRUCTOR _ -> true
       | _ -> false
@@ -1083,7 +1161,7 @@ and whnf_frterm info ft =
 	  let uf = unfreeze info f in
           { norm = uf.norm; term = FLIFT(k, uf) }
       | FCast (f,_) -> whnf_frterm info f  (* remove outer casts *)
-      | FApp (f,appl) -> whnf_apply info f appl
+      | FApp (f,appl) -> whnf_apply info f (append_stack appl empty_stack)
       | FFlex (FConst (sp,vars)) ->
 	  let cst = (sp, Array.map term_of_freeze vars) in
 	  if red_under info.i_flags (CONST [sp]) then
@@ -1152,23 +1230,27 @@ and whnf_frterm info ft =
       | FFix _ | FCoFix _ | FInd _ | FConstruct _ | FLambda _ | FProd _ -> ft
 
 (* Weak head reduction: case of the application (head appl) *)
-and whnf_apply info head appl =
+and whnf_apply info head stack =
   let head = unfreeze info head in
-  if Array.length appl = 0 then 
+  if stack = empty_stack then 
     head
   else
-    let (lft_hd,whd,args) = strip_frterm 0 head [appl] in
+    let (lft_hd,whd,lstack) = strip_frterm 0 head stack in
     match whd.term with
       | FLambda (_,_,_,t,subs) when red_under info.i_flags BETA ->
-          let vbody = contract_subst lft_hd t subs args.(0) in
-          whnf_apply info vbody (array_tl args)
+	  (match decomp_stack lstack with
+	     | Some (c, stack') ->
+		 let vbody = contract_subst lft_hd t subs c in
+		 whnf_apply info vbody stack'
+	     | None -> assert false)
       | FFix ((reci,bnum), _, _, _) as fx
           when red_under info.i_flags IOTA
             & fix_reducible info.i_env 
-	        (unfreeze (infos_under info)) reci.(bnum) args ->
+	        (unfreeze (infos_under info)) reci.(bnum) lstack ->
           let fix = contract_fix_vect fx in
-          whnf_apply info (lift_freeze lft_hd fix) args
-      | _ -> 
+          whnf_apply info (lift_freeze lft_hd fix) lstack
+      | _ ->
+	  let appl = array_of_stack stack in
 	  { norm = (is_val head) & (array_for_all is_val appl);
             term = FApp (head, appl) }
 	    
diff --git a/kernel/closure.mli b/kernel/closure.mli
index c38c6aaa0..8bb25554b 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -82,7 +82,97 @@ type 'a subs =
   | SHIFT of int * 'a subs
   | LIFT of int * 'a subs
 
-(*s Call by value functions *)
+(*s A [stack] is a context of arguments, arguments are pushed by
+   [append_stack] one array at a time but popped with [decomp_stack]
+   one by one *)
+
+type 'a stack
+val empty_stack : 'a stack
+val append_stack : 'a array -> 'a stack -> 'a stack
+val decomp_stack : 'a stack -> ('a * 'a stack) option
+val list_of_stack : 'a stack -> 'a list
+val array_of_stack : 'a stack -> 'a array
+val stack_assign : 'a stack -> int -> 'a -> 'a stack
+val stack_args_size : 'a stack -> int
+val app_stack : constr * constr stack -> constr
+val stack_tail : int -> 'a stack -> 'a stack
+val stack_nth : 'a stack -> int -> 'a
+
+(***********************************************************************)
+(*s Call-by-value reduction *)
+
+(* Entry point for cbv normalization of a constr *)
+type 'a cbv_infos
+val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
+val cbv_norm : 'a cbv_infos -> constr -> constr
+
+(*s Lazy reduction. *)
+
+(* [fconstr] is the type of frozen constr *)
+
+type fconstr
+
+(* [fconstr] can be accessed by using the function [frterm_of] and by
+   matching on type [frterm] *)
+
+type frterm =
+  | FRel of int
+  | FAtom of constr
+  | FCast of fconstr * fconstr
+  | FFlex of frreference
+  | FInd of inductive_path * fconstr array
+  | FConstruct of constructor_path * fconstr array
+  | FApp of fconstr * fconstr array
+  | FFix of (int array * int) * (fconstr array * name list * fconstr array)
+      * constr array * fconstr subs
+  | FCoFix of int * (fconstr array * name list * fconstr array)
+      * constr array * fconstr subs
+  | FCases of case_info * fconstr * fconstr * fconstr array
+  | FLambda of name * fconstr * fconstr * constr * fconstr subs
+  | FProd of name * fconstr * fconstr * constr * fconstr subs
+  | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs
+  | FLIFT of int * fconstr
+  | FFROZEN of constr * fconstr subs
+
+and frreference =
+  | FConst of section_path * fconstr array
+  | FEvar of (existential * fconstr subs)
+  | FVar of identifier
+  | FFarRel of int
+
+val frterm_of : fconstr -> frterm
+
+(* To lazy reduce a constr, create a ['a clos_infos] with
+   [create_cbv_infos], inject the term to reduce with [inject]; then use
+   a reduction function *)
+
+(* Global and local constant cache *)
+type 'a clos_infos
+val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
+val clos_infos_env : 'a clos_infos -> env
+
+val inject : constr -> fconstr
+
+(* Reduction function *)
+
+(* [norm_val] is for strong normalization *)
+val norm_val : 'a clos_infos -> fconstr -> constr
+
+(* [whd_val] is for weak head normalization *)
+val whd_val : 'a clos_infos -> fconstr -> constr
+
+(* [fhnf] and [fnf_apply] are for weak head normalization but staying
+   in [fcontr] world to perform step by step weak head normalization *)
+
+val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr stack
+val fhnf_apply : 'a clos_infos ->
+  int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack
+
+(* [search_frozen_value] unfolds references in a [fconstr] *)
+val search_frozen_value : 'a clos_infos -> frreference -> fconstr option
+
+
+(*i This is for cbv debug *)
 type cbv_value =
   | VAL of int * constr
   | LAM of name * constr * constr * cbv_value subs
@@ -92,75 +182,32 @@ type cbv_value =
 
 val shift_value : int -> cbv_value -> cbv_value
 
-(*i Private ??
-val contract_fixp : cbv_value subs -> fixpoint -> cbv_value subs * constr
-i*)
-
-type stack =
+type cbv_stack =
   | TOP
-  | APP of cbv_value list * stack
-  | CASE of constr * constr array * case_info * cbv_value subs * stack
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
-val stack_app : cbv_value list -> stack -> stack
-val under_case_stack : stack -> bool
-val strip_appl : cbv_value -> stack -> cbv_value * stack
+val stack_app : cbv_value list -> cbv_stack -> cbv_stack
+val under_case_stack : cbv_stack -> bool
+val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
-val red_allowed : flags -> stack -> red_kind -> bool
+val red_allowed : flags -> cbv_stack -> red_kind -> bool
 val reduce_const_body :
-  (cbv_value -> cbv_value) -> cbv_value -> stack -> cbv_value * stack
-(*i Private ??
-val fixp_reducible :
-  (cbv_value -> cbv_value) -> flags -> fixpoint -> stack -> bool
-i*)
-
-(* normalization of a constr: the two functions to know... *)
-type 'a cbv_infos
-val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
-val cbv_norm : 'a cbv_infos -> constr -> constr
+  (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
 (* recursive functions... *)
 val cbv_stack_term : 'a cbv_infos ->
-  stack -> cbv_value subs -> constr -> cbv_value
+  cbv_stack -> cbv_value subs -> constr -> cbv_value
 val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr
 val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
 val norm_head : 'a cbv_infos ->
-  cbv_value subs -> constr -> stack -> cbv_value * stack
-val apply_stack : 'a cbv_infos -> constr -> stack -> constr
+  cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
+val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr
 val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
+(* End of cbv debug section i*)
 
-
-(*s Lazy reduction. *)
-
-type freeze = { 
-  mutable norm: bool; 
-  mutable term: frterm }
-
-and frterm =
-  | FRel of int
-  | FAtom of constr
-  | FCast of freeze * freeze
-  | FFlex of frreference
-  | FInd of inductive_path * freeze array
-  | FConstruct of constructor_path * freeze array
-  | FApp of freeze * freeze array
-  | FFix of (int array * int) * (freeze array * name list * freeze array)
-      * constr array * freeze subs
-  | FCoFix of int * (freeze array * name list * freeze array)
-      * constr array * freeze subs
-  | FCases of case_info * freeze * freeze * freeze array
-  | FLambda of name * freeze * freeze * constr * freeze subs
-  | FProd of name * freeze * freeze * constr * freeze subs
-  | FLetIn of name * freeze * freeze * freeze * constr * freeze subs
-  | FLIFT of int * freeze
-  | FFROZEN of constr * freeze subs
-
-and frreference =
-  | FConst of section_path * freeze array
-  | FEvar of (existential * freeze subs)
-  | FVar of identifier
-  | FFarRel of int
-
-val frterm_of : freeze -> frterm
+(*i This is for lazy debug *)
+type freeze = fconstr
 val is_val : freeze -> bool
 
 val lift_frterm : int -> freeze -> freeze
@@ -181,44 +228,25 @@ val applist_of_freeze : freeze array -> constr list
 (* contract a substitution *)
 val contract_subst : int -> constr -> freeze subs -> freeze -> freeze
 
-(* Global and local constant cache *)
-type 'a clos_infos
-val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
-val clos_infos_env : 'a clos_infos -> env
-
-(* Calculus of Constructions *)
-type fconstr = freeze
-
-val inject : constr -> fconstr
-
 val strip_frterm :
-  int -> fconstr -> fconstr array list -> int * fconstr * fconstr array
-val strip_freeze : fconstr -> int * fconstr * fconstr array
-
+  int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack
+val strip_freeze : fconstr -> int * fconstr * fconstr stack
 
 (* Auxiliary functions for (co)fixpoint reduction *)
 val contract_fix_vect : frterm -> fconstr
 val copy_case : case_info -> fconstr -> fconstr -> fconstr array -> fconstr
 
-
 (* Iota analysis: reducible ? *)
 type case_status =
-  | CONSTRUCTOR of int * fconstr array
+  | CONSTRUCTOR of int * fconstr stack
   | COFIX of int * int * (fconstr array * name list * fconstr array) *
-      fconstr array * constr array * freeze subs
+      fconstr stack * constr array * freeze subs
   | IRREDUCTIBLE
 
-
-(* Reduction function *)
-val norm_val : 'a clos_infos -> fconstr -> constr
-val whd_val : 'a clos_infos -> fconstr -> constr
-val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr array
-val fhnf_apply : 'a clos_infos ->
-  int -> fconstr -> fconstr array -> int * fconstr * fconstr array
-val search_frozen_value : 'a clos_infos -> frreference -> fconstr option
-
 (* recursive functions... *)
 val unfreeze : 'a clos_infos -> fconstr -> fconstr
 val whnf_frterm : 'a clos_infos -> fconstr -> fconstr
 val whnf_term : 'a clos_infos -> fconstr subs -> constr -> fconstr
-val whnf_apply : 'a clos_infos -> fconstr -> fconstr array -> fconstr
+val whnf_apply : 'a clos_infos -> fconstr -> fconstr stack -> fconstr
+
+(* End of cbn debug section i*)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4df8de1a2..43a671536 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -14,13 +14,8 @@ open Closure
 
 exception Elimconst
 
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) 
-type stack =
-  | EmptyStack
-  | ConsStack of constr array * int * stack
-
 (* The type of (machine) states (= lambda-bar-calculus' cuts) *) 
-type state = constr * stack
+type state = constr * constr stack
 
 type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
 type 'a reduction_function = 'a contextual_reduction_function
@@ -36,61 +31,6 @@ type 'a contextual_state_reduction_function =
 type 'a state_reduction_function = 'a contextual_state_reduction_function
 type local_state_reduction_function = state -> state
 
-let empty_stack = EmptyStack
-
-let decomp_stack = function
-  | EmptyStack -> None
-  | ConsStack (v, n, s) ->
-      Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s)))
-
-let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s)
-
-let rec app_stack = function
-  | f, EmptyStack -> f
-  | f, ConsStack (v, n, s) -> 
-      let args = if n=0 then v else Array.sub v n (Array.length v - n) in
-      app_stack (appvect (f, args), s)
-
-let rec list_of_stack = function
-  | EmptyStack -> []
-  | ConsStack (v, n, s) ->
-      let args = if n=0 then v else  Array.sub v n (Array.length v - n) in
-      Array.fold_right (fun a l -> a::l) args (list_of_stack s)
-
-let appterm_of_stack (f,s) = (f,list_of_stack s)
-
-let rec stack_assign s p c = match s with
-  | EmptyStack -> EmptyStack
-  | ConsStack (v, n, s) ->
-      let q = Array.length v - n in 
-      if p >= q then
-	ConsStack (v, n, stack_assign s (p-q) c)
-      else
-	let v' = Array.sub v n q in
-	v'.(p) <- c;
-	ConsStack (v', 0, s)
-
-let rec stack_nth s p = match s with
-  | EmptyStack -> raise Not_found
-  | ConsStack (v, n, s) ->
-      let q = Array.length v - n in
-      if p >= q then stack_nth s (p-q)
-      else v.(p+n)
-
-let rec stack_args_size = function
-  | EmptyStack -> 0
-  | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s
-
-
-(* Version avec listes
-type stack = constr list
-
-let decomp_stack = function
-  | [] -> None
-  | v :: s -> Some (v,s)
-
-let append_stack v s = v@s
-*)
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
@@ -101,6 +41,8 @@ let rec whd_state (x, stack as s) =
     | IsCast (c,_)  -> whd_state (c, stack)
     | _             -> s
 
+let appterm_of_stack (f,s) = (f,list_of_stack s)
+
 let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
 let whd_castapp_stack = whd_stack
 
@@ -204,7 +146,7 @@ let rec stacklam recfun env t stack =
     | _ -> recfun (substl env t, stack)
 
 let beta_applist (c,l) =
-  stacklam app_stack [] c (append_stack (Array.of_list l) EmptyStack)
+  stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack)
 
 (* Iota reduction tools *)
 
@@ -734,6 +676,9 @@ let convert_forall2 f v1 v2 c =
   then array_fold_left2 (fun c x y -> f x y c) c v1 v2
   else raise NotConvertible
 
+let convert_stacks f v1 v2 c =
+  convert_forall2 f (array_of_stack v1) (array_of_stack v2) c
+
 (* Convertibility of sorts *)
 
 let sort_cmp pb s0 s1 =
@@ -771,15 +716,15 @@ and eqappr cv_pb infos appr1 appr2 =
 	(match kind_of_term a1, kind_of_term a2 with
 	   | (IsSort s1, IsSort s2) -> 
 	       bool_and_convert
-		 (Array.length v1 = 0 && Array.length v2 = 0)
+		 (stack_args_size v1 = 0 && stack_args_size v2 = 0)
 		 (sort_cmp cv_pb s1 s2)
 	   | (IsMeta n, IsMeta m) ->
                bool_and_convert (n=m) 
-		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		    v1 v2)
 	   | IsXtra s1, IsXtra s2 ->
                bool_and_convert (s1=s2)
-		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		    v1 v2)
 	   | _ -> fun _ -> raise NotConvertible)
 
@@ -787,14 +732,14 @@ and eqappr cv_pb infos appr1 appr2 =
     | (FRel n, FRel m) ->
         bool_and_convert 
           (reloc_rel n el1 = reloc_rel m el2)
-          (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+          (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
 	convert_or
 	  (* try first intensional equality *)
 	  (bool_and_convert (fl1 = fl2)
-	     (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
+	     (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (fun u ->
 	     match search_frozen_value infos fl2 with
@@ -820,7 +765,7 @@ and eqappr cv_pb infos appr1 appr2 =
     (* other constructors *)
     | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) ->
         bool_and_convert
-	  (Array.length v1 = 0 && Array.length v2 = 0)
+	  (stack_args_size v1 = 0 && stack_args_size v2 = 0)
           (convert_and
 	     (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1)
              (ccnv (pb_equal cv_pb) infos (el_lift el1) (el_lift el2) c2 c'2))
@@ -829,7 +774,7 @@ and eqappr cv_pb infos appr1 appr2 =
 
     | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) ->
 	bool_and_convert
-          (Array.length v1 = 0 && Array.length v2 = 0)
+          (stack_args_size v1 = 0 && stack_args_size v2 = 0)
 	  (convert_and
              (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (* Luo's system *)
              (ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2))
@@ -845,19 +790,19 @@ and eqappr cv_pb infos appr1 appr2 =
 	     (ccnv (pb_equal cv_pb) infos el1 el2 c1 c2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+		(convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 	     ))
 
      | (FInd (op1,cl1), FInd(op2,cl2)) ->
 	 bool_and_convert (op1 = op2)
 	   (convert_and
               (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-              (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
+              (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
      | (FConstruct (op1,cl1), FConstruct(op2,cl2)) ->
 	 bool_and_convert (op1 = op2)
 	   (convert_and
               (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-              (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
+              (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
      | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) ->
 	 let n = Array.length cl1 in
 	 bool_and_convert (op1 = op2)
@@ -867,7 +812,7 @@ and eqappr cv_pb infos appr1 appr2 =
 		 (convert_forall2 (ccnv (pb_equal cv_pb) infos 
 				     (el_liftn n el1) (el_liftn n el2))
 		    cl1 cl2)
-		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		    v1 v2)))
      | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) ->
 	 let n = Array.length cl1 in
@@ -878,7 +823,7 @@ and eqappr cv_pb infos appr1 appr2 =
 		 (convert_forall2 (ccnv (pb_equal cv_pb) infos
 				     (el_liftn n el1) (el_liftn n el2))
 		    cl1 cl2)
-		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		    v1 v2)))
 
      | _ -> (fun _ -> raise NotConvertible)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 7828ff940..600cdd823 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -14,20 +14,7 @@ open Closure
 
 exception Elimconst
 
-(*s A [stack] is a context of arguments, arguments are pushed by
-   [append_stack] one array at a time but popped with [decomp_stack]
-   one by one *)
-
-type stack
-val empty_stack : stack
-val append_stack : constr array -> stack -> stack
-val decomp_stack : stack -> (constr * stack) option
-val list_of_stack : stack -> constr list
-val stack_assign : stack -> int -> constr -> stack
-val stack_args_size : stack -> int
-val app_stack : constr * stack -> constr
-
-type state = constr * stack
+type state = constr * constr stack
 
 type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
 type 'a reduction_function = 'a contextual_reduction_function
@@ -58,7 +45,7 @@ val strong_prodspine : local_reduction_function -> local_reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a state_reduction_function
 i*)
-val stacklam : (state -> 'a) -> constr list -> constr -> stack -> 'a 
+val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a 
 
 (*s Generic Optimized Reduction Function using Closures *)
 
@@ -148,9 +135,9 @@ val whd_programs : 'a reduction_function
 
 type fix_reduction_result = NotReducible | Reduced of state
 
-val fix_recarg : fixpoint -> stack -> (int * constr) option
+val fix_recarg : fixpoint -> constr stack -> (int * constr) option
 val reduce_fix : local_state_reduction_function -> fixpoint
-   -> stack -> fix_reduction_result
+   -> constr stack -> fix_reduction_result
 
 (*s Conversion Functions (uses closures, lazy strategy) *)