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

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

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

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

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

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

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

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

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

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

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

val keyword_discr : keyword -> keyword -> __

val keyword_jmdiscr : keyword -> keyword -> __

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

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

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

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

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

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

val print_String :
  'a1 printing_pass_independent_params -> String.string -> 'a1

val print_keyword : 'a1 printing_pass_independent_params -> keyword -> 'a1

val print_concat : 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1

val print_empty : 'a1 printing_pass_independent_params -> 'a1

val print_ident : 'a1 printing_pass_independent_params -> AST.ident -> 'a1

val print_costlabel :
  'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1

val print_label : 'a1 printing_pass_independent_params -> Graphs.label -> 'a1

val print_OpAccs :
  'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1

val print_Op1 : 'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1

val print_Op2 : 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1

val print_nat : 'a1 printing_pass_independent_params -> Nat.nat -> 'a1

val print_bitvector :
  'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
  'a1

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

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

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

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

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

val printing_pass_independent_params_jmdiscr :
  'a1 printing_pass_independent_params -> 'a1
  printing_pass_independent_params -> __

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

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

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

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

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

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

val print_pass_ind :
  Joint.unserialized_params -> 'a1 printing_params -> 'a1
  printing_pass_independent_params

val print_acc_a_reg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_acc_b_reg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_acc_a_arg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_acc_b_arg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_dpl_reg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_dph_reg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_dpl_arg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_dph_arg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_snd_arg :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_pair_move :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_call_args :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_call_dest :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

val print_ext_seq :
  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1

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

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

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

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

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

val printing_params_jmdiscr :
  Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params ->
  __

val dpi1__o__print_pass_ind__o__inject :
  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
  printing_pass_independent_params Types.sig0

val eject__o__print_pass_ind__o__inject :
  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
  printing_pass_independent_params Types.sig0

val print_pass_ind__o__inject :
  Joint.unserialized_params -> 'a1 printing_params -> 'a1
  printing_pass_independent_params Types.sig0

val dpi1__o__print_pass_ind :
  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
  printing_pass_independent_params

val eject__o__print_pass_ind :
  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
  printing_pass_independent_params

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

val print_serialization_params_rect_Type5 :
  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
  print_serialization_params -> 'a2

val print_serialization_params_rect_Type3 :
  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
  print_serialization_params -> 'a2

val print_serialization_params_rect_Type2 :
  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
  print_serialization_params -> 'a2

val print_serialization_params_rect_Type1 :
  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
  print_serialization_params -> 'a2

val print_serialization_params_rect_Type0 :
  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
  print_serialization_params -> 'a2

val print_succ : Joint.params -> 'a1 print_serialization_params -> __ -> 'a1

val print_code_point :
  Joint.params -> 'a1 print_serialization_params -> __ -> 'a1

val print_serialization_params_inv_rect_Type4 :
  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
  'a1) -> __ -> 'a2) -> 'a2

val print_serialization_params_inv_rect_Type3 :
  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
  'a1) -> __ -> 'a2) -> 'a2

val print_serialization_params_inv_rect_Type2 :
  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
  'a1) -> __ -> 'a2) -> 'a2

val print_serialization_params_inv_rect_Type1 :
  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
  'a1) -> __ -> 'a2) -> 'a2

val print_serialization_params_inv_rect_Type0 :
  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
  'a1) -> __ -> 'a2) -> 'a2

val print_serialization_params_discr :
  Joint.params -> 'a1 print_serialization_params -> 'a1
  print_serialization_params -> __

val print_serialization_params_jmdiscr :
  Joint.params -> 'a1 print_serialization_params -> 'a1
  print_serialization_params -> __

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

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

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

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

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

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

val cip_print_serialization_params :
  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
  'a1 print_serialization_params

val fold_code0 :
  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
  (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3

val print_statementT :
  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
  'a2 -> 'a1

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

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

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

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

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

val code_iteration_params_jmdiscr :
  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
  ('a1, 'a2) code_iteration_params -> __

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

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

val print_list : 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1

val print_joint_seq :
  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
  Joint.joint_seq -> 'a1

val print_joint_step :
  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
  Joint.joint_step -> 'a1

val print_joint_fin_step :
  Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step ->
  'a1

val print_joint_statement :
  Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
  print_serialization_params -> Joint.joint_statement -> 'a1

val graph_print_serialization_params :
  Joint.graph_params -> 'a1 printing_params -> 'a1 print_serialization_params

val graph_code_iteration_params :
  Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
  Joint.joint_statement) code_iteration_params

val lin_print_serialization_params :
  Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params

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

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

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

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