source: extracted/z.ml @ 2755

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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_4734 -> h_pos x_4734
29| Neg x_4735 -> h_neg x_4735
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_4740 -> h_pos x_4740
36| Neg x_4741 -> h_neg x_4741
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_4746 -> h_pos x_4746
43| Neg x_4747 -> h_neg x_4747
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_4752 -> h_pos x_4752
50| Neg x_4753 -> h_neg x_4753
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_4758 -> h_pos x_4758
57| Neg x_4759 -> h_neg x_4759
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_4764 -> h_pos x_4764
64| Neg x_4765 -> h_neg x_4765
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.