open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

type keyword =
| KwCOMMENT
| KwMOVE
| KwPOP
| KwPUSH
| KwADDRESS
| KwOPACCS
| KwOP1
| KwOP2
| KwCLEAR_CARRY
| KwSET_CARRY
| KwLOAD
| KwSTORE
| KwCOST_LABEL
| KwCOND
| KwCALL
| KwGOTO
| KwRETURN
| KwTAILCALL
| KwFCOND

(** val keyword_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
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
| KwCOMMENT -> h_kwCOMMENT
| KwMOVE -> h_kwMOVE
| KwPOP -> h_kwPOP
| KwPUSH -> h_kwPUSH
| KwADDRESS -> h_kwADDRESS
| KwOPACCS -> h_kwOPACCS
| KwOP1 -> h_kwOP1
| KwOP2 -> h_kwOP2
| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
| KwSET_CARRY -> h_kwSET_CARRY
| KwLOAD -> h_kwLOAD
| KwSTORE -> h_kwSTORE
| KwCOST_LABEL -> h_kwCOST_LABEL
| KwCOND -> h_kwCOND
| KwCALL -> h_kwCALL
| KwGOTO -> h_kwGOTO
| KwRETURN -> h_kwRETURN
| KwTAILCALL -> h_kwTAILCALL
| KwFCOND -> h_kwFCOND

(** val keyword_inv_rect_Type4 :
    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
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 =
  let hcut =
    keyword_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val keyword_inv_rect_Type3 :
    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
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 =
  let hcut =
    keyword_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val keyword_inv_rect_Type2 :
    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
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 =
  let hcut =
    keyword_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val keyword_inv_rect_Type1 :
    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
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 =
  let hcut =
    keyword_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val keyword_inv_rect_Type0 :
    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
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 =
  let hcut =
    keyword_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val keyword_discr : keyword -> keyword -> __ **)
let keyword_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
     | KwMOVE -> Obj.magic (fun _ dH -> dH)
     | KwPOP -> Obj.magic (fun _ dH -> dH)
     | KwPUSH -> Obj.magic (fun _ dH -> dH)
     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
     | KwOP1 -> Obj.magic (fun _ dH -> dH)
     | KwOP2 -> Obj.magic (fun _ dH -> dH)
     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
     | KwLOAD -> Obj.magic (fun _ dH -> dH)
     | KwSTORE -> Obj.magic (fun _ dH -> dH)
     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
     | KwCOND -> Obj.magic (fun _ dH -> dH)
     | KwCALL -> Obj.magic (fun _ dH -> dH)
     | KwGOTO -> Obj.magic (fun _ dH -> dH)
     | KwRETURN -> Obj.magic (fun _ dH -> dH)
     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y

(** val keyword_jmdiscr : keyword -> keyword -> __ **)
let keyword_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
     | KwMOVE -> Obj.magic (fun _ dH -> dH)
     | KwPOP -> Obj.magic (fun _ dH -> dH)
     | KwPUSH -> Obj.magic (fun _ dH -> dH)
     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
     | KwOP1 -> Obj.magic (fun _ dH -> dH)
     | KwOP2 -> Obj.magic (fun _ dH -> dH)
     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
     | KwLOAD -> Obj.magic (fun _ dH -> dH)
     | KwSTORE -> Obj.magic (fun _ dH -> dH)
     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
     | KwCOND -> Obj.magic (fun _ dH -> dH)
     | KwCALL -> Obj.magic (fun _ dH -> dH)
     | KwGOTO -> Obj.magic (fun _ dH -> dH)
     | KwRETURN -> Obj.magic (fun _ dH -> dH)
     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y

type 'string printing_pass_independent_params = { print_String : (String.string
                                                                 -> 'string);
                                                  print_keyword : (keyword ->
                                                                  'string);
                                                  print_concat : ('string ->
                                                                 'string ->
                                                                 'string);
                                                  print_empty : 'string;
                                                  print_ident : (AST.ident ->
                                                                'string);
                                                  print_costlabel : (CostLabel.costlabel
                                                                    ->
                                                                    'string);
                                                  print_label : (Graphs.label
                                                                -> 'string);
                                                  print_OpAccs : (BackEndOps.opAccs
                                                                 -> 'string);
                                                  print_Op1 : (BackEndOps.op1
                                                              -> 'string);
                                                  print_Op2 : (BackEndOps.op2
                                                              -> 'string);
                                                  print_nat : (Nat.nat ->
                                                              'string);
                                                  print_bitvector : (Nat.nat
                                                                    ->
                                                                    BitVector.bitVector
                                                                    ->
                                                                    'string) }

(** val printing_pass_independent_params_rect_Type4 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25506
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val printing_pass_independent_params_rect_Type5 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25508
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val printing_pass_independent_params_rect_Type3 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25510
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val printing_pass_independent_params_rect_Type2 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25512
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val printing_pass_independent_params_rect_Type1 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25514
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val printing_pass_independent_params_rect_Type0 :
    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    printing_pass_independent_params -> 'a2 **)
let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
  let { print_String = print_String0; print_keyword = print_keyword0;
    print_concat = print_concat0; print_empty = print_empty0; print_ident =
    print_ident0; print_costlabel = print_costlabel0; print_label =
    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    print_bitvector0 } = x_25516
  in
  h_mk_printing_pass_independent_params print_String0 print_keyword0
    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0

(** val print_String :
    'a1 printing_pass_independent_params -> String.string -> 'a1 **)
let rec print_String xxx =
  xxx.print_String

(** val print_keyword :
    'a1 printing_pass_independent_params -> keyword -> 'a1 **)
let rec print_keyword xxx =
  xxx.print_keyword

(** val print_concat :
    'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
let rec print_concat xxx =
  xxx.print_concat

(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
let rec print_empty xxx =
  xxx.print_empty

(** val print_ident :
    'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
let rec print_ident xxx =
  xxx.print_ident

(** val print_costlabel :
    'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
let rec print_costlabel xxx =
  xxx.print_costlabel

(** val print_label :
    'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
let rec print_label xxx =
  xxx.print_label

(** val print_OpAccs :
    'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
let rec print_OpAccs xxx =
  xxx.print_OpAccs

(** val print_Op1 :
    'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
let rec print_Op1 xxx =
  xxx.print_Op1

(** val print_Op2 :
    'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
let rec print_Op2 xxx =
  xxx.print_Op2

(** val print_nat :
    'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
let rec print_nat xxx =
  xxx.print_nat

(** val print_bitvector :
    'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
    'a1 **)
let rec print_bitvector xxx =
  xxx.print_bitvector

(** val printing_pass_independent_params_inv_rect_Type4 :
    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
    __ -> 'a2) -> 'a2 **)
let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __

(** val printing_pass_independent_params_inv_rect_Type3 :
    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
    __ -> 'a2) -> 'a2 **)
let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __

(** val printing_pass_independent_params_inv_rect_Type2 :
    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
    __ -> 'a2) -> 'a2 **)
let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __

(** val printing_pass_independent_params_inv_rect_Type1 :
    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
    __ -> 'a2) -> 'a2 **)
let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __

(** val printing_pass_independent_params_inv_rect_Type0 :
    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
    __ -> 'a2) -> 'a2 **)
let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __

(** val printing_pass_independent_params_jmdiscr :
    'a1 printing_pass_independent_params -> 'a1
    printing_pass_independent_params -> __ **)
let printing_pass_independent_params_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { print_String = a0; print_keyword = a10; print_concat = a2;
       print_empty = a3; print_ident = a4; print_costlabel = a5;
       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
       print_nat = a100; print_bitvector = a11 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y

type 'string printing_params = { print_pass_ind : 'string
                                                  printing_pass_independent_params;
                                 print_acc_a_reg : (__ -> 'string);
                                 print_acc_b_reg : (__ -> 'string);
                                 print_acc_a_arg : (__ -> 'string);
                                 print_acc_b_arg : (__ -> 'string);
                                 print_dpl_reg : (__ -> 'string);
                                 print_dph_reg : (__ -> 'string);
                                 print_dpl_arg : (__ -> 'string);
                                 print_dph_arg : (__ -> 'string);
                                 print_snd_arg : (__ -> 'string);
                                 print_pair_move : (__ -> 'string);
                                 print_call_args : (__ -> 'string);
                                 print_call_dest : (__ -> 'string);
                                 print_ext_seq : (__ -> 'string) }

(** val printing_params_rect_Type4 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25544
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val printing_params_rect_Type5 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25546
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val printing_params_rect_Type3 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25548
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val printing_params_rect_Type2 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25550
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val printing_params_rect_Type1 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25552
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val printing_params_rect_Type0 :
    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    printing_params -> 'a2 **)
let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    x_25554
  in
  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
    print_call_args0 print_call_dest0 print_ext_seq0

(** val print_pass_ind :
    Joint.unserialized_params -> 'a1 printing_params -> 'a1
    printing_pass_independent_params **)
let rec print_pass_ind p xxx =
  xxx.print_pass_ind

(** val print_acc_a_reg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_acc_a_reg p xxx =
  xxx.print_acc_a_reg

(** val print_acc_b_reg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_acc_b_reg p xxx =
  xxx.print_acc_b_reg

(** val print_acc_a_arg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_acc_a_arg p xxx =
  xxx.print_acc_a_arg

(** val print_acc_b_arg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_acc_b_arg p xxx =
  xxx.print_acc_b_arg

(** val print_dpl_reg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_dpl_reg p xxx =
  xxx.print_dpl_reg

(** val print_dph_reg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_dph_reg p xxx =
  xxx.print_dph_reg

(** val print_dpl_arg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_dpl_arg p xxx =
  xxx.print_dpl_arg

(** val print_dph_arg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_dph_arg p xxx =
  xxx.print_dph_arg

(** val print_snd_arg :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_snd_arg p xxx =
  xxx.print_snd_arg

(** val print_pair_move :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_pair_move p xxx =
  xxx.print_pair_move

(** val print_call_args :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_call_args p xxx =
  xxx.print_call_args

(** val print_call_dest :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_call_dest p xxx =
  xxx.print_call_dest

(** val print_ext_seq :
    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
let rec print_ext_seq p xxx =
  xxx.print_ext_seq

(** val printing_params_inv_rect_Type4 :
    Joint.unserialized_params -> 'a1 printing_params -> ('a1
    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
let printing_params_inv_rect_Type4 x2 hterm h1 =
  let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __

(** val printing_params_inv_rect_Type3 :
    Joint.unserialized_params -> 'a1 printing_params -> ('a1
    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
let printing_params_inv_rect_Type3 x2 hterm h1 =
  let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __

(** val printing_params_inv_rect_Type2 :
    Joint.unserialized_params -> 'a1 printing_params -> ('a1
    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
let printing_params_inv_rect_Type2 x2 hterm h1 =
  let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __

(** val printing_params_inv_rect_Type1 :
    Joint.unserialized_params -> 'a1 printing_params -> ('a1
    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
let printing_params_inv_rect_Type1 x2 hterm h1 =
  let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __

(** val printing_params_inv_rect_Type0 :
    Joint.unserialized_params -> 'a1 printing_params -> ('a1
    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
let printing_params_inv_rect_Type0 x2 hterm h1 =
  let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __

(** val printing_params_jmdiscr :
    Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
    -> __ **)
let printing_params_jmdiscr a2 x y =
  Logic.eq_rect_Type2 x
    (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
       print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
       print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
       print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
       print_call_dest = a12; print_ext_seq = a13 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y

(** val dpi1__o__print_pass_ind__o__inject :
    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
    'a1 printing_pass_independent_params Types.sig0 **)
let dpi1__o__print_pass_ind__o__inject x1 x4 =
  x4.Types.dpi1.print_pass_ind

(** val eject__o__print_pass_ind__o__inject :
    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
    printing_pass_independent_params Types.sig0 **)
let eject__o__print_pass_ind__o__inject x1 x4 =
  (Types.pi1 x4).print_pass_ind

(** val print_pass_ind__o__inject :
    Joint.unserialized_params -> 'a1 printing_params -> 'a1
    printing_pass_independent_params Types.sig0 **)
let print_pass_ind__o__inject x1 x3 =
  x3.print_pass_ind

(** val dpi1__o__print_pass_ind :
    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
    'a1 printing_pass_independent_params **)
let dpi1__o__print_pass_ind x1 x3 =
  x3.Types.dpi1.print_pass_ind

(** val eject__o__print_pass_ind :
    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
    printing_pass_independent_params **)
let eject__o__print_pass_ind x1 x3 =
  (Types.pi1 x3).print_pass_ind

type 'string print_serialization_params = { print_succ : (__ -> 'string);
                                            print_code_point : (__ ->
                                                               'string) }

(** val print_serialization_params_rect_Type4 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25583
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_serialization_params_rect_Type5 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25585
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_serialization_params_rect_Type3 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25587
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_serialization_params_rect_Type2 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25589
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_serialization_params_rect_Type1 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25591
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_serialization_params_rect_Type0 :
    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    print_serialization_params -> 'a2 **)
let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    x_25593
  in
  h_mk_print_serialization_params print_succ0 print_code_point0

(** val print_succ :
    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
let rec print_succ p xxx =
  xxx.print_succ

(** val print_code_point :
    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
let rec print_code_point p xxx =
  xxx.print_code_point

(** val print_serialization_params_inv_rect_Type4 :
    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
    'a1) -> __ -> 'a2) -> 'a2 **)
let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
  let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __

(** val print_serialization_params_inv_rect_Type3 :
    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
    'a1) -> __ -> 'a2) -> 'a2 **)
let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
  let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __

(** val print_serialization_params_inv_rect_Type2 :
    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
    'a1) -> __ -> 'a2) -> 'a2 **)
let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
  let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __

(** val print_serialization_params_inv_rect_Type1 :
    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
    'a1) -> __ -> 'a2) -> 'a2 **)
let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
  let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __

(** val print_serialization_params_inv_rect_Type0 :
    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
    'a1) -> __ -> 'a2) -> 'a2 **)
let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
  let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __

(** val print_serialization_params_discr :
    Joint.params -> 'a1 print_serialization_params -> 'a1
    print_serialization_params -> __ **)
let print_serialization_params_discr a2 x y =
  Logic.eq_rect_Type2 x
    (let { print_succ = a0; print_code_point = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val print_serialization_params_jmdiscr :
    Joint.params -> 'a1 print_serialization_params -> 'a1
    print_serialization_params -> __ **)
let print_serialization_params_jmdiscr a2 x y =
  Logic.eq_rect_Type2 x
    (let { print_succ = a0; print_code_point = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params : 
                                                      'string
                                                      print_serialization_params;
                                                      fold_code : (__ -> (__
                                                                  ->
                                                                  'statementT
                                                                  -> __ ->
                                                                  __) -> __
                                                                  -> __ -> __
                                                                  -> __);
                                                      print_statementT : 
                                                      ('statementT ->
                                                      'string) }

(** val code_iteration_params_rect_Type4 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val code_iteration_params_rect_Type5 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val code_iteration_params_rect_Type3 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val code_iteration_params_rect_Type2 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val code_iteration_params_rect_Type1 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val code_iteration_params_rect_Type0 :
    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
  let { cip_print_serialization_params = cip_print_serialization_params0;
    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
  in
  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
    print_statementT0

(** val cip_print_serialization_params :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> 'a1 print_serialization_params **)
let rec cip_print_serialization_params p globals xxx =
  xxx.cip_print_serialization_params

(** val fold_code0 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
  (let { cip_print_serialization_params = x; fold_code = yyy;
     print_statementT = x0 } = xxx
   in
  Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639

(** val print_statementT :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> 'a2 -> 'a1 **)
let rec print_statementT p globals xxx =
  xxx.print_statementT

(** val code_iteration_params_inv_rect_Type4 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
  let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __

(** val code_iteration_params_inv_rect_Type3 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
  let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __

(** val code_iteration_params_inv_rect_Type2 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
  let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __

(** val code_iteration_params_inv_rect_Type1 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
  let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __

(** val code_iteration_params_inv_rect_Type0 :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
  let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __

(** val code_iteration_params_jmdiscr :
    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    -> ('a1, 'a2) code_iteration_params -> __ **)
let code_iteration_params_jmdiscr a2 a4 x y =
  Logic.eq_rect_Type2 x
    (let { cip_print_serialization_params = a0; fold_code = a10;
       print_statementT = a20 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val pm_choose_with_pref :
    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
    Types.option **)
let pm_choose_with_pref m = function
| Types.None -> PositiveMap.pm_choose m
| Types.Some p ->
  (match PositiveMap.pm_try_remove p m with
   | Types.None -> PositiveMap.pm_choose m
   | Types.Some res ->
     let { Types.fst = a; Types.snd = m' } = res in
     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
     m' })

(** val visit_graph :
    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
    Nat.nat -> 'a2 **)
let rec visit_graph next f b n m = function
| Nat.O -> b
| Nat.S y ->
  (match pm_choose_with_pref m n with
   | Types.None -> b
   | Types.Some res ->
     let { Types.fst = eta32074; Types.snd = m' } = res in
     let { Types.fst = pos; Types.snd = a } = eta32074 in
     visit_graph next f (f pos a b) (next a) m' y)

(** val print_list :
    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
let print_list pp =
  List.foldr pp.print_concat pp.print_empty

(** val print_joint_seq :
    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
    -> Joint.joint_seq -> 'a1 **)
let print_joint_seq p globals pp = function
| Joint.COMMENT str ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
    ((pp.print_pass_ind.print_String str), List.Nil))))
| Joint.MOVE pm ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
    ((pp.print_pair_move pm), List.Nil))))
| Joint.POP arg ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
    ((pp.print_acc_a_reg arg), List.Nil))))
| Joint.PUSH arg ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
    ((pp.print_acc_a_arg arg), List.Nil))))
| Joint.ADDRESS (i, offset, arg1, arg2) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
    ((pp.print_pass_ind.print_ident i), (List.Cons
    ((pp.print_pass_ind.print_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
       (Nat.S Nat.O)))))))))))))))) offset), (List.Cons
    ((pp.print_dpl_reg arg1), (List.Cons ((pp.print_dph_reg arg2),
    List.Nil))))))))))
| Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
    ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
    (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
    ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
| Joint.OP1 (op1, arg1, arg2) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
    ((pp.print_pass_ind.print_Op1 op1), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
    List.Nil))))))))
| Joint.OP2 (op2, arg1, arg2, arg3) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
    ((pp.print_pass_ind.print_Op2 op2), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
    (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
| Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
| Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
| Joint.LOAD (arg1, arg2, arg3) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
    (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
| Joint.STORE (arg1, arg2, arg3) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
    ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
    ((pp.print_acc_a_arg arg3), List.Nil))))))))
| Joint.Extension_seq ext -> pp.print_ext_seq ext

(** val print_joint_step :
    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
    -> Joint.joint_step -> 'a1 **)
let print_joint_step p globals pp = function
| Joint.COST_LABEL arg ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
    ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
| Joint.CALL (arg1, arg2, arg3) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
    ((match arg1 with
      | Types.Inl id -> pp.print_pass_ind.print_ident id
      | Types.Inr arg11_arg12 ->
        pp.print_pass_ind.print_concat
          (pp.print_dpl_arg arg11_arg12.Types.fst)
          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
    ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
    List.Nil))))))))
| Joint.COND (arg1, arg2) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons
    ((pp.print_pass_ind.print_label arg2), List.Nil))))))
| Joint.Step_seq seq -> print_joint_seq p globals pp seq

(** val print_joint_fin_step :
    Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
    -> 'a1 **)
let print_joint_fin_step p pp = function
| Joint.GOTO l ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
    ((pp.print_pass_ind.print_label l), List.Nil))))
| Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
| Joint.TAILCALL (arg1, arg2) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
    ((match arg1 with
      | Types.Inl id -> pp.print_pass_ind.print_ident id
      | Types.Inr arg11_arg12 ->
        pp.print_pass_ind.print_concat
          (pp.print_dpl_arg arg11_arg12.Types.fst)
          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
    ((pp.print_call_args arg2), List.Nil))))))

(** val print_joint_statement :
    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    print_serialization_params -> Joint.joint_statement -> 'a1 **)
let print_joint_statement p globals pp cip = function
| Joint.Sequential (js, arg1) ->
  pp.print_pass_ind.print_concat
    (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
      js) (cip.print_succ arg1)
| Joint.Final fin ->
  print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
| Joint.FCOND (arg1, arg2, arg3) ->
  print_list pp.print_pass_ind (List.Cons
    ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
    ((pp.print_acc_a_reg arg1), (List.Cons
    ((pp.print_pass_ind.print_label arg2), (List.Cons
    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))

(** val graph_print_serialization_params :
    Joint.graph_params -> 'a1 printing_params -> 'a1
    print_serialization_params **)
let graph_print_serialization_params gp pp =
  { print_succ = (Obj.magic pp.print_pass_ind.print_label);
    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }

(** val graph_code_iteration_params :
    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
    Joint.joint_statement) code_iteration_params **)
let graph_code_iteration_params gp globals pp =
  { cip_print_serialization_params =
    (graph_print_serialization_params gp pp); fold_code =
    (fun _ f m initl a ->
    visit_graph (fun stmt ->
      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
              globals stmt with
      | Types.None -> Types.None
      | Types.Some label -> let p = label in Types.Some p) (fun n ->
      Obj.magic f n) a (Types.Some
      (Identifiers.word_of_identifier PreIdentifiers.LabelTag
        (Obj.magic initl))) (let m' = Obj.magic m in m')
      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
    print_statementT =
    (print_joint_statement (Joint.graph_params_to_params gp) globals pp
      (graph_print_serialization_params gp pp)) }

(** val lin_print_serialization_params :
    Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
let lin_print_serialization_params gp pp =
  { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
    (Obj.magic pp.print_pass_ind.print_nat) }

(** val lin_code_iteration_params :
    Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
    (Graphs.label Types.option, Joint.joint_statement) Types.prod)
    code_iteration_params **)
let lin_code_iteration_params lp globals pp =
  { cip_print_serialization_params = (lin_print_serialization_params lp pp);
    fold_code = (fun _ f m x a ->
    (Util.foldl (fun res x0 ->
      let { Types.fst = pc; Types.snd = res' } = res in
      { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x0 res') })
      { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
    print_statementT = (fun linstr ->
    match linstr.Types.fst with
    | Types.None ->
      print_joint_statement (Joint.lin_params_to_params lp) globals pp
        (lin_print_serialization_params lp pp) linstr.Types.snd
    | Types.Some l ->
      print_list pp.print_pass_ind (List.Cons
        ((pp.print_pass_ind.print_label l), (List.Cons
        ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
           (lin_print_serialization_params lp pp) linstr.Types.snd),
        List.Nil))))) }

(** val print_joint_internal_function :
    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
    -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
let print_joint_internal_function p globals cip pp f =
  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
    ((print_list pp.print_pass_ind (List.Cons
       ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
       ((cip.print_statementT stmt), List.Nil))))), acc))
    f.Joint.joint_if_code f.Joint.joint_if_entry List.Nil

(** val print_joint_function :
    Joint.params -> AST.ident List.list -> AST.ident List.list -> ('a2, 'a1)
    code_iteration_params -> 'a2 printing_params -> Joint.joint_function ->
    'a2 List.list **)
let print_joint_function p globals functions cip pp = function
| AST.Internal f0 ->
  print_joint_internal_function p (List.append globals functions) cip pp
    (Types.pi1 f0)
| AST.External f0 -> List.Nil

(** val print_joint_program :
    Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
    code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
let print_joint_program p pp prog cip =
  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
    (print_joint_function p (AST.prog_var_names prog.Joint.joint_prog)
      prog.Joint.jp_functions cip pp f.Types.snd) }, acc)) List.Nil
    prog.Joint.joint_prog.AST.prog_funct