open Preamble

open CostLabel

open Coqlib

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 Csyntax

open TypeComparison

(** val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0 **)
let ptr_type ty = function
| Types.None -> Csyntax.Tpointer ty
| Types.Some n' -> Csyntax.Tarray (ty, n')

type classify_add_cases =
| Add_case_ii of AST.intsize * AST.signedness
| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
   * AST.signedness
| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
   * Csyntax.type0
| Add_default of Csyntax.type0 * Csyntax.type0

(** val classify_add_cases_rect_Type4 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7441 x_7440 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_rect_Type5 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7448 x_7447 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_rect_Type3 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7455 x_7454 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_rect_Type2 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7462 x_7461 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_rect_Type1 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7469 x_7468 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_rect_Type0 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    -> classify_add_cases -> 'a1 **)
let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7476 x_7475 = function
| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
| Add_default (ty1, ty2) -> h_add_default ty1 ty2

(** val classify_add_cases_inv_rect_Type4 :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_add_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_add_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_add_cases_inv_rect_Type3 :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_add_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_add_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_add_cases_inv_rect_Type2 :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_add_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_add_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_add_cases_inv_rect_Type1 :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_add_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_add_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_add_cases_inv_rect_Type0 :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_add_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_add_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_add_cases_discr :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
    classify_add_cases -> __ **)
let classify_add_cases_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Add_case_pi (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Add_case_ip (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_add_cases_jmdiscr :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
    classify_add_cases -> __ **)
let classify_add_cases_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Add_case_pi (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Add_case_ip (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_add :
    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases **)
let classify_add ty1 ty2 =
  match ty1 with
  | Csyntax.Tvoid -> Add_default (Csyntax.Tvoid, ty2)
  | Csyntax.Tint (sz1, sg1) ->
    (match ty2 with
     | Csyntax.Tvoid ->
       Add_default ((Csyntax.Tint (sz1, sg1)), Csyntax.Tvoid)
     | Csyntax.Tint (sz2, sg2) ->
       AST.inttyp_eq_elim' sz1 sz2 sg1 sg2 (Add_case_ii (sz1, sg1))
         (Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tint (sz2, sg2))))
     | Csyntax.Tpointer ty -> Add_case_ip (Types.None, sz1, sg1, ty)
     | Csyntax.Tarray (ty, n) -> Add_case_ip ((Types.Some n), sz1, sg1, ty)
     | Csyntax.Tfunction (x, x0) ->
       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tfunction (x, x0)))
     | Csyntax.Tstruct (x, x0) ->
       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tstruct (x, x0)))
     | Csyntax.Tunion (x, x0) ->
       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tunion (x, x0)))
     | Csyntax.Tcomp_ptr x ->
       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tcomp_ptr x)))
  | Csyntax.Tpointer ty ->
    (match ty2 with
     | Csyntax.Tvoid -> Add_default ((ptr_type ty Types.None), Csyntax.Tvoid)
     | Csyntax.Tint (x, x0) -> Add_case_pi (Types.None, ty, x, x0)
     | Csyntax.Tpointer x ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tpointer x))
     | Csyntax.Tarray (x, x0) ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tarray (x, x0)))
     | Csyntax.Tfunction (x, x0) ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
     | Csyntax.Tstruct (x, x0) ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
     | Csyntax.Tunion (x, x0) ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
     | Csyntax.Tcomp_ptr x ->
       Add_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
  | Csyntax.Tarray (ty, n) ->
    (match ty2 with
     | Csyntax.Tvoid ->
       Add_default ((ptr_type ty (Types.Some n)), Csyntax.Tvoid)
     | Csyntax.Tint (x, x0) -> Add_case_pi ((Types.Some n), ty, x, x0)
     | Csyntax.Tpointer x ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tpointer x))
     | Csyntax.Tarray (x, x0) ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tarray (x, x0)))
     | Csyntax.Tfunction (x, x0) ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tfunction (x,
         x0)))
     | Csyntax.Tstruct (x, x0) ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tstruct (x, x0)))
     | Csyntax.Tunion (x, x0) ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tunion (x, x0)))
     | Csyntax.Tcomp_ptr x ->
       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tcomp_ptr x)))
  | Csyntax.Tfunction (x, x0) ->
    Add_default ((Csyntax.Tfunction (x, x0)), ty2)
  | Csyntax.Tstruct (x, x0) -> Add_default ((Csyntax.Tstruct (x, x0)), ty2)
  | Csyntax.Tunion (x, x0) -> Add_default ((Csyntax.Tunion (x, x0)), ty2)
  | Csyntax.Tcomp_ptr x -> Add_default ((Csyntax.Tcomp_ptr x), ty2)

type classify_sub_cases =
| Sub_case_ii of AST.intsize * AST.signedness
| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
   * AST.signedness
| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
   * Csyntax.type0
| Sub_default of Csyntax.type0 * Csyntax.type0

(** val classify_sub_cases_rect_Type4 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7532 x_7531 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_rect_Type5 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7539 x_7538 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_rect_Type3 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7546 x_7545 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_rect_Type2 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7553 x_7552 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_rect_Type1 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7560 x_7559 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_rect_Type0 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7567 x_7566 = function
| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2

(** val classify_sub_cases_inv_rect_Type4 :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_sub_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_sub_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_sub_cases_inv_rect_Type3 :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_sub_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_sub_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_sub_cases_inv_rect_Type2 :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_sub_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_sub_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_sub_cases_inv_rect_Type1 :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_sub_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_sub_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_sub_cases_inv_rect_Type0 :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_sub_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
  let hcut = classify_sub_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
  hcut __ __ __

(** val classify_sub_cases_discr :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
    classify_sub_cases -> __ **)
let classify_sub_cases_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Sub_case_pi (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sub_case_pp (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_sub_cases_jmdiscr :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
    classify_sub_cases -> __ **)
let classify_sub_cases_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Sub_case_pi (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sub_case_pp (a0, a10, a20, a3) ->
       Obj.magic (fun _ dH -> dH __ __ __ __)
     | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_sub :
    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases **)
let classify_sub ty1 ty2 =
  match ty1 with
  | Csyntax.Tvoid -> Sub_default (Csyntax.Tvoid, ty2)
  | Csyntax.Tint (sz1, sg1) ->
    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Sub_case_ii
      (sz1, sg1)) (Sub_default ((Csyntax.Tint (sz1, sg1)), ty2))
  | Csyntax.Tpointer ty ->
    (match ty2 with
     | Csyntax.Tvoid -> Sub_default ((ptr_type ty Types.None), Csyntax.Tvoid)
     | Csyntax.Tint (sz, sg) -> Sub_case_pi (Types.None, ty, sz, sg)
     | Csyntax.Tpointer x -> Sub_case_pp (Types.None, Types.None, ty, x)
     | Csyntax.Tarray (x, n2) ->
       Sub_case_pp (Types.None, (Types.Some n2), ty, x)
     | Csyntax.Tfunction (x, x0) ->
       Sub_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
     | Csyntax.Tstruct (x, x0) ->
       Sub_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
     | Csyntax.Tunion (x, x0) ->
       Sub_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
     | Csyntax.Tcomp_ptr x ->
       Sub_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
  | Csyntax.Tarray (ty, n1) ->
    (match ty2 with
     | Csyntax.Tvoid ->
       Sub_default ((ptr_type ty (Types.Some n1)), Csyntax.Tvoid)
     | Csyntax.Tint (x, x0) -> Sub_case_pi ((Types.Some n1), ty, x, x0)
     | Csyntax.Tpointer x -> Sub_case_pp ((Types.Some n1), Types.None, ty, x)
     | Csyntax.Tarray (x, n2) ->
       Sub_case_pp ((Types.Some n1), (Types.Some n2), ty, x)
     | Csyntax.Tfunction (x, x0) ->
       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tfunction (x,
         x0)))
     | Csyntax.Tstruct (x, x0) ->
       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tstruct (x, x0)))
     | Csyntax.Tunion (x, x0) ->
       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tunion (x, x0)))
     | Csyntax.Tcomp_ptr x ->
       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tcomp_ptr x)))
  | Csyntax.Tfunction (x, x0) ->
    Sub_default ((Csyntax.Tfunction (x, x0)), ty2)
  | Csyntax.Tstruct (x, x0) -> Sub_default ((Csyntax.Tstruct (x, x0)), ty2)
  | Csyntax.Tunion (x, x0) -> Sub_default ((Csyntax.Tunion (x, x0)), ty2)
  | Csyntax.Tcomp_ptr x -> Sub_default ((Csyntax.Tcomp_ptr x), ty2)

type classify_aop_cases =
| Aop_case_ii of AST.intsize * AST.signedness
| Aop_default of Csyntax.type0 * Csyntax.type0

(** val classify_aop_cases_rect_Type4 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7621 x_7620 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_rect_Type5 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7626 x_7625 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_rect_Type3 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7631 x_7630 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_rect_Type2 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7636 x_7635 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_rect_Type1 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7641 x_7640 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_rect_Type0 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7646 x_7645 = function
| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
| Aop_default (ty, ty') -> h_aop_default ty ty'

(** val classify_aop_cases_inv_rect_Type4 :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_aop_cases_inv_rect_Type4 x1 x2 hterm h1 h2 =
  let hcut = classify_aop_cases_rect_Type4 h1 h2 x1 x2 hterm in hcut __ __ __

(** val classify_aop_cases_inv_rect_Type3 :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_aop_cases_inv_rect_Type3 x1 x2 hterm h1 h2 =
  let hcut = classify_aop_cases_rect_Type3 h1 h2 x1 x2 hterm in hcut __ __ __

(** val classify_aop_cases_inv_rect_Type2 :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_aop_cases_inv_rect_Type2 x1 x2 hterm h1 h2 =
  let hcut = classify_aop_cases_rect_Type2 h1 h2 x1 x2 hterm in hcut __ __ __

(** val classify_aop_cases_inv_rect_Type1 :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_aop_cases_inv_rect_Type1 x1 x2 hterm h1 h2 =
  let hcut = classify_aop_cases_rect_Type1 h1 h2 x1 x2 hterm in hcut __ __ __

(** val classify_aop_cases_inv_rect_Type0 :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_aop_cases_inv_rect_Type0 x1 x2 hterm h1 h2 =
  let hcut = classify_aop_cases_rect_Type0 h1 h2 x1 x2 hterm in hcut __ __ __

(** val classify_aop_cases_discr :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
    classify_aop_cases -> __ **)
let classify_aop_cases_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_aop_cases_jmdiscr :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
    classify_aop_cases -> __ **)
let classify_aop_cases_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_aop :
    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases **)
let classify_aop ty1 ty2 =
  match ty1 with
  | Csyntax.Tvoid -> Aop_default (Csyntax.Tvoid, ty2)
  | Csyntax.Tint (sz1, sg1) ->
    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Aop_case_ii
      (sz1, sg1)) (Aop_default ((Csyntax.Tint (sz1, sg1)), ty2))
  | Csyntax.Tpointer x -> Aop_default ((Csyntax.Tpointer x), ty2)
  | Csyntax.Tarray (x, x0) -> Aop_default ((Csyntax.Tarray (x, x0)), ty2)
  | Csyntax.Tfunction (x, x0) ->
    Aop_default ((Csyntax.Tfunction (x, x0)), ty2)
  | Csyntax.Tstruct (x, x0) -> Aop_default ((Csyntax.Tstruct (x, x0)), ty2)
  | Csyntax.Tunion (x, x0) -> Aop_default ((Csyntax.Tunion (x, x0)), ty2)
  | Csyntax.Tcomp_ptr x -> Aop_default ((Csyntax.Tcomp_ptr x), ty2)

type classify_cmp_cases =
| Cmp_case_ii of AST.intsize * AST.signedness
| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
| Cmp_default of Csyntax.type0 * Csyntax.type0

(** val classify_cmp_cases_rect_Type4 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7687 x_7686 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_rect_Type5 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7693 x_7692 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_rect_Type3 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7699 x_7698 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_rect_Type2 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7705 x_7704 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_rect_Type1 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7711 x_7710 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_rect_Type0 :
    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7717 x_7716 = function
| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
| Cmp_default (ty, ty') -> h_cmp_default ty ty'

(** val classify_cmp_cases_inv_rect_Type4 :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_cmp_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
  let hcut = classify_cmp_cases_rect_Type4 h1 h2 h3 x1 x2 hterm in
  hcut __ __ __

(** val classify_cmp_cases_inv_rect_Type3 :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_cmp_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
  let hcut = classify_cmp_cases_rect_Type3 h1 h2 h3 x1 x2 hterm in
  hcut __ __ __

(** val classify_cmp_cases_inv_rect_Type2 :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_cmp_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
  let hcut = classify_cmp_cases_rect_Type2 h1 h2 h3 x1 x2 hterm in
  hcut __ __ __

(** val classify_cmp_cases_inv_rect_Type1 :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_cmp_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
  let hcut = classify_cmp_cases_rect_Type1 h1 h2 h3 x1 x2 hterm in
  hcut __ __ __

(** val classify_cmp_cases_inv_rect_Type0 :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let classify_cmp_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
  let hcut = classify_cmp_cases_rect_Type0 h1 h2 h3 x1 x2 hterm in
  hcut __ __ __

(** val classify_cmp_cases_discr :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
    classify_cmp_cases -> __ **)
let classify_cmp_cases_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_cmp_cases_jmdiscr :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
    classify_cmp_cases -> __ **)
let classify_cmp_cases_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val classify_cmp :
    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases **)
let classify_cmp ty1 ty2 =
  match ty1 with
  | Csyntax.Tvoid -> Cmp_default (Csyntax.Tvoid, ty2)
  | Csyntax.Tint (sz1, sg1) ->
    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Cmp_case_ii
      (sz1, sg1)) (Cmp_default ((Csyntax.Tint (sz1, sg1)), ty2))
  | Csyntax.Tpointer ty1' ->
    TypeComparison.if_type_eq (Csyntax.Tpointer ty1') ty2 (Cmp_case_pp
      (Types.None, ty1')) (Cmp_default ((Csyntax.Tpointer ty1'), ty2))
  | Csyntax.Tarray (ty1', n1) ->
    TypeComparison.if_type_eq (Csyntax.Tarray (ty1', n1)) ty2 (Cmp_case_pp
      ((Types.Some n1), ty1')) (Cmp_default ((Csyntax.Tarray (ty1', n1)),
      ty2))
  | Csyntax.Tfunction (x, x0) ->
    Cmp_default ((Csyntax.Tfunction (x, x0)), ty2)
  | Csyntax.Tstruct (x, x0) -> Cmp_default ((Csyntax.Tstruct (x, x0)), ty2)
  | Csyntax.Tunion (x, x0) -> Cmp_default ((Csyntax.Tunion (x, x0)), ty2)
  | Csyntax.Tcomp_ptr x -> Cmp_default ((Csyntax.Tcomp_ptr x), ty2)

type classify_fun_cases =
| Fun_case_f of Csyntax.typelist * Csyntax.type0
| Fun_default

(** val classify_fun_cases_rect_Type4 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7765, x_7764) -> h_fun_case_f x_7765 x_7764
| Fun_default -> h_fun_default

(** val classify_fun_cases_rect_Type5 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7770, x_7769) -> h_fun_case_f x_7770 x_7769
| Fun_default -> h_fun_default

(** val classify_fun_cases_rect_Type3 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7775, x_7774) -> h_fun_case_f x_7775 x_7774
| Fun_default -> h_fun_default

(** val classify_fun_cases_rect_Type2 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7780, x_7779) -> h_fun_case_f x_7780 x_7779
| Fun_default -> h_fun_default

(** val classify_fun_cases_rect_Type1 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7785, x_7784) -> h_fun_case_f x_7785 x_7784
| Fun_default -> h_fun_default

(** val classify_fun_cases_rect_Type0 :
    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
    -> 'a1 **)
let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
| Fun_case_f (x_7790, x_7789) -> h_fun_case_f x_7790 x_7789
| Fun_default -> h_fun_default

(** val classify_fun_cases_inv_rect_Type4 :
    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let classify_fun_cases_inv_rect_Type4 hterm h1 h2 =
  let hcut = classify_fun_cases_rect_Type4 h1 h2 hterm in hcut __

(** val classify_fun_cases_inv_rect_Type3 :
    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let classify_fun_cases_inv_rect_Type3 hterm h1 h2 =
  let hcut = classify_fun_cases_rect_Type3 h1 h2 hterm in hcut __

(** val classify_fun_cases_inv_rect_Type2 :
    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let classify_fun_cases_inv_rect_Type2 hterm h1 h2 =
  let hcut = classify_fun_cases_rect_Type2 h1 h2 hterm in hcut __

(** val classify_fun_cases_inv_rect_Type1 :
    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let classify_fun_cases_inv_rect_Type1 hterm h1 h2 =
  let hcut = classify_fun_cases_rect_Type1 h1 h2 hterm in hcut __

(** val classify_fun_cases_inv_rect_Type0 :
    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let classify_fun_cases_inv_rect_Type0 hterm h1 h2 =
  let hcut = classify_fun_cases_rect_Type0 h1 h2 hterm in hcut __

(** val classify_fun_cases_discr :
    classify_fun_cases -> classify_fun_cases -> __ **)
let classify_fun_cases_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Fun_default -> Obj.magic (fun _ dH -> dH)) y

(** val classify_fun_cases_jmdiscr :
    classify_fun_cases -> classify_fun_cases -> __ **)
let classify_fun_cases_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Fun_default -> Obj.magic (fun _ dH -> dH)) y

(** val classify_fun : Csyntax.type0 -> classify_fun_cases **)
let classify_fun = function
| Csyntax.Tvoid -> Fun_default
| Csyntax.Tint (x, x0) -> Fun_default
| Csyntax.Tpointer ty' ->
  (match ty' with
   | Csyntax.Tvoid -> Fun_default
   | Csyntax.Tint (x, x0) -> Fun_default
   | Csyntax.Tpointer x -> Fun_default
   | Csyntax.Tarray (x, x0) -> Fun_default
   | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
   | Csyntax.Tstruct (x, x0) -> Fun_default
   | Csyntax.Tunion (x, x0) -> Fun_default
   | Csyntax.Tcomp_ptr x -> Fun_default)
| Csyntax.Tarray (x, x0) -> Fun_default
| Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
| Csyntax.Tstruct (x, x0) -> Fun_default
| Csyntax.Tunion (x, x0) -> Fun_default
| Csyntax.Tcomp_ptr x -> Fun_default