source: extracted/joint_printer.mli @ 2982

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

Pretty priting of LIN implemented.

File size: 25.7 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                                                  print_nat : (Nat.nat ->
222                                                              'string) }
223
224val printing_pass_independent_params_rect_Type4 :
225  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
226  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
227  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
228  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
229  printing_pass_independent_params -> 'a2
230
231val printing_pass_independent_params_rect_Type5 :
232  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
233  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
234  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
235  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
236  printing_pass_independent_params -> 'a2
237
238val printing_pass_independent_params_rect_Type3 :
239  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
240  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
241  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
242  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
243  printing_pass_independent_params -> 'a2
244
245val printing_pass_independent_params_rect_Type2 :
246  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
247  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
248  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
249  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
250  printing_pass_independent_params -> 'a2
251
252val printing_pass_independent_params_rect_Type1 :
253  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
254  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
255  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
256  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
257  printing_pass_independent_params -> 'a2
258
259val printing_pass_independent_params_rect_Type0 :
260  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
261  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
262  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
263  (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> 'a2) -> 'a1
264  printing_pass_independent_params -> 'a2
265
266val print_String :
267  'a1 printing_pass_independent_params -> String.string -> 'a1
268
269val print_keyword : 'a1 printing_pass_independent_params -> keyword -> 'a1
270
271val print_concat : 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1
272
273val print_empty : 'a1 printing_pass_independent_params -> 'a1
274
275val print_ident : 'a1 printing_pass_independent_params -> AST.ident -> 'a1
276
277val print_costlabel :
278  'a1 printing_pass_independent_params -> CostLabel.costlabel -> 'a1
279
280val print_label : 'a1 printing_pass_independent_params -> Graphs.label -> 'a1
281
282val print_OpAccs :
283  'a1 printing_pass_independent_params -> BackEndOps.opAccs -> 'a1
284
285val print_Op1 : 'a1 printing_pass_independent_params -> BackEndOps.op1 -> 'a1
286
287val print_Op2 : 'a1 printing_pass_independent_params -> BackEndOps.op2 -> 'a1
288
289val print_nat : 'a1 printing_pass_independent_params -> Nat.nat -> 'a1
290
291val printing_pass_independent_params_inv_rect_Type4 :
292  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
293  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
294  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
295  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
296  -> 'a1) -> __ -> 'a2) -> 'a2
297
298val printing_pass_independent_params_inv_rect_Type3 :
299  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
300  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
301  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
302  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
303  -> 'a1) -> __ -> 'a2) -> 'a2
304
305val printing_pass_independent_params_inv_rect_Type2 :
306  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
307  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
308  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
309  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
310  -> 'a1) -> __ -> 'a2) -> 'a2
311
312val printing_pass_independent_params_inv_rect_Type1 :
313  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
314  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
315  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
316  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
317  -> 'a1) -> __ -> 'a2) -> 'a2
318
319val printing_pass_independent_params_inv_rect_Type0 :
320  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
321  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
322  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
323  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> (Nat.nat
324  -> 'a1) -> __ -> 'a2) -> 'a2
325
326val printing_pass_independent_params_jmdiscr :
327  'a1 printing_pass_independent_params -> 'a1
328  printing_pass_independent_params -> __
329
330type 'string printing_params = { print_pass_ind : 'string
331                                                  printing_pass_independent_params;
332                                 print_acc_a_reg : (__ -> 'string);
333                                 print_acc_b_reg : (__ -> 'string);
334                                 print_acc_a_arg : (__ -> 'string);
335                                 print_acc_b_arg : (__ -> 'string);
336                                 print_dpl_reg : (__ -> 'string);
337                                 print_dph_reg : (__ -> 'string);
338                                 print_dpl_arg : (__ -> 'string);
339                                 print_dph_arg : (__ -> 'string);
340                                 print_snd_arg : (__ -> 'string);
341                                 print_pair_move : (__ -> 'string);
342                                 print_call_args : (__ -> 'string);
343                                 print_call_dest : (__ -> 'string);
344                                 print_ext_seq : (__ -> 'string) }
345
346val printing_params_rect_Type4 :
347  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
348  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
349  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
350  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
351
352val printing_params_rect_Type5 :
353  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
354  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
355  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
356  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
357
358val printing_params_rect_Type3 :
359  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
360  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
361  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
362  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
363
364val printing_params_rect_Type2 :
365  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
366  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
367  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
368  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
369
370val printing_params_rect_Type1 :
371  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
372  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
373  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
374  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
375
376val printing_params_rect_Type0 :
377  Joint.unserialized_params -> ('a1 printing_pass_independent_params -> (__
378  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
379  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
380  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2
381
382val print_pass_ind :
383  Joint.unserialized_params -> 'a1 printing_params -> 'a1
384  printing_pass_independent_params
385
386val print_acc_a_reg :
387  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
388
389val print_acc_b_reg :
390  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
391
392val print_acc_a_arg :
393  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
394
395val print_acc_b_arg :
396  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
397
398val print_dpl_reg :
399  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
400
401val print_dph_reg :
402  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
403
404val print_dpl_arg :
405  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
406
407val print_dph_arg :
408  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
409
410val print_snd_arg :
411  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
412
413val print_pair_move :
414  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
415
416val print_call_args :
417  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
418
419val print_call_dest :
420  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
421
422val print_ext_seq :
423  Joint.unserialized_params -> 'a1 printing_params -> __ -> 'a1
424
425val printing_params_inv_rect_Type4 :
426  Joint.unserialized_params -> 'a1 printing_params -> ('a1
427  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
428  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
429  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
430  'a1) -> __ -> 'a2) -> 'a2
431
432val printing_params_inv_rect_Type3 :
433  Joint.unserialized_params -> 'a1 printing_params -> ('a1
434  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
435  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
436  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
437  'a1) -> __ -> 'a2) -> 'a2
438
439val printing_params_inv_rect_Type2 :
440  Joint.unserialized_params -> 'a1 printing_params -> ('a1
441  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
442  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
443  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
444  'a1) -> __ -> 'a2) -> 'a2
445
446val printing_params_inv_rect_Type1 :
447  Joint.unserialized_params -> 'a1 printing_params -> ('a1
448  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
449  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
450  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
451  'a1) -> __ -> 'a2) -> 'a2
452
453val printing_params_inv_rect_Type0 :
454  Joint.unserialized_params -> 'a1 printing_params -> ('a1
455  printing_pass_independent_params -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
456  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
457  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
458  'a1) -> __ -> 'a2) -> 'a2
459
460val printing_params_jmdiscr :
461  Joint.unserialized_params -> 'a1 printing_params -> 'a1 printing_params ->
462  __
463
464val dpi1__o__print_pass_ind__o__inject :
465  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
466  printing_pass_independent_params Types.sig0
467
468val eject__o__print_pass_ind__o__inject :
469  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
470  printing_pass_independent_params Types.sig0
471
472val print_pass_ind__o__inject :
473  Joint.unserialized_params -> 'a1 printing_params -> 'a1
474  printing_pass_independent_params Types.sig0
475
476val dpi1__o__print_pass_ind :
477  Joint.unserialized_params -> ('a1 printing_params, 'a2) Types.dPair -> 'a1
478  printing_pass_independent_params
479
480val eject__o__print_pass_ind :
481  Joint.unserialized_params -> 'a1 printing_params Types.sig0 -> 'a1
482  printing_pass_independent_params
483
484type 'string print_serialization_params = { print_succ : (__ -> 'string);
485                                            print_code_point : (__ ->
486                                                               'string) }
487
488val print_serialization_params_rect_Type4 :
489  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
490  print_serialization_params -> 'a2
491
492val print_serialization_params_rect_Type5 :
493  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
494  print_serialization_params -> 'a2
495
496val print_serialization_params_rect_Type3 :
497  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
498  print_serialization_params -> 'a2
499
500val print_serialization_params_rect_Type2 :
501  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
502  print_serialization_params -> 'a2
503
504val print_serialization_params_rect_Type1 :
505  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
506  print_serialization_params -> 'a2
507
508val print_serialization_params_rect_Type0 :
509  Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
510  print_serialization_params -> 'a2
511
512val print_succ : Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
513
514val print_code_point :
515  Joint.params -> 'a1 print_serialization_params -> __ -> 'a1
516
517val print_serialization_params_inv_rect_Type4 :
518  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
519  'a1) -> __ -> 'a2) -> 'a2
520
521val print_serialization_params_inv_rect_Type3 :
522  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
523  'a1) -> __ -> 'a2) -> 'a2
524
525val print_serialization_params_inv_rect_Type2 :
526  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
527  'a1) -> __ -> 'a2) -> 'a2
528
529val print_serialization_params_inv_rect_Type1 :
530  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
531  'a1) -> __ -> 'a2) -> 'a2
532
533val print_serialization_params_inv_rect_Type0 :
534  Joint.params -> 'a1 print_serialization_params -> ((__ -> 'a1) -> (__ ->
535  'a1) -> __ -> 'a2) -> 'a2
536
537val print_serialization_params_discr :
538  Joint.params -> 'a1 print_serialization_params -> 'a1
539  print_serialization_params -> __
540
541val print_serialization_params_jmdiscr :
542  Joint.params -> 'a1 print_serialization_params -> 'a1
543  print_serialization_params -> __
544
545type ('string, 'statementT) code_iteration_params = { cip_print_serialization_params : 
546                                                      'string
547                                                      print_serialization_params;
548                                                      fold_code : (__ -> (__
549                                                                  ->
550                                                                  'statementT
551                                                                  -> __ ->
552                                                                  __) -> __
553                                                                  -> __ ->
554                                                                  __);
555                                                      print_statementT : 
556                                                      ('statementT ->
557                                                      'string) }
558
559val code_iteration_params_rect_Type4 :
560  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
561  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
562  -> ('a1, 'a2) code_iteration_params -> 'a3
563
564val code_iteration_params_rect_Type5 :
565  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
566  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
567  -> ('a1, 'a2) code_iteration_params -> 'a3
568
569val code_iteration_params_rect_Type3 :
570  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
571  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
572  -> ('a1, 'a2) code_iteration_params -> 'a3
573
574val code_iteration_params_rect_Type2 :
575  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
576  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
577  -> ('a1, 'a2) code_iteration_params -> 'a3
578
579val code_iteration_params_rect_Type1 :
580  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
581  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
582  -> ('a1, 'a2) code_iteration_params -> 'a3
583
584val code_iteration_params_rect_Type0 :
585  Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
586  (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3)
587  -> ('a1, 'a2) code_iteration_params -> 'a3
588
589val cip_print_serialization_params :
590  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
591  'a1 print_serialization_params
592
593val fold_code0 :
594  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
595  (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> 'a3 -> 'a3
596
597val print_statementT :
598  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
599  'a2 -> 'a1
600
601val code_iteration_params_inv_rect_Type4 :
602  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
603  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
604  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
605
606val code_iteration_params_inv_rect_Type3 :
607  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
608  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
609  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
610
611val code_iteration_params_inv_rect_Type2 :
612  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
613  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
614  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
615
616val code_iteration_params_inv_rect_Type1 :
617  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
618  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
619  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
620
621val code_iteration_params_inv_rect_Type0 :
622  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
623  ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ ->
624  __ -> __) -> ('a2 -> 'a1) -> __ -> 'a3) -> 'a3
625
626val code_iteration_params_jmdiscr :
627  Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params ->
628  ('a1, 'a2) code_iteration_params -> __
629
630val pm_choose_with_pref :
631  'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
632  ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
633  Types.option
634
635val visit_graph :
636  ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
637  -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
638  Nat.nat -> 'a2
639
640val print_list : 'a1 printing_pass_independent_params -> 'a1 List.list -> 'a1
641
642val print_joint_seq :
643  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
644  Joint.joint_seq -> 'a1
645
646val print_joint_step :
647  Joint.unserialized_params -> AST.ident List.list -> 'a1 printing_params ->
648  Joint.joint_step -> 'a1
649
650val print_joint_fin_step :
651  Joint.unserialized_params -> 'a1 printing_params -> Joint.joint_fin_step ->
652  'a1
653
654val print_joint_statement :
655  Joint.params -> AST.ident List.list -> 'a1 printing_params -> 'a1
656  print_serialization_params -> Joint.joint_statement -> 'a1
657
658val graph_print_serialization_params :
659  Joint.graph_params -> 'a1 printing_params -> 'a1 print_serialization_params
660
661val graph_code_iteration_params :
662  Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
663  Joint.joint_statement) code_iteration_params
664
665val lin_print_serialization_params :
666  Joint.lin_params -> 'a1 printing_params -> 'a1 print_serialization_params
667
668val lin_code_iteration_params :
669  Joint.lin_params -> AST.ident List.list -> 'a1 printing_params -> ('a1,
670  (Graphs.label Types.option, Joint.joint_statement) Types.prod)
671  code_iteration_params
672
673val print_joint_internal_function :
674  Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params ->
675  'a2 printing_params -> Joint.joint_internal_function -> 'a2 List.list
676
677val print_joint_function :
678  Joint.params -> AST.ident List.list -> ('a2, 'a1) code_iteration_params ->
679  'a2 printing_params -> Joint.joint_function -> 'a2 List.list
680
681val print_joint_program :
682  Joint.params -> 'a2 printing_params -> Joint.joint_program -> ('a2, 'a1)
683  code_iteration_params -> (AST.ident, 'a2 List.list) Types.prod List.list
684
Note: See TracBrowser for help on using the repository browser.