extracted/arithmetic.mli

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Extranat
  10
  11 open Vector
  12
  13 open Div_and_mod
  14
  15 open Jmeq
  16
  17 open Russell
  18
  19 open Types
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Hints_declaration
  30
  31 open Core_notation
  32
  33 open Pts
  34
  35 open Logic
  36
  37 open Relations
  38
  39 open Nat
  40
  41 open BitVector
  42
  43 open Exp
  44
  45 val addr16_of_addr11 : BitVector.word -> BitVector.word11 -> BitVector.word
  46
  47 val nat_of_bool : Bool.bool -> Nat.nat
  48
  49 val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool
  50
  51 val add_with_carries :
  52   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  53   (BitVector.bitVector, BitVector.bitVector) Types.prod
  54
  55 val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool
  56
  57 val sub_with_borrows :
  58   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  59   (BitVector.bitVector, BitVector.bitVector) Types.prod
  60
  61 val add_n_with_carry :
  62   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  63   (BitVector.bitVector, BitVector.bitVector) Types.prod
  64
  65 val sub_n_with_carry :
  66   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  67   (BitVector.bitVector, BitVector.bitVector) Types.prod
  68
  69 val add_8_with_carry :
  70   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  71   (BitVector.bitVector, BitVector.bitVector) Types.prod
  72
  73 val add_16_with_carry :
  74   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  75   (BitVector.bitVector, BitVector.bitVector) Types.prod
  76
  77 val sub_7_with_carry :
  78   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  79   (BitVector.bitVector, BitVector.bitVector) Types.prod
  80
  81 val sub_8_with_carry :
  82   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  83   (BitVector.bitVector, BitVector.bitVector) Types.prod
  84
  85 val sub_16_with_carry :
  86   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  87   (BitVector.bitVector, BitVector.bitVector) Types.prod
  88
  89 val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
  90
  91 val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
  92
  93 val bitvector_of_nat_aux :
  94   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
  95
  96 val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector
  97
  98 val nat_of_bitvector_aux :
  99   Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat
 100
 101 val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat
 102
 103 val two_complement_negation :
 104   Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 105
 106 val addition_n :
 107   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 108   BitVector.bitVector
 109
 110 val subtraction :
 111   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 112   BitVector.bitVector
 113
 114 val mult_aux :
 115   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 116   BitVector.bitVector -> BitVector.bitVector
 117
 118 val multiplication :
 119   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 120   BitVector.bitVector
 121
 122 val short_multiplication :
 123   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 124   BitVector.bitVector
 125
 126 type fbs_diff =
 127 | Fbs_diff' of Nat.nat * Nat.nat
 128
 129 val fbs_diff_rect_Type4 :
 130   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 131
 132 val fbs_diff_rect_Type5 :
 133   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 134
 135 val fbs_diff_rect_Type3 :
 136   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 137
 138 val fbs_diff_rect_Type2 :
 139   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 140
 141 val fbs_diff_rect_Type1 :
 142   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 143
 144 val fbs_diff_rect_Type0 :
 145   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
 146
 147 val fbs_diff_inv_rect_Type4 :
 148   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
 149
 150 val fbs_diff_inv_rect_Type3 :
 151   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
 152
 153 val fbs_diff_inv_rect_Type2 :
 154   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
 155
 156 val fbs_diff_inv_rect_Type1 :
 157   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
 158
 159 val fbs_diff_inv_rect_Type0 :
 160   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
 161
 162 val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __
 163
 164 val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __
 165
 166 val first_bit_set : Nat.nat -> BitVector.bitVector -> fbs_diff Types.option
 167
 168 val divmod_u_aux :
 169   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 170   (BitVector.bitVector, BitVector.bitVector) Types.prod
 171
 172 val divmod_u :
 173   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 174   (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option
 175
 176 val division_u :
 177   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 178   BitVector.bitVector Types.option
 179
 180 val division_s :
 181   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 182   BitVector.bitVector Types.option
 183
 184 val modulus_u :
 185   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 186   BitVector.bitVector Types.option
 187
 188 val modulus_s :
 189   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 190   BitVector.bitVector Types.option
 191
 192 val lt_u :
 193   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 194
 195 val gt_u :
 196   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 197
 198 val lte_u :
 199   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 200
 201 val gte_u :
 202   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 203
 204 val lt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
 205
 206 val gt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
 207
 208 val lte_s :
 209   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
 210
 211 val gte_s :
 212   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
 213
 214 type ternary =
 215 | Zero_carry
 216 | One_carry
 217 | Two_carry
 218
 219 val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 220
 221 val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 222
 223 val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 224
 225 val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 226
 227 val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 228
 229 val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
 230
 231 val ternary_inv_rect_Type4 :
 232   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 233
 234 val ternary_inv_rect_Type3 :
 235   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 236
 237 val ternary_inv_rect_Type2 :
 238   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 239
 240 val ternary_inv_rect_Type1 :
 241   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 242
 243 val ternary_inv_rect_Type0 :
 244   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 245
 246 val ternary_discr : ternary -> ternary -> __
 247
 248 val ternary_jmdiscr : ternary -> ternary -> __
 249
 250 val carry_0 : ternary -> (Bool.bool, ternary) Types.prod
 251
 252 val carry_1 : ternary -> (Bool.bool, ternary) Types.prod
 253
 254 val carry_2 : ternary -> (Bool.bool, ternary) Types.prod
 255
 256 val carry_3 : ternary -> (Bool.bool, ternary) Types.prod
 257
 258 val ternary_carry_of :
 259   Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
 260   Types.prod
 261
 262 val canonical_add :
 263   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 264   BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary) Types.prod
 265
 266 val carries_to_ternary : Bool.bool -> Bool.bool -> ternary
 267
 268 val max_u :
 269   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 270   Vector.vector
 271
 272 val min_u :
 273   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
 274   Vector.vector
 275
 276 val max_s :
 277   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 278   BitVector.bitVector
 279
 280 val min_s :
 281   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 282   BitVector.bitVector
 283
 284 val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector
 285
 286 val full_add :
 287   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
 288   (BitVector.bit, BitVector.bitVector) Types.prod
 289
 290 val half_add :
 291   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
 292   BitVector.bitVector) Types.prod
 293
 294 val add :
 295   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 296   BitVector.bitVector
 297
 298 val sign_extension : BitVector.byte -> BitVector.word
 299
 300 val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool
 301
 302 val sign_extend :
 303   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 304
 305 val zero_ext :
 306   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 307
 308 val sign_ext :
 309   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 310