open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

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 Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Coqlib

open CostLabel

type type0 =
| Tvoid
| Tint of AST.intsize * AST.signedness
| Tpointer of type0
| Tarray of type0 * Nat.nat
| Tfunction of typelist * type0
| Tstruct of AST.ident * fieldlist
| Tunion of AST.ident * fieldlist
| Tcomp_ptr of AST.ident
and typelist =
| Tnil
| Tcons of type0 * typelist
and fieldlist =
| Fnil
| Fcons of AST.ident * type0 * fieldlist

(** val type_inv_rect_Type4 :
    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let type_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut =
    match hterm with
    | Tvoid -> h1
    | Tint (x, x0) -> h2 x x0
    | Tpointer x -> h3 x
    | Tarray (x, x0) -> h4 x x0
    | Tfunction (x, x0) -> h5 x x0
    | Tstruct (x, x0) -> h6 x x0
    | Tunion (x, x0) -> h7 x x0
    | Tcomp_ptr x -> h8 x
  in
  hcut __

(** val type_inv_rect_Type3 :
    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let type_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut =
    match hterm with
    | Tvoid -> h1
    | Tint (x, x0) -> h2 x x0
    | Tpointer x -> h3 x
    | Tarray (x, x0) -> h4 x x0
    | Tfunction (x, x0) -> h5 x x0
    | Tstruct (x, x0) -> h6 x x0
    | Tunion (x, x0) -> h7 x x0
    | Tcomp_ptr x -> h8 x
  in
  hcut __

(** val type_inv_rect_Type2 :
    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let type_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut =
    match hterm with
    | Tvoid -> h1
    | Tint (x, x0) -> h2 x x0
    | Tpointer x -> h3 x
    | Tarray (x, x0) -> h4 x x0
    | Tfunction (x, x0) -> h5 x x0
    | Tstruct (x, x0) -> h6 x x0
    | Tunion (x, x0) -> h7 x x0
    | Tcomp_ptr x -> h8 x
  in
  hcut __

(** val type_inv_rect_Type1 :
    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let type_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut =
    match hterm with
    | Tvoid -> h1
    | Tint (x, x0) -> h2 x x0
    | Tpointer x -> h3 x
    | Tarray (x, x0) -> h4 x x0
    | Tfunction (x, x0) -> h5 x x0
    | Tstruct (x, x0) -> h6 x x0
    | Tunion (x, x0) -> h7 x x0
    | Tcomp_ptr x -> h8 x
  in
  hcut __

(** val type_inv_rect_Type0 :
    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let type_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut =
    match hterm with
    | Tvoid -> h1
    | Tint (x, x0) -> h2 x x0
    | Tpointer x -> h3 x
    | Tarray (x, x0) -> h4 x x0
    | Tfunction (x, x0) -> h5 x x0
    | Tstruct (x, x0) -> h6 x x0
    | Tunion (x, x0) -> h7 x x0
    | Tcomp_ptr x -> h8 x
  in
  hcut __

(** val typelist_inv_rect_Type4 :
    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
let typelist_inv_rect_Type4 hterm h1 h2 =
  let hcut =
    match hterm with
    | Tnil -> h1
    | Tcons (x, x0) -> h2 x x0
  in
  hcut __

(** val typelist_inv_rect_Type3 :
    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
let typelist_inv_rect_Type3 hterm h1 h2 =
  let hcut =
    match hterm with
    | Tnil -> h1
    | Tcons (x, x0) -> h2 x x0
  in
  hcut __

(** val typelist_inv_rect_Type2 :
    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
let typelist_inv_rect_Type2 hterm h1 h2 =
  let hcut =
    match hterm with
    | Tnil -> h1
    | Tcons (x, x0) -> h2 x x0
  in
  hcut __

(** val typelist_inv_rect_Type1 :
    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
let typelist_inv_rect_Type1 hterm h1 h2 =
  let hcut =
    match hterm with
    | Tnil -> h1
    | Tcons (x, x0) -> h2 x x0
  in
  hcut __

(** val typelist_inv_rect_Type0 :
    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
let typelist_inv_rect_Type0 hterm h1 h2 =
  let hcut =
    match hterm with
    | Tnil -> h1
    | Tcons (x, x0) -> h2 x x0
  in
  hcut __

(** val fieldlist_inv_rect_Type4 :
    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
    'a1) -> 'a1 **)
let fieldlist_inv_rect_Type4 hterm h1 h2 =
  let hcut =
    match hterm with
    | Fnil -> h1
    | Fcons (x, x0, x1) -> h2 x x0 x1
  in
  hcut __

(** val fieldlist_inv_rect_Type3 :
    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
    'a1) -> 'a1 **)
let fieldlist_inv_rect_Type3 hterm h1 h2 =
  let hcut =
    match hterm with
    | Fnil -> h1
    | Fcons (x, x0, x1) -> h2 x x0 x1
  in
  hcut __

(** val fieldlist_inv_rect_Type2 :
    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
    'a1) -> 'a1 **)
let fieldlist_inv_rect_Type2 hterm h1 h2 =
  let hcut =
    match hterm with
    | Fnil -> h1
    | Fcons (x, x0, x1) -> h2 x x0 x1
  in
  hcut __

(** val fieldlist_inv_rect_Type1 :
    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
    'a1) -> 'a1 **)
let fieldlist_inv_rect_Type1 hterm h1 h2 =
  let hcut =
    match hterm with
    | Fnil -> h1
    | Fcons (x, x0, x1) -> h2 x x0 x1
  in
  hcut __

(** val fieldlist_inv_rect_Type0 :
    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
    'a1) -> 'a1 **)
let fieldlist_inv_rect_Type0 hterm h1 h2 =
  let hcut =
    match hterm with
    | Fnil -> h1
    | Fcons (x, x0, x1) -> h2 x x0 x1
  in
  hcut __

(** val type_discr : type0 -> type0 -> __ **)
let type_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Tvoid -> Obj.magic (fun _ dH -> dH)
     | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
     | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val typelist_discr : typelist -> typelist -> __ **)
let typelist_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Tnil -> Obj.magic (fun _ dH -> dH)
     | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val fieldlist_discr : fieldlist -> fieldlist -> __ **)
let fieldlist_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fnil -> Obj.magic (fun _ dH -> dH)
     | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val type_jmdiscr : type0 -> type0 -> __ **)
let type_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Tvoid -> Obj.magic (fun _ dH -> dH)
     | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
     | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val typelist_jmdiscr : typelist -> typelist -> __ **)
let typelist_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Tnil -> Obj.magic (fun _ dH -> dH)
     | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val fieldlist_jmdiscr : fieldlist -> fieldlist -> __ **)
let fieldlist_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fnil -> Obj.magic (fun _ dH -> dH)
     | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

type unary_operation =
| Onotbool
| Onotint
| Oneg

(** val unary_operation_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type4 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type5 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type3 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type2 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type1 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
let rec unary_operation_rect_Type0 h_Onotbool h_Onotint h_Oneg = function
| Onotbool -> h_Onotbool
| Onotint -> h_Onotint
| Oneg -> h_Oneg

(** val unary_operation_inv_rect_Type4 :
    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let unary_operation_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = unary_operation_rect_Type4 h1 h2 h3 hterm in hcut __

(** val unary_operation_inv_rect_Type3 :
    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let unary_operation_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = unary_operation_rect_Type3 h1 h2 h3 hterm in hcut __

(** val unary_operation_inv_rect_Type2 :
    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let unary_operation_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = unary_operation_rect_Type2 h1 h2 h3 hterm in hcut __

(** val unary_operation_inv_rect_Type1 :
    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let unary_operation_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = unary_operation_rect_Type1 h1 h2 h3 hterm in hcut __

(** val unary_operation_inv_rect_Type0 :
    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let unary_operation_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = unary_operation_rect_Type0 h1 h2 h3 hterm in hcut __

(** val unary_operation_discr : unary_operation -> unary_operation -> __ **)
let unary_operation_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Onotbool -> Obj.magic (fun _ dH -> dH)
     | Onotint -> Obj.magic (fun _ dH -> dH)
     | Oneg -> Obj.magic (fun _ dH -> dH)) y

(** val unary_operation_jmdiscr :
    unary_operation -> unary_operation -> __ **)
let unary_operation_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Onotbool -> Obj.magic (fun _ dH -> dH)
     | Onotint -> Obj.magic (fun _ dH -> dH)
     | Oneg -> Obj.magic (fun _ dH -> dH)) y

type binary_operation =
| Oadd
| Osub
| Omul
| Odiv
| Omod
| Oand
| Oor
| Oxor
| Oshl
| Oshr
| Oeq
| One
| Olt
| Ogt
| Ole
| Oge

(** val binary_operation_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
| Oadd -> h_Oadd
| Osub -> h_Osub
| Omul -> h_Omul
| Odiv -> h_Odiv
| Omod -> h_Omod
| Oand -> h_Oand
| Oor -> h_Oor
| Oxor -> h_Oxor
| Oshl -> h_Oshl
| Oshr -> h_Oshr
| Oeq -> h_Oeq
| One -> h_One
| Olt -> h_Olt
| Ogt -> h_Ogt
| Ole -> h_Ole
| Oge -> h_Oge

(** val binary_operation_inv_rect_Type4 :
    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
  let hcut =
    binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 hterm
  in
  hcut __

(** val binary_operation_inv_rect_Type3 :
    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
  let hcut =
    binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 hterm
  in
  hcut __

(** val binary_operation_inv_rect_Type2 :
    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
  let hcut =
    binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 hterm
  in
  hcut __

(** val binary_operation_inv_rect_Type1 :
    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
  let hcut =
    binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 hterm
  in
  hcut __

(** val binary_operation_inv_rect_Type0 :
    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
  let hcut =
    binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 hterm
  in
  hcut __

(** val binary_operation_discr :
    binary_operation -> binary_operation -> __ **)
let binary_operation_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Oadd -> Obj.magic (fun _ dH -> dH)
     | Osub -> Obj.magic (fun _ dH -> dH)
     | Omul -> Obj.magic (fun _ dH -> dH)
     | Odiv -> Obj.magic (fun _ dH -> dH)
     | Omod -> Obj.magic (fun _ dH -> dH)
     | Oand -> Obj.magic (fun _ dH -> dH)
     | Oor -> Obj.magic (fun _ dH -> dH)
     | Oxor -> Obj.magic (fun _ dH -> dH)
     | Oshl -> Obj.magic (fun _ dH -> dH)
     | Oshr -> Obj.magic (fun _ dH -> dH)
     | Oeq -> Obj.magic (fun _ dH -> dH)
     | One -> Obj.magic (fun _ dH -> dH)
     | Olt -> Obj.magic (fun _ dH -> dH)
     | Ogt -> Obj.magic (fun _ dH -> dH)
     | Ole -> Obj.magic (fun _ dH -> dH)
     | Oge -> Obj.magic (fun _ dH -> dH)) y

(** val binary_operation_jmdiscr :
    binary_operation -> binary_operation -> __ **)
let binary_operation_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Oadd -> Obj.magic (fun _ dH -> dH)
     | Osub -> Obj.magic (fun _ dH -> dH)
     | Omul -> Obj.magic (fun _ dH -> dH)
     | Odiv -> Obj.magic (fun _ dH -> dH)
     | Omod -> Obj.magic (fun _ dH -> dH)
     | Oand -> Obj.magic (fun _ dH -> dH)
     | Oor -> Obj.magic (fun _ dH -> dH)
     | Oxor -> Obj.magic (fun _ dH -> dH)
     | Oshl -> Obj.magic (fun _ dH -> dH)
     | Oshr -> Obj.magic (fun _ dH -> dH)
     | Oeq -> Obj.magic (fun _ dH -> dH)
     | One -> Obj.magic (fun _ dH -> dH)
     | Olt -> Obj.magic (fun _ dH -> dH)
     | Ogt -> Obj.magic (fun _ dH -> dH)
     | Ole -> Obj.magic (fun _ dH -> dH)
     | Oge -> Obj.magic (fun _ dH -> dH)) y

type expr =
| Expr of expr_descr * type0
and expr_descr =
| Econst_int of AST.intsize * AST.bvint
| Evar of AST.ident
| Ederef of expr
| Eaddrof of expr
| Eunop of unary_operation * expr
| Ebinop of binary_operation * expr * expr
| Ecast of type0 * expr
| Econdition of expr * expr * expr
| Eandbool of expr * expr
| Eorbool of expr * expr
| Esizeof of type0
| Efield of expr * AST.ident
| Ecost of CostLabel.costlabel * expr

(** val expr_inv_rect_Type4 :
    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type4 hterm h1 =
  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __

(** val expr_inv_rect_Type3 :
    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type3 hterm h1 =
  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __

(** val expr_inv_rect_Type2 :
    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type2 hterm h1 =
  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __

(** val expr_inv_rect_Type1 :
    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type1 hterm h1 =
  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __

(** val expr_inv_rect_Type0 :
    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type0 hterm h1 =
  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __

(** val expr_descr_inv_rect_Type4 :
    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
    expr -> __ -> 'a1) -> 'a1 **)
let expr_descr_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut =
    match hterm with
    | Econst_int (x, x0) -> h1 x x0
    | Evar x -> h2 x
    | Ederef x -> h3 x
    | Eaddrof x -> h4 x
    | Eunop (x, x0) -> h5 x x0
    | Ebinop (x, x0, x1) -> h6 x x0 x1
    | Ecast (x, x0) -> h7 x x0
    | Econdition (x, x0, x1) -> h8 x x0 x1
    | Eandbool (x, x0) -> h9 x x0
    | Eorbool (x, x0) -> h10 x x0
    | Esizeof x -> h11 x
    | Efield (x, x0) -> h12 x x0
    | Ecost (x, x0) -> h13 x x0
  in
  hcut __

(** val expr_descr_inv_rect_Type3 :
    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
    expr -> __ -> 'a1) -> 'a1 **)
let expr_descr_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut =
    match hterm with
    | Econst_int (x, x0) -> h1 x x0
    | Evar x -> h2 x
    | Ederef x -> h3 x
    | Eaddrof x -> h4 x
    | Eunop (x, x0) -> h5 x x0
    | Ebinop (x, x0, x1) -> h6 x x0 x1
    | Ecast (x, x0) -> h7 x x0
    | Econdition (x, x0, x1) -> h8 x x0 x1
    | Eandbool (x, x0) -> h9 x x0
    | Eorbool (x, x0) -> h10 x x0
    | Esizeof x -> h11 x
    | Efield (x, x0) -> h12 x x0
    | Ecost (x, x0) -> h13 x x0
  in
  hcut __

(** val expr_descr_inv_rect_Type2 :
    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
    expr -> __ -> 'a1) -> 'a1 **)
let expr_descr_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut =
    match hterm with
    | Econst_int (x, x0) -> h1 x x0
    | Evar x -> h2 x
    | Ederef x -> h3 x
    | Eaddrof x -> h4 x
    | Eunop (x, x0) -> h5 x x0
    | Ebinop (x, x0, x1) -> h6 x x0 x1
    | Ecast (x, x0) -> h7 x x0
    | Econdition (x, x0, x1) -> h8 x x0 x1
    | Eandbool (x, x0) -> h9 x x0
    | Eorbool (x, x0) -> h10 x x0
    | Esizeof x -> h11 x
    | Efield (x, x0) -> h12 x x0
    | Ecost (x, x0) -> h13 x x0
  in
  hcut __

(** val expr_descr_inv_rect_Type1 :
    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
    expr -> __ -> 'a1) -> 'a1 **)
let expr_descr_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut =
    match hterm with
    | Econst_int (x, x0) -> h1 x x0
    | Evar x -> h2 x
    | Ederef x -> h3 x
    | Eaddrof x -> h4 x
    | Eunop (x, x0) -> h5 x x0
    | Ebinop (x, x0, x1) -> h6 x x0 x1
    | Ecast (x, x0) -> h7 x x0
    | Econdition (x, x0, x1) -> h8 x x0 x1
    | Eandbool (x, x0) -> h9 x x0
    | Eorbool (x, x0) -> h10 x x0
    | Esizeof x -> h11 x
    | Efield (x, x0) -> h12 x x0
    | Ecost (x, x0) -> h13 x x0
  in
  hcut __

(** val expr_descr_inv_rect_Type0 :
    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
    expr -> __ -> 'a1) -> 'a1 **)
let expr_descr_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut =
    match hterm with
    | Econst_int (x, x0) -> h1 x x0
    | Evar x -> h2 x
    | Ederef x -> h3 x
    | Eaddrof x -> h4 x
    | Eunop (x, x0) -> h5 x x0
    | Ebinop (x, x0, x1) -> h6 x x0 x1
    | Ecast (x, x0) -> h7 x x0
    | Econdition (x, x0, x1) -> h8 x x0 x1
    | Eandbool (x, x0) -> h9 x x0
    | Eorbool (x, x0) -> h10 x x0
    | Esizeof x -> h11 x
    | Efield (x, x0) -> h12 x x0
    | Ecost (x, x0) -> h13 x x0
  in
  hcut __

(** val expr_discr : expr -> expr -> __ **)
let expr_discr x y =
  Logic.eq_rect_Type2 x
    (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val expr_descr_discr : expr_descr -> expr_descr -> __ **)
let expr_descr_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Evar a0 -> Obj.magic (fun _ dH -> dH __)
     | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
     | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
     | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
     | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val expr_jmdiscr : expr -> expr -> __ **)
let expr_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val expr_descr_jmdiscr : expr_descr -> expr_descr -> __ **)
let expr_descr_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Evar a0 -> Obj.magic (fun _ dH -> dH __)
     | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
     | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
     | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
     | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val typeof : expr -> type0 **)
let typeof = function
| Expr (de, te) -> te

type label = AST.ident

type statement =
| Sskip
| Sassign of expr * expr
| Scall of expr Types.option * expr * expr List.list
| Ssequence of statement * statement
| Sifthenelse of expr * statement * statement
| Swhile of expr * statement
| Sdowhile of expr * statement
| Sfor of statement * expr * statement * statement
| Sbreak
| Scontinue
| Sreturn of expr Types.option
| Sswitch of expr * labeled_statements
| Slabel of label * statement
| Sgoto of label
| Scost of CostLabel.costlabel * statement
and labeled_statements =
| LSdefault of statement
| LScase of AST.intsize * AST.bvint * statement * labeled_statements

(** val statement_inv_rect_Type4 :
    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
    -> 'a1 **)
let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
  let hcut =
    match hterm with
    | Sskip -> h1
    | Sassign (x, x0) -> h2 x x0
    | Scall (x, x0, x1) -> h3 x x0 x1
    | Ssequence (x, x0) -> h4 x x0
    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
    | Swhile (x, x0) -> h6 x x0
    | Sdowhile (x, x0) -> h7 x x0
    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
    | Sbreak -> h9
    | Scontinue -> h10
    | Sreturn x -> h11 x
    | Sswitch (x, x0) -> h12 x x0
    | Slabel (x, x0) -> h13 x x0
    | Sgoto x -> h14 x
    | Scost (x, x0) -> h15 x x0
  in
  hcut __

(** val statement_inv_rect_Type3 :
    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
    -> 'a1 **)
let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
  let hcut =
    match hterm with
    | Sskip -> h1
    | Sassign (x, x0) -> h2 x x0
    | Scall (x, x0, x1) -> h3 x x0 x1
    | Ssequence (x, x0) -> h4 x x0
    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
    | Swhile (x, x0) -> h6 x x0
    | Sdowhile (x, x0) -> h7 x x0
    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
    | Sbreak -> h9
    | Scontinue -> h10
    | Sreturn x -> h11 x
    | Sswitch (x, x0) -> h12 x x0
    | Slabel (x, x0) -> h13 x x0
    | Sgoto x -> h14 x
    | Scost (x, x0) -> h15 x x0
  in
  hcut __

(** val statement_inv_rect_Type2 :
    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
    -> 'a1 **)
let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
  let hcut =
    match hterm with
    | Sskip -> h1
    | Sassign (x, x0) -> h2 x x0
    | Scall (x, x0, x1) -> h3 x x0 x1
    | Ssequence (x, x0) -> h4 x x0
    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
    | Swhile (x, x0) -> h6 x x0
    | Sdowhile (x, x0) -> h7 x x0
    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
    | Sbreak -> h9
    | Scontinue -> h10
    | Sreturn x -> h11 x
    | Sswitch (x, x0) -> h12 x x0
    | Slabel (x, x0) -> h13 x x0
    | Sgoto x -> h14 x
    | Scost (x, x0) -> h15 x x0
  in
  hcut __

(** val statement_inv_rect_Type1 :
    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
    -> 'a1 **)
let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
  let hcut =
    match hterm with
    | Sskip -> h1
    | Sassign (x, x0) -> h2 x x0
    | Scall (x, x0, x1) -> h3 x x0 x1
    | Ssequence (x, x0) -> h4 x x0
    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
    | Swhile (x, x0) -> h6 x x0
    | Sdowhile (x, x0) -> h7 x x0
    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
    | Sbreak -> h9
    | Scontinue -> h10
    | Sreturn x -> h11 x
    | Sswitch (x, x0) -> h12 x x0
    | Slabel (x, x0) -> h13 x x0
    | Sgoto x -> h14 x
    | Scost (x, x0) -> h15 x x0
  in
  hcut __

(** val statement_inv_rect_Type0 :
    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
    -> 'a1 **)
let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
  let hcut =
    match hterm with
    | Sskip -> h1
    | Sassign (x, x0) -> h2 x x0
    | Scall (x, x0, x1) -> h3 x x0 x1
    | Ssequence (x, x0) -> h4 x x0
    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
    | Swhile (x, x0) -> h6 x x0
    | Sdowhile (x, x0) -> h7 x x0
    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
    | Sbreak -> h9
    | Scontinue -> h10
    | Sreturn x -> h11 x
    | Sswitch (x, x0) -> h12 x x0
    | Slabel (x, x0) -> h13 x x0
    | Sgoto x -> h14 x
    | Scost (x, x0) -> h15 x x0
  in
  hcut __

(** val labeled_statements_inv_rect_Type4 :
    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
let labeled_statements_inv_rect_Type4 hterm h1 h2 =
  let hcut =
    match hterm with
    | LSdefault x -> h1 x
    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
  in
  hcut __

(** val labeled_statements_inv_rect_Type3 :
    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
let labeled_statements_inv_rect_Type3 hterm h1 h2 =
  let hcut =
    match hterm with
    | LSdefault x -> h1 x
    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
  in
  hcut __

(** val labeled_statements_inv_rect_Type2 :
    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
let labeled_statements_inv_rect_Type2 hterm h1 h2 =
  let hcut =
    match hterm with
    | LSdefault x -> h1 x
    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
  in
  hcut __

(** val labeled_statements_inv_rect_Type1 :
    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
let labeled_statements_inv_rect_Type1 hterm h1 h2 =
  let hcut =
    match hterm with
    | LSdefault x -> h1 x
    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
  in
  hcut __

(** val labeled_statements_inv_rect_Type0 :
    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
let labeled_statements_inv_rect_Type0 hterm h1 h2 =
  let hcut =
    match hterm with
    | LSdefault x -> h1 x
    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
  in
  hcut __

(** val statement_discr : statement -> statement -> __ **)
let statement_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Sskip -> Obj.magic (fun _ dH -> dH)
     | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sbreak -> Obj.magic (fun _ dH -> dH)
     | Scontinue -> Obj.magic (fun _ dH -> dH)
     | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
     | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
     | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val labeled_statements_discr :
    labeled_statements -> labeled_statements -> __ **)
let labeled_statements_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
     | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val statement_jmdiscr : statement -> statement -> __ **)
let statement_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Sskip -> Obj.magic (fun _ dH -> dH)
     | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sbreak -> Obj.magic (fun _ dH -> dH)
     | Scontinue -> Obj.magic (fun _ dH -> dH)
     | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
     | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
     | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val labeled_statements_jmdiscr :
    labeled_statements -> labeled_statements -> __ **)
let labeled_statements_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
     | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y

type function0 = { fn_return : type0;
                   fn_params : (AST.ident, type0) Types.prod List.list;
                   fn_vars : (AST.ident, type0) Types.prod List.list;
                   fn_body : statement }

(** val function_rect_Type4 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type4 h_mk_function x_4495 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4495
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val function_rect_Type5 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type5 h_mk_function x_4497 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4497
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val function_rect_Type3 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type3 h_mk_function x_4499 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4499
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val function_rect_Type2 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type2 h_mk_function x_4501 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4501
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val function_rect_Type1 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type1 h_mk_function x_4503 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4503
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val function_rect_Type0 :
    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
let rec function_rect_Type0 h_mk_function x_4505 =
  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    fn_body = fn_body0 } = x_4505
  in
  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0

(** val fn_return : function0 -> type0 **)
let rec fn_return xxx =
  xxx.fn_return

(** val fn_params : function0 -> (AST.ident, type0) Types.prod List.list **)
let rec fn_params xxx =
  xxx.fn_params

(** val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list **)
let rec fn_vars xxx =
  xxx.fn_vars

(** val fn_body : function0 -> statement **)
let rec fn_body xxx =
  xxx.fn_body

(** val function_inv_rect_Type4 :
    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
let function_inv_rect_Type4 hterm h1 =
  let hcut = function_rect_Type4 h1 hterm in hcut __

(** val function_inv_rect_Type3 :
    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
let function_inv_rect_Type3 hterm h1 =
  let hcut = function_rect_Type3 h1 hterm in hcut __

(** val function_inv_rect_Type2 :
    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
let function_inv_rect_Type2 hterm h1 =
  let hcut = function_rect_Type2 h1 hterm in hcut __

(** val function_inv_rect_Type1 :
    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
let function_inv_rect_Type1 hterm h1 =
  let hcut = function_rect_Type1 h1 hterm in hcut __

(** val function_inv_rect_Type0 :
    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
let function_inv_rect_Type0 hterm h1 =
  let hcut = function_rect_Type0 h1 hterm in hcut __

(** val function_discr : function0 -> function0 -> __ **)
let function_discr x y =
  Logic.eq_rect_Type2 x
    (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val function_jmdiscr : function0 -> function0 -> __ **)
let function_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

type clight_fundef =
| CL_Internal of function0
| CL_External of AST.ident * typelist * type0

(** val clight_fundef_rect_Type4 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
| CL_Internal x_4527 -> h_CL_Internal x_4527
| CL_External (x_4530, x_4529, x_4528) -> h_CL_External x_4530 x_4529 x_4528

(** val clight_fundef_rect_Type5 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
| CL_Internal x_4534 -> h_CL_Internal x_4534
| CL_External (x_4537, x_4536, x_4535) -> h_CL_External x_4537 x_4536 x_4535

(** val clight_fundef_rect_Type3 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
| CL_Internal x_4541 -> h_CL_Internal x_4541
| CL_External (x_4544, x_4543, x_4542) -> h_CL_External x_4544 x_4543 x_4542

(** val clight_fundef_rect_Type2 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
| CL_Internal x_4548 -> h_CL_Internal x_4548
| CL_External (x_4551, x_4550, x_4549) -> h_CL_External x_4551 x_4550 x_4549

(** val clight_fundef_rect_Type1 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
| CL_Internal x_4555 -> h_CL_Internal x_4555
| CL_External (x_4558, x_4557, x_4556) -> h_CL_External x_4558 x_4557 x_4556

(** val clight_fundef_rect_Type0 :
    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
    clight_fundef -> 'a1 **)
let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
| CL_Internal x_4562 -> h_CL_Internal x_4562
| CL_External (x_4565, x_4564, x_4563) -> h_CL_External x_4565 x_4564 x_4563

(** val clight_fundef_inv_rect_Type4 :
    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
    type0 -> __ -> 'a1) -> 'a1 **)
let clight_fundef_inv_rect_Type4 hterm h1 h2 =
  let hcut = clight_fundef_rect_Type4 h1 h2 hterm in hcut __

(** val clight_fundef_inv_rect_Type3 :
    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
    type0 -> __ -> 'a1) -> 'a1 **)
let clight_fundef_inv_rect_Type3 hterm h1 h2 =
  let hcut = clight_fundef_rect_Type3 h1 h2 hterm in hcut __

(** val clight_fundef_inv_rect_Type2 :
    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
    type0 -> __ -> 'a1) -> 'a1 **)
let clight_fundef_inv_rect_Type2 hterm h1 h2 =
  let hcut = clight_fundef_rect_Type2 h1 h2 hterm in hcut __

(** val clight_fundef_inv_rect_Type1 :
    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
    type0 -> __ -> 'a1) -> 'a1 **)
let clight_fundef_inv_rect_Type1 hterm h1 h2 =
  let hcut = clight_fundef_rect_Type1 h1 h2 hterm in hcut __

(** val clight_fundef_inv_rect_Type0 :
    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
    type0 -> __ -> 'a1) -> 'a1 **)
let clight_fundef_inv_rect_Type0 hterm h1 h2 =
  let hcut = clight_fundef_rect_Type0 h1 h2 hterm in hcut __

(** val clight_fundef_discr : clight_fundef -> clight_fundef -> __ **)
let clight_fundef_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

(** val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __ **)
let clight_fundef_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

type clight_program =
  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program

(** val type_of_params :
    (AST.ident, type0) Types.prod List.list -> typelist **)
let rec type_of_params = function
| List.Nil -> Tnil
| List.Cons (h, rem) ->
  let { Types.fst = id; Types.snd = ty } = h in
  Tcons (ty, (type_of_params rem))

(** val type_of_function : function0 -> type0 **)
let type_of_function f =
  Tfunction ((type_of_params f.fn_params), f.fn_return)

(** val type_of_fundef : clight_fundef -> type0 **)
let type_of_fundef = function
| CL_Internal fd -> type_of_function fd
| CL_External (id, args, res) -> Tfunction (args, res)

(** val alignof : type0 -> Nat.nat **)
let rec alignof = function
| Tvoid -> Nat.S Nat.O
| Tint (sz, x) ->
  (match sz with
   | AST.I8 -> Nat.S Nat.O
   | AST.I16 -> Nat.S (Nat.S Nat.O)
   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
| Tpointer x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
| Tarray (t', n) -> alignof t'
| Tfunction (x, x0) -> Nat.S Nat.O
| Tstruct (x, fld) -> alignof_fields fld
| Tunion (x, fld) -> alignof_fields fld
| Tcomp_ptr x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
(** val alignof_fields : fieldlist -> Nat.nat **)
and alignof_fields = function
| Fnil -> Nat.S Nat.O
| Fcons (id, t, f') -> Nat.max (alignof t) (alignof_fields f')

(** val sizeof : type0 -> Nat.nat **)
let rec sizeof t = match t with
| Tvoid -> Nat.S Nat.O
| Tint (i, x) ->
  (match i with
   | AST.I8 -> Nat.S Nat.O
   | AST.I16 -> Nat.S (Nat.S Nat.O)
   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
| Tpointer x -> AST.size_pointer
| Tarray (t', n) -> Nat.times (sizeof t') (Nat.max (Nat.S Nat.O) n)
| Tfunction (x, x0) -> Nat.S Nat.O
| Tstruct (x, fld) ->
  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_struct fld Nat.O)) (alignof t)
| Tunion (x, fld) ->
  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_union fld)) (alignof t)
| Tcomp_ptr x -> AST.size_pointer
(** val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat **)
and sizeof_struct fld pos =
  match fld with
  | Fnil -> pos
  | Fcons (id, t, fld') ->
    sizeof_struct fld' (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t))
(** val sizeof_union : fieldlist -> Nat.nat **)
and sizeof_union = function
| Fnil -> Nat.O
| Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')

(** val field_offset_rec :
    AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
let rec field_offset_rec id fld pos =
  match fld with
  | Fnil ->
    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
      (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
  | Fcons (id', t, fld') ->
    (match AST.ident_eq id id' with
     | Types.Inl _ -> Errors.OK (Coqlib.align pos (alignof t))
     | Types.Inr _ ->
       field_offset_rec id fld'
         (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t)))

(** val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res **)
let field_offset id fld =
  field_offset_rec id fld Nat.O

(** val field_type : AST.ident -> fieldlist -> type0 Errors.res **)
let rec field_type id = function
| Fnil ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
| Fcons (id', t, fld') ->
  (match AST.ident_eq id id' with
   | Types.Inl _ -> Errors.OK t
   | Types.Inr _ -> field_type id fld')

(** val typ_of_type : type0 -> AST.typ **)
let typ_of_type = function
| Tvoid -> AST.ASTint (AST.I32, AST.Unsigned)
| Tint (sz, sg) -> AST.ASTint (sz, sg)
| Tpointer x -> AST.ASTptr
| Tarray (x, x0) -> AST.ASTptr
| Tfunction (x, x0) -> AST.ASTptr
| Tstruct (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
| Tunion (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
| Tcomp_ptr x -> AST.ASTptr

(** val opttyp_of_type : type0 -> AST.typ Types.option **)
let opttyp_of_type = function
| Tvoid -> Types.None
| Tint (sz, sg) -> Types.Some (AST.ASTint (sz, sg))
| Tpointer x -> Types.Some AST.ASTptr
| Tarray (x, x0) -> Types.Some AST.ASTptr
| Tfunction (x, x0) -> Types.Some AST.ASTptr
| Tstruct (x, x0) -> Types.None
| Tunion (x, x0) -> Types.None
| Tcomp_ptr x -> Types.Some AST.ASTptr

(** val typlist_of_typelist : typelist -> AST.typ List.list **)
let rec typlist_of_typelist = function
| Tnil -> List.Nil
| Tcons (hd, tl0) -> List.Cons ((typ_of_type hd), (typlist_of_typelist tl0))

type mode =
| By_value of AST.typ
| By_reference
| By_nothing of AST.typ

(** val mode_rect_Type4 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4615 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_rect_Type5 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4620 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_rect_Type3 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4625 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_rect_Type2 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4630 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_rect_Type1 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4635 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_rect_Type0 :
    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4640 = function
| By_value t -> h_By_value t
| By_reference -> h_By_reference
| By_nothing t -> h_By_nothing t

(** val mode_inv_rect_Type4 :
    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
let mode_inv_rect_Type4 x1 hterm h1 h2 h3 =
  let hcut = mode_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __

(** val mode_inv_rect_Type3 :
    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
let mode_inv_rect_Type3 x1 hterm h1 h2 h3 =
  let hcut = mode_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __

(** val mode_inv_rect_Type2 :
    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
let mode_inv_rect_Type2 x1 hterm h1 h2 h3 =
  let hcut = mode_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __

(** val mode_inv_rect_Type1 :
    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
let mode_inv_rect_Type1 x1 hterm h1 h2 h3 =
  let hcut = mode_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __

(** val mode_inv_rect_Type0 :
    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
let mode_inv_rect_Type0 x1 hterm h1 h2 h3 =
  let hcut = mode_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __

(** val mode_discr : AST.typ -> mode -> mode -> __ **)
let mode_discr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
     | By_reference -> Obj.magic (fun _ dH -> dH)
     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val mode_jmdiscr : AST.typ -> mode -> mode -> __ **)
let mode_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
     | By_reference -> Obj.magic (fun _ dH -> dH)
     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val access_mode : type0 -> mode **)
let access_mode = function
| Tvoid -> By_nothing (typ_of_type Tvoid)
| Tint (i, s) -> By_value (AST.ASTint (i, s))
| Tpointer x -> By_value AST.ASTptr
| Tarray (x, x0) -> By_reference
| Tfunction (x, x0) -> By_reference
| Tstruct (x, fList) -> By_nothing (typ_of_type (Tstruct (x, fList)))
| Tunion (x, fList) -> By_nothing (typ_of_type (Tunion (x, fList)))
| Tcomp_ptr x -> By_value AST.ASTptr

(** val signature_of_type : typelist -> type0 -> AST.signature **)
let signature_of_type args res =
  { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
    (opttyp_of_type res) }

(** val external_function :
    AST.ident -> typelist -> type0 -> AST.external_function **)
let external_function id targs tres =
  { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }