source: extracted/joint.ml @ 2997

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

New extraction.

File size: 110.3 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_224 -> h_Reg x_224
113| Imm x_225 -> h_Imm x_225
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_229 -> h_Reg x_229
119| Imm x_230 -> h_Imm x_230
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_234 -> h_Reg x_234
125| Imm x_235 -> h_Imm x_235
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_239 -> h_Reg x_239
131| Imm x_240 -> h_Imm x_240
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_244 -> h_Reg x_244
137| Imm x_245 -> h_Imm x_245
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_249 -> h_Reg x_249
143| Imm x_250 -> h_Imm x_250
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_285 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_285
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_287 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_287
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_289 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_289
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_291 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_291
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_293 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_293
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_295 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_295
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_312 =
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_312
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_314 =
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_314
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_316 =
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_316
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_318 =
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_318
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_320 =
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_320
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_322 =
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_322
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_352 =
808  let { u_pars = u_pars0; functs = functs0 } = x_352 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_354 =
815  let { u_pars = u_pars0; functs = functs0 } = x_354 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_356 =
822  let { u_pars = u_pars0; functs = functs0 } = x_356 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_358 =
829  let { u_pars = u_pars0; functs = functs0 } = x_358 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_360 =
836  let { u_pars = u_pars0; functs = functs0 } = x_360 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_362 =
843  let { u_pars = u_pars0; functs = functs0 } = x_362 in
844  h_mk_uns_params u_pars0 functs0
845
846(** val u_pars : uns_params -> unserialized_params **)
847let rec u_pars xxx =
848  xxx.u_pars
849
850(** val functs : uns_params -> get_pseudo_reg_functs **)
851let rec functs xxx =
852  xxx.functs
853
854(** val uns_params_inv_rect_Type4 :
855    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
856    -> 'a1 **)
857let uns_params_inv_rect_Type4 hterm h1 =
858  let hcut = uns_params_rect_Type4 h1 hterm in hcut __
859
860(** val uns_params_inv_rect_Type3 :
861    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
862    -> 'a1 **)
863let uns_params_inv_rect_Type3 hterm h1 =
864  let hcut = uns_params_rect_Type3 h1 hterm in hcut __
865
866(** val uns_params_inv_rect_Type2 :
867    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
868    -> 'a1 **)
869let uns_params_inv_rect_Type2 hterm h1 =
870  let hcut = uns_params_rect_Type2 h1 hterm in hcut __
871
872(** val uns_params_inv_rect_Type1 :
873    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
874    -> 'a1 **)
875let uns_params_inv_rect_Type1 hterm h1 =
876  let hcut = uns_params_rect_Type1 h1 hterm in hcut __
877
878(** val uns_params_inv_rect_Type0 :
879    uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
880    -> 'a1 **)
881let uns_params_inv_rect_Type0 hterm h1 =
882  let hcut = uns_params_rect_Type0 h1 hterm in hcut __
883
884(** val uns_params_jmdiscr : uns_params -> uns_params -> __ **)
885let uns_params_jmdiscr x y =
886  Logic.eq_rect_Type2 x
887    (let { u_pars = a0; functs = a1 } = x in
888    Obj.magic (fun _ dH -> dH __ __)) y
889
890type joint_seq =
891| COMMENT of String.string
892| MOVE of __
893| POP of __
894| PUSH of __
895| ADDRESS of AST.ident * __ * __
896| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
897| OP1 of BackEndOps.op1 * __ * __
898| OP2 of BackEndOps.op2 * __ * __ * __
899| CLEAR_CARRY
900| SET_CARRY
901| LOAD of __ * __ * __
902| STORE of __ * __ * __
903| Extension_seq of __
904
905(** val joint_seq_rect_Type4 :
906    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
907    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
908    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
909    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
910    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
911    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
912let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
913| COMMENT x_417 -> h_COMMENT x_417
914| MOVE x_418 -> h_MOVE x_418
915| POP x_419 -> h_POP x_419
916| PUSH x_420 -> h_PUSH x_420
917| ADDRESS (i, x_422, x_421) -> h_ADDRESS i __ x_422 x_421
918| OPACCS (x_428, x_427, x_426, x_425, x_424) ->
919  h_OPACCS x_428 x_427 x_426 x_425 x_424
920| OP1 (x_431, x_430, x_429) -> h_OP1 x_431 x_430 x_429
921| OP2 (x_435, x_434, x_433, x_432) -> h_OP2 x_435 x_434 x_433 x_432
922| CLEAR_CARRY -> h_CLEAR_CARRY
923| SET_CARRY -> h_SET_CARRY
924| LOAD (x_438, x_437, x_436) -> h_LOAD x_438 x_437 x_436
925| STORE (x_441, x_440, x_439) -> h_STORE x_441 x_440 x_439
926| Extension_seq x_442 -> h_extension_seq x_442
927
928(** val joint_seq_rect_Type5 :
929    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
930    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
931    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
932    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
933    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
934    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
935let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
936| COMMENT x_457 -> h_COMMENT x_457
937| MOVE x_458 -> h_MOVE x_458
938| POP x_459 -> h_POP x_459
939| PUSH x_460 -> h_PUSH x_460
940| ADDRESS (i, x_462, x_461) -> h_ADDRESS i __ x_462 x_461
941| OPACCS (x_468, x_467, x_466, x_465, x_464) ->
942  h_OPACCS x_468 x_467 x_466 x_465 x_464
943| OP1 (x_471, x_470, x_469) -> h_OP1 x_471 x_470 x_469
944| OP2 (x_475, x_474, x_473, x_472) -> h_OP2 x_475 x_474 x_473 x_472
945| CLEAR_CARRY -> h_CLEAR_CARRY
946| SET_CARRY -> h_SET_CARRY
947| LOAD (x_478, x_477, x_476) -> h_LOAD x_478 x_477 x_476
948| STORE (x_481, x_480, x_479) -> h_STORE x_481 x_480 x_479
949| Extension_seq x_482 -> h_extension_seq x_482
950
951(** val joint_seq_rect_Type3 :
952    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
953    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
954    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
955    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
956    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
957    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
958let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
959| COMMENT x_497 -> h_COMMENT x_497
960| MOVE x_498 -> h_MOVE x_498
961| POP x_499 -> h_POP x_499
962| PUSH x_500 -> h_PUSH x_500
963| ADDRESS (i, x_502, x_501) -> h_ADDRESS i __ x_502 x_501
964| OPACCS (x_508, x_507, x_506, x_505, x_504) ->
965  h_OPACCS x_508 x_507 x_506 x_505 x_504
966| OP1 (x_511, x_510, x_509) -> h_OP1 x_511 x_510 x_509
967| OP2 (x_515, x_514, x_513, x_512) -> h_OP2 x_515 x_514 x_513 x_512
968| CLEAR_CARRY -> h_CLEAR_CARRY
969| SET_CARRY -> h_SET_CARRY
970| LOAD (x_518, x_517, x_516) -> h_LOAD x_518 x_517 x_516
971| STORE (x_521, x_520, x_519) -> h_STORE x_521 x_520 x_519
972| Extension_seq x_522 -> h_extension_seq x_522
973
974(** val joint_seq_rect_Type2 :
975    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
976    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
977    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
978    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
979    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
980    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
981let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
982| COMMENT x_537 -> h_COMMENT x_537
983| MOVE x_538 -> h_MOVE x_538
984| POP x_539 -> h_POP x_539
985| PUSH x_540 -> h_PUSH x_540
986| ADDRESS (i, x_542, x_541) -> h_ADDRESS i __ x_542 x_541
987| OPACCS (x_548, x_547, x_546, x_545, x_544) ->
988  h_OPACCS x_548 x_547 x_546 x_545 x_544
989| OP1 (x_551, x_550, x_549) -> h_OP1 x_551 x_550 x_549
990| OP2 (x_555, x_554, x_553, x_552) -> h_OP2 x_555 x_554 x_553 x_552
991| CLEAR_CARRY -> h_CLEAR_CARRY
992| SET_CARRY -> h_SET_CARRY
993| LOAD (x_558, x_557, x_556) -> h_LOAD x_558 x_557 x_556
994| STORE (x_561, x_560, x_559) -> h_STORE x_561 x_560 x_559
995| Extension_seq x_562 -> h_extension_seq x_562
996
997(** val joint_seq_rect_Type1 :
998    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
999    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1000    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1001    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1002    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1003    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1004let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
1005| COMMENT x_577 -> h_COMMENT x_577
1006| MOVE x_578 -> h_MOVE x_578
1007| POP x_579 -> h_POP x_579
1008| PUSH x_580 -> h_PUSH x_580
1009| ADDRESS (i, x_582, x_581) -> h_ADDRESS i __ x_582 x_581
1010| OPACCS (x_588, x_587, x_586, x_585, x_584) ->
1011  h_OPACCS x_588 x_587 x_586 x_585 x_584
1012| OP1 (x_591, x_590, x_589) -> h_OP1 x_591 x_590 x_589
1013| OP2 (x_595, x_594, x_593, x_592) -> h_OP2 x_595 x_594 x_593 x_592
1014| CLEAR_CARRY -> h_CLEAR_CARRY
1015| SET_CARRY -> h_SET_CARRY
1016| LOAD (x_598, x_597, x_596) -> h_LOAD x_598 x_597 x_596
1017| STORE (x_601, x_600, x_599) -> h_STORE x_601 x_600 x_599
1018| Extension_seq x_602 -> h_extension_seq x_602
1019
1020(** val joint_seq_rect_Type0 :
1021    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1022    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1023    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1024    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1025    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1026    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1027let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
1028| COMMENT x_617 -> h_COMMENT x_617
1029| MOVE x_618 -> h_MOVE x_618
1030| POP x_619 -> h_POP x_619
1031| PUSH x_620 -> h_PUSH x_620
1032| ADDRESS (i, x_622, x_621) -> h_ADDRESS i __ x_622 x_621
1033| OPACCS (x_628, x_627, x_626, x_625, x_624) ->
1034  h_OPACCS x_628 x_627 x_626 x_625 x_624
1035| OP1 (x_631, x_630, x_629) -> h_OP1 x_631 x_630 x_629
1036| OP2 (x_635, x_634, x_633, x_632) -> h_OP2 x_635 x_634 x_633 x_632
1037| CLEAR_CARRY -> h_CLEAR_CARRY
1038| SET_CARRY -> h_SET_CARRY
1039| LOAD (x_638, x_637, x_636) -> h_LOAD x_638 x_637 x_636
1040| STORE (x_641, x_640, x_639) -> h_STORE x_641 x_640 x_639
1041| Extension_seq x_642 -> h_extension_seq x_642
1042
1043(** val joint_seq_inv_rect_Type4 :
1044    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1045    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1046    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1047    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1048    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1049    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1050    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1051let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1052  let hcut =
1053    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1054      hterm
1055  in
1056  hcut __
1057
1058(** val joint_seq_inv_rect_Type3 :
1059    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1060    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1061    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1062    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1063    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1064    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1065    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1066let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1067  let hcut =
1068    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1069      hterm
1070  in
1071  hcut __
1072
1073(** val joint_seq_inv_rect_Type2 :
1074    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1075    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1076    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1077    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1078    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1079    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1080    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1081let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1082  let hcut =
1083    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1084      hterm
1085  in
1086  hcut __
1087
1088(** val joint_seq_inv_rect_Type1 :
1089    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1090    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1091    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1092    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1093    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1094    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1095    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1096let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1097  let hcut =
1098    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1099      hterm
1100  in
1101  hcut __
1102
1103(** val joint_seq_inv_rect_Type0 :
1104    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1105    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1106    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1107    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1108    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1109    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1110    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1111let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1112  let hcut =
1113    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1114      hterm
1115  in
1116  hcut __
1117
1118(** val joint_seq_discr :
1119    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1120    __ **)
1121let joint_seq_discr a1 a2 x y =
1122  Logic.eq_rect_Type2 x
1123    (match x with
1124     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1125     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1126     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1127     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1128     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1129     | OPACCS (a0, a10, a20, a3, a4) ->
1130       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1131     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1132     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1133     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1134     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1135     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1136     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1137     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1138
1139(** val joint_seq_jmdiscr :
1140    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1141    __ **)
1142let joint_seq_jmdiscr a1 a2 x y =
1143  Logic.eq_rect_Type2 x
1144    (match x with
1145     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1146     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1147     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1148     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1149     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1150     | OPACCS (a0, a10, a20, a3, a4) ->
1151       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1152     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1153     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1154     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1155     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1156     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1157     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1158     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1159
1160(** val get_used_registers_from_seq :
1161    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1162    joint_seq -> Registers.register List.list **)
1163let get_used_registers_from_seq p globals functs0 = function
1164| COMMENT x -> List.Nil
1165| MOVE pm -> functs0.pair_move_regs pm
1166| POP r -> functs0.acc_a_regs r
1167| PUSH r -> functs0.acc_a_args r
1168| ADDRESS (i, r1, r2) ->
1169  List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1170| OPACCS (o, r1, r2, r3, r4) ->
1171  List.append (functs0.acc_a_regs r1)
1172    (List.append (functs0.acc_b_regs r2)
1173      (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1174| OP1 (o, r1, r2) ->
1175  List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1176| OP2 (o, r1, r2, r3) ->
1177  List.append (functs0.acc_a_regs r1)
1178    (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1179| CLEAR_CARRY -> List.Nil
1180| SET_CARRY -> List.Nil
1181| LOAD (r1, r2, r3) ->
1182  List.append (functs0.acc_a_regs r1)
1183    (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1184| STORE (r1, r2, r3) ->
1185  List.append (functs0.dpl_args r1)
1186    (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1187| Extension_seq ext -> functs0.ext_seq_regs ext
1188
1189(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1190let nOOP p globals =
1191  COMMENT String.EmptyString
1192
1193(** val dpi1__o__extension_seq_to_seq__o__inject :
1194    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1195    joint_seq Types.sig0 **)
1196let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1197  Extension_seq x4.Types.dpi1
1198
1199(** val eject__o__extension_seq_to_seq__o__inject :
1200    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1201    Types.sig0 **)
1202let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1203  Extension_seq (Types.pi1 x4)
1204
1205(** val extension_seq_to_seq__o__inject :
1206    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1207let extension_seq_to_seq__o__inject x0 x1 x3 =
1208  Extension_seq x3
1209
1210(** val dpi1__o__extension_seq_to_seq :
1211    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1212    joint_seq **)
1213let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1214  Extension_seq x3.Types.dpi1
1215
1216(** val eject__o__extension_seq_to_seq :
1217    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1218let eject__o__extension_seq_to_seq x0 x1 x3 =
1219  Extension_seq (Types.pi1 x3)
1220
1221type joint_step =
1222| COST_LABEL of CostLabel.costlabel
1223| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1224| COND of __ * Graphs.label
1225| Step_seq of joint_seq
1226
1227(** val joint_step_rect_Type4 :
1228    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1229    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1230    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1231let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1232| COST_LABEL x_909 -> h_COST_LABEL x_909
1233| CALL (x_912, x_911, x_910) -> h_CALL x_912 x_911 x_910
1234| COND (x_914, x_913) -> h_COND x_914 x_913
1235| Step_seq x_915 -> h_step_seq x_915
1236
1237(** val joint_step_rect_Type5 :
1238    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1239    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1240    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1241let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1242| COST_LABEL x_921 -> h_COST_LABEL x_921
1243| CALL (x_924, x_923, x_922) -> h_CALL x_924 x_923 x_922
1244| COND (x_926, x_925) -> h_COND x_926 x_925
1245| Step_seq x_927 -> h_step_seq x_927
1246
1247(** val joint_step_rect_Type3 :
1248    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1249    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1250    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1251let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1252| COST_LABEL x_933 -> h_COST_LABEL x_933
1253| CALL (x_936, x_935, x_934) -> h_CALL x_936 x_935 x_934
1254| COND (x_938, x_937) -> h_COND x_938 x_937
1255| Step_seq x_939 -> h_step_seq x_939
1256
1257(** val joint_step_rect_Type2 :
1258    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1259    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1260    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1261let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1262| COST_LABEL x_945 -> h_COST_LABEL x_945
1263| CALL (x_948, x_947, x_946) -> h_CALL x_948 x_947 x_946
1264| COND (x_950, x_949) -> h_COND x_950 x_949
1265| Step_seq x_951 -> h_step_seq x_951
1266
1267(** val joint_step_rect_Type1 :
1268    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1269    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1270    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1271let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1272| COST_LABEL x_957 -> h_COST_LABEL x_957
1273| CALL (x_960, x_959, x_958) -> h_CALL x_960 x_959 x_958
1274| COND (x_962, x_961) -> h_COND x_962 x_961
1275| Step_seq x_963 -> h_step_seq x_963
1276
1277(** val joint_step_rect_Type0 :
1278    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1279    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1280    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1281let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1282| COST_LABEL x_969 -> h_COST_LABEL x_969
1283| CALL (x_972, x_971, x_970) -> h_CALL x_972 x_971 x_970
1284| COND (x_974, x_973) -> h_COND x_974 x_973
1285| Step_seq x_975 -> h_step_seq x_975
1286
1287(** val joint_step_inv_rect_Type4 :
1288    unserialized_params -> AST.ident List.list -> joint_step ->
1289    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1290    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1291    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1292let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1293  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1294
1295(** val joint_step_inv_rect_Type3 :
1296    unserialized_params -> AST.ident List.list -> joint_step ->
1297    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1298    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1299    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1300let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1301  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1302
1303(** val joint_step_inv_rect_Type2 :
1304    unserialized_params -> AST.ident List.list -> joint_step ->
1305    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1306    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1307    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1308let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1309  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1310
1311(** val joint_step_inv_rect_Type1 :
1312    unserialized_params -> AST.ident List.list -> joint_step ->
1313    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1314    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1315    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1316let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1317  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1318
1319(** val joint_step_inv_rect_Type0 :
1320    unserialized_params -> AST.ident List.list -> joint_step ->
1321    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1322    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1323    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1324let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1325  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1326
1327(** val joint_step_discr :
1328    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1329    __ **)
1330let joint_step_discr a1 a2 x y =
1331  Logic.eq_rect_Type2 x
1332    (match x with
1333     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1334     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1335     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1336     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1337
1338(** val joint_step_jmdiscr :
1339    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1340    __ **)
1341let joint_step_jmdiscr a1 a2 x y =
1342  Logic.eq_rect_Type2 x
1343    (match x with
1344     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1345     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1346     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1347     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1348
1349(** val get_used_registers_from_step :
1350    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1351    joint_step -> Registers.register List.list **)
1352let get_used_registers_from_step p globals functs0 = function
1353| COST_LABEL c -> List.Nil
1354| CALL (id, args, dest) ->
1355  let r_id =
1356    match id with
1357    | Types.Inl x -> List.Nil
1358    | Types.Inr ptr ->
1359      List.append (functs0.dpl_args ptr.Types.fst)
1360        (functs0.dph_args ptr.Types.snd)
1361  in
1362  List.append r_id
1363    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1364| COND (r, lbl) -> functs0.acc_a_regs r
1365| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1366
1367(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1368    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1369    joint_step Types.sig0 **)
1370let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1371  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1372
1373(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1374    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1375    Types.sig0 **)
1376let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1377  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1378
1379(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1380    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1381let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1382  Step_seq (Extension_seq x2)
1383
1384(** val dpi1__o__seq_to_step__o__inject :
1385    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1386    Types.dPair -> joint_step Types.sig0 **)
1387let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1388  Step_seq x4.Types.dpi1
1389
1390(** val eject__o__seq_to_step__o__inject :
1391    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1392    joint_step Types.sig0 **)
1393let eject__o__seq_to_step__o__inject x0 x1 x4 =
1394  Step_seq (Types.pi1 x4)
1395
1396(** val seq_to_step__o__inject :
1397    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1398    Types.sig0 **)
1399let seq_to_step__o__inject x0 x1 x3 =
1400  Step_seq x3
1401
1402(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1403    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1404    joint_step **)
1405let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1406  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1407
1408(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1409    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1410let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1411  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1412
1413(** val extension_seq_to_seq__o__seq_to_step :
1414    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1415let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1416  Step_seq (Extension_seq x2)
1417
1418(** val dpi1__o__seq_to_step :
1419    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1420    Types.dPair -> joint_step **)
1421let dpi1__o__seq_to_step x0 x1 x3 =
1422  Step_seq x3.Types.dpi1
1423
1424(** val eject__o__seq_to_step :
1425    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1426    joint_step **)
1427let eject__o__seq_to_step x0 x1 x3 =
1428  Step_seq (Types.pi1 x3)
1429
1430(** val step_labels :
1431    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1432    List.list **)
1433let step_labels p globals = function
1434| COST_LABEL x -> List.Nil
1435| CALL (x, x0, x1) -> List.Nil
1436| COND (x, l) -> List.Cons (l, List.Nil)
1437| Step_seq s0 ->
1438  (match s0 with
1439   | COMMENT x -> List.Nil
1440   | MOVE x -> List.Nil
1441   | POP x -> List.Nil
1442   | PUSH x -> List.Nil
1443   | ADDRESS (x, x1, x2) -> List.Nil
1444   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1445   | OP1 (x, x0, x1) -> List.Nil
1446   | OP2 (x, x0, x1, x2) -> List.Nil
1447   | CLEAR_CARRY -> List.Nil
1448   | SET_CARRY -> List.Nil
1449   | LOAD (x, x0, x1) -> List.Nil
1450   | STORE (x, x0, x1) -> List.Nil
1451   | Extension_seq ext -> p.ext_seq_labels ext)
1452
1453type stmt_params = { uns_pars : uns_params;
1454                     succ_label : (__ -> Graphs.label Types.option);
1455                     has_fcond : Bool.bool }
1456
1457(** val stmt_params_rect_Type4 :
1458    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1459    'a1) -> stmt_params -> 'a1 **)
1460let rec stmt_params_rect_Type4 h_mk_stmt_params x_1054 =
1461  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1462    has_fcond0 } = x_1054
1463  in
1464  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1465
1466(** val stmt_params_rect_Type5 :
1467    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1468    'a1) -> stmt_params -> 'a1 **)
1469let rec stmt_params_rect_Type5 h_mk_stmt_params x_1056 =
1470  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1471    has_fcond0 } = x_1056
1472  in
1473  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1474
1475(** val stmt_params_rect_Type3 :
1476    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1477    'a1) -> stmt_params -> 'a1 **)
1478let rec stmt_params_rect_Type3 h_mk_stmt_params x_1058 =
1479  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1480    has_fcond0 } = x_1058
1481  in
1482  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1483
1484(** val stmt_params_rect_Type2 :
1485    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1486    'a1) -> stmt_params -> 'a1 **)
1487let rec stmt_params_rect_Type2 h_mk_stmt_params x_1060 =
1488  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1489    has_fcond0 } = x_1060
1490  in
1491  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1492
1493(** val stmt_params_rect_Type1 :
1494    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1495    'a1) -> stmt_params -> 'a1 **)
1496let rec stmt_params_rect_Type1 h_mk_stmt_params x_1062 =
1497  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1498    has_fcond0 } = x_1062
1499  in
1500  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1501
1502(** val stmt_params_rect_Type0 :
1503    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1504    'a1) -> stmt_params -> 'a1 **)
1505let rec stmt_params_rect_Type0 h_mk_stmt_params x_1064 =
1506  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1507    has_fcond0 } = x_1064
1508  in
1509  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1510
1511(** val uns_pars : stmt_params -> uns_params **)
1512let rec uns_pars xxx =
1513  xxx.uns_pars
1514
1515type succ = __
1516
1517(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1518let rec succ_label xxx =
1519  xxx.succ_label
1520
1521(** val has_fcond : stmt_params -> Bool.bool **)
1522let rec has_fcond xxx =
1523  xxx.has_fcond
1524
1525(** val stmt_params_inv_rect_Type4 :
1526    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1527    Bool.bool -> __ -> 'a1) -> 'a1 **)
1528let stmt_params_inv_rect_Type4 hterm h1 =
1529  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1530
1531(** val stmt_params_inv_rect_Type3 :
1532    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1533    Bool.bool -> __ -> 'a1) -> 'a1 **)
1534let stmt_params_inv_rect_Type3 hterm h1 =
1535  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1536
1537(** val stmt_params_inv_rect_Type2 :
1538    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539    Bool.bool -> __ -> 'a1) -> 'a1 **)
1540let stmt_params_inv_rect_Type2 hterm h1 =
1541  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1542
1543(** val stmt_params_inv_rect_Type1 :
1544    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545    Bool.bool -> __ -> 'a1) -> 'a1 **)
1546let stmt_params_inv_rect_Type1 hterm h1 =
1547  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1548
1549(** val stmt_params_inv_rect_Type0 :
1550    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551    Bool.bool -> __ -> 'a1) -> 'a1 **)
1552let stmt_params_inv_rect_Type0 hterm h1 =
1553  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1554
1555(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1556let stmt_params_jmdiscr x y =
1557  Logic.eq_rect_Type2 x
1558    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1559    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1560
1561(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1562let uns_pars__o__u_pars x0 =
1563  x0.uns_pars.u_pars
1564
1565type joint_fin_step =
1566| GOTO of Graphs.label
1567| RETURN
1568| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1569
1570(** val joint_fin_step_rect_Type4 :
1571    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1572    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1573let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1574| GOTO x_1088 -> h_GOTO x_1088
1575| RETURN -> h_RETURN
1576| TAILCALL (x_1090, x_1089) -> h_TAILCALL __ x_1090 x_1089
1577
1578(** val joint_fin_step_rect_Type5 :
1579    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1580    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1581let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1582| GOTO x_1096 -> h_GOTO x_1096
1583| RETURN -> h_RETURN
1584| TAILCALL (x_1098, x_1097) -> h_TAILCALL __ x_1098 x_1097
1585
1586(** val joint_fin_step_rect_Type3 :
1587    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1588    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1589let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1590| GOTO x_1104 -> h_GOTO x_1104
1591| RETURN -> h_RETURN
1592| TAILCALL (x_1106, x_1105) -> h_TAILCALL __ x_1106 x_1105
1593
1594(** val joint_fin_step_rect_Type2 :
1595    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1596    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1597let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1598| GOTO x_1112 -> h_GOTO x_1112
1599| RETURN -> h_RETURN
1600| TAILCALL (x_1114, x_1113) -> h_TAILCALL __ x_1114 x_1113
1601
1602(** val joint_fin_step_rect_Type1 :
1603    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1604    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1605let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1606| GOTO x_1120 -> h_GOTO x_1120
1607| RETURN -> h_RETURN
1608| TAILCALL (x_1122, x_1121) -> h_TAILCALL __ x_1122 x_1121
1609
1610(** val joint_fin_step_rect_Type0 :
1611    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1612    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1613let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1614| GOTO x_1128 -> h_GOTO x_1128
1615| RETURN -> h_RETURN
1616| TAILCALL (x_1130, x_1129) -> h_TAILCALL __ x_1130 x_1129
1617
1618(** val joint_fin_step_inv_rect_Type4 :
1619    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1620    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1621    __ -> 'a1) -> 'a1 **)
1622let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1623  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1624
1625(** val joint_fin_step_inv_rect_Type3 :
1626    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1627    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1628    __ -> 'a1) -> 'a1 **)
1629let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1630  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1631
1632(** val joint_fin_step_inv_rect_Type2 :
1633    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1634    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1635    __ -> 'a1) -> 'a1 **)
1636let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1637  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1638
1639(** val joint_fin_step_inv_rect_Type1 :
1640    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1641    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1642    __ -> 'a1) -> 'a1 **)
1643let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1644  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1645
1646(** val joint_fin_step_inv_rect_Type0 :
1647    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1648    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1649    __ -> 'a1) -> 'a1 **)
1650let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1651  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1652
1653(** val joint_fin_step_discr :
1654    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1655let joint_fin_step_discr a1 x y =
1656  Logic.eq_rect_Type2 x
1657    (match x with
1658     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1659     | RETURN -> Obj.magic (fun _ dH -> dH)
1660     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1661
1662(** val joint_fin_step_jmdiscr :
1663    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1664let joint_fin_step_jmdiscr a1 x y =
1665  Logic.eq_rect_Type2 x
1666    (match x with
1667     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1668     | RETURN -> Obj.magic (fun _ dH -> dH)
1669     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1670
1671(** val fin_step_labels :
1672    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1673let fin_step_labels p = function
1674| GOTO l -> List.Cons (l, List.Nil)
1675| RETURN -> List.Nil
1676| TAILCALL (x0, x1) -> List.Nil
1677
1678type joint_statement =
1679| Sequential of joint_step * __
1680| Final of joint_fin_step
1681| FCOND of __ * Graphs.label * Graphs.label
1682
1683(** val joint_statement_rect_Type4 :
1684    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1685    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1686    'a1) -> joint_statement -> 'a1 **)
1687let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1688| Sequential (x_1196, x_1195) -> h_sequential x_1196 x_1195
1689| Final x_1197 -> h_final x_1197
1690| FCOND (x_1200, x_1199, x_1198) -> h_FCOND __ x_1200 x_1199 x_1198
1691
1692(** val joint_statement_rect_Type5 :
1693    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1694    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1695    'a1) -> joint_statement -> 'a1 **)
1696let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1697| Sequential (x_1207, x_1206) -> h_sequential x_1207 x_1206
1698| Final x_1208 -> h_final x_1208
1699| FCOND (x_1211, x_1210, x_1209) -> h_FCOND __ x_1211 x_1210 x_1209
1700
1701(** val joint_statement_rect_Type3 :
1702    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1703    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1704    'a1) -> joint_statement -> 'a1 **)
1705let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1706| Sequential (x_1218, x_1217) -> h_sequential x_1218 x_1217
1707| Final x_1219 -> h_final x_1219
1708| FCOND (x_1222, x_1221, x_1220) -> h_FCOND __ x_1222 x_1221 x_1220
1709
1710(** val joint_statement_rect_Type2 :
1711    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1712    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1713    'a1) -> joint_statement -> 'a1 **)
1714let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1715| Sequential (x_1229, x_1228) -> h_sequential x_1229 x_1228
1716| Final x_1230 -> h_final x_1230
1717| FCOND (x_1233, x_1232, x_1231) -> h_FCOND __ x_1233 x_1232 x_1231
1718
1719(** val joint_statement_rect_Type1 :
1720    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1721    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1722    'a1) -> joint_statement -> 'a1 **)
1723let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1724| Sequential (x_1240, x_1239) -> h_sequential x_1240 x_1239
1725| Final x_1241 -> h_final x_1241
1726| FCOND (x_1244, x_1243, x_1242) -> h_FCOND __ x_1244 x_1243 x_1242
1727
1728(** val joint_statement_rect_Type0 :
1729    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1730    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1731    'a1) -> joint_statement -> 'a1 **)
1732let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1733| Sequential (x_1251, x_1250) -> h_sequential x_1251 x_1250
1734| Final x_1252 -> h_final x_1252
1735| FCOND (x_1255, x_1254, x_1253) -> h_FCOND __ x_1255 x_1254 x_1253
1736
1737(** val joint_statement_inv_rect_Type4 :
1738    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1739    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1740    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1741let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1742  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1743
1744(** val joint_statement_inv_rect_Type3 :
1745    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1746    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1747    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1748let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1749  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1750
1751(** val joint_statement_inv_rect_Type2 :
1752    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1753    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1754    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1755let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1756  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1757
1758(** val joint_statement_inv_rect_Type1 :
1759    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1760    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1761    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1762let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1763  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1764
1765(** val joint_statement_inv_rect_Type0 :
1766    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1767    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1768    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1769let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1770  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1771
1772(** val joint_statement_discr :
1773    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1774    -> __ **)
1775let joint_statement_discr a1 a2 x y =
1776  Logic.eq_rect_Type2 x
1777    (match x with
1778     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1779     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1780     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1781
1782(** val joint_statement_jmdiscr :
1783    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1784    -> __ **)
1785let joint_statement_jmdiscr a1 a2 x y =
1786  Logic.eq_rect_Type2 x
1787    (match x with
1788     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1789     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1790     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1791
1792(** val dpi1__o__fin_step_to_stmt__o__inject :
1793    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1794    -> joint_statement Types.sig0 **)
1795let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1796  Final x4.Types.dpi1
1797
1798(** val eject__o__fin_step_to_stmt__o__inject :
1799    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1800    joint_statement Types.sig0 **)
1801let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1802  Final (Types.pi1 x4)
1803
1804(** val fin_step_to_stmt__o__inject :
1805    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1806    Types.sig0 **)
1807let fin_step_to_stmt__o__inject x0 x1 x3 =
1808  Final x3
1809
1810(** val dpi1__o__fin_step_to_stmt :
1811    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1812    -> joint_statement **)
1813let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1814  Final x3.Types.dpi1
1815
1816(** val eject__o__fin_step_to_stmt :
1817    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1818    joint_statement **)
1819let eject__o__fin_step_to_stmt x0 x1 x3 =
1820  Final (Types.pi1 x3)
1821
1822type params = { stmt_pars : stmt_params;
1823                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1824                          Types.option);
1825                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1826                                 -> __ Types.option);
1827                point_of_succ : (__ -> __ -> __) }
1828
1829(** val params_rect_Type4 :
1830    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1831    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1832    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1833    'a1 **)
1834let rec params_rect_Type4 h_mk_params x_1328 =
1835  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1836    point_of_label0; point_of_succ = point_of_succ0 } = x_1328
1837  in
1838  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1839
1840(** val params_rect_Type5 :
1841    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1842    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1843    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1844    'a1 **)
1845let rec params_rect_Type5 h_mk_params x_1330 =
1846  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1847    point_of_label0; point_of_succ = point_of_succ0 } = x_1330
1848  in
1849  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1850
1851(** val params_rect_Type3 :
1852    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1853    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1854    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1855    'a1 **)
1856let rec params_rect_Type3 h_mk_params x_1332 =
1857  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1858    point_of_label0; point_of_succ = point_of_succ0 } = x_1332
1859  in
1860  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1861
1862(** val params_rect_Type2 :
1863    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1864    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1865    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1866    'a1 **)
1867let rec params_rect_Type2 h_mk_params x_1334 =
1868  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1869    point_of_label0; point_of_succ = point_of_succ0 } = x_1334
1870  in
1871  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1872
1873(** val params_rect_Type1 :
1874    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1875    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1876    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1877    'a1 **)
1878let rec params_rect_Type1 h_mk_params x_1336 =
1879  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1880    point_of_label0; point_of_succ = point_of_succ0 } = x_1336
1881  in
1882  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1883
1884(** val params_rect_Type0 :
1885    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1886    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1887    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1888    'a1 **)
1889let rec params_rect_Type0 h_mk_params x_1338 =
1890  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1891    point_of_label0; point_of_succ = point_of_succ0 } = x_1338
1892  in
1893  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1894
1895(** val stmt_pars : params -> stmt_params **)
1896let rec stmt_pars xxx =
1897  xxx.stmt_pars
1898
1899type codeT = __
1900
1901type code_point = __
1902
1903(** val stmt_at :
1904    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1905let rec stmt_at xxx =
1906  xxx.stmt_at
1907
1908(** val point_of_label :
1909    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1910let rec point_of_label xxx =
1911  xxx.point_of_label
1912
1913(** val point_of_succ : params -> __ -> __ -> __ **)
1914let rec point_of_succ xxx =
1915  xxx.point_of_succ
1916
1917(** val params_inv_rect_Type4 :
1918    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1919    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1920    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1921let params_inv_rect_Type4 hterm h1 =
1922  let hcut = params_rect_Type4 h1 hterm in hcut __
1923
1924(** val params_inv_rect_Type3 :
1925    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1926    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1927    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1928let params_inv_rect_Type3 hterm h1 =
1929  let hcut = params_rect_Type3 h1 hterm in hcut __
1930
1931(** val params_inv_rect_Type2 :
1932    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1933    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1934    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1935let params_inv_rect_Type2 hterm h1 =
1936  let hcut = params_rect_Type2 h1 hterm in hcut __
1937
1938(** val params_inv_rect_Type1 :
1939    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1940    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1941    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1942let params_inv_rect_Type1 hterm h1 =
1943  let hcut = params_rect_Type1 h1 hterm in hcut __
1944
1945(** val params_inv_rect_Type0 :
1946    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1947    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1948    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1949let params_inv_rect_Type0 hterm h1 =
1950  let hcut = params_rect_Type0 h1 hterm in hcut __
1951
1952(** val params_jmdiscr : params -> params -> __ **)
1953let params_jmdiscr x y =
1954  Logic.eq_rect_Type2 x
1955    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1956       a5 } = x
1957     in
1958    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1959
1960(** val stmt_pars__o__uns_pars : params -> uns_params **)
1961let stmt_pars__o__uns_pars x0 =
1962  x0.stmt_pars.uns_pars
1963
1964(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1965let stmt_pars__o__uns_pars__o__u_pars x0 =
1966  uns_pars__o__u_pars x0.stmt_pars
1967
1968(** val code_has_point :
1969    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1970let code_has_point p globals c pt =
1971  match p.stmt_at globals c pt with
1972  | Types.None -> Bool.False
1973  | Types.Some x -> Bool.True
1974
1975(** val code_has_label :
1976    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1977let code_has_label p globals c l =
1978  match p.point_of_label globals c l with
1979  | Types.None -> Bool.False
1980  | Types.Some pt -> code_has_point p globals c pt
1981
1982(** val stmt_explicit_labels :
1983    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1984    List.list **)
1985let stmt_explicit_labels p globals = function
1986| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1987| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
1988| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1989
1990(** val stmt_implicit_label :
1991    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1992    Types.option **)
1993let stmt_implicit_label p globals = function
1994| Sequential (x, s0) -> p.succ_label s0
1995| Final x -> Types.None
1996| FCOND (x0, x1, x2) -> Types.None
1997
1998(** val stmt_labels :
1999    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2000    List.list **)
2001let stmt_labels p g stmt =
2002  List.append
2003    (match stmt_implicit_label p g stmt with
2004     | Types.None -> List.Nil
2005     | Types.Some l -> List.Cons (l, List.Nil))
2006    (stmt_explicit_labels p g stmt)
2007
2008(** val stmt_registers :
2009    stmt_params -> AST.ident List.list -> joint_statement ->
2010    Registers.register List.list **)
2011let stmt_registers p globals = function
2012| Sequential (c, x) ->
2013  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2014| Final c ->
2015  (match c with
2016   | GOTO x -> List.Nil
2017   | RETURN -> List.Nil
2018   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2019| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2020
2021type lin_params =
2022  uns_params
2023  (* singleton inductive, whose constructor was mk_lin_params *)
2024
2025(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2026let rec lin_params_rect_Type4 h_mk_lin_params x_1361 =
2027  let l_u_pars = x_1361 in h_mk_lin_params l_u_pars
2028
2029(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2030let rec lin_params_rect_Type5 h_mk_lin_params x_1363 =
2031  let l_u_pars = x_1363 in h_mk_lin_params l_u_pars
2032
2033(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2034let rec lin_params_rect_Type3 h_mk_lin_params x_1365 =
2035  let l_u_pars = x_1365 in h_mk_lin_params l_u_pars
2036
2037(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2038let rec lin_params_rect_Type2 h_mk_lin_params x_1367 =
2039  let l_u_pars = x_1367 in h_mk_lin_params l_u_pars
2040
2041(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2042let rec lin_params_rect_Type1 h_mk_lin_params x_1369 =
2043  let l_u_pars = x_1369 in h_mk_lin_params l_u_pars
2044
2045(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2046let rec lin_params_rect_Type0 h_mk_lin_params x_1371 =
2047  let l_u_pars = x_1371 in h_mk_lin_params l_u_pars
2048
2049(** val l_u_pars : lin_params -> uns_params **)
2050let rec l_u_pars xxx =
2051  let yyy = xxx in yyy
2052
2053(** val lin_params_inv_rect_Type4 :
2054    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2055let lin_params_inv_rect_Type4 hterm h1 =
2056  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2057
2058(** val lin_params_inv_rect_Type3 :
2059    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2060let lin_params_inv_rect_Type3 hterm h1 =
2061  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2062
2063(** val lin_params_inv_rect_Type2 :
2064    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2065let lin_params_inv_rect_Type2 hterm h1 =
2066  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2067
2068(** val lin_params_inv_rect_Type1 :
2069    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2070let lin_params_inv_rect_Type1 hterm h1 =
2071  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2072
2073(** val lin_params_inv_rect_Type0 :
2074    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2075let lin_params_inv_rect_Type0 hterm h1 =
2076  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2077
2078(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2079let lin_params_jmdiscr x y =
2080  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2081
2082(** val lin_params_to_params : lin_params -> params **)
2083let lin_params_to_params lp =
2084  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2085    Types.None); has_fcond = Bool.True }; stmt_at =
2086    (fun globals code point ->
2087    Obj.magic
2088      (Monad.m_bind0 (Monad.max_def Option.option)
2089        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2090        (fun ls ->
2091        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2092    point_of_label = (fun globals c lbl ->
2093    Util.if_then_else_safe
2094      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2095        (Obj.magic c)) (fun _ ->
2096      Obj.magic
2097        (Monad.m_return0 (Monad.max_def Option.option)
2098          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2099            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2100    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2101
2102(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2103let lp_to_p__o__stmt_pars x0 =
2104  (lin_params_to_params x0).stmt_pars
2105
2106(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2107let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2108  stmt_pars__o__uns_pars (lin_params_to_params x0)
2109
2110(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2111    lin_params -> unserialized_params **)
2112let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2113  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2114
2115type graph_params =
2116  uns_params
2117  (* singleton inductive, whose constructor was mk_graph_params *)
2118
2119(** val graph_params_rect_Type4 :
2120    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2121let rec graph_params_rect_Type4 h_mk_graph_params x_1387 =
2122  let g_u_pars = x_1387 in h_mk_graph_params g_u_pars
2123
2124(** val graph_params_rect_Type5 :
2125    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2126let rec graph_params_rect_Type5 h_mk_graph_params x_1389 =
2127  let g_u_pars = x_1389 in h_mk_graph_params g_u_pars
2128
2129(** val graph_params_rect_Type3 :
2130    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2131let rec graph_params_rect_Type3 h_mk_graph_params x_1391 =
2132  let g_u_pars = x_1391 in h_mk_graph_params g_u_pars
2133
2134(** val graph_params_rect_Type2 :
2135    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2136let rec graph_params_rect_Type2 h_mk_graph_params x_1393 =
2137  let g_u_pars = x_1393 in h_mk_graph_params g_u_pars
2138
2139(** val graph_params_rect_Type1 :
2140    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2141let rec graph_params_rect_Type1 h_mk_graph_params x_1395 =
2142  let g_u_pars = x_1395 in h_mk_graph_params g_u_pars
2143
2144(** val graph_params_rect_Type0 :
2145    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2146let rec graph_params_rect_Type0 h_mk_graph_params x_1397 =
2147  let g_u_pars = x_1397 in h_mk_graph_params g_u_pars
2148
2149(** val g_u_pars : graph_params -> uns_params **)
2150let rec g_u_pars xxx =
2151  let yyy = xxx in yyy
2152
2153(** val graph_params_inv_rect_Type4 :
2154    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2155let graph_params_inv_rect_Type4 hterm h1 =
2156  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2157
2158(** val graph_params_inv_rect_Type3 :
2159    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2160let graph_params_inv_rect_Type3 hterm h1 =
2161  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2162
2163(** val graph_params_inv_rect_Type2 :
2164    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2165let graph_params_inv_rect_Type2 hterm h1 =
2166  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2167
2168(** val graph_params_inv_rect_Type1 :
2169    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2170let graph_params_inv_rect_Type1 hterm h1 =
2171  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2172
2173(** val graph_params_inv_rect_Type0 :
2174    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2175let graph_params_inv_rect_Type0 hterm h1 =
2176  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2177
2178(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2179let graph_params_jmdiscr x y =
2180  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2181
2182(** val graph_params_to_params : graph_params -> params **)
2183let graph_params_to_params gp =
2184  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2185    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2186    (fun globals code ->
2187    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2188    point_of_label = (fun x x0 lbl ->
2189    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2190    point_of_succ = (fun x lbl -> lbl) }
2191
2192(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2193let gp_to_p__o__stmt_pars x0 =
2194  (graph_params_to_params x0).stmt_pars
2195
2196(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2197let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2198  stmt_pars__o__uns_pars (graph_params_to_params x0)
2199
2200(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2201    graph_params -> unserialized_params **)
2202let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2203  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2204
2205type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2206                                 joint_if_runiverse : Identifiers.universe;
2207                                 joint_if_result : __; joint_if_params : 
2208                                 __; joint_if_stacksize : Nat.nat;
2209                                 joint_if_local_stacksize : Nat.nat;
2210                                 joint_if_code : __; joint_if_entry : 
2211                                 __ }
2212
2213(** val joint_internal_function_rect_Type4 :
2214    params -> AST.ident List.list -> (Identifiers.universe ->
2215    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2216    'a1) -> joint_internal_function -> 'a1 **)
2217let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_1413 =
2218  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2219    joint_if_runiverse0; joint_if_result = joint_if_result0;
2220    joint_if_params = joint_if_params0; joint_if_stacksize =
2221    joint_if_stacksize0; joint_if_local_stacksize =
2222    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2223    joint_if_entry = joint_if_entry0 } = x_1413
2224  in
2225  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2226    joint_if_result0 joint_if_params0 joint_if_stacksize0
2227    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2228
2229(** val joint_internal_function_rect_Type5 :
2230    params -> AST.ident List.list -> (Identifiers.universe ->
2231    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2232    'a1) -> joint_internal_function -> 'a1 **)
2233let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_1415 =
2234  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2235    joint_if_runiverse0; joint_if_result = joint_if_result0;
2236    joint_if_params = joint_if_params0; joint_if_stacksize =
2237    joint_if_stacksize0; joint_if_local_stacksize =
2238    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2239    joint_if_entry = joint_if_entry0 } = x_1415
2240  in
2241  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2242    joint_if_result0 joint_if_params0 joint_if_stacksize0
2243    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2244
2245(** val joint_internal_function_rect_Type3 :
2246    params -> AST.ident List.list -> (Identifiers.universe ->
2247    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2248    'a1) -> joint_internal_function -> 'a1 **)
2249let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_1417 =
2250  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2251    joint_if_runiverse0; joint_if_result = joint_if_result0;
2252    joint_if_params = joint_if_params0; joint_if_stacksize =
2253    joint_if_stacksize0; joint_if_local_stacksize =
2254    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2255    joint_if_entry = joint_if_entry0 } = x_1417
2256  in
2257  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2258    joint_if_result0 joint_if_params0 joint_if_stacksize0
2259    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2260
2261(** val joint_internal_function_rect_Type2 :
2262    params -> AST.ident List.list -> (Identifiers.universe ->
2263    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2264    'a1) -> joint_internal_function -> 'a1 **)
2265let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_1419 =
2266  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2267    joint_if_runiverse0; joint_if_result = joint_if_result0;
2268    joint_if_params = joint_if_params0; joint_if_stacksize =
2269    joint_if_stacksize0; joint_if_local_stacksize =
2270    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2271    joint_if_entry = joint_if_entry0 } = x_1419
2272  in
2273  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2274    joint_if_result0 joint_if_params0 joint_if_stacksize0
2275    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2276
2277(** val joint_internal_function_rect_Type1 :
2278    params -> AST.ident List.list -> (Identifiers.universe ->
2279    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2280    'a1) -> joint_internal_function -> 'a1 **)
2281let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_1421 =
2282  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2283    joint_if_runiverse0; joint_if_result = joint_if_result0;
2284    joint_if_params = joint_if_params0; joint_if_stacksize =
2285    joint_if_stacksize0; joint_if_local_stacksize =
2286    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2287    joint_if_entry = joint_if_entry0 } = x_1421
2288  in
2289  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2290    joint_if_result0 joint_if_params0 joint_if_stacksize0
2291    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2292
2293(** val joint_internal_function_rect_Type0 :
2294    params -> AST.ident List.list -> (Identifiers.universe ->
2295    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2296    'a1) -> joint_internal_function -> 'a1 **)
2297let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_1423 =
2298  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2299    joint_if_runiverse0; joint_if_result = joint_if_result0;
2300    joint_if_params = joint_if_params0; joint_if_stacksize =
2301    joint_if_stacksize0; joint_if_local_stacksize =
2302    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2303    joint_if_entry = joint_if_entry0 } = x_1423
2304  in
2305  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2306    joint_if_result0 joint_if_params0 joint_if_stacksize0
2307    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2308
2309(** val joint_if_luniverse :
2310    params -> AST.ident List.list -> joint_internal_function ->
2311    Identifiers.universe **)
2312let rec joint_if_luniverse p globals xxx =
2313  xxx.joint_if_luniverse
2314
2315(** val joint_if_runiverse :
2316    params -> AST.ident List.list -> joint_internal_function ->
2317    Identifiers.universe **)
2318let rec joint_if_runiverse p globals xxx =
2319  xxx.joint_if_runiverse
2320
2321(** val joint_if_result :
2322    params -> AST.ident List.list -> joint_internal_function -> __ **)
2323let rec joint_if_result p globals xxx =
2324  xxx.joint_if_result
2325
2326(** val joint_if_params :
2327    params -> AST.ident List.list -> joint_internal_function -> __ **)
2328let rec joint_if_params p globals xxx =
2329  xxx.joint_if_params
2330
2331(** val joint_if_stacksize :
2332    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2333let rec joint_if_stacksize p globals xxx =
2334  xxx.joint_if_stacksize
2335
2336(** val joint_if_local_stacksize :
2337    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2338let rec joint_if_local_stacksize p globals xxx =
2339  xxx.joint_if_local_stacksize
2340
2341(** val joint_if_code :
2342    params -> AST.ident List.list -> joint_internal_function -> __ **)
2343let rec joint_if_code p globals xxx =
2344  xxx.joint_if_code
2345
2346(** val joint_if_entry :
2347    params -> AST.ident List.list -> joint_internal_function -> __ **)
2348let rec joint_if_entry p globals xxx =
2349  xxx.joint_if_entry
2350
2351(** val joint_internal_function_inv_rect_Type4 :
2352    params -> AST.ident List.list -> joint_internal_function ->
2353    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2354    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2355let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2356  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2357
2358(** val joint_internal_function_inv_rect_Type3 :
2359    params -> AST.ident List.list -> joint_internal_function ->
2360    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2361    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2362let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2363  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2364
2365(** val joint_internal_function_inv_rect_Type2 :
2366    params -> AST.ident List.list -> joint_internal_function ->
2367    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2368    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2369let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2370  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2371
2372(** val joint_internal_function_inv_rect_Type1 :
2373    params -> AST.ident List.list -> joint_internal_function ->
2374    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2375    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2376let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2377  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2378
2379(** val joint_internal_function_inv_rect_Type0 :
2380    params -> AST.ident List.list -> joint_internal_function ->
2381    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2382    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2383let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2384  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2385
2386(** val joint_internal_function_jmdiscr :
2387    params -> AST.ident List.list -> joint_internal_function ->
2388    joint_internal_function -> __ **)
2389let joint_internal_function_jmdiscr a1 a2 x y =
2390  Logic.eq_rect_Type2 x
2391    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2392       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2393       joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2394       a7 } = x
2395     in
2396    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2397
2398(** val good_if_rect_Type4 :
2399    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2400    __ -> __ -> __ -> 'a1) -> 'a1 **)
2401let rec good_if_rect_Type4 p globals def h_mk_good_if =
2402  h_mk_good_if __ __ __ __ __
2403
2404(** val good_if_rect_Type5 :
2405    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2406    __ -> __ -> __ -> 'a1) -> 'a1 **)
2407let rec good_if_rect_Type5 p globals def h_mk_good_if =
2408  h_mk_good_if __ __ __ __ __
2409
2410(** val good_if_rect_Type3 :
2411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412    __ -> __ -> __ -> 'a1) -> 'a1 **)
2413let rec good_if_rect_Type3 p globals def h_mk_good_if =
2414  h_mk_good_if __ __ __ __ __
2415
2416(** val good_if_rect_Type2 :
2417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418    __ -> __ -> __ -> 'a1) -> 'a1 **)
2419let rec good_if_rect_Type2 p globals def h_mk_good_if =
2420  h_mk_good_if __ __ __ __ __
2421
2422(** val good_if_rect_Type1 :
2423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424    __ -> __ -> __ -> 'a1) -> 'a1 **)
2425let rec good_if_rect_Type1 p globals def h_mk_good_if =
2426  h_mk_good_if __ __ __ __ __
2427
2428(** val good_if_rect_Type0 :
2429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430    __ -> __ -> __ -> 'a1) -> 'a1 **)
2431let rec good_if_rect_Type0 p globals def h_mk_good_if =
2432  h_mk_good_if __ __ __ __ __
2433
2434(** val good_if_inv_rect_Type4 :
2435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2437let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2438  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2439
2440(** val good_if_inv_rect_Type3 :
2441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2443let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2444  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2445
2446(** val good_if_inv_rect_Type2 :
2447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2450  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2451
2452(** val good_if_inv_rect_Type1 :
2453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2456  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2457
2458(** val good_if_inv_rect_Type0 :
2459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2462  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2463
2464(** val good_if_discr :
2465    params -> AST.ident List.list -> joint_internal_function -> __ **)
2466let good_if_discr a1 a2 a3 =
2467  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2468
2469(** val good_if_jmdiscr :
2470    params -> AST.ident List.list -> joint_internal_function -> __ **)
2471let good_if_jmdiscr a1 a2 a3 =
2472  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2473
2474type joint_closed_internal_function = joint_internal_function Types.sig0
2475
2476(** val set_joint_code :
2477    AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2478    joint_internal_function **)
2479let set_joint_code globals pars int_fun graph entry =
2480  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2481    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2482    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2483    int_fun.joint_if_stacksize; joint_if_local_stacksize =
2484    int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2485    entry }
2486
2487(** val set_luniverse :
2488    params -> AST.ident List.list -> joint_internal_function ->
2489    Identifiers.universe -> joint_internal_function **)
2490let set_luniverse globals pars p luniverse =
2491  { joint_if_luniverse = luniverse; joint_if_runiverse =
2492    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2493    joint_if_params = p.joint_if_params; joint_if_stacksize =
2494    p.joint_if_stacksize; joint_if_local_stacksize =
2495    p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2496    joint_if_entry = p.joint_if_entry }
2497
2498(** val set_runiverse :
2499    params -> AST.ident List.list -> joint_internal_function ->
2500    Identifiers.universe -> joint_internal_function **)
2501let set_runiverse globals pars p runiverse =
2502  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2503    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2504    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2505    joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2506    p.joint_if_code; joint_if_entry = p.joint_if_entry }
2507
2508(** val add_graph :
2509    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2510    joint_internal_function -> joint_internal_function **)
2511let add_graph g_pars globals l stmt p =
2512  let code =
2513    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2514      stmt
2515  in
2516  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2517  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2518  joint_if_params = p.joint_if_params; joint_if_stacksize =
2519  p.joint_if_stacksize; joint_if_local_stacksize =
2520  p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2521  joint_if_entry = p.joint_if_entry }
2522
2523type joint_function = joint_closed_internal_function AST.fundef
2524
2525type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
2526                                    AST.program;
2527                       init_cost_label : CostLabel.costlabel }
2528
2529(** val joint_program_rect_Type4 :
2530    params -> ((joint_function, AST.init_data List.list) AST.program ->
2531    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2532let rec joint_program_rect_Type4 p h_mk_joint_program x_1465 =
2533  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2534    x_1465
2535  in
2536  h_mk_joint_program joint_prog0 init_cost_label0
2537
2538(** val joint_program_rect_Type5 :
2539    params -> ((joint_function, AST.init_data List.list) AST.program ->
2540    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2541let rec joint_program_rect_Type5 p h_mk_joint_program x_1467 =
2542  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2543    x_1467
2544  in
2545  h_mk_joint_program joint_prog0 init_cost_label0
2546
2547(** val joint_program_rect_Type3 :
2548    params -> ((joint_function, AST.init_data List.list) AST.program ->
2549    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2550let rec joint_program_rect_Type3 p h_mk_joint_program x_1469 =
2551  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2552    x_1469
2553  in
2554  h_mk_joint_program joint_prog0 init_cost_label0
2555
2556(** val joint_program_rect_Type2 :
2557    params -> ((joint_function, AST.init_data List.list) AST.program ->
2558    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2559let rec joint_program_rect_Type2 p h_mk_joint_program x_1471 =
2560  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2561    x_1471
2562  in
2563  h_mk_joint_program joint_prog0 init_cost_label0
2564
2565(** val joint_program_rect_Type1 :
2566    params -> ((joint_function, AST.init_data List.list) AST.program ->
2567    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2568let rec joint_program_rect_Type1 p h_mk_joint_program x_1473 =
2569  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2570    x_1473
2571  in
2572  h_mk_joint_program joint_prog0 init_cost_label0
2573
2574(** val joint_program_rect_Type0 :
2575    params -> ((joint_function, AST.init_data List.list) AST.program ->
2576    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2577let rec joint_program_rect_Type0 p h_mk_joint_program x_1475 =
2578  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2579    x_1475
2580  in
2581  h_mk_joint_program joint_prog0 init_cost_label0
2582
2583(** val joint_prog :
2584    params -> joint_program -> (joint_function, AST.init_data List.list)
2585    AST.program **)
2586let rec joint_prog p xxx =
2587  xxx.joint_prog
2588
2589(** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2590let rec init_cost_label p xxx =
2591  xxx.init_cost_label
2592
2593(** val joint_program_inv_rect_Type4 :
2594    params -> joint_program -> ((joint_function, AST.init_data List.list)
2595    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2596let joint_program_inv_rect_Type4 x1 hterm h1 =
2597  let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2598
2599(** val joint_program_inv_rect_Type3 :
2600    params -> joint_program -> ((joint_function, AST.init_data List.list)
2601    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2602let joint_program_inv_rect_Type3 x1 hterm h1 =
2603  let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2604
2605(** val joint_program_inv_rect_Type2 :
2606    params -> joint_program -> ((joint_function, AST.init_data List.list)
2607    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2608let joint_program_inv_rect_Type2 x1 hterm h1 =
2609  let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2610
2611(** val joint_program_inv_rect_Type1 :
2612    params -> joint_program -> ((joint_function, AST.init_data List.list)
2613    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2614let joint_program_inv_rect_Type1 x1 hterm h1 =
2615  let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2616
2617(** val joint_program_inv_rect_Type0 :
2618    params -> joint_program -> ((joint_function, AST.init_data List.list)
2619    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2620let joint_program_inv_rect_Type0 x1 hterm h1 =
2621  let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2622
2623(** val joint_program_discr :
2624    params -> joint_program -> joint_program -> __ **)
2625let joint_program_discr a1 x y =
2626  Logic.eq_rect_Type2 x
2627    (let { joint_prog = a0; init_cost_label = a10 } = x in
2628    Obj.magic (fun _ dH -> dH __ __)) y
2629
2630(** val joint_program_jmdiscr :
2631    params -> joint_program -> joint_program -> __ **)
2632let joint_program_jmdiscr a1 x y =
2633  Logic.eq_rect_Type2 x
2634    (let { joint_prog = a0; init_cost_label = a10 } = x in
2635    Obj.magic (fun _ dH -> dH __ __)) y
2636
2637(** val dpi1__o__joint_prog__o__inject :
2638    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2639    AST.init_data List.list) AST.program Types.sig0 **)
2640let dpi1__o__joint_prog__o__inject x0 x3 =
2641  x3.Types.dpi1.joint_prog
2642
2643(** val eject__o__joint_prog__o__inject :
2644    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2645    List.list) AST.program Types.sig0 **)
2646let eject__o__joint_prog__o__inject x0 x3 =
2647  (Types.pi1 x3).joint_prog
2648
2649(** val joint_prog__o__inject :
2650    params -> joint_program -> (joint_function, AST.init_data List.list)
2651    AST.program Types.sig0 **)
2652let joint_prog__o__inject x0 x2 =
2653  x2.joint_prog
2654
2655(** val dpi1__o__joint_prog :
2656    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2657    AST.init_data List.list) AST.program **)
2658let dpi1__o__joint_prog x0 x2 =
2659  x2.Types.dpi1.joint_prog
2660
2661(** val eject__o__joint_prog :
2662    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2663    List.list) AST.program **)
2664let eject__o__joint_prog x0 x2 =
2665  (Types.pi1 x2).joint_prog
2666
2667type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2668
2669(** val stack_cost : params -> joint_program -> stack_cost_model **)
2670let stack_cost p pr =
2671  List.foldr (fun id_fun acc ->
2672    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2673    (match fun0 with
2674     | AST.Internal jif ->
2675       List.Cons ({ Types.fst = id; Types.snd =
2676         (Types.pi1 jif).joint_if_stacksize }, acc)
2677     | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
2678
2679open Extra_bool
2680
2681open Coqlib
2682
2683open Values
2684
2685open FrontEndVal
2686
2687open GenMem
2688
2689open FrontEndMem
2690
2691open Globalenvs
2692
2693(** val globals_stacksize : params -> joint_program -> Nat.nat **)
2694let globals_stacksize pars p =
2695  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2696    Globalenvs.size_init_data_list entry.Types.snd)
2697    p.joint_prog.AST.prog_vars
2698
Note: See TracBrowser for help on using the repository browser.