source: driver/extracted/vector.ml @ 3106

Last change on this file since 3106 was 2775, checked in by sacerdot, 7 years ago

The compiler now computes also the stack cost model.

File size: 14.8 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Extranat
36
37type 'a vector =
38| VEmpty
39| VCons of Nat.nat * 'a * 'a vector
40
41(** val vector_rect_Type4 :
42    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
43    vector -> 'a2 **)
44let rec vector_rect_Type4 h_VEmpty h_VCons x_1293 = function
45| VEmpty -> h_VEmpty
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)
48
49(** val vector_rect_Type3 :
50    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
51    vector -> 'a2 **)
52let rec vector_rect_Type3 h_VEmpty h_VCons x_1305 = function
53| VEmpty -> h_VEmpty
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)
56
57(** val vector_rect_Type2 :
58    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
59    vector -> 'a2 **)
60let rec vector_rect_Type2 h_VEmpty h_VCons x_1311 = function
61| VEmpty -> h_VEmpty
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)
64
65(** val vector_rect_Type1 :
66    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
67    vector -> 'a2 **)
68let rec vector_rect_Type1 h_VEmpty h_VCons x_1317 = function
69| VEmpty -> h_VEmpty
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)
72
73(** val vector_rect_Type0 :
74    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
75    vector -> 'a2 **)
76let rec vector_rect_Type0 h_VEmpty h_VCons x_1323 = function
77| VEmpty -> h_VEmpty
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)
80
81(** val vector_inv_rect_Type4 :
82    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
83    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
84let vector_inv_rect_Type4 x2 hterm h1 h2 =
85  let hcut = vector_rect_Type4 h1 h2 x2 hterm in hcut __ __
86
87(** val vector_inv_rect_Type3 :
88    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
89    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
90let vector_inv_rect_Type3 x2 hterm h1 h2 =
91  let hcut = vector_rect_Type3 h1 h2 x2 hterm in hcut __ __
92
93(** val vector_inv_rect_Type2 :
94    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
95    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
96let vector_inv_rect_Type2 x2 hterm h1 h2 =
97  let hcut = vector_rect_Type2 h1 h2 x2 hterm in hcut __ __
98
99(** val vector_inv_rect_Type1 :
100    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
101    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
102let vector_inv_rect_Type1 x2 hterm h1 h2 =
103  let hcut = vector_rect_Type1 h1 h2 x2 hterm in hcut __ __
104
105(** val vector_inv_rect_Type0 :
106    Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1
107    vector -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2 **)
108let vector_inv_rect_Type0 x2 hterm h1 h2 =
109  let hcut = vector_rect_Type0 h1 h2 x2 hterm in hcut __ __
110
111(** val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
112let vector_discr a2 x y =
113  Logic.eq_rect_Type2 x
114    (match x with
115     | VEmpty -> Obj.magic (fun _ dH -> dH)
116     | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
117
118(** val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __ **)
119let vector_jmdiscr a2 x y =
120  Logic.eq_rect_Type2 x
121    (match x with
122     | VEmpty -> Obj.magic (fun _ dH -> dH)
123     | VCons (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)) y
124
125(** val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 **)
126let rec get_index_v n v m =
127  (match m with
128   | Nat.O ->
129     (match v with
130      | VEmpty -> (fun _ -> assert false (* absurd case *))
131      | VCons (p, hd, tl) -> (fun _ -> hd))
132   | Nat.S o ->
133     (match v with
134      | VEmpty -> (fun _ -> assert false (* absurd case *))
135      | VCons (p, hd, tl) -> (fun _ -> get_index_v p tl o))) __
136
137(** val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 **)
138let get_index' n m b =
139  get_index_v (Nat.S (Nat.plus n m)) b n
140
141(** val get_index_weak_v :
142    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option **)
143let rec get_index_weak_v n v = function
144| Nat.O ->
145  (match v with
146   | VEmpty -> Types.None
147   | VCons (p, hd, tl) -> Types.Some hd)
148| Nat.S o ->
149  (match v with
150   | VEmpty -> Types.None
151   | VCons (p, hd, tl) -> get_index_weak_v p tl o)
152
153(** val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector **)
154let rec set_index n v m a =
155  (match m with
156   | Nat.O ->
157     (match v with
158      | VEmpty -> (fun _ -> VEmpty)
159      | VCons (p, hd, tl) -> (fun _ -> VCons (p, a, tl)))
160   | Nat.S o ->
161     (match v with
162      | VEmpty -> (fun _ -> VEmpty)
163      | VCons (p, hd, tl) -> (fun _ -> VCons (p, hd, (set_index p tl o a)))))
164    __
165
166(** val set_index_weak :
167    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option **)
168let rec set_index_weak n v m a =
169  match m with
170  | Nat.O ->
171    (match v with
172     | VEmpty -> Types.None
173     | VCons (o, hd, tl) -> Types.Some v)
174  | Nat.S o ->
175    (match v with
176     | VEmpty -> Types.None
177     | VCons (p, hd, tl) ->
178       let settail = set_index_weak p tl o a in
179       (match settail with
180        | Types.None -> Types.None
181        | Types.Some j -> Types.Some v))
182
183(** val drop :
184    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option **)
185let rec drop n v = function
186| Nat.O -> Types.Some v
187| Nat.S o ->
188  (match v with
189   | VEmpty -> Types.None
190   | VCons (p, hd, tl) -> Types.None)
191
192(** val head' : Nat.nat -> 'a1 vector -> 'a1 **)
193let head' n = function
194| VEmpty -> Obj.magic __
195| VCons (x, hd, x0) -> hd
196
197(** val tail : Nat.nat -> 'a1 vector -> 'a1 vector **)
198let tail n = function
199| VEmpty -> Obj.magic __
200| VCons (m, hd, tl) -> tl
201
202(** val vsplit' :
203    Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
204let rec vsplit' m n =
205  match m with
206  | Nat.O -> (fun v -> { Types.fst = VEmpty; Types.snd = v })
207  | Nat.S m' ->
208    (fun v ->
209      let { Types.fst = l; Types.snd = r } =
210        vsplit' m' n (tail (Nat.plus m' n) v)
211      in
212      { Types.fst = (VCons (m', (head' (Nat.plus m' n) v), l)); Types.snd =
213      r })
214
215(** val vsplit :
216    Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod **)
217let rec vsplit m n v =
218  vsplit' m n v
219
220(** val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod **)
221let head n v =
222  (match v with
223   | VEmpty -> (fun _ -> assert false (* absurd case *))
224   | VCons (o, he, tl) -> (fun _ -> { Types.fst = he; Types.snd = tl })) __
225
226(** val from_singl : 'a1 vector -> 'a1 **)
227let from_singl v =
228  (head Nat.O v).Types.fst
229
230(** val fold_right :
231    Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
232let rec fold_right n f x = function
233| VEmpty -> x
234| VCons (n0, hd, tl) -> f hd (fold_right n0 f x tl)
235
236(** val fold_right_i :
237    Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2 **)
238let rec fold_right_i n f x = function
239| VEmpty -> x
240| VCons (n0, hd, tl) -> f n0 hd (fold_right_i n0 f x tl)
241
242(** val fold_right2_i :
243    (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
244    'a2 vector -> 'a3 **)
245let rec fold_right2_i f c n v q =
246  (match v with
247   | VEmpty ->
248     (match q with
249      | VEmpty -> (fun _ -> c)
250      | VCons (o, hd, tl) -> (fun _ -> assert false (* absurd case *)))
251   | VCons (o, hd, tl) ->
252     (match q with
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')))) __
256
257(** val fold_left :
258    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 **)
259let rec fold_left n f x = function
260| VEmpty -> x
261| VCons (n0, hd, tl) -> fold_left n0 f (f x hd) tl
262
263(** val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
264let rec map n f = function
265| VEmpty -> VEmpty
266| VCons (n0, hd, tl) -> VCons (n0, (f hd), (map n0 f tl))
267
268(** val zip_with :
269    Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector **)
270let rec zip_with n f v q =
271  (match v with
272   | VEmpty -> (fun _ -> VEmpty)
273   | VCons (n0, hd, tl) ->
274     (match q with
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)))))) __
279
280(** val zip :
281    Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector **)
282let zip n v q =
283  zip_with n (fun x x0 -> { Types.fst = x; Types.snd = x0 }) v q
284
285(** val replicate : Nat.nat -> 'a1 -> 'a1 vector **)
286let rec replicate n h =
287  match n with
288  | Nat.O -> VEmpty
289  | Nat.S m -> VCons (m, h, (replicate m h))
290
291(** val append :
292    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
293let rec append n m v q =
294  match v with
295  | VEmpty -> q
296  | VCons (o, hd, tl) -> VCons ((Nat.plus o m), hd, (append o m tl q))
297
298(** val scan_left :
299    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector **)
300let rec scan_left n f a v =
301  VCons (n, a,
302    (match v with
303     | VEmpty -> VEmpty
304     | VCons (o, hd, tl) -> scan_left o f (f a hd) tl))
305
306(** val scan_right :
307    Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list **)
308let rec scan_right n f b = function
309| VEmpty -> List.Nil
310| VCons (o, hd, tl) -> List.Cons ((f hd b), (scan_right o f b tl))
311
312(** val revapp :
313    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
314let rec revapp n m v acc =
315  match v with
316  | VEmpty -> acc
317  | VCons (o, hd, tl) -> revapp o (Nat.S m) tl (VCons (m, hd, acc))
318
319(** val reverse : Nat.nat -> 'a1 vector -> 'a1 vector **)
320let rec reverse n v =
321  revapp n Nat.O v VEmpty
322
323(** val pad_vector :
324    'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
325let rec pad_vector a n m v =
326  match n with
327  | Nat.O -> v
328  | Nat.S n' -> VCons ((Nat.plus n' m), a, (pad_vector a n' m v))
329
330(** val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list **)
331let rec list_of_vector n = function
332| VEmpty -> List.Nil
333| VCons (o, hd, tl) -> List.Cons (hd, (list_of_vector o tl))
334
335(** val vector_of_list : 'a1 List.list -> 'a1 vector **)
336let rec vector_of_list = function
337| List.Nil -> VEmpty
338| List.Cons (hd, tl) -> VCons ((List.length tl), hd, (vector_of_list tl))
339
340(** val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
341let rec rotate_left n m v =
342  match m with
343  | Nat.O -> v
344  | Nat.S o ->
345    (match v with
346     | VEmpty -> VEmpty
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))))
350
351(** val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
352let rotate_right n m v =
353  reverse n (rotate_left n m (reverse n v))
354
355(** val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
356let shift_left_1 n v a =
357  (match v with
358   | VEmpty -> (fun _ -> assert false (* absurd case *))
359   | VCons (o, hd, tl) ->
360     (fun _ -> reverse (Nat.S o) (VCons (o, a, (reverse o tl))))) __
361
362(** val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
363let switch_bv_plus n m i =
364  i
365
366(** val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
367let 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)
370  in
371  VCons (n, a, v')
372
373(** val shift_left :
374    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
375let shift_left n m =
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) ->
380    (fun v a ->
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)))
383
384(** val shift_right :
385    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
386let shift_right n m v a =
387  Util.iterate (fun x -> shift_right_1 n x a) v m
388
389(** val eq_v :
390    Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
391    Bool.bool **)
392let rec eq_v n f b c =
393  (match b with
394   | VEmpty ->
395     (fun c0 ->
396       match c0 with
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
401
402(** val vector_inv_n : Nat.nat -> 'a1 vector -> __ **)
403let vector_inv_n n v =
404  (match v with
405   | VEmpty -> (fun _ -> Obj.magic (fun auto -> auto))
406   | VCons (n0, auto, auto') ->
407     (fun _ -> Obj.magic (fun auto'' -> auto'' auto auto'))) __
408
409(** val eq_v_elim :
410    ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ ->
411    __) -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__
412    -> 'a1) -> 'a1 **)
413let 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 __))
416    (fun m h t iH y ->
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
421
422(** val mem :
423    ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool **)
424let mem eq_a n l x =
425  fold_right n (fun y v -> Bool.orb (eq_a x y) v) Bool.False l
426
427(** val subvector_with :
428    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
429    vector -> Bool.bool **)
430let rec subvector_with n m eq sub sup =
431  match sub with
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)
437
438(** val vprefix :
439    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
440    vector -> Bool.bool **)
441let rec vprefix n m test v1 v2 =
442  match v1 with
443  | VEmpty -> Bool.True
444  | VCons (n', hd1, tl1) ->
445    (match v2 with
446     | VEmpty -> Bool.False
447     | VCons (m', hd2, tl2) ->
448       Bool.andb (test hd1 hd2) (vprefix n' m' test tl1 tl2))
449
450(** val vsuffix :
451    Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1
452    vector -> Bool.bool **)
453let rec vsuffix n m test v1 v2 =
454  Util.if_then_else_safe (Nat.leb (Nat.S n) m) (fun _ ->
455    (match v2 with
456     | VEmpty -> (fun _ -> assert false (* absurd case *))
457     | VCons (m', hd2, tl2) -> (fun _ -> vsuffix n m' test v1 tl2)) __)
458    (fun _ ->
459    match Nat.eqb n m with
460    | Bool.True -> vprefix n m test v1 v2
461    | Bool.False -> Bool.False)
462
463(** val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector **)
464let rec rvsplit n m =
465  match n with
466  | Nat.O -> (fun x -> VEmpty)
467  | Nat.S k ->
468    (fun v ->
469      let { Types.fst = pre; Types.snd = post } = vsplit m (Nat.times k m) v
470      in
471      VCons (k, pre, (rvsplit k m post)))
472
473(** val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector **)
474let rec vflatten n m = function
475| VEmpty -> VEmpty
476| VCons (n', hd, tl) -> append m (Nat.times n' m) hd (vflatten n' m tl)
477
Note: See TracBrowser for help on using the repository browser.