source: extracted/joint_printer.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 52.0 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
421(** val printing_pass_independent_params_rect_Type4 :
422    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
423    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
424    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
425    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
426    -> 'a2 **)
427let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
428  let { print_String = print_String0; print_keyword = print_keyword0;
429    print_concat = print_concat0; print_empty = print_empty0; print_ident =
430    print_ident0; print_costlabel = print_costlabel0; print_label =
431    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
432    print_Op2 = print_Op4 } = x_263
433  in
434  h_mk_printing_pass_independent_params print_String0 print_keyword0
435    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
436    print_OpAccs0 print_Op3 print_Op4
437
438(** val printing_pass_independent_params_rect_Type5 :
439    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
440    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
441    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
442    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
443    -> 'a2 **)
444let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
445  let { print_String = print_String0; print_keyword = print_keyword0;
446    print_concat = print_concat0; print_empty = print_empty0; print_ident =
447    print_ident0; print_costlabel = print_costlabel0; print_label =
448    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
449    print_Op2 = print_Op4 } = x_265
450  in
451  h_mk_printing_pass_independent_params print_String0 print_keyword0
452    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
453    print_OpAccs0 print_Op3 print_Op4
454
455(** val printing_pass_independent_params_rect_Type3 :
456    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
457    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
458    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
459    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
460    -> 'a2 **)
461let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
462  let { print_String = print_String0; print_keyword = print_keyword0;
463    print_concat = print_concat0; print_empty = print_empty0; print_ident =
464    print_ident0; print_costlabel = print_costlabel0; print_label =
465    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
466    print_Op2 = print_Op4 } = x_267
467  in
468  h_mk_printing_pass_independent_params print_String0 print_keyword0
469    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
470    print_OpAccs0 print_Op3 print_Op4
471
472(** val printing_pass_independent_params_rect_Type2 :
473    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
474    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
475    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
476    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
477    -> 'a2 **)
478let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
479  let { print_String = print_String0; print_keyword = print_keyword0;
480    print_concat = print_concat0; print_empty = print_empty0; print_ident =
481    print_ident0; print_costlabel = print_costlabel0; print_label =
482    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
483    print_Op2 = print_Op4 } = x_269
484  in
485  h_mk_printing_pass_independent_params print_String0 print_keyword0
486    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
487    print_OpAccs0 print_Op3 print_Op4
488
489(** val printing_pass_independent_params_rect_Type1 :
490    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
491    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
492    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
493    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
494    -> 'a2 **)
495let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
496  let { print_String = print_String0; print_keyword = print_keyword0;
497    print_concat = print_concat0; print_empty = print_empty0; print_ident =
498    print_ident0; print_costlabel = print_costlabel0; print_label =
499    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
500    print_Op2 = print_Op4 } = x_271
501  in
502  h_mk_printing_pass_independent_params print_String0 print_keyword0
503    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
504    print_OpAccs0 print_Op3 print_Op4
505
506(** val printing_pass_independent_params_rect_Type0 :
507    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
508    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
509    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
510    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
511    -> 'a2 **)
512let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
513  let { print_String = print_String0; print_keyword = print_keyword0;
514    print_concat = print_concat0; print_empty = print_empty0; print_ident =
515    print_ident0; print_costlabel = print_costlabel0; print_label =
516    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
517    print_Op2 = print_Op4 } = x_273
518  in
519  h_mk_printing_pass_independent_params print_String0 print_keyword0
520    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
521    print_OpAccs0 print_Op3 print_Op4
522
523(** val print_String :
524    'a1 printing_pass_independent_params -> String.string -> 'a1 **)
525let rec print_String xxx =
526  xxx.print_String
527
528(** val print_keyword :
529    'a1 printing_pass_independent_params -> keyword -> 'a1 **)
530let rec print_keyword xxx =
531  xxx.print_keyword
532
533(** val print_concat :
534    'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
535let rec print_concat xxx =
536  xxx.print_concat
537
538(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
539let rec print_empty xxx =
540  xxx.print_empty
541
542(** val print_ident :
543    'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
544let rec print_ident xxx =
545  xxx.print_ident
546
547(** val print_costlabel :
548    'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
549let rec print_costlabel xxx =
550  xxx.print_costlabel
551
552(** val print_label :
553    'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
554let rec print_label xxx =
555  xxx.print_label
556
557(** val print_OpAccs :
558    'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
559let rec print_OpAccs xxx =
560  xxx.print_OpAccs
561
562(** val print_Op1 :
563    'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
564let rec print_Op1 xxx =
565  xxx.print_Op1
566
567(** val print_Op2 :
568    'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
569let rec print_Op2 xxx =
570  xxx.print_Op2
571
572(** val printing_pass_independent_params_inv_rect_Type4 :
573    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
574    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
575    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
576    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
577    -> 'a1) -> __ -> 'a2) -> 'a2 **)
578let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
579  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
580
581(** val printing_pass_independent_params_inv_rect_Type3 :
582    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
583    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
584    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
585    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
586    -> 'a1) -> __ -> 'a2) -> 'a2 **)
587let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
588  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
589
590(** val printing_pass_independent_params_inv_rect_Type2 :
591    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
592    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
593    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
594    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
595    -> 'a1) -> __ -> 'a2) -> 'a2 **)
596let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
597  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
598
599(** val printing_pass_independent_params_inv_rect_Type1 :
600    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
601    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
602    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
603    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
604    -> 'a1) -> __ -> 'a2) -> 'a2 **)
605let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
606  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
607
608(** val printing_pass_independent_params_inv_rect_Type0 :
609    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
610    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
611    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
612    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
613    -> 'a1) -> __ -> 'a2) -> 'a2 **)
614let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
615  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
616
617(** val printing_pass_independent_params_jmdiscr :
618    'a1 printing_pass_independent_params -> 'a1
619    printing_pass_independent_params -> __ **)
620let printing_pass_independent_params_jmdiscr x y =
621  Logic.eq_rect_Type2 x
622    (let { print_String = a0; print_keyword = a10; print_concat = a2;
623       print_empty = a3; print_ident = a4; print_costlabel = a5;
624       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 =
625       a9 } = x
626     in
627    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
628
629type 'string printing_params = { print_pass_ind : 'string
630                                                  printing_pass_independent_params;
631                                 print_acc_a_reg : (__ -> 'string);
632                                 print_acc_b_reg : (__ -> 'string);
633                                 print_acc_a_arg : (__ -> 'string);
634                                 print_acc_b_arg : (__ -> 'string);
635                                 print_dpl_reg : (__ -> 'string);
636                                 print_dph_reg : (__ -> 'string);
637                                 print_dpl_arg : (__ -> 'string);
638                                 print_dph_arg : (__ -> 'string);
639                                 print_snd_arg : (__ -> 'string);
640                                 print_pair_move : (__ -> 'string);
641                                 print_call_args : (__ -> 'string);
642                                 print_call_dest : (__ -> 'string);
643                                 print_ext_seq : (__ -> 'string) }
644
645(** val printing_params_rect_Type4 :
646    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
647    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
648    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
649    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
650    printing_params -> 'a2 **)
651let rec printing_params_rect_Type4 p h_mk_printing_params x_299 =
652  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
653    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
654    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
655    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
656    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
657    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
658    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
659    x_299
660  in
661  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
662    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
663    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
664    print_call_args0 print_call_dest0 print_ext_seq0
665
666(** val printing_params_rect_Type5 :
667    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
668    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
669    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
670    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
671    printing_params -> 'a2 **)
672let rec printing_params_rect_Type5 p h_mk_printing_params x_301 =
673  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
674    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
675    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
676    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
677    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
678    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
679    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
680    x_301
681  in
682  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
683    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
684    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
685    print_call_args0 print_call_dest0 print_ext_seq0
686
687(** val printing_params_rect_Type3 :
688    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
689    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
690    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
691    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
692    printing_params -> 'a2 **)
693let rec printing_params_rect_Type3 p h_mk_printing_params x_303 =
694  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
695    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
696    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
697    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
698    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
699    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
700    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
701    x_303
702  in
703  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
704    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
705    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
706    print_call_args0 print_call_dest0 print_ext_seq0
707
708(** val printing_params_rect_Type2 :
709    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
710    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
711    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
712    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
713    printing_params -> 'a2 **)
714let rec printing_params_rect_Type2 p h_mk_printing_params x_305 =
715  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
716    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
717    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
718    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
719    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
720    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
721    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
722    x_305
723  in
724  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
725    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
726    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
727    print_call_args0 print_call_dest0 print_ext_seq0
728
729(** val printing_params_rect_Type1 :
730    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
731    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
732    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
733    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
734    printing_params -> 'a2 **)
735let rec printing_params_rect_Type1 p h_mk_printing_params x_307 =
736  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
737    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
738    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
739    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
740    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
741    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
742    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
743    x_307
744  in
745  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
746    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
747    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
748    print_call_args0 print_call_dest0 print_ext_seq0
749
750(** val printing_params_rect_Type0 :
751    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
752    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
753    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
754    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
755    printing_params -> 'a2 **)
756let rec printing_params_rect_Type0 p h_mk_printing_params x_309 =
757  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
758    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
759    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
760    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
761    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
762    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
763    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
764    x_309
765  in
766  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
767    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
768    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
769    print_call_args0 print_call_dest0 print_ext_seq0
770
771(** val print_pass_ind :
772    Joint.unserialized_params -> 'a1 printing_params -> 'a1
773    printing_pass_independent_params **)
774let rec print_pass_ind p xxx =
775  xxx.print_pass_ind
776
777(** val print_acc_a_reg :
778    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
779let rec print_acc_a_reg p xxx =
780  xxx.print_acc_a_reg
781
782(** val print_acc_b_reg :
783    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
784let rec print_acc_b_reg p xxx =
785  xxx.print_acc_b_reg
786
787(** val print_acc_a_arg :
788    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
789let rec print_acc_a_arg p xxx =
790  xxx.print_acc_a_arg
791
792(** val print_acc_b_arg :
793    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
794let rec print_acc_b_arg p xxx =
795  xxx.print_acc_b_arg
796
797(** val print_dpl_reg :
798    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
799let rec print_dpl_reg p xxx =
800  xxx.print_dpl_reg
801
802(** val print_dph_reg :
803    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
804let rec print_dph_reg p xxx =
805  xxx.print_dph_reg
806
807(** val print_dpl_arg :
808    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
809let rec print_dpl_arg p xxx =
810  xxx.print_dpl_arg
811
812(** val print_dph_arg :
813    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
814let rec print_dph_arg p xxx =
815  xxx.print_dph_arg
816
817(** val print_snd_arg :
818    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
819let rec print_snd_arg p xxx =
820  xxx.print_snd_arg
821
822(** val print_pair_move :
823    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
824let rec print_pair_move p xxx =
825  xxx.print_pair_move
826
827(** val print_call_args :
828    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
829let rec print_call_args p xxx =
830  xxx.print_call_args
831
832(** val print_call_dest :
833    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
834let rec print_call_dest p xxx =
835  xxx.print_call_dest
836
837(** val print_ext_seq :
838    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
839let rec print_ext_seq p xxx =
840  xxx.print_ext_seq
841
842(** val printing_params_inv_rect_Type4 :
843    Joint.unserialized_params -> 'a1 printing_params -> ('a1
844    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
845    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
846    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
847    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
848let printing_params_inv_rect_Type4 x2 hterm h1 =
849  let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
850
851(** val printing_params_inv_rect_Type3 :
852    Joint.unserialized_params -> 'a1 printing_params -> ('a1
853    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
854    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
855    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
856    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
857let printing_params_inv_rect_Type3 x2 hterm h1 =
858  let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
859
860(** val printing_params_inv_rect_Type2 :
861    Joint.unserialized_params -> 'a1 printing_params -> ('a1
862    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
863    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
864    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
865    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
866let printing_params_inv_rect_Type2 x2 hterm h1 =
867  let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
868
869(** val printing_params_inv_rect_Type1 :
870    Joint.unserialized_params -> 'a1 printing_params -> ('a1
871    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
872    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
873    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
874    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
875let printing_params_inv_rect_Type1 x2 hterm h1 =
876  let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
877
878(** val printing_params_inv_rect_Type0 :
879    Joint.unserialized_params -> 'a1 printing_params -> ('a1
880    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
881    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
882    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
883    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
884let printing_params_inv_rect_Type0 x2 hterm h1 =
885  let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
886
887(** val printing_params_jmdiscr :
888    Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
889    -> __ **)
890let printing_params_jmdiscr a2 x y =
891  Logic.eq_rect_Type2 x
892    (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
893       print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
894       print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
895       print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
896       print_call_dest = a12; print_ext_seq = a13 } = x
897     in
898    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
899
900(** val dpi1__o__print_pass_ind__o__inject :
901    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
902    'a1 printing_pass_independent_params Types.sig0 **)
903let dpi1__o__print_pass_ind__o__inject x1 x4 =
904  x4.Types.dpi1.print_pass_ind
905
906(** val eject__o__print_pass_ind__o__inject :
907    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
908    printing_pass_independent_params Types.sig0 **)
909let eject__o__print_pass_ind__o__inject x1 x4 =
910  (Types.pi1 x4).print_pass_ind
911
912(** val print_pass_ind__o__inject :
913    Joint.unserialized_params -> 'a1 printing_params -> 'a1
914    printing_pass_independent_params Types.sig0 **)
915let print_pass_ind__o__inject x1 x3 =
916  x3.print_pass_ind
917
918(** val dpi1__o__print_pass_ind :
919    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
920    'a1 printing_pass_independent_params **)
921let dpi1__o__print_pass_ind x1 x3 =
922  x3.Types.dpi1.print_pass_ind
923
924(** val eject__o__print_pass_ind :
925    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
926    printing_pass_independent_params **)
927let eject__o__print_pass_ind x1 x3 =
928  (Types.pi1 x3).print_pass_ind
929
930type 'string code_iteration_params = { fold_code : (__ -> (__ ->
931                                                   Joint.joint_statement ->
932                                                   __ -> __) -> __ -> __ ->
933                                                   __);
934                                       print_succ : (__ -> 'string);
935                                       print_code_point : (__ -> 'string) }
936
937(** val code_iteration_params_rect_Type4 :
938    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
939    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
940    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
941let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_338 =
942  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
943    print_code_point0 } = x_338
944  in
945  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
946
947(** val code_iteration_params_rect_Type5 :
948    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
949    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
950    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
951let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_340 =
952  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
953    print_code_point0 } = x_340
954  in
955  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
956
957(** val code_iteration_params_rect_Type3 :
958    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
959    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
960    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
961let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_342 =
962  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
963    print_code_point0 } = x_342
964  in
965  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
966
967(** val code_iteration_params_rect_Type2 :
968    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
969    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
970    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
971let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_344 =
972  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
973    print_code_point0 } = x_344
974  in
975  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
976
977(** val code_iteration_params_rect_Type1 :
978    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
979    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
980    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
981let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_346 =
982  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
983    print_code_point0 } = x_346
984  in
985  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
986
987(** val code_iteration_params_rect_Type0 :
988    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
989    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
990    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
991let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_348 =
992  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
993    print_code_point0 } = x_348
994  in
995  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
996
997(** val fold_code0 :
998    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__
999    -> Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2 **)
1000let rec fold_code0 p globals xxx x_364 x_365 x_366 =
1001  (let { fold_code = yyy; print_succ = x; print_code_point = x0 } = xxx in
1002  Obj.magic yyy) __ x_364 x_365 x_366
1003
1004(** val print_succ :
1005    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
1006    'a1 **)
1007let rec print_succ p globals xxx =
1008  xxx.print_succ
1009
1010(** val print_code_point :
1011    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
1012    'a1 **)
1013let rec print_code_point p globals xxx =
1014  xxx.print_code_point
1015
1016(** val code_iteration_params_inv_rect_Type4 :
1017    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1018    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1019    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1020let code_iteration_params_inv_rect_Type4 x2 x3 hterm h1 =
1021  let hcut = code_iteration_params_rect_Type4 x2 x3 h1 hterm in hcut __
1022
1023(** val code_iteration_params_inv_rect_Type3 :
1024    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1025    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1026    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1027let code_iteration_params_inv_rect_Type3 x2 x3 hterm h1 =
1028  let hcut = code_iteration_params_rect_Type3 x2 x3 h1 hterm in hcut __
1029
1030(** val code_iteration_params_inv_rect_Type2 :
1031    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1032    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1033    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1034let code_iteration_params_inv_rect_Type2 x2 x3 hterm h1 =
1035  let hcut = code_iteration_params_rect_Type2 x2 x3 h1 hterm in hcut __
1036
1037(** val code_iteration_params_inv_rect_Type1 :
1038    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1039    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1040    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1041let code_iteration_params_inv_rect_Type1 x2 x3 hterm h1 =
1042  let hcut = code_iteration_params_rect_Type1 x2 x3 h1 hterm in hcut __
1043
1044(** val code_iteration_params_inv_rect_Type0 :
1045    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1046    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1047    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1048let code_iteration_params_inv_rect_Type0 x2 x3 hterm h1 =
1049  let hcut = code_iteration_params_rect_Type0 x2 x3 h1 hterm in hcut __
1050
1051(** val code_iteration_params_jmdiscr :
1052    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1053    code_iteration_params -> __ **)
1054let code_iteration_params_jmdiscr a2 a3 x y =
1055  Logic.eq_rect_Type2 x
1056    (let { fold_code = a0; print_succ = a10; print_code_point = a20 } = x in
1057    Obj.magic (fun _ dH -> dH __ __ __)) y
1058
1059(** val pm_choose_with_pref :
1060    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1061    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1062    Types.option **)
1063let pm_choose_with_pref m = function
1064| Types.None -> PositiveMap.pm_choose m
1065| Types.Some p ->
1066  (match PositiveMap.pm_try_remove p m with
1067   | Types.None -> PositiveMap.pm_choose m
1068   | Types.Some res ->
1069     let { Types.fst = a; Types.snd = m' } = res in
1070     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1071     m' })
1072
1073(** val visit_graph :
1074    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1075    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1076    Nat.nat -> 'a2 **)
1077let rec visit_graph next f b n m = function
1078| Nat.O -> b
1079| Nat.S y ->
1080  (match pm_choose_with_pref m n with
1081   | Types.None -> b
1082   | Types.Some res ->
1083     let { Types.fst = eta2; Types.snd = m' } = res in
1084     let { Types.fst = pos; Types.snd = a } = eta2 in
1085     visit_graph next f (f pos a b) (next a) m' y)
1086
1087(** val graph_code_iteration_params :
1088    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1089    code_iteration_params **)
1090let graph_code_iteration_params gp globals pp =
1091  { fold_code = (fun _ f m a ->
1092    visit_graph (fun stmt ->
1093      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1094              globals stmt with
1095      | Types.None -> Types.None
1096      | Types.Some label -> let p = label in Types.Some p) (fun n ->
1097      Obj.magic f n) a (Types.Some Positive.One) (let m' = Obj.magic m in m')
1098      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1099    print_succ = (Obj.magic pp.print_pass_ind.print_label);
1100    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1101
1102(** val print_list :
1103    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1104let print_list pp =
1105  List.foldr pp.print_concat pp.print_empty
1106
1107(** val print_joint_seq :
1108    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1109    -> Joint.joint_seq -> 'a1 **)
1110let print_joint_seq p globals pp = function
1111| Joint.COMMENT str ->
1112  print_list pp.print_pass_ind (List.Cons
1113    ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1114    ((pp.print_pass_ind.print_String str), List.Nil))))
1115| Joint.MOVE pm ->
1116  print_list pp.print_pass_ind (List.Cons
1117    ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1118    ((pp.print_pair_move pm), List.Nil))))
1119| Joint.POP arg ->
1120  print_list pp.print_pass_ind (List.Cons
1121    ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1122    ((pp.print_acc_a_reg arg), List.Nil))))
1123| Joint.PUSH arg ->
1124  print_list pp.print_pass_ind (List.Cons
1125    ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1126    ((pp.print_acc_a_arg arg), List.Nil))))
1127| Joint.ADDRESS (i, arg1, arg2) ->
1128  print_list pp.print_pass_ind (List.Cons
1129    ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1130    ((pp.print_pass_ind.print_ident i), (List.Cons ((pp.print_dpl_reg arg1),
1131    (List.Cons ((pp.print_dph_reg arg2), List.Nil))))))))
1132| Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1133  print_list pp.print_pass_ind (List.Cons
1134    ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1135    ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1136    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1137    (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1138    ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1139| Joint.OP1 (op1, arg1, arg2) ->
1140  print_list pp.print_pass_ind (List.Cons
1141    ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1142    ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1143    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1144    List.Nil))))))))
1145| Joint.OP2 (op2, arg1, arg2, arg3) ->
1146  print_list pp.print_pass_ind (List.Cons
1147    ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1148    ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1149    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1150    (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1151| Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1152| Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1153| Joint.LOAD (arg1, arg2, arg3) ->
1154  print_list pp.print_pass_ind (List.Cons
1155    ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1156    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1157    (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1158| Joint.STORE (arg1, arg2, arg3) ->
1159  print_list pp.print_pass_ind (List.Cons
1160    ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1161    ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1162    ((pp.print_acc_a_arg arg3), List.Nil))))))))
1163| Joint.Extension_seq ext -> pp.print_ext_seq ext
1164
1165(** val print_joint_step :
1166    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1167    -> Joint.joint_step -> 'a1 **)
1168let print_joint_step p globals pp = function
1169| Joint.COST_LABEL arg ->
1170  print_list pp.print_pass_ind (List.Cons
1171    ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1172    ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1173| Joint.CALL (arg1, arg2, arg3) ->
1174  print_list pp.print_pass_ind (List.Cons
1175    ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1176    ((match arg1 with
1177      | Types.Inl id -> pp.print_pass_ind.print_ident id
1178      | Types.Inr arg11_arg12 ->
1179        pp.print_pass_ind.print_concat
1180          (pp.print_dpl_arg arg11_arg12.Types.fst)
1181          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1182    ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1183    List.Nil))))))))
1184| Joint.COND (arg1, arg2) ->
1185  print_list pp.print_pass_ind (List.Cons
1186    ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1187    ((pp.print_acc_a_reg arg1), (List.Cons
1188    ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1189| Joint.Step_seq seq -> print_joint_seq p globals pp seq
1190
1191(** val print_joint_fin_step :
1192    Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1193    -> 'a1 **)
1194let print_joint_fin_step p pp = function
1195| Joint.GOTO l ->
1196  print_list pp.print_pass_ind (List.Cons
1197    ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1198    ((pp.print_pass_ind.print_label l), List.Nil))))
1199| Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1200| Joint.TAILCALL (arg1, arg2) ->
1201  print_list pp.print_pass_ind (List.Cons
1202    ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1203    ((match arg1 with
1204      | Types.Inl id -> pp.print_pass_ind.print_ident id
1205      | Types.Inr arg11_arg12 ->
1206        pp.print_pass_ind.print_concat
1207          (pp.print_dpl_arg arg11_arg12.Types.fst)
1208          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1209    ((pp.print_call_args arg2), List.Nil))))))
1210
1211(** val print_joint_statement :
1212    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1213    code_iteration_params -> Joint.joint_statement -> 'a1 **)
1214let print_joint_statement p globals pp cip = function
1215| Joint.Sequential (js, arg1) ->
1216  pp.print_pass_ind.print_concat
1217    (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1218      js) (cip.print_succ arg1)
1219| Joint.Final fin ->
1220  print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1221| Joint.FCOND (arg1, arg2, arg3) ->
1222  print_list pp.print_pass_ind (List.Cons
1223    ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1224    ((pp.print_acc_a_reg arg1), (List.Cons
1225    ((pp.print_pass_ind.print_label arg2), (List.Cons
1226    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1227
1228(** val print_joint_internal_function :
1229    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1230    printing_params -> Joint.joint_internal_function -> 'a1 List.list **)
1231let print_joint_internal_function p globals cip pp f =
1232  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1233    ((print_list pp.print_pass_ind (List.Cons ((cip.print_code_point cp),
1234       (List.Cons ((print_joint_statement p globals pp cip stmt),
1235       List.Nil))))), acc)) f.Joint.joint_if_code List.Nil
1236
1237(** val print_joint_function :
1238    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1239    printing_params -> Joint.joint_function -> 'a1 List.list **)
1240let print_joint_function p globals cip pp = function
1241| AST.Internal f0 ->
1242  print_joint_internal_function p globals cip pp (Types.pi1 f0)
1243| AST.External f0 -> List.Nil
1244
1245(** val print_joint_program :
1246    Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
1247    code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list **)
1248let print_joint_program p pp prog cip =
1249  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1250    (print_joint_function p
1251      (List.map (fun x -> x.Types.fst.Types.fst)
1252        prog.Joint.joint_prog.AST.prog_vars) cip pp f.Types.snd) }, acc))
1253    List.Nil prog.Joint.joint_prog.AST.prog_funct
1254
Note: See TracBrowser for help on using the repository browser.