extracted/integers.mli

   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
  58 val comparison_rect_Type5 :
  59   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
  60
  61 val comparison_rect_Type3 :
  62   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
  63
  64 val comparison_rect_Type2 :
  65   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
  66
  67 val comparison_rect_Type1 :
  68   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
  69
  70 val comparison_rect_Type0 :
  71   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
  72
  73 val comparison_inv_rect_Type4 :
  74   comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  75   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  76
  77 val comparison_inv_rect_Type3 :
  78   comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  79   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  80
  81 val comparison_inv_rect_Type2 :
  82   comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  83   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  84
  85 val comparison_inv_rect_Type1 :
  86   comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  87   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  88
  89 val comparison_inv_rect_Type0 :
  90   comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  91   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  92
  93 val comparison_discr : comparison -> comparison -> __
  94
  95 val comparison_jmdiscr : comparison -> comparison -> __
  96
  97 val negate_comparison : comparison -> comparison
  98
  99 val swap_comparison : comparison -> comparison
 100
 101 val wordsize : Nat.nat
 102
 103 type int = BitVector.bitVector
 104
 105 val repr : Nat.nat -> int
 106
 107 val zero : int
 108
 109 val one : int
 110
 111 val mone : BitVector.bitVector
 112
 113 val iwordsize : int
 114
 115 val eq_dec : int -> int -> (__, __) Types.sum
 116
 117 val eq : int -> int -> Bool.bool
 118
 119 val lt : int -> int -> Bool.bool
 120
 121 val ltu : int -> int -> Bool.bool
 122
 123 val neg : int -> int
 124
 125 val mul :
 126   BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector
 127
 128 val zero_ext_n :
 129   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 130
 131 val zero_ext : Nat.nat -> int -> int
 132
 133 val sign_ext_n :
 134   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 135
 136 val sign_ext : Nat.nat -> int -> int
 137
 138 val i_and : int -> int -> int
 139
 140 val or0 : int -> int -> int
 141
 142 val xor : int -> int -> int
 143
 144 val not : int -> int
 145
 146 val shl : int -> int -> int
 147
 148 val shru : int -> int -> int
 149
 150 val shr : int -> int -> int
 151
 152 val shrx : int -> int -> int
 153
 154 val shr_carry : int -> int -> BitVector.bitVector
 155
 156 val rol : int -> int -> int
 157
 158 val ror : int -> int -> int
 159
 160 val rolm : int -> int -> int -> int
 161
 162 val cmp : comparison -> int -> int -> Bool.bool
 163
 164 val cmpu : comparison -> int -> int -> Bool.bool
 165
 166 val notbool : int -> int
 167