source: driver/extracted/z.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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_4786 -> h_pos x_4786
29| Neg x_4787 -> h_neg x_4787
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_4792 -> h_pos x_4792
36| Neg x_4793 -> h_neg x_4793
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_4798 -> h_pos x_4798
43| Neg x_4799 -> h_neg x_4799
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_4804 -> h_pos x_4804
50| Neg x_4805 -> h_neg x_4805
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_4810 -> h_pos x_4810
57| Neg x_4811 -> h_neg x_4811
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_4816 -> h_pos x_4816
64| Neg x_4817 -> h_neg x_4817
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.pred n)
134   | Positive.P0 x -> Neg (Positive.pred 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.pred n)
143   | Positive.P0 x -> Pos (Positive.pred n))
144| Neg n -> Neg (Positive.succ n)
145
146(** val eqZb : z -> z -> Bool.bool **)
147let rec eqZb x y =
148  match x with
149  | OZ ->
150    (match y with
151     | OZ -> Bool.True
152     | Pos q -> Bool.False
153     | Neg q -> Bool.False)
154  | Pos p ->
155    (match y with
156     | OZ -> Bool.False
157     | Pos q -> Positive.eqb p q
158     | Neg q -> Bool.False)
159  | Neg p ->
160    (match y with
161     | OZ -> Bool.False
162     | Pos q -> Bool.False
163     | Neg q -> Positive.eqb p q)
164
165(** val z_compare : z -> z -> Positive.compare **)
166let rec z_compare x y =
167  match x with
168  | OZ ->
169    (match y with
170     | OZ -> Positive.EQ
171     | Pos m -> Positive.LT
172     | Neg m -> Positive.GT)
173  | Pos n ->
174    (match y with
175     | OZ -> Positive.GT
176     | Pos m -> Positive.pos_compare n m
177     | Neg m -> Positive.GT)
178  | Neg n ->
179    (match y with
180     | OZ -> Positive.LT
181     | Pos m -> Positive.LT
182     | Neg m -> Positive.pos_compare m n)
183
184(** val zplus : z -> z -> z **)
185let rec zplus x y =
186  match x with
187  | OZ -> y
188  | Pos m ->
189    (match y with
190     | OZ -> x
191     | Pos n -> Pos (Positive.plus m n)
192     | Neg n ->
193       (match Positive.pos_compare m n with
194        | Positive.LT -> Neg (Positive.minus n m)
195        | Positive.EQ -> OZ
196        | Positive.GT -> Pos (Positive.minus m n)))
197  | Neg m ->
198    (match y with
199     | OZ -> x
200     | Pos n ->
201       (match Positive.pos_compare m n with
202        | Positive.LT -> Pos (Positive.minus n m)
203        | Positive.EQ -> OZ
204        | Positive.GT -> Neg (Positive.minus m n))
205     | Neg n -> Neg (Positive.plus m n))
206
207(** val zopp : z -> z **)
208let zopp = function
209| OZ -> OZ
210| Pos n -> Neg n
211| Neg n -> Pos n
212
213(** val zminus : z -> z -> z **)
214let zminus x y =
215  zplus x (zopp y)
216
217(** val z_two_power_nat : Nat.nat -> z **)
218let z_two_power_nat n =
219  Pos (Positive.two_power_nat n)
220
221(** val z_two_power_pos : Positive.pos -> z **)
222let z_two_power_pos n =
223  Pos (Positive.two_power_pos n)
224
225(** val two_p : z -> z **)
226let two_p = function
227| OZ -> Pos Positive.One
228| Pos p -> Pos (Positive.two_power_pos p)
229| Neg x -> OZ
230
231open Types
232
233(** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
234let decidable_eq_Z_Type z1 z2 =
235  (match eqZb z1 z2 with
236   | Bool.True -> (fun _ -> Types.Inl __)
237   | Bool.False -> (fun _ -> Types.Inr __)) __
238
239(** val zleb : z -> z -> Bool.bool **)
240let rec zleb x y =
241  match x with
242  | OZ ->
243    (match y with
244     | OZ -> Bool.True
245     | Pos m -> Bool.True
246     | Neg m -> Bool.False)
247  | Pos n ->
248    (match y with
249     | OZ -> Bool.False
250     | Pos m -> Positive.leb n m
251     | Neg m -> Bool.False)
252  | Neg n ->
253    (match y with
254     | OZ -> Bool.True
255     | Pos m -> Bool.True
256     | Neg m -> Positive.leb m n)
257
258(** val zltb : z -> z -> Bool.bool **)
259let rec zltb x y =
260  match x with
261  | OZ ->
262    (match y with
263     | OZ -> Bool.False
264     | Pos m -> Bool.True
265     | Neg m -> Bool.False)
266  | Pos n ->
267    (match y with
268     | OZ -> Bool.False
269     | Pos m -> Positive.leb (Positive.succ n) m
270     | Neg m -> Bool.False)
271  | Neg n ->
272    (match y with
273     | OZ -> Bool.True
274     | Pos m -> Bool.True
275     | Neg m -> Positive.leb (Positive.succ m) n)
276
277(** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
278let zleb_elim_Type0 n m hle hnle =
279  Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __
280
281(** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
282let zltb_elim_Type0 n m hlt hnlt =
283  Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __
284
285(** val z_times : z -> z -> z **)
286let rec z_times x y =
287  match x with
288  | OZ -> OZ
289  | Pos n ->
290    (match y with
291     | OZ -> OZ
292     | Pos m -> Pos (Positive.times n m)
293     | Neg m -> Neg (Positive.times n m))
294  | Neg n ->
295    (match y with
296     | OZ -> OZ
297     | Pos m -> Neg (Positive.times n m)
298     | Neg m -> Pos (Positive.times n m))
299
300(** val zmax : z -> z -> z **)
301let zmax x y =
302  match z_compare x y with
303  | Positive.LT -> y
304  | Positive.EQ -> x
305  | Positive.GT -> x
306
Note: See TracBrowser for help on using the repository browser.