extracted/cminor_syntax.ml

   1 open Preamble
   2
   3 open FrontEndVal
   4
   5 open Hide
   6
   7 open ByteValues
   8
   9 open GenMem
  10
  11 open FrontEndMem
  12
  13 open Proper
  14
  15 open PositiveMap
  16
  17 open Deqsets
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Identifiers
  24
  25 open Integers
  26
  27 open AST
  28
  29 open Division
  30
  31 open Exp
  32
  33 open Arithmetic
  34
  35 open Extranat
  36
  37 open Vector
  38
  39 open FoldStuff
  40
  41 open BitVector
  42
  43 open Z
  44
  45 open BitVectorZ
  46
  47 open Pointers
  48
  49 open ErrorMessages
  50
  51 open Option
  52
  53 open Setoids
  54
  55 open Monad
  56
  57 open Positive
  58
  59 open PreIdentifiers
  60
  61 open Errors
  62
  63 open Div_and_mod
  64
  65 open Jmeq
  66
  67 open Russell
  68
  69 open Util
  70
  71 open Bool
  72
  73 open Relations
  74
  75 open Nat
  76
  77 open List
  78
  79 open Hints_declaration
  80
  81 open Core_notation
  82
  83 open Pts
  84
  85 open Logic
  86
  87 open Types
  88
  89 open Coqlib
  90
  91 open Values
  92
  93 open FrontEndOps
  94
  95 open CostLabel
  96
  97 type expr =
  98 | Id of AST.typ * AST.ident
  99 | Cst of AST.typ * FrontEndOps.constant
 100 | Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
 101 | Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation *
 102    expr * expr
 103 | Mem of AST.typ * expr
 104 | Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
 105 | Ecost of AST.typ * CostLabel.costlabel * expr
 106
 107 (** val expr_rect_Type4 :
 108     (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 109     -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 110     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 111     expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 112     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
 113     -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
 114     -> 'a1) -> AST.typ -> expr -> 'a1 **)
 115 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13742 = function
 116 | Id (t, x_13744) -> h_Id t x_13744
 117 | Cst (t, x_13745) -> h_Cst t x_13745
 118 | Op1 (t, t', x_13747, x_13746) ->
 119   h_Op1 t t' x_13747 x_13746
 120     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13746)
 121 | Op2 (t1, t2, t', x_13750, x_13749, x_13748) ->
 122   h_Op2 t1 t2 t' x_13750 x_13749 x_13748
 123     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13749)
 124     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13748)
 125 | Mem (t, x_13751) ->
 126   h_Mem t x_13751
 127     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
 128       x_13751)
 129 | Cond (sz, sg, t, x_13754, x_13753, x_13752) ->
 130   h_Cond sz sg t x_13754 x_13753 x_13752
 131     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
 132       (sz, sg)) x_13754)
 133     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13753)
 134     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13752)
 135 | Ecost (t, x_13756, x_13755) ->
 136   h_Ecost t x_13756 x_13755
 137     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13755)
 138
 139 (** val expr_rect_Type3 :
 140     (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 141     -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 142     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 143     expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 144     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
 145     -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
 146     -> 'a1) -> AST.typ -> expr -> 'a1 **)
 147 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13786 = function
 148 | Id (t, x_13788) -> h_Id t x_13788
 149 | Cst (t, x_13789) -> h_Cst t x_13789
 150 | Op1 (t, t', x_13791, x_13790) ->
 151   h_Op1 t t' x_13791 x_13790
 152     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13790)
 153 | Op2 (t1, t2, t', x_13794, x_13793, x_13792) ->
 154   h_Op2 t1 t2 t' x_13794 x_13793 x_13792
 155     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13793)
 156     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13792)
 157 | Mem (t, x_13795) ->
 158   h_Mem t x_13795
 159     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
 160       x_13795)
 161 | Cond (sz, sg, t, x_13798, x_13797, x_13796) ->
 162   h_Cond sz sg t x_13798 x_13797 x_13796
 163     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
 164       (sz, sg)) x_13798)
 165     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13797)
 166     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13796)
 167 | Ecost (t, x_13800, x_13799) ->
 168   h_Ecost t x_13800 x_13799
 169     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13799)
 170
 171 (** val expr_rect_Type2 :
 172     (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 173     -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 174     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 175     expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 176     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
 177     -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
 178     -> 'a1) -> AST.typ -> expr -> 'a1 **)
 179 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13808 = function
 180 | Id (t, x_13810) -> h_Id t x_13810
 181 | Cst (t, x_13811) -> h_Cst t x_13811
 182 | Op1 (t, t', x_13813, x_13812) ->
 183   h_Op1 t t' x_13813 x_13812
 184     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13812)
 185 | Op2 (t1, t2, t', x_13816, x_13815, x_13814) ->
 186   h_Op2 t1 t2 t' x_13816 x_13815 x_13814
 187     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13815)
 188     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13814)
 189 | Mem (t, x_13817) ->
 190   h_Mem t x_13817
 191     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
 192       x_13817)
 193 | Cond (sz, sg, t, x_13820, x_13819, x_13818) ->
 194   h_Cond sz sg t x_13820 x_13819 x_13818
 195     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
 196       (sz, sg)) x_13820)
 197     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13819)
 198     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13818)
 199 | Ecost (t, x_13822, x_13821) ->
 200   h_Ecost t x_13822 x_13821
 201     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13821)
 202
 203 (** val expr_rect_Type1 :
 204     (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 205     -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 206     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 207     expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 208     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
 209     -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
 210     -> 'a1) -> AST.typ -> expr -> 'a1 **)
 211 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13830 = function
 212 | Id (t, x_13832) -> h_Id t x_13832
 213 | Cst (t, x_13833) -> h_Cst t x_13833
 214 | Op1 (t, t', x_13835, x_13834) ->
 215   h_Op1 t t' x_13835 x_13834
 216     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13834)
 217 | Op2 (t1, t2, t', x_13838, x_13837, x_13836) ->
 218   h_Op2 t1 t2 t' x_13838 x_13837 x_13836
 219     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13837)
 220     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13836)
 221 | Mem (t, x_13839) ->
 222   h_Mem t x_13839
 223     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
 224       x_13839)
 225 | Cond (sz, sg, t, x_13842, x_13841, x_13840) ->
 226   h_Cond sz sg t x_13842 x_13841 x_13840
 227     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
 228       (sz, sg)) x_13842)
 229     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13841)
 230     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13840)
 231 | Ecost (t, x_13844, x_13843) ->
 232   h_Ecost t x_13844 x_13843
 233     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13843)
 234
 235 (** val expr_rect_Type0 :
 236     (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 237     -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 238     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 239     expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 240     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
 241     -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
 242     -> 'a1) -> AST.typ -> expr -> 'a1 **)
 243 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13852 = function
 244 | Id (t, x_13854) -> h_Id t x_13854
 245 | Cst (t, x_13855) -> h_Cst t x_13855
 246 | Op1 (t, t', x_13857, x_13856) ->
 247   h_Op1 t t' x_13857 x_13856
 248     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13856)
 249 | Op2 (t1, t2, t', x_13860, x_13859, x_13858) ->
 250   h_Op2 t1 t2 t' x_13860 x_13859 x_13858
 251     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13859)
 252     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13858)
 253 | Mem (t, x_13861) ->
 254   h_Mem t x_13861
 255     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
 256       x_13861)
 257 | Cond (sz, sg, t, x_13864, x_13863, x_13862) ->
 258   h_Cond sz sg t x_13864 x_13863 x_13862
 259     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
 260       (sz, sg)) x_13864)
 261     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13863)
 262     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13862)
 263 | Ecost (t, x_13866, x_13865) ->
 264   h_Ecost t x_13866 x_13865
 265     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13865)
 266
 267 (** val expr_inv_rect_Type4 :
 268     AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
 269     -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 270     FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 271     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 272     expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 273     'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 274     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
 275     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 276     'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
 277     __ -> __ -> 'a1) -> 'a1 **)
 278 let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
 279   let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
 280
 281 (** val expr_inv_rect_Type3 :
 282     AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
 283     -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 284     FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 285     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 286     expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 287     'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 288     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
 289     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 290     'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
 291     __ -> __ -> 'a1) -> 'a1 **)
 292 let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
 293   let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
 294
 295 (** val expr_inv_rect_Type2 :
 296     AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
 297     -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 298     FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 299     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 300     expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 301     'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 302     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
 303     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 304     'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
 305     __ -> __ -> 'a1) -> 'a1 **)
 306 let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
 307   let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
 308
 309 (** val expr_inv_rect_Type1 :
 310     AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
 311     -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 312     FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 313     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 314     expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 315     'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 316     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
 317     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 318     'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
 319     __ -> __ -> 'a1) -> 'a1 **)
 320 let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
 321   let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
 322
 323 (** val expr_inv_rect_Type0 :
 324     AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
 325     -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 326     FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 327     'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 328     expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 329     'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 330     (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
 331     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
 332     'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
 333     __ -> __ -> 'a1) -> 'a1 **)
 334 let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
 335   let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
 336
 337 (** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
 338 let expr_jmdiscr a1 x y =
 339   Logic.eq_rect_Type2 x
 340     (match x with
 341      | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 342      | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 343      | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 344      | Op2 (a0, a10, a2, a3, a4, a5) ->
 345        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
 346      | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 347      | Cond (a0, a10, a2, a3, a4, a5) ->
 348        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
 349      | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 350
 351 type stmt =
 352 | St_skip
 353 | St_assign of AST.typ * AST.ident * expr
 354 | St_store of AST.typ * expr * expr
 355 | St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
 356    * (AST.typ, expr) Types.dPair List.list
 357 | St_seq of stmt * stmt
 358 | St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
 359 | St_return of (AST.typ, expr) Types.dPair Types.option
 360 | St_label of PreIdentifiers.identifier * stmt
 361 | St_goto of PreIdentifiers.identifier
 362 | St_cost of CostLabel.costlabel * stmt
 363
 364 (** val stmt_rect_Type4 :
 365     'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
 366     -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
 367     (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
 368     'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
 369     'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
 370     -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 371     (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 372     -> 'a1) -> stmt -> 'a1 **)
 373 let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
 374 | St_skip -> h_St_skip
 375 | St_assign (t, x_14037, x_14036) -> h_St_assign t x_14037 x_14036
 376 | St_store (t, x_14039, x_14038) -> h_St_store t x_14039 x_14038
 377 | St_call (x_14042, x_14041, x_14040) -> h_St_call x_14042 x_14041 x_14040
 378 | St_seq (x_14044, x_14043) ->
 379   h_St_seq x_14044 x_14043
 380     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 381       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14044)
 382     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 383       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043)
 384 | St_ifthenelse (sz, sg, x_14047, x_14046, x_14045) ->
 385   h_St_ifthenelse sz sg x_14047 x_14046 x_14045
 386     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 387       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046)
 388     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 389       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14045)
 390 | St_return x_14048 -> h_St_return x_14048
 391 | St_label (x_14050, x_14049) ->
 392   h_St_label x_14050 x_14049
 393     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 394       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
 395 | St_goto x_14051 -> h_St_goto x_14051
 396 | St_cost (x_14053, x_14052) ->
 397   h_St_cost x_14053 x_14052
 398     (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 399       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14052)
 400
 401 (** val stmt_rect_Type3 :
 402     'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
 403     -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
 404     (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
 405     'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
 406     'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
 407     -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 408     (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 409     -> 'a1) -> stmt -> 'a1 **)
 410 let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
 411 | St_skip -> h_St_skip
 412 | St_assign (t, x_14095, x_14094) -> h_St_assign t x_14095 x_14094
 413 | St_store (t, x_14097, x_14096) -> h_St_store t x_14097 x_14096
 414 | St_call (x_14100, x_14099, x_14098) -> h_St_call x_14100 x_14099 x_14098
 415 | St_seq (x_14102, x_14101) ->
 416   h_St_seq x_14102 x_14101
 417     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 418       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14102)
 419     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 420       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
 421 | St_ifthenelse (sz, sg, x_14105, x_14104, x_14103) ->
 422   h_St_ifthenelse sz sg x_14105 x_14104 x_14103
 423     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 424       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104)
 425     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 426       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14103)
 427 | St_return x_14106 -> h_St_return x_14106
 428 | St_label (x_14108, x_14107) ->
 429   h_St_label x_14108 x_14107
 430     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 431       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107)
 432 | St_goto x_14109 -> h_St_goto x_14109
 433 | St_cost (x_14111, x_14110) ->
 434   h_St_cost x_14111 x_14110
 435     (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 436       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14110)
 437
 438 (** val stmt_rect_Type2 :
 439     'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
 440     -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
 441     (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
 442     'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
 443     'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
 444     -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 445     (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 446     -> 'a1) -> stmt -> 'a1 **)
 447 let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
 448 | St_skip -> h_St_skip
 449 | St_assign (t, x_14124, x_14123) -> h_St_assign t x_14124 x_14123
 450 | St_store (t, x_14126, x_14125) -> h_St_store t x_14126 x_14125
 451 | St_call (x_14129, x_14128, x_14127) -> h_St_call x_14129 x_14128 x_14127
 452 | St_seq (x_14131, x_14130) ->
 453   h_St_seq x_14131 x_14130
 454     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 455       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14131)
 456     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 457       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
 458 | St_ifthenelse (sz, sg, x_14134, x_14133, x_14132) ->
 459   h_St_ifthenelse sz sg x_14134 x_14133 x_14132
 460     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 461       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133)
 462     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 463       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14132)
 464 | St_return x_14135 -> h_St_return x_14135
 465 | St_label (x_14137, x_14136) ->
 466   h_St_label x_14137 x_14136
 467     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 468       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136)
 469 | St_goto x_14138 -> h_St_goto x_14138
 470 | St_cost (x_14140, x_14139) ->
 471   h_St_cost x_14140 x_14139
 472     (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 473       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14139)
 474
 475 (** val stmt_rect_Type1 :
 476     'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
 477     -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
 478     (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
 479     'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
 480     'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
 481     -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 482     (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 483     -> 'a1) -> stmt -> 'a1 **)
 484 let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
 485 | St_skip -> h_St_skip
 486 | St_assign (t, x_14153, x_14152) -> h_St_assign t x_14153 x_14152
 487 | St_store (t, x_14155, x_14154) -> h_St_store t x_14155 x_14154
 488 | St_call (x_14158, x_14157, x_14156) -> h_St_call x_14158 x_14157 x_14156
 489 | St_seq (x_14160, x_14159) ->
 490   h_St_seq x_14160 x_14159
 491     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 492       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14160)
 493     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 494       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14159)
 495 | St_ifthenelse (sz, sg, x_14163, x_14162, x_14161) ->
 496   h_St_ifthenelse sz sg x_14163 x_14162 x_14161
 497     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 498       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14162)
 499     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 500       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14161)
 501 | St_return x_14164 -> h_St_return x_14164
 502 | St_label (x_14166, x_14165) ->
 503   h_St_label x_14166 x_14165
 504     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 505       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14165)
 506 | St_goto x_14167 -> h_St_goto x_14167
 507 | St_cost (x_14169, x_14168) ->
 508   h_St_cost x_14169 x_14168
 509     (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 510       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14168)
 511
 512 (** val stmt_rect_Type0 :
 513     'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
 514     -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
 515     (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
 516     'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
 517     'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
 518     -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 519     (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 520     -> 'a1) -> stmt -> 'a1 **)
 521 let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
 522 | St_skip -> h_St_skip
 523 | St_assign (t, x_14182, x_14181) -> h_St_assign t x_14182 x_14181
 524 | St_store (t, x_14184, x_14183) -> h_St_store t x_14184 x_14183
 525 | St_call (x_14187, x_14186, x_14185) -> h_St_call x_14187 x_14186 x_14185
 526 | St_seq (x_14189, x_14188) ->
 527   h_St_seq x_14189 x_14188
 528     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 529       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14189)
 530     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 531       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14188)
 532 | St_ifthenelse (sz, sg, x_14192, x_14191, x_14190) ->
 533   h_St_ifthenelse sz sg x_14192 x_14191 x_14190
 534     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 535       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14191)
 536     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 537       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14190)
 538 | St_return x_14193 -> h_St_return x_14193
 539 | St_label (x_14195, x_14194) ->
 540   h_St_label x_14195 x_14194
 541     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 542       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14194)
 543 | St_goto x_14196 -> h_St_goto x_14196
 544 | St_cost (x_14198, x_14197) ->
 545   h_St_cost x_14198 x_14197
 546     (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
 547       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14197)
 548
 549 (** val stmt_inv_rect_Type4 :
 550     stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 551     (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
 552     Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
 553     -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
 554     'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
 555     'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
 556     Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
 557     -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
 558     (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 559 let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
 560   let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
 561
 562 (** val stmt_inv_rect_Type3 :
 563     stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 564     (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
 565     Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
 566     -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
 567     'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
 568     'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
 569     Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
 570     -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
 571     (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 572 let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
 573   let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
 574
 575 (** val stmt_inv_rect_Type2 :
 576     stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 577     (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
 578     Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
 579     -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
 580     'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
 581     'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
 582     Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
 583     -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
 584     (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 585 let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
 586   let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
 587
 588 (** val stmt_inv_rect_Type1 :
 589     stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 590     (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
 591     Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
 592     -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
 593     'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
 594     'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
 595     Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
 596     -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
 597     (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 598 let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
 599   let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
 600
 601 (** val stmt_inv_rect_Type0 :
 602     stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 603     (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
 604     Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
 605     -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
 606     'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
 607     'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
 608     Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
 609     -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
 610     (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 611 let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
 612   let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
 613
 614 (** val stmt_discr : stmt -> stmt -> __ **)
 615 let stmt_discr x y =
 616   Logic.eq_rect_Type2 x
 617     (match x with
 618      | St_skip -> Obj.magic (fun _ dH -> dH)
 619      | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 620      | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 621      | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 622      | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 623      | St_ifthenelse (a0, a1, a2, a3, a4) ->
 624        Obj.magic (fun _ dH -> dH __ __ __ __ __)
 625      | St_return a0 -> Obj.magic (fun _ dH -> dH __)
 626      | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 627      | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
 628      | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 629
 630 (** val stmt_jmdiscr : stmt -> stmt -> __ **)
 631 let stmt_jmdiscr x y =
 632   Logic.eq_rect_Type2 x
 633     (match x with
 634      | St_skip -> Obj.magic (fun _ dH -> dH)
 635      | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 636      | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 637      | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 638      | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 639      | St_ifthenelse (a0, a1, a2, a3, a4) ->
 640        Obj.magic (fun _ dH -> dH __ __ __ __ __)
 641      | St_return a0 -> Obj.magic (fun _ dH -> dH __)
 642      | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 643      | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
 644      | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 645
 646 (** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
 647 let rec labels_of = function
 648 | St_skip -> List.Nil
 649 | St_assign (x, x0, x1) -> List.Nil
 650 | St_store (x, x0, x1) -> List.Nil
 651 | St_call (x, x0, x1) -> List.Nil
 652 | St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
 653 | St_ifthenelse (x, x0, x1, s1, s2) ->
 654   List.append (labels_of s1) (labels_of s2)
 655 | St_return x -> List.Nil
 656 | St_label (l, s0) -> List.Cons (l, (labels_of s0))
 657 | St_goto x -> List.Nil
 658 | St_cost (x, s0) -> labels_of s0
 659
 660 (** val cminor_stmt_inv_rect_Type4 :
 661     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 662     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 663     'a1 **)
 664 let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
 665   h_mk_cminor_stmt_inv __ __ __
 666
 667 (** val cminor_stmt_inv_rect_Type5 :
 668     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 669     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 670     'a1 **)
 671 let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
 672   h_mk_cminor_stmt_inv __ __ __
 673
 674 (** val cminor_stmt_inv_rect_Type3 :
 675     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 676     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 677     'a1 **)
 678 let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
 679   h_mk_cminor_stmt_inv __ __ __
 680
 681 (** val cminor_stmt_inv_rect_Type2 :
 682     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 683     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 684     'a1 **)
 685 let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
 686   h_mk_cminor_stmt_inv __ __ __
 687
 688 (** val cminor_stmt_inv_rect_Type1 :
 689     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 690     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 691     'a1 **)
 692 let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
 693   h_mk_cminor_stmt_inv __ __ __
 694
 695 (** val cminor_stmt_inv_rect_Type0 :
 696     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 697     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
 698     'a1 **)
 699 let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
 700   h_mk_cminor_stmt_inv __ __ __
 701
 702 (** val cminor_stmt_inv_inv_rect_Type4 :
 703     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 704     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
 705     'a1) -> 'a1 **)
 706 let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
 707   let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
 708
 709 (** val cminor_stmt_inv_inv_rect_Type3 :
 710     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 711     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
 712     'a1) -> 'a1 **)
 713 let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
 714   let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
 715
 716 (** val cminor_stmt_inv_inv_rect_Type2 :
 717     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 718     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
 719     'a1) -> 'a1 **)
 720 let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
 721   let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
 722
 723 (** val cminor_stmt_inv_inv_rect_Type1 :
 724     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 725     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
 726     'a1) -> 'a1 **)
 727 let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
 728   let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
 729
 730 (** val cminor_stmt_inv_inv_rect_Type0 :
 731     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 732     List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
 733     'a1) -> 'a1 **)
 734 let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
 735   let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
 736
 737 (** val cminor_stmt_inv_discr :
 738     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 739     List.list -> AST.typ Types.option -> stmt -> __ **)
 740 let cminor_stmt_inv_discr a1 a2 a3 a4 =
 741   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 742
 743 (** val cminor_stmt_inv_jmdiscr :
 744     (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 745     List.list -> AST.typ Types.option -> stmt -> __ **)
 746 let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
 747   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 748
 749 type internal_function = { f_return : AST.typ Types.option;
 750                            f_params : (AST.ident, AST.typ) Types.prod
 751                                       List.list;
 752                            f_vars : (AST.ident, AST.typ) Types.prod List.list;
 753                            f_stacksize : Nat.nat; f_body : stmt }
 754
 755 (** val internal_function_rect_Type4 :
 756     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 757     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 758     -> 'a1) -> internal_function -> 'a1 **)
 759 let rec internal_function_rect_Type4 h_mk_internal_function x_14493 =
 760   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 761     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14493
 762   in
 763   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 764     __
 765
 766 (** val internal_function_rect_Type5 :
 767     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 768     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 769     -> 'a1) -> internal_function -> 'a1 **)
 770 let rec internal_function_rect_Type5 h_mk_internal_function x_14495 =
 771   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 772     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14495
 773   in
 774   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 775     __
 776
 777 (** val internal_function_rect_Type3 :
 778     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 779     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 780     -> 'a1) -> internal_function -> 'a1 **)
 781 let rec internal_function_rect_Type3 h_mk_internal_function x_14497 =
 782   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 783     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14497
 784   in
 785   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 786     __
 787
 788 (** val internal_function_rect_Type2 :
 789     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 790     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 791     -> 'a1) -> internal_function -> 'a1 **)
 792 let rec internal_function_rect_Type2 h_mk_internal_function x_14499 =
 793   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 794     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14499
 795   in
 796   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 797     __
 798
 799 (** val internal_function_rect_Type1 :
 800     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 801     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 802     -> 'a1) -> internal_function -> 'a1 **)
 803 let rec internal_function_rect_Type1 h_mk_internal_function x_14501 =
 804   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 805     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14501
 806   in
 807   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 808     __
 809
 810 (** val internal_function_rect_Type0 :
 811     (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 812     (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
 813     -> 'a1) -> internal_function -> 'a1 **)
 814 let rec internal_function_rect_Type0 h_mk_internal_function x_14503 =
 815   let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
 816     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14503
 817   in
 818   h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
 819     __
 820
 821 (** val f_return : internal_function -> AST.typ Types.option **)
 822 let rec f_return xxx =
 823   xxx.f_return
 824
 825 (** val f_params :
 826     internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
 827 let rec f_params xxx =
 828   xxx.f_params
 829
 830 (** val f_vars :
 831     internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
 832 let rec f_vars xxx =
 833   xxx.f_vars
 834
 835 (** val f_stacksize : internal_function -> Nat.nat **)
 836 let rec f_stacksize xxx =
 837   xxx.f_stacksize
 838
 839 (** val f_body : internal_function -> stmt **)
 840 let rec f_body xxx =
 841   xxx.f_body
 842
 843 (** val internal_function_inv_rect_Type4 :
 844     internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 845     Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
 846     -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
 847 let internal_function_inv_rect_Type4 hterm h1 =
 848   let hcut = internal_function_rect_Type4 h1 hterm in hcut __
 849
 850 (** val internal_function_inv_rect_Type3 :
 851     internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 852     Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
 853     -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
 854 let internal_function_inv_rect_Type3 hterm h1 =
 855   let hcut = internal_function_rect_Type3 h1 hterm in hcut __
 856
 857 (** val internal_function_inv_rect_Type2 :
 858     internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 859     Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
 860     -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
 861 let internal_function_inv_rect_Type2 hterm h1 =
 862   let hcut = internal_function_rect_Type2 h1 hterm in hcut __
 863
 864 (** val internal_function_inv_rect_Type1 :
 865     internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 866     Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
 867     -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
 868 let internal_function_inv_rect_Type1 hterm h1 =
 869   let hcut = internal_function_rect_Type1 h1 hterm in hcut __
 870
 871 (** val internal_function_inv_rect_Type0 :
 872     internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 873     Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
 874     -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
 875 let internal_function_inv_rect_Type0 hterm h1 =
 876   let hcut = internal_function_rect_Type0 h1 hterm in hcut __
 877
 878 (** val internal_function_jmdiscr :
 879     internal_function -> internal_function -> __ **)
 880 let internal_function_jmdiscr x y =
 881   Logic.eq_rect_Type2 x
 882     (let { f_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
 883        f_body = a5 } = x
 884      in
 885     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
 886
 887 type cminor_program =
 888   (internal_function AST.fundef, AST.init_data List.list) AST.program
 889
 890 type cminor_noinit_program =
 891   (internal_function AST.fundef, Nat.nat) AST.program
 892