source: driver/extracted/joint_printer.ml @ 3106

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

New extraction.

File size: 62.5 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121type keyword =
122| KwCOMMENT
123| KwMOVE
124| KwPOP
125| KwPUSH
126| KwADDRESS
127| KwOPACCS
128| KwOP1
129| KwOP2
130| KwCLEAR_CARRY
131| KwSET_CARRY
132| KwLOAD
133| KwSTORE
134| KwCOST_LABEL
135| KwCOND
136| KwCALL
137| KwGOTO
138| KwRETURN
139| KwTAILCALL
140| KwFCOND
141
142(** val keyword_rect_Type4 :
143    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
144    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
145let rec keyword_rect_Type4 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
146| KwCOMMENT -> h_kwCOMMENT
147| KwMOVE -> h_kwMOVE
148| KwPOP -> h_kwPOP
149| KwPUSH -> h_kwPUSH
150| KwADDRESS -> h_kwADDRESS
151| KwOPACCS -> h_kwOPACCS
152| KwOP1 -> h_kwOP1
153| KwOP2 -> h_kwOP2
154| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
155| KwSET_CARRY -> h_kwSET_CARRY
156| KwLOAD -> h_kwLOAD
157| KwSTORE -> h_kwSTORE
158| KwCOST_LABEL -> h_kwCOST_LABEL
159| KwCOND -> h_kwCOND
160| KwCALL -> h_kwCALL
161| KwGOTO -> h_kwGOTO
162| KwRETURN -> h_kwRETURN
163| KwTAILCALL -> h_kwTAILCALL
164| KwFCOND -> h_kwFCOND
165
166(** val keyword_rect_Type5 :
167    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
168    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
169let rec keyword_rect_Type5 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
170| KwCOMMENT -> h_kwCOMMENT
171| KwMOVE -> h_kwMOVE
172| KwPOP -> h_kwPOP
173| KwPUSH -> h_kwPUSH
174| KwADDRESS -> h_kwADDRESS
175| KwOPACCS -> h_kwOPACCS
176| KwOP1 -> h_kwOP1
177| KwOP2 -> h_kwOP2
178| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
179| KwSET_CARRY -> h_kwSET_CARRY
180| KwLOAD -> h_kwLOAD
181| KwSTORE -> h_kwSTORE
182| KwCOST_LABEL -> h_kwCOST_LABEL
183| KwCOND -> h_kwCOND
184| KwCALL -> h_kwCALL
185| KwGOTO -> h_kwGOTO
186| KwRETURN -> h_kwRETURN
187| KwTAILCALL -> h_kwTAILCALL
188| KwFCOND -> h_kwFCOND
189
190(** val keyword_rect_Type3 :
191    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
192    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
193let rec keyword_rect_Type3 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
194| KwCOMMENT -> h_kwCOMMENT
195| KwMOVE -> h_kwMOVE
196| KwPOP -> h_kwPOP
197| KwPUSH -> h_kwPUSH
198| KwADDRESS -> h_kwADDRESS
199| KwOPACCS -> h_kwOPACCS
200| KwOP1 -> h_kwOP1
201| KwOP2 -> h_kwOP2
202| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
203| KwSET_CARRY -> h_kwSET_CARRY
204| KwLOAD -> h_kwLOAD
205| KwSTORE -> h_kwSTORE
206| KwCOST_LABEL -> h_kwCOST_LABEL
207| KwCOND -> h_kwCOND
208| KwCALL -> h_kwCALL
209| KwGOTO -> h_kwGOTO
210| KwRETURN -> h_kwRETURN
211| KwTAILCALL -> h_kwTAILCALL
212| KwFCOND -> h_kwFCOND
213
214(** val keyword_rect_Type2 :
215    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
216    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
217let rec keyword_rect_Type2 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
218| KwCOMMENT -> h_kwCOMMENT
219| KwMOVE -> h_kwMOVE
220| KwPOP -> h_kwPOP
221| KwPUSH -> h_kwPUSH
222| KwADDRESS -> h_kwADDRESS
223| KwOPACCS -> h_kwOPACCS
224| KwOP1 -> h_kwOP1
225| KwOP2 -> h_kwOP2
226| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
227| KwSET_CARRY -> h_kwSET_CARRY
228| KwLOAD -> h_kwLOAD
229| KwSTORE -> h_kwSTORE
230| KwCOST_LABEL -> h_kwCOST_LABEL
231| KwCOND -> h_kwCOND
232| KwCALL -> h_kwCALL
233| KwGOTO -> h_kwGOTO
234| KwRETURN -> h_kwRETURN
235| KwTAILCALL -> h_kwTAILCALL
236| KwFCOND -> h_kwFCOND
237
238(** val keyword_rect_Type1 :
239    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
240    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
241let rec keyword_rect_Type1 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
242| KwCOMMENT -> h_kwCOMMENT
243| KwMOVE -> h_kwMOVE
244| KwPOP -> h_kwPOP
245| KwPUSH -> h_kwPUSH
246| KwADDRESS -> h_kwADDRESS
247| KwOPACCS -> h_kwOPACCS
248| KwOP1 -> h_kwOP1
249| KwOP2 -> h_kwOP2
250| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
251| KwSET_CARRY -> h_kwSET_CARRY
252| KwLOAD -> h_kwLOAD
253| KwSTORE -> h_kwSTORE
254| KwCOST_LABEL -> h_kwCOST_LABEL
255| KwCOND -> h_kwCOND
256| KwCALL -> h_kwCALL
257| KwGOTO -> h_kwGOTO
258| KwRETURN -> h_kwRETURN
259| KwTAILCALL -> h_kwTAILCALL
260| KwFCOND -> h_kwFCOND
261
262(** val keyword_rect_Type0 :
263    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
264    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1 **)
265let rec keyword_rect_Type0 h_kwCOMMENT h_kwMOVE h_kwPOP h_kwPUSH h_kwADDRESS h_kwOPACCS h_kwOP1 h_kwOP2 h_kwCLEAR_CARRY h_kwSET_CARRY h_kwLOAD h_kwSTORE h_kwCOST_LABEL h_kwCOND h_kwCALL h_kwGOTO h_kwRETURN h_kwTAILCALL h_kwFCOND = function
266| KwCOMMENT -> h_kwCOMMENT
267| KwMOVE -> h_kwMOVE
268| KwPOP -> h_kwPOP
269| KwPUSH -> h_kwPUSH
270| KwADDRESS -> h_kwADDRESS
271| KwOPACCS -> h_kwOPACCS
272| KwOP1 -> h_kwOP1
273| KwOP2 -> h_kwOP2
274| KwCLEAR_CARRY -> h_kwCLEAR_CARRY
275| KwSET_CARRY -> h_kwSET_CARRY
276| KwLOAD -> h_kwLOAD
277| KwSTORE -> h_kwSTORE
278| KwCOST_LABEL -> h_kwCOST_LABEL
279| KwCOND -> h_kwCOND
280| KwCALL -> h_kwCALL
281| KwGOTO -> h_kwGOTO
282| KwRETURN -> h_kwRETURN
283| KwTAILCALL -> h_kwTAILCALL
284| KwFCOND -> h_kwFCOND
285
286(** val keyword_inv_rect_Type4 :
287    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
288    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
289    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
291    -> 'a1) -> 'a1 **)
292let keyword_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
293  let hcut =
294    keyword_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
295      h17 h18 h19 hterm
296  in
297  hcut __
298
299(** val keyword_inv_rect_Type3 :
300    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
301    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
302    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
303    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
304    -> 'a1) -> 'a1 **)
305let keyword_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
306  let hcut =
307    keyword_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
308      h17 h18 h19 hterm
309  in
310  hcut __
311
312(** val keyword_inv_rect_Type2 :
313    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
314    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
315    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
316    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
317    -> 'a1) -> 'a1 **)
318let keyword_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
319  let hcut =
320    keyword_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
321      h17 h18 h19 hterm
322  in
323  hcut __
324
325(** val keyword_inv_rect_Type1 :
326    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
327    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
328    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
329    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
330    -> 'a1) -> 'a1 **)
331let keyword_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
332  let hcut =
333    keyword_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
334      h17 h18 h19 hterm
335  in
336  hcut __
337
338(** val keyword_inv_rect_Type0 :
339    keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
340    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
341    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
342    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
343    -> 'a1) -> 'a1 **)
344let keyword_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
345  let hcut =
346    keyword_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
347      h17 h18 h19 hterm
348  in
349  hcut __
350
351(** val keyword_discr : keyword -> keyword -> __ **)
352let keyword_discr x y =
353  Logic.eq_rect_Type2 x
354    (match x with
355     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
356     | KwMOVE -> Obj.magic (fun _ dH -> dH)
357     | KwPOP -> Obj.magic (fun _ dH -> dH)
358     | KwPUSH -> Obj.magic (fun _ dH -> dH)
359     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
360     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
361     | KwOP1 -> Obj.magic (fun _ dH -> dH)
362     | KwOP2 -> Obj.magic (fun _ dH -> dH)
363     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
364     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
365     | KwLOAD -> Obj.magic (fun _ dH -> dH)
366     | KwSTORE -> Obj.magic (fun _ dH -> dH)
367     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
368     | KwCOND -> Obj.magic (fun _ dH -> dH)
369     | KwCALL -> Obj.magic (fun _ dH -> dH)
370     | KwGOTO -> Obj.magic (fun _ dH -> dH)
371     | KwRETURN -> Obj.magic (fun _ dH -> dH)
372     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
373     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
374
375(** val keyword_jmdiscr : keyword -> keyword -> __ **)
376let keyword_jmdiscr x y =
377  Logic.eq_rect_Type2 x
378    (match x with
379     | KwCOMMENT -> Obj.magic (fun _ dH -> dH)
380     | KwMOVE -> Obj.magic (fun _ dH -> dH)
381     | KwPOP -> Obj.magic (fun _ dH -> dH)
382     | KwPUSH -> Obj.magic (fun _ dH -> dH)
383     | KwADDRESS -> Obj.magic (fun _ dH -> dH)
384     | KwOPACCS -> Obj.magic (fun _ dH -> dH)
385     | KwOP1 -> Obj.magic (fun _ dH -> dH)
386     | KwOP2 -> Obj.magic (fun _ dH -> dH)
387     | KwCLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
388     | KwSET_CARRY -> Obj.magic (fun _ dH -> dH)
389     | KwLOAD -> Obj.magic (fun _ dH -> dH)
390     | KwSTORE -> Obj.magic (fun _ dH -> dH)
391     | KwCOST_LABEL -> Obj.magic (fun _ dH -> dH)
392     | KwCOND -> Obj.magic (fun _ dH -> dH)
393     | KwCALL -> Obj.magic (fun _ dH -> dH)
394     | KwGOTO -> Obj.magic (fun _ dH -> dH)
395     | KwRETURN -> Obj.magic (fun _ dH -> dH)
396     | KwTAILCALL -> Obj.magic (fun _ dH -> dH)
397     | KwFCOND -> Obj.magic (fun _ dH -> dH)) y
398
399type 'string printing_pass_independent_params = { print_String : (String.string
400                                                                 -> 'string);
401                                                  print_keyword : (keyword ->
402                                                                  'string);
403                                                  print_concat : ('string ->
404                                                                 'string ->
405                                                                 'string);
406                                                  print_empty : 'string;
407                                                  print_ident : (AST.ident ->
408                                                                'string);
409                                                  print_costlabel : (CostLabel.costlabel
410                                                                    ->
411                                                                    'string);
412                                                  print_label : (Graphs.label
413                                                                -> 'string);
414                                                  print_OpAccs : (BackEndOps.opAccs
415                                                                 -> 'string);
416                                                  print_Op1 : (BackEndOps.op1
417                                                              -> 'string);
418                                                  print_Op2 : (BackEndOps.op2
419                                                              -> 'string);
420                                                  print_nat : (Nat.nat ->
421                                                              'string);
422                                                  print_bitvector : (Nat.nat
423                                                                    ->
424                                                                    BitVector.bitVector
425                                                                    ->
426                                                                    'string) }
427
428(** val printing_pass_independent_params_rect_Type4 :
429    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
430    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
431    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
432    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
433    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
434    printing_pass_independent_params -> 'a2 **)
435let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
436  let { print_String = print_String0; print_keyword = print_keyword0;
437    print_concat = print_concat0; print_empty = print_empty0; print_ident =
438    print_ident0; print_costlabel = print_costlabel0; print_label =
439    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
440    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
441    print_bitvector0 } = x_25506
442  in
443  h_mk_printing_pass_independent_params print_String0 print_keyword0
444    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
445    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
446
447(** val printing_pass_independent_params_rect_Type5 :
448    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
449    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
450    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
451    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
452    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
453    printing_pass_independent_params -> 'a2 **)
454let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
455  let { print_String = print_String0; print_keyword = print_keyword0;
456    print_concat = print_concat0; print_empty = print_empty0; print_ident =
457    print_ident0; print_costlabel = print_costlabel0; print_label =
458    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
459    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
460    print_bitvector0 } = x_25508
461  in
462  h_mk_printing_pass_independent_params print_String0 print_keyword0
463    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
464    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
465
466(** val printing_pass_independent_params_rect_Type3 :
467    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
468    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
469    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
470    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
471    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
472    printing_pass_independent_params -> 'a2 **)
473let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
474  let { print_String = print_String0; print_keyword = print_keyword0;
475    print_concat = print_concat0; print_empty = print_empty0; print_ident =
476    print_ident0; print_costlabel = print_costlabel0; print_label =
477    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
478    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
479    print_bitvector0 } = x_25510
480  in
481  h_mk_printing_pass_independent_params print_String0 print_keyword0
482    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
483    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
484
485(** val printing_pass_independent_params_rect_Type2 :
486    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
487    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
488    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
489    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
490    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
491    printing_pass_independent_params -> 'a2 **)
492let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
493  let { print_String = print_String0; print_keyword = print_keyword0;
494    print_concat = print_concat0; print_empty = print_empty0; print_ident =
495    print_ident0; print_costlabel = print_costlabel0; print_label =
496    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
497    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
498    print_bitvector0 } = x_25512
499  in
500  h_mk_printing_pass_independent_params print_String0 print_keyword0
501    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
502    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
503
504(** val printing_pass_independent_params_rect_Type1 :
505    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
506    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
507    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
508    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
509    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
510    printing_pass_independent_params -> 'a2 **)
511let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
512  let { print_String = print_String0; print_keyword = print_keyword0;
513    print_concat = print_concat0; print_empty = print_empty0; print_ident =
514    print_ident0; print_costlabel = print_costlabel0; print_label =
515    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
516    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
517    print_bitvector0 } = x_25514
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 print_nat0 print_bitvector0
522
523(** val printing_pass_independent_params_rect_Type0 :
524    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
525    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
526    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
527    (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
528    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
529    printing_pass_independent_params -> 'a2 **)
530let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
531  let { print_String = print_String0; print_keyword = print_keyword0;
532    print_concat = print_concat0; print_empty = print_empty0; print_ident =
533    print_ident0; print_costlabel = print_costlabel0; print_label =
534    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
535    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
536    print_bitvector0 } = x_25516
537  in
538  h_mk_printing_pass_independent_params print_String0 print_keyword0
539    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
540    print_OpAccs0 print_Op3 print_Op4 print_nat0 print_bitvector0
541
542(** val print_String :
543    'a1 printing_pass_independent_params -> String.string -> 'a1 **)
544let rec print_String xxx =
545  xxx.print_String
546
547(** val print_keyword :
548    'a1 printing_pass_independent_params -> keyword -> 'a1 **)
549let rec print_keyword xxx =
550  xxx.print_keyword
551
552(** val print_concat :
553    'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1 **)
554let rec print_concat xxx =
555  xxx.print_concat
556
557(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
558let rec print_empty xxx =
559  xxx.print_empty
560
561(** val print_ident :
562    'a1 printing_pass_independent_params -> AST.ident -> 'a1 **)
563let rec print_ident xxx =
564  xxx.print_ident
565
566(** val print_costlabel :
567    'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1 **)
568let rec print_costlabel xxx =
569  xxx.print_costlabel
570
571(** val print_label :
572    'a1 printing_pass_independent_params -> Graphs.label -> 'a1 **)
573let rec print_label xxx =
574  xxx.print_label
575
576(** val print_OpAccs :
577    'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1 **)
578let rec print_OpAccs xxx =
579  xxx.print_OpAccs
580
581(** val print_Op1 :
582    'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1 **)
583let rec print_Op1 xxx =
584  xxx.print_Op1
585
586(** val print_Op2 :
587    'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1 **)
588let rec print_Op2 xxx =
589  xxx.print_Op2
590
591(** val print_nat :
592    'a1 printing_pass_independent_params -> Nat.nat -> 'a1 **)
593let rec print_nat xxx =
594  xxx.print_nat
595
596(** val print_bitvector :
597    'a1 printing_pass_independent_params -> Nat.nat -> BitVector.bitVector ->
598    'a1 **)
599let rec print_bitvector xxx =
600  xxx.print_bitvector
601
602(** val printing_pass_independent_params_inv_rect_Type4 :
603    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
604    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
605    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
606    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
607    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
608    __ -> 'a2) -> 'a2 **)
609let printing_pass_independent_params_inv_rect_Type4 hterm h1 =
610  let hcut = printing_pass_independent_params_rect_Type4 h1 hterm in hcut __
611
612(** val printing_pass_independent_params_inv_rect_Type3 :
613    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
614    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
615    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
616    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
617    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
618    __ -> 'a2) -> 'a2 **)
619let printing_pass_independent_params_inv_rect_Type3 hterm h1 =
620  let hcut = printing_pass_independent_params_rect_Type3 h1 hterm in hcut __
621
622(** val printing_pass_independent_params_inv_rect_Type2 :
623    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
624    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
625    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
626    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
627    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
628    __ -> 'a2) -> 'a2 **)
629let printing_pass_independent_params_inv_rect_Type2 hterm h1 =
630  let hcut = printing_pass_independent_params_rect_Type2 h1 hterm in hcut __
631
632(** val printing_pass_independent_params_inv_rect_Type1 :
633    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
634    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
635    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
636    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
637    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
638    __ -> 'a2) -> 'a2 **)
639let printing_pass_independent_params_inv_rect_Type1 hterm h1 =
640  let hcut = printing_pass_independent_params_rect_Type1 h1 hterm in hcut __
641
642(** val printing_pass_independent_params_inv_rect_Type0 :
643    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
644    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
645    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
646    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
647    -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) ->
648    __ -> 'a2) -> 'a2 **)
649let printing_pass_independent_params_inv_rect_Type0 hterm h1 =
650  let hcut = printing_pass_independent_params_rect_Type0 h1 hterm in hcut __
651
652(** val printing_pass_independent_params_jmdiscr :
653    'a1 printing_pass_independent_params -> 'a1
654    printing_pass_independent_params -> __ **)
655let printing_pass_independent_params_jmdiscr x y =
656  Logic.eq_rect_Type2 x
657    (let { print_String = a0; print_keyword = a10; print_concat = a2;
658       print_empty = a3; print_ident = a4; print_costlabel = a5;
659       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 = a9;
660       print_nat = a100; print_bitvector = a11 } = x
661     in
662    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
663
664type 'string printing_params = { print_pass_ind : 'string
665                                                  printing_pass_independent_params;
666                                 print_acc_a_reg : (__ -> 'string);
667                                 print_acc_b_reg : (__ -> 'string);
668                                 print_acc_a_arg : (__ -> 'string);
669                                 print_acc_b_arg : (__ -> 'string);
670                                 print_dpl_reg : (__ -> 'string);
671                                 print_dph_reg : (__ -> 'string);
672                                 print_dpl_arg : (__ -> 'string);
673                                 print_dph_arg : (__ -> 'string);
674                                 print_snd_arg : (__ -> 'string);
675                                 print_pair_move : (__ -> 'string);
676                                 print_call_args : (__ -> 'string);
677                                 print_call_dest : (__ -> 'string);
678                                 print_ext_seq : (__ -> 'string) }
679
680(** val printing_params_rect_Type4 :
681    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
682    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
683    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
684    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
685    printing_params -> 'a2 **)
686let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
687  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
688    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
689    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
690    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
691    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
692    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
693    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
694    x_25544
695  in
696  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
697    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
698    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
699    print_call_args0 print_call_dest0 print_ext_seq0
700
701(** val printing_params_rect_Type5 :
702    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
703    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
704    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
705    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
706    printing_params -> 'a2 **)
707let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
708  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
709    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
710    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
711    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
712    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
713    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
714    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
715    x_25546
716  in
717  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
718    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
719    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
720    print_call_args0 print_call_dest0 print_ext_seq0
721
722(** val printing_params_rect_Type3 :
723    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
724    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
725    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
726    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
727    printing_params -> 'a2 **)
728let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
729  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
730    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
731    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
732    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
733    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
734    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
735    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
736    x_25548
737  in
738  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
739    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
740    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
741    print_call_args0 print_call_dest0 print_ext_seq0
742
743(** val printing_params_rect_Type2 :
744    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
745    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
746    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
747    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
748    printing_params -> 'a2 **)
749let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
750  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
751    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
752    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
753    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
754    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
755    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
756    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
757    x_25550
758  in
759  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
760    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
761    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
762    print_call_args0 print_call_dest0 print_ext_seq0
763
764(** val printing_params_rect_Type1 :
765    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
766    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
767    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
768    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
769    printing_params -> 'a2 **)
770let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
771  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
772    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
773    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
774    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
775    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
776    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
777    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
778    x_25552
779  in
780  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
781    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
782    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
783    print_call_args0 print_call_dest0 print_ext_seq0
784
785(** val printing_params_rect_Type0 :
786    Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
787    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
788    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
789    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
790    printing_params -> 'a2 **)
791let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
792  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
793    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
794    print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
795    print_dph_reg = print_dph_reg0; print_dpl_arg = print_dpl_arg0;
796    print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
797    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
798    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
799    x_25554
800  in
801  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
802    print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
803    print_dpl_arg0 print_dph_arg0 print_snd_arg0 print_pair_move0
804    print_call_args0 print_call_dest0 print_ext_seq0
805
806(** val print_pass_ind :
807    Joint.unserialized_params -> 'a1 printing_params -> 'a1
808    printing_pass_independent_params **)
809let rec print_pass_ind p xxx =
810  xxx.print_pass_ind
811
812(** val print_acc_a_reg :
813    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
814let rec print_acc_a_reg p xxx =
815  xxx.print_acc_a_reg
816
817(** val print_acc_b_reg :
818    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
819let rec print_acc_b_reg p xxx =
820  xxx.print_acc_b_reg
821
822(** val print_acc_a_arg :
823    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
824let rec print_acc_a_arg p xxx =
825  xxx.print_acc_a_arg
826
827(** val print_acc_b_arg :
828    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
829let rec print_acc_b_arg p xxx =
830  xxx.print_acc_b_arg
831
832(** val print_dpl_reg :
833    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
834let rec print_dpl_reg p xxx =
835  xxx.print_dpl_reg
836
837(** val print_dph_reg :
838    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
839let rec print_dph_reg p xxx =
840  xxx.print_dph_reg
841
842(** val print_dpl_arg :
843    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
844let rec print_dpl_arg p xxx =
845  xxx.print_dpl_arg
846
847(** val print_dph_arg :
848    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
849let rec print_dph_arg p xxx =
850  xxx.print_dph_arg
851
852(** val print_snd_arg :
853    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
854let rec print_snd_arg p xxx =
855  xxx.print_snd_arg
856
857(** val print_pair_move :
858    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
859let rec print_pair_move p xxx =
860  xxx.print_pair_move
861
862(** val print_call_args :
863    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
864let rec print_call_args p xxx =
865  xxx.print_call_args
866
867(** val print_call_dest :
868    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
869let rec print_call_dest p xxx =
870  xxx.print_call_dest
871
872(** val print_ext_seq :
873    Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1 **)
874let rec print_ext_seq p xxx =
875  xxx.print_ext_seq
876
877(** val printing_params_inv_rect_Type4 :
878    Joint.unserialized_params -> 'a1 printing_params -> ('a1
879    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
880    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
881    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
882    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
883let printing_params_inv_rect_Type4 x2 hterm h1 =
884  let hcut = printing_params_rect_Type4 x2 h1 hterm in hcut __
885
886(** val printing_params_inv_rect_Type3 :
887    Joint.unserialized_params -> 'a1 printing_params -> ('a1
888    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
889    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
890    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
891    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
892let printing_params_inv_rect_Type3 x2 hterm h1 =
893  let hcut = printing_params_rect_Type3 x2 h1 hterm in hcut __
894
895(** val printing_params_inv_rect_Type2 :
896    Joint.unserialized_params -> 'a1 printing_params -> ('a1
897    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
898    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
899    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
900    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
901let printing_params_inv_rect_Type2 x2 hterm h1 =
902  let hcut = printing_params_rect_Type2 x2 h1 hterm in hcut __
903
904(** val printing_params_inv_rect_Type1 :
905    Joint.unserialized_params -> 'a1 printing_params -> ('a1
906    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
907    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
908    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
909    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
910let printing_params_inv_rect_Type1 x2 hterm h1 =
911  let hcut = printing_params_rect_Type1 x2 h1 hterm in hcut __
912
913(** val printing_params_inv_rect_Type0 :
914    Joint.unserialized_params -> 'a1 printing_params -> ('a1
915    printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
916    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
917    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
918    (__ -> 'a1) -> __ -> 'a2) -> 'a2 **)
919let printing_params_inv_rect_Type0 x2 hterm h1 =
920  let hcut = printing_params_rect_Type0 x2 h1 hterm in hcut __
921
922(** val printing_params_jmdiscr :
923    Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params
924    -> __ **)
925let printing_params_jmdiscr a2 x y =
926  Logic.eq_rect_Type2 x
927    (let { print_pass_ind = a0; print_acc_a_reg = a10; print_acc_b_reg = a20;
928       print_acc_a_arg = a3; print_acc_b_arg = a4; print_dpl_reg = a5;
929       print_dph_reg = a6; print_dpl_arg = a7; print_dph_arg = a8;
930       print_snd_arg = a9; print_pair_move = a100; print_call_args = a11;
931       print_call_dest = a12; print_ext_seq = a13 } = x
932     in
933    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
934
935(** val dpi1__o__print_pass_ind__o__inject :
936    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
937    'a1 printing_pass_independent_params Types.sig0 **)
938let dpi1__o__print_pass_ind__o__inject x1 x4 =
939  x4.Types.dpi1.print_pass_ind
940
941(** val eject__o__print_pass_ind__o__inject :
942    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
943    printing_pass_independent_params Types.sig0 **)
944let eject__o__print_pass_ind__o__inject x1 x4 =
945  (Types.pi1 x4).print_pass_ind
946
947(** val print_pass_ind__o__inject :
948    Joint.unserialized_params -> 'a1 printing_params -> 'a1
949    printing_pass_independent_params Types.sig0 **)
950let print_pass_ind__o__inject x1 x3 =
951  x3.print_pass_ind
952
953(** val dpi1__o__print_pass_ind :
954    Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair ->
955    'a1 printing_pass_independent_params **)
956let dpi1__o__print_pass_ind x1 x3 =
957  x3.Types.dpi1.print_pass_ind
958
959(** val eject__o__print_pass_ind :
960    Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
961    printing_pass_independent_params **)
962let eject__o__print_pass_ind x1 x3 =
963  (Types.pi1 x3).print_pass_ind
964
965type 'string print_serialization_params = { print_succ : (__ -> 'string);
966                                            print_code_point : (__ ->
967                                                               'string) }
968
969(** val print_serialization_params_rect_Type4 :
970    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
971    print_serialization_params -> 'a2 **)
972let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
973  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
974    x_25583
975  in
976  h_mk_print_serialization_params print_succ0 print_code_point0
977
978(** val print_serialization_params_rect_Type5 :
979    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
980    print_serialization_params -> 'a2 **)
981let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
982  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
983    x_25585
984  in
985  h_mk_print_serialization_params print_succ0 print_code_point0
986
987(** val print_serialization_params_rect_Type3 :
988    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
989    print_serialization_params -> 'a2 **)
990let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
991  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
992    x_25587
993  in
994  h_mk_print_serialization_params print_succ0 print_code_point0
995
996(** val print_serialization_params_rect_Type2 :
997    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
998    print_serialization_params -> 'a2 **)
999let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
1000  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1001    x_25589
1002  in
1003  h_mk_print_serialization_params print_succ0 print_code_point0
1004
1005(** val print_serialization_params_rect_Type1 :
1006    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1007    print_serialization_params -> 'a2 **)
1008let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
1009  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1010    x_25591
1011  in
1012  h_mk_print_serialization_params print_succ0 print_code_point0
1013
1014(** val print_serialization_params_rect_Type0 :
1015    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
1016    print_serialization_params -> 'a2 **)
1017let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
1018  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
1019    x_25593
1020  in
1021  h_mk_print_serialization_params print_succ0 print_code_point0
1022
1023(** val print_succ :
1024    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1025let rec print_succ p xxx =
1026  xxx.print_succ
1027
1028(** val print_code_point :
1029    Joint.params -> 'a1 print_serialization_params -> __ -> 'a1 **)
1030let rec print_code_point p xxx =
1031  xxx.print_code_point
1032
1033(** val print_serialization_params_inv_rect_Type4 :
1034    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1035    'a1) -> __ -> 'a2) -> 'a2 **)
1036let print_serialization_params_inv_rect_Type4 x2 hterm h1 =
1037  let hcut = print_serialization_params_rect_Type4 x2 h1 hterm in hcut __
1038
1039(** val print_serialization_params_inv_rect_Type3 :
1040    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1041    'a1) -> __ -> 'a2) -> 'a2 **)
1042let print_serialization_params_inv_rect_Type3 x2 hterm h1 =
1043  let hcut = print_serialization_params_rect_Type3 x2 h1 hterm in hcut __
1044
1045(** val print_serialization_params_inv_rect_Type2 :
1046    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1047    'a1) -> __ -> 'a2) -> 'a2 **)
1048let print_serialization_params_inv_rect_Type2 x2 hterm h1 =
1049  let hcut = print_serialization_params_rect_Type2 x2 h1 hterm in hcut __
1050
1051(** val print_serialization_params_inv_rect_Type1 :
1052    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1053    'a1) -> __ -> 'a2) -> 'a2 **)
1054let print_serialization_params_inv_rect_Type1 x2 hterm h1 =
1055  let hcut = print_serialization_params_rect_Type1 x2 h1 hterm in hcut __
1056
1057(** val print_serialization_params_inv_rect_Type0 :
1058    Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
1059    'a1) -> __ -> 'a2) -> 'a2 **)
1060let print_serialization_params_inv_rect_Type0 x2 hterm h1 =
1061  let hcut = print_serialization_params_rect_Type0 x2 h1 hterm in hcut __
1062
1063(** val print_serialization_params_discr :
1064    Joint.params -> 'a1 print_serialization_params -> 'a1
1065    print_serialization_params -> __ **)
1066let print_serialization_params_discr a2 x y =
1067  Logic.eq_rect_Type2 x
1068    (let { print_succ = a0; print_code_point = a10 } = x in
1069    Obj.magic (fun _ dH -> dH __ __)) y
1070
1071(** val print_serialization_params_jmdiscr :
1072    Joint.params -> 'a1 print_serialization_params -> 'a1
1073    print_serialization_params -> __ **)
1074let print_serialization_params_jmdiscr a2 x y =
1075  Logic.eq_rect_Type2 x
1076    (let { print_succ = a0; print_code_point = a10 } = x in
1077    Obj.magic (fun _ dH -> dH __ __)) y
1078
1079type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params : 
1080                                                      'string
1081                                                      print_serialization_params;
1082                                                      fold_code : (__ -> (__
1083                                                                  ->
1084                                                                  'statementT
1085                                                                  -> __ ->
1086                                                                  __) -> __
1087                                                                  -> __ -> __
1088                                                                  -> __);
1089                                                      print_statementT : 
1090                                                      ('statementT ->
1091                                                      'string) }
1092
1093(** val code_iteration_params_rect_Type4 :
1094    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1095    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1096    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1097let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
1098  let { cip_print_serialization_params = cip_print_serialization_params0;
1099    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
1100  in
1101  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1102    print_statementT0
1103
1104(** val code_iteration_params_rect_Type5 :
1105    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1106    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1107    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1108let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
1109  let { cip_print_serialization_params = cip_print_serialization_params0;
1110    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
1111  in
1112  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1113    print_statementT0
1114
1115(** val code_iteration_params_rect_Type3 :
1116    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1117    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1118    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1119let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
1120  let { cip_print_serialization_params = cip_print_serialization_params0;
1121    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
1122  in
1123  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1124    print_statementT0
1125
1126(** val code_iteration_params_rect_Type2 :
1127    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1128    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1129    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1130let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
1131  let { cip_print_serialization_params = cip_print_serialization_params0;
1132    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
1133  in
1134  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1135    print_statementT0
1136
1137(** val code_iteration_params_rect_Type1 :
1138    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1139    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1140    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1141let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
1142  let { cip_print_serialization_params = cip_print_serialization_params0;
1143    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
1144  in
1145  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1146    print_statementT0
1147
1148(** val code_iteration_params_rect_Type0 :
1149    Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
1150    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
1151    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
1152let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
1153  let { cip_print_serialization_params = cip_print_serialization_params0;
1154    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
1155  in
1156  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
1157    print_statementT0
1158
1159(** val cip_print_serialization_params :
1160    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1161    -> 'a1 print_serialization_params **)
1162let rec cip_print_serialization_params p globals xxx =
1163  xxx.cip_print_serialization_params
1164
1165(** val fold_code0 :
1166    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1167    -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
1168let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
1169  (let { cip_print_serialization_params = x; fold_code = yyy;
1170     print_statementT = x0 } = xxx
1171   in
1172  Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639
1173
1174(** val print_statementT :
1175    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1176    -> 'a2 -> 'a1 **)
1177let rec print_statementT p globals xxx =
1178  xxx.print_statementT
1179
1180(** val code_iteration_params_inv_rect_Type4 :
1181    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1182    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1183    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1184let code_iteration_params_inv_rect_Type4 x2 x4 hterm h1 =
1185  let hcut = code_iteration_params_rect_Type4 x2 x4 h1 hterm in hcut __
1186
1187(** val code_iteration_params_inv_rect_Type3 :
1188    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1189    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1190    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1191let code_iteration_params_inv_rect_Type3 x2 x4 hterm h1 =
1192  let hcut = code_iteration_params_rect_Type3 x2 x4 h1 hterm in hcut __
1193
1194(** val code_iteration_params_inv_rect_Type2 :
1195    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1196    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1197    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1198let code_iteration_params_inv_rect_Type2 x2 x4 hterm h1 =
1199  let hcut = code_iteration_params_rect_Type2 x2 x4 h1 hterm in hcut __
1200
1201(** val code_iteration_params_inv_rect_Type1 :
1202    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1203    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1204    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1205let code_iteration_params_inv_rect_Type1 x2 x4 hterm h1 =
1206  let hcut = code_iteration_params_rect_Type1 x2 x4 h1 hterm in hcut __
1207
1208(** val code_iteration_params_inv_rect_Type0 :
1209    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1210    -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) ->
1211    __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3 **)
1212let code_iteration_params_inv_rect_Type0 x2 x4 hterm h1 =
1213  let hcut = code_iteration_params_rect_Type0 x2 x4 h1 hterm in hcut __
1214
1215(** val code_iteration_params_jmdiscr :
1216    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
1217    -> ('a1, 'a2) code_iteration_params -> __ **)
1218let code_iteration_params_jmdiscr a2 a4 x y =
1219  Logic.eq_rect_Type2 x
1220    (let { cip_print_serialization_params = a0; fold_code = a10;
1221       print_statementT = a20 } = x
1222     in
1223    Obj.magic (fun _ dH -> dH __ __ __)) y
1224
1225(** val pm_choose_with_pref :
1226    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
1227    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
1228    Types.option **)
1229let pm_choose_with_pref m = function
1230| Types.None -> PositiveMap.pm_choose m
1231| Types.Some p ->
1232  (match PositiveMap.pm_try_remove p m with
1233   | Types.None -> PositiveMap.pm_choose m
1234   | Types.Some res ->
1235     let { Types.fst = a; Types.snd = m' } = res in
1236     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
1237     m' })
1238
1239(** val visit_graph :
1240    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
1241    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
1242    Nat.nat -> 'a2 **)
1243let rec visit_graph next f b n m = function
1244| Nat.O -> b
1245| Nat.S y ->
1246  (match pm_choose_with_pref m n with
1247   | Types.None -> b
1248   | Types.Some res ->
1249     let { Types.fst = eta32074; Types.snd = m' } = res in
1250     let { Types.fst = pos; Types.snd = a } = eta32074 in
1251     visit_graph next f (f pos a b) (next a) m' y)
1252
1253(** val print_list :
1254    'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1 **)
1255let print_list pp =
1256  List.foldr pp.print_concat pp.print_empty
1257
1258(** val print_joint_seq :
1259    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1260    -> Joint.joint_seq -> 'a1 **)
1261let print_joint_seq p globals pp = function
1262| Joint.COMMENT str ->
1263  print_list pp.print_pass_ind (List.Cons
1264    ((pp.print_pass_ind.print_keyword KwCOMMENT), (List.Cons
1265    ((pp.print_pass_ind.print_String str), List.Nil))))
1266| Joint.MOVE pm ->
1267  print_list pp.print_pass_ind (List.Cons
1268    ((pp.print_pass_ind.print_keyword KwMOVE), (List.Cons
1269    ((pp.print_pair_move pm), List.Nil))))
1270| Joint.POP arg ->
1271  print_list pp.print_pass_ind (List.Cons
1272    ((pp.print_pass_ind.print_keyword KwPOP), (List.Cons
1273    ((pp.print_acc_a_reg arg), List.Nil))))
1274| Joint.PUSH arg ->
1275  print_list pp.print_pass_ind (List.Cons
1276    ((pp.print_pass_ind.print_keyword KwPUSH), (List.Cons
1277    ((pp.print_acc_a_arg arg), List.Nil))))
1278| Joint.ADDRESS (i, offset, arg1, arg2) ->
1279  print_list pp.print_pass_ind (List.Cons
1280    ((pp.print_pass_ind.print_keyword KwADDRESS), (List.Cons
1281    ((pp.print_pass_ind.print_ident i), (List.Cons
1282    ((pp.print_pass_ind.print_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1284       (Nat.S Nat.O)))))))))))))))) offset), (List.Cons
1285    ((pp.print_dpl_reg arg1), (List.Cons ((pp.print_dph_reg arg2),
1286    List.Nil))))))))))
1287| Joint.OPACCS (opa, arg1, arg2, arg3, arg4) ->
1288  print_list pp.print_pass_ind (List.Cons
1289    ((pp.print_pass_ind.print_keyword KwOPACCS), (List.Cons
1290    ((pp.print_pass_ind.print_OpAccs opa), (List.Cons
1291    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_b_reg arg2),
1292    (List.Cons ((pp.print_acc_a_arg arg3), (List.Cons
1293    ((pp.print_acc_b_arg arg4), List.Nil))))))))))))
1294| Joint.OP1 (op1, arg1, arg2) ->
1295  print_list pp.print_pass_ind (List.Cons
1296    ((pp.print_pass_ind.print_keyword KwOP1), (List.Cons
1297    ((pp.print_pass_ind.print_Op1 op1), (List.Cons
1298    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_reg arg2),
1299    List.Nil))))))))
1300| Joint.OP2 (op2, arg1, arg2, arg3) ->
1301  print_list pp.print_pass_ind (List.Cons
1302    ((pp.print_pass_ind.print_keyword KwOP2), (List.Cons
1303    ((pp.print_pass_ind.print_Op2 op2), (List.Cons
1304    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_acc_a_arg arg2),
1305    (List.Cons ((pp.print_snd_arg arg3), List.Nil))))))))))
1306| Joint.CLEAR_CARRY -> pp.print_pass_ind.print_keyword KwCLEAR_CARRY
1307| Joint.SET_CARRY -> pp.print_pass_ind.print_keyword KwSET_CARRY
1308| Joint.LOAD (arg1, arg2, arg3) ->
1309  print_list pp.print_pass_ind (List.Cons
1310    ((pp.print_pass_ind.print_keyword KwLOAD), (List.Cons
1311    ((pp.print_acc_a_reg arg1), (List.Cons ((pp.print_dpl_arg arg2),
1312    (List.Cons ((pp.print_dph_arg arg3), List.Nil))))))))
1313| Joint.STORE (arg1, arg2, arg3) ->
1314  print_list pp.print_pass_ind (List.Cons
1315    ((pp.print_pass_ind.print_keyword KwSTORE), (List.Cons
1316    ((pp.print_dpl_arg arg1), (List.Cons ((pp.print_dph_arg arg2), (List.Cons
1317    ((pp.print_acc_a_arg arg3), List.Nil))))))))
1318| Joint.Extension_seq ext -> pp.print_ext_seq ext
1319
1320(** val print_joint_step :
1321    Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params
1322    -> Joint.joint_step -> 'a1 **)
1323let print_joint_step p globals pp = function
1324| Joint.COST_LABEL arg ->
1325  print_list pp.print_pass_ind (List.Cons
1326    ((pp.print_pass_ind.print_keyword KwCOST_LABEL), (List.Cons
1327    ((pp.print_pass_ind.print_costlabel arg), List.Nil))))
1328| Joint.CALL (arg1, arg2, arg3) ->
1329  print_list pp.print_pass_ind (List.Cons
1330    ((pp.print_pass_ind.print_keyword KwCALL), (List.Cons
1331    ((match arg1 with
1332      | Types.Inl id -> pp.print_pass_ind.print_ident id
1333      | Types.Inr arg11_arg12 ->
1334        pp.print_pass_ind.print_concat
1335          (pp.print_dpl_arg arg11_arg12.Types.fst)
1336          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1337    ((pp.print_call_args arg2), (List.Cons ((pp.print_call_dest arg3),
1338    List.Nil))))))))
1339| Joint.COND (arg1, arg2) ->
1340  print_list pp.print_pass_ind (List.Cons
1341    ((pp.print_pass_ind.print_keyword KwCOND), (List.Cons
1342    ((pp.print_acc_a_reg arg1), (List.Cons
1343    ((pp.print_pass_ind.print_label arg2), List.Nil))))))
1344| Joint.Step_seq seq -> print_joint_seq p globals pp seq
1345
1346(** val print_joint_fin_step :
1347    Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step
1348    -> 'a1 **)
1349let print_joint_fin_step p pp = function
1350| Joint.GOTO l ->
1351  print_list pp.print_pass_ind (List.Cons
1352    ((pp.print_pass_ind.print_keyword KwGOTO), (List.Cons
1353    ((pp.print_pass_ind.print_label l), List.Nil))))
1354| Joint.RETURN -> pp.print_pass_ind.print_keyword KwRETURN
1355| Joint.TAILCALL (arg1, arg2) ->
1356  print_list pp.print_pass_ind (List.Cons
1357    ((pp.print_pass_ind.print_keyword KwTAILCALL), (List.Cons
1358    ((match arg1 with
1359      | Types.Inl id -> pp.print_pass_ind.print_ident id
1360      | Types.Inr arg11_arg12 ->
1361        pp.print_pass_ind.print_concat
1362          (pp.print_dpl_arg arg11_arg12.Types.fst)
1363          (pp.print_dph_arg arg11_arg12.Types.snd)), (List.Cons
1364    ((pp.print_call_args arg2), List.Nil))))))
1365
1366(** val print_joint_statement :
1367    Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
1368    print_serialization_params -> Joint.joint_statement -> 'a1 **)
1369let print_joint_statement p globals pp cip = function
1370| Joint.Sequential (js, arg1) ->
1371  pp.print_pass_ind.print_concat
1372    (print_joint_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) globals pp
1373      js) (cip.print_succ arg1)
1374| Joint.Final fin ->
1375  print_joint_fin_step (Joint.stmt_pars__o__uns_pars__o__u_pars p) pp fin
1376| Joint.FCOND (arg1, arg2, arg3) ->
1377  print_list pp.print_pass_ind (List.Cons
1378    ((pp.print_pass_ind.print_keyword KwFCOND), (List.Cons
1379    ((pp.print_acc_a_reg arg1), (List.Cons
1380    ((pp.print_pass_ind.print_label arg2), (List.Cons
1381    ((pp.print_pass_ind.print_label arg3), List.Nil))))))))
1382
1383(** val graph_print_serialization_params :
1384    Joint.graph_params -> 'a1 printing_params -> 'a1
1385    print_serialization_params **)
1386let graph_print_serialization_params gp pp =
1387  { print_succ = (Obj.magic pp.print_pass_ind.print_label);
1388    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
1389
1390(** val graph_code_iteration_params :
1391    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1392    Joint.joint_statement) code_iteration_params **)
1393let graph_code_iteration_params gp globals pp =
1394  { cip_print_serialization_params =
1395    (graph_print_serialization_params gp pp); fold_code =
1396    (fun _ f m initl a ->
1397    visit_graph (fun stmt ->
1398      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
1399              globals stmt with
1400      | Types.None -> Types.None
1401      | Types.Some label -> let p = label in Types.Some p) (fun n ->
1402      Obj.magic f n) a (Types.Some
1403      (Identifiers.word_of_identifier PreIdentifiers.LabelTag
1404        (Obj.magic initl))) (let m' = Obj.magic m in m')
1405      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
1406    print_statementT =
1407    (print_joint_statement (Joint.graph_params_to_params gp) globals pp
1408      (graph_print_serialization_params gp pp)) }
1409
1410(** val lin_print_serialization_params :
1411    Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params **)
1412let lin_print_serialization_params gp pp =
1413  { print_succ = (fun x -> pp.print_pass_ind.print_empty); print_code_point =
1414    (Obj.magic pp.print_pass_ind.print_nat) }
1415
1416(** val lin_code_iteration_params :
1417    Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
1418    (Graphs.label Types.option, Joint.joint_statement) Types.prod)
1419    code_iteration_params **)
1420let lin_code_iteration_params lp globals pp =
1421  { cip_print_serialization_params = (lin_print_serialization_params lp pp);
1422    fold_code = (fun _ f m x a ->
1423    (Util.foldl (fun res x0 ->
1424      let { Types.fst = pc; Types.snd = res' } = res in
1425      { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x0 res') })
1426      { Types.fst = Nat.O; Types.snd = a } (Obj.magic m)).Types.snd);
1427    print_statementT = (fun linstr ->
1428    match linstr.Types.fst with
1429    | Types.None ->
1430      print_joint_statement (Joint.lin_params_to_params lp) globals pp
1431        (lin_print_serialization_params lp pp) linstr.Types.snd
1432    | Types.Some l ->
1433      print_list pp.print_pass_ind (List.Cons
1434        ((pp.print_pass_ind.print_label l), (List.Cons
1435        ((print_joint_statement (Joint.lin_params_to_params lp) globals pp
1436           (lin_print_serialization_params lp pp) linstr.Types.snd),
1437        List.Nil))))) }
1438
1439(** val print_joint_internal_function :
1440    Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params
1441    -> 'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list **)
1442let print_joint_internal_function p globals cip pp f =
1443  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
1444    ((print_list pp.print_pass_ind (List.Cons
1445       ((cip.cip_print_serialization_params.print_code_point cp), (List.Cons
1446       ((cip.print_statementT stmt), List.Nil))))), acc))
1447    f.Joint.joint_if_code f.Joint.joint_if_entry List.Nil
1448
1449(** val print_joint_function :
1450    Joint.params -> AST.ident List.list -> AST.ident List.list -> ('a2, 'a1)
1451    code_iteration_params -> 'a2 printing_params -> Joint.joint_function ->
1452    'a2 List.list **)
1453let print_joint_function p globals functions cip pp = function
1454| AST.Internal f0 ->
1455  print_joint_internal_function p (List.append globals functions) cip pp
1456    (Types.pi1 f0)
1457| AST.External f0 -> List.Nil
1458
1459(** val print_joint_program :
1460    Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
1461    code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list **)
1462let print_joint_program p pp prog cip =
1463  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
1464    (print_joint_function p (AST.prog_var_names prog.Joint.joint_prog)
1465      prog.Joint.jp_functions cip pp f.Types.snd) }, acc)) List.Nil
1466    prog.Joint.joint_prog.AST.prog_funct
1467
Note: See TracBrowser for help on using the repository browser.