9
9
| Length
10
10
| Get of int
11
11
| Set of int * char
12
- | Sub of int * int
13
12
| Copy
13
+ | To_string
14
+ | Sub of int * int
15
+ | Sub_string of int * int
14
16
| Fill of int * int * char
17
+ | Blit_string of string * int * int * int
18
+ | Index of char
19
+ | Index_opt of char
15
20
| To_seq
16
21
17
22
let pp_cmd par fmt x =
@@ -20,27 +25,46 @@ struct
20
25
| Length -> cst0 " Length" fmt
21
26
| Get x -> cst1 pp_int " Get" par fmt x
22
27
| Set (x , y ) -> cst2 pp_int pp_char " Set" par fmt x y
23
- | Sub (x , y ) -> cst2 pp_int pp_int " Sub" par fmt x y
24
28
| Copy -> cst0 " Copy" fmt
29
+ | To_string -> cst0 " To_string" fmt
30
+ | Sub (x , y ) -> cst2 pp_int pp_int " Sub" par fmt x y
31
+ | Sub_string (x , y ) -> cst2 pp_int pp_int " Sub_string" par fmt x y
25
32
| Fill (x , y , z ) -> cst3 pp_int pp_int pp_char " Fill" par fmt x y z
33
+ | Blit_string (x , y , z , w ) -> cst4 pp_string pp_int pp_int pp_int " Blit_string" par fmt x y z w
34
+ | Index x -> cst1 pp_char " Index" par fmt x
35
+ | Index_opt x -> cst1 pp_char " Index_opt" par fmt x
26
36
| To_seq -> cst0 " To_seq" fmt
27
37
28
38
let show_cmd = Util.Pp. to_show pp_cmd
29
39
30
40
type state = char list
31
41
type sut = Bytes .t
32
42
43
+ let shrink_char c = if c = 'a' then Iter. empty else Iter. return 'a' (* much faster than the default *)
44
+
45
+ let shrink_cmd c = match c with
46
+ | Blit_string (src ,spos ,dpos ,l ) ->
47
+ let open Iter in (* shrink spos int before src string *)
48
+ (Iter. map (fun spos -> Blit_string (src,spos,dpos,l)) (Shrink. int spos))
49
+ < +> (Iter. map (fun src -> Blit_string (src,spos,dpos,l)) (Shrink. string ~shrink: shrink_char src))
50
+ | _ -> Iter. empty
51
+
33
52
let arb_cmd s =
34
53
let int_gen = Gen. (oneof [small_nat; int_bound (List. length s - 1 )]) in
35
54
let char_gen = Gen. printable in
36
- QCheck. make ~print: show_cmd (* ~shrink:shrink_cmd*)
55
+ QCheck. make ~print: show_cmd ~shrink: shrink_cmd
37
56
Gen. (oneof
38
57
[ return Length ;
39
58
map (fun i -> Get i) int_gen;
40
59
map2 (fun i c -> Set (i,c)) int_gen char_gen;
41
- map2 (fun i len -> Sub (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *)
42
60
return Copy ;
61
+ return To_string ;
62
+ map2 (fun i len -> Sub (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *)
63
+ map2 (fun i len -> Sub_string (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *)
43
64
map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen char_gen; (* hack: reusing int_gen for length*)
65
+ map4 (fun src spos dpos l -> Blit_string (src,spos,dpos,l)) string_small int_gen int_gen int_gen; (* hack: reusing int_gen for length*)
66
+ map (fun c -> Index c) char_gen;
67
+ map (fun c -> Index_opt c) char_gen;
44
68
return To_seq ;
45
69
])
46
70
@@ -52,12 +76,21 @@ struct
52
76
| Length -> s
53
77
| Get _ -> s
54
78
| Set (i ,c ) -> List. mapi (fun j c' -> if i = j then c else c') s
55
- | Sub (_ ,_ ) -> s
56
79
| Copy -> s
80
+ | To_string -> s
81
+ | Sub (_ ,_ ) -> s
82
+ | Sub_string (_ ,_ ) -> s
57
83
| Fill (i ,l ,c ) ->
58
84
if i > = 0 && l > = 0 && i+ l-1 < (List. length s)
59
85
then List. mapi (fun j c' -> if i < = j && j < = i+ l-1 then c else c') s
60
86
else s
87
+ | Blit_string (src ,spos ,dpos ,l ) ->
88
+ if spos > = 0 && l > = 0 && spos+ l-1 < (String. length src)
89
+ && dpos > = 0 && dpos+ l-1 < (List. length s)
90
+ then List. mapi (fun j c' -> if dpos < = j && j < = dpos+ l-1 then src.[spos+ j- dpos] else c') s
91
+ else s
92
+ | Index _ -> s
93
+ | Index_opt _ -> s
61
94
| To_seq -> s
62
95
63
96
let init_sut () = Bytes. make byte_size 'a'
@@ -70,9 +103,14 @@ struct
70
103
| Length -> Res (int , Bytes. length b)
71
104
| Get i -> Res (result char exn , protect (Bytes. get b) i)
72
105
| Set (i ,c ) -> Res (result unit exn , protect (Bytes. set b i) c)
73
- | Sub (i ,l ) -> Res (result (bytes) exn , protect (Bytes. sub b i) l)
74
106
| Copy -> Res (bytes, Bytes. copy b)
107
+ | To_string -> Res (string , Bytes. to_string b)
108
+ | Sub (i ,l ) -> Res (result bytes exn , protect (Bytes. sub b i) l)
109
+ | Sub_string (i ,l ) -> Res (result string exn , protect (Bytes. sub_string b i) l)
75
110
| Fill (i ,l ,c ) -> Res (result unit exn , protect (Bytes. fill b i l) c)
111
+ | Blit_string (src ,spos ,dpos ,l ) -> Res (result unit exn , protect (Bytes. blit_string src spos b dpos) l)
112
+ | Index c -> Res (result int exn , protect (Bytes. index b) c)
113
+ | Index_opt c -> Res (option int , Bytes. index_opt b c)
76
114
| To_seq -> Res (seq char , List. to_seq (List. of_seq (Bytes. to_seq b)))
77
115
78
116
let postcond c (s : char list ) res = match c, res with
@@ -85,15 +123,30 @@ struct
85
123
if i < 0 || i > = List. length s
86
124
then r = Error (Invalid_argument " index out of bounds" )
87
125
else r = Ok ()
126
+ | Copy , Res ((Bytes,_ ),r ) -> r = Bytes. of_seq (List. to_seq s)
127
+ | To_string , Res ((String,_ ),r ) -> r = String. of_seq (List. to_seq s)
88
128
| Sub (i ,l ), Res ((Result (Bytes,Exn),_ ), r ) ->
89
129
if i < 0 || l < 0 || i+ l > List. length s
90
130
then r = Error (Invalid_argument " String.sub / Bytes.sub" )
91
131
else r = Ok (Bytes. of_seq (List. to_seq (List. filteri (fun j _ -> i < = j && j < = i+ l-1 ) s)))
92
- | Copy , Res ((Bytes,_ ),r ) -> r = Bytes. of_seq (List. to_seq s)
132
+ | Sub_string (i ,l ), Res ((Result (String,Exn),_ ), r ) ->
133
+ if i < 0 || l < 0 || i+ l > List. length s
134
+ then r = Error (Invalid_argument " String.sub / Bytes.sub" )
135
+ else r = Ok (String. of_seq (List. to_seq (List. filteri (fun j _ -> i < = j && j < = i+ l-1 ) s)))
93
136
| Fill (i ,l ,_ ), Res ((Result (Unit,Exn),_ ), r ) ->
94
137
if i < 0 || l < 0 || i+ l > List. length s
95
- then r = Error (Invalid_argument " String.fill / Bytes.fill" )
138
+ then r = Error (Invalid_argument " String.fill / Bytes.fill" )
139
+ else r = Ok ()
140
+ | Blit_string (src ,spos ,dpos ,l ), Res ((Result (Unit,Exn),_ ), r ) ->
141
+ if spos < 0 || dpos < 0 || l < 0 || spos+ l > String. length src || dpos+ l > List. length s
142
+ then r = Error (Invalid_argument " String.blit / Bytes.blit_string" )
96
143
else r = Ok ()
144
+ | Index c , Res ((Result (Int,Exn),_ ), r ) ->
145
+ (match List. find_index (fun c' -> c' = c) s with
146
+ | Some i -> r = Ok i
147
+ | None -> r = Error Not_found )
148
+ | Index_opt c , Res ((Option Int,_ ), r ) ->
149
+ r = List. find_index (fun c' -> c' = c) s
97
150
| To_seq , Res ((Seq Char,_ ),r ) -> Seq. equal (= ) r (List. to_seq s)
98
151
| _ , _ -> false
99
152
end
0 commit comments