source: extracted/positive.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: 12.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Bool
12
13open Relations
14
15open Nat
16
17type compare =
18| LT
19| EQ
20| GT
21
22(** val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
23let rec compare_rect_Type4 h_LT h_EQ h_GT = function
24| LT -> h_LT
25| EQ -> h_EQ
26| GT -> h_GT
27
28(** val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
29let rec compare_rect_Type5 h_LT h_EQ h_GT = function
30| LT -> h_LT
31| EQ -> h_EQ
32| GT -> h_GT
33
34(** val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
35let rec compare_rect_Type3 h_LT h_EQ h_GT = function
36| LT -> h_LT
37| EQ -> h_EQ
38| GT -> h_GT
39
40(** val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
41let rec compare_rect_Type2 h_LT h_EQ h_GT = function
42| LT -> h_LT
43| EQ -> h_EQ
44| GT -> h_GT
45
46(** val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
47let rec compare_rect_Type1 h_LT h_EQ h_GT = function
48| LT -> h_LT
49| EQ -> h_EQ
50| GT -> h_GT
51
52(** val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
53let rec compare_rect_Type0 h_LT h_EQ h_GT = function
54| LT -> h_LT
55| EQ -> h_EQ
56| GT -> h_GT
57
58(** val compare_inv_rect_Type4 :
59    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
60let compare_inv_rect_Type4 hterm h1 h2 h3 =
61  let hcut = compare_rect_Type4 h1 h2 h3 hterm in hcut __
62
63(** val compare_inv_rect_Type3 :
64    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
65let compare_inv_rect_Type3 hterm h1 h2 h3 =
66  let hcut = compare_rect_Type3 h1 h2 h3 hterm in hcut __
67
68(** val compare_inv_rect_Type2 :
69    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
70let compare_inv_rect_Type2 hterm h1 h2 h3 =
71  let hcut = compare_rect_Type2 h1 h2 h3 hterm in hcut __
72
73(** val compare_inv_rect_Type1 :
74    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
75let compare_inv_rect_Type1 hterm h1 h2 h3 =
76  let hcut = compare_rect_Type1 h1 h2 h3 hterm in hcut __
77
78(** val compare_inv_rect_Type0 :
79    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
80let compare_inv_rect_Type0 hterm h1 h2 h3 =
81  let hcut = compare_rect_Type0 h1 h2 h3 hterm in hcut __
82
83(** val compare_discr : compare -> compare -> __ **)
84let compare_discr x y =
85  Logic.eq_rect_Type2 x
86    (match x with
87     | LT -> Obj.magic (fun _ dH -> dH)
88     | EQ -> Obj.magic (fun _ dH -> dH)
89     | GT -> Obj.magic (fun _ dH -> dH)) y
90
91(** val compare_invert : compare -> compare **)
92let compare_invert = function
93| LT -> GT
94| EQ -> EQ
95| GT -> LT
96
97type pos =
98| One
99| P1 of pos
100| P0 of pos
101
102(** val pos_rect_Type4 :
103    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
104let rec pos_rect_Type4 h_one h_p1 h_p0 = function
105| One -> h_one
106| P1 x_1375 -> h_p1 x_1375 (pos_rect_Type4 h_one h_p1 h_p0 x_1375)
107| P0 x_1376 -> h_p0 x_1376 (pos_rect_Type4 h_one h_p1 h_p0 x_1376)
108
109(** val pos_rect_Type3 :
110    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
111let rec pos_rect_Type3 h_one h_p1 h_p0 = function
112| One -> h_one
113| P1 x_1387 -> h_p1 x_1387 (pos_rect_Type3 h_one h_p1 h_p0 x_1387)
114| P0 x_1388 -> h_p0 x_1388 (pos_rect_Type3 h_one h_p1 h_p0 x_1388)
115
116(** val pos_rect_Type2 :
117    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
118let rec pos_rect_Type2 h_one h_p1 h_p0 = function
119| One -> h_one
120| P1 x_1393 -> h_p1 x_1393 (pos_rect_Type2 h_one h_p1 h_p0 x_1393)
121| P0 x_1394 -> h_p0 x_1394 (pos_rect_Type2 h_one h_p1 h_p0 x_1394)
122
123(** val pos_rect_Type1 :
124    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
125let rec pos_rect_Type1 h_one h_p1 h_p0 = function
126| One -> h_one
127| P1 x_1399 -> h_p1 x_1399 (pos_rect_Type1 h_one h_p1 h_p0 x_1399)
128| P0 x_1400 -> h_p0 x_1400 (pos_rect_Type1 h_one h_p1 h_p0 x_1400)
129
130(** val pos_rect_Type0 :
131    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
132let rec pos_rect_Type0 h_one h_p1 h_p0 = function
133| One -> h_one
134| P1 x_1405 -> h_p1 x_1405 (pos_rect_Type0 h_one h_p1 h_p0 x_1405)
135| P0 x_1406 -> h_p0 x_1406 (pos_rect_Type0 h_one h_p1 h_p0 x_1406)
136
137(** val pos_inv_rect_Type4 :
138    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
139    'a1) -> __ -> 'a1) -> 'a1 **)
140let pos_inv_rect_Type4 hterm h1 h2 h3 =
141  let hcut = pos_rect_Type4 h1 h2 h3 hterm in hcut __
142
143(** val pos_inv_rect_Type3 :
144    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
145    'a1) -> __ -> 'a1) -> 'a1 **)
146let pos_inv_rect_Type3 hterm h1 h2 h3 =
147  let hcut = pos_rect_Type3 h1 h2 h3 hterm in hcut __
148
149(** val pos_inv_rect_Type2 :
150    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
151    'a1) -> __ -> 'a1) -> 'a1 **)
152let pos_inv_rect_Type2 hterm h1 h2 h3 =
153  let hcut = pos_rect_Type2 h1 h2 h3 hterm in hcut __
154
155(** val pos_inv_rect_Type1 :
156    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
157    'a1) -> __ -> 'a1) -> 'a1 **)
158let pos_inv_rect_Type1 hterm h1 h2 h3 =
159  let hcut = pos_rect_Type1 h1 h2 h3 hterm in hcut __
160
161(** val pos_inv_rect_Type0 :
162    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
163    'a1) -> __ -> 'a1) -> 'a1 **)
164let pos_inv_rect_Type0 hterm h1 h2 h3 =
165  let hcut = pos_rect_Type0 h1 h2 h3 hterm in hcut __
166
167(** val pos_discr : pos -> pos -> __ **)
168let pos_discr x y =
169  Logic.eq_rect_Type2 x
170    (match x with
171     | One -> Obj.magic (fun _ dH -> dH)
172     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
173     | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y
174
175(** val pred0 : pos -> pos **)
176let rec pred0 = function
177| One -> One
178| P1 ps -> P0 ps
179| P0 ps ->
180  (match ps with
181   | One -> One
182   | P1 x -> P1 (pred0 ps)
183   | P0 x -> P1 (pred0 ps))
184
185(** val succ : pos -> pos **)
186let rec succ = function
187| One -> P0 One
188| P1 ps -> P0 (succ ps)
189| P0 ps -> P1 ps
190
191(** val nat_of_pos : pos -> Nat.nat **)
192let rec nat_of_pos = function
193| One -> Nat.S Nat.O
194| P1 ps -> Nat.S (Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps))
195| P0 ps -> Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps)
196
197(** val succ_pos_of_nat : Nat.nat -> pos **)
198let rec succ_pos_of_nat = function
199| Nat.O -> One
200| Nat.S n' -> succ (succ_pos_of_nat n')
201
202(** val plus0 : pos -> pos -> pos **)
203let rec plus0 n m =
204  match n with
205  | One -> succ m
206  | P1 n' ->
207    (match m with
208     | One -> succ n
209     | P1 m' -> P0 (succ (plus0 n' m'))
210     | P0 m' -> P1 (plus0 n' m'))
211  | P0 n' ->
212    (match m with
213     | One -> P1 n'
214     | P1 m' -> P1 (plus0 n' m')
215     | P0 m' -> P0 (plus0 n' m'))
216
217(** val times0 : pos -> pos -> pos **)
218let rec times0 n m =
219  match n with
220  | One -> m
221  | P1 n' -> plus0 m (P0 (times0 n' m))
222  | P0 n' -> P0 (times0 n' m)
223
224type minusresult =
225| MinusNeg
226| MinusZero
227| MinusPos of pos
228
229(** val minusresult_rect_Type4 :
230    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
231let rec minusresult_rect_Type4 h_MinusNeg h_MinusZero h_MinusPos = function
232| MinusNeg -> h_MinusNeg
233| MinusZero -> h_MinusZero
234| MinusPos x_1582 -> h_MinusPos x_1582
235
236(** val minusresult_rect_Type5 :
237    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
238let rec minusresult_rect_Type5 h_MinusNeg h_MinusZero h_MinusPos = function
239| MinusNeg -> h_MinusNeg
240| MinusZero -> h_MinusZero
241| MinusPos x_1587 -> h_MinusPos x_1587
242
243(** val minusresult_rect_Type3 :
244    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
245let rec minusresult_rect_Type3 h_MinusNeg h_MinusZero h_MinusPos = function
246| MinusNeg -> h_MinusNeg
247| MinusZero -> h_MinusZero
248| MinusPos x_1592 -> h_MinusPos x_1592
249
250(** val minusresult_rect_Type2 :
251    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
252let rec minusresult_rect_Type2 h_MinusNeg h_MinusZero h_MinusPos = function
253| MinusNeg -> h_MinusNeg
254| MinusZero -> h_MinusZero
255| MinusPos x_1597 -> h_MinusPos x_1597
256
257(** val minusresult_rect_Type1 :
258    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
259let rec minusresult_rect_Type1 h_MinusNeg h_MinusZero h_MinusPos = function
260| MinusNeg -> h_MinusNeg
261| MinusZero -> h_MinusZero
262| MinusPos x_1602 -> h_MinusPos x_1602
263
264(** val minusresult_rect_Type0 :
265    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
266let rec minusresult_rect_Type0 h_MinusNeg h_MinusZero h_MinusPos = function
267| MinusNeg -> h_MinusNeg
268| MinusZero -> h_MinusZero
269| MinusPos x_1607 -> h_MinusPos x_1607
270
271(** val minusresult_inv_rect_Type4 :
272    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
273let minusresult_inv_rect_Type4 hterm h1 h2 h3 =
274  let hcut = minusresult_rect_Type4 h1 h2 h3 hterm in hcut __
275
276(** val minusresult_inv_rect_Type3 :
277    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
278let minusresult_inv_rect_Type3 hterm h1 h2 h3 =
279  let hcut = minusresult_rect_Type3 h1 h2 h3 hterm in hcut __
280
281(** val minusresult_inv_rect_Type2 :
282    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
283let minusresult_inv_rect_Type2 hterm h1 h2 h3 =
284  let hcut = minusresult_rect_Type2 h1 h2 h3 hterm in hcut __
285
286(** val minusresult_inv_rect_Type1 :
287    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
288let minusresult_inv_rect_Type1 hterm h1 h2 h3 =
289  let hcut = minusresult_rect_Type1 h1 h2 h3 hterm in hcut __
290
291(** val minusresult_inv_rect_Type0 :
292    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
293let minusresult_inv_rect_Type0 hterm h1 h2 h3 =
294  let hcut = minusresult_rect_Type0 h1 h2 h3 hterm in hcut __
295
296(** val minusresult_discr : minusresult -> minusresult -> __ **)
297let minusresult_discr x y =
298  Logic.eq_rect_Type2 x
299    (match x with
300     | MinusNeg -> Obj.magic (fun _ dH -> dH)
301     | MinusZero -> Obj.magic (fun _ dH -> dH)
302     | MinusPos a0 -> Obj.magic (fun _ dH -> dH __)) y
303
304(** val partial_minus : pos -> pos -> minusresult **)
305let rec partial_minus n m =
306  match n with
307  | One ->
308    (match m with
309     | One -> MinusZero
310     | P1 x -> MinusNeg
311     | P0 x -> MinusNeg)
312  | P1 n' ->
313    (match m with
314     | One -> MinusPos (P0 n')
315     | P1 m' ->
316       (match partial_minus n' m' with
317        | MinusNeg -> MinusNeg
318        | MinusZero -> MinusZero
319        | MinusPos p -> MinusPos (P0 p))
320     | P0 m' ->
321       (match partial_minus n' m' with
322        | MinusNeg -> MinusNeg
323        | MinusZero -> MinusPos One
324        | MinusPos p -> MinusPos (P1 p)))
325  | P0 n' ->
326    (match m with
327     | One -> MinusPos (pred0 n)
328     | P1 m' ->
329       (match partial_minus n' m' with
330        | MinusNeg -> MinusNeg
331        | MinusZero -> MinusNeg
332        | MinusPos p -> MinusPos (pred0 (P0 p)))
333     | P0 m' ->
334       (match partial_minus n' m' with
335        | MinusNeg -> MinusNeg
336        | MinusZero -> MinusZero
337        | MinusPos p -> MinusPos (P0 p)))
338
339(** val minus0 : pos -> pos -> pos **)
340let minus0 n m =
341  match partial_minus n m with
342  | MinusNeg -> One
343  | MinusZero -> One
344  | MinusPos p -> p
345
346(** val eqb0 : pos -> pos -> Bool.bool **)
347let rec eqb0 n m =
348  match n with
349  | One ->
350    (match m with
351     | One -> Bool.True
352     | P1 x -> Bool.False
353     | P0 x -> Bool.False)
354  | P1 p ->
355    (match m with
356     | One -> Bool.False
357     | P1 q -> eqb0 p q
358     | P0 x -> Bool.False)
359  | P0 p ->
360    (match m with
361     | One -> Bool.False
362     | P1 x -> Bool.False
363     | P0 q -> eqb0 p q)
364
365(** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
366let eqb_elim n m x x0 =
367  pos_rect_Type1 (fun m0 ->
368    match m0 with
369    | One -> (fun _ auto auto' -> auto __)
370    | P1 m' -> (fun _ t f -> f __)
371    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
372    match m0 with
373    | One -> (fun _ t f -> f __)
374    | P1 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))
375    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
376    match m0 with
377    | One -> (fun _ t f -> f __)
378    | P1 m' -> (fun _ t f -> f __)
379    | P0 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))) n m
380    __ x x0
381
382(** val leb0 : pos -> pos -> Bool.bool **)
383let rec leb0 n m =
384  match partial_minus n m with
385  | MinusNeg -> Bool.True
386  | MinusZero -> Bool.True
387  | MinusPos x -> Bool.False
388
389(** val pos_compare : pos -> pos -> compare **)
390let pos_compare n m =
391  match partial_minus n m with
392  | MinusNeg -> LT
393  | MinusZero -> EQ
394  | MinusPos x -> GT
395
396(** val two_power_nat : Nat.nat -> pos **)
397let rec two_power_nat = function
398| Nat.O -> One
399| Nat.S n' -> P0 (two_power_nat n')
400
401(** val two_power_pos : pos -> pos **)
402let two_power_pos p =
403  two_power_nat (nat_of_pos p)
404
405(** val max0 : pos -> pos -> pos **)
406let max0 n m =
407  match leb0 n m with
408  | Bool.True -> m
409  | Bool.False -> n
410
Note: See TracBrowser for help on using the repository browser.