Prevent overallocation in Array.map_to_list and remove custom implementation from Detyping.

4 files changed, 22 insertions, 13 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index bb1e335468..85984d4362 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -283,8 +283,7 @@ let rev_of_list = function
   let () = set (len - 1) l in
   ans
 
-let map_to_list f v =
-  List.map f (Array.to_list v)
+let map_to_list = CList.map_of_array
 
 let map_of_list f l =
   let len = List.length l in
diff --git a/lib/cList.ml b/lib/cList.ml
index c8283e3c71..cb84b6097f 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -49,6 +49,7 @@ sig
     (int -> 'a -> bool) -> 'a list -> 'a list
   val partitioni :
     (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+  val map_of_array : ('a -> 'b) -> 'a array -> 'b list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
@@ -159,6 +160,21 @@ let map2 f l1 l2 = match l1, l2 with
   cast c
 | _ -> invalid_arg "List.map2"
 
+let rec map_of_array_loop f p a i l =
+  if Int.equal i l then ()
+  else
+    let c = { head = f (Array.unsafe_get a i); tail = [] } in
+    p.tail <- cast c;
+    map_of_array_loop f c a (i + 1) l
+
+let map_of_array f a =
+  let l = Array.length a in
+  if Int.equal l 0 then []
+  else
+    let c = { head = f (Array.unsafe_get a 0); tail = [] } in
+    map_of_array_loop f c a 1 l;
+    cast c
+
 let rec append_loop p tl = function
 | [] -> p.tail <- tl
 | x :: l ->
diff --git a/lib/cList.mli b/lib/cList.mli
index bc8749b4f8..d7d6614cd3 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -53,7 +53,7 @@ sig
       [Invalid_argument "List.make"] if [n] is negative. *)
 
   val assign : 'a list -> int -> 'a -> 'a list
-  (** [assign l i x] set the [i]-th element of [l] to [x], starting from [0]. *)
+  (** [assign l i x] sets the [i]-th element of [l] to [x], starting from [0]. *)
 
   val distinct : 'a list -> bool
   (** Return [true] if all elements of the list are distinct. *)
@@ -91,6 +91,9 @@ sig
   val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
   val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
 
+  val map_of_array : ('a -> 'b) -> 'a array -> 'b list
+  (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
+
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == l] *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a27debe735..b9cb7ba1b1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -476,7 +476,7 @@ let rec detype flags avoid env sigma t = CAst.make @@
  	| _ -> GApp (f',args')
       in
       mkapp (detype flags avoid env sigma f)
-        (detype_array flags avoid env sigma args)
+        (Array.map_to_list (detype flags avoid env sigma) args)
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
@@ -694,15 +694,6 @@ 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
-    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