source: extracted/joint_printer.ml @ 2890

Last change on this file since 2890 was 2867, checked in by sacerdot, 7 years ago

New extraction after indianess bug fixes by Paolo.

File size: 51.8 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type keyword =
108| KwCOMMENT
109| KwMOVE
110| KwPOP
111| KwPUSH
112| KwADDRESS
113| KwOPACCS
114| KwOP1
115| KwOP2
116| KwCLEAR_CARRY
117| KwSET_CARRY
118| KwLOAD
119| KwSTORE
120| KwCOST_LABEL
121| KwCOND
122| KwCALL
123| KwGOTO
124| KwRETURN
125| KwTAILCALL
126| KwFCOND
127
128(** val keyword_rect_Type4 :
129    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
130    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
131let 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
132| KwCOMMENT -> h_kwCOMMENT
133| KwMOVE -> h_kwMOVE
134| KwPOP -> h_kwPOP
135| KwPUSH -> h_kwPUSH
136| KwADDRESS -> h_kwADDRESS
137| KwOPACCS -> h_kwOPACCS
138| KwOP1 -> h_kwOP1
139| KwOP2 -> h_kwOP2
140| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
141| KwSET_CARRY -> h_kwSET_CARRY
142| KwLOAD -> h_kwLOAD
143| KwSTORE -> h_kwSTORE
144| KwCOST_LABEL -> h_kwCOST_LABEL
145| KwCOND -> h_kwCOND
146| KwCALL -> h_kwCALL
147| KwGOTO -> h_kwGOTO
148| KwRETURN -> h_kwRETURN
149| KwTAILCALL -> h_kwTAILCALL
150| KwFCOND -> h_kwFCOND
151
152(** val keyword_rect_Type5 :
153    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
154    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
155let 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
156| KwCOMMENT -> h_kwCOMMENT
157| KwMOVE -> h_kwMOVE
158| KwPOP -> h_kwPOP
159| KwPUSH -> h_kwPUSH
160| KwADDRESS -> h_kwADDRESS
161| KwOPACCS -> h_kwOPACCS
162| KwOP1 -> h_kwOP1
163| KwOP2 -> h_kwOP2
164| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
165| KwSET_CARRY -> h_kwSET_CARRY
166| KwLOAD -> h_kwLOAD
167| KwSTORE -> h_kwSTORE
168| KwCOST_LABEL -> h_kwCOST_LABEL
169| KwCOND -> h_kwCOND
170| KwCALL -> h_kwCALL
171| KwGOTO -> h_kwGOTO
172| KwRETURN -> h_kwRETURN
173| KwTAILCALL -> h_kwTAILCALL
174| KwFCOND -> h_kwFCOND
175
176(** val keyword_rect_Type3 :
177    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
178    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
179let 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
180| KwCOMMENT -> h_kwCOMMENT
181| KwMOVE -> h_kwMOVE
182| KwPOP -> h_kwPOP
183| KwPUSH -> h_kwPUSH
184| KwADDRESS -> h_kwADDRESS
185| KwOPACCS -> h_kwOPACCS
186| KwOP1 -> h_kwOP1
187| KwOP2 -> h_kwOP2
188| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
189| KwSET_CARRY -> h_kwSET_CARRY
190| KwLOAD -> h_kwLOAD
191| KwSTORE -> h_kwSTORE
192| KwCOST_LABEL -> h_kwCOST_LABEL
193| KwCOND -> h_kwCOND
194| KwCALL -> h_kwCALL
195| KwGOTO -> h_kwGOTO
196| KwRETURN -> h_kwRETURN
197| KwTAILCALL -> h_kwTAILCALL
198| KwFCOND -> h_kwFCOND
199
200(** val keyword_rect_Type2 :
201    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
202    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
203let 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
204| KwCOMMENT -> h_kwCOMMENT
205| KwMOVE -> h_kwMOVE
206| KwPOP -> h_kwPOP
207| KwPUSH -> h_kwPUSH
208| KwADDRESS -> h_kwADDRESS
209| KwOPACCS -> h_kwOPACCS
210| KwOP1 -> h_kwOP1
211| KwOP2 -> h_kwOP2
212| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
213| KwSET_CARRY -> h_kwSET_CARRY
214| KwLOAD -> h_kwLOAD
215| KwSTORE -> h_kwSTORE
216| KwCOST_LABEL -> h_kwCOST_LABEL
217| KwCOND -> h_kwCOND
218| KwCALL -> h_kwCALL
219| KwGOTO -> h_kwGOTO
220| KwRETURN -> h_kwRETURN
221| KwTAILCALL -> h_kwTAILCALL
222| KwFCOND -> h_kwFCOND
223
224(** val keyword_rect_Type1 :
225    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
226    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
227let 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
228| KwCOMMENT -> h_kwCOMMENT
229| KwMOVE -> h_kwMOVE
230| KwPOP -> h_kwPOP
231| KwPUSH -> h_kwPUSH
232| KwADDRESS -> h_kwADDRESS
233| KwOPACCS -> h_kwOPACCS
234| KwOP1 -> h_kwOP1
235| KwOP2 -> h_kwOP2
236| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
237| KwSET_CARRY -> h_kwSET_CARRY
238| KwLOAD -> h_kwLOAD
239| KwSTORE -> h_kwSTORE
240| KwCOST_LABEL -> h_kwCOST_LABEL
241| KwCOND -> h_kwCOND
242| KwCALL -> h_kwCALL
243| KwGOTO -> h_kwGOTO
244| KwRETURN -> h_kwRETURN
245| KwTAILCALL -> h_kwTAILCALL
246| KwFCOND -> h_kwFCOND
247
248(** val keyword_rect_Type0 :
249    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
250    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
251let 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
252| KwCOMMENT -> h_kwCOMMENT
253| KwMOVE -> h_kwMOVE
254| KwPOP -> h_kwPOP
255| KwPUSH -> h_kwPUSH
256| KwADDRESS -> h_kwADDRESS
257| KwOPACCS -> h_kwOPACCS
258| KwOP1 -> h_kwOP1
259| KwOP2 -> h_kwOP2
260| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
261| KwSET_CARRY -> h_kwSET_CARRY
262| KwLOAD -> h_kwLOAD
263| KwSTORE -> h_kwSTORE
264| KwCOST_LABEL -> h_kwCOST_LABEL
265| KwCOND -> h_kwCOND
266| KwCALL -> h_kwCALL
267| KwGOTO -> h_kwGOTO
268| KwRETURN -> h_kwRETURN
269| KwTAILCALL -> h_kwTAILCALL
270| KwFCOND -> h_kwFCOND
271
272(** val keyword_inv_rect_Type4 :
273    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
274    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
275    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
276    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
277    -> 'a1) -> 'a1 **)
278let keyword_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
279  let hcut =
280    keyword_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
281      h17 h18 h19 hterm
282  in
283  hcut __
284
285(** val keyword_inv_rect_Type3 :
286    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
287    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
288    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
289    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
290    -> 'a1) -> 'a1 **)
291let keyword_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
292  let hcut =
293    keyword_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
294      h17 h18 h19 hterm
295  in
296  hcut __
297
298(** val keyword_inv_rect_Type2 :
299    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
300    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
301    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
302    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
303    -> 'a1) -> 'a1 **)
304let keyword_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
305  let hcut =
306    keyword_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
307      h17 h18 h19 hterm
308  in
309  hcut __
310
311(** val keyword_inv_rect_Type1 :
312    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
313    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
314    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
315    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
316    -> 'a1) -> 'a1 **)
317let keyword_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
318  let hcut =
319    keyword_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
320      h17 h18 h19 hterm
321  in
322  hcut __
323
324(** val keyword_inv_rect_Type0 :
325    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
326    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
327    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
328    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
329    -> 'a1) -> 'a1 **)
330let keyword_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
331  let hcut =
332    keyword_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
333      h17 h18 h19 hterm
334  in
335  hcut __
336
337(** val keyword_discr : keyword -> keyword -> __ **)
338let keyword_discr x y =
339  Logic.eq_rect_Type2 x
340    (match x with
341     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
342     | KwMOVE -> Obj.magic (fun _ dH -> dH)
343     | KwPOP -> Obj.magic (fun _ dH -> dH)
344     | KwPUSH -> Obj.magic (fun _ dH -> dH)
345     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
346     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
347     | KwOP1 -> Obj.magic (fun _ dH -> dH)
348     | KwOP2 -> Obj.magic (fun _ dH -> dH)
349     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
350     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
351     | KwLOAD -> Obj.magic (fun _ dH -> dH)
352     | KwSTORE -> Obj.magic (fun _ dH -> dH)
353     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
354     | KwCOND -> Obj.magic (fun _ dH -> dH)
355     | KwCALL -> Obj.magic (fun _ dH -> dH)
356     | KwGOTO -> Obj.magic (fun _ dH -> dH)
357     | KwRETURN -> Obj.magic (fun _ dH -> dH)
358     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
359     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
360
361(** val keyword_jmdiscr : keyword -> keyword -> __ **)
362let keyword_jmdiscr x y =
363  Logic.eq_rect_Type2 x
364    (match x with
365     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
366     | KwMOVE -> Obj.magic (fun _ dH -> dH)
367     | KwPOP -> Obj.magic (fun _ dH -> dH)
368     | KwPUSH -> Obj.magic (fun _ dH -> dH)
369     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
370     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
371     | KwOP1 -> Obj.magic (fun _ dH -> dH)
372     | KwOP2 -> Obj.magic (fun _ dH -> dH)
373     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
374     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
375     | KwLOAD -> Obj.magic (fun _ dH -> dH)
376     | KwSTORE -> Obj.magic (fun _ dH -> dH)
377     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
378     | KwCOND -> Obj.magic (fun _ dH -> dH)
379     | KwCALL -> Obj.magic (fun _ dH -> dH)
380     | KwGOTO -> Obj.magic (fun _ dH -> dH)
381     | KwRETURN -> Obj.magic (fun _ dH -> dH)
382     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
383     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
384
385type 'string printing_pass_independent_params = { print_String : (String.string
386                                                                 -> 'string);
387                                                  print_keyword : (keyword ->
388                                                                  'string);
389                                                  print_concat : ('string ->
390                                                                 'string ->
391                                                                 'string);
392                                                  print_empty : 'string;
393                                                  print_ident : (AST.ident ->
394                                                                'string);
395                                                  print_costlabel : (CostLabel.costlabel
396                                                                    ->
397                                                                    'string);
398                                                  print_label : (Graphs.label
399                                                                -> 'string);
400                                                  print_OpAccs : (BackEndOps.opAccs
401                                                                 -> 'string);
402                                                  print_Op1 : (BackEndOps.op1
403                                                              -> 'string);
404                                                  print_Op2 : (BackEndOps.op2
405                                                              -> 'string) }
406
407(** val printing_pass_independent_params_rect_Type4 :
408    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
409    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
410    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
411    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
412    -> 'a2 **)
413let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_549 =
414  let { print_String = print_String0; print_keyword = print_keyword0;
415    print_concat = print_concat0; print_empty = print_empty0; print_ident =
416    print_ident0; print_costlabel = print_costlabel0; print_label =
417    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
418    print_Op2 = print_Op4 } = x_549
419  in
420  h_mk_printing_pass_independent_params print_String0 print_keyword0
421    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
422    print_OpAccs0 print_Op3 print_Op4
423
424(** val printing_pass_independent_params_rect_Type5 :
425    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
426    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
427    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
428    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
429    -> 'a2 **)
430let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_551 =
431  let { print_String = print_String0; print_keyword = print_keyword0;
432    print_concat = print_concat0; print_empty = print_empty0; print_ident =
433    print_ident0; print_costlabel = print_costlabel0; print_label =
434    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
435    print_Op2 = print_Op4 } = x_551
436  in
437  h_mk_printing_pass_independent_params print_String0 print_keyword0
438    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
439    print_OpAccs0 print_Op3 print_Op4
440
441(** val printing_pass_independent_params_rect_Type3 :
442    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
443    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
444    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
445    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
446    -> 'a2 **)
447let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_553 =
448  let { print_String = print_String0; print_keyword = print_keyword0;
449    print_concat = print_concat0; print_empty = print_empty0; print_ident =
450    print_ident0; print_costlabel = print_costlabel0; print_label =
451    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
452    print_Op2 = print_Op4 } = x_553
453  in
454  h_mk_printing_pass_independent_params print_String0 print_keyword0
455    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
456    print_OpAccs0 print_Op3 print_Op4
457
458(** val printing_pass_independent_params_rect_Type2 :
459    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
460    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
461    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
462    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
463    -> 'a2 **)
464let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_555 =
465  let { print_String = print_String0; print_keyword = print_keyword0;
466    print_concat = print_concat0; print_empty = print_empty0; print_ident =
467    print_ident0; print_costlabel = print_costlabel0; print_label =
468    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
469    print_Op2 = print_Op4 } = x_555
470  in
471  h_mk_printing_pass_independent_params print_String0 print_keyword0
472    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
473    print_OpAccs0 print_Op3 print_Op4
474
475(** val printing_pass_independent_params_rect_Type1 :
476    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
477    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
478    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
479    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
480    -> 'a2 **)
481let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_557 =
482  let { print_String = print_String0; print_keyword = print_keyword0;
483    print_concat = print_concat0; print_empty = print_empty0; print_ident =
484    print_ident0; print_costlabel = print_costlabel0; print_label =
485    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
486    print_Op2 = print_Op4 } = x_557
487  in
488  h_mk_printing_pass_independent_params print_String0 print_keyword0
489    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
490    print_OpAccs0 print_Op3 print_Op4
491
492(** val printing_pass_independent_params_rect_Type0 :
493    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
494    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
495    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
496    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
497    -> 'a2 **)
498let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_559 =
499  let { print_String = print_String0; print_keyword = print_keyword0;
500    print_concat = print_concat0; print_empty = print_empty0; print_ident =
501    print_ident0; print_costlabel = print_costlabel0; print_label =
502    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
503    print_Op2 = print_Op4 } = x_559
504  in
505  h_mk_printing_pass_independent_params print_String0 print_keyword0
506    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
507    print_OpAccs0 print_Op3 print_Op4
508
509(** val print_String :
510    'a1 printing_pass_independent_params -> String.string -> 'a1 **)
511let rec print_String xxx =
512  xxx.print_String
513
514(** val print_keyword :
515    'a1 printing_pass_independent_params -> keyword -> 'a1 **)
516let rec print_keyword xxx =
517  xxx.print_keyword
518
519(** val print_concat :
520    'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
521let rec print_concat xxx =
522  xxx.print_concat
523
524(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
525let rec print_empty xxx =
526  xxx.print_empty
527
528(** val print_ident :
529    'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
530let rec print_ident xxx =
531  xxx.print_ident
532
533(** val print_costlabel :
534    'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
535let rec print_costlabel xxx =
536  xxx.print_costlabel
537
538(** val print_label :
539    'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
540let rec print_label xxx =
541  xxx.print_label
542
543(** val print_OpAccs :
544    'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
545let rec print_OpAccs xxx =
546  xxx.print_OpAccs
547
548(** val print_Op1 :
549    'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
550let rec print_Op1 xxx =
551  xxx.print_Op1
552
553(** val print_Op2 :
554    'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
555let rec print_Op2 xxx =
556  xxx.print_Op2
557
558(** val printing_pass_independent_params_inv_rect_Type4 :
559    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
560    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
561    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
562    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
563    -> 'a1) -> __ -> 'a2) -> 'a2 **)
564let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
565  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
566
567(** val printing_pass_independent_params_inv_rect_Type3 :
568    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
569    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
570    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
571    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
572    -> 'a1) -> __ -> 'a2) -> 'a2 **)
573let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
574  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
575
576(** val printing_pass_independent_params_inv_rect_Type2 :
577    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
578    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
579    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
580    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
581    -> 'a1) -> __ -> 'a2) -> 'a2 **)
582let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
583  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
584
585(** val printing_pass_independent_params_inv_rect_Type1 :
586    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
587    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
588    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
589    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
590    -> 'a1) -> __ -> 'a2) -> 'a2 **)
591let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
592  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
593
594(** val printing_pass_independent_params_inv_rect_Type0 :
595    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
596    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
597    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
598    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
599    -> 'a1) -> __ -> 'a2) -> 'a2 **)
600let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
601  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
602
603(** val printing_pass_independent_params_jmdiscr :
604    'a1 printing_pass_independent_params -> 'a1
605    printing_pass_independent_params -> __ **)
606let printing_pass_independent_params_jmdiscr x y =
607  Logic.eq_rect_Type2 x
608    (let { print_String = a0; print_keyword = a10; print_concat = a2;
609       print_empty = a3; print_ident = a4; print_costlabel = a5;
610       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 =
611       a9 } = x
612     in
613    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
614
615type 'string printing_params = { print_pass_ind : 'string
616                                                  printing_pass_independent_params;
617                                 print_acc_a_reg : (__ -> 'string);
618                                 print_acc_b_reg : (__ -> 'string);
619                                 print_acc_a_arg : (__ -> 'string);
620                                 print_acc_b_arg : (__ -> 'string);
621                                 print_dpl_reg : (__ -> 'string);
622                                 print_dph_reg : (__ -> 'string);
623                                 print_dpl_arg : (__ -> 'string);
624                                 print_dph_arg : (__ -> 'string);
625                                 print_snd_arg : (__ -> 'string);
626                                 print_pair_move : (__ -> 'string);
627                                 print_call_args : (__ -> 'string);
628                                 print_call_dest : (__ -> 'string);
629                                 print_ext_seq : (__ -> 'string) }
630
631(** val printing_params_rect_Type4 :
632    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
633    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
634    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
635    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
636    printing_params -> 'a2 **)
637let rec printing_params_rect_Type4 p h_mk_printing_params x_585 =
638  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
639    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
640    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
641    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
642    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
643    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
644    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
645    x_585
646  in
647  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
648    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
649    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
650    print_call_args0 print_call_dest0 print_ext_seq0
651
652(** val printing_params_rect_Type5 :
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_Type5 p h_mk_printing_params x_587 =
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_587
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_Type3 :
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_Type3 p h_mk_printing_params x_589 =
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_589
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_Type2 :
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_Type2 p h_mk_printing_params x_591 =
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_591
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_Type1 :
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_Type1 p h_mk_printing_params x_593 =
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_593
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_Type0 :
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_Type0 p h_mk_printing_params x_595 =
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_595
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 print_pass_ind :
758    Joint.unserialized_params -> 'a1 printing_params -> 'a1
759    printing_pass_independent_params **)
760let rec print_pass_ind p xxx =
761  xxx.print_pass_ind
762
763(** val print_acc_a_reg :
764    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
765let rec print_acc_a_reg p xxx =
766  xxx.print_acc_a_reg
767
768(** val print_acc_b_reg :
769    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
770let rec print_acc_b_reg p xxx =
771  xxx.print_acc_b_reg
772
773(** val print_acc_a_arg :
774    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
775let rec print_acc_a_arg p xxx =
776  xxx.print_acc_a_arg
777
778(** val print_acc_b_arg :
779    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
780let rec print_acc_b_arg p xxx =
781  xxx.print_acc_b_arg
782
783(** val print_dpl_reg :
784    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
785let rec print_dpl_reg p xxx =
786  xxx.print_dpl_reg
787
788(** val print_dph_reg :
789    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
790let rec print_dph_reg p xxx =
791  xxx.print_dph_reg
792
793(** val print_dpl_arg :
794    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
795let rec print_dpl_arg p xxx =
796  xxx.print_dpl_arg
797
798(** val print_dph_arg :
799    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
800let rec print_dph_arg p xxx =
801  xxx.print_dph_arg
802
803(** val print_snd_arg :
804    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
805let rec print_snd_arg p xxx =
806  xxx.print_snd_arg
807
808(** val print_pair_move :
809    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
810let rec print_pair_move p xxx =
811  xxx.print_pair_move
812
813(** val print_call_args :
814    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
815let rec print_call_args p xxx =
816  xxx.print_call_args
817
818(** val print_call_dest :
819    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
820let rec print_call_dest p xxx =
821  xxx.print_call_dest
822
823(** val print_ext_seq :
824    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
825let rec print_ext_seq p xxx =
826  xxx.print_ext_seq
827
828(** val printing_params_inv_rect_Type4 :
829    Joint.unserialized_params -> 'a1 printing_params -> ('a1
830    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
831    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
832    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
833    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
834let printing_params_inv_rect_Type4 x2 hterm h1 =
835  let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
836
837(** val printing_params_inv_rect_Type3 :
838    Joint.unserialized_params -> 'a1 printing_params -> ('a1
839    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
840    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
841    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
842    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
843let printing_params_inv_rect_Type3 x2 hterm h1 =
844  let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
845
846(** val printing_params_inv_rect_Type2 :
847    Joint.unserialized_params -> 'a1 printing_params -> ('a1
848    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
849    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
850    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
851    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
852let printing_params_inv_rect_Type2 x2 hterm h1 =
853  let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
854
855(** val printing_params_inv_rect_Type1 :
856    Joint.unserialized_params -> 'a1 printing_params -> ('a1
857    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
858    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
859    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
860    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
861let printing_params_inv_rect_Type1 x2 hterm h1 =
862  let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
863
864(** val printing_params_inv_rect_Type0 :
865    Joint.unserialized_params -> 'a1 printing_params -> ('a1
866    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
867    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
868    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
869    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
870let printing_params_inv_rect_Type0 x2 hterm h1 =
871  let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
872
873(** val printing_params_jmdiscr :
874    Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
875    -> __ **)
876let printing_params_jmdiscr a2 x y =
877  Logic.eq_rect_Type2 x
878    (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
879       print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
880       print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
881       print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
882       print_call_dest = a12; print_ext_seq = a13 } = x
883     in
884    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
885
886(** val dpi1__o__print_pass_ind__o__inject :
887    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
888    'a1 printing_pass_independent_params Types.sig0 **)
889let dpi1__o__print_pass_ind__o__inject x1 x4 =
890  x4.Types.dpi1.print_pass_ind
891
892(** val eject__o__print_pass_ind__o__inject :
893    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
894    printing_pass_independent_params Types.sig0 **)
895let eject__o__print_pass_ind__o__inject x1 x4 =
896  (Types.pi1 x4).print_pass_ind
897
898(** val print_pass_ind__o__inject :
899    Joint.unserialized_params -> 'a1 printing_params -> 'a1
900    printing_pass_independent_params Types.sig0 **)
901let print_pass_ind__o__inject x1 x3 =
902  x3.print_pass_ind
903
904(** val dpi1__o__print_pass_ind :
905    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
906    'a1 printing_pass_independent_params **)
907let dpi1__o__print_pass_ind x1 x3 =
908  x3.Types.dpi1.print_pass_ind
909
910(** val eject__o__print_pass_ind :
911    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
912    printing_pass_independent_params **)
913let eject__o__print_pass_ind x1 x3 =
914  (Types.pi1 x3).print_pass_ind
915
916type 'string code_iteration_params = { fold_code : (__ -> (__ ->
917                                                   Joint.joint_statement ->
918                                                   __ -> __) -> __ -> __ ->
919                                                   __);
920                                       print_succ : (__ -> 'string);
921                                       print_code_point : (__ -> 'string) }
922
923(** val code_iteration_params_rect_Type4 :
924    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
925    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
926    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
927let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_624 =
928  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
929    print_code_point0 } = x_624
930  in
931  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
932
933(** val code_iteration_params_rect_Type5 :
934    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
935    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
936    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
937let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_626 =
938  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
939    print_code_point0 } = x_626
940  in
941  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
942
943(** val code_iteration_params_rect_Type3 :
944    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
945    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
946    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
947let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_628 =
948  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
949    print_code_point0 } = x_628
950  in
951  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
952
953(** val code_iteration_params_rect_Type2 :
954    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
955    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
956    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
957let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_630 =
958  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
959    print_code_point0 } = x_630
960  in
961  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
962
963(** val code_iteration_params_rect_Type1 :
964    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
965    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
966    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
967let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_632 =
968  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
969    print_code_point0 } = x_632
970  in
971  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
972
973(** val code_iteration_params_rect_Type0 :
974    Joint.params -> AST.ident List.list -> ((__ -> (__ ->
975    Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) ->
976    (__ -> 'a1) -> 'a2) -> 'a1 code_iteration_params -> 'a2 **)
977let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_634 =
978  let { fold_code = fold_code0; print_succ = print_succ0; print_code_point =
979    print_code_point0 } = x_634
980  in
981  h_mk_code_iteration_params fold_code0 print_succ0 print_code_point0
982
983(** val fold_code0 :
984    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__
985    -> Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2 **)
986let rec fold_code0 p globals xxx x_650 x_651 x_652 =
987  (let { fold_code = yyy; print_succ = x; print_code_point = x0 } = xxx in
988  Obj.magic yyy) __ x_650 x_651 x_652
989
990(** val print_succ :
991    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
992    'a1 **)
993let rec print_succ p globals xxx =
994  xxx.print_succ
995
996(** val print_code_point :
997    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
998    'a1 **)
999let rec print_code_point p globals xxx =
1000  xxx.print_code_point
1001
1002(** val code_iteration_params_inv_rect_Type4 :
1003    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1004    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1005    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1006let code_iteration_params_inv_rect_Type4 x2 x3 hterm h1 =
1007  let hcut = code_iteration_params_rect_Type4 x2 x3 h1 hterm in hcut __
1008
1009(** val code_iteration_params_inv_rect_Type3 :
1010    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__
1011    -> (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ ->
1012    'a1) -> (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
1013let code_iteration_params_inv_rect_Type3 x2 x3 hterm h1 =
1014  let hcut = code_iteration_params_rect_Type3 x2 x3 h1 hterm in hcut __
1015
1016(** val code_iteration_params_inv_rect_Type2 :
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_Type2 x2 x3 hterm h1 =
1021  let hcut = code_iteration_params_rect_Type2 x2 x3 h1 hterm in hcut __
1022
1023(** val code_iteration_params_inv_rect_Type1 :
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_Type1 x2 x3 hterm h1 =
1028  let hcut = code_iteration_params_rect_Type1 x2 x3 h1 hterm in hcut __
1029
1030(** val code_iteration_params_inv_rect_Type0 :
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_Type0 x2 x3 hterm h1 =
1035  let hcut = code_iteration_params_rect_Type0 x2 x3 h1 hterm in hcut __
1036
1037(** val code_iteration_params_jmdiscr :
1038    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1039    code_iteration_params -> __ **)
1040let code_iteration_params_jmdiscr a2 a3 x y =
1041  Logic.eq_rect_Type2 x
1042    (let { fold_code = a0; print_succ = a10; print_code_point = a20 } = x in
1043    Obj.magic (fun _ dH -> dH __ __ __)) y
1044
1045(** val pm_choose_with_pref :
1046    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1047    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1048    Types.option **)
1049let pm_choose_with_pref m = function
1050| Types.None -> PositiveMap.pm_choose m
1051| Types.Some p ->
1052  (match PositiveMap.pm_try_remove p m with
1053   | Types.None -> PositiveMap.pm_choose m
1054   | Types.Some res ->
1055     let { Types.fst = a; Types.snd = m' } = res in
1056     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1057     m' })
1058
1059(** val visit_graph :
1060    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1061    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1062    Nat.nat -> 'a2 **)
1063let rec visit_graph next f b n m = function
1064| Nat.O -> b
1065| Nat.S y ->
1066  (match pm_choose_with_pref m n with
1067   | Types.None -> b
1068   | Types.Some res ->
1069     let { Types.fst = eta6; Types.snd = m' } = res in
1070     let { Types.fst = pos; Types.snd = a } = eta6 in
1071     visit_graph next f (f pos a b) (next a) m' y)
1072
1073(** val graph_code_iteration_params :
1074    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1075    code_iteration_params **)
1076let graph_code_iteration_params gp globals pp =
1077  { fold_code = (fun _ f m a ->
1078    visit_graph (fun stmt ->
1079      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1080              globals stmt with
1081      | Types.None -> Types.None
1082      | Types.Some label -> let p = label in Types.Some p) (fun n ->
1083      Obj.magic f n) a (Types.Some Positive.One) (let m' = Obj.magic m in m')
1084      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1085    print_succ = (Obj.magic pp.print_pass_ind.print_label);
1086    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1087
1088(** val print_list :
1089    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1090let print_list pp =
1091  List.foldr pp.print_concat pp.print_empty
1092
1093(** val print_joint_seq :
1094    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1095    -> Joint.joint_seq -> 'a1 **)
1096let print_joint_seq p globals pp = function
1097| Joint.COMMENT str ->
1098  print_list pp.print_pass_ind (List.Cons
1099    ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1100    ((pp.print_pass_ind.print_String str), List.Nil))))
1101| Joint.MOVE pm ->
1102  print_list pp.print_pass_ind (List.Cons
1103    ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1104    ((pp.print_pair_move pm), List.Nil))))
1105| Joint.POP arg ->
1106  print_list pp.print_pass_ind (List.Cons
1107    ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1108    ((pp.print_acc_a_reg arg), List.Nil))))
1109| Joint.PUSH arg ->
1110  print_list pp.print_pass_ind (List.Cons
1111    ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1112    ((pp.print_acc_a_arg arg), List.Nil))))
1113| Joint.ADDRESS (i, arg1, arg2) ->
1114  print_list pp.print_pass_ind (List.Cons
1115    ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1116    ((pp.print_pass_ind.print_ident i), (List.Cons ((pp.print_dpl_reg arg1),
1117    (List.Cons ((pp.print_dph_reg arg2), List.Nil))))))))
1118| Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1119  print_list pp.print_pass_ind (List.Cons
1120    ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1121    ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1122    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1123    (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1124    ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1125| Joint.OP1 (op1, arg1, arg2) ->
1126  print_list pp.print_pass_ind (List.Cons
1127    ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1128    ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1129    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1130    List.Nil))))))))
1131| Joint.OP2 (op2, arg1, arg2, arg3) ->
1132  print_list pp.print_pass_ind (List.Cons
1133    ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1134    ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1135    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1136    (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1137| Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1138| Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1139| Joint.LOAD (arg1, arg2, arg3) ->
1140  print_list pp.print_pass_ind (List.Cons
1141    ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1142    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1143    (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1144| Joint.STORE (arg1, arg2, arg3) ->
1145  print_list pp.print_pass_ind (List.Cons
1146    ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1147    ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1148    ((pp.print_acc_a_arg arg3), List.Nil))))))))
1149| Joint.Extension_seq ext -> pp.print_ext_seq ext
1150
1151(** val print_joint_step :
1152    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1153    -> Joint.joint_step -> 'a1 **)
1154let print_joint_step p globals pp = function
1155| Joint.COST_LABEL arg ->
1156  print_list pp.print_pass_ind (List.Cons
1157    ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1158    ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1159| Joint.CALL (arg1, arg2, arg3) ->
1160  print_list pp.print_pass_ind (List.Cons
1161    ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1162    ((match arg1 with
1163      | Types.Inl id -> pp.print_pass_ind.print_ident id
1164      | Types.Inr arg11_arg12 ->
1165        pp.print_pass_ind.print_concat
1166          (pp.print_dpl_arg arg11_arg12.Types.fst)
1167          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1168    ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1169    List.Nil))))))))
1170| Joint.COND (arg1, arg2) ->
1171  print_list pp.print_pass_ind (List.Cons
1172    ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1173    ((pp.print_acc_a_reg arg1), (List.Cons
1174    ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1175| Joint.Step_seq seq -> print_joint_seq p globals pp seq
1176
1177(** val print_joint_fin_step :
1178    Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1179    -> 'a1 **)
1180let print_joint_fin_step p pp = function
1181| Joint.GOTO l ->
1182  print_list pp.print_pass_ind (List.Cons
1183    ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1184    ((pp.print_pass_ind.print_label l), List.Nil))))
1185| Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1186| Joint.TAILCALL (arg1, arg2) ->
1187  print_list pp.print_pass_ind (List.Cons
1188    ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1189    ((match arg1 with
1190      | Types.Inl id -> pp.print_pass_ind.print_ident id
1191      | Types.Inr arg11_arg12 ->
1192        pp.print_pass_ind.print_concat
1193          (pp.print_dpl_arg arg11_arg12.Types.fst)
1194          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1195    ((pp.print_call_args arg2), List.Nil))))))
1196
1197(** val print_joint_statement :
1198    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1199    code_iteration_params -> Joint.joint_statement -> 'a1 **)
1200let print_joint_statement p globals pp cip = function
1201| Joint.Sequential (js, arg1) ->
1202  pp.print_pass_ind.print_concat
1203    (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1204      js) (cip.print_succ arg1)
1205| Joint.Final fin ->
1206  print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1207| Joint.FCOND (arg1, arg2, arg3) ->
1208  print_list pp.print_pass_ind (List.Cons
1209    ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1210    ((pp.print_acc_a_reg arg1), (List.Cons
1211    ((pp.print_pass_ind.print_label arg2), (List.Cons
1212    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1213
1214(** val print_joint_internal_function :
1215    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1216    printing_params -> Joint.joint_internal_function -> 'a1 List.list **)
1217let print_joint_internal_function p globals cip pp f =
1218  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1219    ((print_list pp.print_pass_ind (List.Cons ((cip.print_code_point cp),
1220       (List.Cons ((print_joint_statement p globals pp cip stmt),
1221       List.Nil))))), acc)) f.Joint.joint_if_code List.Nil
1222
1223(** val print_joint_function :
1224    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
1225    printing_params -> Joint.joint_function -> 'a1 List.list **)
1226let print_joint_function p globals cip pp = function
1227| AST.Internal f0 ->
1228  print_joint_internal_function p globals cip pp (Types.pi1 f0)
1229| AST.External f0 -> List.Nil
1230
1231(** val print_joint_program :
1232    Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
1233    code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list **)
1234let print_joint_program p pp prog cip =
1235  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1236    (print_joint_function p
1237      (List.map (fun x -> x.Types.fst.Types.fst) prog.AST.prog_vars) cip pp
1238      f.Types.snd) }, acc)) List.Nil prog.AST.prog_funct
1239
Note: See TracBrowser for help on using the repository browser.