From 2f1ee61f9700e3d73e637a82f9089807efab186a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Jul 2017 14:28:04 +0200
Subject: 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.
---
 pretyping/detyping.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f830d4be3f..98f6c24aa4 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
-- 
cgit v1.2.3


From 380dfe70ad9daf766e6acaf028e2c0cedc3be688 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Jul 2017 15:45:18 +0200
Subject: No useless reallocation in Termops.collapse_appl.

This function is suspicious, and reallocates a lot when it should be the
identity. This matters for detyping, where it is about the only place where
it is used.
---
 engine/termops.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/engine/termops.ml b/engine/termops.ml
index 1aba2bbdd1..4b7d600196 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -994,12 +994,14 @@ let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
 (* flattens application lists throwing casts in-between *)
 let collapse_appl sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
+    if EConstr.isCast sigma f then
       let rec collapse_rec f cl2 =
         match EConstr.kind sigma (strip_outer_cast sigma f) with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
         | _ -> EConstr.mkApp (f,cl2)
       in
       collapse_rec f cl
+    else c
   | _ -> c
 
 (* First utilities for avoiding telescope computation for subst_term *)
-- 
cgit v1.2.3


From d5ee6e2d24d0f9b42499b507fe9d03555c9ddf45 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 15:29:16 +0200
Subject: Add a comment regarding the specialization of the combinator in
 Detyping.

---
 pretyping/detyping.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 98f6c24aa4..ebd270e9f9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -694,6 +694,8 @@ 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)
 
+(** We use a dedicated function here to prevent overallocation from
+    Array.map_to_list. *)
 and detype_array flags avoid env sigma args =
   let ans = ref [] in
   for i = Array.length args - 1 downto 0 do
-- 
cgit v1.2.3