extracted/pointers.mli

   1 open Preamble
   2
   3 open Division
   4
   5 open Exp
   6
   7 open Arithmetic
   8
   9 open Setoids
  10
  11 open Monad
  12
  13 open Option
  14
  15 open Extranat
  16
  17 open Vector
  18
  19 open Div_and_mod
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 open List
  26
  27 open Util
  28
  29 open FoldStuff
  30
  31 open BitVector
  32
  33 open Types
  34
  35 open Bool
  36
  37 open Relations
  38
  39 open Nat
  40
  41 open Hints_declaration
  42
  43 open Core_notation
  44
  45 open Pts
  46
  47 open Logic
  48
  49 open Positive
  50
  51 open Z
  52
  53 open BitVectorZ
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Lists
  70
  71 open Identifiers
  72
  73 open Integers
  74
  75 open AST
  76
  77 type block =
  78   Z.z
  79   (* singleton inductive, whose constructor was mk_block *)
  80
  81 val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1
  82
  83 val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1
  84
  85 val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1
  86
  87 val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1
  88
  89 val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1
  90
  91 val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1
  92
  93 val block_id : block -> Z.z
  94
  95 val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1
  96
  97 val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1
  98
  99 val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1
 100
 101 val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1
 102
 103 val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1
 104
 105 val block_discr : block -> block -> __
 106
 107 val block_jmdiscr : block -> block -> __
 108
 109 val block_region : block -> AST.region
 110
 111 val dummy_block_code : block
 112
 113 val eq_block : block -> block -> Bool.bool
 114
 115 val block_eq : Deqsets.deqSet
 116
 117 val offset_size : Nat.nat
 118
 119 type offset =
 120   BitVector.bitVector
 121   (* singleton inductive, whose constructor was mk_offset *)
 122
 123 val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 124
 125 val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 126
 127 val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 128
 129 val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 130
 131 val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 132
 133 val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
 134
 135 val offv : offset -> BitVector.bitVector
 136
 137 val offset_inv_rect_Type4 :
 138   offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
 139
 140 val offset_inv_rect_Type3 :
 141   offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
 142
 143 val offset_inv_rect_Type2 :
 144   offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
 145
 146 val offset_inv_rect_Type1 :
 147   offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
 148
 149 val offset_inv_rect_Type0 :
 150   offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
 151
 152 val offset_discr : offset -> offset -> __
 153
 154 val offset_jmdiscr : offset -> offset -> __
 155
 156 val eq_offset : offset -> offset -> Bool.bool
 157
 158 val offset_of_Z : Z.z -> offset
 159
 160 val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
 161
 162 val shift_offset_n :
 163   Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 164   offset
 165
 166 val neg_shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
 167
 168 val neg_shift_offset_n :
 169   Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 170   offset
 171
 172 val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector
 173
 174 val zero_offset : offset
 175
 176 val lt_offset : offset -> offset -> Bool.bool
 177
 178 type pointer = { pblock : block; poff : offset }
 179
 180 val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1
 181
 182 val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1
 183
 184 val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1
 185
 186 val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1
 187
 188 val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1
 189
 190 val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1
 191
 192 val pblock : pointer -> block
 193
 194 val poff : pointer -> offset
 195
 196 val pointer_inv_rect_Type4 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
 197
 198 val pointer_inv_rect_Type3 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
 199
 200 val pointer_inv_rect_Type2 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
 201
 202 val pointer_inv_rect_Type1 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
 203
 204 val pointer_inv_rect_Type0 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
 205
 206 val pointer_discr : pointer -> pointer -> __
 207
 208 val pointer_jmdiscr : pointer -> pointer -> __
 209
 210 val ptype : pointer -> AST.region
 211
 212 val shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
 213
 214 val shift_pointer_n :
 215   Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 216   pointer
 217
 218 val neg_shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
 219
 220 val neg_shift_pointer_n :
 221   Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 222   pointer
 223
 224 val eq_pointer : pointer -> pointer -> Bool.bool
 225