source: driver/extracted/joint.ml @ 3106

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

New extraction

File size: 113.2 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_16867 -> h_Reg x_16867
113| Imm x_16868 -> h_Imm x_16868
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_16872 -> h_Reg x_16872
119| Imm x_16873 -> h_Imm x_16873
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_16877 -> h_Reg x_16877
125| Imm x_16878 -> h_Imm x_16878
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_16882 -> h_Reg x_16882
131| Imm x_16883 -> h_Imm x_16883
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_16887 -> h_Reg x_16887
137| Imm x_16888 -> h_Imm x_16888
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_16892 -> h_Reg x_16892
143| Imm x_16893 -> h_Imm x_16893
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_16928 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_16928
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_16930 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_16930
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_16932 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_16932
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_16934 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_16934
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_16936 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_16936
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_16938 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_16938
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_16955 =
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_16955
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_16957 =
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_16957
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_16959 =
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_16959
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_16961 =
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_16961
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_16963 =
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_16963
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_16965 =
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_16965
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_16995 =
808  let { u_pars = u_pars0; functs = functs0 } = x_16995 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_16997 =
815  let { u_pars = u_pars0; functs = functs0 } = x_16997 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_16999 =
822  let { u_pars = u_pars0; functs = functs0 } = x_16999 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_17001 =
829  let { u_pars = u_pars0; functs = functs0 } = x_17001 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_17003 =
836  let { u_pars = u_pars0; functs = functs0 } = x_17003 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_17005 =
843  let { u_pars = u_pars0; functs = functs0 } = x_17005 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 * BitVector.word * __ * __
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    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
909    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
910    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
911    __ -> 'a1) -> (__ -> __ -> __ -> '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_17061 -> h_COMMENT x_17061
914| MOVE x_17062 -> h_MOVE x_17062
915| POP x_17063 -> h_POP x_17063
916| PUSH x_17064 -> h_PUSH x_17064
917| ADDRESS (i, x_17067, x_17066, x_17065) ->
918  h_ADDRESS i __ x_17067 x_17066 x_17065
919| OPACCS (x_17073, x_17072, x_17071, x_17070, x_17069) ->
920  h_OPACCS x_17073 x_17072 x_17071 x_17070 x_17069
921| OP1 (x_17076, x_17075, x_17074) -> h_OP1 x_17076 x_17075 x_17074
922| OP2 (x_17080, x_17079, x_17078, x_17077) ->
923  h_OP2 x_17080 x_17079 x_17078 x_17077
924| CLEAR_CARRY -> h_CLEAR_CARRY
925| SET_CARRY -> h_SET_CARRY
926| LOAD (x_17083, x_17082, x_17081) -> h_LOAD x_17083 x_17082 x_17081
927| STORE (x_17086, x_17085, x_17084) -> h_STORE x_17086 x_17085 x_17084
928| Extension_seq x_17087 -> h_extension_seq x_17087
929
930(** val joint_seq_rect_Type5 :
931    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
932    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
933    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
934    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
935    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
936    __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
937let 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
938| COMMENT x_17102 -> h_COMMENT x_17102
939| MOVE x_17103 -> h_MOVE x_17103
940| POP x_17104 -> h_POP x_17104
941| PUSH x_17105 -> h_PUSH x_17105
942| ADDRESS (i, x_17108, x_17107, x_17106) ->
943  h_ADDRESS i __ x_17108 x_17107 x_17106
944| OPACCS (x_17114, x_17113, x_17112, x_17111, x_17110) ->
945  h_OPACCS x_17114 x_17113 x_17112 x_17111 x_17110
946| OP1 (x_17117, x_17116, x_17115) -> h_OP1 x_17117 x_17116 x_17115
947| OP2 (x_17121, x_17120, x_17119, x_17118) ->
948  h_OP2 x_17121 x_17120 x_17119 x_17118
949| CLEAR_CARRY -> h_CLEAR_CARRY
950| SET_CARRY -> h_SET_CARRY
951| LOAD (x_17124, x_17123, x_17122) -> h_LOAD x_17124 x_17123 x_17122
952| STORE (x_17127, x_17126, x_17125) -> h_STORE x_17127 x_17126 x_17125
953| Extension_seq x_17128 -> h_extension_seq x_17128
954
955(** val joint_seq_rect_Type3 :
956    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
957    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
958    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
959    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
960    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
961    __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
962let 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
963| COMMENT x_17143 -> h_COMMENT x_17143
964| MOVE x_17144 -> h_MOVE x_17144
965| POP x_17145 -> h_POP x_17145
966| PUSH x_17146 -> h_PUSH x_17146
967| ADDRESS (i, x_17149, x_17148, x_17147) ->
968  h_ADDRESS i __ x_17149 x_17148 x_17147
969| OPACCS (x_17155, x_17154, x_17153, x_17152, x_17151) ->
970  h_OPACCS x_17155 x_17154 x_17153 x_17152 x_17151
971| OP1 (x_17158, x_17157, x_17156) -> h_OP1 x_17158 x_17157 x_17156
972| OP2 (x_17162, x_17161, x_17160, x_17159) ->
973  h_OP2 x_17162 x_17161 x_17160 x_17159
974| CLEAR_CARRY -> h_CLEAR_CARRY
975| SET_CARRY -> h_SET_CARRY
976| LOAD (x_17165, x_17164, x_17163) -> h_LOAD x_17165 x_17164 x_17163
977| STORE (x_17168, x_17167, x_17166) -> h_STORE x_17168 x_17167 x_17166
978| Extension_seq x_17169 -> h_extension_seq x_17169
979
980(** val joint_seq_rect_Type2 :
981    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
982    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
983    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
984    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
985    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
986    __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
987let 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
988| COMMENT x_17184 -> h_COMMENT x_17184
989| MOVE x_17185 -> h_MOVE x_17185
990| POP x_17186 -> h_POP x_17186
991| PUSH x_17187 -> h_PUSH x_17187
992| ADDRESS (i, x_17190, x_17189, x_17188) ->
993  h_ADDRESS i __ x_17190 x_17189 x_17188
994| OPACCS (x_17196, x_17195, x_17194, x_17193, x_17192) ->
995  h_OPACCS x_17196 x_17195 x_17194 x_17193 x_17192
996| OP1 (x_17199, x_17198, x_17197) -> h_OP1 x_17199 x_17198 x_17197
997| OP2 (x_17203, x_17202, x_17201, x_17200) ->
998  h_OP2 x_17203 x_17202 x_17201 x_17200
999| CLEAR_CARRY -> h_CLEAR_CARRY
1000| SET_CARRY -> h_SET_CARRY
1001| LOAD (x_17206, x_17205, x_17204) -> h_LOAD x_17206 x_17205 x_17204
1002| STORE (x_17209, x_17208, x_17207) -> h_STORE x_17209 x_17208 x_17207
1003| Extension_seq x_17210 -> h_extension_seq x_17210
1004
1005(** val joint_seq_rect_Type1 :
1006    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1007    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1008    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1009    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1010    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1011    __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1012let 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
1013| COMMENT x_17225 -> h_COMMENT x_17225
1014| MOVE x_17226 -> h_MOVE x_17226
1015| POP x_17227 -> h_POP x_17227
1016| PUSH x_17228 -> h_PUSH x_17228
1017| ADDRESS (i, x_17231, x_17230, x_17229) ->
1018  h_ADDRESS i __ x_17231 x_17230 x_17229
1019| OPACCS (x_17237, x_17236, x_17235, x_17234, x_17233) ->
1020  h_OPACCS x_17237 x_17236 x_17235 x_17234 x_17233
1021| OP1 (x_17240, x_17239, x_17238) -> h_OP1 x_17240 x_17239 x_17238
1022| OP2 (x_17244, x_17243, x_17242, x_17241) ->
1023  h_OP2 x_17244 x_17243 x_17242 x_17241
1024| CLEAR_CARRY -> h_CLEAR_CARRY
1025| SET_CARRY -> h_SET_CARRY
1026| LOAD (x_17247, x_17246, x_17245) -> h_LOAD x_17247 x_17246 x_17245
1027| STORE (x_17250, x_17249, x_17248) -> h_STORE x_17250 x_17249 x_17248
1028| Extension_seq x_17251 -> h_extension_seq x_17251
1029
1030(** val joint_seq_rect_Type0 :
1031    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1032    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1033    BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1034    __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1035    (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1036    __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1037let 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
1038| COMMENT x_17266 -> h_COMMENT x_17266
1039| MOVE x_17267 -> h_MOVE x_17267
1040| POP x_17268 -> h_POP x_17268
1041| PUSH x_17269 -> h_PUSH x_17269
1042| ADDRESS (i, x_17272, x_17271, x_17270) ->
1043  h_ADDRESS i __ x_17272 x_17271 x_17270
1044| OPACCS (x_17278, x_17277, x_17276, x_17275, x_17274) ->
1045  h_OPACCS x_17278 x_17277 x_17276 x_17275 x_17274
1046| OP1 (x_17281, x_17280, x_17279) -> h_OP1 x_17281 x_17280 x_17279
1047| OP2 (x_17285, x_17284, x_17283, x_17282) ->
1048  h_OP2 x_17285 x_17284 x_17283 x_17282
1049| CLEAR_CARRY -> h_CLEAR_CARRY
1050| SET_CARRY -> h_SET_CARRY
1051| LOAD (x_17288, x_17287, x_17286) -> h_LOAD x_17288 x_17287 x_17286
1052| STORE (x_17291, x_17290, x_17289) -> h_STORE x_17291 x_17290 x_17289
1053| Extension_seq x_17292 -> h_extension_seq x_17292
1054
1055(** val joint_seq_inv_rect_Type4 :
1056    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1057    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1058    'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1059    (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1060    (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1061    -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1062    __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1063let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1064  let hcut =
1065    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1066      hterm
1067  in
1068  hcut __
1069
1070(** val joint_seq_inv_rect_Type3 :
1071    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1072    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1073    'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1074    (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1075    (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1076    -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1077    __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1078let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1079  let hcut =
1080    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1081      hterm
1082  in
1083  hcut __
1084
1085(** val joint_seq_inv_rect_Type2 :
1086    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1087    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1088    'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1089    (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1090    (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1091    -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1092    __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1093let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1094  let hcut =
1095    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1096      hterm
1097  in
1098  hcut __
1099
1100(** val joint_seq_inv_rect_Type1 :
1101    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1102    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1103    'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1104    (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1105    (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1106    -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1107    __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1108let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1109  let hcut =
1110    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1111      hterm
1112  in
1113  hcut __
1114
1115(** val joint_seq_inv_rect_Type0 :
1116    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1117    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1118    'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1119    (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1120    (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1121    -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1122    __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1123let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1124  let hcut =
1125    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1126      hterm
1127  in
1128  hcut __
1129
1130(** val joint_seq_discr :
1131    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1132    __ **)
1133let joint_seq_discr a1 a2 x y =
1134  Logic.eq_rect_Type2 x
1135    (match x with
1136     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1137     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1138     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1139     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1140     | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1141     | OPACCS (a0, a10, a20, a3, a4) ->
1142       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1143     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1144     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1145     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1146     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1147     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1148     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1149     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1150
1151(** val joint_seq_jmdiscr :
1152    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1153    __ **)
1154let joint_seq_jmdiscr a1 a2 x y =
1155  Logic.eq_rect_Type2 x
1156    (match x with
1157     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1158     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1159     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1160     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1161     | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1162     | OPACCS (a0, a10, a20, a3, a4) ->
1163       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1164     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1165     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1166     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1167     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1168     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1169     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1170     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1171
1172(** val get_used_registers_from_seq :
1173    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1174    joint_seq -> Registers.register List.list **)
1175let get_used_registers_from_seq p globals functs0 = function
1176| COMMENT x -> List.Nil
1177| MOVE pm -> functs0.pair_move_regs pm
1178| POP r -> functs0.acc_a_regs r
1179| PUSH r -> functs0.acc_a_args r
1180| ADDRESS (x, x1, r1, r2) ->
1181  List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1182| OPACCS (o, r1, r2, r3, r4) ->
1183  List.append (functs0.acc_a_regs r1)
1184    (List.append (functs0.acc_b_regs r2)
1185      (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1186| OP1 (o, r1, r2) ->
1187  List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1188| OP2 (o, r1, r2, r3) ->
1189  List.append (functs0.acc_a_regs r1)
1190    (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1191| CLEAR_CARRY -> List.Nil
1192| SET_CARRY -> List.Nil
1193| LOAD (r1, r2, r3) ->
1194  List.append (functs0.acc_a_regs r1)
1195    (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1196| STORE (r1, r2, r3) ->
1197  List.append (functs0.dpl_args r1)
1198    (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1199| Extension_seq ext -> functs0.ext_seq_regs ext
1200
1201(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1202let nOOP p globals =
1203  COMMENT String.EmptyString
1204
1205(** val dpi1__o__extension_seq_to_seq__o__inject :
1206    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1207    joint_seq Types.sig0 **)
1208let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1209  Extension_seq x4.Types.dpi1
1210
1211(** val eject__o__extension_seq_to_seq__o__inject :
1212    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1213    Types.sig0 **)
1214let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1215  Extension_seq (Types.pi1 x4)
1216
1217(** val extension_seq_to_seq__o__inject :
1218    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1219let extension_seq_to_seq__o__inject x0 x1 x3 =
1220  Extension_seq x3
1221
1222(** val dpi1__o__extension_seq_to_seq :
1223    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1224    joint_seq **)
1225let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1226  Extension_seq x3.Types.dpi1
1227
1228(** val eject__o__extension_seq_to_seq :
1229    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1230let eject__o__extension_seq_to_seq x0 x1 x3 =
1231  Extension_seq (Types.pi1 x3)
1232
1233type joint_step =
1234| COST_LABEL of CostLabel.costlabel
1235| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1236| COND of __ * Graphs.label
1237| Step_seq of joint_seq
1238
1239(** val joint_step_rect_Type4 :
1240    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1241    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1242    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1243let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1244| COST_LABEL x_17565 -> h_COST_LABEL x_17565
1245| CALL (x_17568, x_17567, x_17566) -> h_CALL x_17568 x_17567 x_17566
1246| COND (x_17570, x_17569) -> h_COND x_17570 x_17569
1247| Step_seq x_17571 -> h_step_seq x_17571
1248
1249(** val joint_step_rect_Type5 :
1250    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1251    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1252    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1253let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1254| COST_LABEL x_17577 -> h_COST_LABEL x_17577
1255| CALL (x_17580, x_17579, x_17578) -> h_CALL x_17580 x_17579 x_17578
1256| COND (x_17582, x_17581) -> h_COND x_17582 x_17581
1257| Step_seq x_17583 -> h_step_seq x_17583
1258
1259(** val joint_step_rect_Type3 :
1260    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1261    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1262    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1263let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1264| COST_LABEL x_17589 -> h_COST_LABEL x_17589
1265| CALL (x_17592, x_17591, x_17590) -> h_CALL x_17592 x_17591 x_17590
1266| COND (x_17594, x_17593) -> h_COND x_17594 x_17593
1267| Step_seq x_17595 -> h_step_seq x_17595
1268
1269(** val joint_step_rect_Type2 :
1270    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1271    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1272    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1273let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1274| COST_LABEL x_17601 -> h_COST_LABEL x_17601
1275| CALL (x_17604, x_17603, x_17602) -> h_CALL x_17604 x_17603 x_17602
1276| COND (x_17606, x_17605) -> h_COND x_17606 x_17605
1277| Step_seq x_17607 -> h_step_seq x_17607
1278
1279(** val joint_step_rect_Type1 :
1280    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1281    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1282    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1283let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1284| COST_LABEL x_17613 -> h_COST_LABEL x_17613
1285| CALL (x_17616, x_17615, x_17614) -> h_CALL x_17616 x_17615 x_17614
1286| COND (x_17618, x_17617) -> h_COND x_17618 x_17617
1287| Step_seq x_17619 -> h_step_seq x_17619
1288
1289(** val joint_step_rect_Type0 :
1290    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1291    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1292    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1293let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1294| COST_LABEL x_17625 -> h_COST_LABEL x_17625
1295| CALL (x_17628, x_17627, x_17626) -> h_CALL x_17628 x_17627 x_17626
1296| COND (x_17630, x_17629) -> h_COND x_17630 x_17629
1297| Step_seq x_17631 -> h_step_seq x_17631
1298
1299(** val joint_step_inv_rect_Type4 :
1300    unserialized_params -> AST.ident List.list -> joint_step ->
1301    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1302    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1303    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1304let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1305  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1306
1307(** val joint_step_inv_rect_Type3 :
1308    unserialized_params -> AST.ident List.list -> joint_step ->
1309    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1310    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1311    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1312let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1313  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1314
1315(** val joint_step_inv_rect_Type2 :
1316    unserialized_params -> AST.ident List.list -> joint_step ->
1317    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1318    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1319    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1320let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1321  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1322
1323(** val joint_step_inv_rect_Type1 :
1324    unserialized_params -> AST.ident List.list -> joint_step ->
1325    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1326    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1327    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1328let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1329  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1330
1331(** val joint_step_inv_rect_Type0 :
1332    unserialized_params -> AST.ident List.list -> joint_step ->
1333    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1334    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1335    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1336let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1337  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1338
1339(** val joint_step_discr :
1340    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1341    __ **)
1342let joint_step_discr a1 a2 x y =
1343  Logic.eq_rect_Type2 x
1344    (match x with
1345     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1346     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1347     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1348     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1349
1350(** val joint_step_jmdiscr :
1351    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1352    __ **)
1353let joint_step_jmdiscr a1 a2 x y =
1354  Logic.eq_rect_Type2 x
1355    (match x with
1356     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1357     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1358     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1359     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1360
1361(** val get_used_registers_from_step :
1362    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1363    joint_step -> Registers.register List.list **)
1364let get_used_registers_from_step p globals functs0 = function
1365| COST_LABEL c -> List.Nil
1366| CALL (id, args, dest) ->
1367  let r_id =
1368    match id with
1369    | Types.Inl x -> List.Nil
1370    | Types.Inr ptr ->
1371      List.append (functs0.dpl_args ptr.Types.fst)
1372        (functs0.dph_args ptr.Types.snd)
1373  in
1374  List.append r_id
1375    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1376| COND (r, lbl) -> functs0.acc_a_regs r
1377| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1378
1379(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1380    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1381    joint_step Types.sig0 **)
1382let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1383  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1384
1385(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1386    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1387    Types.sig0 **)
1388let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1389  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1390
1391(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1392    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1393let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1394  Step_seq (Extension_seq x2)
1395
1396(** val dpi1__o__seq_to_step__o__inject :
1397    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1398    Types.dPair -> joint_step Types.sig0 **)
1399let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1400  Step_seq x4.Types.dpi1
1401
1402(** val eject__o__seq_to_step__o__inject :
1403    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1404    joint_step Types.sig0 **)
1405let eject__o__seq_to_step__o__inject x0 x1 x4 =
1406  Step_seq (Types.pi1 x4)
1407
1408(** val seq_to_step__o__inject :
1409    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1410    Types.sig0 **)
1411let seq_to_step__o__inject x0 x1 x3 =
1412  Step_seq x3
1413
1414(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1415    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1416    joint_step **)
1417let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1418  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1419
1420(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1421    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1422let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1423  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1424
1425(** val extension_seq_to_seq__o__seq_to_step :
1426    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1427let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1428  Step_seq (Extension_seq x2)
1429
1430(** val dpi1__o__seq_to_step :
1431    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1432    Types.dPair -> joint_step **)
1433let dpi1__o__seq_to_step x0 x1 x3 =
1434  Step_seq x3.Types.dpi1
1435
1436(** val eject__o__seq_to_step :
1437    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1438    joint_step **)
1439let eject__o__seq_to_step x0 x1 x3 =
1440  Step_seq (Types.pi1 x3)
1441
1442(** val step_labels :
1443    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1444    List.list **)
1445let step_labels p globals = function
1446| COST_LABEL x -> List.Nil
1447| CALL (x, x0, x1) -> List.Nil
1448| COND (x, l) -> List.Cons (l, List.Nil)
1449| Step_seq s0 ->
1450  (match s0 with
1451   | COMMENT x -> List.Nil
1452   | MOVE x -> List.Nil
1453   | POP x -> List.Nil
1454   | PUSH x -> List.Nil
1455   | ADDRESS (x, x1, x2, x3) -> List.Nil
1456   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1457   | OP1 (x, x0, x1) -> List.Nil
1458   | OP2 (x, x0, x1, x2) -> List.Nil
1459   | CLEAR_CARRY -> List.Nil
1460   | SET_CARRY -> List.Nil
1461   | LOAD (x, x0, x1) -> List.Nil
1462   | STORE (x, x0, x1) -> List.Nil
1463   | Extension_seq ext -> p.ext_seq_labels ext)
1464
1465type stmt_params = { uns_pars : uns_params;
1466                     succ_label : (__ -> Graphs.label Types.option);
1467                     has_fcond : Bool.bool }
1468
1469(** val stmt_params_rect_Type4 :
1470    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1471    'a1) -> stmt_params -> 'a1 **)
1472let rec stmt_params_rect_Type4 h_mk_stmt_params x_17710 =
1473  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1474    has_fcond0 } = x_17710
1475  in
1476  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1477
1478(** val stmt_params_rect_Type5 :
1479    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1480    'a1) -> stmt_params -> 'a1 **)
1481let rec stmt_params_rect_Type5 h_mk_stmt_params x_17712 =
1482  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1483    has_fcond0 } = x_17712
1484  in
1485  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1486
1487(** val stmt_params_rect_Type3 :
1488    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1489    'a1) -> stmt_params -> 'a1 **)
1490let rec stmt_params_rect_Type3 h_mk_stmt_params x_17714 =
1491  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1492    has_fcond0 } = x_17714
1493  in
1494  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1495
1496(** val stmt_params_rect_Type2 :
1497    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1498    'a1) -> stmt_params -> 'a1 **)
1499let rec stmt_params_rect_Type2 h_mk_stmt_params x_17716 =
1500  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1501    has_fcond0 } = x_17716
1502  in
1503  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1504
1505(** val stmt_params_rect_Type1 :
1506    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1507    'a1) -> stmt_params -> 'a1 **)
1508let rec stmt_params_rect_Type1 h_mk_stmt_params x_17718 =
1509  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1510    has_fcond0 } = x_17718
1511  in
1512  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1513
1514(** val stmt_params_rect_Type0 :
1515    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1516    'a1) -> stmt_params -> 'a1 **)
1517let rec stmt_params_rect_Type0 h_mk_stmt_params x_17720 =
1518  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1519    has_fcond0 } = x_17720
1520  in
1521  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1522
1523(** val uns_pars : stmt_params -> uns_params **)
1524let rec uns_pars xxx =
1525  xxx.uns_pars
1526
1527type succ = __
1528
1529(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1530let rec succ_label xxx =
1531  xxx.succ_label
1532
1533(** val has_fcond : stmt_params -> Bool.bool **)
1534let rec has_fcond xxx =
1535  xxx.has_fcond
1536
1537(** val stmt_params_inv_rect_Type4 :
1538    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539    Bool.bool -> __ -> 'a1) -> 'a1 **)
1540let stmt_params_inv_rect_Type4 hterm h1 =
1541  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1542
1543(** val stmt_params_inv_rect_Type3 :
1544    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545    Bool.bool -> __ -> 'a1) -> 'a1 **)
1546let stmt_params_inv_rect_Type3 hterm h1 =
1547  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1548
1549(** val stmt_params_inv_rect_Type2 :
1550    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551    Bool.bool -> __ -> 'a1) -> 'a1 **)
1552let stmt_params_inv_rect_Type2 hterm h1 =
1553  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1554
1555(** val stmt_params_inv_rect_Type1 :
1556    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1557    Bool.bool -> __ -> 'a1) -> 'a1 **)
1558let stmt_params_inv_rect_Type1 hterm h1 =
1559  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1560
1561(** val stmt_params_inv_rect_Type0 :
1562    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1563    Bool.bool -> __ -> 'a1) -> 'a1 **)
1564let stmt_params_inv_rect_Type0 hterm h1 =
1565  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1566
1567(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1568let stmt_params_jmdiscr x y =
1569  Logic.eq_rect_Type2 x
1570    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1571    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1572
1573(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1574let uns_pars__o__u_pars x0 =
1575  x0.uns_pars.u_pars
1576
1577type joint_fin_step =
1578| GOTO of Graphs.label
1579| RETURN
1580| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1581
1582(** val joint_fin_step_rect_Type4 :
1583    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1584    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1585let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1586| GOTO x_17744 -> h_GOTO x_17744
1587| RETURN -> h_RETURN
1588| TAILCALL (x_17746, x_17745) -> h_TAILCALL __ x_17746 x_17745
1589
1590(** val joint_fin_step_rect_Type5 :
1591    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1592    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1593let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1594| GOTO x_17752 -> h_GOTO x_17752
1595| RETURN -> h_RETURN
1596| TAILCALL (x_17754, x_17753) -> h_TAILCALL __ x_17754 x_17753
1597
1598(** val joint_fin_step_rect_Type3 :
1599    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1600    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1601let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1602| GOTO x_17760 -> h_GOTO x_17760
1603| RETURN -> h_RETURN
1604| TAILCALL (x_17762, x_17761) -> h_TAILCALL __ x_17762 x_17761
1605
1606(** val joint_fin_step_rect_Type2 :
1607    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1608    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1609let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1610| GOTO x_17768 -> h_GOTO x_17768
1611| RETURN -> h_RETURN
1612| TAILCALL (x_17770, x_17769) -> h_TAILCALL __ x_17770 x_17769
1613
1614(** val joint_fin_step_rect_Type1 :
1615    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1616    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1617let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1618| GOTO x_17776 -> h_GOTO x_17776
1619| RETURN -> h_RETURN
1620| TAILCALL (x_17778, x_17777) -> h_TAILCALL __ x_17778 x_17777
1621
1622(** val joint_fin_step_rect_Type0 :
1623    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1624    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1625let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1626| GOTO x_17784 -> h_GOTO x_17784
1627| RETURN -> h_RETURN
1628| TAILCALL (x_17786, x_17785) -> h_TAILCALL __ x_17786 x_17785
1629
1630(** val joint_fin_step_inv_rect_Type4 :
1631    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1632    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1633    __ -> 'a1) -> 'a1 **)
1634let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1635  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1636
1637(** val joint_fin_step_inv_rect_Type3 :
1638    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1639    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1640    __ -> 'a1) -> 'a1 **)
1641let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1642  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1643
1644(** val joint_fin_step_inv_rect_Type2 :
1645    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1646    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1647    __ -> 'a1) -> 'a1 **)
1648let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1649  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1650
1651(** val joint_fin_step_inv_rect_Type1 :
1652    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1653    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1654    __ -> 'a1) -> 'a1 **)
1655let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1656  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1657
1658(** val joint_fin_step_inv_rect_Type0 :
1659    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1660    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1661    __ -> 'a1) -> 'a1 **)
1662let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1663  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1664
1665(** val joint_fin_step_discr :
1666    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1667let joint_fin_step_discr a1 x y =
1668  Logic.eq_rect_Type2 x
1669    (match x with
1670     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1671     | RETURN -> Obj.magic (fun _ dH -> dH)
1672     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1673
1674(** val joint_fin_step_jmdiscr :
1675    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1676let joint_fin_step_jmdiscr a1 x y =
1677  Logic.eq_rect_Type2 x
1678    (match x with
1679     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1680     | RETURN -> Obj.magic (fun _ dH -> dH)
1681     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1682
1683(** val fin_step_labels :
1684    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1685let fin_step_labels p = function
1686| GOTO l -> List.Cons (l, List.Nil)
1687| RETURN -> List.Nil
1688| TAILCALL (x0, x1) -> List.Nil
1689
1690type joint_statement =
1691| Sequential of joint_step * __
1692| Final of joint_fin_step
1693| FCOND of __ * Graphs.label * Graphs.label
1694
1695(** val joint_statement_rect_Type4 :
1696    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1697    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1698    'a1) -> joint_statement -> 'a1 **)
1699let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1700| Sequential (x_17852, x_17851) -> h_sequential x_17852 x_17851
1701| Final x_17853 -> h_final x_17853
1702| FCOND (x_17856, x_17855, x_17854) -> h_FCOND __ x_17856 x_17855 x_17854
1703
1704(** val joint_statement_rect_Type5 :
1705    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1706    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1707    'a1) -> joint_statement -> 'a1 **)
1708let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1709| Sequential (x_17863, x_17862) -> h_sequential x_17863 x_17862
1710| Final x_17864 -> h_final x_17864
1711| FCOND (x_17867, x_17866, x_17865) -> h_FCOND __ x_17867 x_17866 x_17865
1712
1713(** val joint_statement_rect_Type3 :
1714    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1715    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1716    'a1) -> joint_statement -> 'a1 **)
1717let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1718| Sequential (x_17874, x_17873) -> h_sequential x_17874 x_17873
1719| Final x_17875 -> h_final x_17875
1720| FCOND (x_17878, x_17877, x_17876) -> h_FCOND __ x_17878 x_17877 x_17876
1721
1722(** val joint_statement_rect_Type2 :
1723    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1724    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1725    'a1) -> joint_statement -> 'a1 **)
1726let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1727| Sequential (x_17885, x_17884) -> h_sequential x_17885 x_17884
1728| Final x_17886 -> h_final x_17886
1729| FCOND (x_17889, x_17888, x_17887) -> h_FCOND __ x_17889 x_17888 x_17887
1730
1731(** val joint_statement_rect_Type1 :
1732    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1733    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1734    'a1) -> joint_statement -> 'a1 **)
1735let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1736| Sequential (x_17896, x_17895) -> h_sequential x_17896 x_17895
1737| Final x_17897 -> h_final x_17897
1738| FCOND (x_17900, x_17899, x_17898) -> h_FCOND __ x_17900 x_17899 x_17898
1739
1740(** val joint_statement_rect_Type0 :
1741    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1742    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1743    'a1) -> joint_statement -> 'a1 **)
1744let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1745| Sequential (x_17907, x_17906) -> h_sequential x_17907 x_17906
1746| Final x_17908 -> h_final x_17908
1747| FCOND (x_17911, x_17910, x_17909) -> h_FCOND __ x_17911 x_17910 x_17909
1748
1749(** val joint_statement_inv_rect_Type4 :
1750    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1751    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1752    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1753let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1754  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1755
1756(** val joint_statement_inv_rect_Type3 :
1757    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1758    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1759    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1760let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1761  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1762
1763(** val joint_statement_inv_rect_Type2 :
1764    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1765    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1766    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1767let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1768  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1769
1770(** val joint_statement_inv_rect_Type1 :
1771    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1772    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1773    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1774let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1775  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1776
1777(** val joint_statement_inv_rect_Type0 :
1778    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1779    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1780    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1781let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1782  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1783
1784(** val joint_statement_discr :
1785    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1786    -> __ **)
1787let joint_statement_discr a1 a2 x y =
1788  Logic.eq_rect_Type2 x
1789    (match x with
1790     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1791     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1792     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1793
1794(** val joint_statement_jmdiscr :
1795    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1796    -> __ **)
1797let joint_statement_jmdiscr a1 a2 x y =
1798  Logic.eq_rect_Type2 x
1799    (match x with
1800     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1801     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1802     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1803
1804(** val dpi1__o__fin_step_to_stmt__o__inject :
1805    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1806    -> joint_statement Types.sig0 **)
1807let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1808  Final x4.Types.dpi1
1809
1810(** val eject__o__fin_step_to_stmt__o__inject :
1811    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1812    joint_statement Types.sig0 **)
1813let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1814  Final (Types.pi1 x4)
1815
1816(** val fin_step_to_stmt__o__inject :
1817    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1818    Types.sig0 **)
1819let fin_step_to_stmt__o__inject x0 x1 x3 =
1820  Final x3
1821
1822(** val dpi1__o__fin_step_to_stmt :
1823    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1824    -> joint_statement **)
1825let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1826  Final x3.Types.dpi1
1827
1828(** val eject__o__fin_step_to_stmt :
1829    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1830    joint_statement **)
1831let eject__o__fin_step_to_stmt x0 x1 x3 =
1832  Final (Types.pi1 x3)
1833
1834type params = { stmt_pars : stmt_params;
1835                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1836                          Types.option);
1837                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1838                                 -> __ Types.option);
1839                point_of_succ : (__ -> __ -> __) }
1840
1841(** val params_rect_Type4 :
1842    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1843    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1844    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1845    'a1 **)
1846let rec params_rect_Type4 h_mk_params x_17984 =
1847  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1848    point_of_label0; point_of_succ = point_of_succ0 } = x_17984
1849  in
1850  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1851
1852(** val params_rect_Type5 :
1853    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1854    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1855    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1856    'a1 **)
1857let rec params_rect_Type5 h_mk_params x_17986 =
1858  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1859    point_of_label0; point_of_succ = point_of_succ0 } = x_17986
1860  in
1861  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1862
1863(** val params_rect_Type3 :
1864    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1865    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1866    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1867    'a1 **)
1868let rec params_rect_Type3 h_mk_params x_17988 =
1869  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1870    point_of_label0; point_of_succ = point_of_succ0 } = x_17988
1871  in
1872  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1873
1874(** val params_rect_Type2 :
1875    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1876    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1877    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1878    'a1 **)
1879let rec params_rect_Type2 h_mk_params x_17990 =
1880  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1881    point_of_label0; point_of_succ = point_of_succ0 } = x_17990
1882  in
1883  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1884
1885(** val params_rect_Type1 :
1886    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1887    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1888    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1889    'a1 **)
1890let rec params_rect_Type1 h_mk_params x_17992 =
1891  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1892    point_of_label0; point_of_succ = point_of_succ0 } = x_17992
1893  in
1894  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1895
1896(** val params_rect_Type0 :
1897    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1898    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1899    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1900    'a1 **)
1901let rec params_rect_Type0 h_mk_params x_17994 =
1902  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1903    point_of_label0; point_of_succ = point_of_succ0 } = x_17994
1904  in
1905  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1906
1907(** val stmt_pars : params -> stmt_params **)
1908let rec stmt_pars xxx =
1909  xxx.stmt_pars
1910
1911type codeT = __
1912
1913type code_point = __
1914
1915(** val stmt_at :
1916    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1917let rec stmt_at xxx =
1918  xxx.stmt_at
1919
1920(** val point_of_label :
1921    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1922let rec point_of_label xxx =
1923  xxx.point_of_label
1924
1925(** val point_of_succ : params -> __ -> __ -> __ **)
1926let rec point_of_succ xxx =
1927  xxx.point_of_succ
1928
1929(** val params_inv_rect_Type4 :
1930    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1931    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1932    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1933let params_inv_rect_Type4 hterm h1 =
1934  let hcut = params_rect_Type4 h1 hterm in hcut __
1935
1936(** val params_inv_rect_Type3 :
1937    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1938    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1939    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1940let params_inv_rect_Type3 hterm h1 =
1941  let hcut = params_rect_Type3 h1 hterm in hcut __
1942
1943(** val params_inv_rect_Type2 :
1944    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1945    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1946    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1947let params_inv_rect_Type2 hterm h1 =
1948  let hcut = params_rect_Type2 h1 hterm in hcut __
1949
1950(** val params_inv_rect_Type1 :
1951    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1952    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1953    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1954let params_inv_rect_Type1 hterm h1 =
1955  let hcut = params_rect_Type1 h1 hterm in hcut __
1956
1957(** val params_inv_rect_Type0 :
1958    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1959    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1960    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1961let params_inv_rect_Type0 hterm h1 =
1962  let hcut = params_rect_Type0 h1 hterm in hcut __
1963
1964(** val params_jmdiscr : params -> params -> __ **)
1965let params_jmdiscr x y =
1966  Logic.eq_rect_Type2 x
1967    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1968       a5 } = x
1969     in
1970    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1971
1972(** val stmt_pars__o__uns_pars : params -> uns_params **)
1973let stmt_pars__o__uns_pars x0 =
1974  x0.stmt_pars.uns_pars
1975
1976(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1977let stmt_pars__o__uns_pars__o__u_pars x0 =
1978  uns_pars__o__u_pars x0.stmt_pars
1979
1980(** val code_has_point :
1981    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1982let code_has_point p globals c pt =
1983  match p.stmt_at globals c pt with
1984  | Types.None -> Bool.False
1985  | Types.Some x -> Bool.True
1986
1987(** val code_has_label :
1988    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1989let code_has_label p globals c l =
1990  match p.point_of_label globals c l with
1991  | Types.None -> Bool.False
1992  | Types.Some pt -> code_has_point p globals c pt
1993
1994(** val stmt_explicit_labels :
1995    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1996    List.list **)
1997let stmt_explicit_labels p globals = function
1998| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1999| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
2000| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
2001
2002(** val stmt_implicit_label :
2003    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2004    Types.option **)
2005let stmt_implicit_label p globals = function
2006| Sequential (x, s0) -> p.succ_label s0
2007| Final x -> Types.None
2008| FCOND (x0, x1, x2) -> Types.None
2009
2010(** val stmt_labels :
2011    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2012    List.list **)
2013let stmt_labels p g stmt =
2014  List.append
2015    (match stmt_implicit_label p g stmt with
2016     | Types.None -> List.Nil
2017     | Types.Some l -> List.Cons (l, List.Nil))
2018    (stmt_explicit_labels p g stmt)
2019
2020(** val stmt_registers :
2021    stmt_params -> AST.ident List.list -> joint_statement ->
2022    Registers.register List.list **)
2023let stmt_registers p globals = function
2024| Sequential (c, x) ->
2025  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2026| Final c ->
2027  (match c with
2028   | GOTO x -> List.Nil
2029   | RETURN -> List.Nil
2030   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2031| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2032
2033type lin_params =
2034  uns_params
2035  (* singleton inductive, whose constructor was mk_lin_params *)
2036
2037(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2038let rec lin_params_rect_Type4 h_mk_lin_params x_18017 =
2039  let l_u_pars = x_18017 in h_mk_lin_params l_u_pars
2040
2041(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2042let rec lin_params_rect_Type5 h_mk_lin_params x_18019 =
2043  let l_u_pars = x_18019 in h_mk_lin_params l_u_pars
2044
2045(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2046let rec lin_params_rect_Type3 h_mk_lin_params x_18021 =
2047  let l_u_pars = x_18021 in h_mk_lin_params l_u_pars
2048
2049(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2050let rec lin_params_rect_Type2 h_mk_lin_params x_18023 =
2051  let l_u_pars = x_18023 in h_mk_lin_params l_u_pars
2052
2053(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2054let rec lin_params_rect_Type1 h_mk_lin_params x_18025 =
2055  let l_u_pars = x_18025 in h_mk_lin_params l_u_pars
2056
2057(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2058let rec lin_params_rect_Type0 h_mk_lin_params x_18027 =
2059  let l_u_pars = x_18027 in h_mk_lin_params l_u_pars
2060
2061(** val l_u_pars : lin_params -> uns_params **)
2062let rec l_u_pars xxx =
2063  let yyy = xxx in yyy
2064
2065(** val lin_params_inv_rect_Type4 :
2066    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2067let lin_params_inv_rect_Type4 hterm h1 =
2068  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2069
2070(** val lin_params_inv_rect_Type3 :
2071    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2072let lin_params_inv_rect_Type3 hterm h1 =
2073  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2074
2075(** val lin_params_inv_rect_Type2 :
2076    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2077let lin_params_inv_rect_Type2 hterm h1 =
2078  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2079
2080(** val lin_params_inv_rect_Type1 :
2081    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2082let lin_params_inv_rect_Type1 hterm h1 =
2083  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2084
2085(** val lin_params_inv_rect_Type0 :
2086    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2087let lin_params_inv_rect_Type0 hterm h1 =
2088  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2089
2090(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2091let lin_params_jmdiscr x y =
2092  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2093
2094(** val lin_params_to_params : lin_params -> params **)
2095let lin_params_to_params lp =
2096  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2097    Types.None); has_fcond = Bool.True }; stmt_at =
2098    (fun globals code point ->
2099    Obj.magic
2100      (Monad.m_bind0 (Monad.max_def Option.option)
2101        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2102        (fun ls ->
2103        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2104    point_of_label = (fun globals c lbl ->
2105    Util.if_then_else_safe
2106      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2107        (Obj.magic c)) (fun _ ->
2108      Obj.magic
2109        (Monad.m_return0 (Monad.max_def Option.option)
2110          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2111            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2112    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2113
2114(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2115let lp_to_p__o__stmt_pars x0 =
2116  (lin_params_to_params x0).stmt_pars
2117
2118(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2119let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2120  stmt_pars__o__uns_pars (lin_params_to_params x0)
2121
2122(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2123    lin_params -> unserialized_params **)
2124let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2125  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2126
2127type graph_params =
2128  uns_params
2129  (* singleton inductive, whose constructor was mk_graph_params *)
2130
2131(** val graph_params_rect_Type4 :
2132    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2133let rec graph_params_rect_Type4 h_mk_graph_params x_18043 =
2134  let g_u_pars = x_18043 in h_mk_graph_params g_u_pars
2135
2136(** val graph_params_rect_Type5 :
2137    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2138let rec graph_params_rect_Type5 h_mk_graph_params x_18045 =
2139  let g_u_pars = x_18045 in h_mk_graph_params g_u_pars
2140
2141(** val graph_params_rect_Type3 :
2142    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2143let rec graph_params_rect_Type3 h_mk_graph_params x_18047 =
2144  let g_u_pars = x_18047 in h_mk_graph_params g_u_pars
2145
2146(** val graph_params_rect_Type2 :
2147    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2148let rec graph_params_rect_Type2 h_mk_graph_params x_18049 =
2149  let g_u_pars = x_18049 in h_mk_graph_params g_u_pars
2150
2151(** val graph_params_rect_Type1 :
2152    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2153let rec graph_params_rect_Type1 h_mk_graph_params x_18051 =
2154  let g_u_pars = x_18051 in h_mk_graph_params g_u_pars
2155
2156(** val graph_params_rect_Type0 :
2157    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2158let rec graph_params_rect_Type0 h_mk_graph_params x_18053 =
2159  let g_u_pars = x_18053 in h_mk_graph_params g_u_pars
2160
2161(** val g_u_pars : graph_params -> uns_params **)
2162let rec g_u_pars xxx =
2163  let yyy = xxx in yyy
2164
2165(** val graph_params_inv_rect_Type4 :
2166    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2167let graph_params_inv_rect_Type4 hterm h1 =
2168  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2169
2170(** val graph_params_inv_rect_Type3 :
2171    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2172let graph_params_inv_rect_Type3 hterm h1 =
2173  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2174
2175(** val graph_params_inv_rect_Type2 :
2176    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2177let graph_params_inv_rect_Type2 hterm h1 =
2178  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2179
2180(** val graph_params_inv_rect_Type1 :
2181    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2182let graph_params_inv_rect_Type1 hterm h1 =
2183  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2184
2185(** val graph_params_inv_rect_Type0 :
2186    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2187let graph_params_inv_rect_Type0 hterm h1 =
2188  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2189
2190(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2191let graph_params_jmdiscr x y =
2192  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2193
2194(** val graph_params_to_params : graph_params -> params **)
2195let graph_params_to_params gp =
2196  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2197    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2198    (fun globals code ->
2199    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2200    point_of_label = (fun x x0 lbl ->
2201    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2202    point_of_succ = (fun x lbl -> lbl) }
2203
2204(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2205let gp_to_p__o__stmt_pars x0 =
2206  (graph_params_to_params x0).stmt_pars
2207
2208(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2209let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2210  stmt_pars__o__uns_pars (graph_params_to_params x0)
2211
2212(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2213    graph_params -> unserialized_params **)
2214let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2215  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2216
2217type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2218                                 joint_if_runiverse : Identifiers.universe;
2219                                 joint_if_result : __; joint_if_params : 
2220                                 __; joint_if_stacksize : Nat.nat;
2221                                 joint_if_local_stacksize : Nat.nat;
2222                                 joint_if_code : __; joint_if_entry : 
2223                                 __ }
2224
2225(** val joint_internal_function_rect_Type4 :
2226    params -> AST.ident List.list -> (Identifiers.universe ->
2227    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2228    'a1) -> joint_internal_function -> 'a1 **)
2229let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18069 =
2230  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2231    joint_if_runiverse0; joint_if_result = joint_if_result0;
2232    joint_if_params = joint_if_params0; joint_if_stacksize =
2233    joint_if_stacksize0; joint_if_local_stacksize =
2234    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2235    joint_if_entry = joint_if_entry0 } = x_18069
2236  in
2237  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2238    joint_if_result0 joint_if_params0 joint_if_stacksize0
2239    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2240
2241(** val joint_internal_function_rect_Type5 :
2242    params -> AST.ident List.list -> (Identifiers.universe ->
2243    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2244    'a1) -> joint_internal_function -> 'a1 **)
2245let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18071 =
2246  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2247    joint_if_runiverse0; joint_if_result = joint_if_result0;
2248    joint_if_params = joint_if_params0; joint_if_stacksize =
2249    joint_if_stacksize0; joint_if_local_stacksize =
2250    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2251    joint_if_entry = joint_if_entry0 } = x_18071
2252  in
2253  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2254    joint_if_result0 joint_if_params0 joint_if_stacksize0
2255    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2256
2257(** val joint_internal_function_rect_Type3 :
2258    params -> AST.ident List.list -> (Identifiers.universe ->
2259    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2260    'a1) -> joint_internal_function -> 'a1 **)
2261let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18073 =
2262  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2263    joint_if_runiverse0; joint_if_result = joint_if_result0;
2264    joint_if_params = joint_if_params0; joint_if_stacksize =
2265    joint_if_stacksize0; joint_if_local_stacksize =
2266    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2267    joint_if_entry = joint_if_entry0 } = x_18073
2268  in
2269  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2270    joint_if_result0 joint_if_params0 joint_if_stacksize0
2271    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2272
2273(** val joint_internal_function_rect_Type2 :
2274    params -> AST.ident List.list -> (Identifiers.universe ->
2275    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2276    'a1) -> joint_internal_function -> 'a1 **)
2277let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18075 =
2278  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2279    joint_if_runiverse0; joint_if_result = joint_if_result0;
2280    joint_if_params = joint_if_params0; joint_if_stacksize =
2281    joint_if_stacksize0; joint_if_local_stacksize =
2282    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2283    joint_if_entry = joint_if_entry0 } = x_18075
2284  in
2285  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2286    joint_if_result0 joint_if_params0 joint_if_stacksize0
2287    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2288
2289(** val joint_internal_function_rect_Type1 :
2290    params -> AST.ident List.list -> (Identifiers.universe ->
2291    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2292    'a1) -> joint_internal_function -> 'a1 **)
2293let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18077 =
2294  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2295    joint_if_runiverse0; joint_if_result = joint_if_result0;
2296    joint_if_params = joint_if_params0; joint_if_stacksize =
2297    joint_if_stacksize0; joint_if_local_stacksize =
2298    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2299    joint_if_entry = joint_if_entry0 } = x_18077
2300  in
2301  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2302    joint_if_result0 joint_if_params0 joint_if_stacksize0
2303    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2304
2305(** val joint_internal_function_rect_Type0 :
2306    params -> AST.ident List.list -> (Identifiers.universe ->
2307    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2308    'a1) -> joint_internal_function -> 'a1 **)
2309let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18079 =
2310  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2311    joint_if_runiverse0; joint_if_result = joint_if_result0;
2312    joint_if_params = joint_if_params0; joint_if_stacksize =
2313    joint_if_stacksize0; joint_if_local_stacksize =
2314    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2315    joint_if_entry = joint_if_entry0 } = x_18079
2316  in
2317  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2318    joint_if_result0 joint_if_params0 joint_if_stacksize0
2319    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2320
2321(** val joint_if_luniverse :
2322    params -> AST.ident List.list -> joint_internal_function ->
2323    Identifiers.universe **)
2324let rec joint_if_luniverse p globals xxx =
2325  xxx.joint_if_luniverse
2326
2327(** val joint_if_runiverse :
2328    params -> AST.ident List.list -> joint_internal_function ->
2329    Identifiers.universe **)
2330let rec joint_if_runiverse p globals xxx =
2331  xxx.joint_if_runiverse
2332
2333(** val joint_if_result :
2334    params -> AST.ident List.list -> joint_internal_function -> __ **)
2335let rec joint_if_result p globals xxx =
2336  xxx.joint_if_result
2337
2338(** val joint_if_params :
2339    params -> AST.ident List.list -> joint_internal_function -> __ **)
2340let rec joint_if_params p globals xxx =
2341  xxx.joint_if_params
2342
2343(** val joint_if_stacksize :
2344    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2345let rec joint_if_stacksize p globals xxx =
2346  xxx.joint_if_stacksize
2347
2348(** val joint_if_local_stacksize :
2349    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2350let rec joint_if_local_stacksize p globals xxx =
2351  xxx.joint_if_local_stacksize
2352
2353(** val joint_if_code :
2354    params -> AST.ident List.list -> joint_internal_function -> __ **)
2355let rec joint_if_code p globals xxx =
2356  xxx.joint_if_code
2357
2358(** val joint_if_entry :
2359    params -> AST.ident List.list -> joint_internal_function -> __ **)
2360let rec joint_if_entry p globals xxx =
2361  xxx.joint_if_entry
2362
2363(** val joint_internal_function_inv_rect_Type4 :
2364    params -> AST.ident List.list -> joint_internal_function ->
2365    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2366    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2367let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2368  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2369
2370(** val joint_internal_function_inv_rect_Type3 :
2371    params -> AST.ident List.list -> joint_internal_function ->
2372    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2373    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2374let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2375  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2376
2377(** val joint_internal_function_inv_rect_Type2 :
2378    params -> AST.ident List.list -> joint_internal_function ->
2379    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2380    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2381let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2382  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2383
2384(** val joint_internal_function_inv_rect_Type1 :
2385    params -> AST.ident List.list -> joint_internal_function ->
2386    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2387    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2388let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2389  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2390
2391(** val joint_internal_function_inv_rect_Type0 :
2392    params -> AST.ident List.list -> joint_internal_function ->
2393    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2394    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2395let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2396  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2397
2398(** val joint_internal_function_jmdiscr :
2399    params -> AST.ident List.list -> joint_internal_function ->
2400    joint_internal_function -> __ **)
2401let joint_internal_function_jmdiscr a1 a2 x y =
2402  Logic.eq_rect_Type2 x
2403    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2404       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2405       joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2406       a7 } = x
2407     in
2408    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2409
2410(** val good_if_rect_Type4 :
2411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412    __ -> __ -> __ -> 'a1) -> 'a1 **)
2413let rec good_if_rect_Type4 p globals def h_mk_good_if =
2414  h_mk_good_if __ __ __ __ __
2415
2416(** val good_if_rect_Type5 :
2417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418    __ -> __ -> __ -> 'a1) -> 'a1 **)
2419let rec good_if_rect_Type5 p globals def h_mk_good_if =
2420  h_mk_good_if __ __ __ __ __
2421
2422(** val good_if_rect_Type3 :
2423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424    __ -> __ -> __ -> 'a1) -> 'a1 **)
2425let rec good_if_rect_Type3 p globals def h_mk_good_if =
2426  h_mk_good_if __ __ __ __ __
2427
2428(** val good_if_rect_Type2 :
2429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430    __ -> __ -> __ -> 'a1) -> 'a1 **)
2431let rec good_if_rect_Type2 p globals def h_mk_good_if =
2432  h_mk_good_if __ __ __ __ __
2433
2434(** val good_if_rect_Type1 :
2435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436    __ -> __ -> __ -> 'a1) -> 'a1 **)
2437let rec good_if_rect_Type1 p globals def h_mk_good_if =
2438  h_mk_good_if __ __ __ __ __
2439
2440(** val good_if_rect_Type0 :
2441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442    __ -> __ -> __ -> 'a1) -> 'a1 **)
2443let rec good_if_rect_Type0 p globals def h_mk_good_if =
2444  h_mk_good_if __ __ __ __ __
2445
2446(** val good_if_inv_rect_Type4 :
2447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2450  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2451
2452(** val good_if_inv_rect_Type3 :
2453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2456  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2457
2458(** val good_if_inv_rect_Type2 :
2459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2462  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2463
2464(** val good_if_inv_rect_Type1 :
2465    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2466    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2467let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2468  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2469
2470(** val good_if_inv_rect_Type0 :
2471    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2472    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2473let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2474  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2475
2476(** val good_if_discr :
2477    params -> AST.ident List.list -> joint_internal_function -> __ **)
2478let good_if_discr a1 a2 a3 =
2479  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2480
2481(** val good_if_jmdiscr :
2482    params -> AST.ident List.list -> joint_internal_function -> __ **)
2483let good_if_jmdiscr a1 a2 a3 =
2484  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2485
2486type joint_closed_internal_function = joint_internal_function Types.sig0
2487
2488(** val set_joint_code :
2489    AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2490    joint_internal_function **)
2491let set_joint_code globals pars int_fun graph entry =
2492  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2493    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2494    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2495    int_fun.joint_if_stacksize; joint_if_local_stacksize =
2496    int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2497    entry }
2498
2499(** val set_luniverse :
2500    params -> AST.ident List.list -> joint_internal_function ->
2501    Identifiers.universe -> joint_internal_function **)
2502let set_luniverse globals pars p luniverse =
2503  { joint_if_luniverse = luniverse; joint_if_runiverse =
2504    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2505    joint_if_params = p.joint_if_params; joint_if_stacksize =
2506    p.joint_if_stacksize; joint_if_local_stacksize =
2507    p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2508    joint_if_entry = p.joint_if_entry }
2509
2510(** val set_runiverse :
2511    params -> AST.ident List.list -> joint_internal_function ->
2512    Identifiers.universe -> joint_internal_function **)
2513let set_runiverse globals pars p runiverse =
2514  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2515    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2516    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2517    joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2518    p.joint_if_code; joint_if_entry = p.joint_if_entry }
2519
2520(** val add_graph :
2521    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2522    joint_internal_function -> joint_internal_function **)
2523let add_graph g_pars globals l stmt p =
2524  let code =
2525    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2526      stmt
2527  in
2528  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2529  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2530  joint_if_params = p.joint_if_params; joint_if_stacksize =
2531  p.joint_if_stacksize; joint_if_local_stacksize =
2532  p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2533  joint_if_entry = p.joint_if_entry }
2534
2535type joint_function = joint_closed_internal_function AST.fundef
2536
2537type joint_program = { jp_functions : AST.ident List.list;
2538                       joint_prog : (joint_function, AST.init_data List.list)
2539                                    AST.program;
2540                       init_cost_label : CostLabel.costlabel }
2541
2542(** val joint_program_rect_Type4 :
2543    params -> (AST.ident List.list -> (joint_function, AST.init_data
2544    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2545    joint_program -> 'a1 **)
2546let rec joint_program_rect_Type4 p h_mk_joint_program x_18121 =
2547  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2548    init_cost_label = init_cost_label0 } = x_18121
2549  in
2550  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2551
2552(** val joint_program_rect_Type5 :
2553    params -> (AST.ident List.list -> (joint_function, AST.init_data
2554    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2555    joint_program -> 'a1 **)
2556let rec joint_program_rect_Type5 p h_mk_joint_program x_18123 =
2557  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2558    init_cost_label = init_cost_label0 } = x_18123
2559  in
2560  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2561
2562(** val joint_program_rect_Type3 :
2563    params -> (AST.ident List.list -> (joint_function, AST.init_data
2564    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2565    joint_program -> 'a1 **)
2566let rec joint_program_rect_Type3 p h_mk_joint_program x_18125 =
2567  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2568    init_cost_label = init_cost_label0 } = x_18125
2569  in
2570  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2571
2572(** val joint_program_rect_Type2 :
2573    params -> (AST.ident List.list -> (joint_function, AST.init_data
2574    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2575    joint_program -> 'a1 **)
2576let rec joint_program_rect_Type2 p h_mk_joint_program x_18127 =
2577  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2578    init_cost_label = init_cost_label0 } = x_18127
2579  in
2580  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2581
2582(** val joint_program_rect_Type1 :
2583    params -> (AST.ident List.list -> (joint_function, AST.init_data
2584    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2585    joint_program -> 'a1 **)
2586let rec joint_program_rect_Type1 p h_mk_joint_program x_18129 =
2587  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2588    init_cost_label = init_cost_label0 } = x_18129
2589  in
2590  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2591
2592(** val joint_program_rect_Type0 :
2593    params -> (AST.ident List.list -> (joint_function, AST.init_data
2594    List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2595    joint_program -> 'a1 **)
2596let rec joint_program_rect_Type0 p h_mk_joint_program x_18131 =
2597  let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2598    init_cost_label = init_cost_label0 } = x_18131
2599  in
2600  h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2601
2602(** val jp_functions : params -> joint_program -> AST.ident List.list **)
2603let rec jp_functions p xxx =
2604  xxx.jp_functions
2605
2606(** val joint_prog :
2607    params -> joint_program -> (joint_function, AST.init_data List.list)
2608    AST.program **)
2609let rec joint_prog p xxx =
2610  xxx.joint_prog
2611
2612(** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2613let rec init_cost_label p xxx =
2614  xxx.init_cost_label
2615
2616(** val joint_program_inv_rect_Type4 :
2617    params -> joint_program -> (AST.ident List.list -> (joint_function,
2618    AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2619    -> 'a1) -> 'a1 **)
2620let joint_program_inv_rect_Type4 x1 hterm h1 =
2621  let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2622
2623(** val joint_program_inv_rect_Type3 :
2624    params -> joint_program -> (AST.ident List.list -> (joint_function,
2625    AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2626    -> 'a1) -> 'a1 **)
2627let joint_program_inv_rect_Type3 x1 hterm h1 =
2628  let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2629
2630(** val joint_program_inv_rect_Type2 :
2631    params -> joint_program -> (AST.ident List.list -> (joint_function,
2632    AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2633    -> 'a1) -> 'a1 **)
2634let joint_program_inv_rect_Type2 x1 hterm h1 =
2635  let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2636
2637(** val joint_program_inv_rect_Type1 :
2638    params -> joint_program -> (AST.ident List.list -> (joint_function,
2639    AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2640    -> 'a1) -> 'a1 **)
2641let joint_program_inv_rect_Type1 x1 hterm h1 =
2642  let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2643
2644(** val joint_program_inv_rect_Type0 :
2645    params -> joint_program -> (AST.ident List.list -> (joint_function,
2646    AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2647    -> 'a1) -> 'a1 **)
2648let joint_program_inv_rect_Type0 x1 hterm h1 =
2649  let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2650
2651(** val joint_program_discr :
2652    params -> joint_program -> joint_program -> __ **)
2653let joint_program_discr a1 x y =
2654  Logic.eq_rect_Type2 x
2655    (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2656    Obj.magic (fun _ dH -> dH __ __ __ __)) y
2657
2658(** val joint_program_jmdiscr :
2659    params -> joint_program -> joint_program -> __ **)
2660let joint_program_jmdiscr a1 x y =
2661  Logic.eq_rect_Type2 x
2662    (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2663    Obj.magic (fun _ dH -> dH __ __ __ __)) y
2664
2665(** val dpi1__o__joint_prog__o__inject :
2666    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2667    AST.init_data List.list) AST.program Types.sig0 **)
2668let dpi1__o__joint_prog__o__inject x0 x2 =
2669  x2.Types.dpi1.joint_prog
2670
2671(** val eject__o__joint_prog__o__inject :
2672    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2673    List.list) AST.program Types.sig0 **)
2674let eject__o__joint_prog__o__inject x0 x2 =
2675  (Types.pi1 x2).joint_prog
2676
2677(** val joint_prog__o__inject :
2678    params -> joint_program -> (joint_function, AST.init_data List.list)
2679    AST.program Types.sig0 **)
2680let joint_prog__o__inject x0 x1 =
2681  x1.joint_prog
2682
2683(** val dpi1__o__joint_prog :
2684    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2685    AST.init_data List.list) AST.program **)
2686let dpi1__o__joint_prog x0 x2 =
2687  x2.Types.dpi1.joint_prog
2688
2689(** val eject__o__joint_prog :
2690    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2691    List.list) AST.program **)
2692let eject__o__joint_prog x0 x2 =
2693  (Types.pi1 x2).joint_prog
2694
2695(** val prog_names : params -> joint_program -> AST.ident List.list **)
2696let prog_names pars p =
2697  List.append (AST.prog_var_names p.joint_prog) p.jp_functions
2698
2699(** val transform_joint_program :
2700    params -> params -> (AST.ident List.list ->
2701    joint_closed_internal_function -> joint_closed_internal_function) ->
2702    joint_program -> joint_program **)
2703let transform_joint_program src dst trans prog_in =
2704  { jp_functions = prog_in.jp_functions; joint_prog =
2705    (AST.transform_program prog_in.joint_prog (fun vars ->
2706      AST.transf_fundef (trans (List.append vars prog_in.jp_functions))));
2707    init_cost_label = prog_in.init_cost_label }
2708
2709type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2710
2711(** val stack_cost : params -> joint_program -> stack_cost_model **)
2712let stack_cost p pr =
2713  List.foldr (fun id_fun acc ->
2714    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2715    (match fun0 with
2716     | AST.Internal jif ->
2717       List.Cons ({ Types.fst = id; Types.snd =
2718         (Types.pi1 jif).joint_if_stacksize }, acc)
2719     | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
2720
2721open Extra_bool
2722
2723open Coqlib
2724
2725open Values
2726
2727open FrontEndVal
2728
2729open GenMem
2730
2731open FrontEndMem
2732
2733open Globalenvs
2734
2735(** val globals_stacksize : params -> joint_program -> Nat.nat **)
2736let globals_stacksize pars p =
2737  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2738    Globalenvs.size_init_data_list entry.Types.snd)
2739    p.joint_prog.AST.prog_vars
2740
Note: See TracBrowser for help on using the repository browser.