Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom implementation from Detyping.

3 files changed, 21 insertions, 3 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index bb1e33546..85984d436 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 c8283e3c7..cb84b6097 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 bc8749b4f..d7d6614cd 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] *)