extracted/joint_printer.ml

   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 let rec keyword_rect_Type4 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 146 | KwCOMMENT -> h_kwCOMMENT
 147 | KwMOVE -> h_kwMOVE
 148 | KwPOP -> h_kwPOP
 149 | KwPUSH -> h_kwPUSH
 150 | KwADDRESS -> h_kwADDRESS
 151 | KwOPACCS -> h_kwOPACCS
 152 | KwOP1 -> h_kwOP1
 153 | KwOP2 -> h_kwOP2
 154 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 155 | KwSET_CARRY -> h_kwSET_CARRY
 156 | KwLOAD -> h_kwLOAD
 157 | KwSTORE -> h_kwSTORE
 158 | KwCOST_LABEL -> h_kwCOST_LABEL
 159 | KwCOND -> h_kwCOND
 160 | KwCALL -> h_kwCALL
 161 | KwGOTO -> h_kwGOTO
 162 | KwRETURN -> h_kwRETURN
 163 | KwTAILCALL -> h_kwTAILCALL
 164 | KwFCOND -> h_kwFCOND
 165
 166 (** val keyword_rect_Type5 :
 167     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 168     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
 169 let rec keyword_rect_Type5 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 170 | KwCOMMENT -> h_kwCOMMENT
 171 | KwMOVE -> h_kwMOVE
 172 | KwPOP -> h_kwPOP
 173 | KwPUSH -> h_kwPUSH
 174 | KwADDRESS -> h_kwADDRESS
 175 | KwOPACCS -> h_kwOPACCS
 176 | KwOP1 -> h_kwOP1
 177 | KwOP2 -> h_kwOP2
 178 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 179 | KwSET_CARRY -> h_kwSET_CARRY
 180 | KwLOAD -> h_kwLOAD
 181 | KwSTORE -> h_kwSTORE
 182 | KwCOST_LABEL -> h_kwCOST_LABEL
 183 | KwCOND -> h_kwCOND
 184 | KwCALL -> h_kwCALL
 185 | KwGOTO -> h_kwGOTO
 186 | KwRETURN -> h_kwRETURN
 187 | KwTAILCALL -> h_kwTAILCALL
 188 | KwFCOND -> h_kwFCOND
 189
 190 (** val keyword_rect_Type3 :
 191     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 192     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
 193 let rec keyword_rect_Type3 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 194 | KwCOMMENT -> h_kwCOMMENT
 195 | KwMOVE -> h_kwMOVE
 196 | KwPOP -> h_kwPOP
 197 | KwPUSH -> h_kwPUSH
 198 | KwADDRESS -> h_kwADDRESS
 199 | KwOPACCS -> h_kwOPACCS
 200 | KwOP1 -> h_kwOP1
 201 | KwOP2 -> h_kwOP2
 202 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 203 | KwSET_CARRY -> h_kwSET_CARRY
 204 | KwLOAD -> h_kwLOAD
 205 | KwSTORE -> h_kwSTORE
 206 | KwCOST_LABEL -> h_kwCOST_LABEL
 207 | KwCOND -> h_kwCOND
 208 | KwCALL -> h_kwCALL
 209 | KwGOTO -> h_kwGOTO
 210 | KwRETURN -> h_kwRETURN
 211 | KwTAILCALL -> h_kwTAILCALL
 212 | KwFCOND -> h_kwFCOND
 213
 214 (** val keyword_rect_Type2 :
 215     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 216     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
 217 let rec keyword_rect_Type2 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 218 | KwCOMMENT -> h_kwCOMMENT
 219 | KwMOVE -> h_kwMOVE
 220 | KwPOP -> h_kwPOP
 221 | KwPUSH -> h_kwPUSH
 222 | KwADDRESS -> h_kwADDRESS
 223 | KwOPACCS -> h_kwOPACCS
 224 | KwOP1 -> h_kwOP1
 225 | KwOP2 -> h_kwOP2
 226 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 227 | KwSET_CARRY -> h_kwSET_CARRY
 228 | KwLOAD -> h_kwLOAD
 229 | KwSTORE -> h_kwSTORE
 230 | KwCOST_LABEL -> h_kwCOST_LABEL
 231 | KwCOND -> h_kwCOND
 232 | KwCALL -> h_kwCALL
 233 | KwGOTO -> h_kwGOTO
 234 | KwRETURN -> h_kwRETURN
 235 | KwTAILCALL -> h_kwTAILCALL
 236 | KwFCOND -> h_kwFCOND
 237
 238 (** val keyword_rect_Type1 :
 239     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 240     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
 241 let rec keyword_rect_Type1 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 242 | KwCOMMENT -> h_kwCOMMENT
 243 | KwMOVE -> h_kwMOVE
 244 | KwPOP -> h_kwPOP
 245 | KwPUSH -> h_kwPUSH
 246 | KwADDRESS -> h_kwADDRESS
 247 | KwOPACCS -> h_kwOPACCS
 248 | KwOP1 -> h_kwOP1
 249 | KwOP2 -> h_kwOP2
 250 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 251 | KwSET_CARRY -> h_kwSET_CARRY
 252 | KwLOAD -> h_kwLOAD
 253 | KwSTORE -> h_kwSTORE
 254 | KwCOST_LABEL -> h_kwCOST_LABEL
 255 | KwCOND -> h_kwCOND
 256 | KwCALL -> h_kwCALL
 257 | KwGOTO -> h_kwGOTO
 258 | KwRETURN -> h_kwRETURN
 259 | KwTAILCALL -> h_kwTAILCALL
 260 | KwFCOND -> h_kwFCOND
 261
 262 (** val keyword_rect_Type0 :
 263     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 264     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
 265 let rec keyword_rect_Type0 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
 266 | KwCOMMENT -> h_kwCOMMENT
 267 | KwMOVE -> h_kwMOVE
 268 | KwPOP -> h_kwPOP
 269 | KwPUSH -> h_kwPUSH
 270 | KwADDRESS -> h_kwADDRESS
 271 | KwOPACCS -> h_kwOPACCS
 272 | KwOP1 -> h_kwOP1
 273 | KwOP2 -> h_kwOP2
 274 | KwCLEAR_CARRY -> h_kwCLEAR_CARRY
 275 | KwSET_CARRY -> h_kwSET_CARRY
 276 | KwLOAD -> h_kwLOAD
 277 | KwSTORE -> h_kwSTORE
 278 | KwCOST_LABEL -> h_kwCOST_LABEL
 279 | KwCOND -> h_kwCOND
 280 | KwCALL -> h_kwCALL
 281 | KwGOTO -> h_kwGOTO
 282 | KwRETURN -> h_kwRETURN
 283 | KwTAILCALL -> h_kwTAILCALL
 284 | KwFCOND -> h_kwFCOND
 285
 286 (** val keyword_inv_rect_Type4 :
 287     keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 288     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 289     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 290     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 291     -> 'a1) -> 'a1 **)
 292 let keyword_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 293   let hcut =
 294     keyword_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 295       h17 h18 h19 hterm
 296   in
 297   hcut __
 298
 299 (** val keyword_inv_rect_Type3 :
 300     keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 301     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 302     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 303     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 304     -> 'a1) -> 'a1 **)
 305 let keyword_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 306   let hcut =
 307     keyword_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 308       h17 h18 h19 hterm
 309   in
 310   hcut __
 311
 312 (** val keyword_inv_rect_Type2 :
 313     keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 314     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 315     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 316     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 317     -> 'a1) -> 'a1 **)
 318 let keyword_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 319   let hcut =
 320     keyword_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 321       h17 h18 h19 hterm
 322   in
 323   hcut __
 324
 325 (** val keyword_inv_rect_Type1 :
 326     keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 327     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 328     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 329     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 330     -> 'a1) -> 'a1 **)
 331 let keyword_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 332   let hcut =
 333     keyword_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 334       h17 h18 h19 hterm
 335   in
 336   hcut __
 337
 338 (** val keyword_inv_rect_Type0 :
 339     keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 340     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 341     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 342     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 343     -> 'a1) -> 'a1 **)
 344 let keyword_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 345   let hcut =
 346     keyword_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 347       h17 h18 h19 hterm
 348   in
 349   hcut __
 350
 351 (** val keyword_discr : keyword -> keyword -> __ **)
 352 let keyword_discr x y =
 353   Logic.eq_rect_Type2 x
 354     (match x with
 355      | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
 356      | KwMOVE -> Obj.magic (fun _ dH -> dH)
 357      | KwPOP -> Obj.magic (fun _ dH -> dH)
 358      | KwPUSH -> Obj.magic (fun _ dH -> dH)
 359      | KwADDRESS -> Obj.magic (fun _ dH -> dH)
 360      | KwOPACCS -> Obj.magic (fun _ dH -> dH)
 361      | KwOP1 -> Obj.magic (fun _ dH -> dH)
 362      | KwOP2 -> Obj.magic (fun _ dH -> dH)
 363      | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
 364      | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
 365      | KwLOAD -> Obj.magic (fun _ dH -> dH)
 366      | KwSTORE -> Obj.magic (fun _ dH -> dH)
 367      | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
 368      | KwCOND -> Obj.magic (fun _ dH -> dH)
 369      | KwCALL -> Obj.magic (fun _ dH -> dH)
 370      | KwGOTO -> Obj.magic (fun _ dH -> dH)
 371      | KwRETURN -> Obj.magic (fun _ dH -> dH)
 372      | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
 373      | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
 374
 375 (** val keyword_jmdiscr : keyword -> keyword -> __ **)
 376 let keyword_jmdiscr x y =
 377   Logic.eq_rect_Type2 x
 378     (match x with
 379      | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
 380      | KwMOVE -> Obj.magic (fun _ dH -> dH)
 381      | KwPOP -> Obj.magic (fun _ dH -> dH)
 382      | KwPUSH -> Obj.magic (fun _ dH -> dH)
 383      | KwADDRESS -> Obj.magic (fun _ dH -> dH)
 384      | KwOPACCS -> Obj.magic (fun _ dH -> dH)
 385      | KwOP1 -> Obj.magic (fun _ dH -> dH)
 386      | KwOP2 -> Obj.magic (fun _ dH -> dH)
 387      | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
 388      | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
 389      | KwLOAD -> Obj.magic (fun _ dH -> dH)
 390      | KwSTORE -> Obj.magic (fun _ dH -> dH)
 391      | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
 392      | KwCOND -> Obj.magic (fun _ dH -> dH)
 393      | KwCALL -> Obj.magic (fun _ dH -> dH)
 394      | KwGOTO -> Obj.magic (fun _ dH -> dH)
 395      | KwRETURN -> Obj.magic (fun _ dH -> dH)
 396      | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
 397      | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
 398
 399 type 'string printing_pass_independent_params = { print_String : (String.string
 400                                                                  -> 'string);
 401                                                   print_keyword : (keyword ->
 402                                                                   'string);
 403                                                   print_concat : ('string ->
 404                                                                  'string ->
 405                                                                  'string);
 406                                                   print_empty : 'string;
 407                                                   print_ident : (AST.ident ->
 408                                                                 'string);
 409                                                   print_costlabel : (CostLabel.costlabel
 410                                                                     ->
 411                                                                     'string);
 412                                                   print_label : (Graphs.label
 413                                                                 -> 'string);
 414                                                   print_OpAccs : (BackEndOps.opAccs
 415                                                                  -> 'string);
 416                                                   print_Op1 : (BackEndOps.op1
 417                                                               -> 'string);
 418                                                   print_Op2 : (BackEndOps.op2
 419                                                               -> 'string);
 420                                                   print_nat : (Nat.nat ->
 421                                                               'string);
 422                                                   print_bitvector : (Nat.nat
 423                                                                     ->
 424                                                                     BitVector.bitVector
 425                                                                     ->
 426                                                                     'string) }
 427
 428 (** val printing_pass_independent_params_rect_Type4 :
 429     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 430     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 431     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 432     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 433     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 434     printing_pass_independent_params -> 'a2 **)
 435 let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
 436   let { print_String = print_String0; print_keyword = print_keyword0;
 437     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 438     print_ident0; print_costlabel = print_costlabel0; print_label =
 439     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 440     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 441     print_bitvector0 } = x_25506
 442   in
 443   h_mk_printing_pass_independent_params print_String0 print_keyword0
 444     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 445     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 446
 447 (** val printing_pass_independent_params_rect_Type5 :
 448     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 449     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 450     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 451     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 452     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 453     printing_pass_independent_params -> 'a2 **)
 454 let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
 455   let { print_String = print_String0; print_keyword = print_keyword0;
 456     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 457     print_ident0; print_costlabel = print_costlabel0; print_label =
 458     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 459     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 460     print_bitvector0 } = x_25508
 461   in
 462   h_mk_printing_pass_independent_params print_String0 print_keyword0
 463     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 464     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 465
 466 (** val printing_pass_independent_params_rect_Type3 :
 467     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 468     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 469     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 470     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 471     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 472     printing_pass_independent_params -> 'a2 **)
 473 let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
 474   let { print_String = print_String0; print_keyword = print_keyword0;
 475     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 476     print_ident0; print_costlabel = print_costlabel0; print_label =
 477     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 478     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 479     print_bitvector0 } = x_25510
 480   in
 481   h_mk_printing_pass_independent_params print_String0 print_keyword0
 482     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 483     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 484
 485 (** val printing_pass_independent_params_rect_Type2 :
 486     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 487     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 488     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 489     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 490     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 491     printing_pass_independent_params -> 'a2 **)
 492 let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
 493   let { print_String = print_String0; print_keyword = print_keyword0;
 494     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 495     print_ident0; print_costlabel = print_costlabel0; print_label =
 496     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 497     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 498     print_bitvector0 } = x_25512
 499   in
 500   h_mk_printing_pass_independent_params print_String0 print_keyword0
 501     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 502     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 503
 504 (** val printing_pass_independent_params_rect_Type1 :
 505     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 506     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 507     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 508     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 509     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 510     printing_pass_independent_params -> 'a2 **)
 511 let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
 512   let { print_String = print_String0; print_keyword = print_keyword0;
 513     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 514     print_ident0; print_costlabel = print_costlabel0; print_label =
 515     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 516     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 517     print_bitvector0 } = x_25514
 518   in
 519   h_mk_printing_pass_independent_params print_String0 print_keyword0
 520     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 521     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 522
 523 (** val printing_pass_independent_params_rect_Type0 :
 524     ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
 525     -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
 526     'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
 527     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
 528     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
 529     printing_pass_independent_params -> 'a2 **)
 530 let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
 531   let { print_String = print_String0; print_keyword = print_keyword0;
 532     print_concat = print_concat0; print_empty = print_empty0; print_ident =
 533     print_ident0; print_costlabel = print_costlabel0; print_label =
 534     print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
 535     print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
 536     print_bitvector0 } = x_25516
 537   in
 538   h_mk_printing_pass_independent_params print_String0 print_keyword0
 539     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
 540     print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
 541
 542 (** val print_String :
 543     'a1 printing_pass_independent_params -> String.string -> 'a1 **)
 544 let rec print_String xxx =
 545   xxx.print_String
 546
 547 (** val print_keyword :
 548     'a1 printing_pass_independent_params -> keyword -> 'a1 **)
 549 let rec print_keyword xxx =
 550   xxx.print_keyword
 551
 552 (** val print_concat :
 553     'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
 554 let rec print_concat xxx =
 555   xxx.print_concat
 556
 557 (** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
 558 let rec print_empty xxx =
 559   xxx.print_empty
 560
 561 (** val print_ident :
 562     'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
 563 let rec print_ident xxx =
 564   xxx.print_ident
 565
 566 (** val print_costlabel :
 567     'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
 568 let rec print_costlabel xxx =
 569   xxx.print_costlabel
 570
 571 (** val print_label :
 572     'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
 573 let rec print_label xxx =
 574   xxx.print_label
 575
 576 (** val print_OpAccs :
 577     'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
 578 let rec print_OpAccs xxx =
 579   xxx.print_OpAccs
 580
 581 (** val print_Op1 :
 582     'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
 583 let rec print_Op1 xxx =
 584   xxx.print_Op1
 585
 586 (** val print_Op2 :
 587     'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
 588 let rec print_Op2 xxx =
 589   xxx.print_Op2
 590
 591 (** val print_nat :
 592     'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
 593 let rec print_nat xxx =
 594   xxx.print_nat
 595
 596 (** val print_bitvector :
 597     'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
 598     'a1 **)
 599 let rec print_bitvector xxx =
 600   xxx.print_bitvector
 601
 602 (** val printing_pass_independent_params_inv_rect_Type4 :
 603     'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
 604     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 605     (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
 606     (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
 607     -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
 608     __ -> 'a2) -> 'a2 **)
 609 let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
 610   let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
 611
 612 (** val printing_pass_independent_params_inv_rect_Type3 :
 613     'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
 614     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 615     (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
 616     (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
 617     -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
 618     __ -> 'a2) -> 'a2 **)
 619 let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
 620   let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
 621
 622 (** val printing_pass_independent_params_inv_rect_Type2 :
 623     'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
 624     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 625     (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
 626     (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
 627     -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
 628     __ -> 'a2) -> 'a2 **)
 629 let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
 630   let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
 631
 632 (** val printing_pass_independent_params_inv_rect_Type1 :
 633     'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
 634     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 635     (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
 636     (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
 637     -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
 638     __ -> 'a2) -> 'a2 **)
 639 let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
 640   let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
 641
 642 (** val printing_pass_independent_params_inv_rect_Type0 :
 643     'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
 644     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
 645     (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
 646     (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
 647     -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
 648     __ -> 'a2) -> 'a2 **)
 649 let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
 650   let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
 651
 652 (** val printing_pass_independent_params_jmdiscr :
 653     'a1 printing_pass_independent_params -> 'a1
 654     printing_pass_independent_params -> __ **)
 655 let printing_pass_independent_params_jmdiscr x y =
 656   Logic.eq_rect_Type2 x
 657     (let { print_String = a0; print_keyword = a10; print_concat = a2;
 658        print_empty = a3; print_ident = a4; print_costlabel = a5;
 659        print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
 660        print_nat = a100; print_bitvector = a11 } = x
 661      in
 662     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
 663
 664 type 'string printing_params = { print_pass_ind : 'string
 665                                                   printing_pass_independent_params;
 666                                  print_acc_a_reg : (__ -> 'string);
 667                                  print_acc_b_reg : (__ -> 'string);
 668                                  print_acc_a_arg : (__ -> 'string);
 669                                  print_acc_b_arg : (__ -> 'string);
 670                                  print_dpl_reg : (__ -> 'string);
 671                                  print_dph_reg : (__ -> 'string);
 672                                  print_dpl_arg : (__ -> 'string);
 673                                  print_dph_arg : (__ -> 'string);
 674                                  print_snd_arg : (__ -> 'string);
 675                                  print_pair_move : (__ -> 'string);
 676                                  print_call_args : (__ -> 'string);
 677                                  print_call_dest : (__ -> 'string);
 678                                  print_ext_seq : (__ -> 'string) }
 679
 680 (** val printing_params_rect_Type4 :
 681     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 682     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 683     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 684     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 685     printing_params -> 'a2 **)
 686 let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
 687   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 688     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 689     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 690     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 691     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 692     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 693     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 694     x_25544
 695   in
 696   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 697     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 698     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 699     print_call_args0 print_call_dest0 print_ext_seq0
 700
 701 (** val printing_params_rect_Type5 :
 702     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 703     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 704     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 705     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 706     printing_params -> 'a2 **)
 707 let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
 708   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 709     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 710     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 711     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 712     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 713     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 714     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 715     x_25546
 716   in
 717   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 718     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 719     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 720     print_call_args0 print_call_dest0 print_ext_seq0
 721
 722 (** val printing_params_rect_Type3 :
 723     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 724     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 725     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 726     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 727     printing_params -> 'a2 **)
 728 let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
 729   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 730     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 731     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 732     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 733     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 734     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 735     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 736     x_25548
 737   in
 738   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 739     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 740     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 741     print_call_args0 print_call_dest0 print_ext_seq0
 742
 743 (** val printing_params_rect_Type2 :
 744     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 745     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 746     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 747     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 748     printing_params -> 'a2 **)
 749 let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
 750   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 751     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 752     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 753     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 754     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 755     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 756     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 757     x_25550
 758   in
 759   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 760     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 761     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 762     print_call_args0 print_call_dest0 print_ext_seq0
 763
 764 (** val printing_params_rect_Type1 :
 765     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 766     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 767     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 768     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 769     printing_params -> 'a2 **)
 770 let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
 771   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 772     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 773     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 774     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 775     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 776     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 777     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 778     x_25552
 779   in
 780   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 781     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 782     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 783     print_call_args0 print_call_dest0 print_ext_seq0
 784
 785 (** val printing_params_rect_Type0 :
 786     Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
 787     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 788     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 789     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 790     printing_params -> 'a2 **)
 791 let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
 792   let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
 793     print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
 794     print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
 795     print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
 796     print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
 797     print_pair_move = print_pair_move0; print_call_args = print_call_args0;
 798     print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
 799     x_25554
 800   in
 801   h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
 802     print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
 803     print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
 804     print_call_args0 print_call_dest0 print_ext_seq0
 805
 806 (** val print_pass_ind :
 807     Joint.unserialized_params -> 'a1 printing_params -> 'a1
 808     printing_pass_independent_params **)
 809 let rec print_pass_ind p xxx =
 810   xxx.print_pass_ind
 811
 812 (** val print_acc_a_reg :
 813     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 814 let rec print_acc_a_reg p xxx =
 815   xxx.print_acc_a_reg
 816
 817 (** val print_acc_b_reg :
 818     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 819 let rec print_acc_b_reg p xxx =
 820   xxx.print_acc_b_reg
 821
 822 (** val print_acc_a_arg :
 823     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 824 let rec print_acc_a_arg p xxx =
 825   xxx.print_acc_a_arg
 826
 827 (** val print_acc_b_arg :
 828     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 829 let rec print_acc_b_arg p xxx =
 830   xxx.print_acc_b_arg
 831
 832 (** val print_dpl_reg :
 833     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 834 let rec print_dpl_reg p xxx =
 835   xxx.print_dpl_reg
 836
 837 (** val print_dph_reg :
 838     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 839 let rec print_dph_reg p xxx =
 840   xxx.print_dph_reg
 841
 842 (** val print_dpl_arg :
 843     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 844 let rec print_dpl_arg p xxx =
 845   xxx.print_dpl_arg
 846
 847 (** val print_dph_arg :
 848     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 849 let rec print_dph_arg p xxx =
 850   xxx.print_dph_arg
 851
 852 (** val print_snd_arg :
 853     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 854 let rec print_snd_arg p xxx =
 855   xxx.print_snd_arg
 856
 857 (** val print_pair_move :
 858     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 859 let rec print_pair_move p xxx =
 860   xxx.print_pair_move
 861
 862 (** val print_call_args :
 863     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 864 let rec print_call_args p xxx =
 865   xxx.print_call_args
 866
 867 (** val print_call_dest :
 868     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 869 let rec print_call_dest p xxx =
 870   xxx.print_call_dest
 871
 872 (** val print_ext_seq :
 873     Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
 874 let rec print_ext_seq p xxx =
 875   xxx.print_ext_seq
 876
 877 (** val printing_params_inv_rect_Type4 :
 878     Joint.unserialized_params -> 'a1 printing_params -> ('a1
 879     printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 880     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 881     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 882     (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
 883 let printing_params_inv_rect_Type4 x2 hterm h1 =
 884   let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
 885
 886 (** val printing_params_inv_rect_Type3 :
 887     Joint.unserialized_params -> 'a1 printing_params -> ('a1
 888     printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 889     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 890     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 891     (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
 892 let printing_params_inv_rect_Type3 x2 hterm h1 =
 893   let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
 894
 895 (** val printing_params_inv_rect_Type2 :
 896     Joint.unserialized_params -> 'a1 printing_params -> ('a1
 897     printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 898     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 899     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 900     (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
 901 let printing_params_inv_rect_Type2 x2 hterm h1 =
 902   let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
 903
 904 (** val printing_params_inv_rect_Type1 :
 905     Joint.unserialized_params -> 'a1 printing_params -> ('a1
 906     printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 907     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 908     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 909     (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
 910 let printing_params_inv_rect_Type1 x2 hterm h1 =
 911   let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
 912
 913 (** val printing_params_inv_rect_Type0 :
 914     Joint.unserialized_params -> 'a1 printing_params -> ('a1
 915     printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 916     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 917     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 918     (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
 919 let printing_params_inv_rect_Type0 x2 hterm h1 =
 920   let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
 921
 922 (** val printing_params_jmdiscr :
 923     Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
 924     -> __ **)
 925 let printing_params_jmdiscr a2 x y =
 926   Logic.eq_rect_Type2 x
 927     (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
 928        print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
 929        print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
 930        print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
 931        print_call_dest = a12; print_ext_seq = a13 } = x
 932      in
 933     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
 934
 935 (** val dpi1__o__print_pass_ind__o__inject :
 936     Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
 937     'a1 printing_pass_independent_params Types.sig0 **)
 938 let dpi1__o__print_pass_ind__o__inject x1 x4 =
 939   x4.Types.dpi1.print_pass_ind
 940
 941 (** val eject__o__print_pass_ind__o__inject :
 942     Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
 943     printing_pass_independent_params Types.sig0 **)
 944 let eject__o__print_pass_ind__o__inject x1 x4 =
 945   (Types.pi1 x4).print_pass_ind
 946
 947 (** val print_pass_ind__o__inject :
 948     Joint.unserialized_params -> 'a1 printing_params -> 'a1
 949     printing_pass_independent_params Types.sig0 **)
 950 let print_pass_ind__o__inject x1 x3 =
 951   x3.print_pass_ind
 952
 953 (** val dpi1__o__print_pass_ind :
 954     Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
 955     'a1 printing_pass_independent_params **)
 956 let dpi1__o__print_pass_ind x1 x3 =
 957   x3.Types.dpi1.print_pass_ind
 958
 959 (** val eject__o__print_pass_ind :
 960     Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
 961     printing_pass_independent_params **)
 962 let eject__o__print_pass_ind x1 x3 =
 963   (Types.pi1 x3).print_pass_ind
 964
 965 type 'string print_serialization_params = { print_succ : (__ -> 'string);
 966                                             print_code_point : (__ ->
 967                                                                'string) }
 968
 969 (** val print_serialization_params_rect_Type4 :
 970     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 971     print_serialization_params -> 'a2 **)
 972 let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
 973   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
 974     x_25583
 975   in
 976   h_mk_print_serialization_params print_succ0 print_code_point0
 977
 978 (** val print_serialization_params_rect_Type5 :
 979     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 980     print_serialization_params -> 'a2 **)
 981 let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
 982   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
 983     x_25585
 984   in
 985   h_mk_print_serialization_params print_succ0 print_code_point0
 986
 987 (** val print_serialization_params_rect_Type3 :
 988     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 989     print_serialization_params -> 'a2 **)
 990 let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
 991   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
 992     x_25587
 993   in
 994   h_mk_print_serialization_params print_succ0 print_code_point0
 995
 996 (** val print_serialization_params_rect_Type2 :
 997     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
 998     print_serialization_params -> 'a2 **)
 999 let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
1000   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1001     x_25589
1002   in
1003   h_mk_print_serialization_params print_succ0 print_code_point0
1004
1005 (** val print_serialization_params_rect_Type1 :
1006     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1007     print_serialization_params -> 'a2 **)
1008 let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
1009   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1010     x_25591
1011   in
1012   h_mk_print_serialization_params print_succ0 print_code_point0
1013
1014 (** val print_serialization_params_rect_Type0 :
1015     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1016     print_serialization_params -> 'a2 **)
1017 let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
1018   let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1019     x_25593
1020   in
1021   h_mk_print_serialization_params print_succ0 print_code_point0
1022
1023 (** val print_succ :
1024     Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1025 let rec print_succ p xxx =
1026   xxx.print_succ
1027
1028 (** val print_code_point :
1029     Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1030 let rec print_code_point p xxx =
1031   xxx.print_code_point
1032
1033 (** val print_serialization_params_inv_rect_Type4 :
1034     Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1035     'a1) -> __ -> 'a2) -> 'a2 **)
1036 let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
1037   let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __
1038
1039 (** val print_serialization_params_inv_rect_Type3 :
1040     Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1041     'a1) -> __ -> 'a2) -> 'a2 **)
1042 let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
1043   let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __
1044
1045 (** val print_serialization_params_inv_rect_Type2 :
1046     Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1047     'a1) -> __ -> 'a2) -> 'a2 **)
1048 let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
1049   let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __
1050
1051 (** val print_serialization_params_inv_rect_Type1 :
1052     Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1053     'a1) -> __ -> 'a2) -> 'a2 **)
1054 let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
1055   let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __
1056
1057 (** val print_serialization_params_inv_rect_Type0 :
1058     Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1059     'a1) -> __ -> 'a2) -> 'a2 **)
1060 let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
1061   let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __
1062
1063 (** val print_serialization_params_discr :
1064     Joint.params -> 'a1 print_serialization_params -> 'a1
1065     print_serialization_params -> __ **)
1066 let print_serialization_params_discr a2 x y =
1067   Logic.eq_rect_Type2 x
1068     (let { print_succ = a0; print_code_point = a10 } = x in
1069     Obj.magic (fun _ dH -> dH __ __)) y
1070
1071 (** val print_serialization_params_jmdiscr :
1072     Joint.params -> 'a1 print_serialization_params -> 'a1
1073     print_serialization_params -> __ **)
1074 let print_serialization_params_jmdiscr a2 x y =
1075   Logic.eq_rect_Type2 x
1076     (let { print_succ = a0; print_code_point = a10 } = x in
1077     Obj.magic (fun _ dH -> dH __ __)) y
1078
1079 type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params :
1080                                                       'string
1081                                                       print_serialization_params;
1082                                                       fold_code : (__ -> (__
1083                                                                   ->
1084                                                                   'statementT
1085                                                                   -> __ ->
1086                                                                   __) -> __
1087                                                                   -> __ -> __
1088                                                                   -> __);
1089                                                       print_statementT :
1090                                                       ('statementT ->
1091                                                       'string) }
1092
1093 (** val code_iteration_params_rect_Type4 :
1094     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1095     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1096     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1097 let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
1098   let { cip_print_serialization_params = cip_print_serialization_params0;
1099     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
1100   in
1101   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1102     print_statementT0
1103
1104 (** val code_iteration_params_rect_Type5 :
1105     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1106     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1107     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1108 let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
1109   let { cip_print_serialization_params = cip_print_serialization_params0;
1110     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
1111   in
1112   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1113     print_statementT0
1114
1115 (** val code_iteration_params_rect_Type3 :
1116     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1117     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1118     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1119 let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
1120   let { cip_print_serialization_params = cip_print_serialization_params0;
1121     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
1122   in
1123   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1124     print_statementT0
1125
1126 (** val code_iteration_params_rect_Type2 :
1127     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1128     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1129     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1130 let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
1131   let { cip_print_serialization_params = cip_print_serialization_params0;
1132     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
1133   in
1134   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1135     print_statementT0
1136
1137 (** val code_iteration_params_rect_Type1 :
1138     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1139     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1140     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1141 let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
1142   let { cip_print_serialization_params = cip_print_serialization_params0;
1143     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
1144   in
1145   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1146     print_statementT0
1147
1148 (** val code_iteration_params_rect_Type0 :
1149     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1150     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1151     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1152 let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
1153   let { cip_print_serialization_params = cip_print_serialization_params0;
1154     fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
1155   in
1156   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1157     print_statementT0
1158
1159 (** val cip_print_serialization_params :
1160     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1161     -> 'a1 print_serialization_params **)
1162 let rec cip_print_serialization_params p globals xxx =
1163   xxx.cip_print_serialization_params
1164
1165 (** val fold_code0 :
1166     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1167     -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
1168 let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
1169   (let { cip_print_serialization_params = x; fold_code = yyy;
1170      print_statementT = x0 } = xxx
1171    in
1172   Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639
1173
1174 (** val print_statementT :
1175     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1176     -> 'a2 -> 'a1 **)
1177 let rec print_statementT p globals xxx =
1178   xxx.print_statementT
1179
1180 (** val code_iteration_params_inv_rect_Type4 :
1181     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1182     -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1183     __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1184 let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
1185   let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __
1186
1187 (** val code_iteration_params_inv_rect_Type3 :
1188     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1189     -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1190     __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1191 let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
1192   let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __
1193
1194 (** val code_iteration_params_inv_rect_Type2 :
1195     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1196     -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1197     __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1198 let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
1199   let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __
1200
1201 (** val code_iteration_params_inv_rect_Type1 :
1202     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1203     -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1204     __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1205 let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
1206   let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __
1207
1208 (** val code_iteration_params_inv_rect_Type0 :
1209     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1210     -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1211     __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1212 let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
1213   let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __
1214
1215 (** val code_iteration_params_jmdiscr :
1216     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1217     -> ('a1, 'a2) code_iteration_params -> __ **)
1218 let code_iteration_params_jmdiscr a2 a4 x y =
1219   Logic.eq_rect_Type2 x
1220     (let { cip_print_serialization_params = a0; fold_code = a10;
1221        print_statementT = a20 } = x
1222      in
1223     Obj.magic (fun _ dH -> dH __ __ __)) y
1224
1225 (** val pm_choose_with_pref :
1226     'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1227     ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1228     Types.option **)
1229 let pm_choose_with_pref m = function
1230 | Types.None -> PositiveMap.pm_choose m
1231 | Types.Some p ->
1232   (match PositiveMap.pm_try_remove p m with
1233    | Types.None -> PositiveMap.pm_choose m
1234    | Types.Some res ->
1235      let { Types.fst = a; Types.snd = m' } = res in
1236      Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1237      m' })
1238
1239 (** val visit_graph :
1240     ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1241     -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1242     Nat.nat -> 'a2 **)
1243 let rec visit_graph next f b n m = function
1244 | Nat.O -> b
1245 | Nat.S y ->
1246   (match pm_choose_with_pref m n with
1247    | Types.None -> b
1248    | Types.Some res ->
1249      let { Types.fst = eta32074; Types.snd = m' } = res in
1250      let { Types.fst = pos; Types.snd = a } = eta32074 in
1251      visit_graph next f (f pos a b) (next a) m' y)
1252
1253 (** val print_list :
1254     'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1255 let print_list pp =
1256   List.foldr pp.print_concat pp.print_empty
1257
1258 (** val print_joint_seq :
1259     Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1260     -> Joint.joint_seq -> 'a1 **)
1261 let print_joint_seq p globals pp = function
1262 | Joint.COMMENT str ->
1263   print_list pp.print_pass_ind (List.Cons
1264     ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1265     ((pp.print_pass_ind.print_String str), List.Nil))))
1266 | Joint.MOVE pm ->
1267   print_list pp.print_pass_ind (List.Cons
1268     ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1269     ((pp.print_pair_move pm), List.Nil))))
1270 | Joint.POP arg ->
1271   print_list pp.print_pass_ind (List.Cons
1272     ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1273     ((pp.print_acc_a_reg arg), List.Nil))))
1274 | Joint.PUSH arg ->
1275   print_list pp.print_pass_ind (List.Cons
1276     ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1277     ((pp.print_acc_a_arg arg), List.Nil))))
1278 | Joint.ADDRESS (i, offset, arg1, arg2) ->
1279   print_list pp.print_pass_ind (List.Cons
1280     ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1281     ((pp.print_pass_ind.print_ident i), (List.Cons
1282     ((pp.print_pass_ind.print_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1284        (Nat.S Nat.O)))))))))))))))) offset), (List.Cons
1285     ((pp.print_dpl_reg arg1), (List.Cons ((pp.print_dph_reg arg2),
1286     List.Nil))))))))))
1287 | Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1288   print_list pp.print_pass_ind (List.Cons
1289     ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1290     ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1291     ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1292     (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1293     ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1294 | Joint.OP1 (op1, arg1, arg2) ->
1295   print_list pp.print_pass_ind (List.Cons
1296     ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1297     ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1298     ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1299     List.Nil))))))))
1300 | Joint.OP2 (op2, arg1, arg2, arg3) ->
1301   print_list pp.print_pass_ind (List.Cons
1302     ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1303     ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1304     ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1305     (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1306 | Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1307 | Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1308 | Joint.LOAD (arg1, arg2, arg3) ->
1309   print_list pp.print_pass_ind (List.Cons
1310     ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1311     ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1312     (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1313 | Joint.STORE (arg1, arg2, arg3) ->
1314   print_list pp.print_pass_ind (List.Cons
1315     ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1316     ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1317     ((pp.print_acc_a_arg arg3), List.Nil))))))))
1318 | Joint.Extension_seq ext -> pp.print_ext_seq ext
1319
1320 (** val print_joint_step :
1321     Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1322     -> Joint.joint_step -> 'a1 **)
1323 let print_joint_step p globals pp = function
1324 | Joint.COST_LABEL arg ->
1325   print_list pp.print_pass_ind (List.Cons
1326     ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1327     ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1328 | Joint.CALL (arg1, arg2, arg3) ->
1329   print_list pp.print_pass_ind (List.Cons
1330     ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1331     ((match arg1 with
1332       | Types.Inl id -> pp.print_pass_ind.print_ident id
1333       | Types.Inr arg11_arg12 ->
1334         pp.print_pass_ind.print_concat
1335           (pp.print_dpl_arg arg11_arg12.Types.fst)
1336           (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1337     ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1338     List.Nil))))))))
1339 | Joint.COND (arg1, arg2) ->
1340   print_list pp.print_pass_ind (List.Cons
1341     ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1342     ((pp.print_acc_a_reg arg1), (List.Cons
1343     ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1344 | Joint.Step_seq seq -> print_joint_seq p globals pp seq
1345
1346 (** val print_joint_fin_step :
1347     Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1348     -> 'a1 **)
1349 let print_joint_fin_step p pp = function
1350 | Joint.GOTO l ->
1351   print_list pp.print_pass_ind (List.Cons
1352     ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1353     ((pp.print_pass_ind.print_label l), List.Nil))))
1354 | Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1355 | Joint.TAILCALL (arg1, arg2) ->
1356   print_list pp.print_pass_ind (List.Cons
1357     ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1358     ((match arg1 with
1359       | Types.Inl id -> pp.print_pass_ind.print_ident id
1360       | Types.Inr arg11_arg12 ->
1361         pp.print_pass_ind.print_concat
1362           (pp.print_dpl_arg arg11_arg12.Types.fst)
1363           (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1364     ((pp.print_call_args arg2), List.Nil))))))
1365
1366 (** val print_joint_statement :
1367     Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1368     print_serialization_params -> Joint.joint_statement -> 'a1 **)
1369 let print_joint_statement p globals pp cip = function
1370 | Joint.Sequential (js, arg1) ->
1371   pp.print_pass_ind.print_concat
1372     (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1373       js) (cip.print_succ arg1)
1374 | Joint.Final fin ->
1375   print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1376 | Joint.FCOND (arg1, arg2, arg3) ->
1377   print_list pp.print_pass_ind (List.Cons
1378     ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1379     ((pp.print_acc_a_reg arg1), (List.Cons
1380     ((pp.print_pass_ind.print_label arg2), (List.Cons
1381     ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1382
1383 (** val graph_print_serialization_params :
1384     Joint.graph_params -> 'a1 printing_params -> 'a1
1385     print_serialization_params **)
1386 let graph_print_serialization_params gp pp =
1387   { print_succ = (Obj.magic pp.print_pass_ind.print_label);
1388     print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1389
1390 (** val graph_code_iteration_params :
1391     Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1392     Joint.joint_statement) code_iteration_params **)
1393 let graph_code_iteration_params gp globals pp =
1394   { cip_print_serialization_params =
1395     (graph_print_serialization_params gp pp); fold_code =
1396     (fun _ f m initl a ->
1397     visit_graph (fun stmt ->
1398       match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1399               globals stmt with
1400       | Types.None -> Types.None
1401       | Types.Some label -> let p = label in Types.Some p) (fun n ->
1402       Obj.magic f n) a (Types.Some
1403       (Identifiers.word_of_identifier PreIdentifiers.LabelTag
1404         (Obj.magic initl))) (let m' = Obj.magic m in m')
1405       (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1406     print_statementT =
1407     (print_joint_statement (Joint.graph_params_to_params gp) globals pp
1408       (graph_print_serialization_params gp pp)) }
1409
1410 (** val lin_print_serialization_params :
1411     Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
1412 let lin_print_serialization_params gp pp =
1413   { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
1414     (Obj.magic pp.print_pass_ind.print_nat) }
1415
1416 (** val lin_code_iteration_params :
1417     Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1418     (Graphs.label Types.option, Joint.joint_statement) Types.prod)
1419     code_iteration_params **)
1420 let lin_code_iteration_params lp globals pp =
1421   { cip_print_serialization_params = (lin_print_serialization_params lp pp);
1422     fold_code = (fun _ f m x a ->
1423     (Util.foldl (fun res x0 ->
1424       let { Types.fst = pc; Types.snd = res' } = res in
1425       { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x0 res') })
1426       { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
1427     print_statementT = (fun linstr ->
1428     match linstr.Types.fst with
1429     | Types.None ->
1430       print_joint_statement (Joint.lin_params_to_params lp) globals pp
1431         (lin_print_serialization_params lp pp) linstr.Types.snd
1432     | Types.Some l ->
1433       print_list pp.print_pass_ind (List.Cons
1434         ((pp.print_pass_ind.print_label l), (List.Cons
1435         ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
1436            (lin_print_serialization_params lp pp) linstr.Types.snd),
1437         List.Nil))))) }
1438
1439 (** val print_joint_internal_function :
1440     Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
1441     -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
1442 let print_joint_internal_function p globals cip pp f =
1443   fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1444     ((print_list pp.print_pass_ind (List.Cons
1445        ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
1446        ((cip.print_statementT stmt), List.Nil))))), acc))
1447     f.Joint.joint_if_code f.Joint.joint_if_entry List.Nil
1448
1449 (** val print_joint_function :
1450     Joint.params -> AST.ident List.list -> AST.ident List.list -> ('a2, 'a1)
1451     code_iteration_params -> 'a2 printing_params -> Joint.joint_function ->
1452     'a2 List.list **)
1453 let print_joint_function p globals functions cip pp = function
1454 | AST.Internal f0 ->
1455   print_joint_internal_function p (List.append globals functions) cip pp
1456     (Types.pi1 f0)
1457 | AST.External f0 -> List.Nil
1458
1459 (** val print_joint_program :
1460     Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
1461     code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
1462 let print_joint_program p pp prog cip =
1463   List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1464     (print_joint_function p (AST.prog_var_names prog.Joint.joint_prog)
1465       prog.Joint.jp_functions cip pp f.Types.snd) }, acc)) List.Nil
1466     prog.Joint.joint_prog.AST.prog_funct
1467