source: extracted/integers.ml @ 2746

Last change on this file since 2746 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: 9.7 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Types
18
19open Extranat
20
21open Vector
22
23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
29open List
30
31open Util
32
33open FoldStuff
34
35open BitVector
36
37open Exp
38
39open Arithmetic
40
41type comparison =
42| Ceq
43| Cne
44| Clt
45| Cle
46| Cgt
47| Cge
48
49(** val comparison_rect_Type4 :
50    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
51let rec comparison_rect_Type4 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
52| Ceq -> h_Ceq
53| Cne -> h_Cne
54| Clt -> h_Clt
55| Cle -> h_Cle
56| Cgt -> h_Cgt
57| Cge -> h_Cge
58
59(** val comparison_rect_Type5 :
60    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
61let rec comparison_rect_Type5 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
62| Ceq -> h_Ceq
63| Cne -> h_Cne
64| Clt -> h_Clt
65| Cle -> h_Cle
66| Cgt -> h_Cgt
67| Cge -> h_Cge
68
69(** val comparison_rect_Type3 :
70    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
71let rec comparison_rect_Type3 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
72| Ceq -> h_Ceq
73| Cne -> h_Cne
74| Clt -> h_Clt
75| Cle -> h_Cle
76| Cgt -> h_Cgt
77| Cge -> h_Cge
78
79(** val comparison_rect_Type2 :
80    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
81let rec comparison_rect_Type2 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
82| Ceq -> h_Ceq
83| Cne -> h_Cne
84| Clt -> h_Clt
85| Cle -> h_Cle
86| Cgt -> h_Cgt
87| Cge -> h_Cge
88
89(** val comparison_rect_Type1 :
90    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
91let rec comparison_rect_Type1 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
92| Ceq -> h_Ceq
93| Cne -> h_Cne
94| Clt -> h_Clt
95| Cle -> h_Cle
96| Cgt -> h_Cgt
97| Cge -> h_Cge
98
99(** val comparison_rect_Type0 :
100    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
101let rec comparison_rect_Type0 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
102| Ceq -> h_Ceq
103| Cne -> h_Cne
104| Clt -> h_Clt
105| Cle -> h_Cle
106| Cgt -> h_Cgt
107| Cge -> h_Cge
108
109(** val comparison_inv_rect_Type4 :
110    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
111    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
112let comparison_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
113  let hcut = comparison_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
114
115(** val comparison_inv_rect_Type3 :
116    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
117    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
118let comparison_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
119  let hcut = comparison_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
120
121(** val comparison_inv_rect_Type2 :
122    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
123    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
124let comparison_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
125  let hcut = comparison_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
126
127(** val comparison_inv_rect_Type1 :
128    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
129    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
130let comparison_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
131  let hcut = comparison_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
132
133(** val comparison_inv_rect_Type0 :
134    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
135    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
136let comparison_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
137  let hcut = comparison_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
138
139(** val comparison_discr : comparison -> comparison -> __ **)
140let comparison_discr x y =
141  Logic.eq_rect_Type2 x
142    (match x with
143     | Ceq -> Obj.magic (fun _ dH -> dH)
144     | Cne -> Obj.magic (fun _ dH -> dH)
145     | Clt -> Obj.magic (fun _ dH -> dH)
146     | Cle -> Obj.magic (fun _ dH -> dH)
147     | Cgt -> Obj.magic (fun _ dH -> dH)
148     | Cge -> Obj.magic (fun _ dH -> dH)) y
149
150(** val comparison_jmdiscr : comparison -> comparison -> __ **)
151let comparison_jmdiscr x y =
152  Logic.eq_rect_Type2 x
153    (match x with
154     | Ceq -> Obj.magic (fun _ dH -> dH)
155     | Cne -> Obj.magic (fun _ dH -> dH)
156     | Clt -> Obj.magic (fun _ dH -> dH)
157     | Cle -> Obj.magic (fun _ dH -> dH)
158     | Cgt -> Obj.magic (fun _ dH -> dH)
159     | Cge -> Obj.magic (fun _ dH -> dH)) y
160
161(** val negate_comparison : comparison -> comparison **)
162let negate_comparison = function
163| Ceq -> Cne
164| Cne -> Ceq
165| Clt -> Cge
166| Cle -> Cgt
167| Cgt -> Cle
168| Cge -> Clt
169
170(** val swap_comparison : comparison -> comparison **)
171let swap_comparison = function
172| Ceq -> Ceq
173| Cne -> Cne
174| Clt -> Cgt
175| Cle -> Cge
176| Cgt -> Clt
177| Cge -> Cle
178
179(** val wordsize : Nat.nat **)
180let wordsize =
181  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
182    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
183    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
184    (Nat.S Nat.O)))))))))))))))))))))))))))))))
185
186type int = BitVector.bitVector
187
188(** val repr : Nat.nat -> int **)
189let repr n =
190  Arithmetic.bitvector_of_nat wordsize n
191
192(** val zero0 : int **)
193let zero0 =
194  repr Nat.O
195
196(** val one : int **)
197let one =
198  repr (Nat.S Nat.O)
199
200(** val mone : BitVector.bitVector **)
201let mone =
202  Arithmetic.subtraction wordsize zero0 one
203
204(** val iwordsize : int **)
205let iwordsize =
206  repr wordsize
207
208(** val eq_dec : int -> int -> (__, __) Types.sum **)
209let eq_dec x y =
210  (match BitVector.eq_bv wordsize x y with
211   | Bool.True -> (fun _ -> Types.Inl __)
212   | Bool.False -> (fun _ -> Types.Inr __)) __
213
214(** val eq : int -> int -> Bool.bool **)
215let eq =
216  BitVector.eq_bv wordsize
217
218(** val lt : int -> int -> Bool.bool **)
219let lt =
220  Arithmetic.lt_s wordsize
221
222(** val ltu : int -> int -> Bool.bool **)
223let ltu =
224  Arithmetic.lt_u wordsize
225
226(** val neg : int -> int **)
227let neg =
228  Arithmetic.two_complement_negation wordsize
229
230(** val mul :
231    BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector **)
232let mul x y =
233  (Vector.vsplit wordsize wordsize (Arithmetic.multiplication wordsize x y)).Types.snd
234
235(** val zero_ext_n :
236    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
237let zero_ext_n w n =
238  match Extranat.nat_compare n w with
239  | Extranat.Nat_lt (n', w') ->
240    (fun i ->
241      let { Types.fst = h; Types.snd = l } =
242        Vector.vsplit (Nat.S w') n' (Vector.switch_bv_plus n' (Nat.S w') i)
243      in
244      Vector.switch_bv_plus (Nat.S w') n' (BitVector.pad (Nat.S w') n' l))
245  | Extranat.Nat_eq x -> (fun i -> i)
246  | Extranat.Nat_gt (x, x0) -> (fun i -> i)
247
248(** val zero_ext0 : Nat.nat -> int -> int **)
249let zero_ext0 =
250  zero_ext_n wordsize
251
252(** val sign_ext_n :
253    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
254let sign_ext_n w n =
255  match Extranat.nat_compare n w with
256  | Extranat.Nat_lt (n', w') ->
257    (fun i ->
258      let { Types.fst = h; Types.snd = l } =
259        Vector.vsplit (Nat.S w') n' (Vector.switch_bv_plus n' (Nat.S w') i)
260      in
261      Vector.switch_bv_plus (Nat.S w') n'
262        (Vector.pad_vector
263          (match l with
264           | Vector.VEmpty -> Bool.False
265           | Vector.VCons (x, h0, x0) -> h0) (Nat.S w') n' l))
266  | Extranat.Nat_eq x -> (fun i -> i)
267  | Extranat.Nat_gt (x, x0) -> (fun i -> i)
268
269(** val sign_ext0 : Nat.nat -> int -> int **)
270let sign_ext0 =
271  sign_ext_n wordsize
272
273(** val i_and : int -> int -> int **)
274let i_and =
275  BitVector.conjunction_bv wordsize
276
277(** val or0 : int -> int -> int **)
278let or0 =
279  BitVector.inclusive_disjunction_bv wordsize
280
281(** val xor : int -> int -> int **)
282let xor =
283  BitVector.exclusive_disjunction_bv wordsize
284
285(** val not : int -> int **)
286let not =
287  BitVector.negation_bv wordsize
288
289(** val shl : int -> int -> int **)
290let shl x y =
291  Vector.shift_left wordsize (Arithmetic.nat_of_bitvector wordsize y) x
292    Bool.False
293
294(** val shru : int -> int -> int **)
295let shru x y =
296  Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
297    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
298    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
299    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))
300    (Arithmetic.nat_of_bitvector wordsize y) x Bool.False
301
302(** val shr : int -> int -> int **)
303let shr x y =
304  Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
305    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
306    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
307    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))
308    (Arithmetic.nat_of_bitvector wordsize y) x
309    (Vector.head' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
310      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
311      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
312      (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))) x)
313
314(** val shrx : int -> int -> int **)
315let shrx x y =
316  match Arithmetic.division_s wordsize x (shl one y) with
317  | Types.None -> zero0
318  | Types.Some i -> i
319
320(** val shr_carry : int -> int -> BitVector.bitVector **)
321let shr_carry x y =
322  Arithmetic.subtraction wordsize (shrx x y) (shr x y)
323
324(** val rol : int -> int -> int **)
325let rol x y =
326  Vector.rotate_left wordsize (Arithmetic.nat_of_bitvector wordsize y) x
327
328(** val ror : int -> int -> int **)
329let ror x y =
330  Vector.rotate_right wordsize (Arithmetic.nat_of_bitvector wordsize y) x
331
332(** val rolm : int -> int -> int -> int **)
333let rolm x a m =
334  i_and (rol x a) m
335
336(** val cmp : comparison -> int -> int -> Bool.bool **)
337let cmp c x y =
338  match c with
339  | Ceq -> eq x y
340  | Cne -> Bool.notb (eq x y)
341  | Clt -> lt x y
342  | Cle -> Bool.notb (lt y x)
343  | Cgt -> lt y x
344  | Cge -> Bool.notb (lt x y)
345
346(** val cmpu : comparison -> int -> int -> Bool.bool **)
347let cmpu c x y =
348  match c with
349  | Ceq -> eq x y
350  | Cne -> Bool.notb (eq x y)
351  | Clt -> ltu x y
352  | Cle -> Bool.notb (ltu y x)
353  | Cgt -> ltu y x
354  | Cge -> Bool.notb (ltu x y)
355
356(** val notbool : int -> int **)
357let notbool x =
358  match eq x zero0 with
359  | Bool.True -> one
360  | Bool.False -> zero0
361
Note: See TracBrowser for help on using the repository browser.