source: driver/extracted/integers.ml @ 3106

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