extracted/joint.mli

   1 open Preamble
   2
   3 open Hide
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open Div_and_mod
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Util
  52
  53 open FoldStuff
  54
  55 open BitVector
  56
  57 open Types
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Positive
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 open ByteValues
  82
  83 open BackEndOps
  84
  85 open CostLabel
  86
  87 open Order
  88
  89 open Registers
  90
  91 open I8051
  92
  93 open BitVectorTrie
  94
  95 open Graphs
  96
  97 open LabelledObjects
  98
  99 open Sets
 100
 101 open Listb
 102
 103 open String
 104
 105 type 't argument =
 106 | Reg of 't
 107 | Imm of BitVector.byte
 108
 109 val argument_rect_Type4 :
 110   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 111
 112 val argument_rect_Type5 :
 113   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 114
 115 val argument_rect_Type3 :
 116   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 117
 118 val argument_rect_Type2 :
 119   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 120
 121 val argument_rect_Type1 :
 122   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 123
 124 val argument_rect_Type0 :
 125   ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
 126
 127 val argument_inv_rect_Type4 :
 128   'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
 129
 130 val argument_inv_rect_Type3 :
 131   'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
 132
 133 val argument_inv_rect_Type2 :
 134   'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
 135
 136 val argument_inv_rect_Type1 :
 137   'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
 138
 139 val argument_inv_rect_Type0 :
 140   'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
 141
 142 val argument_discr : 'a1 argument -> 'a1 argument -> __
 143
 144 val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __
 145
 146 type psd_argument = Registers.register argument
 147
 148 val psd_argument_from_reg : Registers.register -> psd_argument
 149
 150 val dpi1__o__reg_to_psd_argument__o__inject :
 151   (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0
 152
 153 val eject__o__reg_to_psd_argument__o__inject :
 154   Registers.register Types.sig0 -> psd_argument Types.sig0
 155
 156 val reg_to_psd_argument__o__inject :
 157   Registers.register -> psd_argument Types.sig0
 158
 159 val dpi1__o__reg_to_psd_argument :
 160   (Registers.register, 'a1) Types.dPair -> psd_argument
 161
 162 val eject__o__reg_to_psd_argument :
 163   Registers.register Types.sig0 -> psd_argument
 164
 165 val psd_argument_from_byte : BitVector.byte -> psd_argument
 166
 167 val dpi1__o__byte_to_psd_argument__o__inject :
 168   (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
 169
 170 val eject__o__byte_to_psd_argument__o__inject :
 171   BitVector.byte Types.sig0 -> psd_argument Types.sig0
 172
 173 val byte_to_psd_argument__o__inject :
 174   BitVector.byte -> psd_argument Types.sig0
 175
 176 val dpi1__o__byte_to_psd_argument :
 177   (BitVector.byte, 'a1) Types.dPair -> psd_argument
 178
 179 val eject__o__byte_to_psd_argument :
 180   BitVector.byte Types.sig0 -> psd_argument
 181
 182 type hdw_argument = I8051.register argument
 183
 184 val hdw_argument_from_reg : I8051.register -> hdw_argument
 185
 186 val dpi1__o__reg_to_hdw_argument__o__inject :
 187   (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0
 188
 189 val eject__o__reg_to_hdw_argument__o__inject :
 190   I8051.register Types.sig0 -> hdw_argument Types.sig0
 191
 192 val reg_to_hdw_argument__o__inject :
 193   I8051.register -> hdw_argument Types.sig0
 194
 195 val dpi1__o__reg_to_hdw_argument :
 196   (I8051.register, 'a1) Types.dPair -> hdw_argument
 197
 198 val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument
 199
 200 val hdw_argument_from_byte : BitVector.byte -> hdw_argument
 201
 202 val dpi1__o__byte_to_hdw_argument__o__inject :
 203   (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
 204
 205 val eject__o__byte_to_hdw_argument__o__inject :
 206   BitVector.byte Types.sig0 -> psd_argument Types.sig0
 207
 208 val byte_to_hdw_argument__o__inject :
 209   BitVector.byte -> psd_argument Types.sig0
 210
 211 val dpi1__o__byte_to_hdw_argument :
 212   (BitVector.byte, 'a1) Types.dPair -> psd_argument
 213
 214 val eject__o__byte_to_hdw_argument :
 215   BitVector.byte Types.sig0 -> psd_argument
 216
 217 val byte_of_nat : Nat.nat -> BitVector.byte
 218
 219 val zero_byte : BitVector.byte
 220
 221 type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
 222                              has_tailcalls : Bool.bool }
 223
 224 val unserialized_params_rect_Type4 :
 225   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 226   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 227   unserialized_params -> 'a1
 228
 229 val unserialized_params_rect_Type5 :
 230   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 231   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 232   unserialized_params -> 'a1
 233
 234 val unserialized_params_rect_Type3 :
 235   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 236   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 237   unserialized_params -> 'a1
 238
 239 val unserialized_params_rect_Type2 :
 240   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 241   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 242   unserialized_params -> 'a1
 243
 244 val unserialized_params_rect_Type1 :
 245   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 246   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 247   unserialized_params -> 'a1
 248
 249 val unserialized_params_rect_Type0 :
 250   (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 251   -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 252   unserialized_params -> 'a1
 253
 254 type acc_a_reg
 255
 256 type acc_b_reg
 257
 258 type acc_a_arg
 259
 260 type acc_b_arg
 261
 262 type dpl_reg
 263
 264 type dph_reg
 265
 266 type dpl_arg
 267
 268 type dph_arg
 269
 270 type snd_arg
 271
 272 type pair_move
 273
 274 type call_args
 275
 276 type call_dest
 277
 278 type ext_seq
 279
 280 val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list
 281
 282 val has_tailcalls : unserialized_params -> Bool.bool
 283
 284 type paramsT
 285
 286 val unserialized_params_inv_rect_Type4 :
 287   unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 288   -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
 289   __ -> __ -> 'a1) -> 'a1
 290
 291 val unserialized_params_inv_rect_Type3 :
 292   unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 293   -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
 294   __ -> __ -> 'a1) -> 'a1
 295
 296 val unserialized_params_inv_rect_Type2 :
 297   unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 298   -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
 299   __ -> __ -> 'a1) -> 'a1
 300
 301 val unserialized_params_inv_rect_Type1 :
 302   unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 303   -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
 304   __ -> __ -> 'a1) -> 'a1
 305
 306 val unserialized_params_inv_rect_Type0 :
 307   unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
 308   -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
 309   __ -> __ -> 'a1) -> 'a1
 310
 311 val unserialized_params_jmdiscr :
 312   unserialized_params -> unserialized_params -> __
 313
 314 type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
 315                                             List.list);
 316                                acc_b_regs : (__ -> Registers.register
 317                                             List.list);
 318                                acc_a_args : (__ -> Registers.register
 319                                             List.list);
 320                                acc_b_args : (__ -> Registers.register
 321                                             List.list);
 322                                dpl_regs : (__ -> Registers.register
 323                                           List.list);
 324                                dph_regs : (__ -> Registers.register
 325                                           List.list);
 326                                dpl_args : (__ -> Registers.register
 327                                           List.list);
 328                                dph_args : (__ -> Registers.register
 329                                           List.list);
 330                                snd_args : (__ -> Registers.register
 331                                           List.list);
 332                                pair_move_regs : (__ -> Registers.register
 333                                                 List.list);
 334                                f_call_args : (__ -> Registers.register
 335                                              List.list);
 336                                f_call_dest : (__ -> Registers.register
 337                                              List.list);
 338                                ext_seq_regs : (__ -> Registers.register
 339                                               List.list);
 340                                params_regs : (__ -> Registers.register
 341                                              List.list) }
 342
 343 val get_pseudo_reg_functs_rect_Type4 :
 344   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 345   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 346   (__ -> Registers.register List.list) -> (__ -> Registers.register
 347   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 348   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 349   (__ -> Registers.register List.list) -> (__ -> Registers.register
 350   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 351   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 352   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 353   'a1
 354
 355 val get_pseudo_reg_functs_rect_Type5 :
 356   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 357   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 358   (__ -> Registers.register List.list) -> (__ -> Registers.register
 359   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 360   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 361   (__ -> Registers.register List.list) -> (__ -> Registers.register
 362   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 363   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 364   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 365   'a1
 366
 367 val get_pseudo_reg_functs_rect_Type3 :
 368   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 369   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 370   (__ -> Registers.register List.list) -> (__ -> Registers.register
 371   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 372   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 373   (__ -> Registers.register List.list) -> (__ -> Registers.register
 374   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 375   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 376   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 377   'a1
 378
 379 val get_pseudo_reg_functs_rect_Type2 :
 380   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 381   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 382   (__ -> Registers.register List.list) -> (__ -> Registers.register
 383   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 384   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 385   (__ -> Registers.register List.list) -> (__ -> Registers.register
 386   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 387   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 388   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 389   'a1
 390
 391 val get_pseudo_reg_functs_rect_Type1 :
 392   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 393   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 394   (__ -> Registers.register List.list) -> (__ -> Registers.register
 395   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 396   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 397   (__ -> Registers.register List.list) -> (__ -> Registers.register
 398   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 399   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 400   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 401   'a1
 402
 403 val get_pseudo_reg_functs_rect_Type0 :
 404   unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 405   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 406   (__ -> Registers.register List.list) -> (__ -> Registers.register
 407   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 408   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 409   (__ -> Registers.register List.list) -> (__ -> Registers.register
 410   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 411   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 412   (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 413   'a1
 414
 415 val acc_a_regs :
 416   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 417   List.list
 418
 419 val acc_b_regs :
 420   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 421   List.list
 422
 423 val acc_a_args :
 424   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 425   List.list
 426
 427 val acc_b_args :
 428   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 429   List.list
 430
 431 val dpl_regs :
 432   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 433   List.list
 434
 435 val dph_regs :
 436   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 437   List.list
 438
 439 val dpl_args :
 440   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 441   List.list
 442
 443 val dph_args :
 444   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 445   List.list
 446
 447 val snd_args :
 448   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 449   List.list
 450
 451 val pair_move_regs :
 452   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 453   List.list
 454
 455 val f_call_args :
 456   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 457   List.list
 458
 459 val f_call_dest :
 460   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 461   List.list
 462
 463 val ext_seq_regs :
 464   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 465   List.list
 466
 467 val params_regs :
 468   unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 469   List.list
 470
 471 val get_pseudo_reg_functs_inv_rect_Type4 :
 472   unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
 473   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 474   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 475   (__ -> Registers.register List.list) -> (__ -> Registers.register
 476   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 477   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 478   (__ -> Registers.register List.list) -> (__ -> Registers.register
 479   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 480   Registers.register List.list) -> (__ -> Registers.register List.list) -> __
 481   -> 'a1) -> 'a1
 482
 483 val get_pseudo_reg_functs_inv_rect_Type3 :
 484   unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
 485   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 486   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 487   (__ -> Registers.register List.list) -> (__ -> Registers.register
 488   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 489   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 490   (__ -> Registers.register List.list) -> (__ -> Registers.register
 491   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 492   Registers.register List.list) -> (__ -> Registers.register List.list) -> __
 493   -> 'a1) -> 'a1
 494
 495 val get_pseudo_reg_functs_inv_rect_Type2 :
 496   unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
 497   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 498   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 499   (__ -> Registers.register List.list) -> (__ -> Registers.register
 500   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 501   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 502   (__ -> Registers.register List.list) -> (__ -> Registers.register
 503   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 504   Registers.register List.list) -> (__ -> Registers.register List.list) -> __
 505   -> 'a1) -> 'a1
 506
 507 val get_pseudo_reg_functs_inv_rect_Type1 :
 508   unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
 509   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 510   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 511   (__ -> Registers.register List.list) -> (__ -> Registers.register
 512   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 513   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 514   (__ -> Registers.register List.list) -> (__ -> Registers.register
 515   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 516   Registers.register List.list) -> (__ -> Registers.register List.list) -> __
 517   -> 'a1) -> 'a1
 518
 519 val get_pseudo_reg_functs_inv_rect_Type0 :
 520   unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
 521   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 522   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 523   (__ -> Registers.register List.list) -> (__ -> Registers.register
 524   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 525   Registers.register List.list) -> (__ -> Registers.register List.list) ->
 526   (__ -> Registers.register List.list) -> (__ -> Registers.register
 527   List.list) -> (__ -> Registers.register List.list) -> (__ ->
 528   Registers.register List.list) -> (__ -> Registers.register List.list) -> __
 529   -> 'a1) -> 'a1
 530
 531 val get_pseudo_reg_functs_jmdiscr :
 532   unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs -> __
 533
 534 type uns_params = { u_pars : unserialized_params;
 535                     functs : get_pseudo_reg_functs }
 536
 537 val uns_params_rect_Type4 :
 538   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 539
 540 val uns_params_rect_Type5 :
 541   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 542
 543 val uns_params_rect_Type3 :
 544   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 545
 546 val uns_params_rect_Type2 :
 547   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 548
 549 val uns_params_rect_Type1 :
 550   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 551
 552 val uns_params_rect_Type0 :
 553   (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
 554
 555 val u_pars : uns_params -> unserialized_params
 556
 557 val functs : uns_params -> get_pseudo_reg_functs
 558
 559 val uns_params_inv_rect_Type4 :
 560   uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 561   -> 'a1
 562
 563 val uns_params_inv_rect_Type3 :
 564   uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 565   -> 'a1
 566
 567 val uns_params_inv_rect_Type2 :
 568   uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 569   -> 'a1
 570
 571 val uns_params_inv_rect_Type1 :
 572   uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 573   -> 'a1
 574
 575 val uns_params_inv_rect_Type0 :
 576   uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 577   -> 'a1
 578
 579 val uns_params_jmdiscr : uns_params -> uns_params -> __
 580
 581 type joint_seq =
 582 | COMMENT of String.string
 583 | MOVE of __
 584 | POP of __
 585 | PUSH of __
 586 | ADDRESS of AST.ident * BitVector.word * __ * __
 587 | OPACCS of BackEndOps.opAccs * __ * __ * __ * __
 588 | OP1 of BackEndOps.op1 * __ * __
 589 | OP2 of BackEndOps.op2 * __ * __ * __
 590 | CLEAR_CARRY
 591 | SET_CARRY
 592 | LOAD of __ * __ * __
 593 | STORE of __ * __ * __
 594 | Extension_seq of __
 595
 596 val joint_seq_rect_Type4 :
 597   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 598   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 599   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 600   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 601   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 602   -> (__ -> 'a1) -> joint_seq -> 'a1
 603
 604 val joint_seq_rect_Type5 :
 605   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 606   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 607   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 608   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 609   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 610   -> (__ -> 'a1) -> joint_seq -> 'a1
 611
 612 val joint_seq_rect_Type3 :
 613   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 614   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 615   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 616   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 617   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 618   -> (__ -> 'a1) -> joint_seq -> 'a1
 619
 620 val joint_seq_rect_Type2 :
 621   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 622   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 623   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 624   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 625   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 626   -> (__ -> 'a1) -> joint_seq -> 'a1
 627
 628 val joint_seq_rect_Type1 :
 629   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 630   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 631   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 632   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 633   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 634   -> (__ -> 'a1) -> joint_seq -> 'a1
 635
 636 val joint_seq_rect_Type0 :
 637   unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
 638   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
 639   -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
 640   -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
 641   -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
 642   -> (__ -> 'a1) -> joint_seq -> 'a1
 643
 644 val joint_seq_inv_rect_Type4 :
 645   unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
 646   -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
 647   'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
 648   (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
 649   -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
 650   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
 651   -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
 652
 653 val joint_seq_inv_rect_Type3 :
 654   unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
 655   -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
 656   'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
 657   (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
 658   -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
 659   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
 660   -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
 661
 662 val joint_seq_inv_rect_Type2 :
 663   unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
 664   -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
 665   'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
 666   (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
 667   -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
 668   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
 669   -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
 670
 671 val joint_seq_inv_rect_Type1 :
 672   unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
 673   -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
 674   'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
 675   (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
 676   -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
 677   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
 678   -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
 679
 680 val joint_seq_inv_rect_Type0 :
 681   unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
 682   -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
 683   'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
 684   (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
 685   -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
 686   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
 687   -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
 688
 689 val joint_seq_discr :
 690   unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
 691
 692 val joint_seq_jmdiscr :
 693   unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
 694
 695 val get_used_registers_from_seq :
 696   unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
 697   joint_seq -> Registers.register List.list
 698
 699 val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
 700
 701 val dpi1__o__extension_seq_to_seq__o__inject :
 702   unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
 703   joint_seq Types.sig0
 704
 705 val eject__o__extension_seq_to_seq__o__inject :
 706   unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
 707   Types.sig0
 708
 709 val extension_seq_to_seq__o__inject :
 710   unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0
 711
 712 val dpi1__o__extension_seq_to_seq :
 713   unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
 714   joint_seq
 715
 716 val eject__o__extension_seq_to_seq :
 717   unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
 718
 719 type joint_step =
 720 | COST_LABEL of CostLabel.costlabel
 721 | CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
 722 | COND of __ * Graphs.label
 723 | Step_seq of joint_seq
 724
 725 val joint_step_rect_Type4 :
 726   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 727   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 728   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 729
 730 val joint_step_rect_Type5 :
 731   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 732   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 733   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 734
 735 val joint_step_rect_Type3 :
 736   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 737   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 738   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 739
 740 val joint_step_rect_Type2 :
 741   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 742   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 743   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 744
 745 val joint_step_rect_Type1 :
 746   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 747   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 748   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 749
 750 val joint_step_rect_Type0 :
 751   unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
 752   -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
 753   -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
 754
 755 val joint_step_inv_rect_Type4 :
 756   unserialized_params -> AST.ident List.list -> joint_step ->
 757   (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
 758   Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
 759   (joint_seq -> __ -> 'a1) -> 'a1
 760
 761 val joint_step_inv_rect_Type3 :
 762   unserialized_params -> AST.ident List.list -> joint_step ->
 763   (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
 764   Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
 765   (joint_seq -> __ -> 'a1) -> 'a1
 766
 767 val joint_step_inv_rect_Type2 :
 768   unserialized_params -> AST.ident List.list -> joint_step ->
 769   (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
 770   Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
 771   (joint_seq -> __ -> 'a1) -> 'a1
 772
 773 val joint_step_inv_rect_Type1 :
 774   unserialized_params -> AST.ident List.list -> joint_step ->
 775   (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
 776   Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
 777   (joint_seq -> __ -> 'a1) -> 'a1
 778
 779 val joint_step_inv_rect_Type0 :
 780   unserialized_params -> AST.ident List.list -> joint_step ->
 781   (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
 782   Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
 783   (joint_seq -> __ -> 'a1) -> 'a1
 784
 785 val joint_step_discr :
 786   unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
 787   __
 788
 789 val joint_step_jmdiscr :
 790   unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
 791   __
 792
 793 val get_used_registers_from_step :
 794   unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
 795   joint_step -> Registers.register List.list
 796
 797 val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
 798   unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
 799   joint_step Types.sig0
 800
 801 val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
 802   unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
 803   Types.sig0
 804
 805 val extension_seq_to_seq__o__seq_to_step__o__inject :
 806   unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0
 807
 808 val dpi1__o__seq_to_step__o__inject :
 809   unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
 810   -> joint_step Types.sig0
 811
 812 val eject__o__seq_to_step__o__inject :
 813   unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
 814   joint_step Types.sig0
 815
 816 val seq_to_step__o__inject :
 817   unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
 818   Types.sig0
 819
 820 val dpi1__o__extension_seq_to_seq__o__seq_to_step :
 821   unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
 822   joint_step
 823
 824 val eject__o__extension_seq_to_seq__o__seq_to_step :
 825   unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
 826
 827 val extension_seq_to_seq__o__seq_to_step :
 828   unserialized_params -> AST.ident List.list -> __ -> joint_step
 829
 830 val dpi1__o__seq_to_step :
 831   unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
 832   -> joint_step
 833
 834 val eject__o__seq_to_step :
 835   unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
 836   joint_step
 837
 838 val step_labels :
 839   unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
 840   List.list
 841
 842 type stmt_params = { uns_pars : uns_params;
 843                      succ_label : (__ -> Graphs.label Types.option);
 844                      has_fcond : Bool.bool }
 845
 846 val stmt_params_rect_Type4 :
 847   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 848   -> stmt_params -> 'a1
 849
 850 val stmt_params_rect_Type5 :
 851   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 852   -> stmt_params -> 'a1
 853
 854 val stmt_params_rect_Type3 :
 855   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 856   -> stmt_params -> 'a1
 857
 858 val stmt_params_rect_Type2 :
 859   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 860   -> stmt_params -> 'a1
 861
 862 val stmt_params_rect_Type1 :
 863   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 864   -> stmt_params -> 'a1
 865
 866 val stmt_params_rect_Type0 :
 867   (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
 868   -> stmt_params -> 'a1
 869
 870 val uns_pars : stmt_params -> uns_params
 871
 872 type succ
 873
 874 val succ_label : stmt_params -> __ -> Graphs.label Types.option
 875
 876 val has_fcond : stmt_params -> Bool.bool
 877
 878 val stmt_params_inv_rect_Type4 :
 879   stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
 880   Bool.bool -> __ -> 'a1) -> 'a1
 881
 882 val stmt_params_inv_rect_Type3 :
 883   stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
 884   Bool.bool -> __ -> 'a1) -> 'a1
 885
 886 val stmt_params_inv_rect_Type2 :
 887   stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
 888   Bool.bool -> __ -> 'a1) -> 'a1
 889
 890 val stmt_params_inv_rect_Type1 :
 891   stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
 892   Bool.bool -> __ -> 'a1) -> 'a1
 893
 894 val stmt_params_inv_rect_Type0 :
 895   stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
 896   Bool.bool -> __ -> 'a1) -> 'a1
 897
 898 val stmt_params_jmdiscr : stmt_params -> stmt_params -> __
 899
 900 val uns_pars__o__u_pars : stmt_params -> unserialized_params
 901
 902 type joint_fin_step =
 903 | GOTO of Graphs.label
 904 | RETURN
 905 | TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
 906
 907 val joint_fin_step_rect_Type4 :
 908   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 909   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 910
 911 val joint_fin_step_rect_Type5 :
 912   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 913   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 914
 915 val joint_fin_step_rect_Type3 :
 916   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 917   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 918
 919 val joint_fin_step_rect_Type2 :
 920   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 921   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 922
 923 val joint_fin_step_rect_Type1 :
 924   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 925   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 926
 927 val joint_fin_step_rect_Type0 :
 928   unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
 929   (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
 930
 931 val joint_fin_step_inv_rect_Type4 :
 932   unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
 933   -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
 934   'a1) -> 'a1
 935
 936 val joint_fin_step_inv_rect_Type3 :
 937   unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
 938   -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
 939   'a1) -> 'a1
 940
 941 val joint_fin_step_inv_rect_Type2 :
 942   unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
 943   -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
 944   'a1) -> 'a1
 945
 946 val joint_fin_step_inv_rect_Type1 :
 947   unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
 948   -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
 949   'a1) -> 'a1
 950
 951 val joint_fin_step_inv_rect_Type0 :
 952   unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
 953   -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
 954   'a1) -> 'a1
 955
 956 val joint_fin_step_discr :
 957   unserialized_params -> joint_fin_step -> joint_fin_step -> __
 958
 959 val joint_fin_step_jmdiscr :
 960   unserialized_params -> joint_fin_step -> joint_fin_step -> __
 961
 962 val fin_step_labels :
 963   unserialized_params -> joint_fin_step -> Graphs.label List.list
 964
 965 type joint_statement =
 966 | Sequential of joint_step * __
 967 | Final of joint_fin_step
 968 | FCOND of __ * Graphs.label * Graphs.label
 969
 970 val joint_statement_rect_Type4 :
 971   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 972   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 973   'a1) -> joint_statement -> 'a1
 974
 975 val joint_statement_rect_Type5 :
 976   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 977   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 978   'a1) -> joint_statement -> 'a1
 979
 980 val joint_statement_rect_Type3 :
 981   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 982   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 983   'a1) -> joint_statement -> 'a1
 984
 985 val joint_statement_rect_Type2 :
 986   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 987   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 988   'a1) -> joint_statement -> 'a1
 989
 990 val joint_statement_rect_Type1 :
 991   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 992   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 993   'a1) -> joint_statement -> 'a1
 994
 995 val joint_statement_rect_Type0 :
 996   stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
 997   (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
 998   'a1) -> joint_statement -> 'a1
 999
1000 val joint_statement_inv_rect_Type4 :
1001   stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1002   -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1003   -> Graphs.label -> __ -> 'a1) -> 'a1
1004
1005 val joint_statement_inv_rect_Type3 :
1006   stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1007   -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1008   -> Graphs.label -> __ -> 'a1) -> 'a1
1009
1010 val joint_statement_inv_rect_Type2 :
1011   stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1012   -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1013   -> Graphs.label -> __ -> 'a1) -> 'a1
1014
1015 val joint_statement_inv_rect_Type1 :
1016   stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1017   -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1018   -> Graphs.label -> __ -> 'a1) -> 'a1
1019
1020 val joint_statement_inv_rect_Type0 :
1021   stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1022   -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1023   -> Graphs.label -> __ -> 'a1) -> 'a1
1024
1025 val joint_statement_discr :
1026   stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1027   __
1028
1029 val joint_statement_jmdiscr :
1030   stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1031   __
1032
1033 val dpi1__o__fin_step_to_stmt__o__inject :
1034   stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1035   joint_statement Types.sig0
1036
1037 val eject__o__fin_step_to_stmt__o__inject :
1038   stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1039   joint_statement Types.sig0
1040
1041 val fin_step_to_stmt__o__inject :
1042   stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1043   Types.sig0
1044
1045 val dpi1__o__fin_step_to_stmt :
1046   stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1047   joint_statement
1048
1049 val eject__o__fin_step_to_stmt :
1050   stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1051   joint_statement
1052
1053 type params = { stmt_pars : stmt_params;
1054                 stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1055                           Types.option);
1056                 point_of_label : (AST.ident List.list -> __ -> Graphs.label
1057                                  -> __ Types.option);
1058                 point_of_succ : (__ -> __ -> __) }
1059
1060 val params_rect_Type4 :
1061   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1062   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1063   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1064
1065 val params_rect_Type5 :
1066   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1067   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1068   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1069
1070 val params_rect_Type3 :
1071   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1072   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1073   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1074
1075 val params_rect_Type2 :
1076   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1077   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1078   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1079
1080 val params_rect_Type1 :
1081   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1082   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1083   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1084
1085 val params_rect_Type0 :
1086   (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1087   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1088   -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1089
1090 val stmt_pars : params -> stmt_params
1091
1092 type codeT
1093
1094 type code_point
1095
1096 val stmt_at :
1097   params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option
1098
1099 val point_of_label :
1100   params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option
1101
1102 val point_of_succ : params -> __ -> __ -> __
1103
1104 val params_inv_rect_Type4 :
1105   params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1106   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1107   -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1108
1109 val params_inv_rect_Type3 :
1110   params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1111   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1112   -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1113
1114 val params_inv_rect_Type2 :
1115   params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1116   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1117   -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1118
1119 val params_inv_rect_Type1 :
1120   params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1121   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1122   -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1123
1124 val params_inv_rect_Type0 :
1125   params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1126   joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1127   -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1128
1129 val params_jmdiscr : params -> params -> __
1130
1131 val stmt_pars__o__uns_pars : params -> uns_params
1132
1133 val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params
1134
1135 val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool
1136
1137 val code_has_label :
1138   params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool
1139
1140 val stmt_explicit_labels :
1141   stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1142   List.list
1143
1144 val stmt_implicit_label :
1145   stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1146   Types.option
1147
1148 val stmt_labels :
1149   stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1150   List.list
1151
1152 val stmt_registers :
1153   stmt_params -> AST.ident List.list -> joint_statement -> Registers.register
1154   List.list
1155
1156 type lin_params =
1157   uns_params
1158   (* singleton inductive, whose constructor was mk_lin_params *)
1159
1160 val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1
1161
1162 val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1
1163
1164 val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1
1165
1166 val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1
1167
1168 val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1
1169
1170 val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1
1171
1172 val l_u_pars : lin_params -> uns_params
1173
1174 val lin_params_inv_rect_Type4 :
1175   lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1176
1177 val lin_params_inv_rect_Type3 :
1178   lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1179
1180 val lin_params_inv_rect_Type2 :
1181   lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1182
1183 val lin_params_inv_rect_Type1 :
1184   lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1185
1186 val lin_params_inv_rect_Type0 :
1187   lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1188
1189 val lin_params_jmdiscr : lin_params -> lin_params -> __
1190
1191 val lin_params_to_params : lin_params -> params
1192
1193 val lp_to_p__o__stmt_pars : lin_params -> stmt_params
1194
1195 val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params
1196
1197 val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1198   lin_params -> unserialized_params
1199
1200 type graph_params =
1201   uns_params
1202   (* singleton inductive, whose constructor was mk_graph_params *)
1203
1204 val graph_params_rect_Type4 : (uns_params -> 'a1) -> graph_params -> 'a1
1205
1206 val graph_params_rect_Type5 : (uns_params -> 'a1) -> graph_params -> 'a1
1207
1208 val graph_params_rect_Type3 : (uns_params -> 'a1) -> graph_params -> 'a1
1209
1210 val graph_params_rect_Type2 : (uns_params -> 'a1) -> graph_params -> 'a1
1211
1212 val graph_params_rect_Type1 : (uns_params -> 'a1) -> graph_params -> 'a1
1213
1214 val graph_params_rect_Type0 : (uns_params -> 'a1) -> graph_params -> 'a1
1215
1216 val g_u_pars : graph_params -> uns_params
1217
1218 val graph_params_inv_rect_Type4 :
1219   graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1220
1221 val graph_params_inv_rect_Type3 :
1222   graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1223
1224 val graph_params_inv_rect_Type2 :
1225   graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1226
1227 val graph_params_inv_rect_Type1 :
1228   graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1229
1230 val graph_params_inv_rect_Type0 :
1231   graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1232
1233 val graph_params_jmdiscr : graph_params -> graph_params -> __
1234
1235 val graph_params_to_params : graph_params -> params
1236
1237 val gp_to_p__o__stmt_pars : graph_params -> stmt_params
1238
1239 val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params
1240
1241 val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1242   graph_params -> unserialized_params
1243
1244 type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1245                                  joint_if_runiverse : Identifiers.universe;
1246                                  joint_if_result : __; joint_if_params :
1247                                  __; joint_if_stacksize : Nat.nat;
1248                                  joint_if_local_stacksize : Nat.nat;
1249                                  joint_if_code : __; joint_if_entry :
1250                                  __ }
1251
1252 val joint_internal_function_rect_Type4 :
1253   params -> AST.ident List.list -> (Identifiers.universe ->
1254   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1255   -> joint_internal_function -> 'a1
1256
1257 val joint_internal_function_rect_Type5 :
1258   params -> AST.ident List.list -> (Identifiers.universe ->
1259   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1260   -> joint_internal_function -> 'a1
1261
1262 val joint_internal_function_rect_Type3 :
1263   params -> AST.ident List.list -> (Identifiers.universe ->
1264   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1265   -> joint_internal_function -> 'a1
1266
1267 val joint_internal_function_rect_Type2 :
1268   params -> AST.ident List.list -> (Identifiers.universe ->
1269   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1270   -> joint_internal_function -> 'a1
1271
1272 val joint_internal_function_rect_Type1 :
1273   params -> AST.ident List.list -> (Identifiers.universe ->
1274   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1275   -> joint_internal_function -> 'a1
1276
1277 val joint_internal_function_rect_Type0 :
1278   params -> AST.ident List.list -> (Identifiers.universe ->
1279   Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1280   -> joint_internal_function -> 'a1
1281
1282 val joint_if_luniverse :
1283   params -> AST.ident List.list -> joint_internal_function ->
1284   Identifiers.universe
1285
1286 val joint_if_runiverse :
1287   params -> AST.ident List.list -> joint_internal_function ->
1288   Identifiers.universe
1289
1290 val joint_if_result :
1291   params -> AST.ident List.list -> joint_internal_function -> __
1292
1293 val joint_if_params :
1294   params -> AST.ident List.list -> joint_internal_function -> __
1295
1296 val joint_if_stacksize :
1297   params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1298
1299 val joint_if_local_stacksize :
1300   params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1301
1302 val joint_if_code :
1303   params -> AST.ident List.list -> joint_internal_function -> __
1304
1305 val joint_if_entry :
1306   params -> AST.ident List.list -> joint_internal_function -> __
1307
1308 val joint_internal_function_inv_rect_Type4 :
1309   params -> AST.ident List.list -> joint_internal_function ->
1310   (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1311   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1312
1313 val joint_internal_function_inv_rect_Type3 :
1314   params -> AST.ident List.list -> joint_internal_function ->
1315   (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1316   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1317
1318 val joint_internal_function_inv_rect_Type2 :
1319   params -> AST.ident List.list -> joint_internal_function ->
1320   (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1321   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1322
1323 val joint_internal_function_inv_rect_Type1 :
1324   params -> AST.ident List.list -> joint_internal_function ->
1325   (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1326   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1327
1328 val joint_internal_function_inv_rect_Type0 :
1329   params -> AST.ident List.list -> joint_internal_function ->
1330   (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1331   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1332
1333 val joint_internal_function_jmdiscr :
1334   params -> AST.ident List.list -> joint_internal_function ->
1335   joint_internal_function -> __
1336
1337 val good_if_rect_Type4 :
1338   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1339   -> __ -> __ -> 'a1) -> 'a1
1340
1341 val good_if_rect_Type5 :
1342   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1343   -> __ -> __ -> 'a1) -> 'a1
1344
1345 val good_if_rect_Type3 :
1346   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1347   -> __ -> __ -> 'a1) -> 'a1
1348
1349 val good_if_rect_Type2 :
1350   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1351   -> __ -> __ -> 'a1) -> 'a1
1352
1353 val good_if_rect_Type1 :
1354   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1355   -> __ -> __ -> 'a1) -> 'a1
1356
1357 val good_if_rect_Type0 :
1358   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1359   -> __ -> __ -> 'a1) -> 'a1
1360
1361 val good_if_inv_rect_Type4 :
1362   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1363   -> __ -> __ -> __ -> 'a1) -> 'a1
1364
1365 val good_if_inv_rect_Type3 :
1366   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1367   -> __ -> __ -> __ -> 'a1) -> 'a1
1368
1369 val good_if_inv_rect_Type2 :
1370   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1371   -> __ -> __ -> __ -> 'a1) -> 'a1
1372
1373 val good_if_inv_rect_Type1 :
1374   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1375   -> __ -> __ -> __ -> 'a1) -> 'a1
1376
1377 val good_if_inv_rect_Type0 :
1378   params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1379   -> __ -> __ -> __ -> 'a1) -> 'a1
1380
1381 val good_if_discr :
1382   params -> AST.ident List.list -> joint_internal_function -> __
1383
1384 val good_if_jmdiscr :
1385   params -> AST.ident List.list -> joint_internal_function -> __
1386
1387 type joint_closed_internal_function = joint_internal_function Types.sig0
1388
1389 val set_joint_code :
1390   AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
1391   joint_internal_function
1392
1393 val set_luniverse :
1394   params -> AST.ident List.list -> joint_internal_function ->
1395   Identifiers.universe -> joint_internal_function
1396
1397 val set_runiverse :
1398   params -> AST.ident List.list -> joint_internal_function ->
1399   Identifiers.universe -> joint_internal_function
1400
1401 val add_graph :
1402   graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1403   joint_internal_function -> joint_internal_function
1404
1405 type joint_function = joint_closed_internal_function AST.fundef
1406
1407 type joint_program = { jp_functions : AST.ident List.list;
1408                        joint_prog : (joint_function, AST.init_data List.list)
1409                                     AST.program;
1410                        init_cost_label : CostLabel.costlabel }
1411
1412 val joint_program_rect_Type4 :
1413   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1414   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1415
1416 val joint_program_rect_Type5 :
1417   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1418   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1419
1420 val joint_program_rect_Type3 :
1421   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1422   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1423
1424 val joint_program_rect_Type2 :
1425   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1426   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1427
1428 val joint_program_rect_Type1 :
1429   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1430   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1431
1432 val joint_program_rect_Type0 :
1433   params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1434   AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1435
1436 val jp_functions : params -> joint_program -> AST.ident List.list
1437
1438 val joint_prog :
1439   params -> joint_program -> (joint_function, AST.init_data List.list)
1440   AST.program
1441
1442 val init_cost_label : params -> joint_program -> CostLabel.costlabel
1443
1444 val joint_program_inv_rect_Type4 :
1445   params -> joint_program -> (AST.ident List.list -> (joint_function,
1446   AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1447   'a1) -> 'a1
1448
1449 val joint_program_inv_rect_Type3 :
1450   params -> joint_program -> (AST.ident List.list -> (joint_function,
1451   AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1452   'a1) -> 'a1
1453
1454 val joint_program_inv_rect_Type2 :
1455   params -> joint_program -> (AST.ident List.list -> (joint_function,
1456   AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1457   'a1) -> 'a1
1458
1459 val joint_program_inv_rect_Type1 :
1460   params -> joint_program -> (AST.ident List.list -> (joint_function,
1461   AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1462   'a1) -> 'a1
1463
1464 val joint_program_inv_rect_Type0 :
1465   params -> joint_program -> (AST.ident List.list -> (joint_function,
1466   AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1467   'a1) -> 'a1
1468
1469 val joint_program_discr : params -> joint_program -> joint_program -> __
1470
1471 val joint_program_jmdiscr : params -> joint_program -> joint_program -> __
1472
1473 val dpi1__o__joint_prog__o__inject :
1474   params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1475   AST.init_data List.list) AST.program Types.sig0
1476
1477 val eject__o__joint_prog__o__inject :
1478   params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1479   List.list) AST.program Types.sig0
1480
1481 val joint_prog__o__inject :
1482   params -> joint_program -> (joint_function, AST.init_data List.list)
1483   AST.program Types.sig0
1484
1485 val dpi1__o__joint_prog :
1486   params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1487   AST.init_data List.list) AST.program
1488
1489 val eject__o__joint_prog :
1490   params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1491   List.list) AST.program
1492
1493 val prog_names : params -> joint_program -> AST.ident List.list
1494
1495 val transform_joint_program :
1496   params -> params -> (AST.ident List.list -> joint_closed_internal_function
1497   -> joint_closed_internal_function) -> joint_program -> joint_program
1498
1499 type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
1500
1501 val stack_cost : params -> joint_program -> stack_cost_model
1502
1503 open Extra_bool
1504
1505 open Coqlib
1506
1507 open Values
1508
1509 open FrontEndVal
1510
1511 open GenMem
1512
1513 open FrontEndMem
1514
1515 open Globalenvs
1516
1517 val globals_stacksize : params -> joint_program -> Nat.nat
1518