source: extracted/z.ml @ 2601

Last change on this file since 2601 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: 7.6 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 Positive
18
19type z =
20| OZ
21| Pos of Positive.pos
22| Neg of Positive.pos
23
24(** val z_rect_Type4 :
25    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
26let rec z_rect_Type4 h_OZ h_pos h_neg = function
27| OZ -> h_OZ
28| Pos x_3707 -> h_pos x_3707
29| Neg x_3708 -> h_neg x_3708
30
31(** val z_rect_Type5 :
32    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
33let rec z_rect_Type5 h_OZ h_pos h_neg = function
34| OZ -> h_OZ
35| Pos x_3713 -> h_pos x_3713
36| Neg x_3714 -> h_neg x_3714
37
38(** val z_rect_Type3 :
39    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
40let rec z_rect_Type3 h_OZ h_pos h_neg = function
41| OZ -> h_OZ
42| Pos x_3719 -> h_pos x_3719
43| Neg x_3720 -> h_neg x_3720
44
45(** val z_rect_Type2 :
46    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
47let rec z_rect_Type2 h_OZ h_pos h_neg = function
48| OZ -> h_OZ
49| Pos x_3725 -> h_pos x_3725
50| Neg x_3726 -> h_neg x_3726
51
52(** val z_rect_Type1 :
53    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
54let rec z_rect_Type1 h_OZ h_pos h_neg = function
55| OZ -> h_OZ
56| Pos x_3731 -> h_pos x_3731
57| Neg x_3732 -> h_neg x_3732
58
59(** val z_rect_Type0 :
60    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
61let rec z_rect_Type0 h_OZ h_pos h_neg = function
62| OZ -> h_OZ
63| Pos x_3737 -> h_pos x_3737
64| Neg x_3738 -> h_neg x_3738
65
66(** val z_inv_rect_Type4 :
67    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
68    'a1) -> 'a1 **)
69let z_inv_rect_Type4 hterm h1 h2 h3 =
70  let hcut = z_rect_Type4 h1 h2 h3 hterm in hcut __
71
72(** val z_inv_rect_Type3 :
73    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
74    'a1) -> 'a1 **)
75let z_inv_rect_Type3 hterm h1 h2 h3 =
76  let hcut = z_rect_Type3 h1 h2 h3 hterm in hcut __
77
78(** val z_inv_rect_Type2 :
79    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
80    'a1) -> 'a1 **)
81let z_inv_rect_Type2 hterm h1 h2 h3 =
82  let hcut = z_rect_Type2 h1 h2 h3 hterm in hcut __
83
84(** val z_inv_rect_Type1 :
85    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
86    'a1) -> 'a1 **)
87let z_inv_rect_Type1 hterm h1 h2 h3 =
88  let hcut = z_rect_Type1 h1 h2 h3 hterm in hcut __
89
90(** val z_inv_rect_Type0 :
91    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
92    'a1) -> 'a1 **)
93let z_inv_rect_Type0 hterm h1 h2 h3 =
94  let hcut = z_rect_Type0 h1 h2 h3 hterm in hcut __
95
96(** val z_discr : z -> z -> __ **)
97let z_discr x y =
98  Logic.eq_rect_Type2 x
99    (match x with
100     | OZ -> Obj.magic (fun _ dH -> dH)
101     | Pos a0 -> Obj.magic (fun _ dH -> dH __)
102     | Neg a0 -> Obj.magic (fun _ dH -> dH __)) y
103
104(** val z_of_nat : Nat.nat -> z **)
105let z_of_nat = function
106| Nat.O -> OZ
107| Nat.S n0 -> Pos (Positive.succ_pos_of_nat n0)
108
109(** val neg_Z_of_nat : Nat.nat -> z **)
110let neg_Z_of_nat = function
111| Nat.O -> OZ
112| Nat.S n0 -> Neg (Positive.succ_pos_of_nat n0)
113
114(** val abs : z -> Nat.nat **)
115let abs = function
116| OZ -> Nat.O
117| Pos n -> Positive.nat_of_pos n
118| Neg n -> Positive.nat_of_pos n
119
120(** val oZ_test : z -> Bool.bool **)
121let oZ_test = function
122| OZ -> Bool.True
123| Pos x -> Bool.False
124| Neg x -> Bool.False
125
126(** val zsucc : z -> z **)
127let zsucc = function
128| OZ -> Pos Positive.One
129| Pos n -> Pos (Positive.succ n)
130| Neg n ->
131  (match n with
132   | Positive.One -> OZ
133   | Positive.P1 x -> Neg (Positive.pred0 n)
134   | Positive.P0 x -> Neg (Positive.pred0 n))
135
136(** val zpred : z -> z **)
137let zpred = function
138| OZ -> Neg Positive.One
139| Pos n ->
140  (match n with
141   | Positive.One -> OZ
142   | Positive.P1 x -> Pos (Positive.pred0 n)
143   | Positive.P0 x -> Pos (Positive.pred0 n))
144| Neg n -> Neg (Positive.succ n)
145
146type zle = __
147
148type zlt = __
149
150(** val eqZb : z -> z -> Bool.bool **)
151let rec eqZb x y =
152  match x with
153  | OZ ->
154    (match y with
155     | OZ -> Bool.True
156     | Pos q -> Bool.False
157     | Neg q -> Bool.False)
158  | Pos p ->
159    (match y with
160     | OZ -> Bool.False
161     | Pos q -> Positive.eqb0 p q
162     | Neg q -> Bool.False)
163  | Neg p ->
164    (match y with
165     | OZ -> Bool.False
166     | Pos q -> Bool.False
167     | Neg q -> Positive.eqb0 p q)
168
169(** val z_compare : z -> z -> Positive.compare **)
170let rec z_compare x y =
171  match x with
172  | OZ ->
173    (match y with
174     | OZ -> Positive.EQ
175     | Pos m -> Positive.LT
176     | Neg m -> Positive.GT)
177  | Pos n ->
178    (match y with
179     | OZ -> Positive.GT
180     | Pos m -> Positive.pos_compare n m
181     | Neg m -> Positive.GT)
182  | Neg n ->
183    (match y with
184     | OZ -> Positive.LT
185     | Pos m -> Positive.LT
186     | Neg m -> Positive.pos_compare m n)
187
188(** val zplus : z -> z -> z **)
189let rec zplus x y =
190  match x with
191  | OZ -> y
192  | Pos m ->
193    (match y with
194     | OZ -> x
195     | Pos n -> Pos (Positive.plus0 m n)
196     | Neg n ->
197       (match Positive.pos_compare m n with
198        | Positive.LT -> Neg (Positive.minus0 n m)
199        | Positive.EQ -> OZ
200        | Positive.GT -> Pos (Positive.minus0 m n)))
201  | Neg m ->
202    (match y with
203     | OZ -> x
204     | Pos n ->
205       (match Positive.pos_compare m n with
206        | Positive.LT -> Pos (Positive.minus0 n m)
207        | Positive.EQ -> OZ
208        | Positive.GT -> Neg (Positive.minus0 m n))
209     | Neg n -> Neg (Positive.plus0 m n))
210
211(** val zopp : z -> z **)
212let zopp = function
213| OZ -> OZ
214| Pos n -> Neg n
215| Neg n -> Pos n
216
217(** val zminus : z -> z -> z **)
218let zminus x y =
219  zplus x (zopp y)
220
221(** val z_two_power_nat : Nat.nat -> z **)
222let z_two_power_nat n =
223  Pos (Positive.two_power_nat n)
224
225(** val z_two_power_pos : Positive.pos -> z **)
226let z_two_power_pos n =
227  Pos (Positive.two_power_pos n)
228
229(** val two_p : z -> z **)
230let two_p = function
231| OZ -> Pos Positive.One
232| Pos p -> Pos (Positive.two_power_pos p)
233| Neg x -> OZ
234
235open Types
236
237(** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
238let decidable_eq_Z_Type z1 z2 =
239  (match eqZb z1 z2 with
240   | Bool.True -> (fun _ -> Types.Inl __)
241   | Bool.False -> (fun _ -> Types.Inr __)) __
242
243(** val zleb : z -> z -> Bool.bool **)
244let rec zleb x y =
245  match x with
246  | OZ ->
247    (match y with
248     | OZ -> Bool.True
249     | Pos m -> Bool.True
250     | Neg m -> Bool.False)
251  | Pos n ->
252    (match y with
253     | OZ -> Bool.False
254     | Pos m -> Positive.leb0 n m
255     | Neg m -> Bool.False)
256  | Neg n ->
257    (match y with
258     | OZ -> Bool.True
259     | Pos m -> Bool.True
260     | Neg m -> Positive.leb0 m n)
261
262(** val zltb : z -> z -> Bool.bool **)
263let rec zltb x y =
264  match x with
265  | OZ ->
266    (match y with
267     | OZ -> Bool.False
268     | Pos m -> Bool.True
269     | Neg m -> Bool.False)
270  | Pos n ->
271    (match y with
272     | OZ -> Bool.False
273     | Pos m -> Positive.leb0 (Positive.succ n) m
274     | Neg m -> Bool.False)
275  | Neg n ->
276    (match y with
277     | OZ -> Bool.True
278     | Pos m -> Bool.True
279     | Neg m -> Positive.leb0 (Positive.succ m) n)
280
281(** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
282let zleb_elim_Type0 n m hle hnle =
283  Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __
284
285(** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
286let zltb_elim_Type0 n m hlt hnlt =
287  Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __
288
289(** val z_times : z -> z -> z **)
290let rec z_times x y =
291  match x with
292  | OZ -> OZ
293  | Pos n ->
294    (match y with
295     | OZ -> OZ
296     | Pos m -> Pos (Positive.times0 n m)
297     | Neg m -> Neg (Positive.times0 n m))
298  | Neg n ->
299    (match y with
300     | OZ -> OZ
301     | Pos m -> Neg (Positive.times0 n m)
302     | Neg m -> Pos (Positive.times0 n m))
303
304(** val zmax : z -> z -> z **)
305let zmax x y =
306  match z_compare x y with
307  | Positive.LT -> y
308  | Positive.EQ -> x
309  | Positive.GT -> x
310
Note: See TracBrowser for help on using the repository browser.