extracted/genMem.mli

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open Proper
  32
  33 open PositiveMap
  34
  35 open Deqsets
  36
  37 open ErrorMessages
  38
  39 open PreIdentifiers
  40
  41 open Errors
  42
  43 open Lists
  44
  45 open Identifiers
  46
  47 open Integers
  48
  49 open AST
  50
  51 open Division
  52
  53 open Exp
  54
  55 open Arithmetic
  56
  57 open Setoids
  58
  59 open Monad
  60
  61 open Option
  62
  63 open Extranat
  64
  65 open Vector
  66
  67 open FoldStuff
  68
  69 open BitVector
  70
  71 open Positive
  72
  73 open Z
  74
  75 open BitVectorZ
  76
  77 open Pointers
  78
  79 open Hide
  80
  81 open ByteValues
  82
  83 val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
  84
  85 val update_block :
  86   Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1
  87
  88 type contentmap = Z.z -> ByteValues.beval
  89
  90 type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
  91
  92 val block_contents_rect_Type4 :
  93   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
  94
  95 val block_contents_rect_Type5 :
  96   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
  97
  98 val block_contents_rect_Type3 :
  99   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
 100
 101 val block_contents_rect_Type2 :
 102   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
 103
 104 val block_contents_rect_Type1 :
 105   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
 106
 107 val block_contents_rect_Type0 :
 108   (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
 109
 110 val low : block_contents -> Z.z
 111
 112 val high : block_contents -> Z.z
 113
 114 val contents : block_contents -> contentmap
 115
 116 val block_contents_inv_rect_Type4 :
 117   block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
 118
 119 val block_contents_inv_rect_Type3 :
 120   block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
 121
 122 val block_contents_inv_rect_Type2 :
 123   block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
 124
 125 val block_contents_inv_rect_Type1 :
 126   block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
 127
 128 val block_contents_inv_rect_Type0 :
 129   block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
 130
 131 val block_contents_discr : block_contents -> block_contents -> __
 132
 133 val block_contents_jmdiscr : block_contents -> block_contents -> __
 134
 135 type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
 136
 137 val mem_rect_Type4 :
 138   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 139
 140 val mem_rect_Type5 :
 141   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 142
 143 val mem_rect_Type3 :
 144   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 145
 146 val mem_rect_Type2 :
 147   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 148
 149 val mem_rect_Type1 :
 150   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 151
 152 val mem_rect_Type0 :
 153   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
 154
 155 val blocks : mem -> Pointers.block -> block_contents
 156
 157 val nextblock : mem -> Z.z
 158
 159 val mem_inv_rect_Type4 :
 160   mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 161   'a1
 162
 163 val mem_inv_rect_Type3 :
 164   mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 165   'a1
 166
 167 val mem_inv_rect_Type2 :
 168   mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 169   'a1
 170
 171 val mem_inv_rect_Type1 :
 172   mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 173   'a1
 174
 175 val mem_inv_rect_Type0 :
 176   mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 177   'a1
 178
 179 val mem_discr : mem -> mem -> __
 180
 181 val mem_jmdiscr : mem -> mem -> __
 182
 183 val oneZ : Z.z
 184
 185 val empty_block : Z.z -> Z.z -> block_contents
 186
 187 val empty : mem
 188
 189 val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod
 190
 191 val free : mem -> Pointers.block -> mem
 192
 193 val free_list : mem -> Pointers.block List.list -> mem
 194
 195 val low_bound : mem -> Pointers.block -> Z.z
 196
 197 val high_bound : mem -> Pointers.block -> Z.z
 198
 199 val block_region : mem -> Pointers.block -> AST.region
 200
 201 val do_if_in_bounds :
 202   mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z -> 'a1)
 203   -> 'a1 Types.option
 204
 205 val beloadv : mem -> Pointers.pointer -> ByteValues.beval Types.option
 206
 207 val bestorev :
 208   mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option
 209