open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

type ident = PreIdentifiers.identifier

(** val ident_eq : ident -> ident -> (__, __) Types.sum **)
let ident_eq =
  Identifiers.identifier_eq PreIdentifiers.SymbolTag

(** val ident_of_nat : Nat.nat -> ident **)
let ident_of_nat =
  Identifiers.identifier_of_nat PreIdentifiers.SymbolTag

type region =
| XData
| Code

(** val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type4 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type5 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type3 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type2 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type1 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1 **)
let rec region_rect_Type0 h_XData h_Code = function
| XData -> h_XData
| Code -> h_Code

(** val region_inv_rect_Type4 :
    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let region_inv_rect_Type4 hterm h1 h2 =
  let hcut = region_rect_Type4 h1 h2 hterm in hcut __

(** val region_inv_rect_Type3 :
    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let region_inv_rect_Type3 hterm h1 h2 =
  let hcut = region_rect_Type3 h1 h2 hterm in hcut __

(** val region_inv_rect_Type2 :
    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let region_inv_rect_Type2 hterm h1 h2 =
  let hcut = region_rect_Type2 h1 h2 hterm in hcut __

(** val region_inv_rect_Type1 :
    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let region_inv_rect_Type1 hterm h1 h2 =
  let hcut = region_rect_Type1 h1 h2 hterm in hcut __

(** val region_inv_rect_Type0 :
    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let region_inv_rect_Type0 hterm h1 h2 =
  let hcut = region_rect_Type0 h1 h2 hterm in hcut __

(** val region_discr : region -> region -> __ **)
let region_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | XData -> Obj.magic (fun _ dH -> dH)
     | Code -> Obj.magic (fun _ dH -> dH)) y

(** val region_jmdiscr : region -> region -> __ **)
let region_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | XData -> Obj.magic (fun _ dH -> dH)
     | Code -> Obj.magic (fun _ dH -> dH)) y

(** val eq_region : region -> region -> Bool.bool **)
let eq_region r1 r2 =
  match r1 with
  | XData ->
    (match r2 with
     | XData -> Bool.True
     | Code -> Bool.False)
  | Code ->
    (match r2 with
     | XData -> Bool.False
     | Code -> Bool.True)

(** val eq_region_elim :
    region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eq_region_elim r1 r2 =
  match r1 with
  | XData ->
    (match r2 with
     | XData -> (fun ptrue pfalse -> ptrue __)
     | Code -> (fun ptrue pfalse -> pfalse __))
  | Code ->
    (match r2 with
     | XData -> (fun ptrue pfalse -> pfalse __)
     | Code -> (fun ptrue pfalse -> ptrue __))

(** val eq_region_dec : region -> region -> (__, __) Types.sum **)
let eq_region_dec r1 r2 =
  eq_region_elim r1 r2 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)

(** val size_pointer : Nat.nat **)
let size_pointer =
  Nat.S (Nat.S Nat.O)

type signedness =
| Signed
| Unsigned

(** val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type4 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type5 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type3 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type2 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type1 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1 **)
let rec signedness_rect_Type0 h_Signed h_Unsigned = function
| Signed -> h_Signed
| Unsigned -> h_Unsigned

(** val signedness_inv_rect_Type4 :
    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let signedness_inv_rect_Type4 hterm h1 h2 =
  let hcut = signedness_rect_Type4 h1 h2 hterm in hcut __

(** val signedness_inv_rect_Type3 :
    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let signedness_inv_rect_Type3 hterm h1 h2 =
  let hcut = signedness_rect_Type3 h1 h2 hterm in hcut __

(** val signedness_inv_rect_Type2 :
    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let signedness_inv_rect_Type2 hterm h1 h2 =
  let hcut = signedness_rect_Type2 h1 h2 hterm in hcut __

(** val signedness_inv_rect_Type1 :
    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let signedness_inv_rect_Type1 hterm h1 h2 =
  let hcut = signedness_rect_Type1 h1 h2 hterm in hcut __

(** val signedness_inv_rect_Type0 :
    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let signedness_inv_rect_Type0 hterm h1 h2 =
  let hcut = signedness_rect_Type0 h1 h2 hterm in hcut __

(** val signedness_discr : signedness -> signedness -> __ **)
let signedness_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Signed -> Obj.magic (fun _ dH -> dH)
     | Unsigned -> Obj.magic (fun _ dH -> dH)) y

(** val signedness_jmdiscr : signedness -> signedness -> __ **)
let signedness_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Signed -> Obj.magic (fun _ dH -> dH)
     | Unsigned -> Obj.magic (fun _ dH -> dH)) y

type intsize =
| I8
| I16
| I32

(** val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type4 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type5 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type3 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type2 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type1 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
let rec intsize_rect_Type0 h_I8 h_I16 h_I32 = function
| I8 -> h_I8
| I16 -> h_I16
| I32 -> h_I32

(** val intsize_inv_rect_Type4 :
    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let intsize_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = intsize_rect_Type4 h1 h2 h3 hterm in hcut __

(** val intsize_inv_rect_Type3 :
    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let intsize_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = intsize_rect_Type3 h1 h2 h3 hterm in hcut __

(** val intsize_inv_rect_Type2 :
    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let intsize_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = intsize_rect_Type2 h1 h2 h3 hterm in hcut __

(** val intsize_inv_rect_Type1 :
    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let intsize_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = intsize_rect_Type1 h1 h2 h3 hterm in hcut __

(** val intsize_inv_rect_Type0 :
    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let intsize_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = intsize_rect_Type0 h1 h2 h3 hterm in hcut __

(** val intsize_discr : intsize -> intsize -> __ **)
let intsize_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | I8 -> Obj.magic (fun _ dH -> dH)
     | I16 -> Obj.magic (fun _ dH -> dH)
     | I32 -> Obj.magic (fun _ dH -> dH)) y

(** val intsize_jmdiscr : intsize -> intsize -> __ **)
let intsize_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | I8 -> Obj.magic (fun _ dH -> dH)
     | I16 -> Obj.magic (fun _ dH -> dH)
     | I32 -> Obj.magic (fun _ dH -> dH)) y

type floatsize =
| F32
| F64

(** val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type4 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type5 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type3 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type2 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type1 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
let rec floatsize_rect_Type0 h_F32 h_F64 = function
| F32 -> h_F32
| F64 -> h_F64

(** val floatsize_inv_rect_Type4 :
    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let floatsize_inv_rect_Type4 hterm h1 h2 =
  let hcut = floatsize_rect_Type4 h1 h2 hterm in hcut __

(** val floatsize_inv_rect_Type3 :
    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let floatsize_inv_rect_Type3 hterm h1 h2 =
  let hcut = floatsize_rect_Type3 h1 h2 hterm in hcut __

(** val floatsize_inv_rect_Type2 :
    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let floatsize_inv_rect_Type2 hterm h1 h2 =
  let hcut = floatsize_rect_Type2 h1 h2 hterm in hcut __

(** val floatsize_inv_rect_Type1 :
    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let floatsize_inv_rect_Type1 hterm h1 h2 =
  let hcut = floatsize_rect_Type1 h1 h2 hterm in hcut __

(** val floatsize_inv_rect_Type0 :
    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let floatsize_inv_rect_Type0 hterm h1 h2 =
  let hcut = floatsize_rect_Type0 h1 h2 hterm in hcut __

(** val floatsize_discr : floatsize -> floatsize -> __ **)
let floatsize_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | F32 -> Obj.magic (fun _ dH -> dH)
     | F64 -> Obj.magic (fun _ dH -> dH)) y

(** val floatsize_jmdiscr : floatsize -> floatsize -> __ **)
let floatsize_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | F32 -> Obj.magic (fun _ dH -> dH)
     | F64 -> Obj.magic (fun _ dH -> dH)) y

type typ =
| ASTint of intsize * signedness
| ASTptr

(** val typ_rect_Type4 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type4 h_ASTint h_ASTptr = function
| ASTint (x_3662, x_3661) -> h_ASTint x_3662 x_3661
| ASTptr -> h_ASTptr

(** val typ_rect_Type5 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type5 h_ASTint h_ASTptr = function
| ASTint (x_3667, x_3666) -> h_ASTint x_3667 x_3666
| ASTptr -> h_ASTptr

(** val typ_rect_Type3 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type3 h_ASTint h_ASTptr = function
| ASTint (x_3672, x_3671) -> h_ASTint x_3672 x_3671
| ASTptr -> h_ASTptr

(** val typ_rect_Type2 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type2 h_ASTint h_ASTptr = function
| ASTint (x_3677, x_3676) -> h_ASTint x_3677 x_3676
| ASTptr -> h_ASTptr

(** val typ_rect_Type1 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type1 h_ASTint h_ASTptr = function
| ASTint (x_3682, x_3681) -> h_ASTint x_3682 x_3681
| ASTptr -> h_ASTptr

(** val typ_rect_Type0 :
    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
let rec typ_rect_Type0 h_ASTint h_ASTptr = function
| ASTint (x_3687, x_3686) -> h_ASTint x_3687 x_3686
| ASTptr -> h_ASTptr

(** val typ_inv_rect_Type4 :
    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let typ_inv_rect_Type4 hterm h1 h2 =
  let hcut = typ_rect_Type4 h1 h2 hterm in hcut __

(** val typ_inv_rect_Type3 :
    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let typ_inv_rect_Type3 hterm h1 h2 =
  let hcut = typ_rect_Type3 h1 h2 hterm in hcut __

(** val typ_inv_rect_Type2 :
    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let typ_inv_rect_Type2 hterm h1 h2 =
  let hcut = typ_rect_Type2 h1 h2 hterm in hcut __

(** val typ_inv_rect_Type1 :
    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let typ_inv_rect_Type1 hterm h1 h2 =
  let hcut = typ_rect_Type1 h1 h2 hterm in hcut __

(** val typ_inv_rect_Type0 :
    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let typ_inv_rect_Type0 hterm h1 h2 =
  let hcut = typ_rect_Type0 h1 h2 hterm in hcut __

(** val typ_discr : typ -> typ -> __ **)
let typ_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | ASTptr -> Obj.magic (fun _ dH -> dH)) y

(** val typ_jmdiscr : typ -> typ -> __ **)
let typ_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | ASTptr -> Obj.magic (fun _ dH -> dH)) y

type sigType = typ

(** val sigType_Int : typ **)
let sigType_Int =
  ASTint (I32, Unsigned)

(** val sigType_Ptr : typ **)
let sigType_Ptr =
  ASTptr

(** val pred_size_intsize : intsize -> Nat.nat **)
let pred_size_intsize = function
| I8 -> Nat.O
| I16 -> Nat.S Nat.O
| I32 -> Nat.S (Nat.S (Nat.S Nat.O))

(** val size_intsize : intsize -> Nat.nat **)
let size_intsize sz =
  Nat.S (pred_size_intsize sz)

(** val bitsize_of_intsize : intsize -> Nat.nat **)
let bitsize_of_intsize sz =
  Nat.times (size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S Nat.O))))))))

(** val eq_intsize : intsize -> intsize -> Bool.bool **)
let eq_intsize sz1 sz2 =
  match sz1 with
  | I8 ->
    (match sz2 with
     | I8 -> Bool.True
     | I16 -> Bool.False
     | I32 -> Bool.False)
  | I16 ->
    (match sz2 with
     | I8 -> Bool.False
     | I16 -> Bool.True
     | I32 -> Bool.False)
  | I32 ->
    (match sz2 with
     | I8 -> Bool.False
     | I16 -> Bool.False
     | I32 -> Bool.True)

(** val eq_intsize_elim :
    intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let eq_intsize_elim clearme sz2 x x0 =
  (match clearme with
   | I8 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ hne heq -> heq __)
       | I16 -> (fun _ hne heq -> hne __)
       | I32 -> (fun _ hne heq -> hne __))
   | I16 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ hne heq -> hne __)
       | I16 -> (fun _ hne heq -> heq __)
       | I32 -> (fun _ hne heq -> hne __))
   | I32 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ hne heq -> hne __)
       | I16 -> (fun _ hne heq -> hne __)
       | I32 -> (fun _ hne heq -> heq __))) sz2 __ x x0

(** val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
let signedness_check sg1 sg2 =
  match sg1 with
  | Signed ->
    (fun x ->
      match sg2 with
      | Signed -> (fun d -> x)
      | Unsigned -> (fun d -> d))
  | Unsigned ->
    (fun x ->
      match sg2 with
      | Signed -> (fun d -> d)
      | Unsigned -> (fun d -> x))

(** val inttyp_eq_elim' :
    intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
let rec inttyp_eq_elim' sz1 sz2 sg1 sg2 =
  match sz1 with
  | I8 ->
    (fun x ->
      match sz2 with
      | I8 -> signedness_check sg1 sg2 x
      | I16 -> (fun d -> d)
      | I32 -> (fun d -> d))
  | I16 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun d -> d)
      | I16 -> signedness_check sg1 sg2 x
      | I32 -> (fun d -> d))
  | I32 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun d -> d)
      | I16 -> (fun d -> d)
      | I32 -> signedness_check sg1 sg2 x)

(** val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1 **)
let rec intsize_eq_elim' sz1 sz2 =
  match sz1 with
  | I8 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun d -> x)
      | I16 -> (fun d -> d)
      | I32 -> (fun d -> d))
  | I16 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun d -> d)
      | I16 -> (fun d -> x)
      | I32 -> (fun d -> d))
  | I32 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun d -> d)
      | I16 -> (fun d -> d)
      | I32 -> (fun d -> x))

(** val intsize_eq_elim :
    intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1 **)
let rec intsize_eq_elim sz1 sz2 =
  match sz1 with
  | I8 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun f d -> f x)
      | I16 -> (fun f d -> d)
      | I32 -> (fun f d -> d))
  | I16 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun f d -> d)
      | I16 -> (fun f d -> f x)
      | I32 -> (fun f d -> d))
  | I32 ->
    (fun x ->
      match sz2 with
      | I8 -> (fun f d -> d)
      | I16 -> (fun f d -> d)
      | I32 -> (fun f d -> f x))

(** val intsize_eq_elim_elim :
    intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
    __) -> 'a3 **)
let intsize_eq_elim_elim clearme sz2 p f d x x0 =
  (match clearme with
   | I8 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
       | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
       | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
   | I16 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
       | I16 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
       | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
   | I32 ->
     (fun clearme0 ->
       match clearme0 with
       | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
       | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
       | I32 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __))) sz2 __ p f d
    __ x x0

type bvint = BitVector.bitVector

(** val repr : intsize -> Nat.nat -> bvint **)
let repr sz x =
  Arithmetic.bitvector_of_nat (bitsize_of_intsize sz) x

(** val size_floatsize : floatsize -> Nat.nat **)
let size_floatsize sz =
  Nat.S
    (match sz with
     | F32 -> Nat.S (Nat.S (Nat.S Nat.O))
     | F64 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))

(** val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1 **)
let rec floatsize_eq_elim sz1 sz2 =
  match sz1 with
  | F32 ->
    (fun x ->
      match sz2 with
      | F32 -> (fun d -> x)
      | F64 -> (fun d -> d))
  | F64 ->
    (fun x ->
      match sz2 with
      | F32 -> (fun d -> d)
      | F64 -> (fun d -> x))

(** val typesize : typ -> Nat.nat **)
let typesize = function
| ASTint (sz, x) -> size_intsize sz
| ASTptr -> size_pointer

(** val typ_eq : typ -> typ -> (__, __) Types.sum **)
let typ_eq = function
| ASTint (clearme0, x) ->
  (match clearme0 with
   | I8 ->
     (fun clearme1 ->
       match clearme1 with
       | Signed ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inl __
                  | Unsigned -> Types.Inr __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)) x0
           | ASTptr -> Types.Inr __)
       | Unsigned ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inl __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)) x0
           | ASTptr -> Types.Inr __))
   | I16 ->
     (fun clearme1 ->
       match clearme1 with
       | Signed ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inl __
                  | Unsigned -> Types.Inr __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)) x0
           | ASTptr -> Types.Inr __)
       | Unsigned ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inl __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)) x0
           | ASTptr -> Types.Inr __))
   | I32 ->
     (fun clearme1 ->
       match clearme1 with
       | Signed ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inl __
                  | Unsigned -> Types.Inr __)) x0
           | ASTptr -> Types.Inr __)
       | Unsigned ->
         (fun clearme2 ->
           match clearme2 with
           | ASTint (clearme3, x0) ->
             (match clearme3 with
              | I8 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I16 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inr __)
              | I32 ->
                (fun clearme4 ->
                  match clearme4 with
                  | Signed -> Types.Inr __
                  | Unsigned -> Types.Inl __)) x0
           | ASTptr -> Types.Inr __))) x
| ASTptr ->
  (fun clearme0 ->
    match clearme0 with
    | ASTint (clearme1, x) ->
      (match clearme1 with
       | I8 ->
         (fun clearme2 ->
           match clearme2 with
           | Signed -> Types.Inr __
           | Unsigned -> Types.Inr __)
       | I16 ->
         (fun clearme2 ->
           match clearme2 with
           | Signed -> Types.Inr __
           | Unsigned -> Types.Inr __)
       | I32 ->
         (fun clearme2 ->
           match clearme2 with
           | Signed -> Types.Inr __
           | Unsigned -> Types.Inr __)) x
    | ASTptr -> Types.Inl __)

(** val opt_typ_eq :
    typ Types.option -> typ Types.option -> (__, __) Types.sum **)
let opt_typ_eq t1 t2 =
  match t1 with
  | Types.None ->
    (match t2 with
     | Types.None -> Types.Inl __
     | Types.Some ty -> Types.Inr __)
  | Types.Some x ->
    (match t2 with
     | Types.None -> (fun ty -> Types.Inr __)
     | Types.Some ty1 ->
       (fun ty2 ->
         Types.sum_rect_Type0 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
           (typ_eq ty1 ty2))) x

type signature = { sig_args : typ List.list; sig_res : typ Types.option }

(** val signature_rect_Type4 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type4 h_mk_signature x_3722 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3722 in
  h_mk_signature sig_args0 sig_res0

(** val signature_rect_Type5 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type5 h_mk_signature x_3724 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3724 in
  h_mk_signature sig_args0 sig_res0

(** val signature_rect_Type3 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type3 h_mk_signature x_3726 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3726 in
  h_mk_signature sig_args0 sig_res0

(** val signature_rect_Type2 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type2 h_mk_signature x_3728 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3728 in
  h_mk_signature sig_args0 sig_res0

(** val signature_rect_Type1 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type1 h_mk_signature x_3730 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3730 in
  h_mk_signature sig_args0 sig_res0

(** val signature_rect_Type0 :
    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
let rec signature_rect_Type0 h_mk_signature x_3732 =
  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3732 in
  h_mk_signature sig_args0 sig_res0

(** val sig_args : signature -> typ List.list **)
let rec sig_args xxx =
  xxx.sig_args

(** val sig_res : signature -> typ Types.option **)
let rec sig_res xxx =
  xxx.sig_res

(** val signature_inv_rect_Type4 :
    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
let signature_inv_rect_Type4 hterm h1 =
  let hcut = signature_rect_Type4 h1 hterm in hcut __

(** val signature_inv_rect_Type3 :
    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
let signature_inv_rect_Type3 hterm h1 =
  let hcut = signature_rect_Type3 h1 hterm in hcut __

(** val signature_inv_rect_Type2 :
    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
let signature_inv_rect_Type2 hterm h1 =
  let hcut = signature_rect_Type2 h1 hterm in hcut __

(** val signature_inv_rect_Type1 :
    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
let signature_inv_rect_Type1 hterm h1 =
  let hcut = signature_rect_Type1 h1 hterm in hcut __

(** val signature_inv_rect_Type0 :
    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
let signature_inv_rect_Type0 hterm h1 =
  let hcut = signature_rect_Type0 h1 hterm in hcut __

(** val signature_discr : signature -> signature -> __ **)
let signature_discr x y =
  Logic.eq_rect_Type2 x
    (let { sig_args = a0; sig_res = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val signature_jmdiscr : signature -> signature -> __ **)
let signature_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { sig_args = a0; sig_res = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

type signature0 = signature

(** val signature_args : signature -> typ List.list **)
let signature_args =
  sig_args

(** val signature_return : signature -> typ Types.option **)
let signature_return =
  sig_res

(** val proj_sig_res : signature -> typ **)
let proj_sig_res s =
  match s.sig_res with
  | Types.None -> ASTint (I32, Unsigned)
  | Types.Some t -> t

type init_data =
| Init_int8 of bvint
| Init_int16 of bvint
| Init_int32 of bvint
| Init_space of Nat.nat
| Init_null
| Init_addrof of ident * Nat.nat

(** val init_data_rect_Type4 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3760 -> h_Init_int8 x_3760
| Init_int16 x_3761 -> h_Init_int16 x_3761
| Init_int32 x_3762 -> h_Init_int32 x_3762
| Init_space x_3763 -> h_Init_space x_3763
| Init_null -> h_Init_null
| Init_addrof (x_3765, x_3764) -> h_Init_addrof x_3765 x_3764

(** val init_data_rect_Type5 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3773 -> h_Init_int8 x_3773
| Init_int16 x_3774 -> h_Init_int16 x_3774
| Init_int32 x_3775 -> h_Init_int32 x_3775
| Init_space x_3776 -> h_Init_space x_3776
| Init_null -> h_Init_null
| Init_addrof (x_3778, x_3777) -> h_Init_addrof x_3778 x_3777

(** val init_data_rect_Type3 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3786 -> h_Init_int8 x_3786
| Init_int16 x_3787 -> h_Init_int16 x_3787
| Init_int32 x_3788 -> h_Init_int32 x_3788
| Init_space x_3789 -> h_Init_space x_3789
| Init_null -> h_Init_null
| Init_addrof (x_3791, x_3790) -> h_Init_addrof x_3791 x_3790

(** val init_data_rect_Type2 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3799 -> h_Init_int8 x_3799
| Init_int16 x_3800 -> h_Init_int16 x_3800
| Init_int32 x_3801 -> h_Init_int32 x_3801
| Init_space x_3802 -> h_Init_space x_3802
| Init_null -> h_Init_null
| Init_addrof (x_3804, x_3803) -> h_Init_addrof x_3804 x_3803

(** val init_data_rect_Type1 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3812 -> h_Init_int8 x_3812
| Init_int16 x_3813 -> h_Init_int16 x_3813
| Init_int32 x_3814 -> h_Init_int32 x_3814
| Init_space x_3815 -> h_Init_space x_3815
| Init_null -> h_Init_null
| Init_addrof (x_3817, x_3816) -> h_Init_addrof x_3817 x_3816

(** val init_data_rect_Type0 :
    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
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
| Init_int8 x_3825 -> h_Init_int8 x_3825
| Init_int16 x_3826 -> h_Init_int16 x_3826
| Init_int32 x_3827 -> h_Init_int32 x_3827
| Init_space x_3828 -> h_Init_space x_3828
| Init_null -> h_Init_null
| Init_addrof (x_3830, x_3829) -> h_Init_addrof x_3830 x_3829

(** val init_data_inv_rect_Type4 :
    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
    __ -> 'a1) -> 'a1 **)
let init_data_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = init_data_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val init_data_inv_rect_Type3 :
    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
    __ -> 'a1) -> 'a1 **)
let init_data_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = init_data_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val init_data_inv_rect_Type2 :
    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
    __ -> 'a1) -> 'a1 **)
let init_data_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = init_data_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val init_data_inv_rect_Type1 :
    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
    __ -> 'a1) -> 'a1 **)
let init_data_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = init_data_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val init_data_inv_rect_Type0 :
    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat ->
    __ -> 'a1) -> 'a1 **)
let init_data_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = init_data_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val init_data_discr : init_data -> init_data -> __ **)
let init_data_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_null -> Obj.magic (fun _ dH -> dH)
     | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val init_data_jmdiscr : init_data -> init_data -> __ **)
let init_data_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
     | Init_null -> Obj.magic (fun _ dH -> dH)
     | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
                                      Types.prod List.list;
                          prog_funct : (ident, 'f) Types.prod List.list;
                          prog_main : ident }

(** val program_rect_Type4 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type4 h_mk_program x_3917 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3917
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val program_rect_Type5 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type5 h_mk_program x_3919 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3919
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val program_rect_Type3 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type3 h_mk_program x_3921 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3921
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val program_rect_Type2 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type2 h_mk_program x_3923 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3923
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val program_rect_Type1 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type1 h_mk_program x_3925 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3925
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val program_rect_Type0 :
    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
let rec program_rect_Type0 h_mk_program x_3927 =
  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    prog_main0 } = x_3927
  in
  h_mk_program prog_vars0 prog_funct0 prog_main0

(** val prog_vars :
    ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
    List.list **)
let rec prog_vars xxx =
  xxx.prog_vars

(** val prog_funct :
    ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list **)
let rec prog_funct xxx =
  xxx.prog_funct

(** val prog_main : ('a1, 'a2) program -> ident **)
let rec prog_main xxx =
  xxx.prog_main

(** val program_inv_rect_Type4 :
    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
    'a3 **)
let program_inv_rect_Type4 hterm h1 =
  let hcut = program_rect_Type4 h1 hterm in hcut __

(** val program_inv_rect_Type3 :
    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
    'a3 **)
let program_inv_rect_Type3 hterm h1 =
  let hcut = program_rect_Type3 h1 hterm in hcut __

(** val program_inv_rect_Type2 :
    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
    'a3 **)
let program_inv_rect_Type2 hterm h1 =
  let hcut = program_rect_Type2 h1 hterm in hcut __

(** val program_inv_rect_Type1 :
    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
    'a3 **)
let program_inv_rect_Type1 hterm h1 =
  let hcut = program_rect_Type1 h1 hterm in hcut __

(** val program_inv_rect_Type0 :
    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
    'a3 **)
let program_inv_rect_Type0 hterm h1 =
  let hcut = program_rect_Type0 h1 hterm in hcut __

(** val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
let program_discr x y =
  Logic.eq_rect_Type2 x
    (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
let program_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val prog_funct_names : ('a1, 'a2) program -> ident List.list **)
let prog_funct_names p =
  List.map Types.fst p.prog_funct

(** val prog_var_names : ('a1, 'a2) program -> ident List.list **)
let prog_var_names p =
  List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars

(** val transf_program :
    ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
    Types.prod List.list **)
let transf_program transf l =
  List.map (fun id_fn -> { Types.fst = id_fn.Types.fst; Types.snd =
    (transf id_fn.Types.snd) }) l

(** val transform_program :
    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3)
    program **)
let transform_program p transf =
  { prog_vars = p.prog_vars; prog_funct =
    (transf_program
      (transf (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
      p.prog_funct); prog_main = p.prog_main }

(** val transf_program_gen :
    PreIdentifiers.identifierTag -> Identifiers.universe ->
    (Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe) Types.prod)
    -> (ident, 'a1) Types.prod List.list -> ((ident, 'a2) Types.prod
    List.list, Identifiers.universe) Types.prod **)
let transf_program_gen tag gen transf l =
  List.foldr (fun id_fn bs_gen ->
    let { Types.fst = fn'; Types.snd = gen' } =
      transf bs_gen.Types.snd id_fn.Types.snd
    in
    { Types.fst = (List.Cons ({ Types.fst = id_fn.Types.fst; Types.snd =
    fn' }, bs_gen.Types.fst)); Types.snd = gen' }) { Types.fst = List.Nil;
    Types.snd = gen } l

(** val transform_program_gen :
    PreIdentifiers.identifierTag -> Identifiers.universe -> ('a1, 'a3)
    program -> (ident List.list -> Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> (('a2, 'a3) program,
    Identifiers.universe) Types.prod **)
let transform_program_gen tag gen p trans =
  let fsg =
    transf_program_gen tag gen
      (trans (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
      p.prog_funct
  in
  { Types.fst = { prog_vars = p.prog_vars; prog_funct = fsg.Types.fst;
  prog_main = p.prog_main }; Types.snd = fsg.Types.snd }

(** val map_partial :
    ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
    Types.prod List.list Errors.res **)
let map_partial f =
  Obj.magic
    (Monad.m_list_map (Monad.max_def Errors.res0) (fun ab ->
      let { Types.fst = a; Types.snd = b } = ab in
      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f b) (fun c ->
        Obj.magic (Errors.OK { Types.fst = a; Types.snd = c }))))

(** val transform_partial_program :
    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
    'a3) program Errors.res **)
let transform_partial_program p transf_partial =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (map_partial
          (transf_partial
            (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
          p.prog_funct)) (fun fl ->
      Obj.magic (Errors.OK { prog_vars = p.prog_vars; prog_funct = fl;
        prog_main = p.prog_main })))

(** val transform_partial_program2 :
    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3
    -> 'a4 Errors.res) -> ('a2, 'a4) program Errors.res **)
let transform_partial_program2 p transf_partial_function transf_partial_variable =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (map_partial
          (transf_partial_function
            (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
          p.prog_funct)) (fun fl ->
      (match map_partial transf_partial_variable p.prog_vars with
       | Errors.OK vl ->
         (fun _ ->
           Obj.magic (Errors.OK { prog_vars = vl; prog_funct =
             (Logic.eq_rect_Type0
               (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars) fl
               (List.map (fun x -> x.Types.fst.Types.fst) vl)); prog_main =
             p.prog_main }))
       | Errors.Error err -> (fun _ -> Obj.magic (Errors.Error err))) __))

type matching =
| Mk_matching

(** val matching_rect_Type4 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type4 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

(** val matching_rect_Type5 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type5 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

(** val matching_rect_Type3 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type3 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

(** val matching_rect_Type2 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type2 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

(** val matching_rect_Type1 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type1 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

(** val matching_rect_Type0 :
    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
let rec matching_rect_Type0 h_mk_matching = function
| Mk_matching -> h_mk_matching __ __ __ __ __ __

type m_A = __

type m_B = __

type m_V = __

type m_W = __

(** val matching_inv_rect_Type4 :
    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let matching_inv_rect_Type4 hterm h1 =
  let hcut = matching_rect_Type4 h1 hterm in hcut __

(** val matching_inv_rect_Type3 :
    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let matching_inv_rect_Type3 hterm h1 =
  let hcut = matching_rect_Type3 h1 hterm in hcut __

(** val matching_inv_rect_Type2 :
    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let matching_inv_rect_Type2 hterm h1 =
  let hcut = matching_rect_Type2 h1 hterm in hcut __

(** val matching_inv_rect_Type1 :
    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let matching_inv_rect_Type1 hterm h1 =
  let hcut = matching_rect_Type1 h1 hterm in hcut __

(** val matching_inv_rect_Type0 :
    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let matching_inv_rect_Type0 hterm h1 =
  let hcut = matching_rect_Type0 h1 hterm in hcut __

(** val matching_jmdiscr : matching -> matching -> __ **)
let matching_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let Mk_matching = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y

(** val mfe_cast_fn_type :
    matching -> ident List.list -> ident List.list -> __ -> __ **)
let mfe_cast_fn_type m vs vs' =
  Extralib.eq_rect_Type0_r vs (fun m0 -> m0) vs'

(** val match_program_rect_Type4 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type4 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_rect_Type5 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type5 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_rect_Type3 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type3 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_rect_Type2 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type2 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_rect_Type1 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type1 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_rect_Type0 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    'a1) -> 'a1 **)
let rec match_program_rect_Type0 m p1 p2 h_mk_match_program =
  h_mk_match_program __ __ __

(** val match_program_inv_rect_Type4 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let match_program_inv_rect_Type4 x1 x2 x3 h1 =
  let hcut = match_program_rect_Type4 x1 x2 x3 h1 in hcut __

(** val match_program_inv_rect_Type3 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let match_program_inv_rect_Type3 x1 x2 x3 h1 =
  let hcut = match_program_rect_Type3 x1 x2 x3 h1 in hcut __

(** val match_program_inv_rect_Type2 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let match_program_inv_rect_Type2 x1 x2 x3 h1 =
  let hcut = match_program_rect_Type2 x1 x2 x3 h1 in hcut __

(** val match_program_inv_rect_Type1 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let match_program_inv_rect_Type1 x1 x2 x3 h1 =
  let hcut = match_program_rect_Type1 x1 x2 x3 h1 in hcut __

(** val match_program_inv_rect_Type0 :
    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
    -> 'a1) -> 'a1 **)
let match_program_inv_rect_Type0 x1 x2 x3 h1 =
  let hcut = match_program_rect_Type0 x1 x2 x3 h1 in hcut __

(** val match_program_discr :
    matching -> (__, __) program -> (__, __) program -> __ **)
let match_program_discr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val match_program_jmdiscr :
    matching -> (__, __) program -> (__, __) program -> __ **)
let match_program_jmdiscr a1 a2 a3 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

type external_function = { ef_id : ident; ef_sig : signature }

(** val external_function_rect_Type4 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type4 h_mk_external_function x_4131 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4131 in
  h_mk_external_function ef_id0 ef_sig0

(** val external_function_rect_Type5 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type5 h_mk_external_function x_4133 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4133 in
  h_mk_external_function ef_id0 ef_sig0

(** val external_function_rect_Type3 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type3 h_mk_external_function x_4135 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4135 in
  h_mk_external_function ef_id0 ef_sig0

(** val external_function_rect_Type2 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type2 h_mk_external_function x_4137 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4137 in
  h_mk_external_function ef_id0 ef_sig0

(** val external_function_rect_Type1 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type1 h_mk_external_function x_4139 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4139 in
  h_mk_external_function ef_id0 ef_sig0

(** val external_function_rect_Type0 :
    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
let rec external_function_rect_Type0 h_mk_external_function x_4141 =
  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4141 in
  h_mk_external_function ef_id0 ef_sig0

(** val ef_id : external_function -> ident **)
let rec ef_id xxx =
  xxx.ef_id

(** val ef_sig : external_function -> signature **)
let rec ef_sig xxx =
  xxx.ef_sig

(** val external_function_inv_rect_Type4 :
    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
let external_function_inv_rect_Type4 hterm h1 =
  let hcut = external_function_rect_Type4 h1 hterm in hcut __

(** val external_function_inv_rect_Type3 :
    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
let external_function_inv_rect_Type3 hterm h1 =
  let hcut = external_function_rect_Type3 h1 hterm in hcut __

(** val external_function_inv_rect_Type2 :
    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
let external_function_inv_rect_Type2 hterm h1 =
  let hcut = external_function_rect_Type2 h1 hterm in hcut __

(** val external_function_inv_rect_Type1 :
    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
let external_function_inv_rect_Type1 hterm h1 =
  let hcut = external_function_rect_Type1 h1 hterm in hcut __

(** val external_function_inv_rect_Type0 :
    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
let external_function_inv_rect_Type0 hterm h1 =
  let hcut = external_function_rect_Type0 h1 hterm in hcut __

(** val external_function_discr :
    external_function -> external_function -> __ **)
let external_function_discr x y =
  Logic.eq_rect_Type2 x
    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
    y

(** val external_function_jmdiscr :
    external_function -> external_function -> __ **)
let external_function_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
    y

type externalFunction = external_function

(** val external_function_tag : external_function -> ident **)
let external_function_tag =
  ef_id

(** val external_function_sig : external_function -> signature **)
let external_function_sig =
  ef_sig

type 'f fundef =
| Internal of 'f
| External of external_function

(** val fundef_rect_Type4 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type4 h_Internal h_External = function
| Internal x_4161 -> h_Internal x_4161
| External x_4162 -> h_External x_4162

(** val fundef_rect_Type5 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type5 h_Internal h_External = function
| Internal x_4166 -> h_Internal x_4166
| External x_4167 -> h_External x_4167

(** val fundef_rect_Type3 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type3 h_Internal h_External = function
| Internal x_4171 -> h_Internal x_4171
| External x_4172 -> h_External x_4172

(** val fundef_rect_Type2 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type2 h_Internal h_External = function
| Internal x_4176 -> h_Internal x_4176
| External x_4177 -> h_External x_4177

(** val fundef_rect_Type1 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type1 h_Internal h_External = function
| Internal x_4181 -> h_Internal x_4181
| External x_4182 -> h_External x_4182

(** val fundef_rect_Type0 :
    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
let rec fundef_rect_Type0 h_Internal h_External = function
| Internal x_4186 -> h_Internal x_4186
| External x_4187 -> h_External x_4187

(** val fundef_inv_rect_Type4 :
    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
    'a2 **)
let fundef_inv_rect_Type4 hterm h1 h2 =
  let hcut = fundef_rect_Type4 h1 h2 hterm in hcut __

(** val fundef_inv_rect_Type3 :
    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
    'a2 **)
let fundef_inv_rect_Type3 hterm h1 h2 =
  let hcut = fundef_rect_Type3 h1 h2 hterm in hcut __

(** val fundef_inv_rect_Type2 :
    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
    'a2 **)
let fundef_inv_rect_Type2 hterm h1 h2 =
  let hcut = fundef_rect_Type2 h1 h2 hterm in hcut __

(** val fundef_inv_rect_Type1 :
    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
    'a2 **)
let fundef_inv_rect_Type1 hterm h1 h2 =
  let hcut = fundef_rect_Type1 h1 h2 hterm in hcut __

(** val fundef_inv_rect_Type0 :
    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
    'a2 **)
let fundef_inv_rect_Type0 hterm h1 h2 =
  let hcut = fundef_rect_Type0 h1 h2 hterm in hcut __

(** val fundef_discr : 'a1 fundef -> 'a1 fundef -> __ **)
let fundef_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
     | External a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __ **)
let fundef_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
     | External a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef **)
let transf_fundef transf = function
| Internal f -> Internal (transf f)
| External ef -> External ef

(** val transf_partial_fundef :
    ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res **)
let transf_partial_fundef transf_partial = function
| Internal f ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic transf_partial f)
      (fun f' -> Obj.magic (Errors.OK (Internal f'))))
| External ef -> Errors.OK (External ef)