extracted/globalenvs.ml

   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 let rec genv_t_rect_Type4 h_mk_genv_t x_6621 =
 101   let { functions = functions0; nextfunction = nextfunction0; symbols =
 102     symbols0 } = x_6621
 103   in
 104   h_mk_genv_t functions0 nextfunction0 symbols0 __
 105
 106 (** val genv_t_rect_Type5 :
 107     ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 108     Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
 109 let rec genv_t_rect_Type5 h_mk_genv_t x_6623 =
 110   let { functions = functions0; nextfunction = nextfunction0; symbols =
 111     symbols0 } = x_6623
 112   in
 113   h_mk_genv_t functions0 nextfunction0 symbols0 __
 114
 115 (** val genv_t_rect_Type3 :
 116     ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 117     Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
 118 let rec genv_t_rect_Type3 h_mk_genv_t x_6625 =
 119   let { functions = functions0; nextfunction = nextfunction0; symbols =
 120     symbols0 } = x_6625
 121   in
 122   h_mk_genv_t functions0 nextfunction0 symbols0 __
 123
 124 (** val genv_t_rect_Type2 :
 125     ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 126     Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
 127 let rec genv_t_rect_Type2 h_mk_genv_t x_6627 =
 128   let { functions = functions0; nextfunction = nextfunction0; symbols =
 129     symbols0 } = x_6627
 130   in
 131   h_mk_genv_t functions0 nextfunction0 symbols0 __
 132
 133 (** val genv_t_rect_Type1 :
 134     ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 135     Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
 136 let rec genv_t_rect_Type1 h_mk_genv_t x_6629 =
 137   let { functions = functions0; nextfunction = nextfunction0; symbols =
 138     symbols0 } = x_6629
 139   in
 140   h_mk_genv_t functions0 nextfunction0 symbols0 __
 141
 142 (** val genv_t_rect_Type0 :
 143     ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
 144     Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
 145 let rec genv_t_rect_Type0 h_mk_genv_t x_6631 =
 146   let { functions = functions0; nextfunction = nextfunction0; symbols =
 147     symbols0 } = x_6631
 148   in
 149   h_mk_genv_t functions0 nextfunction0 symbols0 __
 150
 151 (** val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map **)
 152 let rec functions xxx =
 153   xxx.functions
 154
 155 (** val nextfunction : 'a1 genv_t -> Positive.pos **)
 156 let rec nextfunction xxx =
 157   xxx.nextfunction
 158
 159 (** val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map **)
 160 let rec symbols xxx =
 161   xxx.symbols
 162
 163 (** val genv_t_inv_rect_Type4 :
 164     'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 165     Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
 166 let genv_t_inv_rect_Type4 hterm h1 =
 167   let hcut = genv_t_rect_Type4 h1 hterm in hcut __
 168
 169 (** val genv_t_inv_rect_Type3 :
 170     'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 171     Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
 172 let genv_t_inv_rect_Type3 hterm h1 =
 173   let hcut = genv_t_rect_Type3 h1 hterm in hcut __
 174
 175 (** val genv_t_inv_rect_Type2 :
 176     'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 177     Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
 178 let genv_t_inv_rect_Type2 hterm h1 =
 179   let hcut = genv_t_rect_Type2 h1 hterm in hcut __
 180
 181 (** val genv_t_inv_rect_Type1 :
 182     'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 183     Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
 184 let genv_t_inv_rect_Type1 hterm h1 =
 185   let hcut = genv_t_rect_Type1 h1 hterm in hcut __
 186
 187 (** val genv_t_inv_rect_Type0 :
 188     'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
 189     Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
 190 let genv_t_inv_rect_Type0 hterm h1 =
 191   let hcut = genv_t_rect_Type0 h1 hterm in hcut __
 192
 193 (** val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __ **)
 194 let genv_t_discr x y =
 195   Logic.eq_rect_Type2 x
 196     (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
 197     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 198
 199 (** val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __ **)
 200 let genv_t_jmdiscr x y =
 201   Logic.eq_rect_Type2 x
 202     (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
 203     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 204
 205 (** val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t **)
 206 let drop_fn id g =
 207   let fns =
 208     match Identifiers.lookup PreIdentifiers.SymbolTag g.symbols id with
 209     | Types.None -> g.functions
 210     | Types.Some b' ->
 211       (match Pointers.block_id b' with
 212        | Z.OZ -> g.functions
 213        | Z.Pos x -> g.functions
 214        | Z.Neg p -> PositiveMap.pm_set p Types.None g.functions)
 215   in
 216   { functions = fns; nextfunction = g.nextfunction; symbols =
 217   (Identifiers.remove PreIdentifiers.SymbolTag g.symbols id) }
 218
 219 (** val add_funct :
 220     (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
 221 let add_funct name_fun g =
 222   let blk_id = g.nextfunction in
 223   let b = Z.Neg blk_id in
 224   let g' = drop_fn name_fun.Types.fst g in
 225   { functions = (PositiveMap.insert blk_id name_fun.Types.snd g'.functions);
 226   nextfunction = (Positive.succ blk_id); symbols =
 227   (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name_fun.Types.fst b) }
 228
 229 (** val add_symbol :
 230     AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t **)
 231 let add_symbol name b g =
 232   let g' = drop_fn name g in
 233   { functions = g'.functions; nextfunction = g'.nextfunction; symbols =
 234   (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name b) }
 235
 236 (** val empty_mem : GenMem.mem **)
 237 let empty_mem =
 238   GenMem.empty
 239
 240 (** val empty : 'a1 genv_t **)
 241 let empty =
 242   { functions = PositiveMap.Pm_leaf; nextfunction =
 243     (Positive.succ_pos_of_nat (Nat.S (Nat.S Nat.O))); symbols =
 244     (Identifiers.empty_map PreIdentifiers.SymbolTag) }
 245
 246 (** val add_functs :
 247     'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t **)
 248 let add_functs init fns =
 249   List.foldr add_funct init fns
 250
 251 (** val find_symbol :
 252     'a1 genv_t -> AST.ident -> Pointers.block Types.option **)
 253 let find_symbol ge =
 254   Identifiers.lookup PreIdentifiers.SymbolTag ge.symbols
 255
 256 (** val store_init_data :
 257     'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
 258     GenMem.mem Types.option **)
 259 let store_init_data ge m b p id =
 260   let ptr = { Pointers.pblock = b; Pointers.poff =
 261     (BitVectorZ.bitvector_of_Z Pointers.offset_size p) }
 262   in
 263   (match id with
 264    | AST.Init_int8 n ->
 265      FrontEndMem.store (AST.ASTint (AST.I8, AST.Unsigned)) m ptr (Values.Vint
 266        (AST.I8, n))
 267    | AST.Init_int16 n ->
 268      FrontEndMem.store (AST.ASTint (AST.I16, AST.Unsigned)) m ptr
 269        (Values.Vint (AST.I16, n))
 270    | AST.Init_int32 n ->
 271      FrontEndMem.store (AST.ASTint (AST.I32, AST.Unsigned)) m ptr
 272        (Values.Vint (AST.I32, n))
 273    | AST.Init_space n -> Types.Some m
 274    | AST.Init_null -> FrontEndMem.store AST.ASTptr m ptr Values.Vnull
 275    | AST.Init_addrof (symb, ofs) ->
 276      (match find_symbol ge symb with
 277       | Types.None -> Types.None
 278       | Types.Some b' ->
 279         FrontEndMem.store AST.ASTptr m ptr (Values.Vptr { Pointers.pblock =
 280           b'; Pointers.poff =
 281           (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
 282             Pointers.zero_offset (AST.repr AST.I16 ofs)) })))
 283
 284 (** val size_init_data : AST.init_data -> Nat.nat **)
 285 let size_init_data = function
 286 | AST.Init_int8 x -> Nat.S Nat.O
 287 | AST.Init_int16 x -> Nat.S (Nat.S Nat.O)
 288 | AST.Init_int32 x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
 289 | AST.Init_space n -> Nat.max n Nat.O
 290 | AST.Init_null -> AST.size_pointer
 291 | AST.Init_addrof (x, x0) -> AST.size_pointer
 292
 293 (** val store_init_data_list :
 294     'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
 295     List.list -> GenMem.mem Types.option **)
 296 let rec store_init_data_list ge m b p = function
 297 | List.Nil -> Types.Some m
 298 | List.Cons (id, idl') ->
 299   (match store_init_data ge m b p id with
 300    | Types.None -> Types.None
 301    | Types.Some m' ->
 302      store_init_data_list ge m' b
 303        (Z.zplus p (Z.z_of_nat (size_init_data id))) idl')
 304
 305 (** val size_init_data_list : AST.init_data List.list -> Nat.nat **)
 306 let size_init_data_list i_data =
 307   List.foldr (fun i_data0 sz -> Nat.plus (size_init_data i_data0) sz) Nat.O
 308     i_data
 309
 310 (** val add_globals :
 311     ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod
 312     -> ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
 313     genv_t, GenMem.mem) Types.prod **)
 314 let add_globals extract_init init_env vars =
 315   Util.foldl (fun g_st id_init ->
 316     let { Types.fst = eta1345; Types.snd = init_info } = id_init in
 317     let { Types.fst = id; Types.snd = r } = eta1345 in
 318     let init = extract_init init_info in
 319     let { Types.fst = g; Types.snd = st } = g_st in
 320     let { Types.fst = st'; Types.snd = b } =
 321       GenMem.alloc st Z.OZ (Z.z_of_nat (size_init_data_list init))
 322     in
 323     let g' = add_symbol id b g in { Types.fst = g'; Types.snd = st' })
 324     init_env vars
 325
 326 (** val init_globals :
 327     ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
 328     ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
 329     GenMem.mem Errors.res **)
 330 let init_globals extract_init g m vars =
 331   Util.foldl (fun st id_init ->
 332     let { Types.fst = eta1346; Types.snd = init_info } = id_init in
 333     let { Types.fst = id; Types.snd = r } = eta1346 in
 334     let init = extract_init init_info in
 335     Obj.magic
 336       (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
 337         match find_symbol g id with
 338         | Types.None ->
 339           Obj.magic (Errors.Error
 340             (Errors.msg ErrorMessages.InitDataStoreFailed))
 341         | Types.Some b ->
 342           Obj.magic
 343             (Errors.opt_to_res (Errors.msg ErrorMessages.InitDataStoreFailed)
 344               (store_init_data_list g st0 b Z.OZ init))))) (Errors.OK m) vars
 345
 346 (** val globalenv_allocmem :
 347     ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
 348     genv_t, GenMem.mem) Types.prod **)
 349 let globalenv_allocmem init_info p =
 350   add_globals init_info { Types.fst = (add_functs empty p.AST.prog_funct);
 351     Types.snd = empty_mem } p.AST.prog_vars
 352
 353 (** val globalenv :
 354     ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t **)
 355 let globalenv i p =
 356   (globalenv_allocmem i p).Types.fst
 357
 358 (** val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t **)
 359 let globalenv_noinit p =
 360   globalenv (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p
 361
 362 (** val init_mem :
 363     ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
 364     Errors.res **)
 365 let init_mem i p =
 366   let { Types.fst = g; Types.snd = m } = globalenv_allocmem i p in
 367   init_globals i g m p.AST.prog_vars
 368
 369 (** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem **)
 370 let alloc_mem p =
 371   (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd
 372
 373 (** val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option **)
 374 let find_funct_ptr ge b =
 375   match Pointers.block_region b with
 376   | AST.XData -> Types.None
 377   | AST.Code ->
 378     (match Pointers.block_id b with
 379      | Z.OZ -> Types.None
 380      | Z.Pos x -> Types.None
 381      | Z.Neg p -> PositiveMap.lookup_opt p ge.functions)
 382
 383 (** val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option **)
 384 let find_funct ge = function
 385 | Values.Vundef -> Types.None
 386 | Values.Vint (x, x0) -> Types.None
 387 | Values.Vnull -> Types.None
 388 | Values.Vptr ptr ->
 389   (match Pointers.eq_offset ptr.Pointers.poff Pointers.zero_offset with
 390    | Bool.True -> find_funct_ptr ge ptr.Pointers.pblock
 391    | Bool.False -> Types.None)
 392
 393 (** val symbol_for_block :
 394     'a1 genv_t -> Pointers.block -> AST.ident Types.option **)
 395 let symbol_for_block genv b =
 396   Types.option_map Types.fst
 397     (Identifiers.find PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
 398       Pointers.eq_block b b'))
 399
 400 (** val symbol_of_function_block :
 401     'a1 genv_t -> Pointers.block -> AST.ident **)
 402 let symbol_of_function_block ge b =
 403   (match symbol_for_block ge b with
 404    | Types.None -> (fun _ -> assert false (* absurd case *))
 405    | Types.Some id -> (fun _ -> id)) __
 406
 407 (** val symbol_of_function_block' :
 408     'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
 409 let symbol_of_function_block' ge b f =
 410   symbol_of_function_block ge b
 411
 412 (** val find_funct_ptr_id :
 413     'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
 414 let find_funct_ptr_id ge b =
 415   (match find_funct_ptr ge b with
 416    | Types.None -> (fun _ -> Types.None)
 417    | Types.Some f ->
 418      (fun _ -> Types.Some { Types.fst = f; Types.snd =
 419        (symbol_of_function_block' ge b f) })) __
 420
 421 (** val opt_eq_from_res__o__ffpi_drop__o__inject :
 422     Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 423     Types.sig0 **)
 424 let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
 425   __
 426
 427 (** val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 428     Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
 429     'a2) Types.dPair -> __ Types.sig0 **)
 430 let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
 431   __
 432
 433 (** val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 434     Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 435     Types.sig0 -> __ Types.sig0 **)
 436 let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
 437   __
 438
 439 (** val jmeq_to_eq__o__ffpi_drop__o__inject :
 440     Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
 441 let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
 442   __
 443
 444 (** val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
 445     Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 446     Types.sig0 **)
 447 let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
 448   __
 449
 450 (** val dpi1__o__ffpi_drop__o__inject :
 451     Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
 452     -> __ Types.sig0 **)
 453 let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
 454   __
 455
 456 (** val eject__o__ffpi_drop__o__inject :
 457     Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
 458     Types.sig0 **)
 459 let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
 460   __
 461
 462 (** val ffpi_drop__o__inject :
 463     Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
 464 let ffpi_drop__o__inject x1 x2 x3 x4 =
 465   __
 466
 467 (** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
 468 let symbol_of_function_val ge v =
 469   (match v with
 470    | Values.Vundef -> (fun _ -> assert false (* absurd case *))
 471    | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
 472    | Values.Vnull -> (fun _ -> assert false (* absurd case *))
 473    | Values.Vptr p ->
 474      (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
 475
 476 (** val symbol_of_function_val' :
 477     'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
 478 let symbol_of_function_val' ge v f =
 479   symbol_of_function_val ge v
 480
 481 (** val find_funct_id :
 482     'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
 483 let find_funct_id ge v =
 484   (match find_funct ge v with
 485    | Types.None -> (fun _ -> Types.None)
 486    | Types.Some f ->
 487      (fun _ -> Types.Some { Types.fst = f; Types.snd =
 488        (symbol_of_function_val' ge v f) })) __
 489
 490 (** val opt_eq_from_res__o__ffi_drop__o__inject :
 491     Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 492     Types.sig0 **)
 493 let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
 494   __
 495
 496 (** val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
 497     Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
 498     'a2) Types.dPair -> __ Types.sig0 **)
 499 let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
 500   __
 501
 502 (** val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
 503     Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 504     Types.sig0 -> __ Types.sig0 **)
 505 let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
 506   __
 507
 508 (** val jmeq_to_eq__o__ffi_drop__o__inject :
 509     Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
 510 let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
 511   __
 512
 513 (** val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
 514     Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
 515     Types.sig0 **)
 516 let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
 517   __
 518
 519 (** val dpi1__o__ffi_drop__o__inject :
 520     Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
 521     __ Types.sig0 **)
 522 let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
 523   __
 524
 525 (** val eject__o__ffi_drop__o__inject :
 526     Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
 527     Types.sig0 **)
 528 let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
 529   __
 530
 531 (** val ffi_drop__o__inject :
 532     Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
 533 let ffi_drop__o__inject x1 x2 x3 x4 =
 534   __
 535
 536 (** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
 537 let rec nat_plus_pos n p =
 538   match n with
 539   | Nat.O -> p
 540   | Nat.S m -> Positive.succ (nat_plus_pos m p)
 541
 542 (** val alloc_pair :
 543     GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
 544     GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1 **)
 545 let alloc_pair clearme m' l h l' h' x =
 546   (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
 547   (fun clearme0 ->
 548   let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
 549   (fun l0 h0 l'0 h'0 _ _ ->
 550   Extralib.eq_rect_Type0_r nx' (fun _ h1 ->
 551     h1 { GenMem.blocks =
 552       (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
 553         nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
 554         ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
 555       (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
 556         nx' }.GenMem.nextblock) } { GenMem.blocks =
 557       (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
 558         nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
 559         ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
 560       (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
 561         nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
 562       nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
 563
 564 (** val prod_jmdiscr :
 565     ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
 566 let prod_jmdiscr x y =
 567   Logic.eq_rect_Type2 x
 568     (let { Types.fst = a0; Types.snd = a10 } = x in
 569     Obj.magic (fun _ dH -> dH __ __)) y
 570
 571 (** val related_globals_rect_Type4 :
 572     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 573     -> 'a3 **)
 574 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
 575   h_mk_related_globals __ __ __ __
 576
 577 (** val related_globals_rect_Type5 :
 578     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 579     -> 'a3 **)
 580 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
 581   h_mk_related_globals __ __ __ __
 582
 583 (** val related_globals_rect_Type3 :
 584     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 585     -> 'a3 **)
 586 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
 587   h_mk_related_globals __ __ __ __
 588
 589 (** val related_globals_rect_Type2 :
 590     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 591     -> 'a3 **)
 592 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
 593   h_mk_related_globals __ __ __ __
 594
 595 (** val related_globals_rect_Type1 :
 596     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 597     -> 'a3 **)
 598 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
 599   h_mk_related_globals __ __ __ __
 600
 601 (** val related_globals_rect_Type0 :
 602     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
 603     -> 'a3 **)
 604 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
 605   h_mk_related_globals __ __ __ __
 606
 607 (** val related_globals_inv_rect_Type4 :
 608     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
 609     -> 'a3) -> 'a3 **)
 610 let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
 611   let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
 612
 613 (** val related_globals_inv_rect_Type3 :
 614     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
 615     -> 'a3) -> 'a3 **)
 616 let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
 617   let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
 618
 619 (** val related_globals_inv_rect_Type2 :
 620     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
 621     -> 'a3) -> 'a3 **)
 622 let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
 623   let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
 624
 625 (** val related_globals_inv_rect_Type1 :
 626     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
 627     -> 'a3) -> 'a3 **)
 628 let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
 629   let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
 630
 631 (** val related_globals_inv_rect_Type0 :
 632     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
 633     -> 'a3) -> 'a3 **)
 634 let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
 635   let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
 636
 637 (** val related_globals_discr :
 638     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
 639 let related_globals_discr a3 a4 a5 =
 640   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
 641
 642 (** val related_globals_jmdiscr :
 643     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
 644 let related_globals_jmdiscr a3 a4 a5 =
 645   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
 646
 647 (** val related_globals_gen_rect_Type4 :
 648     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 649     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 650     __ -> __ -> __ -> 'a3) -> 'a3 **)
 651 let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
 652   h_mk_related_globals_gen __ __ __ __
 653
 654 (** val related_globals_gen_rect_Type5 :
 655     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 656     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 657     __ -> __ -> __ -> 'a3) -> 'a3 **)
 658 let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
 659   h_mk_related_globals_gen __ __ __ __
 660
 661 (** val related_globals_gen_rect_Type3 :
 662     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 663     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 664     __ -> __ -> __ -> 'a3) -> 'a3 **)
 665 let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
 666   h_mk_related_globals_gen __ __ __ __
 667
 668 (** val related_globals_gen_rect_Type2 :
 669     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 670     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 671     __ -> __ -> __ -> 'a3) -> 'a3 **)
 672 let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
 673   h_mk_related_globals_gen __ __ __ __
 674
 675 (** val related_globals_gen_rect_Type1 :
 676     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 677     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 678     __ -> __ -> __ -> 'a3) -> 'a3 **)
 679 let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
 680   h_mk_related_globals_gen __ __ __ __
 681
 682 (** val related_globals_gen_rect_Type0 :
 683     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 684     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 685     __ -> __ -> __ -> 'a3) -> 'a3 **)
 686 let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
 687   h_mk_related_globals_gen __ __ __ __
 688
 689 (** val related_globals_gen_inv_rect_Type4 :
 690     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 691     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 692     __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
 693 let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
 694   let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
 695
 696 (** val related_globals_gen_inv_rect_Type3 :
 697     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 698     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 699     __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
 700 let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
 701   let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
 702
 703 (** val related_globals_gen_inv_rect_Type2 :
 704     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 705     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 706     __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
 707 let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
 708   let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
 709
 710 (** val related_globals_gen_inv_rect_Type1 :
 711     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 712     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 713     __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
 714 let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
 715   let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
 716
 717 (** val related_globals_gen_inv_rect_Type0 :
 718     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 719     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
 720     __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
 721 let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
 722   let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
 723
 724 (** val related_globals_gen_discr :
 725     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 726     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
 727 let related_globals_gen_discr a1 a4 a5 a6 =
 728   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
 729
 730 (** val related_globals_gen_jmdiscr :
 731     PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
 732     Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
 733 let related_globals_gen_jmdiscr a1 a4 a5 a6 =
 734   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
 735
 736 open Extra_bool
 737