extracted/backEndOps.mli

   1 open Preamble
   2
   3 open Hide
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open Div_and_mod
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Util
  52
  53 open FoldStuff
  54
  55 open BitVector
  56
  57 open Types
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Positive
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 open ByteValues
  82
  83 val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod
  84
  85 type opAccs =
  86 | Mul
  87 | DivuModu
  88
  89 val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1
  90
  91 val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1
  92
  93 val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1
  94
  95 val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1
  96
  97 val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1
  98
  99 val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1
 100
 101 val opAccs_inv_rect_Type4 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 102
 103 val opAccs_inv_rect_Type3 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 104
 105 val opAccs_inv_rect_Type2 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 106
 107 val opAccs_inv_rect_Type1 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 108
 109 val opAccs_inv_rect_Type0 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 110
 111 val opAccs_discr : opAccs -> opAccs -> __
 112
 113 val opAccs_jmdiscr : opAccs -> opAccs -> __
 114
 115 type op1 =
 116 | Cmpl
 117 | Inc
 118 | Rl
 119
 120 val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 121
 122 val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 123
 124 val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 125
 126 val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 127
 128 val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 129
 130 val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
 131
 132 val op1_inv_rect_Type4 :
 133   op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 134
 135 val op1_inv_rect_Type3 :
 136   op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 137
 138 val op1_inv_rect_Type2 :
 139   op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 140
 141 val op1_inv_rect_Type1 :
 142   op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 143
 144 val op1_inv_rect_Type0 :
 145   op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 146
 147 val op1_discr : op1 -> op1 -> __
 148
 149 val op1_jmdiscr : op1 -> op1 -> __
 150
 151 type op2 =
 152 | Add
 153 | Addc
 154 | Sub
 155 | And
 156 | Or
 157 | Xor
 158
 159 val op2_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 160
 161 val op2_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 162
 163 val op2_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 164
 165 val op2_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 166
 167 val op2_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 168
 169 val op2_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
 170
 171 val op2_inv_rect_Type4 :
 172   op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 173   'a1) -> (__ -> 'a1) -> 'a1
 174
 175 val op2_inv_rect_Type3 :
 176   op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 177   'a1) -> (__ -> 'a1) -> 'a1
 178
 179 val op2_inv_rect_Type2 :
 180   op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 181   'a1) -> (__ -> 'a1) -> 'a1
 182
 183 val op2_inv_rect_Type1 :
 184   op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 185   'a1) -> (__ -> 'a1) -> 'a1
 186
 187 val op2_inv_rect_Type0 :
 188   op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 189   'a1) -> (__ -> 'a1) -> 'a1
 190
 191 val op2_discr : op2 -> op2 -> __
 192
 193 val op2_jmdiscr : op2 -> op2 -> __
 194
 195 type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
 196                        (BitVector.byte, BitVector.byte) Types.prod);
 197               op0 : (op1 -> BitVector.byte -> BitVector.byte);
 198               op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
 199                     -> (BitVector.byte, BitVector.bit) Types.prod) }
 200
 201 val eval_rect_Type4 :
 202   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 203   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 204   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 205   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 206
 207 val eval_rect_Type5 :
 208   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 209   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 210   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 211   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 212
 213 val eval_rect_Type3 :
 214   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 215   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 216   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 217   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 218
 219 val eval_rect_Type2 :
 220   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 221   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 222   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 223   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 224
 225 val eval_rect_Type1 :
 226   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 227   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 228   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 229   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 230
 231 val eval_rect_Type0 :
 232   ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 233   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 234   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 235   (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
 236
 237 val opaccs :
 238   eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 239   BitVector.byte) Types.prod
 240
 241 val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte
 242
 243 val op3 :
 244   eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 245   (BitVector.byte, BitVector.bit) Types.prod
 246
 247 val eval_inv_rect_Type4 :
 248   eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 249   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 250   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 251   (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
 252
 253 val eval_inv_rect_Type3 :
 254   eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 255   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 256   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 257   (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
 258
 259 val eval_inv_rect_Type2 :
 260   eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 261   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 262   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 263   (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
 264
 265 val eval_inv_rect_Type1 :
 266   eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 267   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 268   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 269   (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
 270
 271 val eval_inv_rect_Type0 :
 272   eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 273   BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
 274   (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 275   (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
 276
 277 val eval_discr : eval -> eval -> __
 278
 279 val eval_jmdiscr : eval -> eval -> __
 280
 281 val opaccs_implementation :
 282   opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 283   BitVector.byte) Types.prod
 284
 285 val op1_implementation : op1 -> BitVector.byte -> BitVector.byte
 286
 287 val op2_implementation :
 288   BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 289   (BitVector.byte, BitVector.bit) Types.prod
 290
 291 val eval0 : eval
 292
 293 val be_opaccs :
 294   opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
 295   ByteValues.beval) Types.prod Errors.res
 296
 297 val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res
 298
 299 val op2_bytes :
 300   op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
 301   BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
 302   BitVector.bit) Types.prod
 303
 304 val op_of_add_or_sub : ByteValues.add_or_sub -> op2
 305
 306 val be_add_sub_byte :
 307   ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
 308   BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
 309   Errors.res
 310
 311 val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
 312
 313 val eq_opt :
 314   ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
 315   Bool.bool
 316
 317 val be_op2 :
 318   ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
 319   (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
 320