extracted/classifyOp.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 (** val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0 **)
  80 let ptr_type ty = function
  81 | Types.None -> Csyntax.Tpointer ty
  82 | Types.Some n' -> Csyntax.Tarray (ty, n')
  83
  84 type classify_add_cases =
  85 | Add_case_ii of AST.intsize * AST.signedness
  86 | Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
  87    * AST.signedness
  88 | Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
  89    * Csyntax.type0
  90 | Add_default of Csyntax.type0 * Csyntax.type0
  91
  92 (** val classify_add_cases_rect_Type4 :
  93     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  94     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  95     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  96     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  97     -> classify_add_cases -> 'a1 **)
  98 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
  99 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 100 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 101 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 102 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 103
 104 (** val classify_add_cases_rect_Type5 :
 105     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 106     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 107     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 108     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 109     -> classify_add_cases -> 'a1 **)
 110 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
 111 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 112 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 113 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 114 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 115
 116 (** val classify_add_cases_rect_Type3 :
 117     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 118     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 119     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 120     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 121     -> classify_add_cases -> 'a1 **)
 122 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
 123 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 124 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 125 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 126 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 127
 128 (** val classify_add_cases_rect_Type2 :
 129     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 130     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 131     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 132     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 133     -> classify_add_cases -> 'a1 **)
 134 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
 135 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 136 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 137 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 138 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 139
 140 (** val classify_add_cases_rect_Type1 :
 141     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 142     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 143     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 144     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 145     -> classify_add_cases -> 'a1 **)
 146 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
 147 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 148 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 149 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 150 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 151
 152 (** val classify_add_cases_rect_Type0 :
 153     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 154     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 155     Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 156     (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 157     -> classify_add_cases -> 'a1 **)
 158 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
 159 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
 160 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
 161 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
 162 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
 163
 164 (** val classify_add_cases_inv_rect_Type4 :
 165     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 166     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 167     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 168     -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
 169     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 170     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 171 let classify_add_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
 172   let hcut = classify_add_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
 173   hcut __ __ __
 174
 175 (** val classify_add_cases_inv_rect_Type3 :
 176     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 177     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 178     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 179     -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
 180     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 181     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 182 let classify_add_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
 183   let hcut = classify_add_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
 184   hcut __ __ __
 185
 186 (** val classify_add_cases_inv_rect_Type2 :
 187     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 188     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 189     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 190     -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
 191     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 192     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 193 let classify_add_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
 194   let hcut = classify_add_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
 195   hcut __ __ __
 196
 197 (** val classify_add_cases_inv_rect_Type1 :
 198     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 199     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 200     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 201     -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
 202     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 203     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 204 let classify_add_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
 205   let hcut = classify_add_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
 206   hcut __ __ __
 207
 208 (** val classify_add_cases_inv_rect_Type0 :
 209     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 210     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 211     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 212     -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
 213     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 214     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 215 let classify_add_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
 216   let hcut = classify_add_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
 217   hcut __ __ __
 218
 219 (** val classify_add_cases_discr :
 220     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
 221     classify_add_cases -> __ **)
 222 let classify_add_cases_discr a1 a2 x y =
 223   Logic.eq_rect_Type2 x
 224     (match x with
 225      | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 226      | Add_case_pi (a0, a10, a20, a3) ->
 227        Obj.magic (fun _ dH -> dH __ __ __ __)
 228      | Add_case_ip (a0, a10, a20, a3) ->
 229        Obj.magic (fun _ dH -> dH __ __ __ __)
 230      | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 231
 232 (** val classify_add_cases_jmdiscr :
 233     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
 234     classify_add_cases -> __ **)
 235 let classify_add_cases_jmdiscr a1 a2 x y =
 236   Logic.eq_rect_Type2 x
 237     (match x with
 238      | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 239      | Add_case_pi (a0, a10, a20, a3) ->
 240        Obj.magic (fun _ dH -> dH __ __ __ __)
 241      | Add_case_ip (a0, a10, a20, a3) ->
 242        Obj.magic (fun _ dH -> dH __ __ __ __)
 243      | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 244
 245 (** val classify_add :
 246     Csyntax.type0 -> Csyntax.type0 -> classify_add_cases **)
 247 let classify_add ty1 ty2 =
 248   match ty1 with
 249   | Csyntax.Tvoid -> Add_default (Csyntax.Tvoid, ty2)
 250   | Csyntax.Tint (sz1, sg1) ->
 251     (match ty2 with
 252      | Csyntax.Tvoid ->
 253        Add_default ((Csyntax.Tint (sz1, sg1)), Csyntax.Tvoid)
 254      | Csyntax.Tint (sz2, sg2) ->
 255        AST.inttyp_eq_elim' sz1 sz2 sg1 sg2 (Add_case_ii (sz1, sg1))
 256          (Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tint (sz2, sg2))))
 257      | Csyntax.Tpointer ty -> Add_case_ip (Types.None, sz1, sg1, ty)
 258      | Csyntax.Tarray (ty, n) -> Add_case_ip ((Types.Some n), sz1, sg1, ty)
 259      | Csyntax.Tfunction (x, x0) ->
 260        Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tfunction (x, x0)))
 261      | Csyntax.Tstruct (x, x0) ->
 262        Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tstruct (x, x0)))
 263      | Csyntax.Tunion (x, x0) ->
 264        Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tunion (x, x0)))
 265      | Csyntax.Tcomp_ptr x ->
 266        Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tcomp_ptr x)))
 267   | Csyntax.Tpointer ty ->
 268     (match ty2 with
 269      | Csyntax.Tvoid -> Add_default ((ptr_type ty Types.None), Csyntax.Tvoid)
 270      | Csyntax.Tint (x, x0) -> Add_case_pi (Types.None, ty, x, x0)
 271      | Csyntax.Tpointer x ->
 272        Add_default ((ptr_type ty Types.None), (Csyntax.Tpointer x))
 273      | Csyntax.Tarray (x, x0) ->
 274        Add_default ((ptr_type ty Types.None), (Csyntax.Tarray (x, x0)))
 275      | Csyntax.Tfunction (x, x0) ->
 276        Add_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
 277      | Csyntax.Tstruct (x, x0) ->
 278        Add_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
 279      | Csyntax.Tunion (x, x0) ->
 280        Add_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
 281      | Csyntax.Tcomp_ptr x ->
 282        Add_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
 283   | Csyntax.Tarray (ty, n) ->
 284     (match ty2 with
 285      | Csyntax.Tvoid ->
 286        Add_default ((ptr_type ty (Types.Some n)), Csyntax.Tvoid)
 287      | Csyntax.Tint (x, x0) -> Add_case_pi ((Types.Some n), ty, x, x0)
 288      | Csyntax.Tpointer x ->
 289        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tpointer x))
 290      | Csyntax.Tarray (x, x0) ->
 291        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tarray (x, x0)))
 292      | Csyntax.Tfunction (x, x0) ->
 293        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tfunction (x,
 294          x0)))
 295      | Csyntax.Tstruct (x, x0) ->
 296        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tstruct (x, x0)))
 297      | Csyntax.Tunion (x, x0) ->
 298        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tunion (x, x0)))
 299      | Csyntax.Tcomp_ptr x ->
 300        Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tcomp_ptr x)))
 301   | Csyntax.Tfunction (x, x0) ->
 302     Add_default ((Csyntax.Tfunction (x, x0)), ty2)
 303   | Csyntax.Tstruct (x, x0) -> Add_default ((Csyntax.Tstruct (x, x0)), ty2)
 304   | Csyntax.Tunion (x, x0) -> Add_default ((Csyntax.Tunion (x, x0)), ty2)
 305   | Csyntax.Tcomp_ptr x -> Add_default ((Csyntax.Tcomp_ptr x), ty2)
 306
 307 type classify_sub_cases =
 308 | Sub_case_ii of AST.intsize * AST.signedness
 309 | Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
 310    * AST.signedness
 311 | Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
 312    * Csyntax.type0
 313 | Sub_default of Csyntax.type0 * Csyntax.type0
 314
 315 (** val classify_sub_cases_rect_Type4 :
 316     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 317     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 318     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 319     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 320     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 321 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
 322 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 323 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 324 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 325 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 326
 327 (** val classify_sub_cases_rect_Type5 :
 328     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 329     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 330     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 331     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 332     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 333 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
 334 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 335 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 336 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 337 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 338
 339 (** val classify_sub_cases_rect_Type3 :
 340     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 341     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 342     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 343     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 344     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 345 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
 346 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 347 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 348 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 349 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 350
 351 (** val classify_sub_cases_rect_Type2 :
 352     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 353     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 354     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 355     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 356     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 357 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
 358 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 359 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 360 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 361 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 362
 363 (** val classify_sub_cases_rect_Type1 :
 364     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 365     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 366     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 367     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 368     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 369 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
 370 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 371 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 372 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 373 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 374
 375 (** val classify_sub_cases_rect_Type0 :
 376     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 377     Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 378     Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 379     'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 380     Csyntax.type0 -> classify_sub_cases -> 'a1 **)
 381 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
 382 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
 383 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
 384 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
 385 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
 386
 387 (** val classify_sub_cases_inv_rect_Type4 :
 388     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 389     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 390     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 391     -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 392     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 393     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 394 let classify_sub_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
 395   let hcut = classify_sub_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
 396   hcut __ __ __
 397
 398 (** val classify_sub_cases_inv_rect_Type3 :
 399     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 400     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 401     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 402     -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 403     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 404     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 405 let classify_sub_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
 406   let hcut = classify_sub_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
 407   hcut __ __ __
 408
 409 (** val classify_sub_cases_inv_rect_Type2 :
 410     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 411     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 412     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 413     -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 414     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 415     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 416 let classify_sub_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
 417   let hcut = classify_sub_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
 418   hcut __ __ __
 419
 420 (** val classify_sub_cases_inv_rect_Type1 :
 421     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 422     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 423     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 424     -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 425     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 426     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 427 let classify_sub_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
 428   let hcut = classify_sub_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
 429   hcut __ __ __
 430
 431 (** val classify_sub_cases_inv_rect_Type0 :
 432     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 433     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 434     Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
 435     -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 436     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 437     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 438 let classify_sub_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
 439   let hcut = classify_sub_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
 440   hcut __ __ __
 441
 442 (** val classify_sub_cases_discr :
 443     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
 444     classify_sub_cases -> __ **)
 445 let classify_sub_cases_discr a1 a2 x y =
 446   Logic.eq_rect_Type2 x
 447     (match x with
 448      | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 449      | Sub_case_pi (a0, a10, a20, a3) ->
 450        Obj.magic (fun _ dH -> dH __ __ __ __)
 451      | Sub_case_pp (a0, a10, a20, a3) ->
 452        Obj.magic (fun _ dH -> dH __ __ __ __)
 453      | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 454
 455 (** val classify_sub_cases_jmdiscr :
 456     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
 457     classify_sub_cases -> __ **)
 458 let classify_sub_cases_jmdiscr a1 a2 x y =
 459   Logic.eq_rect_Type2 x
 460     (match x with
 461      | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 462      | Sub_case_pi (a0, a10, a20, a3) ->
 463        Obj.magic (fun _ dH -> dH __ __ __ __)
 464      | Sub_case_pp (a0, a10, a20, a3) ->
 465        Obj.magic (fun _ dH -> dH __ __ __ __)
 466      | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 467
 468 (** val classify_sub :
 469     Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases **)
 470 let classify_sub ty1 ty2 =
 471   match ty1 with
 472   | Csyntax.Tvoid -> Sub_default (Csyntax.Tvoid, ty2)
 473   | Csyntax.Tint (sz1, sg1) ->
 474     TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Sub_case_ii
 475       (sz1, sg1)) (Sub_default ((Csyntax.Tint (sz1, sg1)), ty2))
 476   | Csyntax.Tpointer ty ->
 477     (match ty2 with
 478      | Csyntax.Tvoid -> Sub_default ((ptr_type ty Types.None), Csyntax.Tvoid)
 479      | Csyntax.Tint (sz, sg) -> Sub_case_pi (Types.None, ty, sz, sg)
 480      | Csyntax.Tpointer x -> Sub_case_pp (Types.None, Types.None, ty, x)
 481      | Csyntax.Tarray (x, n2) ->
 482        Sub_case_pp (Types.None, (Types.Some n2), ty, x)
 483      | Csyntax.Tfunction (x, x0) ->
 484        Sub_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
 485      | Csyntax.Tstruct (x, x0) ->
 486        Sub_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
 487      | Csyntax.Tunion (x, x0) ->
 488        Sub_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
 489      | Csyntax.Tcomp_ptr x ->
 490        Sub_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
 491   | Csyntax.Tarray (ty, n1) ->
 492     (match ty2 with
 493      | Csyntax.Tvoid ->
 494        Sub_default ((ptr_type ty (Types.Some n1)), Csyntax.Tvoid)
 495      | Csyntax.Tint (x, x0) -> Sub_case_pi ((Types.Some n1), ty, x, x0)
 496      | Csyntax.Tpointer x -> Sub_case_pp ((Types.Some n1), Types.None, ty, x)
 497      | Csyntax.Tarray (x, n2) ->
 498        Sub_case_pp ((Types.Some n1), (Types.Some n2), ty, x)
 499      | Csyntax.Tfunction (x, x0) ->
 500        Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tfunction (x,
 501          x0)))
 502      | Csyntax.Tstruct (x, x0) ->
 503        Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tstruct (x, x0)))
 504      | Csyntax.Tunion (x, x0) ->
 505        Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tunion (x, x0)))
 506      | Csyntax.Tcomp_ptr x ->
 507        Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tcomp_ptr x)))
 508   | Csyntax.Tfunction (x, x0) ->
 509     Sub_default ((Csyntax.Tfunction (x, x0)), ty2)
 510   | Csyntax.Tstruct (x, x0) -> Sub_default ((Csyntax.Tstruct (x, x0)), ty2)
 511   | Csyntax.Tunion (x, x0) -> Sub_default ((Csyntax.Tunion (x, x0)), ty2)
 512   | Csyntax.Tcomp_ptr x -> Sub_default ((Csyntax.Tcomp_ptr x), ty2)
 513
 514 type classify_aop_cases =
 515 | Aop_case_ii of AST.intsize * AST.signedness
 516 | Aop_default of Csyntax.type0 * Csyntax.type0
 517
 518 (** val classify_aop_cases_rect_Type4 :
 519     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 520     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 521 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7621 x_7620 = function
 522 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 523 | Aop_default (ty, ty') -> h_aop_default ty ty'
 524
 525 (** val classify_aop_cases_rect_Type5 :
 526     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 527     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 528 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7626 x_7625 = function
 529 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 530 | Aop_default (ty, ty') -> h_aop_default ty ty'
 531
 532 (** val classify_aop_cases_rect_Type3 :
 533     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 534     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 535 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7631 x_7630 = function
 536 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 537 | Aop_default (ty, ty') -> h_aop_default ty ty'
 538
 539 (** val classify_aop_cases_rect_Type2 :
 540     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 541     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 542 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7636 x_7635 = function
 543 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 544 | Aop_default (ty, ty') -> h_aop_default ty ty'
 545
 546 (** val classify_aop_cases_rect_Type1 :
 547     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 548     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 549 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7641 x_7640 = function
 550 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 551 | Aop_default (ty, ty') -> h_aop_default ty ty'
 552
 553 (** val classify_aop_cases_rect_Type0 :
 554     (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 555     -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
 556 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7646 x_7645 = function
 557 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
 558 | Aop_default (ty, ty') -> h_aop_default ty ty'
 559
 560 (** val classify_aop_cases_inv_rect_Type4 :
 561     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 562     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 563     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 564 let classify_aop_cases_inv_rect_Type4 x1 x2 hterm h1 h2 =
 565   let hcut = classify_aop_cases_rect_Type4 h1 h2 x1 x2 hterm in hcut __ __ __
 566
 567 (** val classify_aop_cases_inv_rect_Type3 :
 568     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 569     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 570     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 571 let classify_aop_cases_inv_rect_Type3 x1 x2 hterm h1 h2 =
 572   let hcut = classify_aop_cases_rect_Type3 h1 h2 x1 x2 hterm in hcut __ __ __
 573
 574 (** val classify_aop_cases_inv_rect_Type2 :
 575     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 576     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 577     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 578 let classify_aop_cases_inv_rect_Type2 x1 x2 hterm h1 h2 =
 579   let hcut = classify_aop_cases_rect_Type2 h1 h2 x1 x2 hterm in hcut __ __ __
 580
 581 (** val classify_aop_cases_inv_rect_Type1 :
 582     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 583     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 584     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 585 let classify_aop_cases_inv_rect_Type1 x1 x2 hterm h1 h2 =
 586   let hcut = classify_aop_cases_rect_Type1 h1 h2 x1 x2 hterm in hcut __ __ __
 587
 588 (** val classify_aop_cases_inv_rect_Type0 :
 589     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 590     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 591     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 592 let classify_aop_cases_inv_rect_Type0 x1 x2 hterm h1 h2 =
 593   let hcut = classify_aop_cases_rect_Type0 h1 h2 x1 x2 hterm in hcut __ __ __
 594
 595 (** val classify_aop_cases_discr :
 596     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
 597     classify_aop_cases -> __ **)
 598 let classify_aop_cases_discr a1 a2 x y =
 599   Logic.eq_rect_Type2 x
 600     (match x with
 601      | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 602      | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 603
 604 (** val classify_aop_cases_jmdiscr :
 605     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
 606     classify_aop_cases -> __ **)
 607 let classify_aop_cases_jmdiscr a1 a2 x y =
 608   Logic.eq_rect_Type2 x
 609     (match x with
 610      | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 611      | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 612
 613 (** val classify_aop :
 614     Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases **)
 615 let classify_aop ty1 ty2 =
 616   match ty1 with
 617   | Csyntax.Tvoid -> Aop_default (Csyntax.Tvoid, ty2)
 618   | Csyntax.Tint (sz1, sg1) ->
 619     TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Aop_case_ii
 620       (sz1, sg1)) (Aop_default ((Csyntax.Tint (sz1, sg1)), ty2))
 621   | Csyntax.Tpointer x -> Aop_default ((Csyntax.Tpointer x), ty2)
 622   | Csyntax.Tarray (x, x0) -> Aop_default ((Csyntax.Tarray (x, x0)), ty2)
 623   | Csyntax.Tfunction (x, x0) ->
 624     Aop_default ((Csyntax.Tfunction (x, x0)), ty2)
 625   | Csyntax.Tstruct (x, x0) -> Aop_default ((Csyntax.Tstruct (x, x0)), ty2)
 626   | Csyntax.Tunion (x, x0) -> Aop_default ((Csyntax.Tunion (x, x0)), ty2)
 627   | Csyntax.Tcomp_ptr x -> Aop_default ((Csyntax.Tcomp_ptr x), ty2)
 628
 629 type classify_cmp_cases =
 630 | Cmp_case_ii of AST.intsize * AST.signedness
 631 | Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
 632 | Cmp_default of Csyntax.type0 * Csyntax.type0
 633
 634 (** val classify_cmp_cases_rect_Type4 :
 635     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 636     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 637     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 638 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7687 x_7686 = function
 639 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 640 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 641 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 642
 643 (** val classify_cmp_cases_rect_Type5 :
 644     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 645     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 646     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 647 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7693 x_7692 = function
 648 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 649 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 650 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 651
 652 (** val classify_cmp_cases_rect_Type3 :
 653     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 654     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 655     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 656 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7699 x_7698 = function
 657 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 658 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 659 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 660
 661 (** val classify_cmp_cases_rect_Type2 :
 662     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 663     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 664     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 665 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7705 x_7704 = function
 666 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 667 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 668 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 669
 670 (** val classify_cmp_cases_rect_Type1 :
 671     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 672     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 673     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 674 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7711 x_7710 = function
 675 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 676 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 677 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 678
 679 (** val classify_cmp_cases_rect_Type0 :
 680     (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 681     Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 682     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
 683 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7717 x_7716 = function
 684 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
 685 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
 686 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
 687
 688 (** val classify_cmp_cases_inv_rect_Type4 :
 689     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 690     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 691     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 692     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 693 let classify_cmp_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
 694   let hcut = classify_cmp_cases_rect_Type4 h1 h2 h3 x1 x2 hterm in
 695   hcut __ __ __
 696
 697 (** val classify_cmp_cases_inv_rect_Type3 :
 698     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 699     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 700     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 701     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 702 let classify_cmp_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
 703   let hcut = classify_cmp_cases_rect_Type3 h1 h2 h3 x1 x2 hterm in
 704   hcut __ __ __
 705
 706 (** val classify_cmp_cases_inv_rect_Type2 :
 707     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 708     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 709     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 710     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 711 let classify_cmp_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
 712   let hcut = classify_cmp_cases_rect_Type2 h1 h2 h3 x1 x2 hterm in
 713   hcut __ __ __
 714
 715 (** val classify_cmp_cases_inv_rect_Type1 :
 716     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 717     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 718     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 719     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 720 let classify_cmp_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
 721   let hcut = classify_cmp_cases_rect_Type1 h1 h2 h3 x1 x2 hterm in
 722   hcut __ __ __
 723
 724 (** val classify_cmp_cases_inv_rect_Type0 :
 725     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 726     AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 727     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
 728     Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 729 let classify_cmp_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
 730   let hcut = classify_cmp_cases_rect_Type0 h1 h2 h3 x1 x2 hterm in
 731   hcut __ __ __
 732
 733 (** val classify_cmp_cases_discr :
 734     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
 735     classify_cmp_cases -> __ **)
 736 let classify_cmp_cases_discr a1 a2 x y =
 737   Logic.eq_rect_Type2 x
 738     (match x with
 739      | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 740      | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 741      | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 742
 743 (** val classify_cmp_cases_jmdiscr :
 744     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
 745     classify_cmp_cases -> __ **)
 746 let classify_cmp_cases_jmdiscr a1 a2 x y =
 747   Logic.eq_rect_Type2 x
 748     (match x with
 749      | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 750      | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 751      | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 752
 753 (** val classify_cmp :
 754     Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases **)
 755 let classify_cmp ty1 ty2 =
 756   match ty1 with
 757   | Csyntax.Tvoid -> Cmp_default (Csyntax.Tvoid, ty2)
 758   | Csyntax.Tint (sz1, sg1) ->
 759     TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Cmp_case_ii
 760       (sz1, sg1)) (Cmp_default ((Csyntax.Tint (sz1, sg1)), ty2))
 761   | Csyntax.Tpointer ty1' ->
 762     TypeComparison.if_type_eq (Csyntax.Tpointer ty1') ty2 (Cmp_case_pp
 763       (Types.None, ty1')) (Cmp_default ((Csyntax.Tpointer ty1'), ty2))
 764   | Csyntax.Tarray (ty1', n1) ->
 765     TypeComparison.if_type_eq (Csyntax.Tarray (ty1', n1)) ty2 (Cmp_case_pp
 766       ((Types.Some n1), ty1')) (Cmp_default ((Csyntax.Tarray (ty1', n1)),
 767       ty2))
 768   | Csyntax.Tfunction (x, x0) ->
 769     Cmp_default ((Csyntax.Tfunction (x, x0)), ty2)
 770   | Csyntax.Tstruct (x, x0) -> Cmp_default ((Csyntax.Tstruct (x, x0)), ty2)
 771   | Csyntax.Tunion (x, x0) -> Cmp_default ((Csyntax.Tunion (x, x0)), ty2)
 772   | Csyntax.Tcomp_ptr x -> Cmp_default ((Csyntax.Tcomp_ptr x), ty2)
 773
 774 type classify_fun_cases =
 775 | Fun_case_f of Csyntax.typelist * Csyntax.type0
 776 | Fun_default
 777
 778 (** val classify_fun_cases_rect_Type4 :
 779     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 780     -> 'a1 **)
 781 let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
 782 | Fun_case_f (x_7765, x_7764) -> h_fun_case_f x_7765 x_7764
 783 | Fun_default -> h_fun_default
 784
 785 (** val classify_fun_cases_rect_Type5 :
 786     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 787     -> 'a1 **)
 788 let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
 789 | Fun_case_f (x_7770, x_7769) -> h_fun_case_f x_7770 x_7769
 790 | Fun_default -> h_fun_default
 791
 792 (** val classify_fun_cases_rect_Type3 :
 793     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 794     -> 'a1 **)
 795 let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
 796 | Fun_case_f (x_7775, x_7774) -> h_fun_case_f x_7775 x_7774
 797 | Fun_default -> h_fun_default
 798
 799 (** val classify_fun_cases_rect_Type2 :
 800     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 801     -> 'a1 **)
 802 let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
 803 | Fun_case_f (x_7780, x_7779) -> h_fun_case_f x_7780 x_7779
 804 | Fun_default -> h_fun_default
 805
 806 (** val classify_fun_cases_rect_Type1 :
 807     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 808     -> 'a1 **)
 809 let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
 810 | Fun_case_f (x_7785, x_7784) -> h_fun_case_f x_7785 x_7784
 811 | Fun_default -> h_fun_default
 812
 813 (** val classify_fun_cases_rect_Type0 :
 814     (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
 815     -> 'a1 **)
 816 let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
 817 | Fun_case_f (x_7790, x_7789) -> h_fun_case_f x_7790 x_7789
 818 | Fun_default -> h_fun_default
 819
 820 (** val classify_fun_cases_inv_rect_Type4 :
 821     classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 822     (__ -> 'a1) -> 'a1 **)
 823 let classify_fun_cases_inv_rect_Type4 hterm h1 h2 =
 824   let hcut = classify_fun_cases_rect_Type4 h1 h2 hterm in hcut __
 825
 826 (** val classify_fun_cases_inv_rect_Type3 :
 827     classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 828     (__ -> 'a1) -> 'a1 **)
 829 let classify_fun_cases_inv_rect_Type3 hterm h1 h2 =
 830   let hcut = classify_fun_cases_rect_Type3 h1 h2 hterm in hcut __
 831
 832 (** val classify_fun_cases_inv_rect_Type2 :
 833     classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 834     (__ -> 'a1) -> 'a1 **)
 835 let classify_fun_cases_inv_rect_Type2 hterm h1 h2 =
 836   let hcut = classify_fun_cases_rect_Type2 h1 h2 hterm in hcut __
 837
 838 (** val classify_fun_cases_inv_rect_Type1 :
 839     classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 840     (__ -> 'a1) -> 'a1 **)
 841 let classify_fun_cases_inv_rect_Type1 hterm h1 h2 =
 842   let hcut = classify_fun_cases_rect_Type1 h1 h2 hterm in hcut __
 843
 844 (** val classify_fun_cases_inv_rect_Type0 :
 845     classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 846     (__ -> 'a1) -> 'a1 **)
 847 let classify_fun_cases_inv_rect_Type0 hterm h1 h2 =
 848   let hcut = classify_fun_cases_rect_Type0 h1 h2 hterm in hcut __
 849
 850 (** val classify_fun_cases_discr :
 851     classify_fun_cases -> classify_fun_cases -> __ **)
 852 let classify_fun_cases_discr x y =
 853   Logic.eq_rect_Type2 x
 854     (match x with
 855      | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 856      | Fun_default -> Obj.magic (fun _ dH -> dH)) y
 857
 858 (** val classify_fun_cases_jmdiscr :
 859     classify_fun_cases -> classify_fun_cases -> __ **)
 860 let classify_fun_cases_jmdiscr x y =
 861   Logic.eq_rect_Type2 x
 862     (match x with
 863      | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 864      | Fun_default -> Obj.magic (fun _ dH -> dH)) y
 865
 866 (** val classify_fun : Csyntax.type0 -> classify_fun_cases **)
 867 let classify_fun = function
 868 | Csyntax.Tvoid -> Fun_default
 869 | Csyntax.Tint (x, x0) -> Fun_default
 870 | Csyntax.Tpointer ty' ->
 871   (match ty' with
 872    | Csyntax.Tvoid -> Fun_default
 873    | Csyntax.Tint (x, x0) -> Fun_default
 874    | Csyntax.Tpointer x -> Fun_default
 875    | Csyntax.Tarray (x, x0) -> Fun_default
 876    | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
 877    | Csyntax.Tstruct (x, x0) -> Fun_default
 878    | Csyntax.Tunion (x, x0) -> Fun_default
 879    | Csyntax.Tcomp_ptr x -> Fun_default)
 880 | Csyntax.Tarray (x, x0) -> Fun_default
 881 | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
 882 | Csyntax.Tstruct (x, x0) -> Fun_default
 883 | Csyntax.Tunion (x, x0) -> Fun_default
 884 | Csyntax.Tcomp_ptr x -> Fun_default
 885