extracted/cminor_syntax.mli

   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
 116 val expr_rect_Type3 :
 117   (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 118   -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 119   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 120   expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 121   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
 122   'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
 123   'a1) -> AST.typ -> expr -> 'a1
 124
 125 val expr_rect_Type2 :
 126   (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 127   -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 128   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 129   expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 130   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
 131   'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
 132   'a1) -> AST.typ -> expr -> 'a1
 133
 134 val expr_rect_Type1 :
 135   (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 136   -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 137   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 138   expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 139   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
 140   'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
 141   'a1) -> AST.typ -> expr -> 'a1
 142
 143 val expr_rect_Type0 :
 144   (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
 145   -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
 146   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 147   expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
 148   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1 ->
 149   'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1 ->
 150   'a1) -> AST.typ -> expr -> 'a1
 151
 152 val expr_inv_rect_Type4 :
 153   AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
 154   FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 155   FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 156   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 157   expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
 158   -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 159   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
 160   __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 161   (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 162   'a1) -> 'a1
 163
 164 val expr_inv_rect_Type3 :
 165   AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
 166   FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 167   FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 168   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 169   expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
 170   -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 171   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
 172   __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 173   (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 174   'a1) -> 'a1
 175
 176 val expr_inv_rect_Type2 :
 177   AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
 178   FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 179   FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 180   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 181   expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
 182   -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 183   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
 184   __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 185   (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 186   'a1) -> 'a1
 187
 188 val expr_inv_rect_Type1 :
 189   AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
 190   FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 191   FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 192   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 193   expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
 194   -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 195   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
 196   __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 197   (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 198   'a1) -> 'a1
 199
 200 val expr_inv_rect_Type0 :
 201   AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ ->
 202   FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
 203   FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 204   'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 205   expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1)
 206   -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 207   (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__ ->
 208   __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
 209   (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
 210   'a1) -> 'a1
 211
 212 val expr_jmdiscr : AST.typ -> expr -> expr -> __
 213
 214 type stmt =
 215 | St_skip
 216 | St_assign of AST.typ * AST.ident * expr
 217 | St_store of AST.typ * expr * expr
 218 | St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
 219    * (AST.typ, expr) Types.dPair List.list
 220 | St_seq of stmt * stmt
 221 | St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
 222 | St_return of (AST.typ, expr) Types.dPair Types.option
 223 | St_label of PreIdentifiers.identifier * stmt
 224 | St_goto of PreIdentifiers.identifier
 225 | St_cost of CostLabel.costlabel * stmt
 226
 227 val stmt_rect_Type4 :
 228   'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
 229   'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
 230   expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
 231   -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
 232   'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
 233   (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 234   (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 235   -> 'a1) -> stmt -> 'a1
 236
 237 val stmt_rect_Type3 :
 238   'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
 239   'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
 240   expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
 241   -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
 242   'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
 243   (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 244   (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 245   -> 'a1) -> stmt -> 'a1
 246
 247 val stmt_rect_Type2 :
 248   'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
 249   'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
 250   expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
 251   -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
 252   'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
 253   (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 254   (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 255   -> 'a1) -> stmt -> 'a1
 256
 257 val stmt_rect_Type1 :
 258   'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
 259   'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
 260   expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
 261   -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
 262   'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
 263   (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 264   (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 265   -> 'a1) -> stmt -> 'a1
 266
 267 val stmt_rect_Type0 :
 268   'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr ->
 269   'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr -> (AST.typ,
 270   expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 -> 'a1 -> 'a1)
 271   -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> 'a1 -> 'a1 ->
 272   'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1) ->
 273   (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
 274   (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
 275   -> 'a1) -> stmt -> 'a1
 276
 277 val stmt_inv_rect_Type4 :
 278   stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 279   (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
 280   Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
 281   -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
 282   (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
 283   (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
 284   __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
 285   'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
 286   stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 287
 288 val stmt_inv_rect_Type3 :
 289   stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 290   (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
 291   Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
 292   -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
 293   (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
 294   (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
 295   __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
 296   'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
 297   stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 298
 299 val stmt_inv_rect_Type2 :
 300   stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 301   (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
 302   Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
 303   -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
 304   (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
 305   (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
 306   __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
 307   'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
 308   stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 309
 310 val stmt_inv_rect_Type1 :
 311   stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 312   (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
 313   Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
 314   -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
 315   (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
 316   (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
 317   __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
 318   'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
 319   stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 320
 321 val stmt_inv_rect_Type0 :
 322   stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
 323   (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ) Types.prod
 324   Types.option -> expr -> (AST.typ, expr) Types.dPair List.list -> __ -> 'a1)
 325   -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ -> 'a1) ->
 326   (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ -> 'a1) ->
 327   (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option ->
 328   __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__ -> 'a1) -> __ ->
 329   'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) -> (CostLabel.costlabel ->
 330   stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
 331
 332 val stmt_discr : stmt -> stmt -> __
 333
 334 val stmt_jmdiscr : stmt -> stmt -> __
 335
 336 val labels_of : stmt -> PreIdentifiers.identifier List.list
 337
 338 val cminor_stmt_inv_rect_Type4 :
 339   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 340   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 341
 342 val cminor_stmt_inv_rect_Type5 :
 343   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 344   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 345
 346 val cminor_stmt_inv_rect_Type3 :
 347   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 348   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 349
 350 val cminor_stmt_inv_rect_Type2 :
 351   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 352   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 353
 354 val cminor_stmt_inv_rect_Type1 :
 355   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 356   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 357
 358 val cminor_stmt_inv_rect_Type0 :
 359   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 360   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 361
 362 val cminor_stmt_inv_inv_rect_Type4 :
 363   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 364   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
 365   -> 'a1
 366
 367 val cminor_stmt_inv_inv_rect_Type3 :
 368   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 369   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
 370   -> 'a1
 371
 372 val cminor_stmt_inv_inv_rect_Type2 :
 373   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 374   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
 375   -> 'a1
 376
 377 val cminor_stmt_inv_inv_rect_Type1 :
 378   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 379   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
 380   -> 'a1
 381
 382 val cminor_stmt_inv_inv_rect_Type0 :
 383   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 384   List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ -> 'a1)
 385   -> 'a1
 386
 387 val cminor_stmt_inv_discr :
 388   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 389   List.list -> AST.typ Types.option -> stmt -> __
 390
 391 val cminor_stmt_inv_jmdiscr :
 392   (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
 393   List.list -> AST.typ Types.option -> stmt -> __
 394
 395 type internal_function = { f_return : AST.typ Types.option;
 396                            f_params : (AST.ident, AST.typ) Types.prod
 397                                       List.list;
 398                            f_vars : (AST.ident, AST.typ) Types.prod List.list;
 399                            f_stacksize : Nat.nat; f_body : stmt }
 400
 401 val internal_function_rect_Type4 :
 402   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 403   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 404   'a1) -> internal_function -> 'a1
 405
 406 val internal_function_rect_Type5 :
 407   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 408   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 409   'a1) -> internal_function -> 'a1
 410
 411 val internal_function_rect_Type3 :
 412   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 413   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 414   'a1) -> internal_function -> 'a1
 415
 416 val internal_function_rect_Type2 :
 417   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 418   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 419   'a1) -> internal_function -> 'a1
 420
 421 val internal_function_rect_Type1 :
 422   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 423   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 424   'a1) -> internal_function -> 'a1
 425
 426 val internal_function_rect_Type0 :
 427   (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
 428   (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __ ->
 429   'a1) -> internal_function -> 'a1
 430
 431 val f_return : internal_function -> AST.typ Types.option
 432
 433 val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list
 434
 435 val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list
 436
 437 val f_stacksize : internal_function -> Nat.nat
 438
 439 val f_body : internal_function -> stmt
 440
 441 val internal_function_inv_rect_Type4 :
 442   internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 443   Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
 444   Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
 445
 446 val internal_function_inv_rect_Type3 :
 447   internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 448   Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
 449   Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
 450
 451 val internal_function_inv_rect_Type2 :
 452   internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 453   Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
 454   Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
 455
 456 val internal_function_inv_rect_Type1 :
 457   internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 458   Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
 459   Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
 460
 461 val internal_function_inv_rect_Type0 :
 462   internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
 463   Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __ ->
 464   Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1
 465
 466 val internal_function_jmdiscr : internal_function -> internal_function -> __
 467
 468 type cminor_program =
 469   (internal_function AST.fundef, AST.init_data List.list) AST.program
 470
 471 type cminor_noinit_program =
 472   (internal_function AST.fundef, Nat.nat) AST.program
 473