source: extracted/vector.ml @ 2746

Last change on this file since 2746 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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