extracted/integers.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open List
  22
  23 open Setoids
  24
  25 open Monad
  26
  27 open Option
  28
  29 open Types
  30
  31 open Extranat
  32
  33 open Vector
  34
  35 open Div_and_mod
  36
  37 open Util
  38
  39 open FoldStuff
  40
  41 open BitVector
  42
  43 open Exp
  44
  45 open Arithmetic
  46
  47 type 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 **)
  57 let 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 **)
  67 let 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 **)
  77 let 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 **)
  87 let 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 **)
  97 let 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 **)
 107 let 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 **)
 118 let 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 **)
 124 let 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 **)
 130 let 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 **)
 136 let 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 **)
 142 let 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 -> __ **)
 146 let 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 -> __ **)
 157 let 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 **)
 168 let 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 **)
 177 let 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 **)
 186 let 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
 192 type int = BitVector.bitVector
 193
 194 (** val repr : Nat.nat -> int **)
 195 let repr n =
 196   Arithmetic.bitvector_of_nat wordsize n
 197
 198 (** val zero : int **)
 199 let zero =
 200   repr Nat.O
 201
 202 (** val one : int **)
 203 let one =
 204   repr (Nat.S Nat.O)
 205
 206 (** val mone : BitVector.bitVector **)
 207 let mone =
 208   Arithmetic.subtraction wordsize zero one
 209
 210 (** val iwordsize : int **)
 211 let iwordsize =
 212   repr wordsize
 213
 214 (** val eq_dec : int -> int -> (__, __) Types.sum **)
 215 let 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 **)
 221 let eq =
 222   BitVector.eq_bv wordsize
 223
 224 (** val lt : int -> int -> Bool.bool **)
 225 let lt =
 226   Arithmetic.lt_s wordsize
 227
 228 (** val ltu : int -> int -> Bool.bool **)
 229 let ltu =
 230   Arithmetic.lt_u wordsize
 231
 232 (** val neg : int -> int **)
 233 let neg =
 234   Arithmetic.two_complement_negation wordsize
 235
 236 (** val mul :
 237     BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector **)
 238 let 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 **)
 243 let 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 **)
 255 let zero_ext =
 256   zero_ext_n wordsize
 257
 258 (** val sign_ext_n :
 259     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 260 let 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 **)
 276 let sign_ext =
 277   sign_ext_n wordsize
 278
 279 (** val i_and : int -> int -> int **)
 280 let i_and =
 281   BitVector.conjunction_bv wordsize
 282
 283 (** val or0 : int -> int -> int **)
 284 let or0 =
 285   BitVector.inclusive_disjunction_bv wordsize
 286
 287 (** val xor : int -> int -> int **)
 288 let xor =
 289   BitVector.exclusive_disjunction_bv wordsize
 290
 291 (** val not : int -> int **)
 292 let not =
 293   BitVector.negation_bv wordsize
 294
 295 (** val shl : int -> int -> int **)
 296 let 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 **)
 301 let 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 **)
 309 let 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 **)
 321 let 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 **)
 327 let shr_carry x y =
 328   Arithmetic.subtraction wordsize (shrx x y) (shr x y)
 329
 330 (** val rol : int -> int -> int **)
 331 let rol x y =
 332   Vector.rotate_left wordsize (Arithmetic.nat_of_bitvector wordsize y) x
 333
 334 (** val ror : int -> int -> int **)
 335 let ror x y =
 336   Vector.rotate_right wordsize (Arithmetic.nat_of_bitvector wordsize y) x
 337
 338 (** val rolm : int -> int -> int -> int **)
 339 let rolm x a m =
 340   i_and (rol x a) m
 341
 342 (** val cmp : comparison -> int -> int -> Bool.bool **)
 343 let 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 **)
 353 let 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 **)
 363 let notbool x =
 364   match eq x zero with
 365   | Bool.True -> one
 366   | Bool.False -> zero
 367