source: extracted/z.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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_4708 -> h_pos x_4708
29| Neg x_4709 -> h_neg x_4709
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_4714 -> h_pos x_4714
36| Neg x_4715 -> h_neg x_4715
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_4720 -> h_pos x_4720
43| Neg x_4721 -> h_neg x_4721
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_4726 -> h_pos x_4726
50| Neg x_4727 -> h_neg x_4727
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_4732 -> h_pos x_4732
57| Neg x_4733 -> h_neg x_4733
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_4738 -> h_pos x_4738
64| Neg x_4739 -> h_neg x_4739
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.