extracted/csyntax.ml

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open ErrorMessages
  10
  11 open PreIdentifiers
  12
  13 open Errors
  14
  15 open Extralib
  16
  17 open Lists
  18
  19 open Positive
  20
  21 open Identifiers
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Vector
  28
  29 open Div_and_mod
  30
  31 open Util
  32
  33 open FoldStuff
  34
  35 open BitVector
  36
  37 open Jmeq
  38
  39 open Russell
  40
  41 open List
  42
  43 open Setoids
  44
  45 open Monad
  46
  47 open Option
  48
  49 open Extranat
  50
  51 open Bool
  52
  53 open Relations
  54
  55 open Nat
  56
  57 open Integers
  58
  59 open Hints_declaration
  60
  61 open Core_notation
  62
  63 open Pts
  64
  65 open Logic
  66
  67 open Types
  68
  69 open AST
  70
  71 open Coqlib
  72
  73 open CostLabel
  74
  75 type type0 =
  76 | Tvoid
  77 | Tint of AST.intsize * AST.signedness
  78 | Tpointer of type0
  79 | Tarray of type0 * Nat.nat
  80 | Tfunction of typelist * type0
  81 | Tstruct of AST.ident * fieldlist
  82 | Tunion of AST.ident * fieldlist
  83 | Tcomp_ptr of AST.ident
  84 and typelist =
  85 | Tnil
  86 | Tcons of type0 * typelist
  87 and fieldlist =
  88 | Fnil
  89 | Fcons of AST.ident * type0 * fieldlist
  90
  91 (** val type_inv_rect_Type4 :
  92     type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  93     (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  94     type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
  95     (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
  96 let type_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  97   let hcut =
  98     match hterm with
  99     | Tvoid -> h1
 100     | Tint (x, x0) -> h2 x x0
 101     | Tpointer x -> h3 x
 102     | Tarray (x, x0) -> h4 x x0
 103     | Tfunction (x, x0) -> h5 x x0
 104     | Tstruct (x, x0) -> h6 x x0
 105     | Tunion (x, x0) -> h7 x x0
 106     | Tcomp_ptr x -> h8 x
 107   in
 108   hcut __
 109
 110 (** val type_inv_rect_Type3 :
 111     type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
 112     (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
 113     type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
 114     (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
 115 let type_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 116   let hcut =
 117     match hterm with
 118     | Tvoid -> h1
 119     | Tint (x, x0) -> h2 x x0
 120     | Tpointer x -> h3 x
 121     | Tarray (x, x0) -> h4 x x0
 122     | Tfunction (x, x0) -> h5 x x0
 123     | Tstruct (x, x0) -> h6 x x0
 124     | Tunion (x, x0) -> h7 x x0
 125     | Tcomp_ptr x -> h8 x
 126   in
 127   hcut __
 128
 129 (** val type_inv_rect_Type2 :
 130     type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
 131     (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
 132     type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
 133     (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
 134 let type_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 135   let hcut =
 136     match hterm with
 137     | Tvoid -> h1
 138     | Tint (x, x0) -> h2 x x0
 139     | Tpointer x -> h3 x
 140     | Tarray (x, x0) -> h4 x x0
 141     | Tfunction (x, x0) -> h5 x x0
 142     | Tstruct (x, x0) -> h6 x x0
 143     | Tunion (x, x0) -> h7 x x0
 144     | Tcomp_ptr x -> h8 x
 145   in
 146   hcut __
 147
 148 (** val type_inv_rect_Type1 :
 149     type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
 150     (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
 151     type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
 152     (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
 153 let type_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 154   let hcut =
 155     match hterm with
 156     | Tvoid -> h1
 157     | Tint (x, x0) -> h2 x x0
 158     | Tpointer x -> h3 x
 159     | Tarray (x, x0) -> h4 x x0
 160     | Tfunction (x, x0) -> h5 x x0
 161     | Tstruct (x, x0) -> h6 x x0
 162     | Tunion (x, x0) -> h7 x x0
 163     | Tcomp_ptr x -> h8 x
 164   in
 165   hcut __
 166
 167 (** val type_inv_rect_Type0 :
 168     type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
 169     (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
 170     type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
 171     (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
 172 let type_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 173   let hcut =
 174     match hterm with
 175     | Tvoid -> h1
 176     | Tint (x, x0) -> h2 x x0
 177     | Tpointer x -> h3 x
 178     | Tarray (x, x0) -> h4 x x0
 179     | Tfunction (x, x0) -> h5 x x0
 180     | Tstruct (x, x0) -> h6 x x0
 181     | Tunion (x, x0) -> h7 x x0
 182     | Tcomp_ptr x -> h8 x
 183   in
 184   hcut __
 185
 186 (** val typelist_inv_rect_Type4 :
 187     typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
 188 let typelist_inv_rect_Type4 hterm h1 h2 =
 189   let hcut =
 190     match hterm with
 191     | Tnil -> h1
 192     | Tcons (x, x0) -> h2 x x0
 193   in
 194   hcut __
 195
 196 (** val typelist_inv_rect_Type3 :
 197     typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
 198 let typelist_inv_rect_Type3 hterm h1 h2 =
 199   let hcut =
 200     match hterm with
 201     | Tnil -> h1
 202     | Tcons (x, x0) -> h2 x x0
 203   in
 204   hcut __
 205
 206 (** val typelist_inv_rect_Type2 :
 207     typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
 208 let typelist_inv_rect_Type2 hterm h1 h2 =
 209   let hcut =
 210     match hterm with
 211     | Tnil -> h1
 212     | Tcons (x, x0) -> h2 x x0
 213   in
 214   hcut __
 215
 216 (** val typelist_inv_rect_Type1 :
 217     typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
 218 let typelist_inv_rect_Type1 hterm h1 h2 =
 219   let hcut =
 220     match hterm with
 221     | Tnil -> h1
 222     | Tcons (x, x0) -> h2 x x0
 223   in
 224   hcut __
 225
 226 (** val typelist_inv_rect_Type0 :
 227     typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
 228 let typelist_inv_rect_Type0 hterm h1 h2 =
 229   let hcut =
 230     match hterm with
 231     | Tnil -> h1
 232     | Tcons (x, x0) -> h2 x x0
 233   in
 234   hcut __
 235
 236 (** val fieldlist_inv_rect_Type4 :
 237     fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
 238     'a1) -> 'a1 **)
 239 let fieldlist_inv_rect_Type4 hterm h1 h2 =
 240   let hcut =
 241     match hterm with
 242     | Fnil -> h1
 243     | Fcons (x, x0, x1) -> h2 x x0 x1
 244   in
 245   hcut __
 246
 247 (** val fieldlist_inv_rect_Type3 :
 248     fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
 249     'a1) -> 'a1 **)
 250 let fieldlist_inv_rect_Type3 hterm h1 h2 =
 251   let hcut =
 252     match hterm with
 253     | Fnil -> h1
 254     | Fcons (x, x0, x1) -> h2 x x0 x1
 255   in
 256   hcut __
 257
 258 (** val fieldlist_inv_rect_Type2 :
 259     fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
 260     'a1) -> 'a1 **)
 261 let fieldlist_inv_rect_Type2 hterm h1 h2 =
 262   let hcut =
 263     match hterm with
 264     | Fnil -> h1
 265     | Fcons (x, x0, x1) -> h2 x x0 x1
 266   in
 267   hcut __
 268
 269 (** val fieldlist_inv_rect_Type1 :
 270     fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
 271     'a1) -> 'a1 **)
 272 let fieldlist_inv_rect_Type1 hterm h1 h2 =
 273   let hcut =
 274     match hterm with
 275     | Fnil -> h1
 276     | Fcons (x, x0, x1) -> h2 x x0 x1
 277   in
 278   hcut __
 279
 280 (** val fieldlist_inv_rect_Type0 :
 281     fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
 282     'a1) -> 'a1 **)
 283 let fieldlist_inv_rect_Type0 hterm h1 h2 =
 284   let hcut =
 285     match hterm with
 286     | Fnil -> h1
 287     | Fcons (x, x0, x1) -> h2 x x0 x1
 288   in
 289   hcut __
 290
 291 (** val type_discr : type0 -> type0 -> __ **)
 292 let type_discr x y =
 293   Logic.eq_rect_Type2 x
 294     (match x with
 295      | Tvoid -> Obj.magic (fun _ dH -> dH)
 296      | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 297      | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
 298      | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 299      | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 300      | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 301      | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 302      | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
 303
 304 (** val typelist_discr : typelist -> typelist -> __ **)
 305 let typelist_discr x y =
 306   Logic.eq_rect_Type2 x
 307     (match x with
 308      | Tnil -> Obj.magic (fun _ dH -> dH)
 309      | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 310
 311 (** val fieldlist_discr : fieldlist -> fieldlist -> __ **)
 312 let fieldlist_discr x y =
 313   Logic.eq_rect_Type2 x
 314     (match x with
 315      | Fnil -> Obj.magic (fun _ dH -> dH)
 316      | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 317
 318 (** val type_jmdiscr : type0 -> type0 -> __ **)
 319 let type_jmdiscr x y =
 320   Logic.eq_rect_Type2 x
 321     (match x with
 322      | Tvoid -> Obj.magic (fun _ dH -> dH)
 323      | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 324      | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
 325      | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 326      | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 327      | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 328      | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 329      | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
 330
 331 (** val typelist_jmdiscr : typelist -> typelist -> __ **)
 332 let typelist_jmdiscr x y =
 333   Logic.eq_rect_Type2 x
 334     (match x with
 335      | Tnil -> Obj.magic (fun _ dH -> dH)
 336      | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 337
 338 (** val fieldlist_jmdiscr : fieldlist -> fieldlist -> __ **)
 339 let fieldlist_jmdiscr x y =
 340   Logic.eq_rect_Type2 x
 341     (match x with
 342      | Fnil -> Obj.magic (fun _ dH -> dH)
 343      | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 344
 345 type unary_operation =
 346 | Onotbool
 347 | Onotint
 348 | Oneg
 349
 350 (** val unary_operation_rect_Type4 :
 351     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 352 let rec unary_operation_rect_Type4 h_Onotbool h_Onotint h_Oneg = function
 353 | Onotbool -> h_Onotbool
 354 | Onotint -> h_Onotint
 355 | Oneg -> h_Oneg
 356
 357 (** val unary_operation_rect_Type5 :
 358     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 359 let rec unary_operation_rect_Type5 h_Onotbool h_Onotint h_Oneg = function
 360 | Onotbool -> h_Onotbool
 361 | Onotint -> h_Onotint
 362 | Oneg -> h_Oneg
 363
 364 (** val unary_operation_rect_Type3 :
 365     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 366 let rec unary_operation_rect_Type3 h_Onotbool h_Onotint h_Oneg = function
 367 | Onotbool -> h_Onotbool
 368 | Onotint -> h_Onotint
 369 | Oneg -> h_Oneg
 370
 371 (** val unary_operation_rect_Type2 :
 372     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 373 let rec unary_operation_rect_Type2 h_Onotbool h_Onotint h_Oneg = function
 374 | Onotbool -> h_Onotbool
 375 | Onotint -> h_Onotint
 376 | Oneg -> h_Oneg
 377
 378 (** val unary_operation_rect_Type1 :
 379     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 380 let rec unary_operation_rect_Type1 h_Onotbool h_Onotint h_Oneg = function
 381 | Onotbool -> h_Onotbool
 382 | Onotint -> h_Onotint
 383 | Oneg -> h_Oneg
 384
 385 (** val unary_operation_rect_Type0 :
 386     'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
 387 let rec unary_operation_rect_Type0 h_Onotbool h_Onotint h_Oneg = function
 388 | Onotbool -> h_Onotbool
 389 | Onotint -> h_Onotint
 390 | Oneg -> h_Oneg
 391
 392 (** val unary_operation_inv_rect_Type4 :
 393     unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 394 let unary_operation_inv_rect_Type4 hterm h1 h2 h3 =
 395   let hcut = unary_operation_rect_Type4 h1 h2 h3 hterm in hcut __
 396
 397 (** val unary_operation_inv_rect_Type3 :
 398     unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 399 let unary_operation_inv_rect_Type3 hterm h1 h2 h3 =
 400   let hcut = unary_operation_rect_Type3 h1 h2 h3 hterm in hcut __
 401
 402 (** val unary_operation_inv_rect_Type2 :
 403     unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 404 let unary_operation_inv_rect_Type2 hterm h1 h2 h3 =
 405   let hcut = unary_operation_rect_Type2 h1 h2 h3 hterm in hcut __
 406
 407 (** val unary_operation_inv_rect_Type1 :
 408     unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 409 let unary_operation_inv_rect_Type1 hterm h1 h2 h3 =
 410   let hcut = unary_operation_rect_Type1 h1 h2 h3 hterm in hcut __
 411
 412 (** val unary_operation_inv_rect_Type0 :
 413     unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 414 let unary_operation_inv_rect_Type0 hterm h1 h2 h3 =
 415   let hcut = unary_operation_rect_Type0 h1 h2 h3 hterm in hcut __
 416
 417 (** val unary_operation_discr : unary_operation -> unary_operation -> __ **)
 418 let unary_operation_discr x y =
 419   Logic.eq_rect_Type2 x
 420     (match x with
 421      | Onotbool -> Obj.magic (fun _ dH -> dH)
 422      | Onotint -> Obj.magic (fun _ dH -> dH)
 423      | Oneg -> Obj.magic (fun _ dH -> dH)) y
 424
 425 (** val unary_operation_jmdiscr :
 426     unary_operation -> unary_operation -> __ **)
 427 let unary_operation_jmdiscr x y =
 428   Logic.eq_rect_Type2 x
 429     (match x with
 430      | Onotbool -> Obj.magic (fun _ dH -> dH)
 431      | Onotint -> Obj.magic (fun _ dH -> dH)
 432      | Oneg -> Obj.magic (fun _ dH -> dH)) y
 433
 434 type binary_operation =
 435 | Oadd
 436 | Osub
 437 | Omul
 438 | Odiv
 439 | Omod
 440 | Oand
 441 | Oor
 442 | Oxor
 443 | Oshl
 444 | Oshr
 445 | Oeq
 446 | One
 447 | Olt
 448 | Ogt
 449 | Ole
 450 | Oge
 451
 452 (** val binary_operation_rect_Type4 :
 453     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 454     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 455 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 456 | Oadd -> h_Oadd
 457 | Osub -> h_Osub
 458 | Omul -> h_Omul
 459 | Odiv -> h_Odiv
 460 | Omod -> h_Omod
 461 | Oand -> h_Oand
 462 | Oor -> h_Oor
 463 | Oxor -> h_Oxor
 464 | Oshl -> h_Oshl
 465 | Oshr -> h_Oshr
 466 | Oeq -> h_Oeq
 467 | One -> h_One
 468 | Olt -> h_Olt
 469 | Ogt -> h_Ogt
 470 | Ole -> h_Ole
 471 | Oge -> h_Oge
 472
 473 (** val binary_operation_rect_Type5 :
 474     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 475     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 476 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 477 | Oadd -> h_Oadd
 478 | Osub -> h_Osub
 479 | Omul -> h_Omul
 480 | Odiv -> h_Odiv
 481 | Omod -> h_Omod
 482 | Oand -> h_Oand
 483 | Oor -> h_Oor
 484 | Oxor -> h_Oxor
 485 | Oshl -> h_Oshl
 486 | Oshr -> h_Oshr
 487 | Oeq -> h_Oeq
 488 | One -> h_One
 489 | Olt -> h_Olt
 490 | Ogt -> h_Ogt
 491 | Ole -> h_Ole
 492 | Oge -> h_Oge
 493
 494 (** val binary_operation_rect_Type3 :
 495     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 496     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 497 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 498 | Oadd -> h_Oadd
 499 | Osub -> h_Osub
 500 | Omul -> h_Omul
 501 | Odiv -> h_Odiv
 502 | Omod -> h_Omod
 503 | Oand -> h_Oand
 504 | Oor -> h_Oor
 505 | Oxor -> h_Oxor
 506 | Oshl -> h_Oshl
 507 | Oshr -> h_Oshr
 508 | Oeq -> h_Oeq
 509 | One -> h_One
 510 | Olt -> h_Olt
 511 | Ogt -> h_Ogt
 512 | Ole -> h_Ole
 513 | Oge -> h_Oge
 514
 515 (** val binary_operation_rect_Type2 :
 516     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 517     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 518 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 519 | Oadd -> h_Oadd
 520 | Osub -> h_Osub
 521 | Omul -> h_Omul
 522 | Odiv -> h_Odiv
 523 | Omod -> h_Omod
 524 | Oand -> h_Oand
 525 | Oor -> h_Oor
 526 | Oxor -> h_Oxor
 527 | Oshl -> h_Oshl
 528 | Oshr -> h_Oshr
 529 | Oeq -> h_Oeq
 530 | One -> h_One
 531 | Olt -> h_Olt
 532 | Ogt -> h_Ogt
 533 | Ole -> h_Ole
 534 | Oge -> h_Oge
 535
 536 (** val binary_operation_rect_Type1 :
 537     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 538     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 539 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 540 | Oadd -> h_Oadd
 541 | Osub -> h_Osub
 542 | Omul -> h_Omul
 543 | Odiv -> h_Odiv
 544 | Omod -> h_Omod
 545 | Oand -> h_Oand
 546 | Oor -> h_Oor
 547 | Oxor -> h_Oxor
 548 | Oshl -> h_Oshl
 549 | Oshr -> h_Oshr
 550 | Oeq -> h_Oeq
 551 | One -> h_One
 552 | Olt -> h_Olt
 553 | Ogt -> h_Ogt
 554 | Ole -> h_Ole
 555 | Oge -> h_Oge
 556
 557 (** val binary_operation_rect_Type0 :
 558     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 559     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
 560 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
 561 | Oadd -> h_Oadd
 562 | Osub -> h_Osub
 563 | Omul -> h_Omul
 564 | Odiv -> h_Odiv
 565 | Omod -> h_Omod
 566 | Oand -> h_Oand
 567 | Oor -> h_Oor
 568 | Oxor -> h_Oxor
 569 | Oshl -> h_Oshl
 570 | Oshr -> h_Oshr
 571 | Oeq -> h_Oeq
 572 | One -> h_One
 573 | Olt -> h_Olt
 574 | Ogt -> h_Ogt
 575 | Ole -> h_Ole
 576 | Oge -> h_Oge
 577
 578 (** val binary_operation_inv_rect_Type4 :
 579     binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 580     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 581     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 582     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 583 let binary_operation_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
 584   let hcut =
 585     binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 586       h14 h15 h16 hterm
 587   in
 588   hcut __
 589
 590 (** val binary_operation_inv_rect_Type3 :
 591     binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 592     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 593     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 594     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 595 let binary_operation_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
 596   let hcut =
 597     binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 598       h14 h15 h16 hterm
 599   in
 600   hcut __
 601
 602 (** val binary_operation_inv_rect_Type2 :
 603     binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 604     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 605     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 606     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 607 let binary_operation_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
 608   let hcut =
 609     binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 610       h14 h15 h16 hterm
 611   in
 612   hcut __
 613
 614 (** val binary_operation_inv_rect_Type1 :
 615     binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 616     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 617     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 618     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 619 let binary_operation_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
 620   let hcut =
 621     binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 622       h14 h15 h16 hterm
 623   in
 624   hcut __
 625
 626 (** val binary_operation_inv_rect_Type0 :
 627     binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 628     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 629     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 630     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 631 let binary_operation_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
 632   let hcut =
 633     binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 634       h14 h15 h16 hterm
 635   in
 636   hcut __
 637
 638 (** val binary_operation_discr :
 639     binary_operation -> binary_operation -> __ **)
 640 let binary_operation_discr x y =
 641   Logic.eq_rect_Type2 x
 642     (match x with
 643      | Oadd -> Obj.magic (fun _ dH -> dH)
 644      | Osub -> Obj.magic (fun _ dH -> dH)
 645      | Omul -> Obj.magic (fun _ dH -> dH)
 646      | Odiv -> Obj.magic (fun _ dH -> dH)
 647      | Omod -> Obj.magic (fun _ dH -> dH)
 648      | Oand -> Obj.magic (fun _ dH -> dH)
 649      | Oor -> Obj.magic (fun _ dH -> dH)
 650      | Oxor -> Obj.magic (fun _ dH -> dH)
 651      | Oshl -> Obj.magic (fun _ dH -> dH)
 652      | Oshr -> Obj.magic (fun _ dH -> dH)
 653      | Oeq -> Obj.magic (fun _ dH -> dH)
 654      | One -> Obj.magic (fun _ dH -> dH)
 655      | Olt -> Obj.magic (fun _ dH -> dH)
 656      | Ogt -> Obj.magic (fun _ dH -> dH)
 657      | Ole -> Obj.magic (fun _ dH -> dH)
 658      | Oge -> Obj.magic (fun _ dH -> dH)) y
 659
 660 (** val binary_operation_jmdiscr :
 661     binary_operation -> binary_operation -> __ **)
 662 let binary_operation_jmdiscr x y =
 663   Logic.eq_rect_Type2 x
 664     (match x with
 665      | Oadd -> Obj.magic (fun _ dH -> dH)
 666      | Osub -> Obj.magic (fun _ dH -> dH)
 667      | Omul -> Obj.magic (fun _ dH -> dH)
 668      | Odiv -> Obj.magic (fun _ dH -> dH)
 669      | Omod -> Obj.magic (fun _ dH -> dH)
 670      | Oand -> Obj.magic (fun _ dH -> dH)
 671      | Oor -> Obj.magic (fun _ dH -> dH)
 672      | Oxor -> Obj.magic (fun _ dH -> dH)
 673      | Oshl -> Obj.magic (fun _ dH -> dH)
 674      | Oshr -> Obj.magic (fun _ dH -> dH)
 675      | Oeq -> Obj.magic (fun _ dH -> dH)
 676      | One -> Obj.magic (fun _ dH -> dH)
 677      | Olt -> Obj.magic (fun _ dH -> dH)
 678      | Ogt -> Obj.magic (fun _ dH -> dH)
 679      | Ole -> Obj.magic (fun _ dH -> dH)
 680      | Oge -> Obj.magic (fun _ dH -> dH)) y
 681
 682 type expr =
 683 | Expr of expr_descr * type0
 684 and expr_descr =
 685 | Econst_int of AST.intsize * AST.bvint
 686 | Evar of AST.ident
 687 | Ederef of expr
 688 | Eaddrof of expr
 689 | Eunop of unary_operation * expr
 690 | Ebinop of binary_operation * expr * expr
 691 | Ecast of type0 * expr
 692 | Econdition of expr * expr * expr
 693 | Eandbool of expr * expr
 694 | Eorbool of expr * expr
 695 | Esizeof of type0
 696 | Efield of expr * AST.ident
 697 | Ecost of CostLabel.costlabel * expr
 698
 699 (** val expr_inv_rect_Type4 :
 700     expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
 701 let expr_inv_rect_Type4 hterm h1 =
 702   let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
 703
 704 (** val expr_inv_rect_Type3 :
 705     expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
 706 let expr_inv_rect_Type3 hterm h1 =
 707   let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
 708
 709 (** val expr_inv_rect_Type2 :
 710     expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
 711 let expr_inv_rect_Type2 hterm h1 =
 712   let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
 713
 714 (** val expr_inv_rect_Type1 :
 715     expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
 716 let expr_inv_rect_Type1 hterm h1 =
 717   let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
 718
 719 (** val expr_inv_rect_Type0 :
 720     expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
 721 let expr_inv_rect_Type0 hterm h1 =
 722   let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
 723
 724 (** val expr_descr_inv_rect_Type4 :
 725     expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
 726     -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
 727     -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
 728     -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
 729     (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
 730     __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
 731     expr -> __ -> 'a1) -> 'a1 **)
 732 let expr_descr_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 733   let hcut =
 734     match hterm with
 735     | Econst_int (x, x0) -> h1 x x0
 736     | Evar x -> h2 x
 737     | Ederef x -> h3 x
 738     | Eaddrof x -> h4 x
 739     | Eunop (x, x0) -> h5 x x0
 740     | Ebinop (x, x0, x1) -> h6 x x0 x1
 741     | Ecast (x, x0) -> h7 x x0
 742     | Econdition (x, x0, x1) -> h8 x x0 x1
 743     | Eandbool (x, x0) -> h9 x x0
 744     | Eorbool (x, x0) -> h10 x x0
 745     | Esizeof x -> h11 x
 746     | Efield (x, x0) -> h12 x x0
 747     | Ecost (x, x0) -> h13 x x0
 748   in
 749   hcut __
 750
 751 (** val expr_descr_inv_rect_Type3 :
 752     expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
 753     -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
 754     -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
 755     -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
 756     (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
 757     __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
 758     expr -> __ -> 'a1) -> 'a1 **)
 759 let expr_descr_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 760   let hcut =
 761     match hterm with
 762     | Econst_int (x, x0) -> h1 x x0
 763     | Evar x -> h2 x
 764     | Ederef x -> h3 x
 765     | Eaddrof x -> h4 x
 766     | Eunop (x, x0) -> h5 x x0
 767     | Ebinop (x, x0, x1) -> h6 x x0 x1
 768     | Ecast (x, x0) -> h7 x x0
 769     | Econdition (x, x0, x1) -> h8 x x0 x1
 770     | Eandbool (x, x0) -> h9 x x0
 771     | Eorbool (x, x0) -> h10 x x0
 772     | Esizeof x -> h11 x
 773     | Efield (x, x0) -> h12 x x0
 774     | Ecost (x, x0) -> h13 x x0
 775   in
 776   hcut __
 777
 778 (** val expr_descr_inv_rect_Type2 :
 779     expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
 780     -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
 781     -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
 782     -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
 783     (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
 784     __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
 785     expr -> __ -> 'a1) -> 'a1 **)
 786 let expr_descr_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 787   let hcut =
 788     match hterm with
 789     | Econst_int (x, x0) -> h1 x x0
 790     | Evar x -> h2 x
 791     | Ederef x -> h3 x
 792     | Eaddrof x -> h4 x
 793     | Eunop (x, x0) -> h5 x x0
 794     | Ebinop (x, x0, x1) -> h6 x x0 x1
 795     | Ecast (x, x0) -> h7 x x0
 796     | Econdition (x, x0, x1) -> h8 x x0 x1
 797     | Eandbool (x, x0) -> h9 x x0
 798     | Eorbool (x, x0) -> h10 x x0
 799     | Esizeof x -> h11 x
 800     | Efield (x, x0) -> h12 x x0
 801     | Ecost (x, x0) -> h13 x x0
 802   in
 803   hcut __
 804
 805 (** val expr_descr_inv_rect_Type1 :
 806     expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
 807     -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
 808     -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
 809     -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
 810     (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
 811     __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
 812     expr -> __ -> 'a1) -> 'a1 **)
 813 let expr_descr_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 814   let hcut =
 815     match hterm with
 816     | Econst_int (x, x0) -> h1 x x0
 817     | Evar x -> h2 x
 818     | Ederef x -> h3 x
 819     | Eaddrof x -> h4 x
 820     | Eunop (x, x0) -> h5 x x0
 821     | Ebinop (x, x0, x1) -> h6 x x0 x1
 822     | Ecast (x, x0) -> h7 x x0
 823     | Econdition (x, x0, x1) -> h8 x x0 x1
 824     | Eandbool (x, x0) -> h9 x x0
 825     | Eorbool (x, x0) -> h10 x x0
 826     | Esizeof x -> h11 x
 827     | Efield (x, x0) -> h12 x x0
 828     | Ecost (x, x0) -> h13 x x0
 829   in
 830   hcut __
 831
 832 (** val expr_descr_inv_rect_Type0 :
 833     expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
 834     -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
 835     -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
 836     -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
 837     (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
 838     __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
 839     expr -> __ -> 'a1) -> 'a1 **)
 840 let expr_descr_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 841   let hcut =
 842     match hterm with
 843     | Econst_int (x, x0) -> h1 x x0
 844     | Evar x -> h2 x
 845     | Ederef x -> h3 x
 846     | Eaddrof x -> h4 x
 847     | Eunop (x, x0) -> h5 x x0
 848     | Ebinop (x, x0, x1) -> h6 x x0 x1
 849     | Ecast (x, x0) -> h7 x x0
 850     | Econdition (x, x0, x1) -> h8 x x0 x1
 851     | Eandbool (x, x0) -> h9 x x0
 852     | Eorbool (x, x0) -> h10 x x0
 853     | Esizeof x -> h11 x
 854     | Efield (x, x0) -> h12 x x0
 855     | Ecost (x, x0) -> h13 x x0
 856   in
 857   hcut __
 858
 859 (** val expr_discr : expr -> expr -> __ **)
 860 let expr_discr x y =
 861   Logic.eq_rect_Type2 x
 862     (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
 863
 864 (** val expr_descr_discr : expr_descr -> expr_descr -> __ **)
 865 let expr_descr_discr x y =
 866   Logic.eq_rect_Type2 x
 867     (match x with
 868      | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 869      | Evar a0 -> Obj.magic (fun _ dH -> dH __)
 870      | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
 871      | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
 872      | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 873      | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 874      | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 875      | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 876      | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 877      | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 878      | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
 879      | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 880      | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 881
 882 (** val expr_jmdiscr : expr -> expr -> __ **)
 883 let expr_jmdiscr x y =
 884   Logic.eq_rect_Type2 x
 885     (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
 886
 887 (** val expr_descr_jmdiscr : expr_descr -> expr_descr -> __ **)
 888 let expr_descr_jmdiscr x y =
 889   Logic.eq_rect_Type2 x
 890     (match x with
 891      | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 892      | Evar a0 -> Obj.magic (fun _ dH -> dH __)
 893      | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
 894      | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
 895      | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 896      | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 897      | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 898      | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 899      | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 900      | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 901      | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
 902      | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 903      | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 904
 905 (** val typeof : expr -> type0 **)
 906 let typeof = function
 907 | Expr (de, te) -> te
 908
 909 type label = AST.ident
 910
 911 type statement =
 912 | Sskip
 913 | Sassign of expr * expr
 914 | Scall of expr Types.option * expr * expr List.list
 915 | Ssequence of statement * statement
 916 | Sifthenelse of expr * statement * statement
 917 | Swhile of expr * statement
 918 | Sdowhile of expr * statement
 919 | Sfor of statement * expr * statement * statement
 920 | Sbreak
 921 | Scontinue
 922 | Sreturn of expr Types.option
 923 | Sswitch of expr * labeled_statements
 924 | Slabel of label * statement
 925 | Sgoto of label
 926 | Scost of CostLabel.costlabel * statement
 927 and labeled_statements =
 928 | LSdefault of statement
 929 | LScase of AST.intsize * AST.bvint * statement * labeled_statements
 930
 931 (** val statement_inv_rect_Type4 :
 932     statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
 933     Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
 934     statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
 935     -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
 936     -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
 937     'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
 938     labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
 939     (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
 940     -> 'a1 **)
 941 let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
 942   let hcut =
 943     match hterm with
 944     | Sskip -> h1
 945     | Sassign (x, x0) -> h2 x x0
 946     | Scall (x, x0, x1) -> h3 x x0 x1
 947     | Ssequence (x, x0) -> h4 x x0
 948     | Sifthenelse (x, x0, x1) -> h5 x x0 x1
 949     | Swhile (x, x0) -> h6 x x0
 950     | Sdowhile (x, x0) -> h7 x x0
 951     | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
 952     | Sbreak -> h9
 953     | Scontinue -> h10
 954     | Sreturn x -> h11 x
 955     | Sswitch (x, x0) -> h12 x x0
 956     | Slabel (x, x0) -> h13 x x0
 957     | Sgoto x -> h14 x
 958     | Scost (x, x0) -> h15 x x0
 959   in
 960   hcut __
 961
 962 (** val statement_inv_rect_Type3 :
 963     statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
 964     Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
 965     statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
 966     -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
 967     -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
 968     'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
 969     labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
 970     (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
 971     -> 'a1 **)
 972 let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
 973   let hcut =
 974     match hterm with
 975     | Sskip -> h1
 976     | Sassign (x, x0) -> h2 x x0
 977     | Scall (x, x0, x1) -> h3 x x0 x1
 978     | Ssequence (x, x0) -> h4 x x0
 979     | Sifthenelse (x, x0, x1) -> h5 x x0 x1
 980     | Swhile (x, x0) -> h6 x x0
 981     | Sdowhile (x, x0) -> h7 x x0
 982     | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
 983     | Sbreak -> h9
 984     | Scontinue -> h10
 985     | Sreturn x -> h11 x
 986     | Sswitch (x, x0) -> h12 x x0
 987     | Slabel (x, x0) -> h13 x x0
 988     | Sgoto x -> h14 x
 989     | Scost (x, x0) -> h15 x x0
 990   in
 991   hcut __
 992
 993 (** val statement_inv_rect_Type2 :
 994     statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
 995     Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
 996     statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
 997     -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
 998     -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
 999     'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1000     labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1001     (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1002     -> 'a1 **)
1003 let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1004   let hcut =
1005     match hterm with
1006     | Sskip -> h1
1007     | Sassign (x, x0) -> h2 x x0
1008     | Scall (x, x0, x1) -> h3 x x0 x1
1009     | Ssequence (x, x0) -> h4 x x0
1010     | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1011     | Swhile (x, x0) -> h6 x x0
1012     | Sdowhile (x, x0) -> h7 x x0
1013     | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1014     | Sbreak -> h9
1015     | Scontinue -> h10
1016     | Sreturn x -> h11 x
1017     | Sswitch (x, x0) -> h12 x x0
1018     | Slabel (x, x0) -> h13 x x0
1019     | Sgoto x -> h14 x
1020     | Scost (x, x0) -> h15 x x0
1021   in
1022   hcut __
1023
1024 (** val statement_inv_rect_Type1 :
1025     statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1026     Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1027     statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1028     -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1029     -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1030     'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1031     labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1032     (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1033     -> 'a1 **)
1034 let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1035   let hcut =
1036     match hterm with
1037     | Sskip -> h1
1038     | Sassign (x, x0) -> h2 x x0
1039     | Scall (x, x0, x1) -> h3 x x0 x1
1040     | Ssequence (x, x0) -> h4 x x0
1041     | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1042     | Swhile (x, x0) -> h6 x x0
1043     | Sdowhile (x, x0) -> h7 x x0
1044     | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1045     | Sbreak -> h9
1046     | Scontinue -> h10
1047     | Sreturn x -> h11 x
1048     | Sswitch (x, x0) -> h12 x x0
1049     | Slabel (x, x0) -> h13 x x0
1050     | Sgoto x -> h14 x
1051     | Scost (x, x0) -> h15 x x0
1052   in
1053   hcut __
1054
1055 (** val statement_inv_rect_Type0 :
1056     statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1057     Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1058     statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1059     -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1060     -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1061     'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1062     labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1063     (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1064     -> 'a1 **)
1065 let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1066   let hcut =
1067     match hterm with
1068     | Sskip -> h1
1069     | Sassign (x, x0) -> h2 x x0
1070     | Scall (x, x0, x1) -> h3 x x0 x1
1071     | Ssequence (x, x0) -> h4 x x0
1072     | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1073     | Swhile (x, x0) -> h6 x x0
1074     | Sdowhile (x, x0) -> h7 x x0
1075     | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1076     | Sbreak -> h9
1077     | Scontinue -> h10
1078     | Sreturn x -> h11 x
1079     | Sswitch (x, x0) -> h12 x x0
1080     | Slabel (x, x0) -> h13 x x0
1081     | Sgoto x -> h14 x
1082     | Scost (x, x0) -> h15 x x0
1083   in
1084   hcut __
1085
1086 (** val labeled_statements_inv_rect_Type4 :
1087     labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1088     AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1089 let labeled_statements_inv_rect_Type4 hterm h1 h2 =
1090   let hcut =
1091     match hterm with
1092     | LSdefault x -> h1 x
1093     | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1094   in
1095   hcut __
1096
1097 (** val labeled_statements_inv_rect_Type3 :
1098     labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1099     AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1100 let labeled_statements_inv_rect_Type3 hterm h1 h2 =
1101   let hcut =
1102     match hterm with
1103     | LSdefault x -> h1 x
1104     | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1105   in
1106   hcut __
1107
1108 (** val labeled_statements_inv_rect_Type2 :
1109     labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1110     AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1111 let labeled_statements_inv_rect_Type2 hterm h1 h2 =
1112   let hcut =
1113     match hterm with
1114     | LSdefault x -> h1 x
1115     | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1116   in
1117   hcut __
1118
1119 (** val labeled_statements_inv_rect_Type1 :
1120     labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1121     AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1122 let labeled_statements_inv_rect_Type1 hterm h1 h2 =
1123   let hcut =
1124     match hterm with
1125     | LSdefault x -> h1 x
1126     | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1127   in
1128   hcut __
1129
1130 (** val labeled_statements_inv_rect_Type0 :
1131     labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1132     AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1133 let labeled_statements_inv_rect_Type0 hterm h1 h2 =
1134   let hcut =
1135     match hterm with
1136     | LSdefault x -> h1 x
1137     | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1138   in
1139   hcut __
1140
1141 (** val statement_discr : statement -> statement -> __ **)
1142 let statement_discr x y =
1143   Logic.eq_rect_Type2 x
1144     (match x with
1145      | Sskip -> Obj.magic (fun _ dH -> dH)
1146      | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1147      | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1148      | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1149      | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1150      | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1151      | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1152      | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1153      | Sbreak -> Obj.magic (fun _ dH -> dH)
1154      | Scontinue -> Obj.magic (fun _ dH -> dH)
1155      | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1156      | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1157      | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1158      | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1159      | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1160
1161 (** val labeled_statements_discr :
1162     labeled_statements -> labeled_statements -> __ **)
1163 let labeled_statements_discr x y =
1164   Logic.eq_rect_Type2 x
1165     (match x with
1166      | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1167      | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1168
1169 (** val statement_jmdiscr : statement -> statement -> __ **)
1170 let statement_jmdiscr x y =
1171   Logic.eq_rect_Type2 x
1172     (match x with
1173      | Sskip -> Obj.magic (fun _ dH -> dH)
1174      | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1175      | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1176      | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1177      | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1178      | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1179      | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1180      | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1181      | Sbreak -> Obj.magic (fun _ dH -> dH)
1182      | Scontinue -> Obj.magic (fun _ dH -> dH)
1183      | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1184      | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1185      | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1186      | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1187      | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1188
1189 (** val labeled_statements_jmdiscr :
1190     labeled_statements -> labeled_statements -> __ **)
1191 let labeled_statements_jmdiscr x y =
1192   Logic.eq_rect_Type2 x
1193     (match x with
1194      | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1195      | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1196
1197 type function0 = { fn_return : type0;
1198                    fn_params : (AST.ident, type0) Types.prod List.list;
1199                    fn_vars : (AST.ident, type0) Types.prod List.list;
1200                    fn_body : statement }
1201
1202 (** val function_rect_Type4 :
1203     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1204     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1205 let rec function_rect_Type4 h_mk_function x_4495 =
1206   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1207     fn_body = fn_body0 } = x_4495
1208   in
1209   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1210
1211 (** val function_rect_Type5 :
1212     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1213     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1214 let rec function_rect_Type5 h_mk_function x_4497 =
1215   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1216     fn_body = fn_body0 } = x_4497
1217   in
1218   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1219
1220 (** val function_rect_Type3 :
1221     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1222     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1223 let rec function_rect_Type3 h_mk_function x_4499 =
1224   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1225     fn_body = fn_body0 } = x_4499
1226   in
1227   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1228
1229 (** val function_rect_Type2 :
1230     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1231     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1232 let rec function_rect_Type2 h_mk_function x_4501 =
1233   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1234     fn_body = fn_body0 } = x_4501
1235   in
1236   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1237
1238 (** val function_rect_Type1 :
1239     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1240     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1241 let rec function_rect_Type1 h_mk_function x_4503 =
1242   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1243     fn_body = fn_body0 } = x_4503
1244   in
1245   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1246
1247 (** val function_rect_Type0 :
1248     (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1249     Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1250 let rec function_rect_Type0 h_mk_function x_4505 =
1251   let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1252     fn_body = fn_body0 } = x_4505
1253   in
1254   h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1255
1256 (** val fn_return : function0 -> type0 **)
1257 let rec fn_return xxx =
1258   xxx.fn_return
1259
1260 (** val fn_params : function0 -> (AST.ident, type0) Types.prod List.list **)
1261 let rec fn_params xxx =
1262   xxx.fn_params
1263
1264 (** val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list **)
1265 let rec fn_vars xxx =
1266   xxx.fn_vars
1267
1268 (** val fn_body : function0 -> statement **)
1269 let rec fn_body xxx =
1270   xxx.fn_body
1271
1272 (** val function_inv_rect_Type4 :
1273     function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1274     (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1275 let function_inv_rect_Type4 hterm h1 =
1276   let hcut = function_rect_Type4 h1 hterm in hcut __
1277
1278 (** val function_inv_rect_Type3 :
1279     function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1280     (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1281 let function_inv_rect_Type3 hterm h1 =
1282   let hcut = function_rect_Type3 h1 hterm in hcut __
1283
1284 (** val function_inv_rect_Type2 :
1285     function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1286     (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1287 let function_inv_rect_Type2 hterm h1 =
1288   let hcut = function_rect_Type2 h1 hterm in hcut __
1289
1290 (** val function_inv_rect_Type1 :
1291     function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1292     (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1293 let function_inv_rect_Type1 hterm h1 =
1294   let hcut = function_rect_Type1 h1 hterm in hcut __
1295
1296 (** val function_inv_rect_Type0 :
1297     function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1298     (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1299 let function_inv_rect_Type0 hterm h1 =
1300   let hcut = function_rect_Type0 h1 hterm in hcut __
1301
1302 (** val function_discr : function0 -> function0 -> __ **)
1303 let function_discr x y =
1304   Logic.eq_rect_Type2 x
1305     (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1306      in
1307     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1308
1309 (** val function_jmdiscr : function0 -> function0 -> __ **)
1310 let function_jmdiscr x y =
1311   Logic.eq_rect_Type2 x
1312     (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1313      in
1314     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1315
1316 type clight_fundef =
1317 | CL_Internal of function0
1318 | CL_External of AST.ident * typelist * type0
1319
1320 (** val clight_fundef_rect_Type4 :
1321     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1322     clight_fundef -> 'a1 **)
1323 let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
1324 | CL_Internal x_4527 -> h_CL_Internal x_4527
1325 | CL_External (x_4530, x_4529, x_4528) -> h_CL_External x_4530 x_4529 x_4528
1326
1327 (** val clight_fundef_rect_Type5 :
1328     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1329     clight_fundef -> 'a1 **)
1330 let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
1331 | CL_Internal x_4534 -> h_CL_Internal x_4534
1332 | CL_External (x_4537, x_4536, x_4535) -> h_CL_External x_4537 x_4536 x_4535
1333
1334 (** val clight_fundef_rect_Type3 :
1335     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1336     clight_fundef -> 'a1 **)
1337 let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
1338 | CL_Internal x_4541 -> h_CL_Internal x_4541
1339 | CL_External (x_4544, x_4543, x_4542) -> h_CL_External x_4544 x_4543 x_4542
1340
1341 (** val clight_fundef_rect_Type2 :
1342     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1343     clight_fundef -> 'a1 **)
1344 let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
1345 | CL_Internal x_4548 -> h_CL_Internal x_4548
1346 | CL_External (x_4551, x_4550, x_4549) -> h_CL_External x_4551 x_4550 x_4549
1347
1348 (** val clight_fundef_rect_Type1 :
1349     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1350     clight_fundef -> 'a1 **)
1351 let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
1352 | CL_Internal x_4555 -> h_CL_Internal x_4555
1353 | CL_External (x_4558, x_4557, x_4556) -> h_CL_External x_4558 x_4557 x_4556
1354
1355 (** val clight_fundef_rect_Type0 :
1356     (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1357     clight_fundef -> 'a1 **)
1358 let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
1359 | CL_Internal x_4562 -> h_CL_Internal x_4562
1360 | CL_External (x_4565, x_4564, x_4563) -> h_CL_External x_4565 x_4564 x_4563
1361
1362 (** val clight_fundef_inv_rect_Type4 :
1363     clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1364     type0 -> __ -> 'a1) -> 'a1 **)
1365 let clight_fundef_inv_rect_Type4 hterm h1 h2 =
1366   let hcut = clight_fundef_rect_Type4 h1 h2 hterm in hcut __
1367
1368 (** val clight_fundef_inv_rect_Type3 :
1369     clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1370     type0 -> __ -> 'a1) -> 'a1 **)
1371 let clight_fundef_inv_rect_Type3 hterm h1 h2 =
1372   let hcut = clight_fundef_rect_Type3 h1 h2 hterm in hcut __
1373
1374 (** val clight_fundef_inv_rect_Type2 :
1375     clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1376     type0 -> __ -> 'a1) -> 'a1 **)
1377 let clight_fundef_inv_rect_Type2 hterm h1 h2 =
1378   let hcut = clight_fundef_rect_Type2 h1 h2 hterm in hcut __
1379
1380 (** val clight_fundef_inv_rect_Type1 :
1381     clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1382     type0 -> __ -> 'a1) -> 'a1 **)
1383 let clight_fundef_inv_rect_Type1 hterm h1 h2 =
1384   let hcut = clight_fundef_rect_Type1 h1 h2 hterm in hcut __
1385
1386 (** val clight_fundef_inv_rect_Type0 :
1387     clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1388     type0 -> __ -> 'a1) -> 'a1 **)
1389 let clight_fundef_inv_rect_Type0 hterm h1 h2 =
1390   let hcut = clight_fundef_rect_Type0 h1 h2 hterm in hcut __
1391
1392 (** val clight_fundef_discr : clight_fundef -> clight_fundef -> __ **)
1393 let clight_fundef_discr x y =
1394   Logic.eq_rect_Type2 x
1395     (match x with
1396      | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1397      | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1398
1399 (** val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __ **)
1400 let clight_fundef_jmdiscr x y =
1401   Logic.eq_rect_Type2 x
1402     (match x with
1403      | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1404      | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1405
1406 type clight_program =
1407   (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
1408
1409 (** val type_of_params :
1410     (AST.ident, type0) Types.prod List.list -> typelist **)
1411 let rec type_of_params = function
1412 | List.Nil -> Tnil
1413 | List.Cons (h, rem) ->
1414   let { Types.fst = id; Types.snd = ty } = h in
1415   Tcons (ty, (type_of_params rem))
1416
1417 (** val type_of_function : function0 -> type0 **)
1418 let type_of_function f =
1419   Tfunction ((type_of_params f.fn_params), f.fn_return)
1420
1421 (** val type_of_fundef : clight_fundef -> type0 **)
1422 let type_of_fundef = function
1423 | CL_Internal fd -> type_of_function fd
1424 | CL_External (id, args, res) -> Tfunction (args, res)
1425
1426 (** val alignof : type0 -> Nat.nat **)
1427 let rec alignof = function
1428 | Tvoid -> Nat.S Nat.O
1429 | Tint (sz, x) ->
1430   (match sz with
1431    | AST.I8 -> Nat.S Nat.O
1432    | AST.I16 -> Nat.S (Nat.S Nat.O)
1433    | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1434 | Tpointer x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1435 | Tarray (t', n) -> alignof t'
1436 | Tfunction (x, x0) -> Nat.S Nat.O
1437 | Tstruct (x, fld) -> alignof_fields fld
1438 | Tunion (x, fld) -> alignof_fields fld
1439 | Tcomp_ptr x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1440 (** val alignof_fields : fieldlist -> Nat.nat **)
1441 and alignof_fields = function
1442 | Fnil -> Nat.S Nat.O
1443 | Fcons (id, t, f') -> Nat.max (alignof t) (alignof_fields f')
1444
1445 (** val sizeof : type0 -> Nat.nat **)
1446 let rec sizeof t = match t with
1447 | Tvoid -> Nat.S Nat.O
1448 | Tint (i, x) ->
1449   (match i with
1450    | AST.I8 -> Nat.S Nat.O
1451    | AST.I16 -> Nat.S (Nat.S Nat.O)
1452    | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1453 | Tpointer x -> AST.size_pointer
1454 | Tarray (t', n) -> Nat.times (sizeof t') (Nat.max (Nat.S Nat.O) n)
1455 | Tfunction (x, x0) -> Nat.S Nat.O
1456 | Tstruct (x, fld) ->
1457   Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_struct fld Nat.O)) (alignof t)
1458 | Tunion (x, fld) ->
1459   Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_union fld)) (alignof t)
1460 | Tcomp_ptr x -> AST.size_pointer
1461 (** val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat **)
1462 and sizeof_struct fld pos =
1463   match fld with
1464   | Fnil -> pos
1465   | Fcons (id, t, fld') ->
1466     sizeof_struct fld' (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t))
1467 (** val sizeof_union : fieldlist -> Nat.nat **)
1468 and sizeof_union = function
1469 | Fnil -> Nat.O
1470 | Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')
1471
1472 (** val field_offset_rec :
1473     AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
1474 let rec field_offset_rec id fld pos =
1475   match fld with
1476   | Fnil ->
1477     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1478       (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1479   | Fcons (id', t, fld') ->
1480     (match AST.ident_eq id id' with
1481      | Types.Inl _ -> Errors.OK (Coqlib.align pos (alignof t))
1482      | Types.Inr _ ->
1483        field_offset_rec id fld'
1484          (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t)))
1485
1486 (** val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res **)
1487 let field_offset id fld =
1488   field_offset_rec id fld Nat.O
1489
1490 (** val field_type : AST.ident -> fieldlist -> type0 Errors.res **)
1491 let rec field_type id = function
1492 | Fnil ->
1493   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1494     (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1495 | Fcons (id', t, fld') ->
1496   (match AST.ident_eq id id' with
1497    | Types.Inl _ -> Errors.OK t
1498    | Types.Inr _ -> field_type id fld')
1499
1500 (** val typ_of_type : type0 -> AST.typ **)
1501 let typ_of_type = function
1502 | Tvoid -> AST.ASTint (AST.I32, AST.Unsigned)
1503 | Tint (sz, sg) -> AST.ASTint (sz, sg)
1504 | Tpointer x -> AST.ASTptr
1505 | Tarray (x, x0) -> AST.ASTptr
1506 | Tfunction (x, x0) -> AST.ASTptr
1507 | Tstruct (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1508 | Tunion (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1509 | Tcomp_ptr x -> AST.ASTptr
1510
1511 (** val opttyp_of_type : type0 -> AST.typ Types.option **)
1512 let opttyp_of_type = function
1513 | Tvoid -> Types.None
1514 | Tint (sz, sg) -> Types.Some (AST.ASTint (sz, sg))
1515 | Tpointer x -> Types.Some AST.ASTptr
1516 | Tarray (x, x0) -> Types.Some AST.ASTptr
1517 | Tfunction (x, x0) -> Types.Some AST.ASTptr
1518 | Tstruct (x, x0) -> Types.None
1519 | Tunion (x, x0) -> Types.None
1520 | Tcomp_ptr x -> Types.Some AST.ASTptr
1521
1522 (** val typlist_of_typelist : typelist -> AST.typ List.list **)
1523 let rec typlist_of_typelist = function
1524 | Tnil -> List.Nil
1525 | Tcons (hd, tl0) -> List.Cons ((typ_of_type hd), (typlist_of_typelist tl0))
1526
1527 type mode =
1528 | By_value of AST.typ
1529 | By_reference
1530 | By_nothing of AST.typ
1531
1532 (** val mode_rect_Type4 :
1533     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1534 let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4615 = function
1535 | By_value t -> h_By_value t
1536 | By_reference -> h_By_reference
1537 | By_nothing t -> h_By_nothing t
1538
1539 (** val mode_rect_Type5 :
1540     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1541 let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4620 = function
1542 | By_value t -> h_By_value t
1543 | By_reference -> h_By_reference
1544 | By_nothing t -> h_By_nothing t
1545
1546 (** val mode_rect_Type3 :
1547     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1548 let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4625 = function
1549 | By_value t -> h_By_value t
1550 | By_reference -> h_By_reference
1551 | By_nothing t -> h_By_nothing t
1552
1553 (** val mode_rect_Type2 :
1554     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1555 let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4630 = function
1556 | By_value t -> h_By_value t
1557 | By_reference -> h_By_reference
1558 | By_nothing t -> h_By_nothing t
1559
1560 (** val mode_rect_Type1 :
1561     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1562 let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4635 = function
1563 | By_value t -> h_By_value t
1564 | By_reference -> h_By_reference
1565 | By_nothing t -> h_By_nothing t
1566
1567 (** val mode_rect_Type0 :
1568     (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1569 let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4640 = function
1570 | By_value t -> h_By_value t
1571 | By_reference -> h_By_reference
1572 | By_nothing t -> h_By_nothing t
1573
1574 (** val mode_inv_rect_Type4 :
1575     AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1576     (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1577 let mode_inv_rect_Type4 x1 hterm h1 h2 h3 =
1578   let hcut = mode_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
1579
1580 (** val mode_inv_rect_Type3 :
1581     AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1582     (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1583 let mode_inv_rect_Type3 x1 hterm h1 h2 h3 =
1584   let hcut = mode_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
1585
1586 (** val mode_inv_rect_Type2 :
1587     AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1588     (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1589 let mode_inv_rect_Type2 x1 hterm h1 h2 h3 =
1590   let hcut = mode_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
1591
1592 (** val mode_inv_rect_Type1 :
1593     AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1594     (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1595 let mode_inv_rect_Type1 x1 hterm h1 h2 h3 =
1596   let hcut = mode_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
1597
1598 (** val mode_inv_rect_Type0 :
1599     AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1600     (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1601 let mode_inv_rect_Type0 x1 hterm h1 h2 h3 =
1602   let hcut = mode_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
1603
1604 (** val mode_discr : AST.typ -> mode -> mode -> __ **)
1605 let mode_discr a1 x y =
1606   Logic.eq_rect_Type2 x
1607     (match x with
1608      | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1609      | By_reference -> Obj.magic (fun _ dH -> dH)
1610      | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1611
1612 (** val mode_jmdiscr : AST.typ -> mode -> mode -> __ **)
1613 let mode_jmdiscr a1 x y =
1614   Logic.eq_rect_Type2 x
1615     (match x with
1616      | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1617      | By_reference -> Obj.magic (fun _ dH -> dH)
1618      | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1619
1620 (** val access_mode : type0 -> mode **)
1621 let access_mode = function
1622 | Tvoid -> By_nothing (typ_of_type Tvoid)
1623 | Tint (i, s) -> By_value (AST.ASTint (i, s))
1624 | Tpointer x -> By_value AST.ASTptr
1625 | Tarray (x, x0) -> By_reference
1626 | Tfunction (x, x0) -> By_reference
1627 | Tstruct (x, fList) -> By_nothing (typ_of_type (Tstruct (x, fList)))
1628 | Tunion (x, fList) -> By_nothing (typ_of_type (Tunion (x, fList)))
1629 | Tcomp_ptr x -> By_value AST.ASTptr
1630
1631 (** val signature_of_type : typelist -> type0 -> AST.signature **)
1632 let signature_of_type args res =
1633   { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
1634     (opttyp_of_type res) }
1635
1636 (** val external_function :
1637     AST.ident -> typelist -> type0 -> AST.external_function **)
1638 let external_function id targs tres =
1639   { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }
1640