extracted/aST.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Exp
  14
  15 open Arithmetic
  16
  17 open Vector
  18
  19 open Div_and_mod
  20
  21 open Util
  22
  23 open FoldStuff
  24
  25 open BitVector
  26
  27 open Jmeq
  28
  29 open Russell
  30
  31 open List
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Bool
  42
  43 open Relations
  44
  45 open Nat
  46
  47 open Integers
  48
  49 open Proper
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open ErrorMessages
  56
  57 open PreIdentifiers
  58
  59 open Errors
  60
  61 open Extralib
  62
  63 open Lists
  64
  65 open Positive
  66
  67 open Identifiers
  68
  69 type ident = PreIdentifiers.identifier
  70
  71 val ident_eq : ident -> ident -> (__, __) Types.sum
  72
  73 val ident_of_nat : Nat.nat -> ident
  74
  75 type region =
  76 | XData
  77 | Code
  78
  79 val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1
  80
  81 val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1
  82
  83 val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1
  84
  85 val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1
  86
  87 val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1
  88
  89 val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1
  90
  91 val region_inv_rect_Type4 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  92
  93 val region_inv_rect_Type3 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  94
  95 val region_inv_rect_Type2 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  96
  97 val region_inv_rect_Type1 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  98
  99 val region_inv_rect_Type0 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 100
 101 val region_discr : region -> region -> __
 102
 103 val region_jmdiscr : region -> region -> __
 104
 105 val eq_region : region -> region -> Bool.bool
 106
 107 val eq_region_elim : region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 108
 109 val eq_region_dec : region -> region -> (__, __) Types.sum
 110
 111 val size_pointer : Nat.nat
 112
 113 type signedness =
 114 | Signed
 115 | Unsigned
 116
 117 val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1
 118
 119 val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1
 120
 121 val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1
 122
 123 val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1
 124
 125 val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1
 126
 127 val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1
 128
 129 val signedness_inv_rect_Type4 :
 130   signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 131
 132 val signedness_inv_rect_Type3 :
 133   signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 134
 135 val signedness_inv_rect_Type2 :
 136   signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 137
 138 val signedness_inv_rect_Type1 :
 139   signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 140
 141 val signedness_inv_rect_Type0 :
 142   signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 143
 144 val signedness_discr : signedness -> signedness -> __
 145
 146 val signedness_jmdiscr : signedness -> signedness -> __
 147
 148 type intsize =
 149 | I8
 150 | I16
 151 | I32
 152
 153 val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 154
 155 val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 156
 157 val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 158
 159 val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 160
 161 val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 162
 163 val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
 164
 165 val intsize_inv_rect_Type4 :
 166   intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 167
 168 val intsize_inv_rect_Type3 :
 169   intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 170
 171 val intsize_inv_rect_Type2 :
 172   intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 173
 174 val intsize_inv_rect_Type1 :
 175   intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 176
 177 val intsize_inv_rect_Type0 :
 178   intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 179
 180 val intsize_discr : intsize -> intsize -> __
 181
 182 val intsize_jmdiscr : intsize -> intsize -> __
 183
 184 type floatsize =
 185 | F32
 186 | F64
 187
 188 val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1
 189
 190 val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1
 191
 192 val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1
 193
 194 val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1
 195
 196 val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1
 197
 198 val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1
 199
 200 val floatsize_inv_rect_Type4 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 201
 202 val floatsize_inv_rect_Type3 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 203
 204 val floatsize_inv_rect_Type2 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 205
 206 val floatsize_inv_rect_Type1 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 207
 208 val floatsize_inv_rect_Type0 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 209
 210 val floatsize_discr : floatsize -> floatsize -> __
 211
 212 val floatsize_jmdiscr : floatsize -> floatsize -> __
 213
 214 type typ =
 215 | ASTint of intsize * signedness
 216 | ASTptr
 217
 218 val typ_rect_Type4 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 219
 220 val typ_rect_Type5 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 221
 222 val typ_rect_Type3 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 223
 224 val typ_rect_Type2 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 225
 226 val typ_rect_Type1 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 227
 228 val typ_rect_Type0 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
 229
 230 val typ_inv_rect_Type4 :
 231   typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 232
 233 val typ_inv_rect_Type3 :
 234   typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 235
 236 val typ_inv_rect_Type2 :
 237   typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 238
 239 val typ_inv_rect_Type1 :
 240   typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 241
 242 val typ_inv_rect_Type0 :
 243   typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
 244
 245 val typ_discr : typ -> typ -> __
 246
 247 val typ_jmdiscr : typ -> typ -> __
 248
 249 type sigType = typ
 250
 251 val sigType_Int : typ
 252
 253 val sigType_Ptr : typ
 254
 255 val pred_size_intsize : intsize -> Nat.nat
 256
 257 val size_intsize : intsize -> Nat.nat
 258
 259 val bitsize_of_intsize : intsize -> Nat.nat
 260
 261 val eq_intsize : intsize -> intsize -> Bool.bool
 262
 263 val eq_intsize_elim : intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 264
 265 val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1
 266
 267 val inttyp_eq_elim' :
 268   intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1
 269
 270 val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1
 271
 272 val intsize_eq_elim : intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1
 273
 274 val intsize_eq_elim_elim :
 275   intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
 276   __) -> 'a3
 277
 278 type bvint = BitVector.bitVector
 279
 280 val repr : intsize -> Nat.nat -> bvint
 281
 282 val size_floatsize : floatsize -> Nat.nat
 283
 284 val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1
 285
 286 val typesize : typ -> Nat.nat
 287
 288 val typ_eq : typ -> typ -> (__, __) Types.sum
 289
 290 val opt_typ_eq : typ Types.option -> typ Types.option -> (__, __) Types.sum
 291
 292 type signature = { sig_args : typ List.list; sig_res : typ Types.option }
 293
 294 val signature_rect_Type4 :
 295   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 296
 297 val signature_rect_Type5 :
 298   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 299
 300 val signature_rect_Type3 :
 301   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 302
 303 val signature_rect_Type2 :
 304   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 305
 306 val signature_rect_Type1 :
 307   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 308
 309 val signature_rect_Type0 :
 310   (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
 311
 312 val sig_args : signature -> typ List.list
 313
 314 val sig_res : signature -> typ Types.option
 315
 316 val signature_inv_rect_Type4 :
 317   signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
 318
 319 val signature_inv_rect_Type3 :
 320   signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
 321
 322 val signature_inv_rect_Type2 :
 323   signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
 324
 325 val signature_inv_rect_Type1 :
 326   signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
 327
 328 val signature_inv_rect_Type0 :
 329   signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
 330
 331 val signature_discr : signature -> signature -> __
 332
 333 val signature_jmdiscr : signature -> signature -> __
 334
 335 type signature0 = signature
 336
 337 val signature_args : signature -> typ List.list
 338
 339 val signature_return : signature -> typ Types.option
 340
 341 val proj_sig_res : signature -> typ
 342
 343 type init_data =
 344 | Init_int8 of bvint
 345 | Init_int16 of bvint
 346 | Init_int32 of bvint
 347 | Init_space of Nat.nat
 348 | Init_null
 349 | Init_addrof of ident * Nat.nat
 350
 351 val init_data_rect_Type4 :
 352   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 353   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 354
 355 val init_data_rect_Type5 :
 356   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 357   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 358
 359 val init_data_rect_Type3 :
 360   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 361   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 362
 363 val init_data_rect_Type2 :
 364   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 365   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 366
 367 val init_data_rect_Type1 :
 368   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 369   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 370
 371 val init_data_rect_Type0 :
 372   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
 373   'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
 374
 375 val init_data_inv_rect_Type4 :
 376   init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
 377   -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
 378   -> 'a1) -> 'a1
 379
 380 val init_data_inv_rect_Type3 :
 381   init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
 382   -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
 383   -> 'a1) -> 'a1
 384
 385 val init_data_inv_rect_Type2 :
 386   init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
 387   -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
 388   -> 'a1) -> 'a1
 389
 390 val init_data_inv_rect_Type1 :
 391   init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
 392   -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
 393   -> 'a1) -> 'a1
 394
 395 val init_data_inv_rect_Type0 :
 396   init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
 397   -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
 398   -> 'a1) -> 'a1
 399
 400 val init_data_discr : init_data -> init_data -> __
 401
 402 val init_data_jmdiscr : init_data -> init_data -> __
 403
 404 type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
 405                                       Types.prod List.list;
 406                           prog_funct : (ident, 'f) Types.prod List.list;
 407                           prog_main : ident }
 408
 409 val program_rect_Type4 :
 410   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 411   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 412
 413 val program_rect_Type5 :
 414   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 415   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 416
 417 val program_rect_Type3 :
 418   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 419   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 420
 421 val program_rect_Type2 :
 422   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 423   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 424
 425 val program_rect_Type1 :
 426   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 427   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 428
 429 val program_rect_Type0 :
 430   (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
 431   Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
 432
 433 val prog_vars :
 434   ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
 435   List.list
 436
 437 val prog_funct : ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list
 438
 439 val prog_main : ('a1, 'a2) program -> ident
 440
 441 val program_inv_rect_Type4 :
 442   ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
 443   List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
 444   'a3
 445
 446 val program_inv_rect_Type3 :
 447   ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
 448   List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
 449   'a3
 450
 451 val program_inv_rect_Type2 :
 452   ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
 453   List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
 454   'a3
 455
 456 val program_inv_rect_Type1 :
 457   ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
 458   List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
 459   'a3
 460
 461 val program_inv_rect_Type0 :
 462   ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
 463   List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
 464   'a3
 465
 466 val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __
 467
 468 val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __
 469
 470 val prog_funct_names : ('a1, 'a2) program -> ident List.list
 471
 472 val prog_var_names : ('a1, 'a2) program -> ident List.list
 473
 474 val transf_program :
 475   ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
 476   Types.prod List.list
 477
 478 val transform_program :
 479   ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3) program
 480
 481 val transf_program_gen :
 482   PreIdentifiers.identifierTag -> Identifiers.universe ->
 483   (Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe) Types.prod) ->
 484   (ident, 'a1) Types.prod List.list -> ((ident, 'a2) Types.prod List.list,
 485   Identifiers.universe) Types.prod
 486
 487 val transform_program_gen :
 488   PreIdentifiers.identifierTag -> Identifiers.universe -> ('a1, 'a3) program
 489   -> (ident List.list -> Identifiers.universe -> 'a1 -> ('a2,
 490   Identifiers.universe) Types.prod) -> (('a2, 'a3) program,
 491   Identifiers.universe) Types.prod
 492
 493 val map_partial :
 494   ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
 495   Types.prod List.list Errors.res
 496
 497 val transform_partial_program :
 498   ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
 499   'a3) program Errors.res
 500
 501 val transform_partial_program2 :
 502   ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3 ->
 503   'a4 Errors.res) -> ('a2, 'a4) program Errors.res
 504
 505 type matching =
 506 | Mk_matching
 507
 508 val matching_rect_Type4 :
 509   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 510
 511 val matching_rect_Type5 :
 512   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 513
 514 val matching_rect_Type3 :
 515   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 516
 517 val matching_rect_Type2 :
 518   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 519
 520 val matching_rect_Type1 :
 521   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 522
 523 val matching_rect_Type0 :
 524   (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
 525
 526 type m_A
 527
 528 type m_B
 529
 530 type m_V
 531
 532 type m_W
 533
 534 val matching_inv_rect_Type4 :
 535   matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 536
 537 val matching_inv_rect_Type3 :
 538   matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 539
 540 val matching_inv_rect_Type2 :
 541   matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 542
 543 val matching_inv_rect_Type1 :
 544   matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 545
 546 val matching_inv_rect_Type0 :
 547   matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 548
 549 val matching_jmdiscr : matching -> matching -> __
 550
 551 val mfe_cast_fn_type :
 552   matching -> ident List.list -> ident List.list -> __ -> __
 553
 554 val match_program_rect_Type4 :
 555   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 556   -> 'a1
 557
 558 val match_program_rect_Type5 :
 559   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 560   -> 'a1
 561
 562 val match_program_rect_Type3 :
 563   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 564   -> 'a1
 565
 566 val match_program_rect_Type2 :
 567   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 568   -> 'a1
 569
 570 val match_program_rect_Type1 :
 571   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 572   -> 'a1
 573
 574 val match_program_rect_Type0 :
 575   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
 576   -> 'a1
 577
 578 val match_program_inv_rect_Type4 :
 579   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
 580   -> 'a1) -> 'a1
 581
 582 val match_program_inv_rect_Type3 :
 583   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
 584   -> 'a1) -> 'a1
 585
 586 val match_program_inv_rect_Type2 :
 587   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
 588   -> 'a1) -> 'a1
 589
 590 val match_program_inv_rect_Type1 :
 591   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
 592   -> 'a1) -> 'a1
 593
 594 val match_program_inv_rect_Type0 :
 595   matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
 596   -> 'a1) -> 'a1
 597
 598 val match_program_discr :
 599   matching -> (__, __) program -> (__, __) program -> __
 600
 601 val match_program_jmdiscr :
 602   matching -> (__, __) program -> (__, __) program -> __
 603
 604 type external_function = { ef_id : ident; ef_sig : signature }
 605
 606 val external_function_rect_Type4 :
 607   (ident -> signature -> 'a1) -> external_function -> 'a1
 608
 609 val external_function_rect_Type5 :
 610   (ident -> signature -> 'a1) -> external_function -> 'a1
 611
 612 val external_function_rect_Type3 :
 613   (ident -> signature -> 'a1) -> external_function -> 'a1
 614
 615 val external_function_rect_Type2 :
 616   (ident -> signature -> 'a1) -> external_function -> 'a1
 617
 618 val external_function_rect_Type1 :
 619   (ident -> signature -> 'a1) -> external_function -> 'a1
 620
 621 val external_function_rect_Type0 :
 622   (ident -> signature -> 'a1) -> external_function -> 'a1
 623
 624 val ef_id : external_function -> ident
 625
 626 val ef_sig : external_function -> signature
 627
 628 val external_function_inv_rect_Type4 :
 629   external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
 630
 631 val external_function_inv_rect_Type3 :
 632   external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
 633
 634 val external_function_inv_rect_Type2 :
 635   external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
 636
 637 val external_function_inv_rect_Type1 :
 638   external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
 639
 640 val external_function_inv_rect_Type0 :
 641   external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
 642
 643 val external_function_discr : external_function -> external_function -> __
 644
 645 val external_function_jmdiscr : external_function -> external_function -> __
 646
 647 type externalFunction = external_function
 648
 649 val external_function_tag : external_function -> ident
 650
 651 val external_function_sig : external_function -> signature
 652
 653 type 'f fundef =
 654 | Internal of 'f
 655 | External of external_function
 656
 657 val fundef_rect_Type4 :
 658   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 659
 660 val fundef_rect_Type5 :
 661   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 662
 663 val fundef_rect_Type3 :
 664   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 665
 666 val fundef_rect_Type2 :
 667   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 668
 669 val fundef_rect_Type1 :
 670   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 671
 672 val fundef_rect_Type0 :
 673   ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
 674
 675 val fundef_inv_rect_Type4 :
 676   'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
 677
 678 val fundef_inv_rect_Type3 :
 679   'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
 680
 681 val fundef_inv_rect_Type2 :
 682   'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
 683
 684 val fundef_inv_rect_Type1 :
 685   'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
 686
 687 val fundef_inv_rect_Type0 :
 688   'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
 689
 690 val fundef_discr : 'a1 fundef -> 'a1 fundef -> __
 691
 692 val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __
 693
 694 val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef
 695
 696 val transf_partial_fundef :
 697   ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res
 698