source: extracted/integers.ml @ 2649

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

...

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