extracted/classifyOp.mli

   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
  81 type classify_add_cases =
  82 | Add_case_ii of AST.intsize * AST.signedness
  83 | Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
  84    * AST.signedness
  85 | Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
  86    * Csyntax.type0
  87 | Add_default of Csyntax.type0 * Csyntax.type0
  88
  89 val classify_add_cases_rect_Type4 :
  90   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  91   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  92   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
  93   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
  94   -> classify_add_cases -> 'a1
  95
  96 val classify_add_cases_rect_Type5 :
  97   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
  98   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
  99   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 100   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 101   -> classify_add_cases -> 'a1
 102
 103 val classify_add_cases_rect_Type3 :
 104   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 105   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 106   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 107   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 108   -> classify_add_cases -> 'a1
 109
 110 val classify_add_cases_rect_Type2 :
 111   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 112   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 113   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 114   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 115   -> classify_add_cases -> 'a1
 116
 117 val classify_add_cases_rect_Type1 :
 118   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 119   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 120   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 121   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 122   -> classify_add_cases -> 'a1
 123
 124 val classify_add_cases_rect_Type0 :
 125   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 126   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 127   Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
 128   (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
 129   -> classify_add_cases -> 'a1
 130
 131 val classify_add_cases_inv_rect_Type4 :
 132   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 133   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 134   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 135   (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
 136   __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
 137   -> 'a1) -> 'a1
 138
 139 val classify_add_cases_inv_rect_Type3 :
 140   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 141   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 142   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 143   (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
 144   __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
 145   -> 'a1) -> 'a1
 146
 147 val classify_add_cases_inv_rect_Type2 :
 148   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 149   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 150   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 151   (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
 152   __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
 153   -> 'a1) -> 'a1
 154
 155 val classify_add_cases_inv_rect_Type1 :
 156   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 157   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 158   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 159   (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
 160   __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
 161   -> 'a1) -> 'a1
 162
 163 val classify_add_cases_inv_rect_Type0 :
 164   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
 165   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 166   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 167   (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
 168   __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
 169   -> 'a1) -> 'a1
 170
 171 val classify_add_cases_discr :
 172   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
 173   -> __
 174
 175 val classify_add_cases_jmdiscr :
 176   Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
 177   -> __
 178
 179 val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases
 180
 181 type classify_sub_cases =
 182 | Sub_case_ii of AST.intsize * AST.signedness
 183 | Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
 184    * AST.signedness
 185 | Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
 186    * Csyntax.type0
 187 | Sub_default of Csyntax.type0 * Csyntax.type0
 188
 189 val classify_sub_cases_rect_Type4 :
 190   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 191   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 192   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 193   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 194   Csyntax.type0 -> classify_sub_cases -> 'a1
 195
 196 val classify_sub_cases_rect_Type5 :
 197   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 198   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 199   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 200   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 201   Csyntax.type0 -> classify_sub_cases -> 'a1
 202
 203 val classify_sub_cases_rect_Type3 :
 204   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 205   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 206   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 207   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 208   Csyntax.type0 -> classify_sub_cases -> 'a1
 209
 210 val classify_sub_cases_rect_Type2 :
 211   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 212   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 213   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 214   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 215   Csyntax.type0 -> classify_sub_cases -> 'a1
 216
 217 val classify_sub_cases_rect_Type1 :
 218   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 219   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 220   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 221   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 222   Csyntax.type0 -> classify_sub_cases -> 'a1
 223
 224 val classify_sub_cases_rect_Type0 :
 225   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 226   Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
 227   Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
 228   'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
 229   Csyntax.type0 -> classify_sub_cases -> 'a1
 230
 231 val classify_sub_cases_inv_rect_Type4 :
 232   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 233   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 234   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 235   (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 236   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 237   -> __ -> __ -> __ -> 'a1) -> 'a1
 238
 239 val classify_sub_cases_inv_rect_Type3 :
 240   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 241   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 242   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 243   (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 244   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 245   -> __ -> __ -> __ -> 'a1) -> 'a1
 246
 247 val classify_sub_cases_inv_rect_Type2 :
 248   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 249   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 250   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 251   (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 252   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 253   -> __ -> __ -> __ -> 'a1) -> 'a1
 254
 255 val classify_sub_cases_inv_rect_Type1 :
 256   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 257   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 258   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 259   (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 260   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 261   -> __ -> __ -> __ -> 'a1) -> 'a1
 262
 263 val classify_sub_cases_inv_rect_Type0 :
 264   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
 265   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 266   Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 267   (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
 268   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 269   -> __ -> __ -> __ -> 'a1) -> 'a1
 270
 271 val classify_sub_cases_discr :
 272   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
 273   -> __
 274
 275 val classify_sub_cases_jmdiscr :
 276   Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
 277   -> __
 278
 279 val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases
 280
 281 type classify_aop_cases =
 282 | Aop_case_ii of AST.intsize * AST.signedness
 283 | Aop_default of Csyntax.type0 * Csyntax.type0
 284
 285 val classify_aop_cases_rect_Type4 :
 286   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 287   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 288
 289 val classify_aop_cases_rect_Type5 :
 290   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 291   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 292
 293 val classify_aop_cases_rect_Type3 :
 294   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 295   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 296
 297 val classify_aop_cases_rect_Type2 :
 298   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 299   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 300
 301 val classify_aop_cases_rect_Type1 :
 302   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 303   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 304
 305 val classify_aop_cases_rect_Type0 :
 306   (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 307   -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
 308
 309 val classify_aop_cases_inv_rect_Type4 :
 310   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 311   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 312   -> __ -> __ -> __ -> 'a1) -> 'a1
 313
 314 val classify_aop_cases_inv_rect_Type3 :
 315   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 316   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 317   -> __ -> __ -> __ -> 'a1) -> 'a1
 318
 319 val classify_aop_cases_inv_rect_Type2 :
 320   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 321   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 322   -> __ -> __ -> __ -> 'a1) -> 'a1
 323
 324 val classify_aop_cases_inv_rect_Type1 :
 325   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 326   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 327   -> __ -> __ -> __ -> 'a1) -> 'a1
 328
 329 val classify_aop_cases_inv_rect_Type0 :
 330   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
 331   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 332   -> __ -> __ -> __ -> 'a1) -> 'a1
 333
 334 val classify_aop_cases_discr :
 335   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
 336   -> __
 337
 338 val classify_aop_cases_jmdiscr :
 339   Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
 340   -> __
 341
 342 val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases
 343
 344 type classify_cmp_cases =
 345 | Cmp_case_ii of AST.intsize * AST.signedness
 346 | Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
 347 | Cmp_default of Csyntax.type0 * Csyntax.type0
 348
 349 val classify_cmp_cases_rect_Type4 :
 350   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 351   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 352   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 353
 354 val classify_cmp_cases_rect_Type5 :
 355   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 356   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 357   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 358
 359 val classify_cmp_cases_rect_Type3 :
 360   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 361   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 362   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 363
 364 val classify_cmp_cases_rect_Type2 :
 365   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 366   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 367   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 368
 369 val classify_cmp_cases_rect_Type1 :
 370   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 371   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 372   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 373
 374 val classify_cmp_cases_rect_Type0 :
 375   (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
 376   Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
 377   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
 378
 379 val classify_cmp_cases_inv_rect_Type4 :
 380   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 381   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 382   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 383   -> __ -> __ -> __ -> 'a1) -> 'a1
 384
 385 val classify_cmp_cases_inv_rect_Type3 :
 386   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 387   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 388   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 389   -> __ -> __ -> __ -> 'a1) -> 'a1
 390
 391 val classify_cmp_cases_inv_rect_Type2 :
 392   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 393   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 394   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 395   -> __ -> __ -> __ -> 'a1) -> 'a1
 396
 397 val classify_cmp_cases_inv_rect_Type1 :
 398   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 399   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 400   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 401   -> __ -> __ -> __ -> 'a1) -> 'a1
 402
 403 val classify_cmp_cases_inv_rect_Type0 :
 404   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
 405   AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
 406   Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
 407   -> __ -> __ -> __ -> 'a1) -> 'a1
 408
 409 val classify_cmp_cases_discr :
 410   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
 411   -> __
 412
 413 val classify_cmp_cases_jmdiscr :
 414   Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
 415   -> __
 416
 417 val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases
 418
 419 type classify_fun_cases =
 420 | Fun_case_f of Csyntax.typelist * Csyntax.type0
 421 | Fun_default
 422
 423 val classify_fun_cases_rect_Type4 :
 424   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 425   'a1
 426
 427 val classify_fun_cases_rect_Type5 :
 428   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 429   'a1
 430
 431 val classify_fun_cases_rect_Type3 :
 432   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 433   'a1
 434
 435 val classify_fun_cases_rect_Type2 :
 436   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 437   'a1
 438
 439 val classify_fun_cases_rect_Type1 :
 440   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 441   'a1
 442
 443 val classify_fun_cases_rect_Type0 :
 444   (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
 445   'a1
 446
 447 val classify_fun_cases_inv_rect_Type4 :
 448   classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 449   (__ -> 'a1) -> 'a1
 450
 451 val classify_fun_cases_inv_rect_Type3 :
 452   classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 453   (__ -> 'a1) -> 'a1
 454
 455 val classify_fun_cases_inv_rect_Type2 :
 456   classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 457   (__ -> 'a1) -> 'a1
 458
 459 val classify_fun_cases_inv_rect_Type1 :
 460   classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 461   (__ -> 'a1) -> 'a1
 462
 463 val classify_fun_cases_inv_rect_Type0 :
 464   classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
 465   (__ -> 'a1) -> 'a1
 466
 467 val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __
 468
 469 val classify_fun_cases_jmdiscr :
 470   classify_fun_cases -> classify_fun_cases -> __
 471
 472 val classify_fun : Csyntax.type0 -> classify_fun_cases
 473