source: extracted/joint.ml @ 2827

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

Everything extracted again.

File size: 105.5 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_19661 -> h_Reg x_19661
113| Imm x_19662 -> h_Imm x_19662
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_19666 -> h_Reg x_19666
119| Imm x_19667 -> h_Imm x_19667
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_19671 -> h_Reg x_19671
125| Imm x_19672 -> h_Imm x_19672
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_19676 -> h_Reg x_19676
131| Imm x_19677 -> h_Imm x_19677
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_19681 -> h_Reg x_19681
137| Imm x_19682 -> h_Imm x_19682
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_19686 -> h_Reg x_19686
143| Imm x_19687 -> h_Imm x_19687
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_19722 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_19722
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_19724 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_19724
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_19726 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_19726
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_19728 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_19728
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_19730 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_19730
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_19732 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_19732
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_19749 =
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_19749
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_19751 =
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_19751
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_19753 =
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_19753
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_19755 =
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_19755
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_19757 =
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_19757
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_19759 =
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_19759
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_19789 =
808  let { u_pars = u_pars0; functs = functs0 } = x_19789 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_19791 =
815  let { u_pars = u_pars0; functs = functs0 } = x_19791 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_19793 =
822  let { u_pars = u_pars0; functs = functs0 } = x_19793 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_19795 =
829  let { u_pars = u_pars0; functs = functs0 } = x_19795 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_19797 =
836  let { u_pars = u_pars0; functs = functs0 } = x_19797 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_19799 =
843  let { u_pars = u_pars0; functs = functs0 } = x_19799 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_19854 -> h_COMMENT x_19854
914| MOVE x_19855 -> h_MOVE x_19855
915| POP x_19856 -> h_POP x_19856
916| PUSH x_19857 -> h_PUSH x_19857
917| ADDRESS (i, x_19859, x_19858) -> h_ADDRESS i __ x_19859 x_19858
918| OPACCS (x_19865, x_19864, x_19863, x_19862, x_19861) ->
919  h_OPACCS x_19865 x_19864 x_19863 x_19862 x_19861
920| OP1 (x_19868, x_19867, x_19866) -> h_OP1 x_19868 x_19867 x_19866
921| OP2 (x_19872, x_19871, x_19870, x_19869) ->
922  h_OP2 x_19872 x_19871 x_19870 x_19869
923| CLEAR_CARRY -> h_CLEAR_CARRY
924| SET_CARRY -> h_SET_CARRY
925| LOAD (x_19875, x_19874, x_19873) -> h_LOAD x_19875 x_19874 x_19873
926| STORE (x_19878, x_19877, x_19876) -> h_STORE x_19878 x_19877 x_19876
927| Extension_seq x_19879 -> h_extension_seq x_19879
928
929(** val joint_seq_rect_Type5 :
930    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
931    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
932    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
933    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
934    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
935    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
936let 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
937| COMMENT x_19894 -> h_COMMENT x_19894
938| MOVE x_19895 -> h_MOVE x_19895
939| POP x_19896 -> h_POP x_19896
940| PUSH x_19897 -> h_PUSH x_19897
941| ADDRESS (i, x_19899, x_19898) -> h_ADDRESS i __ x_19899 x_19898
942| OPACCS (x_19905, x_19904, x_19903, x_19902, x_19901) ->
943  h_OPACCS x_19905 x_19904 x_19903 x_19902 x_19901
944| OP1 (x_19908, x_19907, x_19906) -> h_OP1 x_19908 x_19907 x_19906
945| OP2 (x_19912, x_19911, x_19910, x_19909) ->
946  h_OP2 x_19912 x_19911 x_19910 x_19909
947| CLEAR_CARRY -> h_CLEAR_CARRY
948| SET_CARRY -> h_SET_CARRY
949| LOAD (x_19915, x_19914, x_19913) -> h_LOAD x_19915 x_19914 x_19913
950| STORE (x_19918, x_19917, x_19916) -> h_STORE x_19918 x_19917 x_19916
951| Extension_seq x_19919 -> h_extension_seq x_19919
952
953(** val joint_seq_rect_Type3 :
954    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
955    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
956    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
957    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
958    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
959    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
960let 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
961| COMMENT x_19934 -> h_COMMENT x_19934
962| MOVE x_19935 -> h_MOVE x_19935
963| POP x_19936 -> h_POP x_19936
964| PUSH x_19937 -> h_PUSH x_19937
965| ADDRESS (i, x_19939, x_19938) -> h_ADDRESS i __ x_19939 x_19938
966| OPACCS (x_19945, x_19944, x_19943, x_19942, x_19941) ->
967  h_OPACCS x_19945 x_19944 x_19943 x_19942 x_19941
968| OP1 (x_19948, x_19947, x_19946) -> h_OP1 x_19948 x_19947 x_19946
969| OP2 (x_19952, x_19951, x_19950, x_19949) ->
970  h_OP2 x_19952 x_19951 x_19950 x_19949
971| CLEAR_CARRY -> h_CLEAR_CARRY
972| SET_CARRY -> h_SET_CARRY
973| LOAD (x_19955, x_19954, x_19953) -> h_LOAD x_19955 x_19954 x_19953
974| STORE (x_19958, x_19957, x_19956) -> h_STORE x_19958 x_19957 x_19956
975| Extension_seq x_19959 -> h_extension_seq x_19959
976
977(** val joint_seq_rect_Type2 :
978    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
979    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
980    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
981    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
982    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
983    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
984let 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
985| COMMENT x_19974 -> h_COMMENT x_19974
986| MOVE x_19975 -> h_MOVE x_19975
987| POP x_19976 -> h_POP x_19976
988| PUSH x_19977 -> h_PUSH x_19977
989| ADDRESS (i, x_19979, x_19978) -> h_ADDRESS i __ x_19979 x_19978
990| OPACCS (x_19985, x_19984, x_19983, x_19982, x_19981) ->
991  h_OPACCS x_19985 x_19984 x_19983 x_19982 x_19981
992| OP1 (x_19988, x_19987, x_19986) -> h_OP1 x_19988 x_19987 x_19986
993| OP2 (x_19992, x_19991, x_19990, x_19989) ->
994  h_OP2 x_19992 x_19991 x_19990 x_19989
995| CLEAR_CARRY -> h_CLEAR_CARRY
996| SET_CARRY -> h_SET_CARRY
997| LOAD (x_19995, x_19994, x_19993) -> h_LOAD x_19995 x_19994 x_19993
998| STORE (x_19998, x_19997, x_19996) -> h_STORE x_19998 x_19997 x_19996
999| Extension_seq x_19999 -> h_extension_seq x_19999
1000
1001(** val joint_seq_rect_Type1 :
1002    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1003    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1004    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1005    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1006    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1007    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1008let 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
1009| COMMENT x_20014 -> h_COMMENT x_20014
1010| MOVE x_20015 -> h_MOVE x_20015
1011| POP x_20016 -> h_POP x_20016
1012| PUSH x_20017 -> h_PUSH x_20017
1013| ADDRESS (i, x_20019, x_20018) -> h_ADDRESS i __ x_20019 x_20018
1014| OPACCS (x_20025, x_20024, x_20023, x_20022, x_20021) ->
1015  h_OPACCS x_20025 x_20024 x_20023 x_20022 x_20021
1016| OP1 (x_20028, x_20027, x_20026) -> h_OP1 x_20028 x_20027 x_20026
1017| OP2 (x_20032, x_20031, x_20030, x_20029) ->
1018  h_OP2 x_20032 x_20031 x_20030 x_20029
1019| CLEAR_CARRY -> h_CLEAR_CARRY
1020| SET_CARRY -> h_SET_CARRY
1021| LOAD (x_20035, x_20034, x_20033) -> h_LOAD x_20035 x_20034 x_20033
1022| STORE (x_20038, x_20037, x_20036) -> h_STORE x_20038 x_20037 x_20036
1023| Extension_seq x_20039 -> h_extension_seq x_20039
1024
1025(** val joint_seq_rect_Type0 :
1026    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1027    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
1028    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
1029    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
1030    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1031    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1032let 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
1033| COMMENT x_20054 -> h_COMMENT x_20054
1034| MOVE x_20055 -> h_MOVE x_20055
1035| POP x_20056 -> h_POP x_20056
1036| PUSH x_20057 -> h_PUSH x_20057
1037| ADDRESS (i, x_20059, x_20058) -> h_ADDRESS i __ x_20059 x_20058
1038| OPACCS (x_20065, x_20064, x_20063, x_20062, x_20061) ->
1039  h_OPACCS x_20065 x_20064 x_20063 x_20062 x_20061
1040| OP1 (x_20068, x_20067, x_20066) -> h_OP1 x_20068 x_20067 x_20066
1041| OP2 (x_20072, x_20071, x_20070, x_20069) ->
1042  h_OP2 x_20072 x_20071 x_20070 x_20069
1043| CLEAR_CARRY -> h_CLEAR_CARRY
1044| SET_CARRY -> h_SET_CARRY
1045| LOAD (x_20075, x_20074, x_20073) -> h_LOAD x_20075 x_20074 x_20073
1046| STORE (x_20078, x_20077, x_20076) -> h_STORE x_20078 x_20077 x_20076
1047| Extension_seq x_20079 -> h_extension_seq x_20079
1048
1049(** val joint_seq_inv_rect_Type4 :
1050    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1051    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1052    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1053    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1054    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1055    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1056    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1057let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1058  let hcut =
1059    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1060      hterm
1061  in
1062  hcut __
1063
1064(** val joint_seq_inv_rect_Type3 :
1065    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1066    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1067    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1068    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1069    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1070    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1071    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1072let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1073  let hcut =
1074    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1075      hterm
1076  in
1077  hcut __
1078
1079(** val joint_seq_inv_rect_Type2 :
1080    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1081    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1082    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1083    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1084    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1085    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1086    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1087let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1088  let hcut =
1089    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1090      hterm
1091  in
1092  hcut __
1093
1094(** val joint_seq_inv_rect_Type1 :
1095    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1096    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1097    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1098    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1099    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1100    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1101    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1102let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1103  let hcut =
1104    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1105      hterm
1106  in
1107  hcut __
1108
1109(** val joint_seq_inv_rect_Type0 :
1110    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1111    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1112    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
1113    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
1114    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
1115    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
1116    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1117let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1118  let hcut =
1119    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1120      hterm
1121  in
1122  hcut __
1123
1124(** val joint_seq_discr :
1125    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1126    __ **)
1127let joint_seq_discr a1 a2 x y =
1128  Logic.eq_rect_Type2 x
1129    (match x with
1130     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1131     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1132     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1133     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1134     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1135     | OPACCS (a0, a10, a20, a3, a4) ->
1136       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1137     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1138     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1139     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1140     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1141     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1142     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1143     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1144
1145(** val joint_seq_jmdiscr :
1146    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1147    __ **)
1148let joint_seq_jmdiscr a1 a2 x y =
1149  Logic.eq_rect_Type2 x
1150    (match x with
1151     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1152     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1153     | POP a0 -> Obj.magic (fun _ dH -> dH __)
1154     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1155     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1156     | OPACCS (a0, a10, a20, a3, a4) ->
1157       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1158     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1159     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1160     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1161     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1162     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1163     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1164     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1165
1166(** val get_used_registers_from_seq :
1167    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1168    joint_seq -> Registers.register List.list **)
1169let get_used_registers_from_seq p globals functs0 = function
1170| COMMENT x -> List.Nil
1171| MOVE pm -> functs0.pair_move_regs pm
1172| POP r -> functs0.acc_a_regs r
1173| PUSH r -> functs0.acc_a_args r
1174| ADDRESS (i, r1, r2) ->
1175  List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1176| OPACCS (o, r1, r2, r3, r4) ->
1177  List.append (functs0.acc_a_regs r1)
1178    (List.append (functs0.acc_b_regs r2)
1179      (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1180| OP1 (o, r1, r2) ->
1181  List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1182| OP2 (o, r1, r2, r3) ->
1183  List.append (functs0.acc_a_regs r1)
1184    (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1185| CLEAR_CARRY -> List.Nil
1186| SET_CARRY -> List.Nil
1187| LOAD (r1, r2, r3) ->
1188  List.append (functs0.acc_a_regs r1)
1189    (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1190| STORE (r1, r2, r3) ->
1191  List.append (functs0.dpl_args r1)
1192    (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1193| Extension_seq ext -> functs0.ext_seq_regs ext
1194
1195(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1196let nOOP p globals =
1197  COMMENT String.EmptyString
1198
1199(** val dpi1__o__extension_seq_to_seq__o__inject :
1200    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1201    joint_seq Types.sig0 **)
1202let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1203  Extension_seq x4.Types.dpi1
1204
1205(** val eject__o__extension_seq_to_seq__o__inject :
1206    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1207    Types.sig0 **)
1208let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1209  Extension_seq (Types.pi1 x4)
1210
1211(** val extension_seq_to_seq__o__inject :
1212    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1213let extension_seq_to_seq__o__inject x0 x1 x3 =
1214  Extension_seq x3
1215
1216(** val dpi1__o__extension_seq_to_seq :
1217    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1218    joint_seq **)
1219let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1220  Extension_seq x3.Types.dpi1
1221
1222(** val eject__o__extension_seq_to_seq :
1223    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1224let eject__o__extension_seq_to_seq x0 x1 x3 =
1225  Extension_seq (Types.pi1 x3)
1226
1227type joint_step =
1228| COST_LABEL of CostLabel.costlabel
1229| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1230| COND of __ * Graphs.label
1231| Step_seq of joint_seq
1232
1233(** val joint_step_rect_Type4 :
1234    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1235    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1236    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1237let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1238| COST_LABEL x_20346 -> h_COST_LABEL x_20346
1239| CALL (x_20349, x_20348, x_20347) -> h_CALL x_20349 x_20348 x_20347
1240| COND (x_20351, x_20350) -> h_COND x_20351 x_20350
1241| Step_seq x_20352 -> h_step_seq x_20352
1242
1243(** val joint_step_rect_Type5 :
1244    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1245    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1246    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1247let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1248| COST_LABEL x_20358 -> h_COST_LABEL x_20358
1249| CALL (x_20361, x_20360, x_20359) -> h_CALL x_20361 x_20360 x_20359
1250| COND (x_20363, x_20362) -> h_COND x_20363 x_20362
1251| Step_seq x_20364 -> h_step_seq x_20364
1252
1253(** val joint_step_rect_Type3 :
1254    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1255    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1256    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1257let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1258| COST_LABEL x_20370 -> h_COST_LABEL x_20370
1259| CALL (x_20373, x_20372, x_20371) -> h_CALL x_20373 x_20372 x_20371
1260| COND (x_20375, x_20374) -> h_COND x_20375 x_20374
1261| Step_seq x_20376 -> h_step_seq x_20376
1262
1263(** val joint_step_rect_Type2 :
1264    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1265    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1266    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1267let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1268| COST_LABEL x_20382 -> h_COST_LABEL x_20382
1269| CALL (x_20385, x_20384, x_20383) -> h_CALL x_20385 x_20384 x_20383
1270| COND (x_20387, x_20386) -> h_COND x_20387 x_20386
1271| Step_seq x_20388 -> h_step_seq x_20388
1272
1273(** val joint_step_rect_Type1 :
1274    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1275    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1276    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1277let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1278| COST_LABEL x_20394 -> h_COST_LABEL x_20394
1279| CALL (x_20397, x_20396, x_20395) -> h_CALL x_20397 x_20396 x_20395
1280| COND (x_20399, x_20398) -> h_COND x_20399 x_20398
1281| Step_seq x_20400 -> h_step_seq x_20400
1282
1283(** val joint_step_rect_Type0 :
1284    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1285    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1286    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1287let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1288| COST_LABEL x_20406 -> h_COST_LABEL x_20406
1289| CALL (x_20409, x_20408, x_20407) -> h_CALL x_20409 x_20408 x_20407
1290| COND (x_20411, x_20410) -> h_COND x_20411 x_20410
1291| Step_seq x_20412 -> h_step_seq x_20412
1292
1293(** val joint_step_inv_rect_Type4 :
1294    unserialized_params -> AST.ident List.list -> joint_step ->
1295    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1296    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1297    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1298let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1299  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1300
1301(** val joint_step_inv_rect_Type3 :
1302    unserialized_params -> AST.ident List.list -> joint_step ->
1303    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1304    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1305    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1306let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1307  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1308
1309(** val joint_step_inv_rect_Type2 :
1310    unserialized_params -> AST.ident List.list -> joint_step ->
1311    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1312    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1313    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1314let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1315  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1316
1317(** val joint_step_inv_rect_Type1 :
1318    unserialized_params -> AST.ident List.list -> joint_step ->
1319    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1320    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1321    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1322let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1323  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1324
1325(** val joint_step_inv_rect_Type0 :
1326    unserialized_params -> AST.ident List.list -> joint_step ->
1327    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1328    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1329    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1330let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1331  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1332
1333(** val joint_step_discr :
1334    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1335    __ **)
1336let joint_step_discr a1 a2 x y =
1337  Logic.eq_rect_Type2 x
1338    (match x with
1339     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1340     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1341     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1342     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1343
1344(** val joint_step_jmdiscr :
1345    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1346    __ **)
1347let joint_step_jmdiscr a1 a2 x y =
1348  Logic.eq_rect_Type2 x
1349    (match x with
1350     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1351     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1352     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1353     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1354
1355(** val get_used_registers_from_step :
1356    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1357    joint_step -> Registers.register List.list **)
1358let get_used_registers_from_step p globals functs0 = function
1359| COST_LABEL c -> List.Nil
1360| CALL (id, args, dest) ->
1361  List.append (functs0.f_call_args args) (functs0.f_call_dest dest)
1362| COND (r, lbl) -> functs0.acc_a_regs r
1363| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1364
1365(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1366    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1367    joint_step Types.sig0 **)
1368let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1369  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1370
1371(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1372    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1373    Types.sig0 **)
1374let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1375  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1376
1377(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1378    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1379let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1380  Step_seq (Extension_seq x2)
1381
1382(** val dpi1__o__seq_to_step__o__inject :
1383    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1384    Types.dPair -> joint_step Types.sig0 **)
1385let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1386  Step_seq x4.Types.dpi1
1387
1388(** val eject__o__seq_to_step__o__inject :
1389    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1390    joint_step Types.sig0 **)
1391let eject__o__seq_to_step__o__inject x0 x1 x4 =
1392  Step_seq (Types.pi1 x4)
1393
1394(** val seq_to_step__o__inject :
1395    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1396    Types.sig0 **)
1397let seq_to_step__o__inject x0 x1 x3 =
1398  Step_seq x3
1399
1400(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1401    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1402    joint_step **)
1403let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1404  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1405
1406(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1407    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1408let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1409  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1410
1411(** val extension_seq_to_seq__o__seq_to_step :
1412    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1413let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1414  Step_seq (Extension_seq x2)
1415
1416(** val dpi1__o__seq_to_step :
1417    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1418    Types.dPair -> joint_step **)
1419let dpi1__o__seq_to_step x0 x1 x3 =
1420  Step_seq x3.Types.dpi1
1421
1422(** val eject__o__seq_to_step :
1423    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1424    joint_step **)
1425let eject__o__seq_to_step x0 x1 x3 =
1426  Step_seq (Types.pi1 x3)
1427
1428(** val step_labels :
1429    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1430    List.list **)
1431let step_labels p globals = function
1432| COST_LABEL x -> List.Nil
1433| CALL (x, x0, x1) -> List.Nil
1434| COND (x, l) -> List.Cons (l, List.Nil)
1435| Step_seq s0 ->
1436  (match s0 with
1437   | COMMENT x -> List.Nil
1438   | MOVE x -> List.Nil
1439   | POP x -> List.Nil
1440   | PUSH x -> List.Nil
1441   | ADDRESS (x, x1, x2) -> List.Nil
1442   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1443   | OP1 (x, x0, x1) -> List.Nil
1444   | OP2 (x, x0, x1, x2) -> List.Nil
1445   | CLEAR_CARRY -> List.Nil
1446   | SET_CARRY -> List.Nil
1447   | LOAD (x, x0, x1) -> List.Nil
1448   | STORE (x, x0, x1) -> List.Nil
1449   | Extension_seq ext -> p.ext_seq_labels ext)
1450
1451type stmt_params = { uns_pars : uns_params;
1452                     succ_label : (__ -> Graphs.label Types.option);
1453                     has_fcond : Bool.bool }
1454
1455(** val stmt_params_rect_Type4 :
1456    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1457    'a1) -> stmt_params -> 'a1 **)
1458let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 =
1459  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1460    has_fcond0 } = x_20491
1461  in
1462  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1463
1464(** val stmt_params_rect_Type5 :
1465    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1466    'a1) -> stmt_params -> 'a1 **)
1467let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 =
1468  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1469    has_fcond0 } = x_20493
1470  in
1471  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1472
1473(** val stmt_params_rect_Type3 :
1474    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1475    'a1) -> stmt_params -> 'a1 **)
1476let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 =
1477  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1478    has_fcond0 } = x_20495
1479  in
1480  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1481
1482(** val stmt_params_rect_Type2 :
1483    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1484    'a1) -> stmt_params -> 'a1 **)
1485let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 =
1486  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1487    has_fcond0 } = x_20497
1488  in
1489  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1490
1491(** val stmt_params_rect_Type1 :
1492    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1493    'a1) -> stmt_params -> 'a1 **)
1494let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 =
1495  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1496    has_fcond0 } = x_20499
1497  in
1498  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1499
1500(** val stmt_params_rect_Type0 :
1501    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1502    'a1) -> stmt_params -> 'a1 **)
1503let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 =
1504  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1505    has_fcond0 } = x_20501
1506  in
1507  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1508
1509(** val uns_pars : stmt_params -> uns_params **)
1510let rec uns_pars xxx =
1511  xxx.uns_pars
1512
1513type succ = __
1514
1515(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1516let rec succ_label xxx =
1517  xxx.succ_label
1518
1519(** val has_fcond : stmt_params -> Bool.bool **)
1520let rec has_fcond xxx =
1521  xxx.has_fcond
1522
1523(** val stmt_params_inv_rect_Type4 :
1524    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1525    Bool.bool -> __ -> 'a1) -> 'a1 **)
1526let stmt_params_inv_rect_Type4 hterm h1 =
1527  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1528
1529(** val stmt_params_inv_rect_Type3 :
1530    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1531    Bool.bool -> __ -> 'a1) -> 'a1 **)
1532let stmt_params_inv_rect_Type3 hterm h1 =
1533  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1534
1535(** val stmt_params_inv_rect_Type2 :
1536    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1537    Bool.bool -> __ -> 'a1) -> 'a1 **)
1538let stmt_params_inv_rect_Type2 hterm h1 =
1539  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1540
1541(** val stmt_params_inv_rect_Type1 :
1542    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1543    Bool.bool -> __ -> 'a1) -> 'a1 **)
1544let stmt_params_inv_rect_Type1 hterm h1 =
1545  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1546
1547(** val stmt_params_inv_rect_Type0 :
1548    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1549    Bool.bool -> __ -> 'a1) -> 'a1 **)
1550let stmt_params_inv_rect_Type0 hterm h1 =
1551  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1552
1553(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1554let stmt_params_jmdiscr x y =
1555  Logic.eq_rect_Type2 x
1556    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1557    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1558
1559(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1560let uns_pars__o__u_pars x0 =
1561  x0.uns_pars.u_pars
1562
1563type joint_fin_step =
1564| GOTO of Graphs.label
1565| RETURN
1566| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1567
1568(** val joint_fin_step_rect_Type4 :
1569    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1570    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1571let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1572| GOTO x_20525 -> h_GOTO x_20525
1573| RETURN -> h_RETURN
1574| TAILCALL (x_20527, x_20526) -> h_TAILCALL __ x_20527 x_20526
1575
1576(** val joint_fin_step_rect_Type5 :
1577    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1579let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1580| GOTO x_20533 -> h_GOTO x_20533
1581| RETURN -> h_RETURN
1582| TAILCALL (x_20535, x_20534) -> h_TAILCALL __ x_20535 x_20534
1583
1584(** val joint_fin_step_rect_Type3 :
1585    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1587let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1588| GOTO x_20541 -> h_GOTO x_20541
1589| RETURN -> h_RETURN
1590| TAILCALL (x_20543, x_20542) -> h_TAILCALL __ x_20543 x_20542
1591
1592(** val joint_fin_step_rect_Type2 :
1593    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1595let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1596| GOTO x_20549 -> h_GOTO x_20549
1597| RETURN -> h_RETURN
1598| TAILCALL (x_20551, x_20550) -> h_TAILCALL __ x_20551 x_20550
1599
1600(** val joint_fin_step_rect_Type1 :
1601    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1603let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1604| GOTO x_20557 -> h_GOTO x_20557
1605| RETURN -> h_RETURN
1606| TAILCALL (x_20559, x_20558) -> h_TAILCALL __ x_20559 x_20558
1607
1608(** val joint_fin_step_rect_Type0 :
1609    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1611let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1612| GOTO x_20565 -> h_GOTO x_20565
1613| RETURN -> h_RETURN
1614| TAILCALL (x_20567, x_20566) -> h_TAILCALL __ x_20567 x_20566
1615
1616(** val joint_fin_step_inv_rect_Type4 :
1617    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1618    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1619    __ -> 'a1) -> 'a1 **)
1620let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1621  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1622
1623(** val joint_fin_step_inv_rect_Type3 :
1624    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1625    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1626    __ -> 'a1) -> 'a1 **)
1627let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1628  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1629
1630(** val joint_fin_step_inv_rect_Type2 :
1631    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1632    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1633    __ -> 'a1) -> 'a1 **)
1634let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1635  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1636
1637(** val joint_fin_step_inv_rect_Type1 :
1638    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1639    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1640    __ -> 'a1) -> 'a1 **)
1641let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1642  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1643
1644(** val joint_fin_step_inv_rect_Type0 :
1645    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1646    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1647    __ -> 'a1) -> 'a1 **)
1648let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1649  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1650
1651(** val joint_fin_step_discr :
1652    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1653let joint_fin_step_discr a1 x y =
1654  Logic.eq_rect_Type2 x
1655    (match x with
1656     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1657     | RETURN -> Obj.magic (fun _ dH -> dH)
1658     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1659
1660(** val joint_fin_step_jmdiscr :
1661    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1662let joint_fin_step_jmdiscr a1 x y =
1663  Logic.eq_rect_Type2 x
1664    (match x with
1665     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1666     | RETURN -> Obj.magic (fun _ dH -> dH)
1667     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1668
1669(** val fin_step_labels :
1670    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1671let fin_step_labels p = function
1672| GOTO l -> List.Cons (l, List.Nil)
1673| RETURN -> List.Nil
1674| TAILCALL (x0, x1) -> List.Nil
1675
1676type joint_statement =
1677| Sequential of joint_step * __
1678| Final of joint_fin_step
1679| FCOND of __ * Graphs.label * Graphs.label
1680
1681(** val joint_statement_rect_Type4 :
1682    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1683    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1684    'a1) -> joint_statement -> 'a1 **)
1685let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1686| Sequential (x_20633, x_20632) -> h_sequential x_20633 x_20632
1687| Final x_20634 -> h_final x_20634
1688| FCOND (x_20637, x_20636, x_20635) -> h_FCOND __ x_20637 x_20636 x_20635
1689
1690(** val joint_statement_rect_Type5 :
1691    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1692    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1693    'a1) -> joint_statement -> 'a1 **)
1694let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1695| Sequential (x_20644, x_20643) -> h_sequential x_20644 x_20643
1696| Final x_20645 -> h_final x_20645
1697| FCOND (x_20648, x_20647, x_20646) -> h_FCOND __ x_20648 x_20647 x_20646
1698
1699(** val joint_statement_rect_Type3 :
1700    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1701    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1702    'a1) -> joint_statement -> 'a1 **)
1703let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1704| Sequential (x_20655, x_20654) -> h_sequential x_20655 x_20654
1705| Final x_20656 -> h_final x_20656
1706| FCOND (x_20659, x_20658, x_20657) -> h_FCOND __ x_20659 x_20658 x_20657
1707
1708(** val joint_statement_rect_Type2 :
1709    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1710    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1711    'a1) -> joint_statement -> 'a1 **)
1712let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1713| Sequential (x_20666, x_20665) -> h_sequential x_20666 x_20665
1714| Final x_20667 -> h_final x_20667
1715| FCOND (x_20670, x_20669, x_20668) -> h_FCOND __ x_20670 x_20669 x_20668
1716
1717(** val joint_statement_rect_Type1 :
1718    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1719    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1720    'a1) -> joint_statement -> 'a1 **)
1721let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1722| Sequential (x_20677, x_20676) -> h_sequential x_20677 x_20676
1723| Final x_20678 -> h_final x_20678
1724| FCOND (x_20681, x_20680, x_20679) -> h_FCOND __ x_20681 x_20680 x_20679
1725
1726(** val joint_statement_rect_Type0 :
1727    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1728    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1729    'a1) -> joint_statement -> 'a1 **)
1730let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1731| Sequential (x_20688, x_20687) -> h_sequential x_20688 x_20687
1732| Final x_20689 -> h_final x_20689
1733| FCOND (x_20692, x_20691, x_20690) -> h_FCOND __ x_20692 x_20691 x_20690
1734
1735(** val joint_statement_inv_rect_Type4 :
1736    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1737    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1738    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1739let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1740  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1741
1742(** val joint_statement_inv_rect_Type3 :
1743    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1744    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1745    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1746let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1747  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1748
1749(** val joint_statement_inv_rect_Type2 :
1750    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1751    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1752    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1753let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1754  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1755
1756(** val joint_statement_inv_rect_Type1 :
1757    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1758    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1759    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1760let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1761  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1762
1763(** val joint_statement_inv_rect_Type0 :
1764    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1765    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1766    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1767let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1768  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1769
1770(** val joint_statement_discr :
1771    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1772    -> __ **)
1773let joint_statement_discr a1 a2 x y =
1774  Logic.eq_rect_Type2 x
1775    (match x with
1776     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1777     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1778     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1779
1780(** val joint_statement_jmdiscr :
1781    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1782    -> __ **)
1783let joint_statement_jmdiscr a1 a2 x y =
1784  Logic.eq_rect_Type2 x
1785    (match x with
1786     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1787     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1788     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1789
1790(** val dpi1__o__fin_step_to_stmt__o__inject :
1791    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1792    -> joint_statement Types.sig0 **)
1793let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1794  Final x4.Types.dpi1
1795
1796(** val eject__o__fin_step_to_stmt__o__inject :
1797    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1798    joint_statement Types.sig0 **)
1799let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1800  Final (Types.pi1 x4)
1801
1802(** val fin_step_to_stmt__o__inject :
1803    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1804    Types.sig0 **)
1805let fin_step_to_stmt__o__inject x0 x1 x3 =
1806  Final x3
1807
1808(** val dpi1__o__fin_step_to_stmt :
1809    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1810    -> joint_statement **)
1811let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1812  Final x3.Types.dpi1
1813
1814(** val eject__o__fin_step_to_stmt :
1815    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1816    joint_statement **)
1817let eject__o__fin_step_to_stmt x0 x1 x3 =
1818  Final (Types.pi1 x3)
1819
1820type params = { stmt_pars : stmt_params;
1821                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1822                          Types.option);
1823                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1824                                 -> __ Types.option);
1825                point_of_succ : (__ -> __ -> __) }
1826
1827(** val params_rect_Type4 :
1828    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1829    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1830    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1831    'a1 **)
1832let rec params_rect_Type4 h_mk_params x_20765 =
1833  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1834    point_of_label0; point_of_succ = point_of_succ0 } = x_20765
1835  in
1836  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1837
1838(** val params_rect_Type5 :
1839    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1840    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1841    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1842    'a1 **)
1843let rec params_rect_Type5 h_mk_params x_20767 =
1844  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1845    point_of_label0; point_of_succ = point_of_succ0 } = x_20767
1846  in
1847  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1848
1849(** val params_rect_Type3 :
1850    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1851    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1852    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1853    'a1 **)
1854let rec params_rect_Type3 h_mk_params x_20769 =
1855  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1856    point_of_label0; point_of_succ = point_of_succ0 } = x_20769
1857  in
1858  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1859
1860(** val params_rect_Type2 :
1861    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1862    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1863    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1864    'a1 **)
1865let rec params_rect_Type2 h_mk_params x_20771 =
1866  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1867    point_of_label0; point_of_succ = point_of_succ0 } = x_20771
1868  in
1869  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1870
1871(** val params_rect_Type1 :
1872    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1873    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1874    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1875    'a1 **)
1876let rec params_rect_Type1 h_mk_params x_20773 =
1877  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1878    point_of_label0; point_of_succ = point_of_succ0 } = x_20773
1879  in
1880  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1881
1882(** val params_rect_Type0 :
1883    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1884    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1885    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1886    'a1 **)
1887let rec params_rect_Type0 h_mk_params x_20775 =
1888  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1889    point_of_label0; point_of_succ = point_of_succ0 } = x_20775
1890  in
1891  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1892
1893(** val stmt_pars : params -> stmt_params **)
1894let rec stmt_pars xxx =
1895  xxx.stmt_pars
1896
1897type codeT = __
1898
1899type code_point = __
1900
1901(** val stmt_at :
1902    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1903let rec stmt_at xxx =
1904  xxx.stmt_at
1905
1906(** val point_of_label :
1907    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1908let rec point_of_label xxx =
1909  xxx.point_of_label
1910
1911(** val point_of_succ : params -> __ -> __ -> __ **)
1912let rec point_of_succ xxx =
1913  xxx.point_of_succ
1914
1915(** val params_inv_rect_Type4 :
1916    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1917    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1918    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1919let params_inv_rect_Type4 hterm h1 =
1920  let hcut = params_rect_Type4 h1 hterm in hcut __
1921
1922(** val params_inv_rect_Type3 :
1923    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1924    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1925    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1926let params_inv_rect_Type3 hterm h1 =
1927  let hcut = params_rect_Type3 h1 hterm in hcut __
1928
1929(** val params_inv_rect_Type2 :
1930    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1931    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1932    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1933let params_inv_rect_Type2 hterm h1 =
1934  let hcut = params_rect_Type2 h1 hterm in hcut __
1935
1936(** val params_inv_rect_Type1 :
1937    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1938    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1939    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1940let params_inv_rect_Type1 hterm h1 =
1941  let hcut = params_rect_Type1 h1 hterm in hcut __
1942
1943(** val params_inv_rect_Type0 :
1944    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1945    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1946    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1947let params_inv_rect_Type0 hterm h1 =
1948  let hcut = params_rect_Type0 h1 hterm in hcut __
1949
1950(** val params_jmdiscr : params -> params -> __ **)
1951let params_jmdiscr x y =
1952  Logic.eq_rect_Type2 x
1953    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1954       a5 } = x
1955     in
1956    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1957
1958(** val stmt_pars__o__uns_pars : params -> uns_params **)
1959let stmt_pars__o__uns_pars x0 =
1960  x0.stmt_pars.uns_pars
1961
1962(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1963let stmt_pars__o__uns_pars__o__u_pars x0 =
1964  uns_pars__o__u_pars x0.stmt_pars
1965
1966(** val code_has_point :
1967    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1968let code_has_point p globals c pt =
1969  match p.stmt_at globals c pt with
1970  | Types.None -> Bool.False
1971  | Types.Some x -> Bool.True
1972
1973(** val code_has_label :
1974    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1975let code_has_label p globals c l =
1976  match p.point_of_label globals c l with
1977  | Types.None -> Bool.False
1978  | Types.Some pt -> code_has_point p globals c pt
1979
1980(** val stmt_explicit_labels :
1981    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1982    List.list **)
1983let stmt_explicit_labels p globals = function
1984| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1985| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
1986| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1987
1988(** val stmt_implicit_label :
1989    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1990    Types.option **)
1991let stmt_implicit_label p globals = function
1992| Sequential (x, s0) -> p.succ_label s0
1993| Final x -> Types.None
1994| FCOND (x0, x1, x2) -> Types.None
1995
1996(** val stmt_labels :
1997    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1998    List.list **)
1999let stmt_labels p g stmt =
2000  List.append
2001    (match stmt_implicit_label p g stmt with
2002     | Types.None -> List.Nil
2003     | Types.Some l -> List.Cons (l, List.Nil))
2004    (stmt_explicit_labels p g stmt)
2005
2006(** val stmt_registers :
2007    stmt_params -> AST.ident List.list -> joint_statement ->
2008    Registers.register List.list **)
2009let stmt_registers p globals = function
2010| Sequential (c, x) ->
2011  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2012| Final c ->
2013  (match c with
2014   | GOTO x -> List.Nil
2015   | RETURN -> List.Nil
2016   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2017| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2018
2019type lin_params =
2020  uns_params
2021  (* singleton inductive, whose constructor was mk_lin_params *)
2022
2023(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2024let rec lin_params_rect_Type4 h_mk_lin_params x_20798 =
2025  let l_u_pars = x_20798 in h_mk_lin_params l_u_pars
2026
2027(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2028let rec lin_params_rect_Type5 h_mk_lin_params x_20800 =
2029  let l_u_pars = x_20800 in h_mk_lin_params l_u_pars
2030
2031(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2032let rec lin_params_rect_Type3 h_mk_lin_params x_20802 =
2033  let l_u_pars = x_20802 in h_mk_lin_params l_u_pars
2034
2035(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2036let rec lin_params_rect_Type2 h_mk_lin_params x_20804 =
2037  let l_u_pars = x_20804 in h_mk_lin_params l_u_pars
2038
2039(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2040let rec lin_params_rect_Type1 h_mk_lin_params x_20806 =
2041  let l_u_pars = x_20806 in h_mk_lin_params l_u_pars
2042
2043(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2044let rec lin_params_rect_Type0 h_mk_lin_params x_20808 =
2045  let l_u_pars = x_20808 in h_mk_lin_params l_u_pars
2046
2047(** val l_u_pars : lin_params -> uns_params **)
2048let rec l_u_pars xxx =
2049  let yyy = xxx in yyy
2050
2051(** val lin_params_inv_rect_Type4 :
2052    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2053let lin_params_inv_rect_Type4 hterm h1 =
2054  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2055
2056(** val lin_params_inv_rect_Type3 :
2057    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2058let lin_params_inv_rect_Type3 hterm h1 =
2059  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2060
2061(** val lin_params_inv_rect_Type2 :
2062    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2063let lin_params_inv_rect_Type2 hterm h1 =
2064  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2065
2066(** val lin_params_inv_rect_Type1 :
2067    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2068let lin_params_inv_rect_Type1 hterm h1 =
2069  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2070
2071(** val lin_params_inv_rect_Type0 :
2072    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2073let lin_params_inv_rect_Type0 hterm h1 =
2074  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2075
2076(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2077let lin_params_jmdiscr x y =
2078  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2079
2080(** val lin_params_to_params : lin_params -> params **)
2081let lin_params_to_params lp =
2082  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2083    Types.None); has_fcond = Bool.True }; stmt_at =
2084    (fun globals code point ->
2085    Obj.magic
2086      (Monad.m_bind0 (Monad.max_def Option.option)
2087        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2088        (fun ls ->
2089        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2090    point_of_label = (fun globals c lbl ->
2091    Util.if_then_else_safe
2092      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2093        (Obj.magic c)) (fun _ ->
2094      Obj.magic
2095        (Monad.m_return0 (Monad.max_def Option.option)
2096          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2097            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2098    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2099
2100(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2101let lp_to_p__o__stmt_pars x0 =
2102  (lin_params_to_params x0).stmt_pars
2103
2104(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2105let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2106  stmt_pars__o__uns_pars (lin_params_to_params x0)
2107
2108(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2109    lin_params -> unserialized_params **)
2110let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2111  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2112
2113type graph_params =
2114  uns_params
2115  (* singleton inductive, whose constructor was mk_graph_params *)
2116
2117(** val graph_params_rect_Type4 :
2118    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2119let rec graph_params_rect_Type4 h_mk_graph_params x_20824 =
2120  let g_u_pars = x_20824 in h_mk_graph_params g_u_pars
2121
2122(** val graph_params_rect_Type5 :
2123    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2124let rec graph_params_rect_Type5 h_mk_graph_params x_20826 =
2125  let g_u_pars = x_20826 in h_mk_graph_params g_u_pars
2126
2127(** val graph_params_rect_Type3 :
2128    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2129let rec graph_params_rect_Type3 h_mk_graph_params x_20828 =
2130  let g_u_pars = x_20828 in h_mk_graph_params g_u_pars
2131
2132(** val graph_params_rect_Type2 :
2133    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2134let rec graph_params_rect_Type2 h_mk_graph_params x_20830 =
2135  let g_u_pars = x_20830 in h_mk_graph_params g_u_pars
2136
2137(** val graph_params_rect_Type1 :
2138    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2139let rec graph_params_rect_Type1 h_mk_graph_params x_20832 =
2140  let g_u_pars = x_20832 in h_mk_graph_params g_u_pars
2141
2142(** val graph_params_rect_Type0 :
2143    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2144let rec graph_params_rect_Type0 h_mk_graph_params x_20834 =
2145  let g_u_pars = x_20834 in h_mk_graph_params g_u_pars
2146
2147(** val g_u_pars : graph_params -> uns_params **)
2148let rec g_u_pars xxx =
2149  let yyy = xxx in yyy
2150
2151(** val graph_params_inv_rect_Type4 :
2152    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2153let graph_params_inv_rect_Type4 hterm h1 =
2154  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2155
2156(** val graph_params_inv_rect_Type3 :
2157    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2158let graph_params_inv_rect_Type3 hterm h1 =
2159  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2160
2161(** val graph_params_inv_rect_Type2 :
2162    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2163let graph_params_inv_rect_Type2 hterm h1 =
2164  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2165
2166(** val graph_params_inv_rect_Type1 :
2167    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2168let graph_params_inv_rect_Type1 hterm h1 =
2169  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2170
2171(** val graph_params_inv_rect_Type0 :
2172    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2173let graph_params_inv_rect_Type0 hterm h1 =
2174  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2175
2176(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2177let graph_params_jmdiscr x y =
2178  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2179
2180(** val graph_params_to_params : graph_params -> params **)
2181let graph_params_to_params gp =
2182  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2183    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2184    (fun globals code ->
2185    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2186    point_of_label = (fun x x0 lbl ->
2187    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2188    point_of_succ = (fun x lbl -> lbl) }
2189
2190(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2191let gp_to_p__o__stmt_pars x0 =
2192  (graph_params_to_params x0).stmt_pars
2193
2194(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2195let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2196  stmt_pars__o__uns_pars (graph_params_to_params x0)
2197
2198(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2199    graph_params -> unserialized_params **)
2200let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2201  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2202
2203type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2204                                 joint_if_runiverse : Identifiers.universe;
2205                                 joint_if_result : __; joint_if_params : 
2206                                 __; joint_if_stacksize : Nat.nat;
2207                                 joint_if_local_stacksize : Nat.nat;
2208                                 joint_if_code : __; joint_if_entry : 
2209                                 __ }
2210
2211(** val joint_internal_function_rect_Type4 :
2212    params -> AST.ident List.list -> (Identifiers.universe ->
2213    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2214    'a1) -> joint_internal_function -> 'a1 **)
2215let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 =
2216  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2217    joint_if_runiverse0; joint_if_result = joint_if_result0;
2218    joint_if_params = joint_if_params0; joint_if_stacksize =
2219    joint_if_stacksize0; joint_if_local_stacksize =
2220    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2221    joint_if_entry = joint_if_entry0 } = x_20850
2222  in
2223  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2224    joint_if_result0 joint_if_params0 joint_if_stacksize0
2225    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2226
2227(** val joint_internal_function_rect_Type5 :
2228    params -> AST.ident List.list -> (Identifiers.universe ->
2229    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2230    'a1) -> joint_internal_function -> 'a1 **)
2231let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 =
2232  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2233    joint_if_runiverse0; joint_if_result = joint_if_result0;
2234    joint_if_params = joint_if_params0; joint_if_stacksize =
2235    joint_if_stacksize0; joint_if_local_stacksize =
2236    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2237    joint_if_entry = joint_if_entry0 } = x_20852
2238  in
2239  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2240    joint_if_result0 joint_if_params0 joint_if_stacksize0
2241    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2242
2243(** val joint_internal_function_rect_Type3 :
2244    params -> AST.ident List.list -> (Identifiers.universe ->
2245    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2246    'a1) -> joint_internal_function -> 'a1 **)
2247let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 =
2248  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2249    joint_if_runiverse0; joint_if_result = joint_if_result0;
2250    joint_if_params = joint_if_params0; joint_if_stacksize =
2251    joint_if_stacksize0; joint_if_local_stacksize =
2252    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2253    joint_if_entry = joint_if_entry0 } = x_20854
2254  in
2255  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2256    joint_if_result0 joint_if_params0 joint_if_stacksize0
2257    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2258
2259(** val joint_internal_function_rect_Type2 :
2260    params -> AST.ident List.list -> (Identifiers.universe ->
2261    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2262    'a1) -> joint_internal_function -> 'a1 **)
2263let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 =
2264  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2265    joint_if_runiverse0; joint_if_result = joint_if_result0;
2266    joint_if_params = joint_if_params0; joint_if_stacksize =
2267    joint_if_stacksize0; joint_if_local_stacksize =
2268    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2269    joint_if_entry = joint_if_entry0 } = x_20856
2270  in
2271  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2272    joint_if_result0 joint_if_params0 joint_if_stacksize0
2273    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2274
2275(** val joint_internal_function_rect_Type1 :
2276    params -> AST.ident List.list -> (Identifiers.universe ->
2277    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2278    'a1) -> joint_internal_function -> 'a1 **)
2279let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 =
2280  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2281    joint_if_runiverse0; joint_if_result = joint_if_result0;
2282    joint_if_params = joint_if_params0; joint_if_stacksize =
2283    joint_if_stacksize0; joint_if_local_stacksize =
2284    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2285    joint_if_entry = joint_if_entry0 } = x_20858
2286  in
2287  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2288    joint_if_result0 joint_if_params0 joint_if_stacksize0
2289    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2290
2291(** val joint_internal_function_rect_Type0 :
2292    params -> AST.ident List.list -> (Identifiers.universe ->
2293    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2294    'a1) -> joint_internal_function -> 'a1 **)
2295let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 =
2296  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2297    joint_if_runiverse0; joint_if_result = joint_if_result0;
2298    joint_if_params = joint_if_params0; joint_if_stacksize =
2299    joint_if_stacksize0; joint_if_local_stacksize =
2300    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2301    joint_if_entry = joint_if_entry0 } = x_20860
2302  in
2303  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2304    joint_if_result0 joint_if_params0 joint_if_stacksize0
2305    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2306
2307(** val joint_if_luniverse :
2308    params -> AST.ident List.list -> joint_internal_function ->
2309    Identifiers.universe **)
2310let rec joint_if_luniverse p globals xxx =
2311  xxx.joint_if_luniverse
2312
2313(** val joint_if_runiverse :
2314    params -> AST.ident List.list -> joint_internal_function ->
2315    Identifiers.universe **)
2316let rec joint_if_runiverse p globals xxx =
2317  xxx.joint_if_runiverse
2318
2319(** val joint_if_result :
2320    params -> AST.ident List.list -> joint_internal_function -> __ **)
2321let rec joint_if_result p globals xxx =
2322  xxx.joint_if_result
2323
2324(** val joint_if_params :
2325    params -> AST.ident List.list -> joint_internal_function -> __ **)
2326let rec joint_if_params p globals xxx =
2327  xxx.joint_if_params
2328
2329(** val joint_if_stacksize :
2330    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2331let rec joint_if_stacksize p globals xxx =
2332  xxx.joint_if_stacksize
2333
2334(** val joint_if_local_stacksize :
2335    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2336let rec joint_if_local_stacksize p globals xxx =
2337  xxx.joint_if_local_stacksize
2338
2339(** val joint_if_code :
2340    params -> AST.ident List.list -> joint_internal_function -> __ **)
2341let rec joint_if_code p globals xxx =
2342  xxx.joint_if_code
2343
2344(** val joint_if_entry :
2345    params -> AST.ident List.list -> joint_internal_function -> __ **)
2346let rec joint_if_entry p globals xxx =
2347  xxx.joint_if_entry
2348
2349(** val joint_internal_function_inv_rect_Type4 :
2350    params -> AST.ident List.list -> joint_internal_function ->
2351    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2352    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2353let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2354  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2355
2356(** val joint_internal_function_inv_rect_Type3 :
2357    params -> AST.ident List.list -> joint_internal_function ->
2358    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2359    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2360let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2361  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2362
2363(** val joint_internal_function_inv_rect_Type2 :
2364    params -> AST.ident List.list -> joint_internal_function ->
2365    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2366    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2367let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2368  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2369
2370(** val joint_internal_function_inv_rect_Type1 :
2371    params -> AST.ident List.list -> joint_internal_function ->
2372    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2373    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2374let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2375  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2376
2377(** val joint_internal_function_inv_rect_Type0 :
2378    params -> AST.ident List.list -> joint_internal_function ->
2379    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2380    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2381let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2382  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2383
2384(** val joint_internal_function_jmdiscr :
2385    params -> AST.ident List.list -> joint_internal_function ->
2386    joint_internal_function -> __ **)
2387let joint_internal_function_jmdiscr a1 a2 x y =
2388  Logic.eq_rect_Type2 x
2389    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2390       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2391       joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2392       a7 } = x
2393     in
2394    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2395
2396(** val good_if_rect_Type4 :
2397    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2398    __ -> __ -> __ -> 'a1) -> 'a1 **)
2399let rec good_if_rect_Type4 p globals def h_mk_good_if =
2400  h_mk_good_if __ __ __ __ __
2401
2402(** val good_if_rect_Type5 :
2403    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2404    __ -> __ -> __ -> 'a1) -> 'a1 **)
2405let rec good_if_rect_Type5 p globals def h_mk_good_if =
2406  h_mk_good_if __ __ __ __ __
2407
2408(** val good_if_rect_Type3 :
2409    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2410    __ -> __ -> __ -> 'a1) -> 'a1 **)
2411let rec good_if_rect_Type3 p globals def h_mk_good_if =
2412  h_mk_good_if __ __ __ __ __
2413
2414(** val good_if_rect_Type2 :
2415    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2416    __ -> __ -> __ -> 'a1) -> 'a1 **)
2417let rec good_if_rect_Type2 p globals def h_mk_good_if =
2418  h_mk_good_if __ __ __ __ __
2419
2420(** val good_if_rect_Type1 :
2421    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2422    __ -> __ -> __ -> 'a1) -> 'a1 **)
2423let rec good_if_rect_Type1 p globals def h_mk_good_if =
2424  h_mk_good_if __ __ __ __ __
2425
2426(** val good_if_rect_Type0 :
2427    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2428    __ -> __ -> __ -> 'a1) -> 'a1 **)
2429let rec good_if_rect_Type0 p globals def h_mk_good_if =
2430  h_mk_good_if __ __ __ __ __
2431
2432(** val good_if_inv_rect_Type4 :
2433    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2434    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2435let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2436  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2437
2438(** val good_if_inv_rect_Type3 :
2439    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2440    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2441let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2442  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2443
2444(** val good_if_inv_rect_Type2 :
2445    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2446    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2447let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2448  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2449
2450(** val good_if_inv_rect_Type1 :
2451    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2452    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2453let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2454  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2455
2456(** val good_if_inv_rect_Type0 :
2457    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2458    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2459let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2460  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2461
2462(** val good_if_discr :
2463    params -> AST.ident List.list -> joint_internal_function -> __ **)
2464let good_if_discr a1 a2 a3 =
2465  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2466
2467(** val good_if_jmdiscr :
2468    params -> AST.ident List.list -> joint_internal_function -> __ **)
2469let good_if_jmdiscr a1 a2 a3 =
2470  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2471
2472type joint_closed_internal_function = joint_internal_function Types.sig0
2473
2474(** val set_joint_code :
2475    AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2476    joint_internal_function **)
2477let set_joint_code globals pars int_fun graph entry =
2478  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2479    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2480    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2481    int_fun.joint_if_stacksize; joint_if_local_stacksize =
2482    int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2483    entry }
2484
2485(** val set_luniverse :
2486    params -> AST.ident List.list -> joint_internal_function ->
2487    Identifiers.universe -> joint_internal_function **)
2488let set_luniverse globals pars p luniverse =
2489  { joint_if_luniverse = luniverse; joint_if_runiverse =
2490    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2491    joint_if_params = p.joint_if_params; joint_if_stacksize =
2492    p.joint_if_stacksize; joint_if_local_stacksize =
2493    p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2494    joint_if_entry = p.joint_if_entry }
2495
2496(** val set_runiverse :
2497    params -> AST.ident List.list -> joint_internal_function ->
2498    Identifiers.universe -> joint_internal_function **)
2499let set_runiverse globals pars p runiverse =
2500  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2501    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2502    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2503    joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2504    p.joint_if_code; joint_if_entry = p.joint_if_entry }
2505
2506(** val add_graph :
2507    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2508    joint_internal_function -> joint_internal_function **)
2509let add_graph g_pars globals l stmt p =
2510  let code =
2511    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2512      stmt
2513  in
2514  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2515  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2516  joint_if_params = p.joint_if_params; joint_if_stacksize =
2517  p.joint_if_stacksize; joint_if_local_stacksize =
2518  p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2519  joint_if_entry = p.joint_if_entry }
2520
2521type joint_function = joint_closed_internal_function AST.fundef
2522
2523type joint_program = (joint_function, Nat.nat) AST.program
2524
2525type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2526
2527(** val stack_cost : params -> joint_program -> stack_cost_model **)
2528let stack_cost p pr =
2529  List.foldr (fun id_fun acc ->
2530    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2531    (match fun0 with
2532     | AST.Internal jif ->
2533       List.Cons ({ Types.fst = id; Types.snd =
2534         (Types.pi1 jif).joint_if_stacksize }, acc)
2535     | AST.External x -> acc)) List.Nil pr.AST.prog_funct
2536
2537(** val globals_stacksize : params -> joint_program -> Nat.nat **)
2538let globals_stacksize pars p =
2539  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2540    entry.Types.snd) p.AST.prog_vars
2541
Note: See TracBrowser for help on using the repository browser.