source: driver/extracted/joint_printer.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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