diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-31 11:51:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-31 11:51:38 +0200 |
commit | 8f04b4714f2a797b98be4d87866af3d93ecb78b6 (patch) | |
tree | 492e08d1f445fbc62476540dfbe1de4bdb01ea20 /lib | |
parent | 2c50427e59f932f26a8b643ea30c158c5deb432a (diff) | |
parent | bd3a48926a075296486c552ccef6b87e3fddd5e4 (diff) |
Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom implementation from Detyping.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cArray.ml | 3 | ||||
-rw-r--r-- | lib/cList.ml | 16 | ||||
-rw-r--r-- | lib/cList.mli | 5 |
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] *) |