extracted/aST.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Exp
  14
  15 open Arithmetic
  16
  17 open Vector
  18
  19 open Div_and_mod
  20
  21 open Util
  22
  23 open FoldStuff
  24
  25 open BitVector
  26
  27 open Jmeq
  28
  29 open Russell
  30
  31 open List
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Bool
  42
  43 open Relations
  44
  45 open Nat
  46
  47 open Integers
  48
  49 open Proper
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open ErrorMessages
  56
  57 open PreIdentifiers
  58
  59 open Errors
  60
  61 open Extralib
  62
  63 open Lists
  64
  65 open Positive
  66
  67 open Identifiers
  68
  69 type ident = PreIdentifiers.identifier
  70
  71 (** val ident_eq : ident -> ident -> (__, __) Types.sum **)
  72 let ident_eq =
  73   Identifiers.identifier_eq PreIdentifiers.SymbolTag
  74
  75 (** val ident_of_nat : Nat.nat -> ident **)
  76 let ident_of_nat =
  77   Identifiers.identifier_of_nat PreIdentifiers.SymbolTag
  78
  79 type region =
  80 | XData
  81 | Code
  82
  83 (** val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1 **)
  84 let rec region_rect_Type4 h_XData h_Code = function
  85 | XData -> h_XData
  86 | Code -> h_Code
  87
  88 (** val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1 **)
  89 let rec region_rect_Type5 h_XData h_Code = function
  90 | XData -> h_XData
  91 | Code -> h_Code
  92
  93 (** val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1 **)
  94 let rec region_rect_Type3 h_XData h_Code = function
  95 | XData -> h_XData
  96 | Code -> h_Code
  97
  98 (** val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1 **)
  99 let rec region_rect_Type2 h_XData h_Code = function
 100 | XData -> h_XData
 101 | Code -> h_Code
 102
 103 (** val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1 **)
 104 let rec region_rect_Type1 h_XData h_Code = function
 105 | XData -> h_XData
 106 | Code -> h_Code
 107
 108 (** val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1 **)
 109 let rec region_rect_Type0 h_XData h_Code = function
 110 | XData -> h_XData
 111 | Code -> h_Code
 112
 113 (** val region_inv_rect_Type4 :
 114     region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 115 let region_inv_rect_Type4 hterm h1 h2 =
 116   let hcut = region_rect_Type4 h1 h2 hterm in hcut __
 117
 118 (** val region_inv_rect_Type3 :
 119     region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 120 let region_inv_rect_Type3 hterm h1 h2 =
 121   let hcut = region_rect_Type3 h1 h2 hterm in hcut __
 122
 123 (** val region_inv_rect_Type2 :
 124     region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 125 let region_inv_rect_Type2 hterm h1 h2 =
 126   let hcut = region_rect_Type2 h1 h2 hterm in hcut __
 127
 128 (** val region_inv_rect_Type1 :
 129     region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 130 let region_inv_rect_Type1 hterm h1 h2 =
 131   let hcut = region_rect_Type1 h1 h2 hterm in hcut __
 132
 133 (** val region_inv_rect_Type0 :
 134     region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 135 let region_inv_rect_Type0 hterm h1 h2 =
 136   let hcut = region_rect_Type0 h1 h2 hterm in hcut __
 137
 138 (** val region_discr : region -> region -> __ **)
 139 let region_discr x y =
 140   Logic.eq_rect_Type2 x
 141     (match x with
 142      | XData -> Obj.magic (fun _ dH -> dH)
 143      | Code -> Obj.magic (fun _ dH -> dH)) y
 144
 145 (** val region_jmdiscr : region -> region -> __ **)
 146 let region_jmdiscr x y =
 147   Logic.eq_rect_Type2 x
 148     (match x with
 149      | XData -> Obj.magic (fun _ dH -> dH)
 150      | Code -> Obj.magic (fun _ dH -> dH)) y
 151
 152 (** val eq_region : region -> region -> Bool.bool **)
 153 let eq_region r1 r2 =
 154   match r1 with
 155   | XData ->
 156     (match r2 with
 157      | XData -> Bool.True
 158      | Code -> Bool.False)
 159   | Code ->
 160     (match r2 with
 161      | XData -> Bool.False
 162      | Code -> Bool.True)
 163
 164 (** val eq_region_elim :
 165     region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 166 let eq_region_elim r1 r2 =
 167   match r1 with
 168   | XData ->
 169     (match r2 with
 170      | XData -> (fun ptrue pfalse -> ptrue __)
 171      | Code -> (fun ptrue pfalse -> pfalse __))
 172   | Code ->
 173     (match r2 with
 174      | XData -> (fun ptrue pfalse -> pfalse __)
 175      | Code -> (fun ptrue pfalse -> ptrue __))
 176
 177 (** val eq_region_dec : region -> region -> (__, __) Types.sum **)
 178 let eq_region_dec r1 r2 =
 179   eq_region_elim r1 r2 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
 180
 181 (** val size_pointer : Nat.nat **)
 182 let size_pointer =
 183   Nat.S (Nat.S Nat.O)
 184
 185 type signedness =
 186 | Signed
 187 | Unsigned
 188
 189 (** val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 190 let rec signedness_rect_Type4 h_Signed h_Unsigned = function
 191 | Signed -> h_Signed
 192 | Unsigned -> h_Unsigned
 193
 194 (** val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 195 let rec signedness_rect_Type5 h_Signed h_Unsigned = function
 196 | Signed -> h_Signed
 197 | Unsigned -> h_Unsigned
 198
 199 (** val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 200 let rec signedness_rect_Type3 h_Signed h_Unsigned = function
 201 | Signed -> h_Signed
 202 | Unsigned -> h_Unsigned
 203
 204 (** val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 205 let rec signedness_rect_Type2 h_Signed h_Unsigned = function
 206 | Signed -> h_Signed
 207 | Unsigned -> h_Unsigned
 208
 209 (** val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 210 let rec signedness_rect_Type1 h_Signed h_Unsigned = function
 211 | Signed -> h_Signed
 212 | Unsigned -> h_Unsigned
 213
 214 (** val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1 **)
 215 let rec signedness_rect_Type0 h_Signed h_Unsigned = function
 216 | Signed -> h_Signed
 217 | Unsigned -> h_Unsigned
 218
 219 (** val signedness_inv_rect_Type4 :
 220     signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 221 let signedness_inv_rect_Type4 hterm h1 h2 =
 222   let hcut = signedness_rect_Type4 h1 h2 hterm in hcut __
 223
 224 (** val signedness_inv_rect_Type3 :
 225     signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 226 let signedness_inv_rect_Type3 hterm h1 h2 =
 227   let hcut = signedness_rect_Type3 h1 h2 hterm in hcut __
 228
 229 (** val signedness_inv_rect_Type2 :
 230     signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 231 let signedness_inv_rect_Type2 hterm h1 h2 =
 232   let hcut = signedness_rect_Type2 h1 h2 hterm in hcut __
 233
 234 (** val signedness_inv_rect_Type1 :
 235     signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 236 let signedness_inv_rect_Type1 hterm h1 h2 =
 237   let hcut = signedness_rect_Type1 h1 h2 hterm in hcut __
 238
 239 (** val signedness_inv_rect_Type0 :
 240     signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 241 let signedness_inv_rect_Type0 hterm h1 h2 =
 242   let hcut = signedness_rect_Type0 h1 h2 hterm in hcut __
 243
 244 (** val signedness_discr : signedness -> signedness -> __ **)
 245 let signedness_discr x y =
 246   Logic.eq_rect_Type2 x
 247     (match x with
 248      | Signed -> Obj.magic (fun _ dH -> dH)
 249      | Unsigned -> Obj.magic (fun _ dH -> dH)) y
 250
 251 (** val signedness_jmdiscr : signedness -> signedness -> __ **)
 252 let signedness_jmdiscr x y =
 253   Logic.eq_rect_Type2 x
 254     (match x with
 255      | Signed -> Obj.magic (fun _ dH -> dH)
 256      | Unsigned -> Obj.magic (fun _ dH -> dH)) y
 257
 258 type intsize =
 259 | I8
 260 | I16
 261 | I32
 262
 263 (** val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 264 let rec intsize_rect_Type4 h_I8 h_I16 h_I32 = function
 265 | I8 -> h_I8
 266 | I16 -> h_I16
 267 | I32 -> h_I32
 268
 269 (** val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 270 let rec intsize_rect_Type5 h_I8 h_I16 h_I32 = function
 271 | I8 -> h_I8
 272 | I16 -> h_I16
 273 | I32 -> h_I32
 274
 275 (** val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 276 let rec intsize_rect_Type3 h_I8 h_I16 h_I32 = function
 277 | I8 -> h_I8
 278 | I16 -> h_I16
 279 | I32 -> h_I32
 280
 281 (** val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 282 let rec intsize_rect_Type2 h_I8 h_I16 h_I32 = function
 283 | I8 -> h_I8
 284 | I16 -> h_I16
 285 | I32 -> h_I32
 286
 287 (** val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 288 let rec intsize_rect_Type1 h_I8 h_I16 h_I32 = function
 289 | I8 -> h_I8
 290 | I16 -> h_I16
 291 | I32 -> h_I32
 292
 293 (** val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
 294 let rec intsize_rect_Type0 h_I8 h_I16 h_I32 = function
 295 | I8 -> h_I8
 296 | I16 -> h_I16
 297 | I32 -> h_I32
 298
 299 (** val intsize_inv_rect_Type4 :
 300     intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 301 let intsize_inv_rect_Type4 hterm h1 h2 h3 =
 302   let hcut = intsize_rect_Type4 h1 h2 h3 hterm in hcut __
 303
 304 (** val intsize_inv_rect_Type3 :
 305     intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 306 let intsize_inv_rect_Type3 hterm h1 h2 h3 =
 307   let hcut = intsize_rect_Type3 h1 h2 h3 hterm in hcut __
 308
 309 (** val intsize_inv_rect_Type2 :
 310     intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 311 let intsize_inv_rect_Type2 hterm h1 h2 h3 =
 312   let hcut = intsize_rect_Type2 h1 h2 h3 hterm in hcut __
 313
 314 (** val intsize_inv_rect_Type1 :
 315     intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 316 let intsize_inv_rect_Type1 hterm h1 h2 h3 =
 317   let hcut = intsize_rect_Type1 h1 h2 h3 hterm in hcut __
 318
 319 (** val intsize_inv_rect_Type0 :
 320     intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 321 let intsize_inv_rect_Type0 hterm h1 h2 h3 =
 322   let hcut = intsize_rect_Type0 h1 h2 h3 hterm in hcut __
 323
 324 (** val intsize_discr : intsize -> intsize -> __ **)
 325 let intsize_discr x y =
 326   Logic.eq_rect_Type2 x
 327     (match x with
 328      | I8 -> Obj.magic (fun _ dH -> dH)
 329      | I16 -> Obj.magic (fun _ dH -> dH)
 330      | I32 -> Obj.magic (fun _ dH -> dH)) y
 331
 332 (** val intsize_jmdiscr : intsize -> intsize -> __ **)
 333 let intsize_jmdiscr x y =
 334   Logic.eq_rect_Type2 x
 335     (match x with
 336      | I8 -> Obj.magic (fun _ dH -> dH)
 337      | I16 -> Obj.magic (fun _ dH -> dH)
 338      | I32 -> Obj.magic (fun _ dH -> dH)) y
 339
 340 type floatsize =
 341 | F32
 342 | F64
 343
 344 (** val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 345 let rec floatsize_rect_Type4 h_F32 h_F64 = function
 346 | F32 -> h_F32
 347 | F64 -> h_F64
 348
 349 (** val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 350 let rec floatsize_rect_Type5 h_F32 h_F64 = function
 351 | F32 -> h_F32
 352 | F64 -> h_F64
 353
 354 (** val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 355 let rec floatsize_rect_Type3 h_F32 h_F64 = function
 356 | F32 -> h_F32
 357 | F64 -> h_F64
 358
 359 (** val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 360 let rec floatsize_rect_Type2 h_F32 h_F64 = function
 361 | F32 -> h_F32
 362 | F64 -> h_F64
 363
 364 (** val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 365 let rec floatsize_rect_Type1 h_F32 h_F64 = function
 366 | F32 -> h_F32
 367 | F64 -> h_F64
 368
 369 (** val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
 370 let rec floatsize_rect_Type0 h_F32 h_F64 = function
 371 | F32 -> h_F32
 372 | F64 -> h_F64
 373
 374 (** val floatsize_inv_rect_Type4 :
 375     floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 376 let floatsize_inv_rect_Type4 hterm h1 h2 =
 377   let hcut = floatsize_rect_Type4 h1 h2 hterm in hcut __
 378
 379 (** val floatsize_inv_rect_Type3 :
 380     floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 381 let floatsize_inv_rect_Type3 hterm h1 h2 =
 382   let hcut = floatsize_rect_Type3 h1 h2 hterm in hcut __
 383
 384 (** val floatsize_inv_rect_Type2 :
 385     floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 386 let floatsize_inv_rect_Type2 hterm h1 h2 =
 387   let hcut = floatsize_rect_Type2 h1 h2 hterm in hcut __
 388
 389 (** val floatsize_inv_rect_Type1 :
 390     floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 391 let floatsize_inv_rect_Type1 hterm h1 h2 =
 392   let hcut = floatsize_rect_Type1 h1 h2 hterm in hcut __
 393
 394 (** val floatsize_inv_rect_Type0 :
 395     floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 396 let floatsize_inv_rect_Type0 hterm h1 h2 =
 397   let hcut = floatsize_rect_Type0 h1 h2 hterm in hcut __
 398
 399 (** val floatsize_discr : floatsize -> floatsize -> __ **)
 400 let floatsize_discr x y =
 401   Logic.eq_rect_Type2 x
 402     (match x with
 403      | F32 -> Obj.magic (fun _ dH -> dH)
 404      | F64 -> Obj.magic (fun _ dH -> dH)) y
 405
 406 (** val floatsize_jmdiscr : floatsize -> floatsize -> __ **)
 407 let floatsize_jmdiscr x y =
 408   Logic.eq_rect_Type2 x
 409     (match x with
 410      | F32 -> Obj.magic (fun _ dH -> dH)
 411      | F64 -> Obj.magic (fun _ dH -> dH)) y
 412
 413 type typ =
 414 | ASTint of intsize * signedness
 415 | ASTptr
 416
 417 (** val typ_rect_Type4 :
 418     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 419 let rec typ_rect_Type4 h_ASTint h_ASTptr = function
 420 | ASTint (x_3662, x_3661) -> h_ASTint x_3662 x_3661
 421 | ASTptr -> h_ASTptr
 422
 423 (** val typ_rect_Type5 :
 424     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 425 let rec typ_rect_Type5 h_ASTint h_ASTptr = function
 426 | ASTint (x_3667, x_3666) -> h_ASTint x_3667 x_3666
 427 | ASTptr -> h_ASTptr
 428
 429 (** val typ_rect_Type3 :
 430     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 431 let rec typ_rect_Type3 h_ASTint h_ASTptr = function
 432 | ASTint (x_3672, x_3671) -> h_ASTint x_3672 x_3671
 433 | ASTptr -> h_ASTptr
 434
 435 (** val typ_rect_Type2 :
 436     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 437 let rec typ_rect_Type2 h_ASTint h_ASTptr = function
 438 | ASTint (x_3677, x_3676) -> h_ASTint x_3677 x_3676
 439 | ASTptr -> h_ASTptr
 440
 441 (** val typ_rect_Type1 :
 442     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 443 let rec typ_rect_Type1 h_ASTint h_ASTptr = function
 444 | ASTint (x_3682, x_3681) -> h_ASTint x_3682 x_3681
 445 | ASTptr -> h_ASTptr
 446
 447 (** val typ_rect_Type0 :
 448     (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
 449 let rec typ_rect_Type0 h_ASTint h_ASTptr = function
 450 | ASTint (x_3687, x_3686) -> h_ASTint x_3687 x_3686
 451 | ASTptr -> h_ASTptr
 452
 453 (** val typ_inv_rect_Type4 :
 454     typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 455 let typ_inv_rect_Type4 hterm h1 h2 =
 456   let hcut = typ_rect_Type4 h1 h2 hterm in hcut __
 457
 458 (** val typ_inv_rect_Type3 :
 459     typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 460 let typ_inv_rect_Type3 hterm h1 h2 =
 461   let hcut = typ_rect_Type3 h1 h2 hterm in hcut __
 462
 463 (** val typ_inv_rect_Type2 :
 464     typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 465 let typ_inv_rect_Type2 hterm h1 h2 =
 466   let hcut = typ_rect_Type2 h1 h2 hterm in hcut __
 467
 468 (** val typ_inv_rect_Type1 :
 469     typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 470 let typ_inv_rect_Type1 hterm h1 h2 =
 471   let hcut = typ_rect_Type1 h1 h2 hterm in hcut __
 472
 473 (** val typ_inv_rect_Type0 :
 474     typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 475 let typ_inv_rect_Type0 hterm h1 h2 =
 476   let hcut = typ_rect_Type0 h1 h2 hterm in hcut __
 477
 478 (** val typ_discr : typ -> typ -> __ **)
 479 let typ_discr x y =
 480   Logic.eq_rect_Type2 x
 481     (match x with
 482      | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 483      | ASTptr -> Obj.magic (fun _ dH -> dH)) y
 484
 485 (** val typ_jmdiscr : typ -> typ -> __ **)
 486 let typ_jmdiscr x y =
 487   Logic.eq_rect_Type2 x
 488     (match x with
 489      | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 490      | ASTptr -> Obj.magic (fun _ dH -> dH)) y
 491
 492 type sigType = typ
 493
 494 (** val sigType_Int : typ **)
 495 let sigType_Int =
 496   ASTint (I32, Unsigned)
 497
 498 (** val sigType_Ptr : typ **)
 499 let sigType_Ptr =
 500   ASTptr
 501
 502 (** val pred_size_intsize : intsize -> Nat.nat **)
 503 let pred_size_intsize = function
 504 | I8 -> Nat.O
 505 | I16 -> Nat.S Nat.O
 506 | I32 -> Nat.S (Nat.S (Nat.S Nat.O))
 507
 508 (** val size_intsize : intsize -> Nat.nat **)
 509 let size_intsize sz =
 510   Nat.S (pred_size_intsize sz)
 511
 512 (** val bitsize_of_intsize : intsize -> Nat.nat **)
 513 let bitsize_of_intsize sz =
 514   Nat.times (size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 515     (Nat.S (Nat.S Nat.O))))))))
 516
 517 (** val eq_intsize : intsize -> intsize -> Bool.bool **)
 518 let eq_intsize sz1 sz2 =
 519   match sz1 with
 520   | I8 ->
 521     (match sz2 with
 522      | I8 -> Bool.True
 523      | I16 -> Bool.False
 524      | I32 -> Bool.False)
 525   | I16 ->
 526     (match sz2 with
 527      | I8 -> Bool.False
 528      | I16 -> Bool.True
 529      | I32 -> Bool.False)
 530   | I32 ->
 531     (match sz2 with
 532      | I8 -> Bool.False
 533      | I16 -> Bool.False
 534      | I32 -> Bool.True)
 535
 536 (** val eq_intsize_elim :
 537     intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 538 let eq_intsize_elim clearme sz2 x x0 =
 539   (match clearme with
 540    | I8 ->
 541      (fun clearme0 ->
 542        match clearme0 with
 543        | I8 -> (fun _ hne heq -> heq __)
 544        | I16 -> (fun _ hne heq -> hne __)
 545        | I32 -> (fun _ hne heq -> hne __))
 546    | I16 ->
 547      (fun clearme0 ->
 548        match clearme0 with
 549        | I8 -> (fun _ hne heq -> hne __)
 550        | I16 -> (fun _ hne heq -> heq __)
 551        | I32 -> (fun _ hne heq -> hne __))
 552    | I32 ->
 553      (fun clearme0 ->
 554        match clearme0 with
 555        | I8 -> (fun _ hne heq -> hne __)
 556        | I16 -> (fun _ hne heq -> hne __)
 557        | I32 -> (fun _ hne heq -> heq __))) sz2 __ x x0
 558
 559 (** val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
 560 let signedness_check sg1 sg2 =
 561   match sg1 with
 562   | Signed ->
 563     (fun x ->
 564       match sg2 with
 565       | Signed -> (fun d -> x)
 566       | Unsigned -> (fun d -> d))
 567   | Unsigned ->
 568     (fun x ->
 569       match sg2 with
 570       | Signed -> (fun d -> d)
 571       | Unsigned -> (fun d -> x))
 572
 573 (** val inttyp_eq_elim' :
 574     intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
 575 let rec inttyp_eq_elim' sz1 sz2 sg1 sg2 =
 576   match sz1 with
 577   | I8 ->
 578     (fun x ->
 579       match sz2 with
 580       | I8 -> signedness_check sg1 sg2 x
 581       | I16 -> (fun d -> d)
 582       | I32 -> (fun d -> d))
 583   | I16 ->
 584     (fun x ->
 585       match sz2 with
 586       | I8 -> (fun d -> d)
 587       | I16 -> signedness_check sg1 sg2 x
 588       | I32 -> (fun d -> d))
 589   | I32 ->
 590     (fun x ->
 591       match sz2 with
 592       | I8 -> (fun d -> d)
 593       | I16 -> (fun d -> d)
 594       | I32 -> signedness_check sg1 sg2 x)
 595
 596 (** val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1 **)
 597 let rec intsize_eq_elim' sz1 sz2 =
 598   match sz1 with
 599   | I8 ->
 600     (fun x ->
 601       match sz2 with
 602       | I8 -> (fun d -> x)
 603       | I16 -> (fun d -> d)
 604       | I32 -> (fun d -> d))
 605   | I16 ->
 606     (fun x ->
 607       match sz2 with
 608       | I8 -> (fun d -> d)
 609       | I16 -> (fun d -> x)
 610       | I32 -> (fun d -> d))
 611   | I32 ->
 612     (fun x ->
 613       match sz2 with
 614       | I8 -> (fun d -> d)
 615       | I16 -> (fun d -> d)
 616       | I32 -> (fun d -> x))
 617
 618 (** val intsize_eq_elim :
 619     intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1 **)
 620 let rec intsize_eq_elim sz1 sz2 =
 621   match sz1 with
 622   | I8 ->
 623     (fun x ->
 624       match sz2 with
 625       | I8 -> (fun f d -> f x)
 626       | I16 -> (fun f d -> d)
 627       | I32 -> (fun f d -> d))
 628   | I16 ->
 629     (fun x ->
 630       match sz2 with
 631       | I8 -> (fun f d -> d)
 632       | I16 -> (fun f d -> f x)
 633       | I32 -> (fun f d -> d))
 634   | I32 ->
 635     (fun x ->
 636       match sz2 with
 637       | I8 -> (fun f d -> d)
 638       | I16 -> (fun f d -> d)
 639       | I32 -> (fun f d -> f x))
 640
 641 (** val intsize_eq_elim_elim :
 642     intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
 643     __) -> 'a3 **)
 644 let intsize_eq_elim_elim clearme sz2 p f d x x0 =
 645   (match clearme with
 646    | I8 ->
 647      (fun clearme0 ->
 648        match clearme0 with
 649        | I8 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
 650        | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
 651        | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
 652    | I16 ->
 653      (fun clearme0 ->
 654        match clearme0 with
 655        | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
 656        | I16 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
 657        | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
 658    | I32 ->
 659      (fun clearme0 ->
 660        match clearme0 with
 661        | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
 662        | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
 663        | I32 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __))) sz2 __ p f d
 664     __ x x0
 665
 666 type bvint = BitVector.bitVector
 667
 668 (** val repr : intsize -> Nat.nat -> bvint **)
 669 let repr sz x =
 670   Arithmetic.bitvector_of_nat (bitsize_of_intsize sz) x
 671
 672 (** val size_floatsize : floatsize -> Nat.nat **)
 673 let size_floatsize sz =
 674   Nat.S
 675     (match sz with
 676      | F32 -> Nat.S (Nat.S (Nat.S Nat.O))
 677      | F64 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
 678
 679 (** val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1 **)
 680 let rec floatsize_eq_elim sz1 sz2 =
 681   match sz1 with
 682   | F32 ->
 683     (fun x ->
 684       match sz2 with
 685       | F32 -> (fun d -> x)
 686       | F64 -> (fun d -> d))
 687   | F64 ->
 688     (fun x ->
 689       match sz2 with
 690       | F32 -> (fun d -> d)
 691       | F64 -> (fun d -> x))
 692
 693 (** val typesize : typ -> Nat.nat **)
 694 let typesize = function
 695 | ASTint (sz, x) -> size_intsize sz
 696 | ASTptr -> size_pointer
 697
 698 (** val typ_eq : typ -> typ -> (__, __) Types.sum **)
 699 let typ_eq = function
 700 | ASTint (clearme0, x) ->
 701   (match clearme0 with
 702    | I8 ->
 703      (fun clearme1 ->
 704        match clearme1 with
 705        | Signed ->
 706          (fun clearme2 ->
 707            match clearme2 with
 708            | ASTint (clearme3, x0) ->
 709              (match clearme3 with
 710               | I8 ->
 711                 (fun clearme4 ->
 712                   match clearme4 with
 713                   | Signed -> Types.Inl __
 714                   | Unsigned -> Types.Inr __)
 715               | I16 ->
 716                 (fun clearme4 ->
 717                   match clearme4 with
 718                   | Signed -> Types.Inr __
 719                   | Unsigned -> Types.Inr __)
 720               | I32 ->
 721                 (fun clearme4 ->
 722                   match clearme4 with
 723                   | Signed -> Types.Inr __
 724                   | Unsigned -> Types.Inr __)) x0
 725            | ASTptr -> Types.Inr __)
 726        | Unsigned ->
 727          (fun clearme2 ->
 728            match clearme2 with
 729            | ASTint (clearme3, x0) ->
 730              (match clearme3 with
 731               | I8 ->
 732                 (fun clearme4 ->
 733                   match clearme4 with
 734                   | Signed -> Types.Inr __
 735                   | Unsigned -> Types.Inl __)
 736               | I16 ->
 737                 (fun clearme4 ->
 738                   match clearme4 with
 739                   | Signed -> Types.Inr __
 740                   | Unsigned -> Types.Inr __)
 741               | I32 ->
 742                 (fun clearme4 ->
 743                   match clearme4 with
 744                   | Signed -> Types.Inr __
 745                   | Unsigned -> Types.Inr __)) x0
 746            | ASTptr -> Types.Inr __))
 747    | I16 ->
 748      (fun clearme1 ->
 749        match clearme1 with
 750        | Signed ->
 751          (fun clearme2 ->
 752            match clearme2 with
 753            | ASTint (clearme3, x0) ->
 754              (match clearme3 with
 755               | I8 ->
 756                 (fun clearme4 ->
 757                   match clearme4 with
 758                   | Signed -> Types.Inr __
 759                   | Unsigned -> Types.Inr __)
 760               | I16 ->
 761                 (fun clearme4 ->
 762                   match clearme4 with
 763                   | Signed -> Types.Inl __
 764                   | Unsigned -> Types.Inr __)
 765               | I32 ->
 766                 (fun clearme4 ->
 767                   match clearme4 with
 768                   | Signed -> Types.Inr __
 769                   | Unsigned -> Types.Inr __)) x0
 770            | ASTptr -> Types.Inr __)
 771        | Unsigned ->
 772          (fun clearme2 ->
 773            match clearme2 with
 774            | ASTint (clearme3, x0) ->
 775              (match clearme3 with
 776               | I8 ->
 777                 (fun clearme4 ->
 778                   match clearme4 with
 779                   | Signed -> Types.Inr __
 780                   | Unsigned -> Types.Inr __)
 781               | I16 ->
 782                 (fun clearme4 ->
 783                   match clearme4 with
 784                   | Signed -> Types.Inr __
 785                   | Unsigned -> Types.Inl __)
 786               | I32 ->
 787                 (fun clearme4 ->
 788                   match clearme4 with
 789                   | Signed -> Types.Inr __
 790                   | Unsigned -> Types.Inr __)) x0
 791            | ASTptr -> Types.Inr __))
 792    | I32 ->
 793      (fun clearme1 ->
 794        match clearme1 with
 795        | Signed ->
 796          (fun clearme2 ->
 797            match clearme2 with
 798            | ASTint (clearme3, x0) ->
 799              (match clearme3 with
 800               | I8 ->
 801                 (fun clearme4 ->
 802                   match clearme4 with
 803                   | Signed -> Types.Inr __
 804                   | Unsigned -> Types.Inr __)
 805               | I16 ->
 806                 (fun clearme4 ->
 807                   match clearme4 with
 808                   | Signed -> Types.Inr __
 809                   | Unsigned -> Types.Inr __)
 810               | I32 ->
 811                 (fun clearme4 ->
 812                   match clearme4 with
 813                   | Signed -> Types.Inl __
 814                   | Unsigned -> Types.Inr __)) x0
 815            | ASTptr -> Types.Inr __)
 816        | Unsigned ->
 817          (fun clearme2 ->
 818            match clearme2 with
 819            | ASTint (clearme3, x0) ->
 820              (match clearme3 with
 821               | I8 ->
 822                 (fun clearme4 ->
 823                   match clearme4 with
 824                   | Signed -> Types.Inr __
 825                   | Unsigned -> Types.Inr __)
 826               | I16 ->
 827                 (fun clearme4 ->
 828                   match clearme4 with
 829                   | Signed -> Types.Inr __
 830                   | Unsigned -> Types.Inr __)
 831               | I32 ->
 832                 (fun clearme4 ->
 833                   match clearme4 with
 834                   | Signed -> Types.Inr __
 835                   | Unsigned -> Types.Inl __)) x0
 836            | ASTptr -> Types.Inr __))) x
 837 | ASTptr ->
 838   (fun clearme0 ->
 839     match clearme0 with
 840     | ASTint (clearme1, x) ->
 841       (match clearme1 with
 842        | I8 ->
 843          (fun clearme2 ->
 844            match clearme2 with
 845            | Signed -> Types.Inr __
 846            | Unsigned -> Types.Inr __)
 847        | I16 ->
 848          (fun clearme2 ->
 849            match clearme2 with
 850            | Signed -> Types.Inr __
 851            | Unsigned -> Types.Inr __)
 852        | I32 ->
 853          (fun clearme2 ->
 854            match clearme2 with
 855            | Signed -> Types.Inr __
 856            | Unsigned -> Types.Inr __)) x
 857     | ASTptr -> Types.Inl __)
 858
 859 (** val opt_typ_eq :
 860     typ Types.option -> typ Types.option -> (__, __) Types.sum **)
 861 let opt_typ_eq t1 t2 =
 862   match t1 with
 863   | Types.None ->
 864     (match t2 with
 865      | Types.None -> Types.Inl __
 866      | Types.Some ty -> Types.Inr __)
 867   | Types.Some x ->
 868     (match t2 with
 869      | Types.None -> (fun ty -> Types.Inr __)
 870      | Types.Some ty1 ->
 871        (fun ty2 ->
 872          Types.sum_rect_Type0 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
 873            (typ_eq ty1 ty2))) x
 874
 875 type signature = { sig_args : typ List.list; sig_res : typ Types.option }
 876
 877 (** val signature_rect_Type4 :
 878     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 879 let rec signature_rect_Type4 h_mk_signature x_3722 =
 880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3722 in
 881   h_mk_signature sig_args0 sig_res0
 882
 883 (** val signature_rect_Type5 :
 884     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 885 let rec signature_rect_Type5 h_mk_signature x_3724 =
 886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3724 in
 887   h_mk_signature sig_args0 sig_res0
 888
 889 (** val signature_rect_Type3 :
 890     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 891 let rec signature_rect_Type3 h_mk_signature x_3726 =
 892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3726 in
 893   h_mk_signature sig_args0 sig_res0
 894
 895 (** val signature_rect_Type2 :
 896     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 897 let rec signature_rect_Type2 h_mk_signature x_3728 =
 898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3728 in
 899   h_mk_signature sig_args0 sig_res0
 900
 901 (** val signature_rect_Type1 :
 902     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 903 let rec signature_rect_Type1 h_mk_signature x_3730 =
 904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3730 in
 905   h_mk_signature sig_args0 sig_res0
 906
 907 (** val signature_rect_Type0 :
 908     (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
 909 let rec signature_rect_Type0 h_mk_signature x_3732 =
 910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3732 in
 911   h_mk_signature sig_args0 sig_res0
 912
 913 (** val sig_args : signature -> typ List.list **)
 914 let rec sig_args xxx =
 915   xxx.sig_args
 916
 917 (** val sig_res : signature -> typ Types.option **)
 918 let rec sig_res xxx =
 919   xxx.sig_res
 920
 921 (** val signature_inv_rect_Type4 :
 922     signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
 923 let signature_inv_rect_Type4 hterm h1 =
 924   let hcut = signature_rect_Type4 h1 hterm in hcut __
 925
 926 (** val signature_inv_rect_Type3 :
 927     signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
 928 let signature_inv_rect_Type3 hterm h1 =
 929   let hcut = signature_rect_Type3 h1 hterm in hcut __
 930
 931 (** val signature_inv_rect_Type2 :
 932     signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
 933 let signature_inv_rect_Type2 hterm h1 =
 934   let hcut = signature_rect_Type2 h1 hterm in hcut __
 935
 936 (** val signature_inv_rect_Type1 :
 937     signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
 938 let signature_inv_rect_Type1 hterm h1 =
 939   let hcut = signature_rect_Type1 h1 hterm in hcut __
 940
 941 (** val signature_inv_rect_Type0 :
 942     signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
 943 let signature_inv_rect_Type0 hterm h1 =
 944   let hcut = signature_rect_Type0 h1 hterm in hcut __
 945
 946 (** val signature_discr : signature -> signature -> __ **)
 947 let signature_discr x y =
 948   Logic.eq_rect_Type2 x
 949     (let { sig_args = a0; sig_res = a1 } = x in
 950     Obj.magic (fun _ dH -> dH __ __)) y
 951
 952 (** val signature_jmdiscr : signature -> signature -> __ **)
 953 let signature_jmdiscr x y =
 954   Logic.eq_rect_Type2 x
 955     (let { sig_args = a0; sig_res = a1 } = x in
 956     Obj.magic (fun _ dH -> dH __ __)) y
 957
 958 type signature0 = signature
 959
 960 (** val signature_args : signature -> typ List.list **)
 961 let signature_args =
 962   sig_args
 963
 964 (** val signature_return : signature -> typ Types.option **)
 965 let signature_return =
 966   sig_res
 967
 968 (** val proj_sig_res : signature -> typ **)
 969 let proj_sig_res s =
 970   match s.sig_res with
 971   | Types.None -> ASTint (I32, Unsigned)
 972   | Types.Some t -> t
 973
 974 type init_data =
 975 | Init_int8 of bvint
 976 | Init_int16 of bvint
 977 | Init_int32 of bvint
 978 | Init_space of Nat.nat
 979 | Init_null
 980 | Init_addrof of ident * Nat.nat
 981
 982 (** val init_data_rect_Type4 :
 983     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 984     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
 985 let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
 986 | Init_int8 x_3760 -> h_Init_int8 x_3760
 987 | Init_int16 x_3761 -> h_Init_int16 x_3761
 988 | Init_int32 x_3762 -> h_Init_int32 x_3762
 989 | Init_space x_3763 -> h_Init_space x_3763
 990 | Init_null -> h_Init_null
 991 | Init_addrof (x_3765, x_3764) -> h_Init_addrof x_3765 x_3764
 992
 993 (** val init_data_rect_Type5 :
 994     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 995     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
 996 let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
 997 | Init_int8 x_3773 -> h_Init_int8 x_3773
 998 | Init_int16 x_3774 -> h_Init_int16 x_3774
 999 | Init_int32 x_3775 -> h_Init_int32 x_3775
1000 | Init_space x_3776 -> h_Init_space x_3776
1001 | Init_null -> h_Init_null
1002 | Init_addrof (x_3778, x_3777) -> h_Init_addrof x_3778 x_3777
1003
1004 (** val init_data_rect_Type3 :
1005     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
1006     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
1007 let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
1008 | Init_int8 x_3786 -> h_Init_int8 x_3786
1009 | Init_int16 x_3787 -> h_Init_int16 x_3787
1010 | Init_int32 x_3788 -> h_Init_int32 x_3788
1011 | Init_space x_3789 -> h_Init_space x_3789
1012 | Init_null -> h_Init_null
1013 | Init_addrof (x_3791, x_3790) -> h_Init_addrof x_3791 x_3790
1014
1015 (** val init_data_rect_Type2 :
1016     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
1017     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
1018 let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
1019 | Init_int8 x_3799 -> h_Init_int8 x_3799
1020 | Init_int16 x_3800 -> h_Init_int16 x_3800
1021 | Init_int32 x_3801 -> h_Init_int32 x_3801
1022 | Init_space x_3802 -> h_Init_space x_3802
1023 | Init_null -> h_Init_null
1024 | Init_addrof (x_3804, x_3803) -> h_Init_addrof x_3804 x_3803
1025
1026 (** val init_data_rect_Type1 :
1027     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
1028     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
1029 let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
1030 | Init_int8 x_3812 -> h_Init_int8 x_3812
1031 | Init_int16 x_3813 -> h_Init_int16 x_3813
1032 | Init_int32 x_3814 -> h_Init_int32 x_3814
1033 | Init_space x_3815 -> h_Init_space x_3815
1034 | Init_null -> h_Init_null
1035 | Init_addrof (x_3817, x_3816) -> h_Init_addrof x_3817 x_3816
1036
1037 (** val init_data_rect_Type0 :
1038     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
1039     'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
1040 let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
1041 | Init_int8 x_3825 -> h_Init_int8 x_3825
1042 | Init_int16 x_3826 -> h_Init_int16 x_3826
1043 | Init_int32 x_3827 -> h_Init_int32 x_3827
1044 | Init_space x_3828 -> h_Init_space x_3828
1045 | Init_null -> h_Init_null
1046 | Init_addrof (x_3830, x_3829) -> h_Init_addrof x_3830 x_3829
1047
1048 (** val init_data_inv_rect_Type4 :
1049     init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1050     -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
1051     __ -> 'a1) -> 'a1 **)
1052 let init_data_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
1053   let hcut = init_data_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
1054
1055 (** val init_data_inv_rect_Type3 :
1056     init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1057     -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
1058     __ -> 'a1) -> 'a1 **)
1059 let init_data_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
1060   let hcut = init_data_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
1061
1062 (** val init_data_inv_rect_Type2 :
1063     init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1064     -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
1065     __ -> 'a1) -> 'a1 **)
1066 let init_data_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
1067   let hcut = init_data_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
1068
1069 (** val init_data_inv_rect_Type1 :
1070     init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1071     -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
1072     __ -> 'a1) -> 'a1 **)
1073 let init_data_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
1074   let hcut = init_data_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
1075
1076 (** val init_data_inv_rect_Type0 :
1077     init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1078     -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
1079     __ -> 'a1) -> 'a1 **)
1080 let init_data_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
1081   let hcut = init_data_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
1082
1083 (** val init_data_discr : init_data -> init_data -> __ **)
1084 let init_data_discr x y =
1085   Logic.eq_rect_Type2 x
1086     (match x with
1087      | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
1088      | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
1089      | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
1090      | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
1091      | Init_null -> Obj.magic (fun _ dH -> dH)
1092      | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1093
1094 (** val init_data_jmdiscr : init_data -> init_data -> __ **)
1095 let init_data_jmdiscr x y =
1096   Logic.eq_rect_Type2 x
1097     (match x with
1098      | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
1099      | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
1100      | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
1101      | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
1102      | Init_null -> Obj.magic (fun _ dH -> dH)
1103      | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1104
1105 type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
1106                                       Types.prod List.list;
1107                           prog_funct : (ident, 'f) Types.prod List.list;
1108                           prog_main : ident }
1109
1110 (** val program_rect_Type4 :
1111     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1112     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1113 let rec program_rect_Type4 h_mk_program x_3917 =
1114   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1115     prog_main0 } = x_3917
1116   in
1117   h_mk_program prog_vars0 prog_funct0 prog_main0
1118
1119 (** val program_rect_Type5 :
1120     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1121     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1122 let rec program_rect_Type5 h_mk_program x_3919 =
1123   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1124     prog_main0 } = x_3919
1125   in
1126   h_mk_program prog_vars0 prog_funct0 prog_main0
1127
1128 (** val program_rect_Type3 :
1129     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1130     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1131 let rec program_rect_Type3 h_mk_program x_3921 =
1132   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1133     prog_main0 } = x_3921
1134   in
1135   h_mk_program prog_vars0 prog_funct0 prog_main0
1136
1137 (** val program_rect_Type2 :
1138     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1139     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1140 let rec program_rect_Type2 h_mk_program x_3923 =
1141   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1142     prog_main0 } = x_3923
1143   in
1144   h_mk_program prog_vars0 prog_funct0 prog_main0
1145
1146 (** val program_rect_Type1 :
1147     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1148     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1149 let rec program_rect_Type1 h_mk_program x_3925 =
1150   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1151     prog_main0 } = x_3925
1152   in
1153   h_mk_program prog_vars0 prog_funct0 prog_main0
1154
1155 (** val program_rect_Type0 :
1156     (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1157     Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1158 let rec program_rect_Type0 h_mk_program x_3927 =
1159   let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1160     prog_main0 } = x_3927
1161   in
1162   h_mk_program prog_vars0 prog_funct0 prog_main0
1163
1164 (** val prog_vars :
1165     ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
1166     List.list **)
1167 let rec prog_vars xxx =
1168   xxx.prog_vars
1169
1170 (** val prog_funct :
1171     ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list **)
1172 let rec prog_funct xxx =
1173   xxx.prog_funct
1174
1175 (** val prog_main : ('a1, 'a2) program -> ident **)
1176 let rec prog_main xxx =
1177   xxx.prog_main
1178
1179 (** val program_inv_rect_Type4 :
1180     ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1181     List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1182     'a3 **)
1183 let program_inv_rect_Type4 hterm h1 =
1184   let hcut = program_rect_Type4 h1 hterm in hcut __
1185
1186 (** val program_inv_rect_Type3 :
1187     ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1188     List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1189     'a3 **)
1190 let program_inv_rect_Type3 hterm h1 =
1191   let hcut = program_rect_Type3 h1 hterm in hcut __
1192
1193 (** val program_inv_rect_Type2 :
1194     ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1195     List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1196     'a3 **)
1197 let program_inv_rect_Type2 hterm h1 =
1198   let hcut = program_rect_Type2 h1 hterm in hcut __
1199
1200 (** val program_inv_rect_Type1 :
1201     ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1202     List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1203     'a3 **)
1204 let program_inv_rect_Type1 hterm h1 =
1205   let hcut = program_rect_Type1 h1 hterm in hcut __
1206
1207 (** val program_inv_rect_Type0 :
1208     ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1209     List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1210     'a3 **)
1211 let program_inv_rect_Type0 hterm h1 =
1212   let hcut = program_rect_Type0 h1 hterm in hcut __
1213
1214 (** val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1215 let program_discr x y =
1216   Logic.eq_rect_Type2 x
1217     (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
1218     Obj.magic (fun _ dH -> dH __ __ __)) y
1219
1220 (** val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1221 let program_jmdiscr x y =
1222   Logic.eq_rect_Type2 x
1223     (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
1224     Obj.magic (fun _ dH -> dH __ __ __)) y
1225
1226 (** val prog_funct_names : ('a1, 'a2) program -> ident List.list **)
1227 let prog_funct_names p =
1228   List.map Types.fst p.prog_funct
1229
1230 (** val prog_var_names : ('a1, 'a2) program -> ident List.list **)
1231 let prog_var_names p =
1232   List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars
1233
1234 (** val transf_program :
1235     ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
1236     Types.prod List.list **)
1237 let transf_program transf l =
1238   List.map (fun id_fn -> { Types.fst = id_fn.Types.fst; Types.snd =
1239     (transf id_fn.Types.snd) }) l
1240
1241 (** val transform_program :
1242     ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3)
1243     program **)
1244 let transform_program p transf =
1245   { prog_vars = p.prog_vars; prog_funct =
1246     (transf_program
1247       (transf (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1248       p.prog_funct); prog_main = p.prog_main }
1249
1250 (** val transf_program_gen :
1251     PreIdentifiers.identifierTag -> Identifiers.universe ->
1252     (Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe) Types.prod)
1253     -> (ident, 'a1) Types.prod List.list -> ((ident, 'a2) Types.prod
1254     List.list, Identifiers.universe) Types.prod **)
1255 let transf_program_gen tag gen transf l =
1256   List.foldr (fun id_fn bs_gen ->
1257     let { Types.fst = fn'; Types.snd = gen' } =
1258       transf bs_gen.Types.snd id_fn.Types.snd
1259     in
1260     { Types.fst = (List.Cons ({ Types.fst = id_fn.Types.fst; Types.snd =
1261     fn' }, bs_gen.Types.fst)); Types.snd = gen' }) { Types.fst = List.Nil;
1262     Types.snd = gen } l
1263
1264 (** val transform_program_gen :
1265     PreIdentifiers.identifierTag -> Identifiers.universe -> ('a1, 'a3)
1266     program -> (ident List.list -> Identifiers.universe -> 'a1 -> ('a2,
1267     Identifiers.universe) Types.prod) -> (('a2, 'a3) program,
1268     Identifiers.universe) Types.prod **)
1269 let transform_program_gen tag gen p trans =
1270   let fsg =
1271     transf_program_gen tag gen
1272       (trans (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1273       p.prog_funct
1274   in
1275   { Types.fst = { prog_vars = p.prog_vars; prog_funct = fsg.Types.fst;
1276   prog_main = p.prog_main }; Types.snd = fsg.Types.snd }
1277
1278 (** val map_partial :
1279     ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
1280     Types.prod List.list Errors.res **)
1281 let map_partial f =
1282   Obj.magic
1283     (Monad.m_list_map (Monad.max_def Errors.res0) (fun ab ->
1284       let { Types.fst = a; Types.snd = b } = ab in
1285       Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f b) (fun c ->
1286         Obj.magic (Errors.OK { Types.fst = a; Types.snd = c }))))
1287
1288 (** val transform_partial_program :
1289     ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
1290     'a3) program Errors.res **)
1291 let transform_partial_program p transf_partial =
1292   Obj.magic
1293     (Monad.m_bind0 (Monad.max_def Errors.res0)
1294       (Obj.magic
1295         (map_partial
1296           (transf_partial
1297             (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1298           p.prog_funct)) (fun fl ->
1299       Obj.magic (Errors.OK { prog_vars = p.prog_vars; prog_funct = fl;
1300         prog_main = p.prog_main })))
1301
1302 (** val transform_partial_program2 :
1303     ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3
1304     -> 'a4 Errors.res) -> ('a2, 'a4) program Errors.res **)
1305 let transform_partial_program2 p transf_partial_function transf_partial_variable =
1306   Obj.magic
1307     (Monad.m_bind0 (Monad.max_def Errors.res0)
1308       (Obj.magic
1309         (map_partial
1310           (transf_partial_function
1311             (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1312           p.prog_funct)) (fun fl ->
1313       (match map_partial transf_partial_variable p.prog_vars with
1314        | Errors.OK vl ->
1315          (fun _ ->
1316            Obj.magic (Errors.OK { prog_vars = vl; prog_funct =
1317              (Logic.eq_rect_Type0
1318                (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars) fl
1319                (List.map (fun x -> x.Types.fst.Types.fst) vl)); prog_main =
1320              p.prog_main }))
1321        | Errors.Error err -> (fun _ -> Obj.magic (Errors.Error err))) __))
1322
1323 type matching =
1324 | Mk_matching
1325
1326 (** val matching_rect_Type4 :
1327     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1328 let rec matching_rect_Type4 h_mk_matching = function
1329 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1330
1331 (** val matching_rect_Type5 :
1332     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1333 let rec matching_rect_Type5 h_mk_matching = function
1334 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1335
1336 (** val matching_rect_Type3 :
1337     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1338 let rec matching_rect_Type3 h_mk_matching = function
1339 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1340
1341 (** val matching_rect_Type2 :
1342     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1343 let rec matching_rect_Type2 h_mk_matching = function
1344 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1345
1346 (** val matching_rect_Type1 :
1347     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1348 let rec matching_rect_Type1 h_mk_matching = function
1349 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1350
1351 (** val matching_rect_Type0 :
1352     (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1353 let rec matching_rect_Type0 h_mk_matching = function
1354 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1355
1356 type m_A = __
1357
1358 type m_B = __
1359
1360 type m_V = __
1361
1362 type m_W = __
1363
1364 (** val matching_inv_rect_Type4 :
1365     matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1366 let matching_inv_rect_Type4 hterm h1 =
1367   let hcut = matching_rect_Type4 h1 hterm in hcut __
1368
1369 (** val matching_inv_rect_Type3 :
1370     matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1371 let matching_inv_rect_Type3 hterm h1 =
1372   let hcut = matching_rect_Type3 h1 hterm in hcut __
1373
1374 (** val matching_inv_rect_Type2 :
1375     matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376 let matching_inv_rect_Type2 hterm h1 =
1377   let hcut = matching_rect_Type2 h1 hterm in hcut __
1378
1379 (** val matching_inv_rect_Type1 :
1380     matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1381 let matching_inv_rect_Type1 hterm h1 =
1382   let hcut = matching_rect_Type1 h1 hterm in hcut __
1383
1384 (** val matching_inv_rect_Type0 :
1385     matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1386 let matching_inv_rect_Type0 hterm h1 =
1387   let hcut = matching_rect_Type0 h1 hterm in hcut __
1388
1389 (** val matching_jmdiscr : matching -> matching -> __ **)
1390 let matching_jmdiscr x y =
1391   Logic.eq_rect_Type2 x
1392     (let Mk_matching = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1393
1394 (** val mfe_cast_fn_type :
1395     matching -> ident List.list -> ident List.list -> __ -> __ **)
1396 let mfe_cast_fn_type m vs vs' =
1397   Extralib.eq_rect_Type0_r vs (fun m0 -> m0) vs'
1398
1399 (** val match_program_rect_Type4 :
1400     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1401     'a1) -> 'a1 **)
1402 let rec match_program_rect_Type4 m p1 p2 h_mk_match_program =
1403   h_mk_match_program __ __ __
1404
1405 (** val match_program_rect_Type5 :
1406     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1407     'a1) -> 'a1 **)
1408 let rec match_program_rect_Type5 m p1 p2 h_mk_match_program =
1409   h_mk_match_program __ __ __
1410
1411 (** val match_program_rect_Type3 :
1412     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1413     'a1) -> 'a1 **)
1414 let rec match_program_rect_Type3 m p1 p2 h_mk_match_program =
1415   h_mk_match_program __ __ __
1416
1417 (** val match_program_rect_Type2 :
1418     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1419     'a1) -> 'a1 **)
1420 let rec match_program_rect_Type2 m p1 p2 h_mk_match_program =
1421   h_mk_match_program __ __ __
1422
1423 (** val match_program_rect_Type1 :
1424     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1425     'a1) -> 'a1 **)
1426 let rec match_program_rect_Type1 m p1 p2 h_mk_match_program =
1427   h_mk_match_program __ __ __
1428
1429 (** val match_program_rect_Type0 :
1430     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1431     'a1) -> 'a1 **)
1432 let rec match_program_rect_Type0 m p1 p2 h_mk_match_program =
1433   h_mk_match_program __ __ __
1434
1435 (** val match_program_inv_rect_Type4 :
1436     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1437     -> 'a1) -> 'a1 **)
1438 let match_program_inv_rect_Type4 x1 x2 x3 h1 =
1439   let hcut = match_program_rect_Type4 x1 x2 x3 h1 in hcut __
1440
1441 (** val match_program_inv_rect_Type3 :
1442     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1443     -> 'a1) -> 'a1 **)
1444 let match_program_inv_rect_Type3 x1 x2 x3 h1 =
1445   let hcut = match_program_rect_Type3 x1 x2 x3 h1 in hcut __
1446
1447 (** val match_program_inv_rect_Type2 :
1448     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1449     -> 'a1) -> 'a1 **)
1450 let match_program_inv_rect_Type2 x1 x2 x3 h1 =
1451   let hcut = match_program_rect_Type2 x1 x2 x3 h1 in hcut __
1452
1453 (** val match_program_inv_rect_Type1 :
1454     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1455     -> 'a1) -> 'a1 **)
1456 let match_program_inv_rect_Type1 x1 x2 x3 h1 =
1457   let hcut = match_program_rect_Type1 x1 x2 x3 h1 in hcut __
1458
1459 (** val match_program_inv_rect_Type0 :
1460     matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1461     -> 'a1) -> 'a1 **)
1462 let match_program_inv_rect_Type0 x1 x2 x3 h1 =
1463   let hcut = match_program_rect_Type0 x1 x2 x3 h1 in hcut __
1464
1465 (** val match_program_discr :
1466     matching -> (__, __) program -> (__, __) program -> __ **)
1467 let match_program_discr a1 a2 a3 =
1468   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1469
1470 (** val match_program_jmdiscr :
1471     matching -> (__, __) program -> (__, __) program -> __ **)
1472 let match_program_jmdiscr a1 a2 a3 =
1473   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1474
1475 type external_function = { ef_id : ident; ef_sig : signature }
1476
1477 (** val external_function_rect_Type4 :
1478     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1479 let rec external_function_rect_Type4 h_mk_external_function x_4131 =
1480   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4131 in
1481   h_mk_external_function ef_id0 ef_sig0
1482
1483 (** val external_function_rect_Type5 :
1484     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1485 let rec external_function_rect_Type5 h_mk_external_function x_4133 =
1486   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4133 in
1487   h_mk_external_function ef_id0 ef_sig0
1488
1489 (** val external_function_rect_Type3 :
1490     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1491 let rec external_function_rect_Type3 h_mk_external_function x_4135 =
1492   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4135 in
1493   h_mk_external_function ef_id0 ef_sig0
1494
1495 (** val external_function_rect_Type2 :
1496     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1497 let rec external_function_rect_Type2 h_mk_external_function x_4137 =
1498   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4137 in
1499   h_mk_external_function ef_id0 ef_sig0
1500
1501 (** val external_function_rect_Type1 :
1502     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1503 let rec external_function_rect_Type1 h_mk_external_function x_4139 =
1504   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4139 in
1505   h_mk_external_function ef_id0 ef_sig0
1506
1507 (** val external_function_rect_Type0 :
1508     (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1509 let rec external_function_rect_Type0 h_mk_external_function x_4141 =
1510   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4141 in
1511   h_mk_external_function ef_id0 ef_sig0
1512
1513 (** val ef_id : external_function -> ident **)
1514 let rec ef_id xxx =
1515   xxx.ef_id
1516
1517 (** val ef_sig : external_function -> signature **)
1518 let rec ef_sig xxx =
1519   xxx.ef_sig
1520
1521 (** val external_function_inv_rect_Type4 :
1522     external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1523 let external_function_inv_rect_Type4 hterm h1 =
1524   let hcut = external_function_rect_Type4 h1 hterm in hcut __
1525
1526 (** val external_function_inv_rect_Type3 :
1527     external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1528 let external_function_inv_rect_Type3 hterm h1 =
1529   let hcut = external_function_rect_Type3 h1 hterm in hcut __
1530
1531 (** val external_function_inv_rect_Type2 :
1532     external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1533 let external_function_inv_rect_Type2 hterm h1 =
1534   let hcut = external_function_rect_Type2 h1 hterm in hcut __
1535
1536 (** val external_function_inv_rect_Type1 :
1537     external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1538 let external_function_inv_rect_Type1 hterm h1 =
1539   let hcut = external_function_rect_Type1 h1 hterm in hcut __
1540
1541 (** val external_function_inv_rect_Type0 :
1542     external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1543 let external_function_inv_rect_Type0 hterm h1 =
1544   let hcut = external_function_rect_Type0 h1 hterm in hcut __
1545
1546 (** val external_function_discr :
1547     external_function -> external_function -> __ **)
1548 let external_function_discr x y =
1549   Logic.eq_rect_Type2 x
1550     (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1551     y
1552
1553 (** val external_function_jmdiscr :
1554     external_function -> external_function -> __ **)
1555 let external_function_jmdiscr x y =
1556   Logic.eq_rect_Type2 x
1557     (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1558     y
1559
1560 type externalFunction = external_function
1561
1562 (** val external_function_tag : external_function -> ident **)
1563 let external_function_tag =
1564   ef_id
1565
1566 (** val external_function_sig : external_function -> signature **)
1567 let external_function_sig =
1568   ef_sig
1569
1570 type 'f fundef =
1571 | Internal of 'f
1572 | External of external_function
1573
1574 (** val fundef_rect_Type4 :
1575     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1576 let rec fundef_rect_Type4 h_Internal h_External = function
1577 | Internal x_4161 -> h_Internal x_4161
1578 | External x_4162 -> h_External x_4162
1579
1580 (** val fundef_rect_Type5 :
1581     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1582 let rec fundef_rect_Type5 h_Internal h_External = function
1583 | Internal x_4166 -> h_Internal x_4166
1584 | External x_4167 -> h_External x_4167
1585
1586 (** val fundef_rect_Type3 :
1587     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1588 let rec fundef_rect_Type3 h_Internal h_External = function
1589 | Internal x_4171 -> h_Internal x_4171
1590 | External x_4172 -> h_External x_4172
1591
1592 (** val fundef_rect_Type2 :
1593     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1594 let rec fundef_rect_Type2 h_Internal h_External = function
1595 | Internal x_4176 -> h_Internal x_4176
1596 | External x_4177 -> h_External x_4177
1597
1598 (** val fundef_rect_Type1 :
1599     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1600 let rec fundef_rect_Type1 h_Internal h_External = function
1601 | Internal x_4181 -> h_Internal x_4181
1602 | External x_4182 -> h_External x_4182
1603
1604 (** val fundef_rect_Type0 :
1605     ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1606 let rec fundef_rect_Type0 h_Internal h_External = function
1607 | Internal x_4186 -> h_Internal x_4186
1608 | External x_4187 -> h_External x_4187
1609
1610 (** val fundef_inv_rect_Type4 :
1611     'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1612     'a2 **)
1613 let fundef_inv_rect_Type4 hterm h1 h2 =
1614   let hcut = fundef_rect_Type4 h1 h2 hterm in hcut __
1615
1616 (** val fundef_inv_rect_Type3 :
1617     'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1618     'a2 **)
1619 let fundef_inv_rect_Type3 hterm h1 h2 =
1620   let hcut = fundef_rect_Type3 h1 h2 hterm in hcut __
1621
1622 (** val fundef_inv_rect_Type2 :
1623     'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1624     'a2 **)
1625 let fundef_inv_rect_Type2 hterm h1 h2 =
1626   let hcut = fundef_rect_Type2 h1 h2 hterm in hcut __
1627
1628 (** val fundef_inv_rect_Type1 :
1629     'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1630     'a2 **)
1631 let fundef_inv_rect_Type1 hterm h1 h2 =
1632   let hcut = fundef_rect_Type1 h1 h2 hterm in hcut __
1633
1634 (** val fundef_inv_rect_Type0 :
1635     'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1636     'a2 **)
1637 let fundef_inv_rect_Type0 hterm h1 h2 =
1638   let hcut = fundef_rect_Type0 h1 h2 hterm in hcut __
1639
1640 (** val fundef_discr : 'a1 fundef -> 'a1 fundef -> __ **)
1641 let fundef_discr x y =
1642   Logic.eq_rect_Type2 x
1643     (match x with
1644      | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1645      | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1646
1647 (** val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __ **)
1648 let fundef_jmdiscr x y =
1649   Logic.eq_rect_Type2 x
1650     (match x with
1651      | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1652      | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1653
1654 (** val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef **)
1655 let transf_fundef transf = function
1656 | Internal f -> Internal (transf f)
1657 | External ef -> External ef
1658
1659 (** val transf_partial_fundef :
1660     ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res **)
1661 let transf_partial_fundef transf_partial = function
1662 | Internal f ->
1663   Obj.magic
1664     (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic transf_partial f)
1665       (fun f' -> Obj.magic (Errors.OK (Internal f'))))
1666 | External ef -> Errors.OK (External ef)
1667