source: extracted/types.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.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11type void = unit (* empty inductive *)
12
13(** val void_rect_Type4 : void -> 'a1 **)
14let rec void_rect_Type4 x_327 =
15  assert false (* absurd case *)
16
17(** val void_rect_Type5 : void -> 'a1 **)
18let rec void_rect_Type5 x_328 =
19  assert false (* absurd case *)
20
21(** val void_rect_Type3 : void -> 'a1 **)
22let rec void_rect_Type3 x_329 =
23  assert false (* absurd case *)
24
25(** val void_rect_Type2 : void -> 'a1 **)
26let rec void_rect_Type2 x_330 =
27  assert false (* absurd case *)
28
29(** val void_rect_Type1 : void -> 'a1 **)
30let rec void_rect_Type1 x_331 =
31  assert false (* absurd case *)
32
33(** val void_rect_Type0 : void -> 'a1 **)
34let rec void_rect_Type0 x_332 =
35  assert false (* absurd case *)
36
37type unit0 =
38| It
39
40(** val unit_rect_Type4 : 'a1 -> unit0 -> 'a1 **)
41let rec unit_rect_Type4 h_it = function
42| It -> h_it
43
44(** val unit_rect_Type5 : 'a1 -> unit0 -> 'a1 **)
45let rec unit_rect_Type5 h_it = function
46| It -> h_it
47
48(** val unit_rect_Type3 : 'a1 -> unit0 -> 'a1 **)
49let rec unit_rect_Type3 h_it = function
50| It -> h_it
51
52(** val unit_rect_Type2 : 'a1 -> unit0 -> 'a1 **)
53let rec unit_rect_Type2 h_it = function
54| It -> h_it
55
56(** val unit_rect_Type1 : 'a1 -> unit0 -> 'a1 **)
57let rec unit_rect_Type1 h_it = function
58| It -> h_it
59
60(** val unit_rect_Type0 : 'a1 -> unit0 -> 'a1 **)
61let rec unit_rect_Type0 h_it = function
62| It -> h_it
63
64(** val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1 **)
65let unit_inv_rect_Type4 hterm h1 =
66  let hcut = unit_rect_Type4 h1 hterm in hcut __
67
68(** val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1 **)
69let unit_inv_rect_Type3 hterm h1 =
70  let hcut = unit_rect_Type3 h1 hterm in hcut __
71
72(** val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1 **)
73let unit_inv_rect_Type2 hterm h1 =
74  let hcut = unit_rect_Type2 h1 hterm in hcut __
75
76(** val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1 **)
77let unit_inv_rect_Type1 hterm h1 =
78  let hcut = unit_rect_Type1 h1 hterm in hcut __
79
80(** val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1 **)
81let unit_inv_rect_Type0 hterm h1 =
82  let hcut = unit_rect_Type0 h1 hterm in hcut __
83
84(** val unit_discr : unit0 -> unit0 -> __ **)
85let unit_discr x y =
86  Logic.eq_rect_Type2 x (let It = x in Obj.magic (fun _ dH -> dH)) y
87
88type ('a, 'b) sum =
89| Inl of 'a
90| Inr of 'b
91
92(** val sum_rect_Type4 :
93    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
94let rec sum_rect_Type4 h_inl h_inr = function
95| Inl x_371 -> h_inl x_371
96| Inr x_372 -> h_inr x_372
97
98(** val sum_rect_Type5 :
99    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
100let rec sum_rect_Type5 h_inl h_inr = function
101| Inl x_376 -> h_inl x_376
102| Inr x_377 -> h_inr x_377
103
104(** val sum_rect_Type3 :
105    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
106let rec sum_rect_Type3 h_inl h_inr = function
107| Inl x_381 -> h_inl x_381
108| Inr x_382 -> h_inr x_382
109
110(** val sum_rect_Type2 :
111    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
112let rec sum_rect_Type2 h_inl h_inr = function
113| Inl x_386 -> h_inl x_386
114| Inr x_387 -> h_inr x_387
115
116(** val sum_rect_Type1 :
117    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
118let rec sum_rect_Type1 h_inl h_inr = function
119| Inl x_391 -> h_inl x_391
120| Inr x_392 -> h_inr x_392
121
122(** val sum_rect_Type0 :
123    ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
124let rec sum_rect_Type0 h_inl h_inr = function
125| Inl x_396 -> h_inl x_396
126| Inr x_397 -> h_inr x_397
127
128(** val sum_inv_rect_Type4 :
129    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
130let sum_inv_rect_Type4 hterm h1 h2 =
131  let hcut = sum_rect_Type4 h1 h2 hterm in hcut __
132
133(** val sum_inv_rect_Type3 :
134    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
135let sum_inv_rect_Type3 hterm h1 h2 =
136  let hcut = sum_rect_Type3 h1 h2 hterm in hcut __
137
138(** val sum_inv_rect_Type2 :
139    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
140let sum_inv_rect_Type2 hterm h1 h2 =
141  let hcut = sum_rect_Type2 h1 h2 hterm in hcut __
142
143(** val sum_inv_rect_Type1 :
144    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
145let sum_inv_rect_Type1 hterm h1 h2 =
146  let hcut = sum_rect_Type1 h1 h2 hterm in hcut __
147
148(** val sum_inv_rect_Type0 :
149    ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
150let sum_inv_rect_Type0 hterm h1 h2 =
151  let hcut = sum_rect_Type0 h1 h2 hterm in hcut __
152
153(** val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __ **)
154let sum_discr x y =
155  Logic.eq_rect_Type2 x
156    (match x with
157     | Inl a0 -> Obj.magic (fun _ dH -> dH __)
158     | Inr a0 -> Obj.magic (fun _ dH -> dH __)) y
159
160type 'a option =
161| None
162| Some of 'a
163
164(** val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
165let rec option_rect_Type4 h_None h_Some = function
166| None -> h_None
167| Some x_435 -> h_Some x_435
168
169(** val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
170let rec option_rect_Type5 h_None h_Some = function
171| None -> h_None
172| Some x_439 -> h_Some x_439
173
174(** val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
175let rec option_rect_Type3 h_None h_Some = function
176| None -> h_None
177| Some x_443 -> h_Some x_443
178
179(** val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
180let rec option_rect_Type2 h_None h_Some = function
181| None -> h_None
182| Some x_447 -> h_Some x_447
183
184(** val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
185let rec option_rect_Type1 h_None h_Some = function
186| None -> h_None
187| Some x_451 -> h_Some x_451
188
189(** val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
190let rec option_rect_Type0 h_None h_Some = function
191| None -> h_None
192| Some x_455 -> h_Some x_455
193
194(** val option_inv_rect_Type4 :
195    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
196let option_inv_rect_Type4 hterm h1 h2 =
197  let hcut = option_rect_Type4 h1 h2 hterm in hcut __
198
199(** val option_inv_rect_Type3 :
200    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
201let option_inv_rect_Type3 hterm h1 h2 =
202  let hcut = option_rect_Type3 h1 h2 hterm in hcut __
203
204(** val option_inv_rect_Type2 :
205    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
206let option_inv_rect_Type2 hterm h1 h2 =
207  let hcut = option_rect_Type2 h1 h2 hterm in hcut __
208
209(** val option_inv_rect_Type1 :
210    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
211let option_inv_rect_Type1 hterm h1 h2 =
212  let hcut = option_rect_Type1 h1 h2 hterm in hcut __
213
214(** val option_inv_rect_Type0 :
215    'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
216let option_inv_rect_Type0 hterm h1 h2 =
217  let hcut = option_rect_Type0 h1 h2 hterm in hcut __
218
219(** val option_discr : 'a1 option -> 'a1 option -> __ **)
220let option_discr x y =
221  Logic.eq_rect_Type2 x
222    (match x with
223     | None -> Obj.magic (fun _ dH -> dH)
224     | Some a0 -> Obj.magic (fun _ dH -> dH __)) y
225
226(** val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option **)
227let option_map f = function
228| None -> None
229| Some a -> Some (f a)
230
231(** val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2 **)
232let option_map_def f d = function
233| None -> d
234| Some a -> f a
235
236(** val refute_none_by_refl :
237    ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3 **)
238let refute_none_by_refl p clearme x =
239  (match clearme with
240   | None -> (fun _ -> assert false (* absurd case *))
241   | Some a -> (fun _ p0 -> p0 a __)) __ x
242
243type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
244
245(** val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
246let rec dPair_rect_Type4 h_mk_DPair x_484 =
247  let { dpi1 = dpi3; dpi2 = dpi4 } = x_484 in h_mk_DPair dpi3 dpi4
248
249(** val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
250let rec dPair_rect_Type5 h_mk_DPair x_486 =
251  let { dpi1 = dpi3; dpi2 = dpi4 } = x_486 in h_mk_DPair dpi3 dpi4
252
253(** val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
254let rec dPair_rect_Type3 h_mk_DPair x_488 =
255  let { dpi1 = dpi3; dpi2 = dpi4 } = x_488 in h_mk_DPair dpi3 dpi4
256
257(** val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
258let rec dPair_rect_Type2 h_mk_DPair x_490 =
259  let { dpi1 = dpi3; dpi2 = dpi4 } = x_490 in h_mk_DPair dpi3 dpi4
260
261(** val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
262let rec dPair_rect_Type1 h_mk_DPair x_492 =
263  let { dpi1 = dpi3; dpi2 = dpi4 } = x_492 in h_mk_DPair dpi3 dpi4
264
265(** val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
266let rec dPair_rect_Type0 h_mk_DPair x_494 =
267  let { dpi1 = dpi3; dpi2 = dpi4 } = x_494 in h_mk_DPair dpi3 dpi4
268
269(** val dpi1 : ('a1, 'a2) dPair -> 'a1 **)
270let rec dpi1 xxx =
271  xxx.dpi1
272
273(** val dpi2 : ('a1, 'a2) dPair -> 'a2 **)
274let rec dpi2 xxx =
275  xxx.dpi2
276
277(** val dPair_inv_rect_Type4 :
278    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
279let dPair_inv_rect_Type4 hterm h1 =
280  let hcut = dPair_rect_Type4 h1 hterm in hcut __
281
282(** val dPair_inv_rect_Type3 :
283    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
284let dPair_inv_rect_Type3 hterm h1 =
285  let hcut = dPair_rect_Type3 h1 hterm in hcut __
286
287(** val dPair_inv_rect_Type2 :
288    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
289let dPair_inv_rect_Type2 hterm h1 =
290  let hcut = dPair_rect_Type2 h1 hterm in hcut __
291
292(** val dPair_inv_rect_Type1 :
293    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
294let dPair_inv_rect_Type1 hterm h1 =
295  let hcut = dPair_rect_Type1 h1 hterm in hcut __
296
297(** val dPair_inv_rect_Type0 :
298    ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
299let dPair_inv_rect_Type0 hterm h1 =
300  let hcut = dPair_rect_Type0 h1 hterm in hcut __
301
302(** val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __ **)
303let dPair_discr x y =
304  Logic.eq_rect_Type2 x
305    (let { dpi1 = a0; dpi2 = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
306
307type 'a sig0 =
308  'a
309  (* singleton inductive, whose constructor was mk_Sig *)
310
311(** val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
312let rec sig_rect_Type4 h_mk_Sig x_510 =
313  let pi1 = x_510 in h_mk_Sig pi1 __
314
315(** val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
316let rec sig_rect_Type5 h_mk_Sig x_512 =
317  let pi1 = x_512 in h_mk_Sig pi1 __
318
319(** val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
320let rec sig_rect_Type3 h_mk_Sig x_514 =
321  let pi1 = x_514 in h_mk_Sig pi1 __
322
323(** val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
324let rec sig_rect_Type2 h_mk_Sig x_516 =
325  let pi1 = x_516 in h_mk_Sig pi1 __
326
327(** val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
328let rec sig_rect_Type1 h_mk_Sig x_518 =
329  let pi1 = x_518 in h_mk_Sig pi1 __
330
331(** val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
332let rec sig_rect_Type0 h_mk_Sig x_520 =
333  let pi1 = x_520 in h_mk_Sig pi1 __
334
335(** val pi1 : 'a1 sig0 -> 'a1 **)
336let rec pi1 xxx =
337  let yyy = xxx in yyy
338
339(** val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
340let sig_inv_rect_Type4 hterm h1 =
341  let hcut = sig_rect_Type4 h1 hterm in hcut __
342
343(** val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
344let sig_inv_rect_Type3 hterm h1 =
345  let hcut = sig_rect_Type3 h1 hterm in hcut __
346
347(** val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
348let sig_inv_rect_Type2 hterm h1 =
349  let hcut = sig_rect_Type2 h1 hterm in hcut __
350
351(** val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
352let sig_inv_rect_Type1 hterm h1 =
353  let hcut = sig_rect_Type1 h1 hterm in hcut __
354
355(** val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
356let sig_inv_rect_Type0 hterm h1 =
357  let hcut = sig_rect_Type0 h1 hterm in hcut __
358
359(** val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __ **)
360let sig_discr x y =
361  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
362
363type ('a, 'b) prod = { fst : 'a; snd : 'b }
364
365(** val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
366let rec prod_rect_Type4 h_mk_Prod x_536 =
367  let { fst = fst0; snd = snd0 } = x_536 in h_mk_Prod fst0 snd0
368
369(** val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
370let rec prod_rect_Type5 h_mk_Prod x_538 =
371  let { fst = fst0; snd = snd0 } = x_538 in h_mk_Prod fst0 snd0
372
373(** val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
374let rec prod_rect_Type3 h_mk_Prod x_540 =
375  let { fst = fst0; snd = snd0 } = x_540 in h_mk_Prod fst0 snd0
376
377(** val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
378let rec prod_rect_Type2 h_mk_Prod x_542 =
379  let { fst = fst0; snd = snd0 } = x_542 in h_mk_Prod fst0 snd0
380
381(** val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
382let rec prod_rect_Type1 h_mk_Prod x_544 =
383  let { fst = fst0; snd = snd0 } = x_544 in h_mk_Prod fst0 snd0
384
385(** val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
386let rec prod_rect_Type0 h_mk_Prod x_546 =
387  let { fst = fst0; snd = snd0 } = x_546 in h_mk_Prod fst0 snd0
388
389(** val fst : ('a1, 'a2) prod -> 'a1 **)
390let rec fst xxx =
391  xxx.fst
392
393(** val snd : ('a1, 'a2) prod -> 'a2 **)
394let rec snd xxx =
395  xxx.snd
396
397(** val prod_inv_rect_Type4 :
398    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
399let prod_inv_rect_Type4 hterm h1 =
400  let hcut = prod_rect_Type4 h1 hterm in hcut __
401
402(** val prod_inv_rect_Type3 :
403    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
404let prod_inv_rect_Type3 hterm h1 =
405  let hcut = prod_rect_Type3 h1 hterm in hcut __
406
407(** val prod_inv_rect_Type2 :
408    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
409let prod_inv_rect_Type2 hterm h1 =
410  let hcut = prod_rect_Type2 h1 hterm in hcut __
411
412(** val prod_inv_rect_Type1 :
413    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
414let prod_inv_rect_Type1 hterm h1 =
415  let hcut = prod_rect_Type1 h1 hterm in hcut __
416
417(** val prod_inv_rect_Type0 :
418    ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
419let prod_inv_rect_Type0 hterm h1 =
420  let hcut = prod_rect_Type0 h1 hterm in hcut __
421
422(** val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __ **)
423let prod_discr x y =
424  Logic.eq_rect_Type2 x
425    (let { fst = a0; snd = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
426
427(** val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod **)
428let coerc_pair_sigma clearme =
429  (let { fst = a; snd = b } = clearme in (fun _ -> { fst = a; snd = b })) __
430
Note: See TracBrowser for help on using the repository browser.