source: extracted/joint.ml @ 3009

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

New extraction.

File size: 110.7 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
109(** val argument_rect_Type4 :
110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
111let rec argument_rect_Type4 h_Reg h_Imm = function
112| Reg x_3753 -> h_Reg x_3753
113| Imm x_3754 -> h_Imm x_3754
114
115(** val argument_rect_Type5 :
116    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
117let rec argument_rect_Type5 h_Reg h_Imm = function
118| Reg x_3758 -> h_Reg x_3758
119| Imm x_3759 -> h_Imm x_3759
120
121(** val argument_rect_Type3 :
122    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
123let rec argument_rect_Type3 h_Reg h_Imm = function
124| Reg x_3763 -> h_Reg x_3763
125| Imm x_3764 -> h_Imm x_3764
126
127(** val argument_rect_Type2 :
128    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
129let rec argument_rect_Type2 h_Reg h_Imm = function
130| Reg x_3768 -> h_Reg x_3768
131| Imm x_3769 -> h_Imm x_3769
132
133(** val argument_rect_Type1 :
134    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
135let rec argument_rect_Type1 h_Reg h_Imm = function
136| Reg x_3773 -> h_Reg x_3773
137| Imm x_3774 -> h_Imm x_3774
138
139(** val argument_rect_Type0 :
140    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
141let rec argument_rect_Type0 h_Reg h_Imm = function
142| Reg x_3778 -> h_Reg x_3778
143| Imm x_3779 -> h_Imm x_3779
144
145(** val argument_inv_rect_Type4 :
146    'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
147    'a2 **)
148let argument_inv_rect_Type4 hterm h1 h2 =
149  let hcut = argument_rect_Type4 h1 h2 hterm in hcut __
150
151(** val argument_inv_rect_Type3 :
152    'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
153    'a2 **)
154let argument_inv_rect_Type3 hterm h1 h2 =
155  let hcut = argument_rect_Type3 h1 h2 hterm in hcut __
156
157(** val argument_inv_rect_Type2 :
158    'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
159    'a2 **)
160let argument_inv_rect_Type2 hterm h1 h2 =
161  let hcut = argument_rect_Type2 h1 h2 hterm in hcut __
162
163(** val argument_inv_rect_Type1 :
164    'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
165    'a2 **)
166let argument_inv_rect_Type1 hterm h1 h2 =
167  let hcut = argument_rect_Type1 h1 h2 hterm in hcut __
168
169(** val argument_inv_rect_Type0 :
170    'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
171    'a2 **)
172let argument_inv_rect_Type0 hterm h1 h2 =
173  let hcut = argument_rect_Type0 h1 h2 hterm in hcut __
174
175(** val argument_discr : 'a1 argument -> 'a1 argument -> __ **)
176let argument_discr x y =
177  Logic.eq_rect_Type2 x
178    (match x with
179     | Reg a0 -> Obj.magic (fun _ dH -> dH __)
180     | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
181
182(** val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __ **)
183let argument_jmdiscr x y =
184  Logic.eq_rect_Type2 x
185    (match x with
186     | Reg a0 -> Obj.magic (fun _ dH -> dH __)
187     | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
188
189type psd_argument = Registers.register argument
190
191(** val psd_argument_from_reg : Registers.register -> psd_argument **)
192let psd_argument_from_reg x =
193  Reg x
194
195(** val dpi1__o__reg_to_psd_argument__o__inject :
196    (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0 **)
197let dpi1__o__reg_to_psd_argument__o__inject x2 =
198  psd_argument_from_reg x2.Types.dpi1
199
200(** val eject__o__reg_to_psd_argument__o__inject :
201    Registers.register Types.sig0 -> psd_argument Types.sig0 **)
202let eject__o__reg_to_psd_argument__o__inject x2 =
203  psd_argument_from_reg (Types.pi1 x2)
204
205(** val reg_to_psd_argument__o__inject :
206    Registers.register -> psd_argument Types.sig0 **)
207let reg_to_psd_argument__o__inject x1 =
208  psd_argument_from_reg x1
209
210(** val dpi1__o__reg_to_psd_argument :
211    (Registers.register, 'a1) Types.dPair -> psd_argument **)
212let dpi1__o__reg_to_psd_argument x1 =
213  psd_argument_from_reg x1.Types.dpi1
214
215(** val eject__o__reg_to_psd_argument :
216    Registers.register Types.sig0 -> psd_argument **)
217let eject__o__reg_to_psd_argument x1 =
218  psd_argument_from_reg (Types.pi1 x1)
219
220(** val psd_argument_from_byte : BitVector.byte -> psd_argument **)
221let psd_argument_from_byte x =
222  Imm x
223
224(** val dpi1__o__byte_to_psd_argument__o__inject :
225    (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
226let dpi1__o__byte_to_psd_argument__o__inject x2 =
227  psd_argument_from_byte x2.Types.dpi1
228
229(** val eject__o__byte_to_psd_argument__o__inject :
230    BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
231let eject__o__byte_to_psd_argument__o__inject x2 =
232  psd_argument_from_byte (Types.pi1 x2)
233
234(** val byte_to_psd_argument__o__inject :
235    BitVector.byte -> psd_argument Types.sig0 **)
236let byte_to_psd_argument__o__inject x1 =
237  psd_argument_from_byte x1
238
239(** val dpi1__o__byte_to_psd_argument :
240    (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
241let dpi1__o__byte_to_psd_argument x1 =
242  psd_argument_from_byte x1.Types.dpi1
243
244(** val eject__o__byte_to_psd_argument :
245    BitVector.byte Types.sig0 -> psd_argument **)
246let eject__o__byte_to_psd_argument x1 =
247  psd_argument_from_byte (Types.pi1 x1)
248
249type hdw_argument = I8051.register argument
250
251(** val hdw_argument_from_reg : I8051.register -> hdw_argument **)
252let hdw_argument_from_reg x =
253  Reg x
254
255(** val dpi1__o__reg_to_hdw_argument__o__inject :
256    (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0 **)
257let dpi1__o__reg_to_hdw_argument__o__inject x2 =
258  hdw_argument_from_reg x2.Types.dpi1
259
260(** val eject__o__reg_to_hdw_argument__o__inject :
261    I8051.register Types.sig0 -> hdw_argument Types.sig0 **)
262let eject__o__reg_to_hdw_argument__o__inject x2 =
263  hdw_argument_from_reg (Types.pi1 x2)
264
265(** val reg_to_hdw_argument__o__inject :
266    I8051.register -> hdw_argument Types.sig0 **)
267let reg_to_hdw_argument__o__inject x1 =
268  hdw_argument_from_reg x1
269
270(** val dpi1__o__reg_to_hdw_argument :
271    (I8051.register, 'a1) Types.dPair -> hdw_argument **)
272let dpi1__o__reg_to_hdw_argument x1 =
273  hdw_argument_from_reg x1.Types.dpi1
274
275(** val eject__o__reg_to_hdw_argument :
276    I8051.register Types.sig0 -> hdw_argument **)
277let eject__o__reg_to_hdw_argument x1 =
278  hdw_argument_from_reg (Types.pi1 x1)
279
280(** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **)
281let hdw_argument_from_byte x =
282  Imm x
283
284(** val dpi1__o__byte_to_hdw_argument__o__inject :
285    (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
286let dpi1__o__byte_to_hdw_argument__o__inject x2 =
287  psd_argument_from_byte x2.Types.dpi1
288
289(** val eject__o__byte_to_hdw_argument__o__inject :
290    BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
291let eject__o__byte_to_hdw_argument__o__inject x2 =
292  psd_argument_from_byte (Types.pi1 x2)
293
294(** val byte_to_hdw_argument__o__inject :
295    BitVector.byte -> psd_argument Types.sig0 **)
296let byte_to_hdw_argument__o__inject x1 =
297  psd_argument_from_byte x1
298
299(** val dpi1__o__byte_to_hdw_argument :
300    (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
301let dpi1__o__byte_to_hdw_argument x1 =
302  psd_argument_from_byte x1.Types.dpi1
303
304(** val eject__o__byte_to_hdw_argument :
305    BitVector.byte Types.sig0 -> psd_argument **)
306let eject__o__byte_to_hdw_argument x1 =
307  psd_argument_from_byte (Types.pi1 x1)
308
309(** val byte_of_nat : Nat.nat -> BitVector.byte **)
310let byte_of_nat =
311  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
312    (Nat.S (Nat.S Nat.O))))))))
313
314(** val zero_byte : BitVector.byte **)
315let zero_byte =
316  BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
317    Nat.O))))))))
318
319type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
320                             has_tailcalls : Bool.bool }
321
322(** val unserialized_params_rect_Type4 :
323    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
324    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
325    unserialized_params -> 'a1 **)
326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_3814 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_3814
329  in
330  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
331    ext_seq_labels0 has_tailcalls0 __
332
333(** val unserialized_params_rect_Type5 :
334    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
335    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
336    unserialized_params -> 'a1 **)
337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_3816 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_3816
340  in
341  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
342    ext_seq_labels0 has_tailcalls0 __
343
344(** val unserialized_params_rect_Type3 :
345    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
346    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
347    unserialized_params -> 'a1 **)
348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_3818 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_3818
351  in
352  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
353    ext_seq_labels0 has_tailcalls0 __
354
355(** val unserialized_params_rect_Type2 :
356    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
357    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
358    unserialized_params -> 'a1 **)
359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_3820 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_3820
362  in
363  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
364    ext_seq_labels0 has_tailcalls0 __
365
366(** val unserialized_params_rect_Type1 :
367    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
368    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
369    unserialized_params -> 'a1 **)
370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_3822 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_3822
373  in
374  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
375    ext_seq_labels0 has_tailcalls0 __
376
377(** val unserialized_params_rect_Type0 :
378    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
379    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
380    unserialized_params -> 'a1 **)
381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_3824 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_3824
384  in
385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
386    ext_seq_labels0 has_tailcalls0 __
387
388type acc_a_reg = __
389
390type acc_b_reg = __
391
392type acc_a_arg = __
393
394type acc_b_arg = __
395
396type dpl_reg = __
397
398type dph_reg = __
399
400type dpl_arg = __
401
402type dph_arg = __
403
404type snd_arg = __
405
406type pair_move = __
407
408type call_args = __
409
410type call_dest = __
411
412type ext_seq = __
413
414(** val ext_seq_labels :
415    unserialized_params -> __ -> Graphs.label List.list **)
416let rec ext_seq_labels xxx =
417  xxx.ext_seq_labels
418
419(** val has_tailcalls : unserialized_params -> Bool.bool **)
420let rec has_tailcalls xxx =
421  xxx.has_tailcalls
422
423type paramsT = __
424
425(** val unserialized_params_inv_rect_Type4 :
426    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
427    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
428    -> __ -> __ -> 'a1) -> 'a1 **)
429let unserialized_params_inv_rect_Type4 hterm h1 =
430  let hcut = unserialized_params_rect_Type4 h1 hterm in hcut __
431
432(** val unserialized_params_inv_rect_Type3 :
433    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
434    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
435    -> __ -> __ -> 'a1) -> 'a1 **)
436let unserialized_params_inv_rect_Type3 hterm h1 =
437  let hcut = unserialized_params_rect_Type3 h1 hterm in hcut __
438
439(** val unserialized_params_inv_rect_Type2 :
440    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
441    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
442    -> __ -> __ -> 'a1) -> 'a1 **)
443let unserialized_params_inv_rect_Type2 hterm h1 =
444  let hcut = unserialized_params_rect_Type2 h1 hterm in hcut __
445
446(** val unserialized_params_inv_rect_Type1 :
447    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
448    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
449    -> __ -> __ -> 'a1) -> 'a1 **)
450let unserialized_params_inv_rect_Type1 hterm h1 =
451  let hcut = unserialized_params_rect_Type1 h1 hterm in hcut __
452
453(** val unserialized_params_inv_rect_Type0 :
454    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
455    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
456    -> __ -> __ -> 'a1) -> 'a1 **)
457let unserialized_params_inv_rect_Type0 hterm h1 =
458  let hcut = unserialized_params_rect_Type0 h1 hterm in hcut __
459
460(** val unserialized_params_jmdiscr :
461    unserialized_params -> unserialized_params -> __ **)
462let unserialized_params_jmdiscr x y =
463  Logic.eq_rect_Type2 x
464    (let { ext_seq_labels = a13; has_tailcalls = a14 } = x in
465    Obj.magic (fun _ dH ->
466      dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
467
468type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
469                                            List.list);
470                               acc_b_regs : (__ -> Registers.register
471                                            List.list);
472                               acc_a_args : (__ -> Registers.register
473                                            List.list);
474                               acc_b_args : (__ -> Registers.register
475                                            List.list);
476                               dpl_regs : (__ -> Registers.register
477                                          List.list);
478                               dph_regs : (__ -> Registers.register
479                                          List.list);
480                               dpl_args : (__ -> Registers.register
481                                          List.list);
482                               dph_args : (__ -> Registers.register
483                                          List.list);
484                               snd_args : (__ -> Registers.register
485                                          List.list);
486                               pair_move_regs : (__ -> Registers.register
487                                                List.list);
488                               f_call_args : (__ -> Registers.register
489                                             List.list);
490                               f_call_dest : (__ -> Registers.register
491                                             List.list);
492                               ext_seq_regs : (__ -> Registers.register
493                                              List.list);
494                               params_regs : (__ -> Registers.register
495                                             List.list) }
496
497(** val get_pseudo_reg_functs_rect_Type4 :
498    unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
499    Registers.register List.list) -> (__ -> Registers.register List.list) ->
500    (__ -> Registers.register List.list) -> (__ -> Registers.register
501    List.list) -> (__ -> Registers.register List.list) -> (__ ->
502    Registers.register List.list) -> (__ -> Registers.register List.list) ->
503    (__ -> Registers.register List.list) -> (__ -> Registers.register
504    List.list) -> (__ -> Registers.register List.list) -> (__ ->
505    Registers.register List.list) -> (__ -> Registers.register List.list) ->
506    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
507    'a1 **)
508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_3841 =
509  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
510    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
511    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
512    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
513    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
514    params_regs0 } = x_3841
515  in
516  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
517    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
518    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
519
520(** val get_pseudo_reg_functs_rect_Type5 :
521    unserialized_params -> ((__ -> 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    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
530    'a1 **)
531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_3843 =
532  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
533    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
534    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
535    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
536    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
537    params_regs0 } = x_3843
538  in
539  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
540    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
541    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
542
543(** val get_pseudo_reg_functs_rect_Type3 :
544    unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
545    Registers.register List.list) -> (__ -> Registers.register List.list) ->
546    (__ -> Registers.register List.list) -> (__ -> Registers.register
547    List.list) -> (__ -> Registers.register List.list) -> (__ ->
548    Registers.register List.list) -> (__ -> Registers.register List.list) ->
549    (__ -> Registers.register List.list) -> (__ -> Registers.register
550    List.list) -> (__ -> Registers.register List.list) -> (__ ->
551    Registers.register List.list) -> (__ -> Registers.register List.list) ->
552    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
553    'a1 **)
554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_3845 =
555  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
556    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
557    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
558    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
559    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
560    params_regs0 } = x_3845
561  in
562  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
563    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
564    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
565
566(** val get_pseudo_reg_functs_rect_Type2 :
567    unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
568    Registers.register List.list) -> (__ -> Registers.register List.list) ->
569    (__ -> Registers.register List.list) -> (__ -> Registers.register
570    List.list) -> (__ -> Registers.register List.list) -> (__ ->
571    Registers.register List.list) -> (__ -> Registers.register List.list) ->
572    (__ -> Registers.register List.list) -> (__ -> Registers.register
573    List.list) -> (__ -> Registers.register List.list) -> (__ ->
574    Registers.register List.list) -> (__ -> Registers.register List.list) ->
575    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
576    'a1 **)
577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_3847 =
578  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
579    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
580    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
581    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
582    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
583    params_regs0 } = x_3847
584  in
585  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
586    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
587    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
588
589(** val get_pseudo_reg_functs_rect_Type1 :
590    unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
591    Registers.register List.list) -> (__ -> Registers.register List.list) ->
592    (__ -> Registers.register List.list) -> (__ -> Registers.register
593    List.list) -> (__ -> Registers.register List.list) -> (__ ->
594    Registers.register List.list) -> (__ -> Registers.register List.list) ->
595    (__ -> Registers.register List.list) -> (__ -> Registers.register
596    List.list) -> (__ -> Registers.register List.list) -> (__ ->
597    Registers.register List.list) -> (__ -> Registers.register List.list) ->
598    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
599    'a1 **)
600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_3849 =
601  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
602    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
603    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
604    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
605    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
606    params_regs0 } = x_3849
607  in
608  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
609    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
610    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
611
612(** val get_pseudo_reg_functs_rect_Type0 :
613    unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
614    Registers.register List.list) -> (__ -> Registers.register List.list) ->
615    (__ -> Registers.register List.list) -> (__ -> Registers.register
616    List.list) -> (__ -> Registers.register List.list) -> (__ ->
617    Registers.register List.list) -> (__ -> Registers.register List.list) ->
618    (__ -> Registers.register List.list) -> (__ -> Registers.register
619    List.list) -> (__ -> Registers.register List.list) -> (__ ->
620    Registers.register List.list) -> (__ -> Registers.register List.list) ->
621    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
622    'a1 **)
623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_3851 =
624  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
625    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
626    dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
627    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
628    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
629    params_regs0 } = x_3851
630  in
631  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
632    dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
633    f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
634
635(** val acc_a_regs :
636    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
637    List.list **)
638let rec acc_a_regs p xxx =
639  xxx.acc_a_regs
640
641(** val acc_b_regs :
642    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
643    List.list **)
644let rec acc_b_regs p xxx =
645  xxx.acc_b_regs
646
647(** val acc_a_args :
648    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
649    List.list **)
650let rec acc_a_args p xxx =
651  xxx.acc_a_args
652
653(** val acc_b_args :
654    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
655    List.list **)
656let rec acc_b_args p xxx =
657  xxx.acc_b_args
658
659(** val dpl_regs :
660    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
661    List.list **)
662let rec dpl_regs p xxx =
663  xxx.dpl_regs
664
665(** val dph_regs :
666    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
667    List.list **)
668let rec dph_regs p xxx =
669  xxx.dph_regs
670
671(** val dpl_args :
672    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
673    List.list **)
674let rec dpl_args p xxx =
675  xxx.dpl_args
676
677(** val dph_args :
678    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
679    List.list **)
680let rec dph_args p xxx =
681  xxx.dph_args
682
683(** val snd_args :
684    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
685    List.list **)
686let rec snd_args p xxx =
687  xxx.snd_args
688
689(** val pair_move_regs :
690    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
691    List.list **)
692let rec pair_move_regs p xxx =
693  xxx.pair_move_regs
694
695(** val f_call_args :
696    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
697    List.list **)
698let rec f_call_args p xxx =
699  xxx.f_call_args
700
701(** val f_call_dest :
702    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
703    List.list **)
704let rec f_call_dest p xxx =
705  xxx.f_call_dest
706
707(** val ext_seq_regs :
708    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
709    List.list **)
710let rec ext_seq_regs p xxx =
711  xxx.ext_seq_regs
712
713(** val params_regs :
714    unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
715    List.list **)
716let rec params_regs p xxx =
717  xxx.params_regs
718
719(** val get_pseudo_reg_functs_inv_rect_Type4 :
720    unserialized_params -> get_pseudo_reg_functs -> ((__ ->
721    Registers.register List.list) -> (__ -> Registers.register List.list) ->
722    (__ -> Registers.register List.list) -> (__ -> Registers.register
723    List.list) -> (__ -> Registers.register List.list) -> (__ ->
724    Registers.register List.list) -> (__ -> Registers.register List.list) ->
725    (__ -> Registers.register List.list) -> (__ -> Registers.register
726    List.list) -> (__ -> Registers.register List.list) -> (__ ->
727    Registers.register List.list) -> (__ -> Registers.register List.list) ->
728    (__ -> Registers.register List.list) -> (__ -> Registers.register
729    List.list) -> __ -> 'a1) -> 'a1 **)
730let get_pseudo_reg_functs_inv_rect_Type4 x1 hterm h1 =
731  let hcut = get_pseudo_reg_functs_rect_Type4 x1 h1 hterm in hcut __
732
733(** val get_pseudo_reg_functs_inv_rect_Type3 :
734    unserialized_params -> get_pseudo_reg_functs -> ((__ ->
735    Registers.register List.list) -> (__ -> Registers.register List.list) ->
736    (__ -> Registers.register List.list) -> (__ -> Registers.register
737    List.list) -> (__ -> Registers.register List.list) -> (__ ->
738    Registers.register List.list) -> (__ -> Registers.register List.list) ->
739    (__ -> Registers.register List.list) -> (__ -> Registers.register
740    List.list) -> (__ -> Registers.register List.list) -> (__ ->
741    Registers.register List.list) -> (__ -> Registers.register List.list) ->
742    (__ -> Registers.register List.list) -> (__ -> Registers.register
743    List.list) -> __ -> 'a1) -> 'a1 **)
744let get_pseudo_reg_functs_inv_rect_Type3 x1 hterm h1 =
745  let hcut = get_pseudo_reg_functs_rect_Type3 x1 h1 hterm in hcut __
746
747(** val get_pseudo_reg_functs_inv_rect_Type2 :
748    unserialized_params -> get_pseudo_reg_functs -> ((__ ->
749    Registers.register List.list) -> (__ -> Registers.register List.list) ->
750    (__ -> Registers.register List.list) -> (__ -> Registers.register
751    List.list) -> (__ -> Registers.register List.list) -> (__ ->
752    Registers.register List.list) -> (__ -> Registers.register List.list) ->
753    (__ -> Registers.register List.list) -> (__ -> Registers.register
754    List.list) -> (__ -> Registers.register List.list) -> (__ ->
755    Registers.register List.list) -> (__ -> Registers.register List.list) ->
756    (__ -> Registers.register List.list) -> (__ -> Registers.register
757    List.list) -> __ -> 'a1) -> 'a1 **)
758let get_pseudo_reg_functs_inv_rect_Type2 x1 hterm h1 =
759  let hcut = get_pseudo_reg_functs_rect_Type2 x1 h1 hterm in hcut __
760
761(** val get_pseudo_reg_functs_inv_rect_Type1 :
762    unserialized_params -> get_pseudo_reg_functs -> ((__ ->
763    Registers.register List.list) -> (__ -> Registers.register List.list) ->
764    (__ -> Registers.register List.list) -> (__ -> Registers.register
765    List.list) -> (__ -> Registers.register List.list) -> (__ ->
766    Registers.register List.list) -> (__ -> Registers.register List.list) ->
767    (__ -> Registers.register List.list) -> (__ -> Registers.register
768    List.list) -> (__ -> Registers.register List.list) -> (__ ->
769    Registers.register List.list) -> (__ -> Registers.register List.list) ->
770    (__ -> Registers.register List.list) -> (__ -> Registers.register
771    List.list) -> __ -> 'a1) -> 'a1 **)
772let get_pseudo_reg_functs_inv_rect_Type1 x1 hterm h1 =
773  let hcut = get_pseudo_reg_functs_rect_Type1 x1 h1 hterm in hcut __
774
775(** val get_pseudo_reg_functs_inv_rect_Type0 :
776    unserialized_params -> get_pseudo_reg_functs -> ((__ ->
777    Registers.register List.list) -> (__ -> Registers.register List.list) ->
778    (__ -> Registers.register List.list) -> (__ -> Registers.register
779    List.list) -> (__ -> Registers.register List.list) -> (__ ->
780    Registers.register List.list) -> (__ -> Registers.register List.list) ->
781    (__ -> Registers.register List.list) -> (__ -> Registers.register
782    List.list) -> (__ -> Registers.register List.list) -> (__ ->
783    Registers.register List.list) -> (__ -> Registers.register List.list) ->
784    (__ -> Registers.register List.list) -> (__ -> Registers.register
785    List.list) -> __ -> 'a1) -> 'a1 **)
786let get_pseudo_reg_functs_inv_rect_Type0 x1 hterm h1 =
787  let hcut = get_pseudo_reg_functs_rect_Type0 x1 h1 hterm in hcut __
788
789(** val get_pseudo_reg_functs_jmdiscr :
790    unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs ->
791    __ **)
792let get_pseudo_reg_functs_jmdiscr a1 x y =
793  Logic.eq_rect_Type2 x
794    (let { acc_a_regs = a0; acc_b_regs = a10; acc_a_args = a2; acc_b_args =
795       a3; dpl_regs = a4; dph_regs = a5; dpl_args = a6; dph_args = a7;
796       snd_args = a8; pair_move_regs = a9; f_call_args = a100; f_call_dest =
797       a11; ext_seq_regs = a12; params_regs = a13 } = x
798     in
799    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
800
801type uns_params = { u_pars : unserialized_params;
802                    functs : get_pseudo_reg_functs }
803
804(** val uns_params_rect_Type4 :
805    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
806    'a1 **)
807let rec uns_params_rect_Type4 h_mk_uns_params x_3881 =
808  let { u_pars = u_pars0; functs = functs0 } = x_3881 in
809  h_mk_uns_params u_pars0 functs0
810
811(** val uns_params_rect_Type5 :
812    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
813    'a1 **)
814let rec uns_params_rect_Type5 h_mk_uns_params x_3883 =
815  let { u_pars = u_pars0; functs = functs0 } = x_3883 in
816  h_mk_uns_params u_pars0 functs0
817
818(** val uns_params_rect_Type3 :
819    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
820    'a1 **)
821let rec uns_params_rect_Type3 h_mk_uns_params x_3885 =
822  let { u_pars = u_pars0; functs = functs0 } = x_3885 in
823  h_mk_uns_params u_pars0 functs0
824
825(** val uns_params_rect_Type2 :
826    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
827    'a1 **)
828let rec uns_params_rect_Type2 h_mk_uns_params x_3887 =
829  let { u_pars = u_pars0; functs = functs0 } = x_3887 in
830  h_mk_uns_params u_pars0 functs0
831
832(** val uns_params_rect_Type1 :
833    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
834    'a1 **)
835let rec uns_params_rect_Type1 h_mk_uns_params x_3889 =
836  let { u_pars = u_pars0; functs = functs0 } = x_3889 in
837  h_mk_uns_params u_pars0 functs0
838
839(** val uns_params_rect_Type0 :
840    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
841    'a1 **)
842let rec uns_params_rect_Type0 h_mk_uns_params x_3891 =
843  let { u_pars = u_pars0; functs = functs0 } = x_3891 in
844  h_mk_uns_params u_pars0 functs0
845
846(** val u_pars : uns_params -> unserialized_params **)
847let rec u_pars xxx =
848  xxx.u_pars
849
850(** val functs : uns_params -> get_pseudo_reg_functs **)
851let rec functs xxx =
852  xxx.functs
853
854(** val uns_params_inv_rect_Type4 :
855    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
856    -> 'a1 **)
857let uns_params_inv_rect_Type4 hterm h1 =
858  let hcut = uns_params_rect_Type4 h1 hterm in hcut __
859
860(** val uns_params_inv_rect_Type3 :
861    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
862    -> 'a1 **)
863let uns_params_inv_rect_Type3 hterm h1 =
864  let hcut = uns_params_rect_Type3 h1 hterm in hcut __
865
866(** val uns_params_inv_rect_Type2 :
867    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
868    -> 'a1 **)
869let uns_params_inv_rect_Type2 hterm h1 =
870  let hcut = uns_params_rect_Type2 h1 hterm in hcut __
871
872(** val uns_params_inv_rect_Type1 :
873    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
874    -> 'a1 **)
875let uns_params_inv_rect_Type1 hterm h1 =
876  let hcut = uns_params_rect_Type1 h1 hterm in hcut __
877
878(** val uns_params_inv_rect_Type0 :
879    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
880    -> 'a1 **)
881let uns_params_inv_rect_Type0 hterm h1 =
882  let hcut = uns_params_rect_Type0 h1 hterm in hcut __
883
884(** val uns_params_jmdiscr : uns_params -> uns_params -> __ **)
885let uns_params_jmdiscr x y =
886  Logic.eq_rect_Type2 x
887    (let { u_pars = a0; functs = a1 } = x in
888    Obj.magic (fun _ dH -> dH __ __)) y
889
890type joint_seq =
891| COMMENT of String.string
892| MOVE of __
893| POP of __
894| PUSH of __
895| ADDRESS of AST.ident * __ * __
896| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
897| OP1 of BackEndOps.op1 * __ * __
898| OP2 of BackEndOps.op2 * __ * __ * __
899| CLEAR_CARRY
900| SET_CARRY
901| LOAD of __ * __ * __
902| STORE of __ * __ * __
903| Extension_seq of __
904
905(** val joint_seq_rect_Type4 :
906    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
907    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
908    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
909    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
910    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
911    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
912let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
913| COMMENT x_3946 -> h_COMMENT x_3946
914| MOVE x_3947 -> h_MOVE x_3947
915| POP x_3948 -> h_POP x_3948
916| PUSH x_3949 -> h_PUSH x_3949
917| ADDRESS (i, x_3951, x_3950) -> h_ADDRESS i __ x_3951 x_3950
918| OPACCS (x_3957, x_3956, x_3955, x_3954, x_3953) ->
919  h_OPACCS x_3957 x_3956 x_3955 x_3954 x_3953
920| OP1 (x_3960, x_3959, x_3958) -> h_OP1 x_3960 x_3959 x_3958
921| OP2 (x_3964, x_3963, x_3962, x_3961) -> h_OP2 x_3964 x_3963 x_3962 x_3961
922| CLEAR_CARRY -> h_CLEAR_CARRY
923| SET_CARRY -> h_SET_CARRY
924| LOAD (x_3967, x_3966, x_3965) -> h_LOAD x_3967 x_3966 x_3965
925| STORE (x_3970, x_3969, x_3968) -> h_STORE x_3970 x_3969 x_3968
926| Extension_seq x_3971 -> h_extension_seq x_3971
927
928(** val joint_seq_rect_Type5 :
929    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
930    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
931    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
932    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
933    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
934    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
935let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
936| COMMENT x_3986 -> h_COMMENT x_3986
937| MOVE x_3987 -> h_MOVE x_3987
938| POP x_3988 -> h_POP x_3988
939| PUSH x_3989 -> h_PUSH x_3989
940| ADDRESS (i, x_3991, x_3990) -> h_ADDRESS i __ x_3991 x_3990
941| OPACCS (x_3997, x_3996, x_3995, x_3994, x_3993) ->
942  h_OPACCS x_3997 x_3996 x_3995 x_3994 x_3993
943| OP1 (x_4000, x_3999, x_3998) -> h_OP1 x_4000 x_3999 x_3998
944| OP2 (x_4004, x_4003, x_4002, x_4001) -> h_OP2 x_4004 x_4003 x_4002 x_4001
945| CLEAR_CARRY -> h_CLEAR_CARRY
946| SET_CARRY -> h_SET_CARRY
947| LOAD (x_4007, x_4006, x_4005) -> h_LOAD x_4007 x_4006 x_4005
948| STORE (x_4010, x_4009, x_4008) -> h_STORE x_4010 x_4009 x_4008
949| Extension_seq x_4011 -> h_extension_seq x_4011
950
951(** val joint_seq_rect_Type3 :
952    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
953    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
954    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
955    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
956    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
957    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
958let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
959| COMMENT x_4026 -> h_COMMENT x_4026
960| MOVE x_4027 -> h_MOVE x_4027
961| POP x_4028 -> h_POP x_4028
962| PUSH x_4029 -> h_PUSH x_4029
963| ADDRESS (i, x_4031, x_4030) -> h_ADDRESS i __ x_4031 x_4030
964| OPACCS (x_4037, x_4036, x_4035, x_4034, x_4033) ->
965  h_OPACCS x_4037 x_4036 x_4035 x_4034 x_4033
966| OP1 (x_4040, x_4039, x_4038) -> h_OP1 x_4040 x_4039 x_4038
967| OP2 (x_4044, x_4043, x_4042, x_4041) -> h_OP2 x_4044 x_4043 x_4042 x_4041
968| CLEAR_CARRY -> h_CLEAR_CARRY
969| SET_CARRY -> h_SET_CARRY
970| LOAD (x_4047, x_4046, x_4045) -> h_LOAD x_4047 x_4046 x_4045
971| STORE (x_4050, x_4049, x_4048) -> h_STORE x_4050 x_4049 x_4048
972| Extension_seq x_4051 -> h_extension_seq x_4051
973
974(** val joint_seq_rect_Type2 :
975    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
976    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
977    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
978    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
979    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
980    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
981let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
982| COMMENT x_4066 -> h_COMMENT x_4066
983| MOVE x_4067 -> h_MOVE x_4067
984| POP x_4068 -> h_POP x_4068
985| PUSH x_4069 -> h_PUSH x_4069
986| ADDRESS (i, x_4071, x_4070) -> h_ADDRESS i __ x_4071 x_4070
987| OPACCS (x_4077, x_4076, x_4075, x_4074, x_4073) ->
988  h_OPACCS x_4077 x_4076 x_4075 x_4074 x_4073
989| OP1 (x_4080, x_4079, x_4078) -> h_OP1 x_4080 x_4079 x_4078
990| OP2 (x_4084, x_4083, x_4082, x_4081) -> h_OP2 x_4084 x_4083 x_4082 x_4081
991| CLEAR_CARRY -> h_CLEAR_CARRY
992| SET_CARRY -> h_SET_CARRY
993| LOAD (x_4087, x_4086, x_4085) -> h_LOAD x_4087 x_4086 x_4085
994| STORE (x_4090, x_4089, x_4088) -> h_STORE x_4090 x_4089 x_4088
995| Extension_seq x_4091 -> h_extension_seq x_4091
996
997(** val joint_seq_rect_Type1 :
998    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
999    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1000    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1001    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1002    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1003    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1004let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
1005| COMMENT x_4106 -> h_COMMENT x_4106
1006| MOVE x_4107 -> h_MOVE x_4107
1007| POP x_4108 -> h_POP x_4108
1008| PUSH x_4109 -> h_PUSH x_4109
1009| ADDRESS (i, x_4111, x_4110) -> h_ADDRESS i __ x_4111 x_4110
1010| OPACCS (x_4117, x_4116, x_4115, x_4114, x_4113) ->
1011  h_OPACCS x_4117 x_4116 x_4115 x_4114 x_4113
1012| OP1 (x_4120, x_4119, x_4118) -> h_OP1 x_4120 x_4119 x_4118
1013| OP2 (x_4124, x_4123, x_4122, x_4121) -> h_OP2 x_4124 x_4123 x_4122 x_4121
1014| CLEAR_CARRY -> h_CLEAR_CARRY
1015| SET_CARRY -> h_SET_CARRY
1016| LOAD (x_4127, x_4126, x_4125) -> h_LOAD x_4127 x_4126 x_4125
1017| STORE (x_4130, x_4129, x_4128) -> h_STORE x_4130 x_4129 x_4128
1018| Extension_seq x_4131 -> h_extension_seq x_4131
1019
1020(** val joint_seq_rect_Type0 :
1021    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1022    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1023    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1024    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1025    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1026    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1027let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
1028| COMMENT x_4146 -> h_COMMENT x_4146
1029| MOVE x_4147 -> h_MOVE x_4147
1030| POP x_4148 -> h_POP x_4148
1031| PUSH x_4149 -> h_PUSH x_4149
1032| ADDRESS (i, x_4151, x_4150) -> h_ADDRESS i __ x_4151 x_4150
1033| OPACCS (x_4157, x_4156, x_4155, x_4154, x_4153) ->
1034  h_OPACCS x_4157 x_4156 x_4155 x_4154 x_4153
1035| OP1 (x_4160, x_4159, x_4158) -> h_OP1 x_4160 x_4159 x_4158
1036| OP2 (x_4164, x_4163, x_4162, x_4161) -> h_OP2 x_4164 x_4163 x_4162 x_4161
1037| CLEAR_CARRY -> h_CLEAR_CARRY
1038| SET_CARRY -> h_SET_CARRY
1039| LOAD (x_4167, x_4166, x_4165) -> h_LOAD x_4167 x_4166 x_4165
1040| STORE (x_4170, x_4169, x_4168) -> h_STORE x_4170 x_4169 x_4168
1041| Extension_seq x_4171 -> h_extension_seq x_4171
1042
1043(** val joint_seq_inv_rect_Type4 :
1044    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1045    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1046    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1047    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1048    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1049    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1050    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1051let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1052  let hcut =
1053    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1054      hterm
1055  in
1056  hcut __
1057
1058(** val joint_seq_inv_rect_Type3 :
1059    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1060    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1061    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1062    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1063    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1064    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1065    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1066let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1067  let hcut =
1068    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1069      hterm
1070  in
1071  hcut __
1072
1073(** val joint_seq_inv_rect_Type2 :
1074    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1075    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1076    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1077    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1078    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1079    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1080    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1081let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1082  let hcut =
1083    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1084      hterm
1085  in
1086  hcut __
1087
1088(** val joint_seq_inv_rect_Type1 :
1089    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1090    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1091    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1092    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1093    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1094    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1095    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1096let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1097  let hcut =
1098    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1099      hterm
1100  in
1101  hcut __
1102
1103(** val joint_seq_inv_rect_Type0 :
1104    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1105    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1106    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1107    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1108    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1109    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1110    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1111let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1112  let hcut =
1113    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1114      hterm
1115  in
1116  hcut __
1117
1118(** val joint_seq_discr :
1119    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1120    __ **)
1121let joint_seq_discr a1 a2 x y =
1122  Logic.eq_rect_Type2 x
1123    (match x with
1124     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1125     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1126     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1127     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1128     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1129     | OPACCS (a0, a10, a20, a3, a4) ->
1130       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1131     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1132     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1133     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1134     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1135     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1136     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1137     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1138
1139(** val joint_seq_jmdiscr :
1140    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1141    __ **)
1142let joint_seq_jmdiscr a1 a2 x y =
1143  Logic.eq_rect_Type2 x
1144    (match x with
1145     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1146     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1147     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1148     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1149     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1150     | OPACCS (a0, a10, a20, a3, a4) ->
1151       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1152     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1153     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1154     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1155     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1156     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1157     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1158     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1159
1160(** val get_used_registers_from_seq :
1161    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1162    joint_seq -> Registers.register List.list **)
1163let get_used_registers_from_seq p globals functs0 = function
1164| COMMENT x -> List.Nil
1165| MOVE pm -> functs0.pair_move_regs pm
1166| POP r -> functs0.acc_a_regs r
1167| PUSH r -> functs0.acc_a_args r
1168| ADDRESS (i, r1, r2) ->
1169  List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1170| OPACCS (o, r1, r2, r3, r4) ->
1171  List.append (functs0.acc_a_regs r1)
1172    (List.append (functs0.acc_b_regs r2)
1173      (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1174| OP1 (o, r1, r2) ->
1175  List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1176| OP2 (o, r1, r2, r3) ->
1177  List.append (functs0.acc_a_regs r1)
1178    (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1179| CLEAR_CARRY -> List.Nil
1180| SET_CARRY -> List.Nil
1181| LOAD (r1, r2, r3) ->
1182  List.append (functs0.acc_a_regs r1)
1183    (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1184| STORE (r1, r2, r3) ->
1185  List.append (functs0.dpl_args r1)
1186    (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1187| Extension_seq ext -> functs0.ext_seq_regs ext
1188
1189(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1190let nOOP p globals =
1191  COMMENT String.EmptyString
1192
1193(** val dpi1__o__extension_seq_to_seq__o__inject :
1194    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1195    joint_seq Types.sig0 **)
1196let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1197  Extension_seq x4.Types.dpi1
1198
1199(** val eject__o__extension_seq_to_seq__o__inject :
1200    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1201    Types.sig0 **)
1202let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1203  Extension_seq (Types.pi1 x4)
1204
1205(** val extension_seq_to_seq__o__inject :
1206    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1207let extension_seq_to_seq__o__inject x0 x1 x3 =
1208  Extension_seq x3
1209
1210(** val dpi1__o__extension_seq_to_seq :
1211    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1212    joint_seq **)
1213let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1214  Extension_seq x3.Types.dpi1
1215
1216(** val eject__o__extension_seq_to_seq :
1217    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1218let eject__o__extension_seq_to_seq x0 x1 x3 =
1219  Extension_seq (Types.pi1 x3)
1220
1221type joint_step =
1222| COST_LABEL of CostLabel.costlabel
1223| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1224| COND of __ * Graphs.label
1225| Step_seq of joint_seq
1226
1227(** val joint_step_rect_Type4 :
1228    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1229    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1230    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1231let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1232| COST_LABEL x_4438 -> h_COST_LABEL x_4438
1233| CALL (x_4441, x_4440, x_4439) -> h_CALL x_4441 x_4440 x_4439
1234| COND (x_4443, x_4442) -> h_COND x_4443 x_4442
1235| Step_seq x_4444 -> h_step_seq x_4444
1236
1237(** val joint_step_rect_Type5 :
1238    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1239    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1240    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1241let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1242| COST_LABEL x_4450 -> h_COST_LABEL x_4450
1243| CALL (x_4453, x_4452, x_4451) -> h_CALL x_4453 x_4452 x_4451
1244| COND (x_4455, x_4454) -> h_COND x_4455 x_4454
1245| Step_seq x_4456 -> h_step_seq x_4456
1246
1247(** val joint_step_rect_Type3 :
1248    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1249    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1250    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1251let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1252| COST_LABEL x_4462 -> h_COST_LABEL x_4462
1253| CALL (x_4465, x_4464, x_4463) -> h_CALL x_4465 x_4464 x_4463
1254| COND (x_4467, x_4466) -> h_COND x_4467 x_4466
1255| Step_seq x_4468 -> h_step_seq x_4468
1256
1257(** val joint_step_rect_Type2 :
1258    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1259    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1260    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1261let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1262| COST_LABEL x_4474 -> h_COST_LABEL x_4474
1263| CALL (x_4477, x_4476, x_4475) -> h_CALL x_4477 x_4476 x_4475
1264| COND (x_4479, x_4478) -> h_COND x_4479 x_4478
1265| Step_seq x_4480 -> h_step_seq x_4480
1266
1267(** val joint_step_rect_Type1 :
1268    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1269    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1270    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1271let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1272| COST_LABEL x_4486 -> h_COST_LABEL x_4486
1273| CALL (x_4489, x_4488, x_4487) -> h_CALL x_4489 x_4488 x_4487
1274| COND (x_4491, x_4490) -> h_COND x_4491 x_4490
1275| Step_seq x_4492 -> h_step_seq x_4492
1276
1277(** val joint_step_rect_Type0 :
1278    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1279    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1280    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1281let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1282| COST_LABEL x_4498 -> h_COST_LABEL x_4498
1283| CALL (x_4501, x_4500, x_4499) -> h_CALL x_4501 x_4500 x_4499
1284| COND (x_4503, x_4502) -> h_COND x_4503 x_4502
1285| Step_seq x_4504 -> h_step_seq x_4504
1286
1287(** val joint_step_inv_rect_Type4 :
1288    unserialized_params -> AST.ident List.list -> joint_step ->
1289    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1290    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1291    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1292let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1293  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1294
1295(** val joint_step_inv_rect_Type3 :
1296    unserialized_params -> AST.ident List.list -> joint_step ->
1297    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1298    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1299    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1300let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1301  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1302
1303(** val joint_step_inv_rect_Type2 :
1304    unserialized_params -> AST.ident List.list -> joint_step ->
1305    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1306    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1307    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1308let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1309  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1310
1311(** val joint_step_inv_rect_Type1 :
1312    unserialized_params -> AST.ident List.list -> joint_step ->
1313    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1314    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1315    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1316let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1317  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1318
1319(** val joint_step_inv_rect_Type0 :
1320    unserialized_params -> AST.ident List.list -> joint_step ->
1321    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1322    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1323    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1324let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1325  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1326
1327(** val joint_step_discr :
1328    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1329    __ **)
1330let joint_step_discr a1 a2 x y =
1331  Logic.eq_rect_Type2 x
1332    (match x with
1333     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1334     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1335     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1336     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1337
1338(** val joint_step_jmdiscr :
1339    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1340    __ **)
1341let joint_step_jmdiscr a1 a2 x y =
1342  Logic.eq_rect_Type2 x
1343    (match x with
1344     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1345     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1346     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1347     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1348
1349(** val get_used_registers_from_step :
1350    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1351    joint_step -> Registers.register List.list **)
1352let get_used_registers_from_step p globals functs0 = function
1353| COST_LABEL c -> List.Nil
1354| CALL (id, args, dest) ->
1355  let r_id =
1356    match id with
1357    | Types.Inl x -> List.Nil
1358    | Types.Inr ptr ->
1359      List.append (functs0.dpl_args ptr.Types.fst)
1360        (functs0.dph_args ptr.Types.snd)
1361  in
1362  List.append r_id
1363    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1364| COND (r, lbl) -> functs0.acc_a_regs r
1365| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1366
1367(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1368    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1369    joint_step Types.sig0 **)
1370let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1371  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1372
1373(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1374    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1375    Types.sig0 **)
1376let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1377  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1378
1379(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1380    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1381let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1382  Step_seq (Extension_seq x2)
1383
1384(** val dpi1__o__seq_to_step__o__inject :
1385    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1386    Types.dPair -> joint_step Types.sig0 **)
1387let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1388  Step_seq x4.Types.dpi1
1389
1390(** val eject__o__seq_to_step__o__inject :
1391    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1392    joint_step Types.sig0 **)
1393let eject__o__seq_to_step__o__inject x0 x1 x4 =
1394  Step_seq (Types.pi1 x4)
1395
1396(** val seq_to_step__o__inject :
1397    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1398    Types.sig0 **)
1399let seq_to_step__o__inject x0 x1 x3 =
1400  Step_seq x3
1401
1402(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1403    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1404    joint_step **)
1405let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1406  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1407
1408(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1409    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1410let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1411  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1412
1413(** val extension_seq_to_seq__o__seq_to_step :
1414    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1415let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1416  Step_seq (Extension_seq x2)
1417
1418(** val dpi1__o__seq_to_step :
1419    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1420    Types.dPair -> joint_step **)
1421let dpi1__o__seq_to_step x0 x1 x3 =
1422  Step_seq x3.Types.dpi1
1423
1424(** val eject__o__seq_to_step :
1425    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1426    joint_step **)
1427let eject__o__seq_to_step x0 x1 x3 =
1428  Step_seq (Types.pi1 x3)
1429
1430(** val step_labels :
1431    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1432    List.list **)
1433let step_labels p globals = function
1434| COST_LABEL x -> List.Nil
1435| CALL (x, x0, x1) -> List.Nil
1436| COND (x, l) -> List.Cons (l, List.Nil)
1437| Step_seq s0 ->
1438  (match s0 with
1439   | COMMENT x -> List.Nil
1440   | MOVE x -> List.Nil
1441   | POP x -> List.Nil
1442   | PUSH x -> List.Nil
1443   | ADDRESS (x, x1, x2) -> List.Nil
1444   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1445   | OP1 (x, x0, x1) -> List.Nil
1446   | OP2 (x, x0, x1, x2) -> List.Nil
1447   | CLEAR_CARRY -> List.Nil
1448   | SET_CARRY -> List.Nil
1449   | LOAD (x, x0, x1) -> List.Nil
1450   | STORE (x, x0, x1) -> List.Nil
1451   | Extension_seq ext -> p.ext_seq_labels ext)
1452
1453type stmt_params = { uns_pars : uns_params;
1454                     succ_label : (__ -> Graphs.label Types.option);
1455                     has_fcond : Bool.bool }
1456
1457(** val stmt_params_rect_Type4 :
1458    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1459    'a1) -> stmt_params -> 'a1 **)
1460let rec stmt_params_rect_Type4 h_mk_stmt_params x_4583 =
1461  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1462    has_fcond0 } = x_4583
1463  in
1464  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1465
1466(** val stmt_params_rect_Type5 :
1467    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1468    'a1) -> stmt_params -> 'a1 **)
1469let rec stmt_params_rect_Type5 h_mk_stmt_params x_4585 =
1470  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1471    has_fcond0 } = x_4585
1472  in
1473  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1474
1475(** val stmt_params_rect_Type3 :
1476    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1477    'a1) -> stmt_params -> 'a1 **)
1478let rec stmt_params_rect_Type3 h_mk_stmt_params x_4587 =
1479  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1480    has_fcond0 } = x_4587
1481  in
1482  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1483
1484(** val stmt_params_rect_Type2 :
1485    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1486    'a1) -> stmt_params -> 'a1 **)
1487let rec stmt_params_rect_Type2 h_mk_stmt_params x_4589 =
1488  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1489    has_fcond0 } = x_4589
1490  in
1491  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1492
1493(** val stmt_params_rect_Type1 :
1494    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1495    'a1) -> stmt_params -> 'a1 **)
1496let rec stmt_params_rect_Type1 h_mk_stmt_params x_4591 =
1497  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1498    has_fcond0 } = x_4591
1499  in
1500  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1501
1502(** val stmt_params_rect_Type0 :
1503    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1504    'a1) -> stmt_params -> 'a1 **)
1505let rec stmt_params_rect_Type0 h_mk_stmt_params x_4593 =
1506  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1507    has_fcond0 } = x_4593
1508  in
1509  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1510
1511(** val uns_pars : stmt_params -> uns_params **)
1512let rec uns_pars xxx =
1513  xxx.uns_pars
1514
1515type succ = __
1516
1517(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1518let rec succ_label xxx =
1519  xxx.succ_label
1520
1521(** val has_fcond : stmt_params -> Bool.bool **)
1522let rec has_fcond xxx =
1523  xxx.has_fcond
1524
1525(** val stmt_params_inv_rect_Type4 :
1526    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1527    Bool.bool -> __ -> 'a1) -> 'a1 **)
1528let stmt_params_inv_rect_Type4 hterm h1 =
1529  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1530
1531(** val stmt_params_inv_rect_Type3 :
1532    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1533    Bool.bool -> __ -> 'a1) -> 'a1 **)
1534let stmt_params_inv_rect_Type3 hterm h1 =
1535  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1536
1537(** val stmt_params_inv_rect_Type2 :
1538    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539    Bool.bool -> __ -> 'a1) -> 'a1 **)
1540let stmt_params_inv_rect_Type2 hterm h1 =
1541  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1542
1543(** val stmt_params_inv_rect_Type1 :
1544    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545    Bool.bool -> __ -> 'a1) -> 'a1 **)
1546let stmt_params_inv_rect_Type1 hterm h1 =
1547  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1548
1549(** val stmt_params_inv_rect_Type0 :
1550    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551    Bool.bool -> __ -> 'a1) -> 'a1 **)
1552let stmt_params_inv_rect_Type0 hterm h1 =
1553  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1554
1555(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1556let stmt_params_jmdiscr x y =
1557  Logic.eq_rect_Type2 x
1558    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1559    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1560
1561(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1562let uns_pars__o__u_pars x0 =
1563  x0.uns_pars.u_pars
1564
1565type joint_fin_step =
1566| GOTO of Graphs.label
1567| RETURN
1568| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1569
1570(** val joint_fin_step_rect_Type4 :
1571    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1572    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1573let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1574| GOTO x_4617 -> h_GOTO x_4617
1575| RETURN -> h_RETURN
1576| TAILCALL (x_4619, x_4618) -> h_TAILCALL __ x_4619 x_4618
1577
1578(** val joint_fin_step_rect_Type5 :
1579    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1580    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1581let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1582| GOTO x_4625 -> h_GOTO x_4625
1583| RETURN -> h_RETURN
1584| TAILCALL (x_4627, x_4626) -> h_TAILCALL __ x_4627 x_4626
1585
1586(** val joint_fin_step_rect_Type3 :
1587    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1588    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1589let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1590| GOTO x_4633 -> h_GOTO x_4633
1591| RETURN -> h_RETURN
1592| TAILCALL (x_4635, x_4634) -> h_TAILCALL __ x_4635 x_4634
1593
1594(** val joint_fin_step_rect_Type2 :
1595    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1596    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1597let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1598| GOTO x_4641 -> h_GOTO x_4641
1599| RETURN -> h_RETURN
1600| TAILCALL (x_4643, x_4642) -> h_TAILCALL __ x_4643 x_4642
1601
1602(** val joint_fin_step_rect_Type1 :
1603    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1604    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1605let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1606| GOTO x_4649 -> h_GOTO x_4649
1607| RETURN -> h_RETURN
1608| TAILCALL (x_4651, x_4650) -> h_TAILCALL __ x_4651 x_4650
1609
1610(** val joint_fin_step_rect_Type0 :
1611    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1612    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1613let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1614| GOTO x_4657 -> h_GOTO x_4657
1615| RETURN -> h_RETURN
1616| TAILCALL (x_4659, x_4658) -> h_TAILCALL __ x_4659 x_4658
1617
1618(** val joint_fin_step_inv_rect_Type4 :
1619    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1620    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1621    __ -> 'a1) -> 'a1 **)
1622let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1623  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1624
1625(** val joint_fin_step_inv_rect_Type3 :
1626    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1627    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1628    __ -> 'a1) -> 'a1 **)
1629let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1630  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1631
1632(** val joint_fin_step_inv_rect_Type2 :
1633    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1634    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1635    __ -> 'a1) -> 'a1 **)
1636let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1637  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1638
1639(** val joint_fin_step_inv_rect_Type1 :
1640    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1641    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1642    __ -> 'a1) -> 'a1 **)
1643let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1644  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1645
1646(** val joint_fin_step_inv_rect_Type0 :
1647    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1648    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1649    __ -> 'a1) -> 'a1 **)
1650let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1651  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1652
1653(** val joint_fin_step_discr :
1654    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1655let joint_fin_step_discr a1 x y =
1656  Logic.eq_rect_Type2 x
1657    (match x with
1658     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1659     | RETURN -> Obj.magic (fun _ dH -> dH)
1660     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1661
1662(** val joint_fin_step_jmdiscr :
1663    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1664let joint_fin_step_jmdiscr a1 x y =
1665  Logic.eq_rect_Type2 x
1666    (match x with
1667     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1668     | RETURN -> Obj.magic (fun _ dH -> dH)
1669     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1670
1671(** val fin_step_labels :
1672    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1673let fin_step_labels p = function
1674| GOTO l -> List.Cons (l, List.Nil)
1675| RETURN -> List.Nil
1676| TAILCALL (x0, x1) -> List.Nil
1677
1678type joint_statement =
1679| Sequential of joint_step * __
1680| Final of joint_fin_step
1681| FCOND of __ * Graphs.label * Graphs.label
1682
1683(** val joint_statement_rect_Type4 :
1684    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1685    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1686    'a1) -> joint_statement -> 'a1 **)
1687let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1688| Sequential (x_4725, x_4724) -> h_sequential x_4725 x_4724
1689| Final x_4726 -> h_final x_4726
1690| FCOND (x_4729, x_4728, x_4727) -> h_FCOND __ x_4729 x_4728 x_4727
1691
1692(** val joint_statement_rect_Type5 :
1693    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1694    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1695    'a1) -> joint_statement -> 'a1 **)
1696let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1697| Sequential (x_4736, x_4735) -> h_sequential x_4736 x_4735
1698| Final x_4737 -> h_final x_4737
1699| FCOND (x_4740, x_4739, x_4738) -> h_FCOND __ x_4740 x_4739 x_4738
1700
1701(** val joint_statement_rect_Type3 :
1702    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1703    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1704    'a1) -> joint_statement -> 'a1 **)
1705let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1706| Sequential (x_4747, x_4746) -> h_sequential x_4747 x_4746
1707| Final x_4748 -> h_final x_4748
1708| FCOND (x_4751, x_4750, x_4749) -> h_FCOND __ x_4751 x_4750 x_4749
1709
1710(** val joint_statement_rect_Type2 :
1711    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1712    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1713    'a1) -> joint_statement -> 'a1 **)
1714let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1715| Sequential (x_4758, x_4757) -> h_sequential x_4758 x_4757
1716| Final x_4759 -> h_final x_4759
1717| FCOND (x_4762, x_4761, x_4760) -> h_FCOND __ x_4762 x_4761 x_4760
1718
1719(** val joint_statement_rect_Type1 :
1720    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1721    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1722    'a1) -> joint_statement -> 'a1 **)
1723let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1724| Sequential (x_4769, x_4768) -> h_sequential x_4769 x_4768
1725| Final x_4770 -> h_final x_4770
1726| FCOND (x_4773, x_4772, x_4771) -> h_FCOND __ x_4773 x_4772 x_4771
1727
1728(** val joint_statement_rect_Type0 :
1729    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1730    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1731    'a1) -> joint_statement -> 'a1 **)
1732let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1733| Sequential (x_4780, x_4779) -> h_sequential x_4780 x_4779
1734| Final x_4781 -> h_final x_4781
1735| FCOND (x_4784, x_4783, x_4782) -> h_FCOND __ x_4784 x_4783 x_4782
1736
1737(** val joint_statement_inv_rect_Type4 :
1738    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1739    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1740    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1741let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1742  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1743
1744(** val joint_statement_inv_rect_Type3 :
1745    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1746    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1747    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1748let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1749  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1750
1751(** val joint_statement_inv_rect_Type2 :
1752    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1753    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1754    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1755let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1756  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1757
1758(** val joint_statement_inv_rect_Type1 :
1759    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1760    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1761    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1762let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1763  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1764
1765(** val joint_statement_inv_rect_Type0 :
1766    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1767    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1768    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1769let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1770  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1771
1772(** val joint_statement_discr :
1773    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1774    -> __ **)
1775let joint_statement_discr a1 a2 x y =
1776  Logic.eq_rect_Type2 x
1777    (match x with
1778     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1779     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1780     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1781
1782(** val joint_statement_jmdiscr :
1783    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1784    -> __ **)
1785let joint_statement_jmdiscr a1 a2 x y =
1786  Logic.eq_rect_Type2 x
1787    (match x with
1788     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1789     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1790     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1791
1792(** val dpi1__o__fin_step_to_stmt__o__inject :
1793    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1794    -> joint_statement Types.sig0 **)
1795let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1796  Final x4.Types.dpi1
1797
1798(** val eject__o__fin_step_to_stmt__o__inject :
1799    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1800    joint_statement Types.sig0 **)
1801let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1802  Final (Types.pi1 x4)
1803
1804(** val fin_step_to_stmt__o__inject :
1805    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1806    Types.sig0 **)
1807let fin_step_to_stmt__o__inject x0 x1 x3 =
1808  Final x3
1809
1810(** val dpi1__o__fin_step_to_stmt :
1811    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1812    -> joint_statement **)
1813let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1814  Final x3.Types.dpi1
1815
1816(** val eject__o__fin_step_to_stmt :
1817    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1818    joint_statement **)
1819let eject__o__fin_step_to_stmt x0 x1 x3 =
1820  Final (Types.pi1 x3)
1821
1822type params = { stmt_pars : stmt_params;
1823                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1824                          Types.option);
1825                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1826                                 -> __ Types.option);
1827                point_of_succ : (__ -> __ -> __) }
1828
1829(** val params_rect_Type4 :
1830    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1831    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1832    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1833    'a1 **)
1834let rec params_rect_Type4 h_mk_params x_4857 =
1835  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1836    point_of_label0; point_of_succ = point_of_succ0 } = x_4857
1837  in
1838  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1839
1840(** val params_rect_Type5 :
1841    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1842    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1843    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1844    'a1 **)
1845let rec params_rect_Type5 h_mk_params x_4859 =
1846  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1847    point_of_label0; point_of_succ = point_of_succ0 } = x_4859
1848  in
1849  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1850
1851(** val params_rect_Type3 :
1852    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1853    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1854    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1855    'a1 **)
1856let rec params_rect_Type3 h_mk_params x_4861 =
1857  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1858    point_of_label0; point_of_succ = point_of_succ0 } = x_4861
1859  in
1860  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1861
1862(** val params_rect_Type2 :
1863    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1864    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1865    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1866    'a1 **)
1867let rec params_rect_Type2 h_mk_params x_4863 =
1868  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1869    point_of_label0; point_of_succ = point_of_succ0 } = x_4863
1870  in
1871  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1872
1873(** val params_rect_Type1 :
1874    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1875    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1876    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1877    'a1 **)
1878let rec params_rect_Type1 h_mk_params x_4865 =
1879  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1880    point_of_label0; point_of_succ = point_of_succ0 } = x_4865
1881  in
1882  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1883
1884(** val params_rect_Type0 :
1885    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1886    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1887    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1888    'a1 **)
1889let rec params_rect_Type0 h_mk_params x_4867 =
1890  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1891    point_of_label0; point_of_succ = point_of_succ0 } = x_4867
1892  in
1893  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1894
1895(** val stmt_pars : params -> stmt_params **)
1896let rec stmt_pars xxx =
1897  xxx.stmt_pars
1898
1899type codeT = __
1900
1901type code_point = __
1902
1903(** val stmt_at :
1904    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1905let rec stmt_at xxx =
1906  xxx.stmt_at
1907
1908(** val point_of_label :
1909    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1910let rec point_of_label xxx =
1911  xxx.point_of_label
1912
1913(** val point_of_succ : params -> __ -> __ -> __ **)
1914let rec point_of_succ xxx =
1915  xxx.point_of_succ
1916
1917(** val params_inv_rect_Type4 :
1918    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1919    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1920    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1921let params_inv_rect_Type4 hterm h1 =
1922  let hcut = params_rect_Type4 h1 hterm in hcut __
1923
1924(** val params_inv_rect_Type3 :
1925    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1926    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1927    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1928let params_inv_rect_Type3 hterm h1 =
1929  let hcut = params_rect_Type3 h1 hterm in hcut __
1930
1931(** val params_inv_rect_Type2 :
1932    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1933    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1934    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1935let params_inv_rect_Type2 hterm h1 =
1936  let hcut = params_rect_Type2 h1 hterm in hcut __
1937
1938(** val params_inv_rect_Type1 :
1939    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1940    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1941    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1942let params_inv_rect_Type1 hterm h1 =
1943  let hcut = params_rect_Type1 h1 hterm in hcut __
1944
1945(** val params_inv_rect_Type0 :
1946    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1947    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1948    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1949let params_inv_rect_Type0 hterm h1 =
1950  let hcut = params_rect_Type0 h1 hterm in hcut __
1951
1952(** val params_jmdiscr : params -> params -> __ **)
1953let params_jmdiscr x y =
1954  Logic.eq_rect_Type2 x
1955    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1956       a5 } = x
1957     in
1958    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1959
1960(** val stmt_pars__o__uns_pars : params -> uns_params **)
1961let stmt_pars__o__uns_pars x0 =
1962  x0.stmt_pars.uns_pars
1963
1964(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1965let stmt_pars__o__uns_pars__o__u_pars x0 =
1966  uns_pars__o__u_pars x0.stmt_pars
1967
1968(** val code_has_point :
1969    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1970let code_has_point p globals c pt =
1971  match p.stmt_at globals c pt with
1972  | Types.None -> Bool.False
1973  | Types.Some x -> Bool.True
1974
1975(** val code_has_label :
1976    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1977let code_has_label p globals c l =
1978  match p.point_of_label globals c l with
1979  | Types.None -> Bool.False
1980  | Types.Some pt -> code_has_point p globals c pt
1981
1982(** val stmt_explicit_labels :
1983    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1984    List.list **)
1985let stmt_explicit_labels p globals = function
1986| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1987| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
1988| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1989
1990(** val stmt_implicit_label :
1991    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1992    Types.option **)
1993let stmt_implicit_label p globals = function
1994| Sequential (x, s0) -> p.succ_label s0
1995| Final x -> Types.None
1996| FCOND (x0, x1, x2) -> Types.None
1997
1998(** val stmt_labels :
1999    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2000    List.list **)
2001let stmt_labels p g stmt =
2002  List.append
2003    (match stmt_implicit_label p g stmt with
2004     | Types.None -> List.Nil
2005     | Types.Some l -> List.Cons (l, List.Nil))
2006    (stmt_explicit_labels p g stmt)
2007
2008(** val stmt_registers :
2009    stmt_params -> AST.ident List.list -> joint_statement ->
2010    Registers.register List.list **)
2011let stmt_registers p globals = function
2012| Sequential (c, x) ->
2013  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2014| Final c ->
2015  (match c with
2016   | GOTO x -> List.Nil
2017   | RETURN -> List.Nil
2018   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2019| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2020
2021type lin_params =
2022  uns_params
2023  (* singleton inductive, whose constructor was mk_lin_params *)
2024
2025(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2026let rec lin_params_rect_Type4 h_mk_lin_params x_4890 =
2027  let l_u_pars = x_4890 in h_mk_lin_params l_u_pars
2028
2029(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2030let rec lin_params_rect_Type5 h_mk_lin_params x_4892 =
2031  let l_u_pars = x_4892 in h_mk_lin_params l_u_pars
2032
2033(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2034let rec lin_params_rect_Type3 h_mk_lin_params x_4894 =
2035  let l_u_pars = x_4894 in h_mk_lin_params l_u_pars
2036
2037(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2038let rec lin_params_rect_Type2 h_mk_lin_params x_4896 =
2039  let l_u_pars = x_4896 in h_mk_lin_params l_u_pars
2040
2041(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2042let rec lin_params_rect_Type1 h_mk_lin_params x_4898 =
2043  let l_u_pars = x_4898 in h_mk_lin_params l_u_pars
2044
2045(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2046let rec lin_params_rect_Type0 h_mk_lin_params x_4900 =
2047  let l_u_pars = x_4900 in h_mk_lin_params l_u_pars
2048
2049(** val l_u_pars : lin_params -> uns_params **)
2050let rec l_u_pars xxx =
2051  let yyy = xxx in yyy
2052
2053(** val lin_params_inv_rect_Type4 :
2054    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2055let lin_params_inv_rect_Type4 hterm h1 =
2056  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2057
2058(** val lin_params_inv_rect_Type3 :
2059    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2060let lin_params_inv_rect_Type3 hterm h1 =
2061  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2062
2063(** val lin_params_inv_rect_Type2 :
2064    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2065let lin_params_inv_rect_Type2 hterm h1 =
2066  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2067
2068(** val lin_params_inv_rect_Type1 :
2069    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2070let lin_params_inv_rect_Type1 hterm h1 =
2071  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2072
2073(** val lin_params_inv_rect_Type0 :
2074    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2075let lin_params_inv_rect_Type0 hterm h1 =
2076  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2077
2078(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2079let lin_params_jmdiscr x y =
2080  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2081
2082(** val lin_params_to_params : lin_params -> params **)
2083let lin_params_to_params lp =
2084  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2085    Types.None); has_fcond = Bool.True }; stmt_at =
2086    (fun globals code point ->
2087    Obj.magic
2088      (Monad.m_bind0 (Monad.max_def Option.option)
2089        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2090        (fun ls ->
2091        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2092    point_of_label = (fun globals c lbl ->
2093    Util.if_then_else_safe
2094      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2095        (Obj.magic c)) (fun _ ->
2096      Obj.magic
2097        (Monad.m_return0 (Monad.max_def Option.option)
2098          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2099            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2100    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2101
2102(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2103let lp_to_p__o__stmt_pars x0 =
2104  (lin_params_to_params x0).stmt_pars
2105
2106(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2107let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2108  stmt_pars__o__uns_pars (lin_params_to_params x0)
2109
2110(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2111    lin_params -> unserialized_params **)
2112let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2113  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2114
2115type graph_params =
2116  uns_params
2117  (* singleton inductive, whose constructor was mk_graph_params *)
2118
2119(** val graph_params_rect_Type4 :
2120    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2121let rec graph_params_rect_Type4 h_mk_graph_params x_4916 =
2122  let g_u_pars = x_4916 in h_mk_graph_params g_u_pars
2123
2124(** val graph_params_rect_Type5 :
2125    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2126let rec graph_params_rect_Type5 h_mk_graph_params x_4918 =
2127  let g_u_pars = x_4918 in h_mk_graph_params g_u_pars
2128
2129(** val graph_params_rect_Type3 :
2130    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2131let rec graph_params_rect_Type3 h_mk_graph_params x_4920 =
2132  let g_u_pars = x_4920 in h_mk_graph_params g_u_pars
2133
2134(** val graph_params_rect_Type2 :
2135    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2136let rec graph_params_rect_Type2 h_mk_graph_params x_4922 =
2137  let g_u_pars = x_4922 in h_mk_graph_params g_u_pars
2138
2139(** val graph_params_rect_Type1 :
2140    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2141let rec graph_params_rect_Type1 h_mk_graph_params x_4924 =
2142  let g_u_pars = x_4924 in h_mk_graph_params g_u_pars
2143
2144(** val graph_params_rect_Type0 :
2145    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2146let rec graph_params_rect_Type0 h_mk_graph_params x_4926 =
2147  let g_u_pars = x_4926 in h_mk_graph_params g_u_pars
2148
2149(** val g_u_pars : graph_params -> uns_params **)
2150let rec g_u_pars xxx =
2151  let yyy = xxx in yyy
2152
2153(** val graph_params_inv_rect_Type4 :
2154    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2155let graph_params_inv_rect_Type4 hterm h1 =
2156  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2157
2158(** val graph_params_inv_rect_Type3 :
2159    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2160let graph_params_inv_rect_Type3 hterm h1 =
2161  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2162
2163(** val graph_params_inv_rect_Type2 :
2164    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2165let graph_params_inv_rect_Type2 hterm h1 =
2166  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2167
2168(** val graph_params_inv_rect_Type1 :
2169    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2170let graph_params_inv_rect_Type1 hterm h1 =
2171  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2172
2173(** val graph_params_inv_rect_Type0 :
2174    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2175let graph_params_inv_rect_Type0 hterm h1 =
2176  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2177
2178(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2179let graph_params_jmdiscr x y =
2180  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2181
2182(** val graph_params_to_params : graph_params -> params **)
2183let graph_params_to_params gp =
2184  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2185    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2186    (fun globals code ->
2187    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2188    point_of_label = (fun x x0 lbl ->
2189    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2190    point_of_succ = (fun x lbl -> lbl) }
2191
2192(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2193let gp_to_p__o__stmt_pars x0 =
2194  (graph_params_to_params x0).stmt_pars
2195
2196(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2197let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2198  stmt_pars__o__uns_pars (graph_params_to_params x0)
2199
2200(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2201    graph_params -> unserialized_params **)
2202let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2203  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2204
2205type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2206                                 joint_if_runiverse : Identifiers.universe;
2207                                 joint_if_result : __; joint_if_params : 
2208                                 __; joint_if_stacksize : Nat.nat;
2209                                 joint_if_local_stacksize : Nat.nat;
2210                                 joint_if_code : __; joint_if_entry : 
2211                                 __ }
2212
2213(** val joint_internal_function_rect_Type4 :
2214    params -> AST.ident List.list -> (Identifiers.universe ->
2215    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2216    'a1) -> joint_internal_function -> 'a1 **)
2217let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_4942 =
2218  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2219    joint_if_runiverse0; joint_if_result = joint_if_result0;
2220    joint_if_params = joint_if_params0; joint_if_stacksize =
2221    joint_if_stacksize0; joint_if_local_stacksize =
2222    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2223    joint_if_entry = joint_if_entry0 } = x_4942
2224  in
2225  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2226    joint_if_result0 joint_if_params0 joint_if_stacksize0
2227    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2228
2229(** val joint_internal_function_rect_Type5 :
2230    params -> AST.ident List.list -> (Identifiers.universe ->
2231    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2232    'a1) -> joint_internal_function -> 'a1 **)
2233let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_4944 =
2234  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2235    joint_if_runiverse0; joint_if_result = joint_if_result0;
2236    joint_if_params = joint_if_params0; joint_if_stacksize =
2237    joint_if_stacksize0; joint_if_local_stacksize =
2238    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2239    joint_if_entry = joint_if_entry0 } = x_4944
2240  in
2241  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2242    joint_if_result0 joint_if_params0 joint_if_stacksize0
2243    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2244
2245(** val joint_internal_function_rect_Type3 :
2246    params -> AST.ident List.list -> (Identifiers.universe ->
2247    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2248    'a1) -> joint_internal_function -> 'a1 **)
2249let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_4946 =
2250  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2251    joint_if_runiverse0; joint_if_result = joint_if_result0;
2252    joint_if_params = joint_if_params0; joint_if_stacksize =
2253    joint_if_stacksize0; joint_if_local_stacksize =
2254    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2255    joint_if_entry = joint_if_entry0 } = x_4946
2256  in
2257  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2258    joint_if_result0 joint_if_params0 joint_if_stacksize0
2259    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2260
2261(** val joint_internal_function_rect_Type2 :
2262    params -> AST.ident List.list -> (Identifiers.universe ->
2263    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2264    'a1) -> joint_internal_function -> 'a1 **)
2265let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_4948 =
2266  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2267    joint_if_runiverse0; joint_if_result = joint_if_result0;
2268    joint_if_params = joint_if_params0; joint_if_stacksize =
2269    joint_if_stacksize0; joint_if_local_stacksize =
2270    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2271    joint_if_entry = joint_if_entry0 } = x_4948
2272  in
2273  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2274    joint_if_result0 joint_if_params0 joint_if_stacksize0
2275    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2276
2277(** val joint_internal_function_rect_Type1 :
2278    params -> AST.ident List.list -> (Identifiers.universe ->
2279    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2280    'a1) -> joint_internal_function -> 'a1 **)
2281let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_4950 =
2282  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2283    joint_if_runiverse0; joint_if_result = joint_if_result0;
2284    joint_if_params = joint_if_params0; joint_if_stacksize =
2285    joint_if_stacksize0; joint_if_local_stacksize =
2286    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2287    joint_if_entry = joint_if_entry0 } = x_4950
2288  in
2289  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2290    joint_if_result0 joint_if_params0 joint_if_stacksize0
2291    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2292
2293(** val joint_internal_function_rect_Type0 :
2294    params -> AST.ident List.list -> (Identifiers.universe ->
2295    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2296    'a1) -> joint_internal_function -> 'a1 **)
2297let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_4952 =
2298  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2299    joint_if_runiverse0; joint_if_result = joint_if_result0;
2300    joint_if_params = joint_if_params0; joint_if_stacksize =
2301    joint_if_stacksize0; joint_if_local_stacksize =
2302    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2303    joint_if_entry = joint_if_entry0 } = x_4952
2304  in
2305  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2306    joint_if_result0 joint_if_params0 joint_if_stacksize0
2307    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2308
2309(** val joint_if_luniverse :
2310    params -> AST.ident List.list -> joint_internal_function ->
2311    Identifiers.universe **)
2312let rec joint_if_luniverse p globals xxx =
2313  xxx.joint_if_luniverse
2314
2315(** val joint_if_runiverse :
2316    params -> AST.ident List.list -> joint_internal_function ->
2317    Identifiers.universe **)
2318let rec joint_if_runiverse p globals xxx =
2319  xxx.joint_if_runiverse
2320
2321(** val joint_if_result :
2322    params -> AST.ident List.list -> joint_internal_function -> __ **)
2323let rec joint_if_result p globals xxx =
2324  xxx.joint_if_result
2325
2326(** val joint_if_params :
2327    params -> AST.ident List.list -> joint_internal_function -> __ **)
2328let rec joint_if_params p globals xxx =
2329  xxx.joint_if_params
2330
2331(** val joint_if_stacksize :
2332    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2333let rec joint_if_stacksize p globals xxx =
2334  xxx.joint_if_stacksize
2335
2336(** val joint_if_local_stacksize :
2337    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2338let rec joint_if_local_stacksize p globals xxx =
2339  xxx.joint_if_local_stacksize
2340
2341(** val joint_if_code :
2342    params -> AST.ident List.list -> joint_internal_function -> __ **)
2343let rec joint_if_code p globals xxx =
2344  xxx.joint_if_code
2345
2346(** val joint_if_entry :
2347    params -> AST.ident List.list -> joint_internal_function -> __ **)
2348let rec joint_if_entry p globals xxx =
2349  xxx.joint_if_entry
2350
2351(** val joint_internal_function_inv_rect_Type4 :
2352    params -> AST.ident List.list -> joint_internal_function ->
2353    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2354    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2355let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2356  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2357
2358(** val joint_internal_function_inv_rect_Type3 :
2359    params -> AST.ident List.list -> joint_internal_function ->
2360    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2361    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2362let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2363  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2364
2365(** val joint_internal_function_inv_rect_Type2 :
2366    params -> AST.ident List.list -> joint_internal_function ->
2367    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2368    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2369let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2370  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2371
2372(** val joint_internal_function_inv_rect_Type1 :
2373    params -> AST.ident List.list -> joint_internal_function ->
2374    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2375    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2376let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2377  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2378
2379(** val joint_internal_function_inv_rect_Type0 :
2380    params -> AST.ident List.list -> joint_internal_function ->
2381    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2382    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2383let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2384  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2385
2386(** val joint_internal_function_jmdiscr :
2387    params -> AST.ident List.list -> joint_internal_function ->
2388    joint_internal_function -> __ **)
2389let joint_internal_function_jmdiscr a1 a2 x y =
2390  Logic.eq_rect_Type2 x
2391    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2392       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2393       joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2394       a7 } = x
2395     in
2396    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2397
2398(** val good_if_rect_Type4 :
2399    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2400    __ -> __ -> __ -> 'a1) -> 'a1 **)
2401let rec good_if_rect_Type4 p globals def h_mk_good_if =
2402  h_mk_good_if __ __ __ __ __
2403
2404(** val good_if_rect_Type5 :
2405    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2406    __ -> __ -> __ -> 'a1) -> 'a1 **)
2407let rec good_if_rect_Type5 p globals def h_mk_good_if =
2408  h_mk_good_if __ __ __ __ __
2409
2410(** val good_if_rect_Type3 :
2411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412    __ -> __ -> __ -> 'a1) -> 'a1 **)
2413let rec good_if_rect_Type3 p globals def h_mk_good_if =
2414  h_mk_good_if __ __ __ __ __
2415
2416(** val good_if_rect_Type2 :
2417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418    __ -> __ -> __ -> 'a1) -> 'a1 **)
2419let rec good_if_rect_Type2 p globals def h_mk_good_if =
2420  h_mk_good_if __ __ __ __ __
2421
2422(** val good_if_rect_Type1 :
2423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424    __ -> __ -> __ -> 'a1) -> 'a1 **)
2425let rec good_if_rect_Type1 p globals def h_mk_good_if =
2426  h_mk_good_if __ __ __ __ __
2427
2428(** val good_if_rect_Type0 :
2429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430    __ -> __ -> __ -> 'a1) -> 'a1 **)
2431let rec good_if_rect_Type0 p globals def h_mk_good_if =
2432  h_mk_good_if __ __ __ __ __
2433
2434(** val good_if_inv_rect_Type4 :
2435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2437let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2438  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2439
2440(** val good_if_inv_rect_Type3 :
2441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2443let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2444  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2445
2446(** val good_if_inv_rect_Type2 :
2447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2450  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2451
2452(** val good_if_inv_rect_Type1 :
2453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2456  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2457
2458(** val good_if_inv_rect_Type0 :
2459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2462  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2463
2464(** val good_if_discr :
2465    params -> AST.ident List.list -> joint_internal_function -> __ **)
2466let good_if_discr a1 a2 a3 =
2467  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2468
2469(** val good_if_jmdiscr :
2470    params -> AST.ident List.list -> joint_internal_function -> __ **)
2471let good_if_jmdiscr a1 a2 a3 =
2472  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2473
2474type joint_closed_internal_function = joint_internal_function Types.sig0
2475
2476(** val set_joint_code :
2477    AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2478    joint_internal_function **)
2479let set_joint_code globals pars int_fun graph entry =
2480  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2481    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2482    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2483    int_fun.joint_if_stacksize; joint_if_local_stacksize =
2484    int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2485    entry }
2486
2487(** val set_luniverse :
2488    params -> AST.ident List.list -> joint_internal_function ->
2489    Identifiers.universe -> joint_internal_function **)
2490let set_luniverse globals pars p luniverse =
2491  { joint_if_luniverse = luniverse; joint_if_runiverse =
2492    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2493    joint_if_params = p.joint_if_params; joint_if_stacksize =
2494    p.joint_if_stacksize; joint_if_local_stacksize =
2495    p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2496    joint_if_entry = p.joint_if_entry }
2497
2498(** val set_runiverse :
2499    params -> AST.ident List.list -> joint_internal_function ->
2500    Identifiers.universe -> joint_internal_function **)
2501let set_runiverse globals pars p runiverse =
2502  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2503    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2504    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2505    joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2506    p.joint_if_code; joint_if_entry = p.joint_if_entry }
2507
2508(** val add_graph :
2509    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2510    joint_internal_function -> joint_internal_function **)
2511let add_graph g_pars globals l stmt p =
2512  let code =
2513    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2514      stmt
2515  in
2516  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2517  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2518  joint_if_params = p.joint_if_params; joint_if_stacksize =
2519  p.joint_if_stacksize; joint_if_local_stacksize =
2520  p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2521  joint_if_entry = p.joint_if_entry }
2522
2523type joint_function = joint_closed_internal_function AST.fundef
2524
2525type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
2526                                    AST.program;
2527                       init_cost_label : CostLabel.costlabel }
2528
2529(** val joint_program_rect_Type4 :
2530    params -> ((joint_function, AST.init_data List.list) AST.program ->
2531    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2532let rec joint_program_rect_Type4 p h_mk_joint_program x_4994 =
2533  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2534    x_4994
2535  in
2536  h_mk_joint_program joint_prog0 init_cost_label0
2537
2538(** val joint_program_rect_Type5 :
2539    params -> ((joint_function, AST.init_data List.list) AST.program ->
2540    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2541let rec joint_program_rect_Type5 p h_mk_joint_program x_4996 =
2542  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2543    x_4996
2544  in
2545  h_mk_joint_program joint_prog0 init_cost_label0
2546
2547(** val joint_program_rect_Type3 :
2548    params -> ((joint_function, AST.init_data List.list) AST.program ->
2549    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2550let rec joint_program_rect_Type3 p h_mk_joint_program x_4998 =
2551  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2552    x_4998
2553  in
2554  h_mk_joint_program joint_prog0 init_cost_label0
2555
2556(** val joint_program_rect_Type2 :
2557    params -> ((joint_function, AST.init_data List.list) AST.program ->
2558    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2559let rec joint_program_rect_Type2 p h_mk_joint_program x_5000 =
2560  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2561    x_5000
2562  in
2563  h_mk_joint_program joint_prog0 init_cost_label0
2564
2565(** val joint_program_rect_Type1 :
2566    params -> ((joint_function, AST.init_data List.list) AST.program ->
2567    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2568let rec joint_program_rect_Type1 p h_mk_joint_program x_5002 =
2569  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2570    x_5002
2571  in
2572  h_mk_joint_program joint_prog0 init_cost_label0
2573
2574(** val joint_program_rect_Type0 :
2575    params -> ((joint_function, AST.init_data List.list) AST.program ->
2576    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2577let rec joint_program_rect_Type0 p h_mk_joint_program x_5004 =
2578  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2579    x_5004
2580  in
2581  h_mk_joint_program joint_prog0 init_cost_label0
2582
2583(** val joint_prog :
2584    params -> joint_program -> (joint_function, AST.init_data List.list)
2585    AST.program **)
2586let rec joint_prog p xxx =
2587  xxx.joint_prog
2588
2589(** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2590let rec init_cost_label p xxx =
2591  xxx.init_cost_label
2592
2593(** val joint_program_inv_rect_Type4 :
2594    params -> joint_program -> ((joint_function, AST.init_data List.list)
2595    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2596let joint_program_inv_rect_Type4 x1 hterm h1 =
2597  let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2598
2599(** val joint_program_inv_rect_Type3 :
2600    params -> joint_program -> ((joint_function, AST.init_data List.list)
2601    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2602let joint_program_inv_rect_Type3 x1 hterm h1 =
2603  let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2604
2605(** val joint_program_inv_rect_Type2 :
2606    params -> joint_program -> ((joint_function, AST.init_data List.list)
2607    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2608let joint_program_inv_rect_Type2 x1 hterm h1 =
2609  let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2610
2611(** val joint_program_inv_rect_Type1 :
2612    params -> joint_program -> ((joint_function, AST.init_data List.list)
2613    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2614let joint_program_inv_rect_Type1 x1 hterm h1 =
2615  let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2616
2617(** val joint_program_inv_rect_Type0 :
2618    params -> joint_program -> ((joint_function, AST.init_data List.list)
2619    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2620let joint_program_inv_rect_Type0 x1 hterm h1 =
2621  let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2622
2623(** val joint_program_discr :
2624    params -> joint_program -> joint_program -> __ **)
2625let joint_program_discr a1 x y =
2626  Logic.eq_rect_Type2 x
2627    (let { joint_prog = a0; init_cost_label = a10 } = x in
2628    Obj.magic (fun _ dH -> dH __ __)) y
2629
2630(** val joint_program_jmdiscr :
2631    params -> joint_program -> joint_program -> __ **)
2632let joint_program_jmdiscr a1 x y =
2633  Logic.eq_rect_Type2 x
2634    (let { joint_prog = a0; init_cost_label = a10 } = x in
2635    Obj.magic (fun _ dH -> dH __ __)) y
2636
2637(** val dpi1__o__joint_prog__o__inject :
2638    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2639    AST.init_data List.list) AST.program Types.sig0 **)
2640let dpi1__o__joint_prog__o__inject x0 x3 =
2641  x3.Types.dpi1.joint_prog
2642
2643(** val eject__o__joint_prog__o__inject :
2644    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2645    List.list) AST.program Types.sig0 **)
2646let eject__o__joint_prog__o__inject x0 x3 =
2647  (Types.pi1 x3).joint_prog
2648
2649(** val joint_prog__o__inject :
2650    params -> joint_program -> (joint_function, AST.init_data List.list)
2651    AST.program Types.sig0 **)
2652let joint_prog__o__inject x0 x2 =
2653  x2.joint_prog
2654
2655(** val dpi1__o__joint_prog :
2656    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2657    AST.init_data List.list) AST.program **)
2658let dpi1__o__joint_prog x0 x2 =
2659  x2.Types.dpi1.joint_prog
2660
2661(** val eject__o__joint_prog :
2662    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2663    List.list) AST.program **)
2664let eject__o__joint_prog x0 x2 =
2665  (Types.pi1 x2).joint_prog
2666
2667type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2668
2669(** val stack_cost : params -> joint_program -> stack_cost_model **)
2670let stack_cost p pr =
2671  List.foldr (fun id_fun acc ->
2672    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2673    (match fun0 with
2674     | AST.Internal jif ->
2675       List.Cons ({ Types.fst = id; Types.snd =
2676         (Types.pi1 jif).joint_if_stacksize }, acc)
2677     | AST.External x -> acc)) List.Nil (AST.prog_funct pr.joint_prog)
2678
2679open Extra_bool
2680
2681open Coqlib
2682
2683open Values
2684
2685open FrontEndVal
2686
2687open GenMem
2688
2689open FrontEndMem
2690
2691open Globalenvs
2692
2693(** val globals_stacksize : params -> joint_program -> Nat.nat **)
2694let globals_stacksize pars p =
2695  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2696    Globalenvs.size_init_data_list entry.Types.snd)
2697    (AST.prog_vars p.joint_prog)
2698
Note: See TracBrowser for help on using the repository browser.