source: extracted/joint_printer.ml @ 2982

Last change on this file since 2982 was 2982, checked in by sacerdot, 6 years ago

Pretty priting of LIN implemented.

File size: 60.6 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121type 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 **)
145let 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 **)
169let 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 **)
193let 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 **)
217let 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 **)
241let 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 **)
265let 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 **)
292let 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 **)
305let 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 **)
318let 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 **)
331let 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 **)
344let 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 -> __ **)
352let 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 -> __ **)
376let 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
399type '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
423(** val printing_pass_independent_params_rect_Type4 :
424    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
425    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
426    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
427    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
428    printing_pass_independent_params -> 'a2 **)
429let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
430  let { print_String = print_String0; print_keyword = print_keyword0;
431    print_concat = print_concat0; print_empty = print_empty0; print_ident =
432    print_ident0; print_costlabel = print_costlabel0; print_label =
433    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
434    print_Op2 = print_Op4; print_nat = print_nat0 } = x_263
435  in
436  h_mk_printing_pass_independent_params print_String0 print_keyword0
437    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
438    print_OpAccs0 print_Op3 print_Op4 print_nat0
439
440(** val printing_pass_independent_params_rect_Type5 :
441    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
442    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
443    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
444    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
445    printing_pass_independent_params -> 'a2 **)
446let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
447  let { print_String = print_String0; print_keyword = print_keyword0;
448    print_concat = print_concat0; print_empty = print_empty0; print_ident =
449    print_ident0; print_costlabel = print_costlabel0; print_label =
450    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
451    print_Op2 = print_Op4; print_nat = print_nat0 } = x_265
452  in
453  h_mk_printing_pass_independent_params print_String0 print_keyword0
454    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
455    print_OpAccs0 print_Op3 print_Op4 print_nat0
456
457(** val printing_pass_independent_params_rect_Type3 :
458    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
459    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
460    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
461    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
462    printing_pass_independent_params -> 'a2 **)
463let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
464  let { print_String = print_String0; print_keyword = print_keyword0;
465    print_concat = print_concat0; print_empty = print_empty0; print_ident =
466    print_ident0; print_costlabel = print_costlabel0; print_label =
467    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
468    print_Op2 = print_Op4; print_nat = print_nat0 } = x_267
469  in
470  h_mk_printing_pass_independent_params print_String0 print_keyword0
471    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
472    print_OpAccs0 print_Op3 print_Op4 print_nat0
473
474(** val printing_pass_independent_params_rect_Type2 :
475    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
476    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
477    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
478    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
479    printing_pass_independent_params -> 'a2 **)
480let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
481  let { print_String = print_String0; print_keyword = print_keyword0;
482    print_concat = print_concat0; print_empty = print_empty0; print_ident =
483    print_ident0; print_costlabel = print_costlabel0; print_label =
484    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
485    print_Op2 = print_Op4; print_nat = print_nat0 } = x_269
486  in
487  h_mk_printing_pass_independent_params print_String0 print_keyword0
488    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
489    print_OpAccs0 print_Op3 print_Op4 print_nat0
490
491(** val printing_pass_independent_params_rect_Type1 :
492    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
493    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
494    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
495    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
496    printing_pass_independent_params -> 'a2 **)
497let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
498  let { print_String = print_String0; print_keyword = print_keyword0;
499    print_concat = print_concat0; print_empty = print_empty0; print_ident =
500    print_ident0; print_costlabel = print_costlabel0; print_label =
501    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
502    print_Op2 = print_Op4; print_nat = print_nat0 } = x_271
503  in
504  h_mk_printing_pass_independent_params print_String0 print_keyword0
505    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
506    print_OpAccs0 print_Op3 print_Op4 print_nat0
507
508(** val printing_pass_independent_params_rect_Type0 :
509    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
510    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
511    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
512    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
513    printing_pass_independent_params -> 'a2 **)
514let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
515  let { print_String = print_String0; print_keyword = print_keyword0;
516    print_concat = print_concat0; print_empty = print_empty0; print_ident =
517    print_ident0; print_costlabel = print_costlabel0; print_label =
518    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
519    print_Op2 = print_Op4; print_nat = print_nat0 } = x_273
520  in
521  h_mk_printing_pass_independent_params print_String0 print_keyword0
522    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
523    print_OpAccs0 print_Op3 print_Op4 print_nat0
524
525(** val print_String :
526    'a1 printing_pass_independent_params -> String.string -> 'a1 **)
527let rec print_String xxx =
528  xxx.print_String
529
530(** val print_keyword :
531    'a1 printing_pass_independent_params -> keyword -> 'a1 **)
532let rec print_keyword xxx =
533  xxx.print_keyword
534
535(** val print_concat :
536    'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
537let rec print_concat xxx =
538  xxx.print_concat
539
540(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
541let rec print_empty xxx =
542  xxx.print_empty
543
544(** val print_ident :
545    'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
546let rec print_ident xxx =
547  xxx.print_ident
548
549(** val print_costlabel :
550    'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
551let rec print_costlabel xxx =
552  xxx.print_costlabel
553
554(** val print_label :
555    'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
556let rec print_label xxx =
557  xxx.print_label
558
559(** val print_OpAccs :
560    'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
561let rec print_OpAccs xxx =
562  xxx.print_OpAccs
563
564(** val print_Op1 :
565    'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
566let rec print_Op1 xxx =
567  xxx.print_Op1
568
569(** val print_Op2 :
570    'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
571let rec print_Op2 xxx =
572  xxx.print_Op2
573
574(** val print_nat :
575    'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
576let rec print_nat xxx =
577  xxx.print_nat
578
579(** val printing_pass_independent_params_inv_rect_Type4 :
580    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
581    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
582    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
583    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
584    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
585let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
586  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
587
588(** val printing_pass_independent_params_inv_rect_Type3 :
589    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
590    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
591    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
592    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
593    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
594let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
595  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
596
597(** val printing_pass_independent_params_inv_rect_Type2 :
598    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
599    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
600    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
601    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
602    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
603let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
604  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
605
606(** val printing_pass_independent_params_inv_rect_Type1 :
607    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
608    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
609    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
610    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
611    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
612let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
613  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
614
615(** val printing_pass_independent_params_inv_rect_Type0 :
616    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
617    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
618    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
619    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
620    -> 'a1) -> (Nat.nat -> 'a1) -> __ -> 'a2) -> 'a2 **)
621let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
622  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
623
624(** val printing_pass_independent_params_jmdiscr :
625    'a1 printing_pass_independent_params -> 'a1
626    printing_pass_independent_params -> __ **)
627let printing_pass_independent_params_jmdiscr x y =
628  Logic.eq_rect_Type2 x
629    (let { print_String = a0; print_keyword = a10; print_concat = a2;
630       print_empty = a3; print_ident = a4; print_costlabel = a5;
631       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
632       print_nat = a100 } = x
633     in
634    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
635
636type 'string printing_params = { print_pass_ind : 'string
637                                                  printing_pass_independent_params;
638                                 print_acc_a_reg : (__ -> 'string);
639                                 print_acc_b_reg : (__ -> 'string);
640                                 print_acc_a_arg : (__ -> 'string);
641                                 print_acc_b_arg : (__ -> 'string);
642                                 print_dpl_reg : (__ -> 'string);
643                                 print_dph_reg : (__ -> 'string);
644                                 print_dpl_arg : (__ -> 'string);
645                                 print_dph_arg : (__ -> 'string);
646                                 print_snd_arg : (__ -> 'string);
647                                 print_pair_move : (__ -> 'string);
648                                 print_call_args : (__ -> 'string);
649                                 print_call_dest : (__ -> 'string);
650                                 print_ext_seq : (__ -> 'string) }
651
652(** val printing_params_rect_Type4 :
653    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
654    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
655    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
656    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
657    printing_params -> 'a2 **)
658let rec printing_params_rect_Type4 p h_mk_printing_params x_300 =
659  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
660    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
661    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
662    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
663    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
664    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
665    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
666    x_300
667  in
668  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
669    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
670    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
671    print_call_args0 print_call_dest0 print_ext_seq0
672
673(** val printing_params_rect_Type5 :
674    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
675    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
676    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
677    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
678    printing_params -> 'a2 **)
679let rec printing_params_rect_Type5 p h_mk_printing_params x_302 =
680  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
681    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
682    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
683    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
684    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
685    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
686    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
687    x_302
688  in
689  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
690    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
691    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
692    print_call_args0 print_call_dest0 print_ext_seq0
693
694(** val printing_params_rect_Type3 :
695    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
696    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
697    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
698    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
699    printing_params -> 'a2 **)
700let rec printing_params_rect_Type3 p h_mk_printing_params x_304 =
701  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
702    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
703    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
704    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
705    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
706    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
707    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
708    x_304
709  in
710  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
711    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
712    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
713    print_call_args0 print_call_dest0 print_ext_seq0
714
715(** val printing_params_rect_Type2 :
716    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
717    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
718    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
719    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
720    printing_params -> 'a2 **)
721let rec printing_params_rect_Type2 p h_mk_printing_params x_306 =
722  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
723    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
724    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
725    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
726    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
727    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
728    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
729    x_306
730  in
731  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
732    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
733    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
734    print_call_args0 print_call_dest0 print_ext_seq0
735
736(** val printing_params_rect_Type1 :
737    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
738    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
739    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
740    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
741    printing_params -> 'a2 **)
742let rec printing_params_rect_Type1 p h_mk_printing_params x_308 =
743  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
744    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
745    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
746    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
747    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
748    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
749    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
750    x_308
751  in
752  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
753    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
754    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
755    print_call_args0 print_call_dest0 print_ext_seq0
756
757(** val printing_params_rect_Type0 :
758    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
759    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
760    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
761    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
762    printing_params -> 'a2 **)
763let rec printing_params_rect_Type0 p h_mk_printing_params x_310 =
764  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
765    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
766    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
767    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
768    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
769    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
770    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
771    x_310
772  in
773  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
774    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
775    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
776    print_call_args0 print_call_dest0 print_ext_seq0
777
778(** val print_pass_ind :
779    Joint.unserialized_params -> 'a1 printing_params -> 'a1
780    printing_pass_independent_params **)
781let rec print_pass_ind p xxx =
782  xxx.print_pass_ind
783
784(** val print_acc_a_reg :
785    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
786let rec print_acc_a_reg p xxx =
787  xxx.print_acc_a_reg
788
789(** val print_acc_b_reg :
790    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
791let rec print_acc_b_reg p xxx =
792  xxx.print_acc_b_reg
793
794(** val print_acc_a_arg :
795    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
796let rec print_acc_a_arg p xxx =
797  xxx.print_acc_a_arg
798
799(** val print_acc_b_arg :
800    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
801let rec print_acc_b_arg p xxx =
802  xxx.print_acc_b_arg
803
804(** val print_dpl_reg :
805    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
806let rec print_dpl_reg p xxx =
807  xxx.print_dpl_reg
808
809(** val print_dph_reg :
810    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
811let rec print_dph_reg p xxx =
812  xxx.print_dph_reg
813
814(** val print_dpl_arg :
815    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
816let rec print_dpl_arg p xxx =
817  xxx.print_dpl_arg
818
819(** val print_dph_arg :
820    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
821let rec print_dph_arg p xxx =
822  xxx.print_dph_arg
823
824(** val print_snd_arg :
825    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
826let rec print_snd_arg p xxx =
827  xxx.print_snd_arg
828
829(** val print_pair_move :
830    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
831let rec print_pair_move p xxx =
832  xxx.print_pair_move
833
834(** val print_call_args :
835    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
836let rec print_call_args p xxx =
837  xxx.print_call_args
838
839(** val print_call_dest :
840    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
841let rec print_call_dest p xxx =
842  xxx.print_call_dest
843
844(** val print_ext_seq :
845    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
846let rec print_ext_seq p xxx =
847  xxx.print_ext_seq
848
849(** val printing_params_inv_rect_Type4 :
850    Joint.unserialized_params -> 'a1 printing_params -> ('a1
851    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
852    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
853    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
854    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
855let printing_params_inv_rect_Type4 x2 hterm h1 =
856  let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
857
858(** val printing_params_inv_rect_Type3 :
859    Joint.unserialized_params -> 'a1 printing_params -> ('a1
860    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
861    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
862    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
863    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
864let printing_params_inv_rect_Type3 x2 hterm h1 =
865  let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
866
867(** val printing_params_inv_rect_Type2 :
868    Joint.unserialized_params -> 'a1 printing_params -> ('a1
869    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
870    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
871    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
872    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
873let printing_params_inv_rect_Type2 x2 hterm h1 =
874  let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
875
876(** val printing_params_inv_rect_Type1 :
877    Joint.unserialized_params -> 'a1 printing_params -> ('a1
878    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
879    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
880    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
881    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
882let printing_params_inv_rect_Type1 x2 hterm h1 =
883  let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
884
885(** val printing_params_inv_rect_Type0 :
886    Joint.unserialized_params -> 'a1 printing_params -> ('a1
887    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
888    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
889    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
890    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
891let printing_params_inv_rect_Type0 x2 hterm h1 =
892  let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
893
894(** val printing_params_jmdiscr :
895    Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
896    -> __ **)
897let printing_params_jmdiscr a2 x y =
898  Logic.eq_rect_Type2 x
899    (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
900       print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
901       print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
902       print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
903       print_call_dest = a12; print_ext_seq = a13 } = x
904     in
905    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
906
907(** val dpi1__o__print_pass_ind__o__inject :
908    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
909    'a1 printing_pass_independent_params Types.sig0 **)
910let dpi1__o__print_pass_ind__o__inject x1 x4 =
911  x4.Types.dpi1.print_pass_ind
912
913(** val eject__o__print_pass_ind__o__inject :
914    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
915    printing_pass_independent_params Types.sig0 **)
916let eject__o__print_pass_ind__o__inject x1 x4 =
917  (Types.pi1 x4).print_pass_ind
918
919(** val print_pass_ind__o__inject :
920    Joint.unserialized_params -> 'a1 printing_params -> 'a1
921    printing_pass_independent_params Types.sig0 **)
922let print_pass_ind__o__inject x1 x3 =
923  x3.print_pass_ind
924
925(** val dpi1__o__print_pass_ind :
926    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
927    'a1 printing_pass_independent_params **)
928let dpi1__o__print_pass_ind x1 x3 =
929  x3.Types.dpi1.print_pass_ind
930
931(** val eject__o__print_pass_ind :
932    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
933    printing_pass_independent_params **)
934let eject__o__print_pass_ind x1 x3 =
935  (Types.pi1 x3).print_pass_ind
936
937type 'string print_serialization_params = { print_succ : (__ -> 'string);
938                                            print_code_point : (__ ->
939                                                               'string) }
940
941(** val print_serialization_params_rect_Type4 :
942    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
943    print_serialization_params -> 'a2 **)
944let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_339 =
945  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
946    x_339
947  in
948  h_mk_print_serialization_params print_succ0 print_code_point0
949
950(** val print_serialization_params_rect_Type5 :
951    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
952    print_serialization_params -> 'a2 **)
953let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_341 =
954  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
955    x_341
956  in
957  h_mk_print_serialization_params print_succ0 print_code_point0
958
959(** val print_serialization_params_rect_Type3 :
960    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
961    print_serialization_params -> 'a2 **)
962let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_343 =
963  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
964    x_343
965  in
966  h_mk_print_serialization_params print_succ0 print_code_point0
967
968(** val print_serialization_params_rect_Type2 :
969    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
970    print_serialization_params -> 'a2 **)
971let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_345 =
972  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
973    x_345
974  in
975  h_mk_print_serialization_params print_succ0 print_code_point0
976
977(** val print_serialization_params_rect_Type1 :
978    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
979    print_serialization_params -> 'a2 **)
980let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_347 =
981  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
982    x_347
983  in
984  h_mk_print_serialization_params print_succ0 print_code_point0
985
986(** val print_serialization_params_rect_Type0 :
987    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
988    print_serialization_params -> 'a2 **)
989let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_349 =
990  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
991    x_349
992  in
993  h_mk_print_serialization_params print_succ0 print_code_point0
994
995(** val print_succ :
996    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
997let rec print_succ p xxx =
998  xxx.print_succ
999
1000(** val print_code_point :
1001    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1002let rec print_code_point p xxx =
1003  xxx.print_code_point
1004
1005(** val print_serialization_params_inv_rect_Type4 :
1006    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1007    'a1) -> __ -> 'a2) -> 'a2 **)
1008let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
1009  let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __
1010
1011(** val print_serialization_params_inv_rect_Type3 :
1012    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1013    'a1) -> __ -> 'a2) -> 'a2 **)
1014let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
1015  let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __
1016
1017(** val print_serialization_params_inv_rect_Type2 :
1018    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1019    'a1) -> __ -> 'a2) -> 'a2 **)
1020let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
1021  let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __
1022
1023(** val print_serialization_params_inv_rect_Type1 :
1024    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1025    'a1) -> __ -> 'a2) -> 'a2 **)
1026let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
1027  let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __
1028
1029(** val print_serialization_params_inv_rect_Type0 :
1030    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1031    'a1) -> __ -> 'a2) -> 'a2 **)
1032let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
1033  let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __
1034
1035(** val print_serialization_params_discr :
1036    Joint.params -> 'a1 print_serialization_params -> 'a1
1037    print_serialization_params -> __ **)
1038let print_serialization_params_discr a2 x y =
1039  Logic.eq_rect_Type2 x
1040    (let { print_succ = a0; print_code_point = a10 } = x in
1041    Obj.magic (fun _ dH -> dH __ __)) y
1042
1043(** val print_serialization_params_jmdiscr :
1044    Joint.params -> 'a1 print_serialization_params -> 'a1
1045    print_serialization_params -> __ **)
1046let print_serialization_params_jmdiscr a2 x y =
1047  Logic.eq_rect_Type2 x
1048    (let { print_succ = a0; print_code_point = a10 } = x in
1049    Obj.magic (fun _ dH -> dH __ __)) y
1050
1051type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params : 
1052                                                      'string
1053                                                      print_serialization_params;
1054                                                      fold_code : (__ -> (__
1055                                                                  ->
1056                                                                  'statementT
1057                                                                  -> __ ->
1058                                                                  __) -> __
1059                                                                  -> __ ->
1060                                                                  __);
1061                                                      print_statementT : 
1062                                                      ('statementT ->
1063                                                      'string) }
1064
1065(** val code_iteration_params_rect_Type4 :
1066    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1067    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1068    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1069let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_367 =
1070  let { cip_print_serialization_params = cip_print_serialization_params0;
1071    fold_code = fold_code0; print_statementT = print_statementT0 } = x_367
1072  in
1073  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1074    print_statementT0
1075
1076(** val code_iteration_params_rect_Type5 :
1077    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1078    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1079    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1080let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_369 =
1081  let { cip_print_serialization_params = cip_print_serialization_params0;
1082    fold_code = fold_code0; print_statementT = print_statementT0 } = x_369
1083  in
1084  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1085    print_statementT0
1086
1087(** val code_iteration_params_rect_Type3 :
1088    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1089    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1090    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1091let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_371 =
1092  let { cip_print_serialization_params = cip_print_serialization_params0;
1093    fold_code = fold_code0; print_statementT = print_statementT0 } = x_371
1094  in
1095  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1096    print_statementT0
1097
1098(** val code_iteration_params_rect_Type2 :
1099    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1100    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1101    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1102let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_373 =
1103  let { cip_print_serialization_params = cip_print_serialization_params0;
1104    fold_code = fold_code0; print_statementT = print_statementT0 } = x_373
1105  in
1106  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1107    print_statementT0
1108
1109(** val code_iteration_params_rect_Type1 :
1110    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1111    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1112    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1113let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_375 =
1114  let { cip_print_serialization_params = cip_print_serialization_params0;
1115    fold_code = fold_code0; print_statementT = print_statementT0 } = x_375
1116  in
1117  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1118    print_statementT0
1119
1120(** val code_iteration_params_rect_Type0 :
1121    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1122    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
1123    -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1124let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_377 =
1125  let { cip_print_serialization_params = cip_print_serialization_params0;
1126    fold_code = fold_code0; print_statementT = print_statementT0 } = x_377
1127  in
1128  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1129    print_statementT0
1130
1131(** val cip_print_serialization_params :
1132    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1133    -> 'a1 print_serialization_params **)
1134let rec cip_print_serialization_params p globals xxx =
1135  xxx.cip_print_serialization_params
1136
1137(** val fold_code0 :
1138    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1139    -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> 'a3 -> 'a3 **)
1140let rec fold_code0 p globals xxx x_392 x_393 x_394 =
1141  (let { cip_print_serialization_params = x; fold_code = yyy;
1142     print_statementT = x0 } = xxx
1143   in
1144  Obj.magic yyy) __ x_392 x_393 x_394
1145
1146(** val print_statementT :
1147    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1148    -> 'a2 -> 'a1 **)
1149let rec print_statementT p globals xxx =
1150  xxx.print_statementT
1151
1152(** val code_iteration_params_inv_rect_Type4 :
1153    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1154    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1155    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1156let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
1157  let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __
1158
1159(** val code_iteration_params_inv_rect_Type3 :
1160    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1161    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1162    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1163let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
1164  let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __
1165
1166(** val code_iteration_params_inv_rect_Type2 :
1167    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1168    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1169    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1170let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
1171  let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __
1172
1173(** val code_iteration_params_inv_rect_Type1 :
1174    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1175    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1176    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1177let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
1178  let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __
1179
1180(** val code_iteration_params_inv_rect_Type0 :
1181    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1182    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1183    __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1184let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
1185  let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __
1186
1187(** val code_iteration_params_jmdiscr :
1188    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1189    -> ('a1, 'a2) code_iteration_params -> __ **)
1190let code_iteration_params_jmdiscr a2 a4 x y =
1191  Logic.eq_rect_Type2 x
1192    (let { cip_print_serialization_params = a0; fold_code = a10;
1193       print_statementT = a20 } = x
1194     in
1195    Obj.magic (fun _ dH -> dH __ __ __)) y
1196
1197(** val pm_choose_with_pref :
1198    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1199    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1200    Types.option **)
1201let pm_choose_with_pref m = function
1202| Types.None -> PositiveMap.pm_choose m
1203| Types.Some p ->
1204  (match PositiveMap.pm_try_remove p m with
1205   | Types.None -> PositiveMap.pm_choose m
1206   | Types.Some res ->
1207     let { Types.fst = a; Types.snd = m' } = res in
1208     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1209     m' })
1210
1211(** val visit_graph :
1212    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1213    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1214    Nat.nat -> 'a2 **)
1215let rec visit_graph next f b n m = function
1216| Nat.O -> b
1217| Nat.S y ->
1218  (match pm_choose_with_pref m n with
1219   | Types.None -> b
1220   | Types.Some res ->
1221     let { Types.fst = eta2; Types.snd = m' } = res in
1222     let { Types.fst = pos; Types.snd = a } = eta2 in
1223     visit_graph next f (f pos a b) (next a) m' y)
1224
1225(** val print_list :
1226    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1227let print_list pp =
1228  List.foldr pp.print_concat pp.print_empty
1229
1230(** val print_joint_seq :
1231    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1232    -> Joint.joint_seq -> 'a1 **)
1233let print_joint_seq p globals pp = function
1234| Joint.COMMENT str ->
1235  print_list pp.print_pass_ind (List.Cons
1236    ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1237    ((pp.print_pass_ind.print_String str), List.Nil))))
1238| Joint.MOVE pm ->
1239  print_list pp.print_pass_ind (List.Cons
1240    ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1241    ((pp.print_pair_move pm), List.Nil))))
1242| Joint.POP arg ->
1243  print_list pp.print_pass_ind (List.Cons
1244    ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1245    ((pp.print_acc_a_reg arg), List.Nil))))
1246| Joint.PUSH arg ->
1247  print_list pp.print_pass_ind (List.Cons
1248    ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1249    ((pp.print_acc_a_arg arg), List.Nil))))
1250| Joint.ADDRESS (i, arg1, arg2) ->
1251  print_list pp.print_pass_ind (List.Cons
1252    ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1253    ((pp.print_pass_ind.print_ident i), (List.Cons ((pp.print_dpl_reg arg1),
1254    (List.Cons ((pp.print_dph_reg arg2), List.Nil))))))))
1255| Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1256  print_list pp.print_pass_ind (List.Cons
1257    ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1258    ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1259    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1260    (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1261    ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1262| Joint.OP1 (op1, arg1, arg2) ->
1263  print_list pp.print_pass_ind (List.Cons
1264    ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1265    ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1266    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1267    List.Nil))))))))
1268| Joint.OP2 (op2, arg1, arg2, arg3) ->
1269  print_list pp.print_pass_ind (List.Cons
1270    ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1271    ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1272    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1273    (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1274| Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1275| Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1276| Joint.LOAD (arg1, arg2, arg3) ->
1277  print_list pp.print_pass_ind (List.Cons
1278    ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1279    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1280    (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1281| Joint.STORE (arg1, arg2, arg3) ->
1282  print_list pp.print_pass_ind (List.Cons
1283    ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1284    ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1285    ((pp.print_acc_a_arg arg3), List.Nil))))))))
1286| Joint.Extension_seq ext -> pp.print_ext_seq ext
1287
1288(** val print_joint_step :
1289    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1290    -> Joint.joint_step -> 'a1 **)
1291let print_joint_step p globals pp = function
1292| Joint.COST_LABEL arg ->
1293  print_list pp.print_pass_ind (List.Cons
1294    ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1295    ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1296| Joint.CALL (arg1, arg2, arg3) ->
1297  print_list pp.print_pass_ind (List.Cons
1298    ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1299    ((match arg1 with
1300      | Types.Inl id -> pp.print_pass_ind.print_ident id
1301      | Types.Inr arg11_arg12 ->
1302        pp.print_pass_ind.print_concat
1303          (pp.print_dpl_arg arg11_arg12.Types.fst)
1304          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1305    ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1306    List.Nil))))))))
1307| Joint.COND (arg1, arg2) ->
1308  print_list pp.print_pass_ind (List.Cons
1309    ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1310    ((pp.print_acc_a_reg arg1), (List.Cons
1311    ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1312| Joint.Step_seq seq -> print_joint_seq p globals pp seq
1313
1314(** val print_joint_fin_step :
1315    Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1316    -> 'a1 **)
1317let print_joint_fin_step p pp = function
1318| Joint.GOTO l ->
1319  print_list pp.print_pass_ind (List.Cons
1320    ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1321    ((pp.print_pass_ind.print_label l), List.Nil))))
1322| Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1323| Joint.TAILCALL (arg1, arg2) ->
1324  print_list pp.print_pass_ind (List.Cons
1325    ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1326    ((match arg1 with
1327      | Types.Inl id -> pp.print_pass_ind.print_ident id
1328      | Types.Inr arg11_arg12 ->
1329        pp.print_pass_ind.print_concat
1330          (pp.print_dpl_arg arg11_arg12.Types.fst)
1331          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1332    ((pp.print_call_args arg2), List.Nil))))))
1333
1334(** val print_joint_statement :
1335    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1336    print_serialization_params -> Joint.joint_statement -> 'a1 **)
1337let print_joint_statement p globals pp cip = function
1338| Joint.Sequential (js, arg1) ->
1339  pp.print_pass_ind.print_concat
1340    (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1341      js) (cip.print_succ arg1)
1342| Joint.Final fin ->
1343  print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1344| Joint.FCOND (arg1, arg2, arg3) ->
1345  print_list pp.print_pass_ind (List.Cons
1346    ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1347    ((pp.print_acc_a_reg arg1), (List.Cons
1348    ((pp.print_pass_ind.print_label arg2), (List.Cons
1349    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1350
1351(** val graph_print_serialization_params :
1352    Joint.graph_params -> 'a1 printing_params -> 'a1
1353    print_serialization_params **)
1354let graph_print_serialization_params gp pp =
1355  { print_succ = (Obj.magic pp.print_pass_ind.print_label);
1356    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1357
1358(** val graph_code_iteration_params :
1359    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1360    Joint.joint_statement) code_iteration_params **)
1361let graph_code_iteration_params gp globals pp =
1362  { cip_print_serialization_params =
1363    (graph_print_serialization_params gp pp); fold_code = (fun _ f m a ->
1364    visit_graph (fun stmt ->
1365      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1366              globals stmt with
1367      | Types.None -> Types.None
1368      | Types.Some label -> let p = label in Types.Some p) (fun n ->
1369      Obj.magic f n) a (Types.Some Positive.One) (let m' = Obj.magic m in m')
1370      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1371    print_statementT =
1372    (print_joint_statement (Joint.graph_params_to_params gp) globals pp
1373      (graph_print_serialization_params gp pp)) }
1374
1375(** val lin_print_serialization_params :
1376    Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
1377let lin_print_serialization_params gp pp =
1378  { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
1379    (Obj.magic pp.print_pass_ind.print_nat) }
1380
1381(** val lin_code_iteration_params :
1382    Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1383    (Graphs.label Types.option, Joint.joint_statement) Types.prod)
1384    code_iteration_params **)
1385let lin_code_iteration_params lp globals pp =
1386  { cip_print_serialization_params = (lin_print_serialization_params lp pp);
1387    fold_code = (fun _ f m a ->
1388    (List.foldr (fun x res ->
1389      let { Types.fst = pc; Types.snd = res' } = res in
1390      { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x res') })
1391      { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
1392    print_statementT = (fun linstr ->
1393    match linstr.Types.fst with
1394    | Types.None ->
1395      print_joint_statement (Joint.lin_params_to_params lp) globals pp
1396        (lin_print_serialization_params lp pp) linstr.Types.snd
1397    | Types.Some l ->
1398      print_list pp.print_pass_ind (List.Cons
1399        ((pp.print_pass_ind.print_label l), (List.Cons
1400        ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
1401           (lin_print_serialization_params lp pp) linstr.Types.snd),
1402        List.Nil))))) }
1403
1404(** val print_joint_internal_function :
1405    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
1406    -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
1407let print_joint_internal_function p globals cip pp f =
1408  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1409    ((print_list pp.print_pass_ind (List.Cons
1410       ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
1411       ((cip.print_statementT stmt), List.Nil))))), acc))
1412    f.Joint.joint_if_code List.Nil
1413
1414(** val print_joint_function :
1415    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
1416    -> 'a2 printing_params -> Joint.joint_function -> 'a2 List.list **)
1417let print_joint_function p globals cip pp = function
1418| AST.Internal f0 ->
1419  print_joint_internal_function p globals cip pp (Types.pi1 f0)
1420| AST.External f0 -> List.Nil
1421
1422(** val print_joint_program :
1423    Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
1424    code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
1425let print_joint_program p pp prog cip =
1426  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1427    (print_joint_function p
1428      (List.map (fun x -> x.Types.fst.Types.fst)
1429        prog.Joint.joint_prog.AST.prog_vars) cip pp f.Types.snd) }, acc))
1430    List.Nil prog.Joint.joint_prog.AST.prog_funct
1431
Note: See TracBrowser for help on using the repository browser.