source: extracted/integers.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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