Allocation-friendly detyping of term arrays.

This is important for externalization big terms. We were indeed allocating
twice as much as needed lists for the application node case, as the
Array.map_to_list function is exactly List.map o Array.to_list.

We could probably tweak this function instead, at the expense that order of
evaluation is not guaranteed. I'm not willing to do that though.

1 files changed, 9 insertions, 2 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f830d4be3..98f6c24aa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -475,8 +475,8 @@ let rec detype flags avoid env sigma t = CAst.make @@
  	  GApp (f',args''@args')
  	| _ -> GApp (f',args')
       in
-	mkapp (detype flags avoid env sigma f)
-	  (Array.map_to_list (detype flags avoid env sigma) args)
+      mkapp (detype flags avoid env sigma f)
+        (detype_array flags avoid env sigma args)
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
@@ -694,6 +694,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
       let t = if s != InProp  && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
       GLetIn (na', c, t, r)
 
+and detype_array flags avoid env sigma args =
+  let ans = ref [] in
+  for i = Array.length args - 1 downto 0 do
+    ans := detype flags avoid env sigma args.(i) :: !ans;
+  done;
+  !ans
+
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function