source: extracted/vector.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 8 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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_1761 = function
45| VEmpty -> h_VEmpty
46| VCons (n, x_1764, x_1763) ->
47  h_VCons n x_1764 x_1763 (vector_rect_Type4 h_VEmpty h_VCons n x_1763)
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_1773 = function
53| VEmpty -> h_VEmpty
54| VCons (n, x_1776, x_1775) ->
55  h_VCons n x_1776 x_1775 (vector_rect_Type3 h_VEmpty h_VCons n x_1775)
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_1779 = function
61| VEmpty -> h_VEmpty
62| VCons (n, x_1782, x_1781) ->
63  h_VCons n x_1782 x_1781 (vector_rect_Type2 h_VEmpty h_VCons n x_1781)
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_1785 = function
69| VEmpty -> h_VEmpty
70| VCons (n, x_1788, x_1787) ->
71  h_VCons n x_1788 x_1787 (vector_rect_Type1 h_VEmpty h_VCons n x_1787)
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_1791 = function
77| VEmpty -> h_VEmpty
78| VCons (n, x_1794, x_1793) ->
79  h_VCons n x_1794 x_1793 (vector_rect_Type0 h_VEmpty h_VCons n x_1793)
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.