Stop back-and-forth array to list conversions in simpl.

1 files changed, 36 insertions, 28 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index baa32565f6..396d780161 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -574,6 +574,11 @@ let match_eval_ref_value env sigma constr stack =
      env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
   | _ -> None
 
+let push_app sigma (hd, stk as p) = match EConstr.kind sigma hd with
+| App (hd, args) ->
+  (hd, Array.fold_right (fun x accu -> x :: accu) args stk)
+| _ -> p
+
 let special_red_case env sigma whfun (ci, p, iv, c, lf) =
   let rec redrec s =
     let (constr, cargs) = whfun s in
@@ -587,7 +592,7 @@ let special_red_case env sigma whfun (ci, p, iv, c, lf) =
           {mP=p; mconstr=gvalue; mcargs=cargs;
            mci=ci; mlf=lf}
         else
-          redrec (applist(gvalue, cargs)))
+          redrec (gvalue, cargs))
     | None ->
       if reducible_mind_case sigma constr then
         reduce_mind_case sigma
@@ -596,7 +601,7 @@ let special_red_case env sigma whfun (ci, p, iv, c, lf) =
       else
         raise Redelimination
   in
-  redrec c
+  redrec (push_app sigma (c, []))
 
 let recargs = function
   | EvalVar _ | EvalRel _ | EvalEvar _ -> None
@@ -628,6 +633,10 @@ let reduce_proj env sigma whfun whfun' c =
     | _ -> raise Redelimination
   in redrec c
 
+let rec beta_applist sigma accu c stk = match EConstr.kind sigma c, stk with
+| Lambda (_, _, c), arg :: stk -> beta_applist sigma (arg :: accu) c stk
+| _ -> substl accu c, stk
+
 let whd_nothing_for_iota env sigma s =
   let rec whrec (x, stack as s) =
     match EConstr.kind sigma x with
@@ -650,17 +659,17 @@ let whd_nothing_for_iota env sigma s =
           (match constant_opt_value_in env (const, u) with
              | Some  body -> whrec (EConstr.of_constr body, stack)
              | None -> s)
-      | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack
+      | LetIn (_,b,_,c) -> whrec (beta_applist sigma [b] c stack)
       | Cast (c,_,_) -> whrec (c, stack)
-      | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
+      | App (f,cl)  -> whrec (f, Array.fold_right (fun c accu -> c :: accu) cl stack)
       | Lambda (na,t,c) ->
-          (match Stack.decomp stack with
-             | Some (a,m) -> stacklam whrec [a] sigma c m
+          (match stack with
+             | a :: stack -> whrec (beta_applist sigma [a] c stack)
              | _ -> s)
 
       | x -> s
   in
-  EConstr.decompose_app sigma (Stack.zip sigma (whrec (s,Stack.empty)))
+  whrec s
 
 (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
    constants by keeping the name of the constants in the recursive calls;
@@ -703,18 +712,18 @@ let rec red_elim_const env sigma ref u largs =
   try match reference_eval env sigma ref with
     | EliminationCases n when nargs >= n ->
         let c = reference_value env sigma ref u in
-        let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
+        let c', lrest = whd_nothing_for_iota env sigma (c, largs) in
         let whfun = whd_simpl_stack env sigma in
         (special_red_case env sigma whfun (EConstr.destCase sigma c'), lrest), nocase
     | EliminationProj n when nargs >= n ->
         let c = reference_value env sigma ref u in
-        let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
+        let c', lrest = whd_nothing_for_iota env sigma (c, largs) in
         let whfun = whd_construct_stack env sigma in
         let whfun' = whd_simpl_stack env sigma in
           (reduce_proj env sigma whfun whfun' c', lrest), nocase
     | EliminationFix (min,minfxargs,infos) when nargs >= min ->
         let c = reference_value env sigma ref u in
-        let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
+        let d, lrest = whd_nothing_for_iota env sigma (c, largs) in
         let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in
         let whfun = whd_construct_stack env sigma in
         (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
@@ -729,7 +738,7 @@ let rec red_elim_const env sigma ref u largs =
             let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in
             descend (destEvalRefU sigma c') lrest in
         let (_, midargs as s) = descend (ref,u) largs in
-        let d, lrest = whd_nothing_for_iota env sigma (applist s) in
+        let d, lrest = whd_nothing_for_iota env sigma s in
         let f = make_elim_fun refinfos u midargs in
         let whfun = whd_construct_stack env sigma in
         (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
@@ -762,25 +771,24 @@ and reduce_params env sigma stack l =
 and whd_simpl_stack env sigma =
   let open ReductionBehaviour in
   let rec redrec s =
-    let (x, stack) = decompose_app_vect sigma s in
-    let stack = Array.to_list stack in
-    let s' = (x, stack) in
+    let s' = push_app sigma s in
+    let (x, stack) = s' in
     match EConstr.kind sigma x with
       | Lambda (na,t,c) ->
           (match stack with
              | [] -> s'
-             | a :: rest -> redrec (beta_applist sigma (x, stack)))
-      | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
-      | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
-      | Cast (c,_,_) -> redrec (applist(c, stack))
+             | a :: rest -> redrec (beta_applist sigma [a] c rest))
+      | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack)
+      | App (f,cl) -> assert false (* see push_app above *)
+      | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,iv,c,lf) ->
           (try
-            redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack))
+            redrec (special_red_case env sigma redrec (ci,p,iv,c,lf), stack)
           with
               Redelimination -> s')
       | Fix fix ->
           (try match reduce_fix (whd_construct_stack env) sigma fix stack with
-            | Reduced s' -> redrec (applist s')
+            | Reduced s' -> redrec s'
             | NotReducible -> s'
           with Redelimination -> s')
 
@@ -800,11 +808,11 @@ and whd_simpl_stack env sigma =
                 (match reduce_projection env sigma p ~npars
                          (whd_construct_stack env sigma c) stack
                  with
-                 | Reduced s' -> redrec (applist s')
+                 | Reduced s' -> redrec s'
                  | NotReducible -> s')
               | _ ->
                 match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
-                | Reduced s' -> redrec (applist s')
+                | Reduced s' -> redrec s'
                             | NotReducible -> s')
                  else s'
                with Redelimination -> s')
@@ -814,7 +822,7 @@ and whd_simpl_stack env sigma =
         | Some (ref, u) ->
           (try
              let sapp, nocase = red_elim_const env sigma ref u stack in
-             let hd, _ as s'' = redrec (applist(sapp)) in
+             let hd, _ as s'' = redrec sapp in
              let rec is_case x = match EConstr.kind sigma x with
                | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
                | App (hd, _) -> is_case hd
@@ -830,7 +838,7 @@ and whd_simpl_stack env sigma =
 (* reduce until finding an applied constructor or fail *)
 
 and whd_construct_stack env sigma s =
-  let (constr, cargs as s') = whd_simpl_stack env sigma s in
+  let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in
   if reducible_mind_case sigma constr then s'
   else match match_eval_ref env sigma constr cargs with
   | Some (ref, u) ->
@@ -973,19 +981,19 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
           if List.length stack <= npars then
             (* Do not show the eta-expanded form *)
             s'
-          else redrec (applist (c, stack))
-      | _ -> redrec (applist(c, stack)))
+          else redrec (c, stack)
+      | _ -> redrec (c, stack))
     | None -> s'
   in
   let simpfun = clos_norm_flags betaiota env sigma in
   simpfun (applist (redrec c))
 
-let hnf_constr = whd_simpl_orelse_delta_but_fix
+let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
 
 (* The "simpl" reduction tactic *)
 
 let whd_simpl env sigma c =
-  applist (whd_simpl_stack env sigma c)
+  applist (whd_simpl_stack env sigma (c, []))
 
 let simpl env sigma c = strong whd_simpl env sigma c