39 | VCons of Nat.nat * 'a * 'a vector
41 (** val vector_rect_Type4 :
42 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
44 let rec vector_rect_Type4 h_VEmpty h_VCons x_1293 = function
46 | VCons (n, x_1296, x_1295) ->
47 h_VCons n x_1296 x_1295 (vector_rect_Type4 h_VEmpty h_VCons n x_1295)
49 (** val vector_rect_Type3 :
50 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
52 let rec vector_rect_Type3 h_VEmpty h_VCons x_1305 = function
54 | VCons (n, x_1308, x_1307) ->
55 h_VCons n x_1308 x_1307 (vector_rect_Type3 h_VEmpty h_VCons n x_1307)
57 (** val vector_rect_Type2 :
58 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
60 let rec vector_rect_Type2 h_VEmpty h_VCons x_1311 = function
62 | VCons (n, x_1314, x_1313) ->
63 h_VCons n x_1314 x_1313 (vector_rect_Type2 h_VEmpty h_VCons n x_1313)
65 (** val vector_rect_Type1 :
66 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
68 let rec vector_rect_Type1 h_VEmpty h_VCons x_1317 = function
70 | VCons (n, x_1320, x_1319) ->
71 h_VCons n x_1320 x_1319 (vector_rect_Type1 h_VEmpty h_VCons n x_1319)
73 (** val vector_rect_Type0 :
74 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
76 let rec vector_rect_Type0 h_VEmpty h_VCons x_1323 = function
78 | VCons (n, x_1326, x_1325) ->
79 h_VCons n x_1326 x_1325 (vector_rect_Type0 h_VEmpty h_VCons n x_1325)
81 (** val vector_inv_rect_Type4 :
82 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
83 vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
84 let vector_inv_rect_Type4 x2 hterm h1 h2 =
85 let hcut = vector_rect_Type4 h1 h2 x2 hterm in hcut __ __
87 (** val vector_inv_rect_Type3 :
88 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
89 vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
90 let vector_inv_rect_Type3 x2 hterm h1 h2 =
91 let hcut = vector_rect_Type3 h1 h2 x2 hterm in hcut __ __
93 (** val vector_inv_rect_Type2 :
94 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
95 vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
96 let vector_inv_rect_Type2 x2 hterm h1 h2 =
97 let hcut = vector_rect_Type2 h1 h2 x2 hterm in hcut __ __
99 (** val vector_inv_rect_Type1 :
100 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
101 vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
102 let vector_inv_rect_Type1 x2 hterm h1 h2 =
103 let hcut = vector_rect_Type1 h1 h2 x2 hterm in hcut __ __
105 (** val vector_inv_rect_Type0 :
106 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
107 vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
108 let vector_inv_rect_Type0 x2 hterm h1 h2 =
109 let hcut = vector_rect_Type0 h1 h2 x2 hterm in hcut __ __
111 (** val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
112 let vector_discr a2 x y =
113 Logic.eq_rect_Type2 x
115 | VEmpty -> Obj.magic (fun _ dH -> dH)
116 | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
118 (** val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
119 let vector_jmdiscr a2 x y =
120 Logic.eq_rect_Type2 x
122 | VEmpty -> Obj.magic (fun _ dH -> dH)
123 | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
125 (** val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 **)
126 let rec get_index_v n v m =
130 | VEmpty -> (fun _ -> assert false (* absurd case *))
131 | VCons (p, hd, tl) -> (fun _ -> hd))
134 | VEmpty -> (fun _ -> assert false (* absurd case *))
135 | VCons (p, hd, tl) -> (fun _ -> get_index_v p tl o))) __
137 (** val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 **)
138 let get_index' n m b =
139 get_index_v (Nat.S (Nat.plus n m)) b n
141 (** val get_index_weak_v :
142 Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option **)
143 let rec get_index_weak_v n v = function
146 | VEmpty -> Types.None
147 | VCons (p, hd, tl) -> Types.Some hd)
150 | VEmpty -> Types.None
151 | VCons (p, hd, tl) -> get_index_weak_v p tl o)
153 (** val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector **)
154 let rec set_index n v m a =
158 | VEmpty -> (fun _ -> VEmpty)
159 | VCons (p, hd, tl) -> (fun _ -> VCons (p, a, tl)))
162 | VEmpty -> (fun _ -> VEmpty)
163 | VCons (p, hd, tl) -> (fun _ -> VCons (p, hd, (set_index p tl o a)))))
166 (** val set_index_weak :
167 Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option **)
168 let rec set_index_weak n v m a =
172 | VEmpty -> Types.None
173 | VCons (o, hd, tl) -> Types.Some v)
176 | VEmpty -> Types.None
177 | VCons (p, hd, tl) ->
178 let settail = set_index_weak p tl o a in
180 | Types.None -> Types.None
181 | Types.Some j -> Types.Some v))
184 Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option **)
185 let rec drop n v = function
186 | Nat.O -> Types.Some v
189 | VEmpty -> Types.None
190 | VCons (p, hd, tl) -> Types.None)
192 (** val head' : Nat.nat -> 'a1 vector -> 'a1 **)
193 let head' n = function
194 | VEmpty -> Obj.magic __
195 | VCons (x, hd, x0) -> hd
197 (** val tail : Nat.nat -> 'a1 vector -> 'a1 vector **)
198 let tail n = function
199 | VEmpty -> Obj.magic __
200 | VCons (m, hd, tl) -> tl
203 Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
204 let rec vsplit' m n =
206 | Nat.O -> (fun v -> { Types.fst = VEmpty; Types.snd = v })
209 let { Types.fst = l; Types.snd = r } =
210 vsplit' m' n (tail (Nat.plus m' n) v)
212 { Types.fst = (VCons (m', (head' (Nat.plus m' n) v), l)); Types.snd =
216 Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
217 let rec vsplit m n v =
220 (** val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod **)
223 | VEmpty -> (fun _ -> assert false (* absurd case *))
224 | VCons (o, he, tl) -> (fun _ -> { Types.fst = he; Types.snd = tl })) __
226 (** val from_singl : 'a1 vector -> 'a1 **)
228 (head Nat.O v).Types.fst
231 Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
232 let rec fold_right n f x = function
234 | VCons (n0, hd, tl) -> f hd (fold_right n0 f x tl)
236 (** val fold_right_i :
237 Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
238 let rec fold_right_i n f x = function
240 | VCons (n0, hd, tl) -> f n0 hd (fold_right_i n0 f x tl)
242 (** val fold_right2_i :
243 (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
244 'a2 vector -> 'a3 **)
245 let rec fold_right2_i f c n v q =
249 | VEmpty -> (fun _ -> c)
250 | VCons (o, hd, tl) -> (fun _ -> assert false (* absurd case *)))
251 | VCons (o, hd, tl) ->
253 | VEmpty -> (fun _ -> assert false (* absurd case *))
254 | VCons (p, hd', tl') ->
255 (fun _ -> f o hd hd' (fold_right2_i f c o tl tl')))) __
258 Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 **)
259 let rec fold_left n f x = function
261 | VCons (n0, hd, tl) -> fold_left n0 f (f x hd) tl
263 (** val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
264 let rec map n f = function
266 | VCons (n0, hd, tl) -> VCons (n0, (f hd), (map n0 f tl))
269 Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector **)
270 let rec zip_with n f v q =
272 | VEmpty -> (fun _ -> VEmpty)
273 | VCons (n0, hd, tl) ->
275 | VEmpty -> (fun _ -> Obj.magic Nat.nat_discr (Nat.S n0) Nat.O __)
276 | VCons (m, hd', tl') ->
277 (fun _ -> VCons (n0, (f hd hd'),
278 (zip_with n0 f tl (Util.eq_rect_Type0_r m tl' n0)))))) __
281 Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector **)
283 zip_with n (fun x x0 -> { Types.fst = x; Types.snd = x0 }) v q
285 (** val replicate : Nat.nat -> 'a1 -> 'a1 vector **)
286 let rec replicate n h =
289 | Nat.S m -> VCons (m, h, (replicate m h))
292 Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
293 let rec append n m v q =
296 | VCons (o, hd, tl) -> VCons ((Nat.plus o m), hd, (append o m tl q))
299 Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector **)
300 let rec scan_left n f a v =
304 | VCons (o, hd, tl) -> scan_left o f (f a hd) tl))
307 Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list **)
308 let rec scan_right n f b = function
310 | VCons (o, hd, tl) -> List.Cons ((f hd b), (scan_right o f b tl))
313 Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
314 let rec revapp n m v acc =
317 | VCons (o, hd, tl) -> revapp o (Nat.S m) tl (VCons (m, hd, acc))
319 (** val reverse : Nat.nat -> 'a1 vector -> 'a1 vector **)
320 let rec reverse n v =
321 revapp n Nat.O v VEmpty
324 'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
325 let rec pad_vector a n m v =
328 | Nat.S n' -> VCons ((Nat.plus n' m), a, (pad_vector a n' m v))
330 (** val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list **)
331 let rec list_of_vector n = function
333 | VCons (o, hd, tl) -> List.Cons (hd, (list_of_vector o tl))
335 (** val vector_of_list : 'a1 List.list -> 'a1 vector **)
336 let rec vector_of_list = function
338 | List.Cons (hd, tl) -> VCons ((List.length tl), hd, (vector_of_list tl))
340 (** val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
341 let rec rotate_left n m v =
347 | VCons (p, hd, tl) ->
348 rotate_left (Nat.S p) o
349 (append p (Nat.S Nat.O) tl (VCons (Nat.O, hd, VEmpty))))
351 (** val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
352 let rotate_right n m v =
353 reverse n (rotate_left n m (reverse n v))
355 (** val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
356 let shift_left_1 n v a =
358 | VEmpty -> (fun _ -> assert false (* absurd case *))
359 | VCons (o, hd, tl) ->
360 (fun _ -> reverse (Nat.S o) (VCons (o, a, (reverse o tl))))) __
362 (** val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
363 let switch_bv_plus n m i =
366 (** val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
367 let shift_right_1 n v a =
368 let { Types.fst = v'; Types.snd = dropped } =
369 vsplit n (Nat.S Nat.O) (switch_bv_plus (Nat.S Nat.O) n v)
374 Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
376 match Extranat.nat_compare n m with
377 | Extranat.Nat_lt (x, x0) -> (fun v a -> replicate x a)
378 | Extranat.Nat_eq x -> (fun v a -> replicate x a)
379 | Extranat.Nat_gt (d, m0) ->
381 let { Types.fst = v0; Types.snd = v' } = vsplit m0 (Nat.S d) v in
382 switch_bv_plus (Nat.S d) m0 (append (Nat.S d) m0 v' (replicate m0 a)))
384 (** val shift_right :
385 Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
386 let shift_right n m v a =
387 Util.iterate (fun x -> shift_right_1 n x a) v m
390 Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
392 let rec eq_v n f b c =
397 | VEmpty -> Bool.True
398 | VCons (x, x0, x1) -> Obj.magic __ x x0 x1)
399 | VCons (m, hd, tl) ->
400 (fun c0 -> Bool.andb (f hd (head' m c0)) (eq_v m f tl (tail m c0)))) c
402 (** val vector_inv_n : Nat.nat -> 'a1 vector -> __ **)
403 let vector_inv_n n v =
405 | VEmpty -> (fun _ -> Obj.magic (fun auto -> auto))
406 | VCons (n0, auto, auto') ->
407 (fun _ -> Obj.magic (fun auto'' -> auto'' auto auto'))) __
410 ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ ->
411 __) -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__
413 let eq_v_elim f f_elim n x =
414 vector_rect_Type0 (fun y ->
415 Obj.magic vector_inv_n Nat.O y (fun auto auto' -> auto __))
417 Obj.magic vector_inv_n (Nat.S m) y (fun h' t' ht hf ->
418 Obj.magic f_elim __ h h' (fun _ ->
419 iH (tail m (VCons (m, h', t'))) (fun _ -> ht __) (fun _ -> hf __))
420 (fun _ -> hf __))) n x
423 ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool **)
425 fold_right n (fun y v -> Bool.orb (eq_a x y) v) Bool.False l
427 (** val subvector_with :
428 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
429 vector -> Bool.bool **)
430 let rec subvector_with n m eq sub sup =
432 | VEmpty -> Bool.True
433 | VCons (n', hd, tl) ->
434 (match mem eq m sup hd with
435 | Bool.True -> subvector_with n' m eq tl sup
436 | Bool.False -> Bool.False)
439 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
440 vector -> Bool.bool **)
441 let rec vprefix n m test v1 v2 =
443 | VEmpty -> Bool.True
444 | VCons (n', hd1, tl1) ->
446 | VEmpty -> Bool.False
447 | VCons (m', hd2, tl2) ->
448 Bool.andb (test hd1 hd2) (vprefix n' m' test tl1 tl2))
451 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
452 vector -> Bool.bool **)
453 let rec vsuffix n m test v1 v2 =
454 Util.if_then_else_safe (Nat.leb (Nat.S n) m) (fun _ ->
456 | VEmpty -> (fun _ -> assert false (* absurd case *))
457 | VCons (m', hd2, tl2) -> (fun _ -> vsuffix n m' test v1 tl2)) __)
459 match Nat.eqb n m with
460 | Bool.True -> vprefix n m test v1 v2
461 | Bool.False -> Bool.False)
463 (** val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector **)
464 let rec rvsplit n m =
466 | Nat.O -> (fun x -> VEmpty)
469 let { Types.fst = pre; Types.snd = post } = vsplit m (Nat.times k m) v
471 VCons (k, pre, (rvsplit k m post)))
473 (** val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector **)
474 let rec vflatten n m = function
476 | VCons (n', hd, tl) -> append m (Nat.times n' m) hd (vflatten n' m tl)