extracted/joint_printer.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 type keyword =
 122 | KwCOMMENT
 123 | KwMOVE
 124 | KwPOP
 125 | KwPUSH
 126 | KwADDRESS
 127 | KwOPACCS
 128 | KwOP1
 129 | KwOP2
 130 | KwCLEAR_CARRY
 131 | KwSET_CARRY
 132 | KwLOAD
 133 | KwSTORE
 134 | KwCOST_LABEL
 135 | KwCOND
 136 | KwCALL
 137 | KwGOTO
 138 | KwRETURN
 139 | KwTAILCALL
 140 | KwFCOND
 141
 142 val keyword_rect_Type4 :
 143   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 144   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 145
 146 val keyword_rect_Type5 :
 147   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 148   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 149
 150 val keyword_rect_Type3 :
 151   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 152   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 153
 154 val keyword_rect_Type2 :
 155   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 156   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 157
 158 val keyword_rect_Type1 :
 159   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 160   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 161
 162 val keyword_rect_Type0 :
 163   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 164   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
 165
 166 val keyword_inv_rect_Type4 :
 167   keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 168   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 169   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 170   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 171
 172 val keyword_inv_rect_Type3 :
 173   keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 174   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 175   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 176   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 177
 178 val keyword_inv_rect_Type2 :
 179   keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 180   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 181   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 182   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 183
 184 val keyword_inv_rect_Type1 :
 185   keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 186   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 187   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 188   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 189
 190 val keyword_inv_rect_Type0 :
 191   keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 192   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 193   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 194   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 195
 196 val keyword_discr : keyword -> keyword -> __
 197
 198 val keyword_jmdiscr : keyword -> keyword -> __
 199
 200 type 'string printing_pass_independent_params = { print_String : (String.string
 201                                                                  -> 'string);
 202                                                   print_keyword : (keyword ->
 203                                                                   'string);
 204                                                   print_concat : ('string ->
 205                                                                  'string ->
 206                                                                  'string);
 207                                                   print_empty : 'string;
 208                                                   print_ident : (AST.ident ->
 209                                                                 'string);
 210                                                   print_costlabel : (CostLabel.costlabel
 211                                                                     ->
 212                                                                     'string);
 213                                                   print_label : (Graphs.label
 214                                                                 -> 'string);
 215                                                   print_OpAccs : (BackEndOps.opAccs
 216                                                                  -> 'string);
 217                                                   print_Op1 : (BackEndOps.op1
 218                                                               -> 'string);
 219                                                   print_Op2 : (BackEndOps.op2
 220                                                               -> 'string);
 221                                                   print_nat : (Nat.nat ->
 222                                                               'string);
 223                                                   print_bitvector : (Nat.nat
 224                                                                     ->
 225                                                                     BitVector.bitVector
 226                                                                     ->
 227                                                                     'string) }
 228
 229 val printing_pass_independent_params_rect_Type4 :
 230   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 231   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 232   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 233   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 234   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 235   -> 'a2
 236
 237 val printing_pass_independent_params_rect_Type5 :
 238   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 239   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 240   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 241   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 242   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 243   -> 'a2
 244
 245 val printing_pass_independent_params_rect_Type3 :
 246   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 247   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 248   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 249   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 250   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 251   -> 'a2
 252
 253 val printing_pass_independent_params_rect_Type2 :
 254   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 255   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 256   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 257   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 258   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 259   -> 'a2
 260
 261 val printing_pass_independent_params_rect_Type1 :
 262   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 263   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 264   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 265   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 266   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 267   -> 'a2
 268
 269 val printing_pass_independent_params_rect_Type0 :
 270   ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 271   -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 272   'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 273   (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 274   BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
 275   -> 'a2
 276
 277 val print_String :
 278   'a1 printing_pass_independent_params -> String.string -> 'a1
 279
 280 val print_keyword : 'a1 printing_pass_independent_params -> keyword -> 'a1
 281
 282 val print_concat : 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1
 283
 284 val print_empty : 'a1 printing_pass_independent_params -> 'a1
 285
 286 val print_ident : 'a1 printing_pass_independent_params -> AST.ident -> 'a1
 287
 288 val print_costlabel :
 289   'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1
 290
 291 val print_label : 'a1 printing_pass_independent_params -> Graphs.label -> 'a1
 292
 293 val print_OpAccs :
 294   'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1
 295
 296 val print_Op1 : 'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1
 297
 298 val print_Op2 : 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1
 299
 300 val print_nat : 'a1 printing_pass_independent_params -> Nat.nat -> 'a1
 301
 302 val print_bitvector :
 303   'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
 304   'a1
 305
 306 val printing_pass_independent_params_inv_rect_Type4 :
 307   'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
 308   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 309   (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
 310   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
 311   -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> __ -> 'a2) -> 'a2
 312
 313 val printing_pass_independent_params_inv_rect_Type3 :
 314   'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
 315   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 316   (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
 317   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
 318   -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> __ -> 'a2) -> 'a2
 319
 320 val printing_pass_independent_params_inv_rect_Type2 :
 321   'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
 322   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 323   (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
 324   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
 325   -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> __ -> 'a2) -> 'a2
 326
 327 val printing_pass_independent_params_inv_rect_Type1 :
 328   'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
 329   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 330   (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
 331   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
 332   -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> __ -> 'a2) -> 'a2
 333
 334 val printing_pass_independent_params_inv_rect_Type0 :
 335   'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
 336   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 337   (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
 338   -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
 339   -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> __ -> 'a2) -> 'a2
 340
 341 val printing_pass_independent_params_jmdiscr :
 342   'a1 printing_pass_independent_params -> 'a1
 343   printing_pass_independent_params -> __
 344
 345 type 'string printing_params = { print_pass_ind : 'string
 346                                                   printing_pass_independent_params;
 347                                  print_acc_a_reg : (__ -> 'string);
 348                                  print_acc_b_reg : (__ -> 'string);
 349                                  print_acc_a_arg : (__ -> 'string);
 350                                  print_acc_b_arg : (__ -> 'string);
 351                                  print_dpl_reg : (__ -> 'string);
 352                                  print_dph_reg : (__ -> 'string);
 353                                  print_dpl_arg : (__ -> 'string);
 354                                  print_dph_arg : (__ -> 'string);
 355                                  print_snd_arg : (__ -> 'string);
 356                                  print_pair_move : (__ -> 'string);
 357                                  print_call_args : (__ -> 'string);
 358                                  print_call_dest : (__ -> 'string);
 359                                  print_ext_seq : (__ -> 'string) }
 360
 361 val printing_params_rect_Type4 :
 362   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 363   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 364   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 365   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 366
 367 val printing_params_rect_Type5 :
 368   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 369   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 370   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 371   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 372
 373 val printing_params_rect_Type3 :
 374   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 375   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 376   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 377   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 378
 379 val printing_params_rect_Type2 :
 380   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 381   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 382   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 383   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 384
 385 val printing_params_rect_Type1 :
 386   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 387   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 388   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 389   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 390
 391 val printing_params_rect_Type0 :
 392   Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 393   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 394   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 395   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
 396
 397 val print_pass_ind :
 398   Joint.unserialized_params -> 'a1 printing_params -> 'a1
 399   printing_pass_independent_params
 400
 401 val print_acc_a_reg :
 402   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 403
 404 val print_acc_b_reg :
 405   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 406
 407 val print_acc_a_arg :
 408   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 409
 410 val print_acc_b_arg :
 411   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 412
 413 val print_dpl_reg :
 414   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 415
 416 val print_dph_reg :
 417   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 418
 419 val print_dpl_arg :
 420   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 421
 422 val print_dph_arg :
 423   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 424
 425 val print_snd_arg :
 426   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 427
 428 val print_pair_move :
 429   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 430
 431 val print_call_args :
 432   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 433
 434 val print_call_dest :
 435   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 436
 437 val print_ext_seq :
 438   Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
 439
 440 val printing_params_inv_rect_Type4 :
 441   Joint.unserialized_params -> 'a1 printing_params -> ('a1
 442   printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 443   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 444   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 445   'a1) -> __ -> 'a2) -> 'a2
 446
 447 val printing_params_inv_rect_Type3 :
 448   Joint.unserialized_params -> 'a1 printing_params -> ('a1
 449   printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 450   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 451   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 452   'a1) -> __ -> 'a2) -> 'a2
 453
 454 val printing_params_inv_rect_Type2 :
 455   Joint.unserialized_params -> 'a1 printing_params -> ('a1
 456   printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 457   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 458   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 459   'a1) -> __ -> 'a2) -> 'a2
 460
 461 val printing_params_inv_rect_Type1 :
 462   Joint.unserialized_params -> 'a1 printing_params -> ('a1
 463   printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 464   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 465   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 466   'a1) -> __ -> 'a2) -> 'a2
 467
 468 val printing_params_inv_rect_Type0 :
 469   Joint.unserialized_params -> 'a1 printing_params -> ('a1
 470   printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 471   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 472   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 473   'a1) -> __ -> 'a2) -> 'a2
 474
 475 val printing_params_jmdiscr :
 476   Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params ->
 477   __
 478
 479 val dpi1__o__print_pass_ind__o__inject :
 480   Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
 481   printing_pass_independent_params Types.sig0
 482
 483 val eject__o__print_pass_ind__o__inject :
 484   Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
 485   printing_pass_independent_params Types.sig0
 486
 487 val print_pass_ind__o__inject :
 488   Joint.unserialized_params -> 'a1 printing_params -> 'a1
 489   printing_pass_independent_params Types.sig0
 490
 491 val dpi1__o__print_pass_ind :
 492   Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
 493   printing_pass_independent_params
 494
 495 val eject__o__print_pass_ind :
 496   Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
 497   printing_pass_independent_params
 498
 499 type 'string print_serialization_params = { print_succ : (__ -> 'string);
 500                                             print_code_point : (__ ->
 501                                                                'string) }
 502
 503 val print_serialization_params_rect_Type4 :
 504   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 505   print_serialization_params -> 'a2
 506
 507 val print_serialization_params_rect_Type5 :
 508   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 509   print_serialization_params -> 'a2
 510
 511 val print_serialization_params_rect_Type3 :
 512   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 513   print_serialization_params -> 'a2
 514
 515 val print_serialization_params_rect_Type2 :
 516   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 517   print_serialization_params -> 'a2
 518
 519 val print_serialization_params_rect_Type1 :
 520   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 521   print_serialization_params -> 'a2
 522
 523 val print_serialization_params_rect_Type0 :
 524   Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 525   print_serialization_params -> 'a2
 526
 527 val print_succ : Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
 528
 529 val print_code_point :
 530   Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
 531
 532 val print_serialization_params_inv_rect_Type4 :
 533   Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
 534   'a1) -> __ -> 'a2) -> 'a2
 535
 536 val print_serialization_params_inv_rect_Type3 :
 537   Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
 538   'a1) -> __ -> 'a2) -> 'a2
 539
 540 val print_serialization_params_inv_rect_Type2 :
 541   Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
 542   'a1) -> __ -> 'a2) -> 'a2
 543
 544 val print_serialization_params_inv_rect_Type1 :
 545   Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
 546   'a1) -> __ -> 'a2) -> 'a2
 547
 548 val print_serialization_params_inv_rect_Type0 :
 549   Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
 550   'a1) -> __ -> 'a2) -> 'a2
 551
 552 val print_serialization_params_discr :
 553   Joint.params -> 'a1 print_serialization_params -> 'a1
 554   print_serialization_params -> __
 555
 556 val print_serialization_params_jmdiscr :
 557   Joint.params -> 'a1 print_serialization_params -> 'a1
 558   print_serialization_params -> __
 559
 560 type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params :
 561                                                       'string
 562                                                       print_serialization_params;
 563                                                       fold_code : (__ -> (__
 564                                                                   ->
 565                                                                   'statementT
 566                                                                   -> __ ->
 567                                                                   __) -> __
 568                                                                   -> __ -> __
 569                                                                   -> __);
 570                                                       print_statementT :
 571                                                       ('statementT ->
 572                                                       'string) }
 573
 574 val code_iteration_params_rect_Type4 :
 575   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 576   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 577   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 578
 579 val code_iteration_params_rect_Type5 :
 580   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 581   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 582   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 583
 584 val code_iteration_params_rect_Type3 :
 585   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 586   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 587   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 588
 589 val code_iteration_params_rect_Type2 :
 590   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 591   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 592   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 593
 594 val code_iteration_params_rect_Type1 :
 595   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 596   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 597   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 598
 599 val code_iteration_params_rect_Type0 :
 600   Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
 601   (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) ->
 602   'a3) -> ('a1, 'a2) code_iteration_params -> 'a3
 603
 604 val cip_print_serialization_params :
 605   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 606   'a1 print_serialization_params
 607
 608 val fold_code0 :
 609   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 610   (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3
 611
 612 val print_statementT :
 613   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 614   'a2 -> 'a1
 615
 616 val code_iteration_params_inv_rect_Type4 :
 617   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 618   ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
 619   __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
 620
 621 val code_iteration_params_inv_rect_Type3 :
 622   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 623   ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
 624   __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
 625
 626 val code_iteration_params_inv_rect_Type2 :
 627   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 628   ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
 629   __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
 630
 631 val code_iteration_params_inv_rect_Type1 :
 632   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 633   ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
 634   __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
 635
 636 val code_iteration_params_inv_rect_Type0 :
 637   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 638   ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
 639   __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
 640
 641 val code_iteration_params_jmdiscr :
 642   Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
 643   ('a1, 'a2) code_iteration_params -> __
 644
 645 val pm_choose_with_pref :
 646   'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
 647   ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
 648   Types.option
 649
 650 val visit_graph :
 651   ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
 652   -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
 653   Nat.nat -> 'a2
 654
 655 val print_list : 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1
 656
 657 val print_joint_seq :
 658   Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
 659   Joint.joint_seq -> 'a1
 660
 661 val print_joint_step :
 662   Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
 663   Joint.joint_step -> 'a1
 664
 665 val print_joint_fin_step :
 666   Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step ->
 667   'a1
 668
 669 val print_joint_statement :
 670   Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
 671   print_serialization_params -> Joint.joint_statement -> 'a1
 672
 673 val graph_print_serialization_params :
 674   Joint.graph_params -> 'a1 printing_params -> 'a1 print_serialization_params
 675
 676 val graph_code_iteration_params :
 677   Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
 678   Joint.joint_statement) code_iteration_params
 679
 680 val lin_print_serialization_params :
 681   Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params
 682
 683 val lin_code_iteration_params :
 684   Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
 685   (Graphs.label Types.option, Joint.joint_statement) Types.prod)
 686   code_iteration_params
 687
 688 val print_joint_internal_function :
 689   Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params ->
 690   'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list
 691
 692 val print_joint_function :
 693   Joint.params -> AST.ident List.list -> AST.ident List.list -> ('a2, 'a1)
 694   code_iteration_params -> 'a2 printing_params -> Joint.joint_function -> 'a2
 695   List.list
 696
 697 val print_joint_program :
 698   Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
 699   code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list
 700