source: extracted/joint.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: 54.0 KB
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83open BackEndOps
84
85open CostLabel
86
87open Order
88
89open Registers
90
91open I8051
92
93open BitVectorTrie
94
95open Graphs
96
97open LabelledObjects
98
99open Sets
100
101open Listb
102
103open String
104
105type 't argument =
106| Reg of 't
107| Imm of BitVector.byte
108
109val argument_rect_Type4 :
110  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
111
112val argument_rect_Type5 :
113  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
114
115val argument_rect_Type3 :
116  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
117
118val argument_rect_Type2 :
119  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
120
121val argument_rect_Type1 :
122  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
123
124val argument_rect_Type0 :
125  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
126
127val argument_inv_rect_Type4 :
128  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
129
130val argument_inv_rect_Type3 :
131  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
132
133val argument_inv_rect_Type2 :
134  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
135
136val argument_inv_rect_Type1 :
137  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
138
139val argument_inv_rect_Type0 :
140  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
141
142val argument_discr : 'a1 argument -> 'a1 argument -> __
143
144val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __
145
146type psd_argument = Registers.register argument
147
148val psd_argument_from_reg : Registers.register -> psd_argument
149
150val dpi1__o__reg_to_psd_argument__o__inject :
151  (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0
152
153val eject__o__reg_to_psd_argument__o__inject :
154  Registers.register Types.sig0 -> psd_argument Types.sig0
155
156val reg_to_psd_argument__o__inject :
157  Registers.register -> psd_argument Types.sig0
158
159val dpi1__o__reg_to_psd_argument :
160  (Registers.register, 'a1) Types.dPair -> psd_argument
161
162val eject__o__reg_to_psd_argument :
163  Registers.register Types.sig0 -> psd_argument
164
165val psd_argument_from_byte : BitVector.byte -> psd_argument
166
167val dpi1__o__byte_to_psd_argument__o__inject :
168  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
169
170val eject__o__byte_to_psd_argument__o__inject :
171  BitVector.byte Types.sig0 -> psd_argument Types.sig0
172
173val byte_to_psd_argument__o__inject :
174  BitVector.byte -> psd_argument Types.sig0
175
176val dpi1__o__byte_to_psd_argument :
177  (BitVector.byte, 'a1) Types.dPair -> psd_argument
178
179val eject__o__byte_to_psd_argument :
180  BitVector.byte Types.sig0 -> psd_argument
181
182type hdw_argument = I8051.register argument
183
184val hdw_argument_from_reg : I8051.register -> hdw_argument
185
186val dpi1__o__reg_to_hdw_argument__o__inject :
187  (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0
188
189val eject__o__reg_to_hdw_argument__o__inject :
190  I8051.register Types.sig0 -> hdw_argument Types.sig0
191
192val reg_to_hdw_argument__o__inject :
193  I8051.register -> hdw_argument Types.sig0
194
195val dpi1__o__reg_to_hdw_argument :
196  (I8051.register, 'a1) Types.dPair -> hdw_argument
197
198val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument
199
200val hdw_argument_from_byte : BitVector.byte -> hdw_argument
201
202val dpi1__o__byte_to_hdw_argument__o__inject :
203  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
204
205val eject__o__byte_to_hdw_argument__o__inject :
206  BitVector.byte Types.sig0 -> psd_argument Types.sig0
207
208val byte_to_hdw_argument__o__inject :
209  BitVector.byte -> psd_argument Types.sig0
210
211val dpi1__o__byte_to_hdw_argument :
212  (BitVector.byte, 'a1) Types.dPair -> psd_argument
213
214val eject__o__byte_to_hdw_argument :
215  BitVector.byte Types.sig0 -> psd_argument
216
217val byte_of_nat : Nat.nat -> BitVector.byte
218
219val zero_byte : BitVector.byte
220
221type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
222                             has_tailcalls : Bool.bool }
223
224val unserialized_params_rect_Type4 :
225  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
226  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
227  unserialized_params -> 'a1
228
229val unserialized_params_rect_Type5 :
230  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
231  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
232  unserialized_params -> 'a1
233
234val unserialized_params_rect_Type3 :
235  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
236  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
237  unserialized_params -> 'a1
238
239val unserialized_params_rect_Type2 :
240  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
241  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
242  unserialized_params -> 'a1
243
244val unserialized_params_rect_Type1 :
245  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
246  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
247  unserialized_params -> 'a1
248
249val unserialized_params_rect_Type0 :
250  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
251  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
252  unserialized_params -> 'a1
253
254type acc_a_reg
255
256type acc_b_reg
257
258type acc_a_arg
259
260type acc_b_arg
261
262type dpl_reg
263
264type dph_reg
265
266type dpl_arg
267
268type dph_arg
269
270type snd_arg
271
272type pair_move
273
274type call_args
275
276type call_dest
277
278type ext_seq
279
280val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list
281
282val has_tailcalls : unserialized_params -> Bool.bool
283
284type paramsT
285
286val unserialized_params_inv_rect_Type4 :
287  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
288  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
289  __ -> __ -> 'a1) -> 'a1
290
291val unserialized_params_inv_rect_Type3 :
292  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
293  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
294  __ -> __ -> 'a1) -> 'a1
295
296val unserialized_params_inv_rect_Type2 :
297  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
298  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
299  __ -> __ -> 'a1) -> 'a1
300
301val unserialized_params_inv_rect_Type1 :
302  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
303  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
304  __ -> __ -> 'a1) -> 'a1
305
306val unserialized_params_inv_rect_Type0 :
307  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
308  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
309  __ -> __ -> 'a1) -> 'a1
310
311val unserialized_params_jmdiscr :
312  unserialized_params -> unserialized_params -> __
313
314type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
315                                            List.list);
316                               acc_b_regs : (__ -> Registers.register
317                                            List.list);
318                               acc_a_args : (__ -> Registers.register
319                                            List.list);
320                               acc_b_args : (__ -> Registers.register
321                                            List.list);
322                               dpl_regs : (__ -> Registers.register
323                                          List.list);
324                               dph_regs : (__ -> Registers.register
325                                          List.list);
326                               dpl_args : (__ -> Registers.register
327                                          List.list);
328                               dph_args : (__ -> Registers.register
329                                          List.list);
330                               snd_args : (__ -> Registers.register
331                                          List.list);
332                               pair_move_regs : (__ -> Registers.register
333                                                List.list);
334                               f_call_args : (__ -> Registers.register
335                                             List.list);
336                               f_call_dest : (__ -> Registers.register
337                                             List.list);
338                               ext_seq_regs : (__ -> Registers.register
339                                              List.list);
340                               params_regs : (__ -> Registers.register
341                                             List.list) }
342
343val get_pseudo_reg_functs_rect_Type4 :
344  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
345  Registers.register List.list) -> (__ -> Registers.register List.list) ->
346  (__ -> Registers.register List.list) -> (__ -> Registers.register
347  List.list) -> (__ -> Registers.register List.list) -> (__ ->
348  Registers.register List.list) -> (__ -> Registers.register List.list) ->
349  (__ -> Registers.register List.list) -> (__ -> Registers.register
350  List.list) -> (__ -> Registers.register List.list) -> (__ ->
351  Registers.register List.list) -> (__ -> Registers.register List.list) ->
352  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
353  'a1
354
355val get_pseudo_reg_functs_rect_Type5 :
356  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
357  Registers.register List.list) -> (__ -> Registers.register List.list) ->
358  (__ -> Registers.register List.list) -> (__ -> Registers.register
359  List.list) -> (__ -> Registers.register List.list) -> (__ ->
360  Registers.register List.list) -> (__ -> Registers.register List.list) ->
361  (__ -> Registers.register List.list) -> (__ -> Registers.register
362  List.list) -> (__ -> Registers.register List.list) -> (__ ->
363  Registers.register List.list) -> (__ -> Registers.register List.list) ->
364  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
365  'a1
366
367val get_pseudo_reg_functs_rect_Type3 :
368  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
369  Registers.register List.list) -> (__ -> Registers.register List.list) ->
370  (__ -> Registers.register List.list) -> (__ -> Registers.register
371  List.list) -> (__ -> Registers.register List.list) -> (__ ->
372  Registers.register List.list) -> (__ -> Registers.register List.list) ->
373  (__ -> Registers.register List.list) -> (__ -> Registers.register
374  List.list) -> (__ -> Registers.register List.list) -> (__ ->
375  Registers.register List.list) -> (__ -> Registers.register List.list) ->
376  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
377  'a1
378
379val get_pseudo_reg_functs_rect_Type2 :
380  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
381  Registers.register List.list) -> (__ -> Registers.register List.list) ->
382  (__ -> Registers.register List.list) -> (__ -> Registers.register
383  List.list) -> (__ -> Registers.register List.list) -> (__ ->
384  Registers.register List.list) -> (__ -> Registers.register List.list) ->
385  (__ -> Registers.register List.list) -> (__ -> Registers.register
386  List.list) -> (__ -> Registers.register List.list) -> (__ ->
387  Registers.register List.list) -> (__ -> Registers.register List.list) ->
388  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
389  'a1
390
391val get_pseudo_reg_functs_rect_Type1 :
392  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
393  Registers.register List.list) -> (__ -> Registers.register List.list) ->
394  (__ -> Registers.register List.list) -> (__ -> Registers.register
395  List.list) -> (__ -> Registers.register List.list) -> (__ ->
396  Registers.register List.list) -> (__ -> Registers.register List.list) ->
397  (__ -> Registers.register List.list) -> (__ -> Registers.register
398  List.list) -> (__ -> Registers.register List.list) -> (__ ->
399  Registers.register List.list) -> (__ -> Registers.register List.list) ->
400  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
401  'a1
402
403val get_pseudo_reg_functs_rect_Type0 :
404  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
405  Registers.register List.list) -> (__ -> Registers.register List.list) ->
406  (__ -> Registers.register List.list) -> (__ -> Registers.register
407  List.list) -> (__ -> Registers.register List.list) -> (__ ->
408  Registers.register List.list) -> (__ -> Registers.register List.list) ->
409  (__ -> Registers.register List.list) -> (__ -> Registers.register
410  List.list) -> (__ -> Registers.register List.list) -> (__ ->
411  Registers.register List.list) -> (__ -> Registers.register List.list) ->
412  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
413  'a1
414
415val acc_a_regs :
416  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
417  List.list
418
419val acc_b_regs :
420  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
421  List.list
422
423val acc_a_args :
424  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
425  List.list
426
427val acc_b_args :
428  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
429  List.list
430
431val dpl_regs :
432  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
433  List.list
434
435val dph_regs :
436  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
437  List.list
438
439val dpl_args :
440  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
441  List.list
442
443val dph_args :
444  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
445  List.list
446
447val snd_args :
448  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
449  List.list
450
451val pair_move_regs :
452  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
453  List.list
454
455val f_call_args :
456  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
457  List.list
458
459val f_call_dest :
460  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
461  List.list
462
463val ext_seq_regs :
464  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
465  List.list
466
467val params_regs :
468  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
469  List.list
470
471val get_pseudo_reg_functs_inv_rect_Type4 :
472  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
473  List.list) -> (__ -> Registers.register List.list) -> (__ ->
474  Registers.register List.list) -> (__ -> Registers.register List.list) ->
475  (__ -> Registers.register List.list) -> (__ -> Registers.register
476  List.list) -> (__ -> Registers.register List.list) -> (__ ->
477  Registers.register List.list) -> (__ -> Registers.register List.list) ->
478  (__ -> Registers.register List.list) -> (__ -> Registers.register
479  List.list) -> (__ -> Registers.register List.list) -> (__ ->
480  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
481  -> 'a1) -> 'a1
482
483val get_pseudo_reg_functs_inv_rect_Type3 :
484  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
485  List.list) -> (__ -> Registers.register List.list) -> (__ ->
486  Registers.register List.list) -> (__ -> Registers.register List.list) ->
487  (__ -> Registers.register List.list) -> (__ -> Registers.register
488  List.list) -> (__ -> Registers.register List.list) -> (__ ->
489  Registers.register List.list) -> (__ -> Registers.register List.list) ->
490  (__ -> Registers.register List.list) -> (__ -> Registers.register
491  List.list) -> (__ -> Registers.register List.list) -> (__ ->
492  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
493  -> 'a1) -> 'a1
494
495val get_pseudo_reg_functs_inv_rect_Type2 :
496  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
497  List.list) -> (__ -> Registers.register List.list) -> (__ ->
498  Registers.register List.list) -> (__ -> Registers.register List.list) ->
499  (__ -> Registers.register List.list) -> (__ -> Registers.register
500  List.list) -> (__ -> Registers.register List.list) -> (__ ->
501  Registers.register List.list) -> (__ -> Registers.register List.list) ->
502  (__ -> Registers.register List.list) -> (__ -> Registers.register
503  List.list) -> (__ -> Registers.register List.list) -> (__ ->
504  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
505  -> 'a1) -> 'a1
506
507val get_pseudo_reg_functs_inv_rect_Type1 :
508  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
509  List.list) -> (__ -> Registers.register List.list) -> (__ ->
510  Registers.register List.list) -> (__ -> Registers.register List.list) ->
511  (__ -> Registers.register List.list) -> (__ -> Registers.register
512  List.list) -> (__ -> Registers.register List.list) -> (__ ->
513  Registers.register List.list) -> (__ -> Registers.register List.list) ->
514  (__ -> Registers.register List.list) -> (__ -> Registers.register
515  List.list) -> (__ -> Registers.register List.list) -> (__ ->
516  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
517  -> 'a1) -> 'a1
518
519val get_pseudo_reg_functs_inv_rect_Type0 :
520  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
521  List.list) -> (__ -> Registers.register List.list) -> (__ ->
522  Registers.register List.list) -> (__ -> Registers.register List.list) ->
523  (__ -> Registers.register List.list) -> (__ -> Registers.register
524  List.list) -> (__ -> Registers.register List.list) -> (__ ->
525  Registers.register List.list) -> (__ -> Registers.register List.list) ->
526  (__ -> Registers.register List.list) -> (__ -> Registers.register
527  List.list) -> (__ -> Registers.register List.list) -> (__ ->
528  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
529  -> 'a1) -> 'a1
530
531val get_pseudo_reg_functs_jmdiscr :
532  unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs -> __
533
534type uns_params = { u_pars : unserialized_params;
535                    functs : get_pseudo_reg_functs }
536
537val uns_params_rect_Type4 :
538  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
539
540val uns_params_rect_Type5 :
541  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
542
543val uns_params_rect_Type3 :
544  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
545
546val uns_params_rect_Type2 :
547  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
548
549val uns_params_rect_Type1 :
550  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
551
552val uns_params_rect_Type0 :
553  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
554
555val u_pars : uns_params -> unserialized_params
556
557val functs : uns_params -> get_pseudo_reg_functs
558
559val uns_params_inv_rect_Type4 :
560  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
561  -> 'a1
562
563val uns_params_inv_rect_Type3 :
564  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
565  -> 'a1
566
567val uns_params_inv_rect_Type2 :
568  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
569  -> 'a1
570
571val uns_params_inv_rect_Type1 :
572  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
573  -> 'a1
574
575val uns_params_inv_rect_Type0 :
576  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
577  -> 'a1
578
579val uns_params_jmdiscr : uns_params -> uns_params -> __
580
581type joint_seq =
582| COMMENT of String.string
583| MOVE of __
584| POP of __
585| PUSH of __
586| ADDRESS of AST.ident * __ * __
587| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
588| OP1 of BackEndOps.op1 * __ * __
589| OP2 of BackEndOps.op2 * __ * __ * __
590| CLEAR_CARRY
591| SET_CARRY
592| LOAD of __ * __ * __
593| STORE of __ * __ * __
594| Extension_seq of __
595
596val joint_seq_rect_Type4 :
597  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
598  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
599  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
600  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
601  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
602  (__ -> 'a1) -> joint_seq -> 'a1
603
604val joint_seq_rect_Type5 :
605  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
606  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
607  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
608  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
609  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
610  (__ -> 'a1) -> joint_seq -> 'a1
611
612val joint_seq_rect_Type3 :
613  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
614  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
615  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
616  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
617  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
618  (__ -> 'a1) -> joint_seq -> 'a1
619
620val joint_seq_rect_Type2 :
621  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
622  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
623  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
624  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
625  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
626  (__ -> 'a1) -> joint_seq -> 'a1
627
628val joint_seq_rect_Type1 :
629  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
630  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
631  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
632  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
633  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
634  (__ -> 'a1) -> joint_seq -> 'a1
635
636val joint_seq_rect_Type0 :
637  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
638  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
639  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
640  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
641  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
642  (__ -> 'a1) -> joint_seq -> 'a1
643
644val joint_seq_inv_rect_Type4 :
645  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
646  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
647  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
648  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
649  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
650  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
651  'a1) -> (__ -> __ -> 'a1) -> 'a1
652
653val joint_seq_inv_rect_Type3 :
654  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
655  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
656  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
657  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
658  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
659  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
660  'a1) -> (__ -> __ -> 'a1) -> 'a1
661
662val joint_seq_inv_rect_Type2 :
663  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
664  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
665  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
666  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
667  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
668  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
669  'a1) -> (__ -> __ -> 'a1) -> 'a1
670
671val joint_seq_inv_rect_Type1 :
672  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
673  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
674  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
675  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
676  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
677  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
678  'a1) -> (__ -> __ -> 'a1) -> 'a1
679
680val joint_seq_inv_rect_Type0 :
681  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
682  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
683  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
684  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
685  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
686  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
687  'a1) -> (__ -> __ -> 'a1) -> 'a1
688
689val joint_seq_discr :
690  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
691
692val joint_seq_jmdiscr :
693  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
694
695val get_used_registers_from_seq :
696  unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
697  joint_seq -> Registers.register List.list
698
699val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
700
701val dpi1__o__extension_seq_to_seq__o__inject :
702  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
703  joint_seq Types.sig0
704
705val eject__o__extension_seq_to_seq__o__inject :
706  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
707  Types.sig0
708
709val extension_seq_to_seq__o__inject :
710  unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0
711
712val dpi1__o__extension_seq_to_seq :
713  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
714  joint_seq
715
716val eject__o__extension_seq_to_seq :
717  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
718
719type joint_step =
720| COST_LABEL of CostLabel.costlabel
721| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
722| COND of __ * Graphs.label
723| Step_seq of joint_seq
724
725val joint_step_rect_Type4 :
726  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
727  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
728  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
729
730val joint_step_rect_Type5 :
731  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
732  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
733  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
734
735val joint_step_rect_Type3 :
736  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
737  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
738  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
739
740val joint_step_rect_Type2 :
741  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
742  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
743  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
744
745val joint_step_rect_Type1 :
746  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
747  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
748  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
749
750val joint_step_rect_Type0 :
751  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
752  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
753  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
754
755val joint_step_inv_rect_Type4 :
756  unserialized_params -> AST.ident List.list -> joint_step ->
757  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
758  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
759  (joint_seq -> __ -> 'a1) -> 'a1
760
761val joint_step_inv_rect_Type3 :
762  unserialized_params -> AST.ident List.list -> joint_step ->
763  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
764  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
765  (joint_seq -> __ -> 'a1) -> 'a1
766
767val joint_step_inv_rect_Type2 :
768  unserialized_params -> AST.ident List.list -> joint_step ->
769  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
770  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
771  (joint_seq -> __ -> 'a1) -> 'a1
772
773val joint_step_inv_rect_Type1 :
774  unserialized_params -> AST.ident List.list -> joint_step ->
775  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
776  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
777  (joint_seq -> __ -> 'a1) -> 'a1
778
779val joint_step_inv_rect_Type0 :
780  unserialized_params -> AST.ident List.list -> joint_step ->
781  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
782  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
783  (joint_seq -> __ -> 'a1) -> 'a1
784
785val joint_step_discr :
786  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
787  __
788
789val joint_step_jmdiscr :
790  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
791  __
792
793val get_used_registers_from_step :
794  unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
795  joint_step -> Registers.register List.list
796
797val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
798  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
799  joint_step Types.sig0
800
801val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
802  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
803  Types.sig0
804
805val extension_seq_to_seq__o__seq_to_step__o__inject :
806  unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0
807
808val dpi1__o__seq_to_step__o__inject :
809  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
810  -> joint_step Types.sig0
811
812val eject__o__seq_to_step__o__inject :
813  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
814  joint_step Types.sig0
815
816val seq_to_step__o__inject :
817  unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
818  Types.sig0
819
820val dpi1__o__extension_seq_to_seq__o__seq_to_step :
821  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
822  joint_step
823
824val eject__o__extension_seq_to_seq__o__seq_to_step :
825  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
826
827val extension_seq_to_seq__o__seq_to_step :
828  unserialized_params -> AST.ident List.list -> __ -> joint_step
829
830val dpi1__o__seq_to_step :
831  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
832  -> joint_step
833
834val eject__o__seq_to_step :
835  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
836  joint_step
837
838val step_labels :
839  unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
840  List.list
841
842type stmt_params = { uns_pars : uns_params;
843                     succ_label : (__ -> Graphs.label Types.option);
844                     has_fcond : Bool.bool }
845
846val stmt_params_rect_Type4 :
847  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
848  -> stmt_params -> 'a1
849
850val stmt_params_rect_Type5 :
851  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
852  -> stmt_params -> 'a1
853
854val stmt_params_rect_Type3 :
855  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
856  -> stmt_params -> 'a1
857
858val stmt_params_rect_Type2 :
859  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
860  -> stmt_params -> 'a1
861
862val stmt_params_rect_Type1 :
863  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
864  -> stmt_params -> 'a1
865
866val stmt_params_rect_Type0 :
867  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
868  -> stmt_params -> 'a1
869
870val uns_pars : stmt_params -> uns_params
871
872type succ
873
874val succ_label : stmt_params -> __ -> Graphs.label Types.option
875
876val has_fcond : stmt_params -> Bool.bool
877
878val stmt_params_inv_rect_Type4 :
879  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
880  Bool.bool -> __ -> 'a1) -> 'a1
881
882val stmt_params_inv_rect_Type3 :
883  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
884  Bool.bool -> __ -> 'a1) -> 'a1
885
886val stmt_params_inv_rect_Type2 :
887  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
888  Bool.bool -> __ -> 'a1) -> 'a1
889
890val stmt_params_inv_rect_Type1 :
891  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
892  Bool.bool -> __ -> 'a1) -> 'a1
893
894val stmt_params_inv_rect_Type0 :
895  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
896  Bool.bool -> __ -> 'a1) -> 'a1
897
898val stmt_params_jmdiscr : stmt_params -> stmt_params -> __
899
900val uns_pars__o__u_pars : stmt_params -> unserialized_params
901
902type joint_fin_step =
903| GOTO of Graphs.label
904| RETURN
905| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
906
907val joint_fin_step_rect_Type4 :
908  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
909  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
910
911val joint_fin_step_rect_Type5 :
912  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
913  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
914
915val joint_fin_step_rect_Type3 :
916  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
917  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
918
919val joint_fin_step_rect_Type2 :
920  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
921  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
922
923val joint_fin_step_rect_Type1 :
924  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
925  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
926
927val joint_fin_step_rect_Type0 :
928  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
929  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
930
931val joint_fin_step_inv_rect_Type4 :
932  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
933  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
934  'a1) -> 'a1
935
936val joint_fin_step_inv_rect_Type3 :
937  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
938  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
939  'a1) -> 'a1
940
941val joint_fin_step_inv_rect_Type2 :
942  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
943  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
944  'a1) -> 'a1
945
946val joint_fin_step_inv_rect_Type1 :
947  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
948  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
949  'a1) -> 'a1
950
951val joint_fin_step_inv_rect_Type0 :
952  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
953  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
954  'a1) -> 'a1
955
956val joint_fin_step_discr :
957  unserialized_params -> joint_fin_step -> joint_fin_step -> __
958
959val joint_fin_step_jmdiscr :
960  unserialized_params -> joint_fin_step -> joint_fin_step -> __
961
962val fin_step_labels :
963  unserialized_params -> joint_fin_step -> Graphs.label List.list
964
965type joint_statement =
966| Sequential of joint_step * __
967| Final of joint_fin_step
968| FCOND of __ * Graphs.label * Graphs.label
969
970val joint_statement_rect_Type4 :
971  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
972  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
973  'a1) -> joint_statement -> 'a1
974
975val joint_statement_rect_Type5 :
976  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
977  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
978  'a1) -> joint_statement -> 'a1
979
980val joint_statement_rect_Type3 :
981  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
982  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
983  'a1) -> joint_statement -> 'a1
984
985val joint_statement_rect_Type2 :
986  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
987  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
988  'a1) -> joint_statement -> 'a1
989
990val joint_statement_rect_Type1 :
991  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
992  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
993  'a1) -> joint_statement -> 'a1
994
995val joint_statement_rect_Type0 :
996  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
997  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
998  'a1) -> joint_statement -> 'a1
999
1000val joint_statement_inv_rect_Type4 :
1001  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1002  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1003  -> Graphs.label -> __ -> 'a1) -> 'a1
1004
1005val joint_statement_inv_rect_Type3 :
1006  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1007  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1008  -> Graphs.label -> __ -> 'a1) -> 'a1
1009
1010val joint_statement_inv_rect_Type2 :
1011  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1012  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1013  -> Graphs.label -> __ -> 'a1) -> 'a1
1014
1015val joint_statement_inv_rect_Type1 :
1016  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1017  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1018  -> Graphs.label -> __ -> 'a1) -> 'a1
1019
1020val joint_statement_inv_rect_Type0 :
1021  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1022  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1023  -> Graphs.label -> __ -> 'a1) -> 'a1
1024
1025val joint_statement_discr :
1026  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1027  __
1028
1029val joint_statement_jmdiscr :
1030  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1031  __
1032
1033val dpi1__o__fin_step_to_stmt__o__inject :
1034  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1035  joint_statement Types.sig0
1036
1037val eject__o__fin_step_to_stmt__o__inject :
1038  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1039  joint_statement Types.sig0
1040
1041val fin_step_to_stmt__o__inject :
1042  stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1043  Types.sig0
1044
1045val dpi1__o__fin_step_to_stmt :
1046  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1047  joint_statement
1048
1049val eject__o__fin_step_to_stmt :
1050  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1051  joint_statement
1052
1053type params = { stmt_pars : stmt_params;
1054                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1055                          Types.option);
1056                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1057                                 -> __ Types.option);
1058                point_of_succ : (__ -> __ -> __) }
1059
1060val params_rect_Type4 :
1061  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1062  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1063  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1064
1065val params_rect_Type5 :
1066  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1067  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1068  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1069
1070val params_rect_Type3 :
1071  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1072  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1073  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1074
1075val params_rect_Type2 :
1076  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1077  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1078  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1079
1080val params_rect_Type1 :
1081  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1082  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1083  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1084
1085val params_rect_Type0 :
1086  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1087  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1088  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1089
1090val stmt_pars : params -> stmt_params
1091
1092type codeT
1093
1094type code_point
1095
1096val stmt_at :
1097  params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option
1098
1099val point_of_label :
1100  params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option
1101
1102val point_of_succ : params -> __ -> __ -> __
1103
1104val params_inv_rect_Type4 :
1105  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1106  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1107  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1108
1109val params_inv_rect_Type3 :
1110  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1111  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1112  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1113
1114val params_inv_rect_Type2 :
1115  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1116  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1117  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1118
1119val params_inv_rect_Type1 :
1120  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1121  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1122  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1123
1124val params_inv_rect_Type0 :
1125  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1126  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1127  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1128
1129val params_jmdiscr : params -> params -> __
1130
1131val stmt_pars__o__uns_pars : params -> uns_params
1132
1133val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params
1134
1135val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool
1136
1137val code_has_label :
1138  params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool
1139
1140val stmt_explicit_labels :
1141  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1142  List.list
1143
1144val stmt_implicit_label :
1145  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1146  Types.option
1147
1148val stmt_labels :
1149  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1150  List.list
1151
1152val stmt_registers :
1153  stmt_params -> AST.ident List.list -> joint_statement -> Registers.register
1154  List.list
1155
1156type lin_params =
1157  uns_params
1158  (* singleton inductive, whose constructor was mk_lin_params *)
1159
1160val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1
1161
1162val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1
1163
1164val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1
1165
1166val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1
1167
1168val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1
1169
1170val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1
1171
1172val l_u_pars : lin_params -> uns_params
1173
1174val lin_params_inv_rect_Type4 :
1175  lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1176
1177val lin_params_inv_rect_Type3 :
1178  lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1179
1180val lin_params_inv_rect_Type2 :
1181  lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1182
1183val lin_params_inv_rect_Type1 :
1184  lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1185
1186val lin_params_inv_rect_Type0 :
1187  lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1188
1189val lin_params_jmdiscr : lin_params -> lin_params -> __
1190
1191val lin_params_to_params : lin_params -> params
1192
1193val lp_to_p__o__stmt_pars : lin_params -> stmt_params
1194
1195val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params
1196
1197val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1198  lin_params -> unserialized_params
1199
1200type graph_params =
1201  uns_params
1202  (* singleton inductive, whose constructor was mk_graph_params *)
1203
1204val graph_params_rect_Type4 : (uns_params -> 'a1) -> graph_params -> 'a1
1205
1206val graph_params_rect_Type5 : (uns_params -> 'a1) -> graph_params -> 'a1
1207
1208val graph_params_rect_Type3 : (uns_params -> 'a1) -> graph_params -> 'a1
1209
1210val graph_params_rect_Type2 : (uns_params -> 'a1) -> graph_params -> 'a1
1211
1212val graph_params_rect_Type1 : (uns_params -> 'a1) -> graph_params -> 'a1
1213
1214val graph_params_rect_Type0 : (uns_params -> 'a1) -> graph_params -> 'a1
1215
1216val g_u_pars : graph_params -> uns_params
1217
1218val graph_params_inv_rect_Type4 :
1219  graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1220
1221val graph_params_inv_rect_Type3 :
1222  graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1223
1224val graph_params_inv_rect_Type2 :
1225  graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1226
1227val graph_params_inv_rect_Type1 :
1228  graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1229
1230val graph_params_inv_rect_Type0 :
1231  graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1232
1233val graph_params_jmdiscr : graph_params -> graph_params -> __
1234
1235val graph_params_to_params : graph_params -> params
1236
1237val gp_to_p__o__stmt_pars : graph_params -> stmt_params
1238
1239val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params
1240
1241val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1242  graph_params -> unserialized_params
1243
1244type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1245                                 joint_if_runiverse : Identifiers.universe;
1246                                 joint_if_result : __; joint_if_params : 
1247                                 __; joint_if_stacksize : Nat.nat;
1248                                 joint_if_local_stacksize : Nat.nat;
1249                                 joint_if_code : __; joint_if_entry : 
1250                                 __ }
1251
1252val joint_internal_function_rect_Type4 :
1253  params -> AST.ident List.list -> (Identifiers.universe ->
1254  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1255  -> joint_internal_function -> 'a1
1256
1257val joint_internal_function_rect_Type5 :
1258  params -> AST.ident List.list -> (Identifiers.universe ->
1259  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1260  -> joint_internal_function -> 'a1
1261
1262val joint_internal_function_rect_Type3 :
1263  params -> AST.ident List.list -> (Identifiers.universe ->
1264  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1265  -> joint_internal_function -> 'a1
1266
1267val joint_internal_function_rect_Type2 :
1268  params -> AST.ident List.list -> (Identifiers.universe ->
1269  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1270  -> joint_internal_function -> 'a1
1271
1272val joint_internal_function_rect_Type1 :
1273  params -> AST.ident List.list -> (Identifiers.universe ->
1274  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1275  -> joint_internal_function -> 'a1
1276
1277val joint_internal_function_rect_Type0 :
1278  params -> AST.ident List.list -> (Identifiers.universe ->
1279  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1280  -> joint_internal_function -> 'a1
1281
1282val joint_if_luniverse :
1283  params -> AST.ident List.list -> joint_internal_function ->
1284  Identifiers.universe
1285
1286val joint_if_runiverse :
1287  params -> AST.ident List.list -> joint_internal_function ->
1288  Identifiers.universe
1289
1290val joint_if_result :
1291  params -> AST.ident List.list -> joint_internal_function -> __
1292
1293val joint_if_params :
1294  params -> AST.ident List.list -> joint_internal_function -> __
1295
1296val joint_if_stacksize :
1297  params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1298
1299val joint_if_local_stacksize :
1300  params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1301
1302val joint_if_code :
1303  params -> AST.ident List.list -> joint_internal_function -> __
1304
1305val joint_if_entry :
1306  params -> AST.ident List.list -> joint_internal_function -> __
1307
1308val joint_internal_function_inv_rect_Type4 :
1309  params -> AST.ident List.list -> joint_internal_function ->
1310  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1311  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1312
1313val joint_internal_function_inv_rect_Type3 :
1314  params -> AST.ident List.list -> joint_internal_function ->
1315  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1316  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1317
1318val joint_internal_function_inv_rect_Type2 :
1319  params -> AST.ident List.list -> joint_internal_function ->
1320  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1321  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1322
1323val joint_internal_function_inv_rect_Type1 :
1324  params -> AST.ident List.list -> joint_internal_function ->
1325  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1326  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1327
1328val joint_internal_function_inv_rect_Type0 :
1329  params -> AST.ident List.list -> joint_internal_function ->
1330  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1331  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1332
1333val joint_internal_function_jmdiscr :
1334  params -> AST.ident List.list -> joint_internal_function ->
1335  joint_internal_function -> __
1336
1337val good_if_rect_Type4 :
1338  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1339  -> __ -> __ -> 'a1) -> 'a1
1340
1341val good_if_rect_Type5 :
1342  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1343  -> __ -> __ -> 'a1) -> 'a1
1344
1345val good_if_rect_Type3 :
1346  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1347  -> __ -> __ -> 'a1) -> 'a1
1348
1349val good_if_rect_Type2 :
1350  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1351  -> __ -> __ -> 'a1) -> 'a1
1352
1353val good_if_rect_Type1 :
1354  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1355  -> __ -> __ -> 'a1) -> 'a1
1356
1357val good_if_rect_Type0 :
1358  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1359  -> __ -> __ -> 'a1) -> 'a1
1360
1361val good_if_inv_rect_Type4 :
1362  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1363  -> __ -> __ -> __ -> 'a1) -> 'a1
1364
1365val good_if_inv_rect_Type3 :
1366  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1367  -> __ -> __ -> __ -> 'a1) -> 'a1
1368
1369val good_if_inv_rect_Type2 :
1370  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1371  -> __ -> __ -> __ -> 'a1) -> 'a1
1372
1373val good_if_inv_rect_Type1 :
1374  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1375  -> __ -> __ -> __ -> 'a1) -> 'a1
1376
1377val good_if_inv_rect_Type0 :
1378  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1379  -> __ -> __ -> __ -> 'a1) -> 'a1
1380
1381val good_if_discr :
1382  params -> AST.ident List.list -> joint_internal_function -> __
1383
1384val good_if_jmdiscr :
1385  params -> AST.ident List.list -> joint_internal_function -> __
1386
1387type joint_closed_internal_function = joint_internal_function Types.sig0
1388
1389val set_joint_code :
1390  AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
1391  joint_internal_function
1392
1393val set_luniverse :
1394  params -> AST.ident List.list -> joint_internal_function ->
1395  Identifiers.universe -> joint_internal_function
1396
1397val set_runiverse :
1398  params -> AST.ident List.list -> joint_internal_function ->
1399  Identifiers.universe -> joint_internal_function
1400
1401val add_graph :
1402  graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1403  joint_internal_function -> joint_internal_function
1404
1405type joint_function = joint_closed_internal_function AST.fundef
1406
1407type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
1408                                    AST.program;
1409                       init_cost_label : CostLabel.costlabel }
1410
1411val joint_program_rect_Type4 :
1412  params -> ((joint_function, AST.init_data List.list) AST.program ->
1413  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1414
1415val joint_program_rect_Type5 :
1416  params -> ((joint_function, AST.init_data List.list) AST.program ->
1417  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1418
1419val joint_program_rect_Type3 :
1420  params -> ((joint_function, AST.init_data List.list) AST.program ->
1421  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1422
1423val joint_program_rect_Type2 :
1424  params -> ((joint_function, AST.init_data List.list) AST.program ->
1425  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1426
1427val joint_program_rect_Type1 :
1428  params -> ((joint_function, AST.init_data List.list) AST.program ->
1429  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1430
1431val joint_program_rect_Type0 :
1432  params -> ((joint_function, AST.init_data List.list) AST.program ->
1433  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
1434
1435val joint_prog :
1436  params -> joint_program -> (joint_function, AST.init_data List.list)
1437  AST.program
1438
1439val init_cost_label : params -> joint_program -> CostLabel.costlabel
1440
1441val joint_program_inv_rect_Type4 :
1442  params -> joint_program -> ((joint_function, AST.init_data List.list)
1443  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
1444
1445val joint_program_inv_rect_Type3 :
1446  params -> joint_program -> ((joint_function, AST.init_data List.list)
1447  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
1448
1449val joint_program_inv_rect_Type2 :
1450  params -> joint_program -> ((joint_function, AST.init_data List.list)
1451  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
1452
1453val joint_program_inv_rect_Type1 :
1454  params -> joint_program -> ((joint_function, AST.init_data List.list)
1455  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
1456
1457val joint_program_inv_rect_Type0 :
1458  params -> joint_program -> ((joint_function, AST.init_data List.list)
1459  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
1460
1461val joint_program_discr : params -> joint_program -> joint_program -> __
1462
1463val joint_program_jmdiscr : params -> joint_program -> joint_program -> __
1464
1465val dpi1__o__joint_prog__o__inject :
1466  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1467  AST.init_data List.list) AST.program Types.sig0
1468
1469val eject__o__joint_prog__o__inject :
1470  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1471  List.list) AST.program Types.sig0
1472
1473val joint_prog__o__inject :
1474  params -> joint_program -> (joint_function, AST.init_data List.list)
1475  AST.program Types.sig0
1476
1477val dpi1__o__joint_prog :
1478  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1479  AST.init_data List.list) AST.program
1480
1481val eject__o__joint_prog :
1482  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1483  List.list) AST.program
1484
1485type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
1486
1487val stack_cost : params -> joint_program -> stack_cost_model
1488
1489open Extra_bool
1490
1491open Coqlib
1492
1493open Values
1494
1495open FrontEndVal
1496
1497open GenMem
1498
1499open FrontEndMem
1500
1501open Globalenvs
1502
1503val globals_stacksize : params -> joint_program -> Nat.nat
1504
Note: See TracBrowser for help on using the repository browser.