source: extracted/joint_printer.mli @ 2951

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

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

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)
File size: 21.9 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
142val 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
145
146val keyword_rect_Type5 :
147  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
148  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
149
150val keyword_rect_Type3 :
151  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
152  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
153
154val keyword_rect_Type2 :
155  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
156  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
157
158val keyword_rect_Type1 :
159  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
160  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
161
162val keyword_rect_Type0 :
163  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
164  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> keyword -> 'a1
165
166val keyword_inv_rect_Type4 :
167  keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
168  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
169  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
170  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
171
172val keyword_inv_rect_Type3 :
173  keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
174  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
175  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
176  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
177
178val keyword_inv_rect_Type2 :
179  keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
180  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
181  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
182  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
183
184val keyword_inv_rect_Type1 :
185  keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
186  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
187  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
188  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
189
190val keyword_inv_rect_Type0 :
191  keyword -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
192  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
193  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
194  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
195
196val keyword_discr : keyword -> keyword -> __
197
198val keyword_jmdiscr : keyword -> keyword -> __
199
200type 'string printing_pass_independent_params = { print_String : (String.string
201                                                                 -> 'string);
202                                                  print_keyword : (keyword ->
203                                                                  'string);
204                                                  print_concat : ('string ->
205                                                                 'string ->
206                                                                 'string);
207                                                  print_empty : 'string;
208                                                  print_ident : (AST.ident ->
209                                                                'string);
210                                                  print_costlabel : (CostLabel.costlabel
211                                                                    ->
212                                                                    'string);
213                                                  print_label : (Graphs.label
214                                                                -> 'string);
215                                                  print_OpAccs : (BackEndOps.opAccs
216                                                                 -> 'string);
217                                                  print_Op1 : (BackEndOps.op1
218                                                              -> 'string);
219                                                  print_Op2 : (BackEndOps.op2
220                                                              -> 'string) }
221
222val printing_pass_independent_params_rect_Type4 :
223  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
224  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
225  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
226  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
227  'a2
228
229val printing_pass_independent_params_rect_Type5 :
230  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
231  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
232  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
233  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
234  'a2
235
236val printing_pass_independent_params_rect_Type3 :
237  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
238  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
239  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
240  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
241  'a2
242
243val printing_pass_independent_params_rect_Type2 :
244  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
245  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
246  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
247  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
248  'a2
249
250val printing_pass_independent_params_rect_Type1 :
251  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
252  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
253  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
254  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
255  'a2
256
257val printing_pass_independent_params_rect_Type0 :
258  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
259  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
260  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
261  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
262  'a2
263
264val print_String :
265  'a1 printing_pass_independent_params -> String.string -> 'a1
266
267val print_keyword : 'a1 printing_pass_independent_params -> keyword -> 'a1
268
269val print_concat : 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1
270
271val print_empty : 'a1 printing_pass_independent_params -> 'a1
272
273val print_ident : 'a1 printing_pass_independent_params -> AST.ident -> 'a1
274
275val print_costlabel :
276  'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1
277
278val print_label : 'a1 printing_pass_independent_params -> Graphs.label -> 'a1
279
280val print_OpAccs :
281  'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1
282
283val print_Op1 : 'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1
284
285val print_Op2 : 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1
286
287val printing_pass_independent_params_inv_rect_Type4 :
288  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
289  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
290  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
291  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
292  -> 'a2
293
294val printing_pass_independent_params_inv_rect_Type3 :
295  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
296  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
297  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
298  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
299  -> 'a2
300
301val printing_pass_independent_params_inv_rect_Type2 :
302  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
303  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
304  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
305  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
306  -> 'a2
307
308val printing_pass_independent_params_inv_rect_Type1 :
309  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
310  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
311  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
312  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
313  -> 'a2
314
315val printing_pass_independent_params_inv_rect_Type0 :
316  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
317  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
318  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
319  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
320  -> 'a2
321
322val printing_pass_independent_params_jmdiscr :
323  'a1 printing_pass_independent_params -> 'a1
324  printing_pass_independent_params -> __
325
326type 'string printing_params = { print_pass_ind : 'string
327                                                  printing_pass_independent_params;
328                                 print_acc_a_reg : (__ -> 'string);
329                                 print_acc_b_reg : (__ -> 'string);
330                                 print_acc_a_arg : (__ -> 'string);
331                                 print_acc_b_arg : (__ -> 'string);
332                                 print_dpl_reg : (__ -> 'string);
333                                 print_dph_reg : (__ -> 'string);
334                                 print_dpl_arg : (__ -> 'string);
335                                 print_dph_arg : (__ -> 'string);
336                                 print_snd_arg : (__ -> 'string);
337                                 print_pair_move : (__ -> 'string);
338                                 print_call_args : (__ -> 'string);
339                                 print_call_dest : (__ -> 'string);
340                                 print_ext_seq : (__ -> 'string) }
341
342val printing_params_rect_Type4 :
343  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
344  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
345  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
346  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
347
348val printing_params_rect_Type5 :
349  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
350  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
351  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
352  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
353
354val printing_params_rect_Type3 :
355  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
356  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
357  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
358  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
359
360val printing_params_rect_Type2 :
361  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
362  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
363  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
364  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
365
366val printing_params_rect_Type1 :
367  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
368  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
369  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
370  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
371
372val printing_params_rect_Type0 :
373  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
374  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
375  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
376  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
377
378val print_pass_ind :
379  Joint.unserialized_params -> 'a1 printing_params -> 'a1
380  printing_pass_independent_params
381
382val print_acc_a_reg :
383  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
384
385val print_acc_b_reg :
386  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
387
388val print_acc_a_arg :
389  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
390
391val print_acc_b_arg :
392  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
393
394val print_dpl_reg :
395  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
396
397val print_dph_reg :
398  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
399
400val print_dpl_arg :
401  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
402
403val print_dph_arg :
404  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
405
406val print_snd_arg :
407  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
408
409val print_pair_move :
410  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
411
412val print_call_args :
413  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
414
415val print_call_dest :
416  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
417
418val print_ext_seq :
419  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
420
421val printing_params_inv_rect_Type4 :
422  Joint.unserialized_params -> 'a1 printing_params -> ('a1
423  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
424  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
425  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
426  'a1) -> __ -> 'a2) -> 'a2
427
428val printing_params_inv_rect_Type3 :
429  Joint.unserialized_params -> 'a1 printing_params -> ('a1
430  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
431  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
432  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
433  'a1) -> __ -> 'a2) -> 'a2
434
435val printing_params_inv_rect_Type2 :
436  Joint.unserialized_params -> 'a1 printing_params -> ('a1
437  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
438  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
439  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
440  'a1) -> __ -> 'a2) -> 'a2
441
442val printing_params_inv_rect_Type1 :
443  Joint.unserialized_params -> 'a1 printing_params -> ('a1
444  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
445  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
446  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
447  'a1) -> __ -> 'a2) -> 'a2
448
449val printing_params_inv_rect_Type0 :
450  Joint.unserialized_params -> 'a1 printing_params -> ('a1
451  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
452  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
453  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
454  'a1) -> __ -> 'a2) -> 'a2
455
456val printing_params_jmdiscr :
457  Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params ->
458  __
459
460val dpi1__o__print_pass_ind__o__inject :
461  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
462  printing_pass_independent_params Types.sig0
463
464val eject__o__print_pass_ind__o__inject :
465  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
466  printing_pass_independent_params Types.sig0
467
468val print_pass_ind__o__inject :
469  Joint.unserialized_params -> 'a1 printing_params -> 'a1
470  printing_pass_independent_params Types.sig0
471
472val dpi1__o__print_pass_ind :
473  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
474  printing_pass_independent_params
475
476val eject__o__print_pass_ind :
477  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
478  printing_pass_independent_params
479
480type 'string code_iteration_params = { fold_code : (__ -> (__ ->
481                                                   Joint.joint_statement ->
482                                                   __ -> __) -> __ -> __ ->
483                                                   __);
484                                       print_succ : (__ -> 'string);
485                                       print_code_point : (__ -> 'string) }
486
487val code_iteration_params_rect_Type4 :
488  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
489  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
490  'a1 code_iteration_params -> 'a2
491
492val code_iteration_params_rect_Type5 :
493  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
494  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
495  'a1 code_iteration_params -> 'a2
496
497val code_iteration_params_rect_Type3 :
498  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
499  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
500  'a1 code_iteration_params -> 'a2
501
502val code_iteration_params_rect_Type2 :
503  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
504  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
505  'a1 code_iteration_params -> 'a2
506
507val code_iteration_params_rect_Type1 :
508  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
509  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
510  'a1 code_iteration_params -> 'a2
511
512val code_iteration_params_rect_Type0 :
513  Joint.params -> AST.ident List.list -> ((__ -> (__ -> Joint.joint_statement
514  -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) ->
515  'a1 code_iteration_params -> 'a2
516
517val fold_code0 :
518  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> (__ ->
519  Joint.joint_statement -> 'a2 -> 'a2) -> __ -> 'a2 -> 'a2
520
521val print_succ :
522  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
523  'a1
524
525val print_code_point :
526  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> __ ->
527  'a1
528
529val code_iteration_params_inv_rect_Type4 :
530  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
531  (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
532  -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
533
534val code_iteration_params_inv_rect_Type3 :
535  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
536  (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
537  -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
538
539val code_iteration_params_inv_rect_Type2 :
540  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
541  (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
542  -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
543
544val code_iteration_params_inv_rect_Type1 :
545  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
546  (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
547  -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
548
549val code_iteration_params_inv_rect_Type0 :
550  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> ((__ ->
551  (__ -> Joint.joint_statement -> __ -> __) -> __ -> __ -> __) -> (__ -> 'a1)
552  -> (__ -> 'a1) -> __ -> 'a2) -> 'a2
553
554val code_iteration_params_jmdiscr :
555  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
556  code_iteration_params -> __
557
558val pm_choose_with_pref :
559  'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
560  ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
561  Types.option
562
563val visit_graph :
564  ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
565  -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
566  Nat.nat -> 'a2
567
568val graph_code_iteration_params :
569  Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
570  code_iteration_params
571
572val print_list : 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1
573
574val print_joint_seq :
575  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
576  Joint.joint_seq -> 'a1
577
578val print_joint_step :
579  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
580  Joint.joint_step -> 'a1
581
582val print_joint_fin_step :
583  Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step ->
584  'a1
585
586val print_joint_statement :
587  Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
588  code_iteration_params -> Joint.joint_statement -> 'a1
589
590val print_joint_internal_function :
591  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
592  printing_params -> Joint.joint_internal_function -> 'a1 List.list
593
594val print_joint_function :
595  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
596  printing_params -> Joint.joint_function -> 'a1 List.list
597
598val print_joint_program :
599  Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
600  code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list
601
Note: See TracBrowser for help on using the repository browser.