Source file `BuiltinArray.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
(******************************************************************************)
(*                                                                            *)
(*                                  Monolith                                  *)
(*                                                                            *)
(*                              François Pottier                              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Lesser General Public License as published by the Free   *)
(*  Software Foundation, either version 3 of the License, or (at your         *)
(*  option) any later version, as described in the file LICENSE.              *)
(*                                                                            *)
(******************************************************************************)

open Spec

(* This file offers ready-made functions that help deal with arrays. *)

(* -------------------------------------------------------------------------- *)

(* Naive arrays. *)

(* This is the simplest way of dealing with arrays. At construction time, we
   always generate a fresh array; we never re-use an existing array that is at
   hand. At deconstruction time, the fact that an array is a mutable data
   structure is ignored; we eagerly convert the array to a list. By doing so,
   we verify that the content of the array is correct now; we do not test any
   property related to the identity of this array. *)

let constructible_array ~length spec =
  map_outof
    Array.of_list
    (Array.of_list, Code.constant "Array.of_list")
    (list ~length spec)

let deconstructible_array spec =
  map_into
    Array.to_list
    (Array.to_list, Code.constant "Array.to_list")
    (list spec)

let naive_array ?length:(length=Gen.lt 16) spec =
  ifpol
    (constructible_array ~length spec)
    (deconstructible_array spec)