extracted/globalenvs.mli

   1 open Preamble
   2
   3 open ErrorMessages
   4
   5 open Option
   6
   7 open Setoids
   8
   9 open Monad
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Positive
  16
  17 open PreIdentifiers
  18
  19 open Bool
  20
  21 open Relations
  22
  23 open Nat
  24
  25 open List
  26
  27 open Hints_declaration
  28
  29 open Core_notation
  30
  31 open Pts
  32
  33 open Logic
  34
  35 open Types
  36
  37 open Errors
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open Extralib
  46
  47 open Lists
  48
  49 open Identifiers
  50
  51 open Exp
  52
  53 open Arithmetic
  54
  55 open Vector
  56
  57 open Div_and_mod
  58
  59 open Util
  60
  61 open FoldStuff
  62
  63 open BitVector
  64
  65 open Extranat
  66
  67 open Integers
  68
  69 open AST
  70
  71 open Coqlib
  72
  73 open Values
  74
  75 open FrontEndVal
  76
  77 open Hide
  78
  79 open ByteValues
  80
  81 open Division
  82
  83 open Z
  84
  85 open BitVectorZ
  86
  87 open Pointers
  88
  89 open GenMem
  90
  91 open FrontEndMem
  92
  93 type 'f genv_t = { functions : 'f PositiveMap.positive_map;
  94                    nextfunction : Positive.pos;
  95                    symbols : Pointers.block Identifiers.identifier_map }
  96
  97 val genv_t_rect_Type4 :
  98   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  99   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 100
 101 val genv_t_rect_Type5 :
 102   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 103   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 104
 105 val genv_t_rect_Type3 :
 106   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 107   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 108
 109 val genv_t_rect_Type2 :
 110   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 111   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 112
 113 val genv_t_rect_Type1 :
 114   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 115   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 116
 117 val genv_t_rect_Type0 :
 118   ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 119   Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
 120
 121 val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map
 122
 123 val nextfunction : 'a1 genv_t -> Positive.pos
 124
 125 val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map
 126
 127 val genv_t_inv_rect_Type4 :
 128   'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 129   Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
 130
 131 val genv_t_inv_rect_Type3 :
 132   'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 133   Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
 134
 135 val genv_t_inv_rect_Type2 :
 136   'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 137   Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
 138
 139 val genv_t_inv_rect_Type1 :
 140   'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 141   Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
 142
 143 val genv_t_inv_rect_Type0 :
 144   'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 145   Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
 146
 147 val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __
 148
 149 val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __
 150
 151 val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t
 152
 153 val add_funct : (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t
 154
 155 val add_symbol : AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t
 156
 157 val empty_mem : GenMem.mem
 158
 159 val empty : 'a1 genv_t
 160
 161 val add_functs :
 162   'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t
 163
 164 val find_symbol : 'a1 genv_t -> AST.ident -> Pointers.block Types.option
 165
 166 val store_init_data :
 167   'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
 168   GenMem.mem Types.option
 169
 170 val size_init_data : AST.init_data -> Nat.nat
 171
 172 val store_init_data_list :
 173   'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
 174   List.list -> GenMem.mem Types.option
 175
 176 val size_init_data_list : AST.init_data List.list -> Nat.nat
 177
 178 val add_globals :
 179   ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod ->
 180   ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
 181   genv_t, GenMem.mem) Types.prod
 182
 183 val init_globals :
 184   ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
 185   ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
 186   GenMem.mem Errors.res
 187
 188 val globalenv_allocmem :
 189   ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1 genv_t,
 190   GenMem.mem) Types.prod
 191
 192 val globalenv :
 193   ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t
 194
 195 val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t
 196
 197 val init_mem :
 198   ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
 199   Errors.res
 200
 201 val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem
 202
 203 val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option
 204
 205 val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option
 206
 207 val symbol_for_block : 'a1 genv_t -> Pointers.block -> AST.ident Types.option
 208
 209 val symbol_of_function_block : 'a1 genv_t -> Pointers.block -> AST.ident
 210
 211 val symbol_of_function_block' :
 212   'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident
 213
 214 val find_funct_ptr_id :
 215   'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option
 216
 217 val opt_eq_from_res__o__ffpi_drop__o__inject :
 218   Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 219   Types.sig0
 220
 221 val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 222   Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
 223   'a2) Types.dPair -> __ Types.sig0
 224
 225 val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 226   Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 227   Types.sig0 -> __ Types.sig0
 228
 229 val jmeq_to_eq__o__ffpi_drop__o__inject :
 230   Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
 231
 232 val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 233   Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 234   Types.sig0
 235
 236 val dpi1__o__ffpi_drop__o__inject :
 237   Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
 238   -> __ Types.sig0
 239
 240 val eject__o__ffpi_drop__o__inject :
 241   Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
 242   Types.sig0
 243
 244 val ffpi_drop__o__inject :
 245   Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
 246
 247 val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident
 248
 249 val symbol_of_function_val' : 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident
 250
 251 val find_funct_id :
 252   'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option
 253
 254 val opt_eq_from_res__o__ffi_drop__o__inject :
 255   Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 256   Types.sig0
 257
 258 val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
 259   Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2)
 260   Types.dPair -> __ Types.sig0
 261
 262 val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
 263   Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 264   Types.sig0 -> __ Types.sig0
 265
 266 val jmeq_to_eq__o__ffi_drop__o__inject :
 267   Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
 268
 269 val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
 270   Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 271   Types.sig0
 272
 273 val dpi1__o__ffi_drop__o__inject :
 274   Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
 275   __ Types.sig0
 276
 277 val eject__o__ffi_drop__o__inject :
 278   Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
 279   Types.sig0
 280
 281 val ffi_drop__o__inject :
 282   Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
 283
 284 val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
 285
 286 val alloc_pair :
 287   GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
 288   GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1
 289
 290 val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
 291
 292 val related_globals_rect_Type4 :
 293   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 294   -> 'a3
 295
 296 val related_globals_rect_Type5 :
 297   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 298   -> 'a3
 299
 300 val related_globals_rect_Type3 :
 301   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 302   -> 'a3
 303
 304 val related_globals_rect_Type2 :
 305   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 306   -> 'a3
 307
 308 val related_globals_rect_Type1 :
 309   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 310   -> 'a3
 311
 312 val related_globals_rect_Type0 :
 313   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 314   -> 'a3
 315
 316 val related_globals_inv_rect_Type4 :
 317   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
 318   'a3) -> 'a3
 319
 320 val related_globals_inv_rect_Type3 :
 321   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
 322   'a3) -> 'a3
 323
 324 val related_globals_inv_rect_Type2 :
 325   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
 326   'a3) -> 'a3
 327
 328 val related_globals_inv_rect_Type1 :
 329   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
 330   'a3) -> 'a3
 331
 332 val related_globals_inv_rect_Type0 :
 333   ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
 334   'a3) -> 'a3
 335
 336 val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
 337
 338 val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
 339
 340 val related_globals_gen_rect_Type4 :
 341   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 342   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 343   -> __ -> __ -> 'a3) -> 'a3
 344
 345 val related_globals_gen_rect_Type5 :
 346   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 347   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 348   -> __ -> __ -> 'a3) -> 'a3
 349
 350 val related_globals_gen_rect_Type3 :
 351   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 352   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 353   -> __ -> __ -> 'a3) -> 'a3
 354
 355 val related_globals_gen_rect_Type2 :
 356   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 357   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 358   -> __ -> __ -> 'a3) -> 'a3
 359
 360 val related_globals_gen_rect_Type1 :
 361   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 362   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 363   -> __ -> __ -> 'a3) -> 'a3
 364
 365 val related_globals_gen_rect_Type0 :
 366   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 367   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 368   -> __ -> __ -> 'a3) -> 'a3
 369
 370 val related_globals_gen_inv_rect_Type4 :
 371   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 372   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 373   -> __ -> __ -> __ -> 'a3) -> 'a3
 374
 375 val related_globals_gen_inv_rect_Type3 :
 376   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 377   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 378   -> __ -> __ -> __ -> 'a3) -> 'a3
 379
 380 val related_globals_gen_inv_rect_Type2 :
 381   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 382   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 383   -> __ -> __ -> __ -> 'a3) -> 'a3
 384
 385 val related_globals_gen_inv_rect_Type1 :
 386   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 387   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 388   -> __ -> __ -> __ -> 'a3) -> 'a3
 389
 390 val related_globals_gen_inv_rect_Type0 :
 391   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 392   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
 393   -> __ -> __ -> __ -> 'a3) -> 'a3
 394
 395 val related_globals_gen_discr :
 396   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 397   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
 398
 399 val related_globals_gen_jmdiscr :
 400   PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 401   Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
 402
 403 open Extra_bool
 404