source: extracted/joint.ml @ 2993

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 111.3 KB
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83open BackEndOps
84
85open CostLabel
86
87open Order
88
89open Registers
90
91open I8051
92
93open BitVectorTrie
94
95open Graphs
96
97open LabelledObjects
98
99open Sets
100
101open Listb
102
103open String
104
105type 't argument =
106| Reg of 't
107| Imm of BitVector.byte
108
109(** val argument_rect_Type4 :
110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
111let rec argument_rect_Type4 h_Reg h_Imm = function
112| Reg x_16908 -> h_Reg x_16908
113| Imm x_16909 -> h_Imm x_16909
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_16913 -> h_Reg x_16913
119| Imm x_16914 -> h_Imm x_16914
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_16918 -> h_Reg x_16918
125| Imm x_16919 -> h_Imm x_16919
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_16923 -> h_Reg x_16923
131| Imm x_16924 -> h_Imm x_16924
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_16928 -> h_Reg x_16928
137| Imm x_16929 -> h_Imm x_16929
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_16933 -> h_Reg x_16933
143| Imm x_16934 -> h_Imm x_16934
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_16969 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_16969
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_16971 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_16971
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_16973 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_16973
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_16975 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_16975
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_16977 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_16977
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_16979 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_16979
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_16996 =
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_16996
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_16998 =
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_16998
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_17000 =
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_17000
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_17002 =
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_17002
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_17004 =
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_17004
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_17006 =
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_17006
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_17036 =
808  let { u_pars = u_pars0; functs = functs0 } = x_17036 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_17038 =
815  let { u_pars = u_pars0; functs = functs0 } = x_17038 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_17040 =
822  let { u_pars = u_pars0; functs = functs0 } = x_17040 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_17042 =
829  let { u_pars = u_pars0; functs = functs0 } = x_17042 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_17044 =
836  let { u_pars = u_pars0; functs = functs0 } = x_17044 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_17046 =
843  let { u_pars = u_pars0; functs = functs0 } = x_17046 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_17101 -> h_COMMENT x_17101
914| MOVE x_17102 -> h_MOVE x_17102
915| POP x_17103 -> h_POP x_17103
916| PUSH x_17104 -> h_PUSH x_17104
917| ADDRESS (i, x_17106, x_17105) -> h_ADDRESS i __ x_17106 x_17105
918| OPACCS (x_17112, x_17111, x_17110, x_17109, x_17108) ->
919  h_OPACCS x_17112 x_17111 x_17110 x_17109 x_17108
920| OP1 (x_17115, x_17114, x_17113) -> h_OP1 x_17115 x_17114 x_17113
921| OP2 (x_17119, x_17118, x_17117, x_17116) ->
922  h_OP2 x_17119 x_17118 x_17117 x_17116
923| CLEAR_CARRY -> h_CLEAR_CARRY
924| SET_CARRY -> h_SET_CARRY
925| LOAD (x_17122, x_17121, x_17120) -> h_LOAD x_17122 x_17121 x_17120
926| STORE (x_17125, x_17124, x_17123) -> h_STORE x_17125 x_17124 x_17123
927| Extension_seq x_17126 -> h_extension_seq x_17126
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_17141 -> h_COMMENT x_17141
938| MOVE x_17142 -> h_MOVE x_17142
939| POP x_17143 -> h_POP x_17143
940| PUSH x_17144 -> h_PUSH x_17144
941| ADDRESS (i, x_17146, x_17145) -> h_ADDRESS i __ x_17146 x_17145
942| OPACCS (x_17152, x_17151, x_17150, x_17149, x_17148) ->
943  h_OPACCS x_17152 x_17151 x_17150 x_17149 x_17148
944| OP1 (x_17155, x_17154, x_17153) -> h_OP1 x_17155 x_17154 x_17153
945| OP2 (x_17159, x_17158, x_17157, x_17156) ->
946  h_OP2 x_17159 x_17158 x_17157 x_17156
947| CLEAR_CARRY -> h_CLEAR_CARRY
948| SET_CARRY -> h_SET_CARRY
949| LOAD (x_17162, x_17161, x_17160) -> h_LOAD x_17162 x_17161 x_17160
950| STORE (x_17165, x_17164, x_17163) -> h_STORE x_17165 x_17164 x_17163
951| Extension_seq x_17166 -> h_extension_seq x_17166
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_17181 -> h_COMMENT x_17181
962| MOVE x_17182 -> h_MOVE x_17182
963| POP x_17183 -> h_POP x_17183
964| PUSH x_17184 -> h_PUSH x_17184
965| ADDRESS (i, x_17186, x_17185) -> h_ADDRESS i __ x_17186 x_17185
966| OPACCS (x_17192, x_17191, x_17190, x_17189, x_17188) ->
967  h_OPACCS x_17192 x_17191 x_17190 x_17189 x_17188
968| OP1 (x_17195, x_17194, x_17193) -> h_OP1 x_17195 x_17194 x_17193
969| OP2 (x_17199, x_17198, x_17197, x_17196) ->
970  h_OP2 x_17199 x_17198 x_17197 x_17196
971| CLEAR_CARRY -> h_CLEAR_CARRY
972| SET_CARRY -> h_SET_CARRY
973| LOAD (x_17202, x_17201, x_17200) -> h_LOAD x_17202 x_17201 x_17200
974| STORE (x_17205, x_17204, x_17203) -> h_STORE x_17205 x_17204 x_17203
975| Extension_seq x_17206 -> h_extension_seq x_17206
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_17221 -> h_COMMENT x_17221
986| MOVE x_17222 -> h_MOVE x_17222
987| POP x_17223 -> h_POP x_17223
988| PUSH x_17224 -> h_PUSH x_17224
989| ADDRESS (i, x_17226, x_17225) -> h_ADDRESS i __ x_17226 x_17225
990| OPACCS (x_17232, x_17231, x_17230, x_17229, x_17228) ->
991  h_OPACCS x_17232 x_17231 x_17230 x_17229 x_17228
992| OP1 (x_17235, x_17234, x_17233) -> h_OP1 x_17235 x_17234 x_17233
993| OP2 (x_17239, x_17238, x_17237, x_17236) ->
994  h_OP2 x_17239 x_17238 x_17237 x_17236
995| CLEAR_CARRY -> h_CLEAR_CARRY
996| SET_CARRY -> h_SET_CARRY
997| LOAD (x_17242, x_17241, x_17240) -> h_LOAD x_17242 x_17241 x_17240
998| STORE (x_17245, x_17244, x_17243) -> h_STORE x_17245 x_17244 x_17243
999| Extension_seq x_17246 -> h_extension_seq x_17246
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_17261 -> h_COMMENT x_17261
1010| MOVE x_17262 -> h_MOVE x_17262
1011| POP x_17263 -> h_POP x_17263
1012| PUSH x_17264 -> h_PUSH x_17264
1013| ADDRESS (i, x_17266, x_17265) -> h_ADDRESS i __ x_17266 x_17265
1014| OPACCS (x_17272, x_17271, x_17270, x_17269, x_17268) ->
1015  h_OPACCS x_17272 x_17271 x_17270 x_17269 x_17268
1016| OP1 (x_17275, x_17274, x_17273) -> h_OP1 x_17275 x_17274 x_17273
1017| OP2 (x_17279, x_17278, x_17277, x_17276) ->
1018  h_OP2 x_17279 x_17278 x_17277 x_17276
1019| CLEAR_CARRY -> h_CLEAR_CARRY
1020| SET_CARRY -> h_SET_CARRY
1021| LOAD (x_17282, x_17281, x_17280) -> h_LOAD x_17282 x_17281 x_17280
1022| STORE (x_17285, x_17284, x_17283) -> h_STORE x_17285 x_17284 x_17283
1023| Extension_seq x_17286 -> h_extension_seq x_17286
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_17301 -> h_COMMENT x_17301
1034| MOVE x_17302 -> h_MOVE x_17302
1035| POP x_17303 -> h_POP x_17303
1036| PUSH x_17304 -> h_PUSH x_17304
1037| ADDRESS (i, x_17306, x_17305) -> h_ADDRESS i __ x_17306 x_17305
1038| OPACCS (x_17312, x_17311, x_17310, x_17309, x_17308) ->
1039  h_OPACCS x_17312 x_17311 x_17310 x_17309 x_17308
1040| OP1 (x_17315, x_17314, x_17313) -> h_OP1 x_17315 x_17314 x_17313
1041| OP2 (x_17319, x_17318, x_17317, x_17316) ->
1042  h_OP2 x_17319 x_17318 x_17317 x_17316
1043| CLEAR_CARRY -> h_CLEAR_CARRY
1044| SET_CARRY -> h_SET_CARRY
1045| LOAD (x_17322, x_17321, x_17320) -> h_LOAD x_17322 x_17321 x_17320
1046| STORE (x_17325, x_17324, x_17323) -> h_STORE x_17325 x_17324 x_17323
1047| Extension_seq x_17326 -> h_extension_seq x_17326
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_17593 -> h_COST_LABEL x_17593
1239| CALL (x_17596, x_17595, x_17594) -> h_CALL x_17596 x_17595 x_17594
1240| COND (x_17598, x_17597) -> h_COND x_17598 x_17597
1241| Step_seq x_17599 -> h_step_seq x_17599
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_17605 -> h_COST_LABEL x_17605
1249| CALL (x_17608, x_17607, x_17606) -> h_CALL x_17608 x_17607 x_17606
1250| COND (x_17610, x_17609) -> h_COND x_17610 x_17609
1251| Step_seq x_17611 -> h_step_seq x_17611
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_17617 -> h_COST_LABEL x_17617
1259| CALL (x_17620, x_17619, x_17618) -> h_CALL x_17620 x_17619 x_17618
1260| COND (x_17622, x_17621) -> h_COND x_17622 x_17621
1261| Step_seq x_17623 -> h_step_seq x_17623
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_17629 -> h_COST_LABEL x_17629
1269| CALL (x_17632, x_17631, x_17630) -> h_CALL x_17632 x_17631 x_17630
1270| COND (x_17634, x_17633) -> h_COND x_17634 x_17633
1271| Step_seq x_17635 -> h_step_seq x_17635
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_17641 -> h_COST_LABEL x_17641
1279| CALL (x_17644, x_17643, x_17642) -> h_CALL x_17644 x_17643 x_17642
1280| COND (x_17646, x_17645) -> h_COND x_17646 x_17645
1281| Step_seq x_17647 -> h_step_seq x_17647
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_17653 -> h_COST_LABEL x_17653
1289| CALL (x_17656, x_17655, x_17654) -> h_CALL x_17656 x_17655 x_17654
1290| COND (x_17658, x_17657) -> h_COND x_17658 x_17657
1291| Step_seq x_17659 -> h_step_seq x_17659
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  let r_id =
1362    match id with
1363    | Types.Inl x -> List.Nil
1364    | Types.Inr ptr ->
1365      List.append (functs0.dpl_args ptr.Types.fst)
1366        (functs0.dph_args ptr.Types.snd)
1367  in
1368  List.append r_id
1369    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1370| COND (r, lbl) -> functs0.acc_a_regs r
1371| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1372
1373(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1374    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1375    joint_step Types.sig0 **)
1376let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1377  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1378
1379(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1380    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1381    Types.sig0 **)
1382let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1383  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1384
1385(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1386    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1387let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1388  Step_seq (Extension_seq x2)
1389
1390(** val dpi1__o__seq_to_step__o__inject :
1391    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1392    Types.dPair -> joint_step Types.sig0 **)
1393let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1394  Step_seq x4.Types.dpi1
1395
1396(** val eject__o__seq_to_step__o__inject :
1397    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1398    joint_step Types.sig0 **)
1399let eject__o__seq_to_step__o__inject x0 x1 x4 =
1400  Step_seq (Types.pi1 x4)
1401
1402(** val seq_to_step__o__inject :
1403    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1404    Types.sig0 **)
1405let seq_to_step__o__inject x0 x1 x3 =
1406  Step_seq x3
1407
1408(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1409    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1410    joint_step **)
1411let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1412  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1413
1414(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1415    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1416let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1417  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1418
1419(** val extension_seq_to_seq__o__seq_to_step :
1420    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1421let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1422  Step_seq (Extension_seq x2)
1423
1424(** val dpi1__o__seq_to_step :
1425    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1426    Types.dPair -> joint_step **)
1427let dpi1__o__seq_to_step x0 x1 x3 =
1428  Step_seq x3.Types.dpi1
1429
1430(** val eject__o__seq_to_step :
1431    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1432    joint_step **)
1433let eject__o__seq_to_step x0 x1 x3 =
1434  Step_seq (Types.pi1 x3)
1435
1436(** val step_labels :
1437    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1438    List.list **)
1439let step_labels p globals = function
1440| COST_LABEL x -> List.Nil
1441| CALL (x, x0, x1) -> List.Nil
1442| COND (x, l) -> List.Cons (l, List.Nil)
1443| Step_seq s0 ->
1444  (match s0 with
1445   | COMMENT x -> List.Nil
1446   | MOVE x -> List.Nil
1447   | POP x -> List.Nil
1448   | PUSH x -> List.Nil
1449   | ADDRESS (x, x1, x2) -> List.Nil
1450   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1451   | OP1 (x, x0, x1) -> List.Nil
1452   | OP2 (x, x0, x1, x2) -> List.Nil
1453   | CLEAR_CARRY -> List.Nil
1454   | SET_CARRY -> List.Nil
1455   | LOAD (x, x0, x1) -> List.Nil
1456   | STORE (x, x0, x1) -> List.Nil
1457   | Extension_seq ext -> p.ext_seq_labels ext)
1458
1459type stmt_params = { uns_pars : uns_params;
1460                     succ_label : (__ -> Graphs.label Types.option);
1461                     has_fcond : Bool.bool }
1462
1463(** val stmt_params_rect_Type4 :
1464    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1465    'a1) -> stmt_params -> 'a1 **)
1466let rec stmt_params_rect_Type4 h_mk_stmt_params x_17738 =
1467  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1468    has_fcond0 } = x_17738
1469  in
1470  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1471
1472(** val stmt_params_rect_Type5 :
1473    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1474    'a1) -> stmt_params -> 'a1 **)
1475let rec stmt_params_rect_Type5 h_mk_stmt_params x_17740 =
1476  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1477    has_fcond0 } = x_17740
1478  in
1479  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1480
1481(** val stmt_params_rect_Type3 :
1482    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1483    'a1) -> stmt_params -> 'a1 **)
1484let rec stmt_params_rect_Type3 h_mk_stmt_params x_17742 =
1485  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1486    has_fcond0 } = x_17742
1487  in
1488  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1489
1490(** val stmt_params_rect_Type2 :
1491    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1492    'a1) -> stmt_params -> 'a1 **)
1493let rec stmt_params_rect_Type2 h_mk_stmt_params x_17744 =
1494  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1495    has_fcond0 } = x_17744
1496  in
1497  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1498
1499(** val stmt_params_rect_Type1 :
1500    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1501    'a1) -> stmt_params -> 'a1 **)
1502let rec stmt_params_rect_Type1 h_mk_stmt_params x_17746 =
1503  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1504    has_fcond0 } = x_17746
1505  in
1506  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1507
1508(** val stmt_params_rect_Type0 :
1509    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1510    'a1) -> stmt_params -> 'a1 **)
1511let rec stmt_params_rect_Type0 h_mk_stmt_params x_17748 =
1512  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1513    has_fcond0 } = x_17748
1514  in
1515  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1516
1517(** val uns_pars : stmt_params -> uns_params **)
1518let rec uns_pars xxx =
1519  xxx.uns_pars
1520
1521type succ = __
1522
1523(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1524let rec succ_label xxx =
1525  xxx.succ_label
1526
1527(** val has_fcond : stmt_params -> Bool.bool **)
1528let rec has_fcond xxx =
1529  xxx.has_fcond
1530
1531(** val stmt_params_inv_rect_Type4 :
1532    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1533    Bool.bool -> __ -> 'a1) -> 'a1 **)
1534let stmt_params_inv_rect_Type4 hterm h1 =
1535  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1536
1537(** val stmt_params_inv_rect_Type3 :
1538    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539    Bool.bool -> __ -> 'a1) -> 'a1 **)
1540let stmt_params_inv_rect_Type3 hterm h1 =
1541  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1542
1543(** val stmt_params_inv_rect_Type2 :
1544    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545    Bool.bool -> __ -> 'a1) -> 'a1 **)
1546let stmt_params_inv_rect_Type2 hterm h1 =
1547  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1548
1549(** val stmt_params_inv_rect_Type1 :
1550    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551    Bool.bool -> __ -> 'a1) -> 'a1 **)
1552let stmt_params_inv_rect_Type1 hterm h1 =
1553  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1554
1555(** val stmt_params_inv_rect_Type0 :
1556    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1557    Bool.bool -> __ -> 'a1) -> 'a1 **)
1558let stmt_params_inv_rect_Type0 hterm h1 =
1559  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1560
1561(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1562let stmt_params_jmdiscr x y =
1563  Logic.eq_rect_Type2 x
1564    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1565    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1566
1567(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1568let uns_pars__o__u_pars x0 =
1569  x0.uns_pars.u_pars
1570
1571type joint_fin_step =
1572| GOTO of Graphs.label
1573| RETURN
1574| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1575
1576(** val joint_fin_step_rect_Type4 :
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_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1580| GOTO x_17772 -> h_GOTO x_17772
1581| RETURN -> h_RETURN
1582| TAILCALL (x_17774, x_17773) -> h_TAILCALL __ x_17774 x_17773
1583
1584(** val joint_fin_step_rect_Type5 :
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_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1588| GOTO x_17780 -> h_GOTO x_17780
1589| RETURN -> h_RETURN
1590| TAILCALL (x_17782, x_17781) -> h_TAILCALL __ x_17782 x_17781
1591
1592(** val joint_fin_step_rect_Type3 :
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_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1596| GOTO x_17788 -> h_GOTO x_17788
1597| RETURN -> h_RETURN
1598| TAILCALL (x_17790, x_17789) -> h_TAILCALL __ x_17790 x_17789
1599
1600(** val joint_fin_step_rect_Type2 :
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_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1604| GOTO x_17796 -> h_GOTO x_17796
1605| RETURN -> h_RETURN
1606| TAILCALL (x_17798, x_17797) -> h_TAILCALL __ x_17798 x_17797
1607
1608(** val joint_fin_step_rect_Type1 :
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_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1612| GOTO x_17804 -> h_GOTO x_17804
1613| RETURN -> h_RETURN
1614| TAILCALL (x_17806, x_17805) -> h_TAILCALL __ x_17806 x_17805
1615
1616(** val joint_fin_step_rect_Type0 :
1617    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1618    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1619let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1620| GOTO x_17812 -> h_GOTO x_17812
1621| RETURN -> h_RETURN
1622| TAILCALL (x_17814, x_17813) -> h_TAILCALL __ x_17814 x_17813
1623
1624(** val joint_fin_step_inv_rect_Type4 :
1625    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1626    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1627    __ -> 'a1) -> 'a1 **)
1628let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1629  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1630
1631(** val joint_fin_step_inv_rect_Type3 :
1632    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1633    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1634    __ -> 'a1) -> 'a1 **)
1635let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1636  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1637
1638(** val joint_fin_step_inv_rect_Type2 :
1639    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1640    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1641    __ -> 'a1) -> 'a1 **)
1642let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1643  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1644
1645(** val joint_fin_step_inv_rect_Type1 :
1646    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1647    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1648    __ -> 'a1) -> 'a1 **)
1649let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1650  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1651
1652(** val joint_fin_step_inv_rect_Type0 :
1653    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1654    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1655    __ -> 'a1) -> 'a1 **)
1656let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1657  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1658
1659(** val joint_fin_step_discr :
1660    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1661let joint_fin_step_discr a1 x y =
1662  Logic.eq_rect_Type2 x
1663    (match x with
1664     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1665     | RETURN -> Obj.magic (fun _ dH -> dH)
1666     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1667
1668(** val joint_fin_step_jmdiscr :
1669    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1670let joint_fin_step_jmdiscr a1 x y =
1671  Logic.eq_rect_Type2 x
1672    (match x with
1673     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1674     | RETURN -> Obj.magic (fun _ dH -> dH)
1675     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1676
1677(** val fin_step_labels :
1678    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1679let fin_step_labels p = function
1680| GOTO l -> List.Cons (l, List.Nil)
1681| RETURN -> List.Nil
1682| TAILCALL (x0, x1) -> List.Nil
1683
1684type joint_statement =
1685| Sequential of joint_step * __
1686| Final of joint_fin_step
1687| FCOND of __ * Graphs.label * Graphs.label
1688
1689(** val joint_statement_rect_Type4 :
1690    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1691    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1692    'a1) -> joint_statement -> 'a1 **)
1693let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1694| Sequential (x_17880, x_17879) -> h_sequential x_17880 x_17879
1695| Final x_17881 -> h_final x_17881
1696| FCOND (x_17884, x_17883, x_17882) -> h_FCOND __ x_17884 x_17883 x_17882
1697
1698(** val joint_statement_rect_Type5 :
1699    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1700    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1701    'a1) -> joint_statement -> 'a1 **)
1702let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1703| Sequential (x_17891, x_17890) -> h_sequential x_17891 x_17890
1704| Final x_17892 -> h_final x_17892
1705| FCOND (x_17895, x_17894, x_17893) -> h_FCOND __ x_17895 x_17894 x_17893
1706
1707(** val joint_statement_rect_Type3 :
1708    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1709    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1710    'a1) -> joint_statement -> 'a1 **)
1711let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1712| Sequential (x_17902, x_17901) -> h_sequential x_17902 x_17901
1713| Final x_17903 -> h_final x_17903
1714| FCOND (x_17906, x_17905, x_17904) -> h_FCOND __ x_17906 x_17905 x_17904
1715
1716(** val joint_statement_rect_Type2 :
1717    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1718    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1719    'a1) -> joint_statement -> 'a1 **)
1720let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1721| Sequential (x_17913, x_17912) -> h_sequential x_17913 x_17912
1722| Final x_17914 -> h_final x_17914
1723| FCOND (x_17917, x_17916, x_17915) -> h_FCOND __ x_17917 x_17916 x_17915
1724
1725(** val joint_statement_rect_Type1 :
1726    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1727    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1728    'a1) -> joint_statement -> 'a1 **)
1729let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1730| Sequential (x_17924, x_17923) -> h_sequential x_17924 x_17923
1731| Final x_17925 -> h_final x_17925
1732| FCOND (x_17928, x_17927, x_17926) -> h_FCOND __ x_17928 x_17927 x_17926
1733
1734(** val joint_statement_rect_Type0 :
1735    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1736    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1737    'a1) -> joint_statement -> 'a1 **)
1738let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1739| Sequential (x_17935, x_17934) -> h_sequential x_17935 x_17934
1740| Final x_17936 -> h_final x_17936
1741| FCOND (x_17939, x_17938, x_17937) -> h_FCOND __ x_17939 x_17938 x_17937
1742
1743(** val joint_statement_inv_rect_Type4 :
1744    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1745    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1746    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1747let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1748  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1749
1750(** val joint_statement_inv_rect_Type3 :
1751    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1752    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1753    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1754let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1755  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1756
1757(** val joint_statement_inv_rect_Type2 :
1758    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1759    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1760    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1761let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1762  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1763
1764(** val joint_statement_inv_rect_Type1 :
1765    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1766    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1767    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1768let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1769  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1770
1771(** val joint_statement_inv_rect_Type0 :
1772    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1773    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1774    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1775let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1776  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1777
1778(** val joint_statement_discr :
1779    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1780    -> __ **)
1781let joint_statement_discr a1 a2 x y =
1782  Logic.eq_rect_Type2 x
1783    (match x with
1784     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1785     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1786     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1787
1788(** val joint_statement_jmdiscr :
1789    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1790    -> __ **)
1791let joint_statement_jmdiscr a1 a2 x y =
1792  Logic.eq_rect_Type2 x
1793    (match x with
1794     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1795     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1796     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1797
1798(** val dpi1__o__fin_step_to_stmt__o__inject :
1799    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1800    -> joint_statement Types.sig0 **)
1801let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1802  Final x4.Types.dpi1
1803
1804(** val eject__o__fin_step_to_stmt__o__inject :
1805    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1806    joint_statement Types.sig0 **)
1807let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1808  Final (Types.pi1 x4)
1809
1810(** val fin_step_to_stmt__o__inject :
1811    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1812    Types.sig0 **)
1813let fin_step_to_stmt__o__inject x0 x1 x3 =
1814  Final x3
1815
1816(** val dpi1__o__fin_step_to_stmt :
1817    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1818    -> joint_statement **)
1819let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1820  Final x3.Types.dpi1
1821
1822(** val eject__o__fin_step_to_stmt :
1823    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1824    joint_statement **)
1825let eject__o__fin_step_to_stmt x0 x1 x3 =
1826  Final (Types.pi1 x3)
1827
1828type params = { stmt_pars : stmt_params;
1829                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1830                          Types.option);
1831                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1832                                 -> __ Types.option);
1833                point_of_succ : (__ -> __ -> __) }
1834
1835(** val params_rect_Type4 :
1836    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1837    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1838    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1839    'a1 **)
1840let rec params_rect_Type4 h_mk_params x_18012 =
1841  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1842    point_of_label0; point_of_succ = point_of_succ0 } = x_18012
1843  in
1844  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1845
1846(** val params_rect_Type5 :
1847    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1848    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1849    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1850    'a1 **)
1851let rec params_rect_Type5 h_mk_params x_18014 =
1852  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1853    point_of_label0; point_of_succ = point_of_succ0 } = x_18014
1854  in
1855  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1856
1857(** val params_rect_Type3 :
1858    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1859    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1860    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1861    'a1 **)
1862let rec params_rect_Type3 h_mk_params x_18016 =
1863  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1864    point_of_label0; point_of_succ = point_of_succ0 } = x_18016
1865  in
1866  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1867
1868(** val params_rect_Type2 :
1869    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1870    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1871    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1872    'a1 **)
1873let rec params_rect_Type2 h_mk_params x_18018 =
1874  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1875    point_of_label0; point_of_succ = point_of_succ0 } = x_18018
1876  in
1877  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1878
1879(** val params_rect_Type1 :
1880    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1881    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1882    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1883    'a1 **)
1884let rec params_rect_Type1 h_mk_params x_18020 =
1885  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1886    point_of_label0; point_of_succ = point_of_succ0 } = x_18020
1887  in
1888  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1889
1890(** val params_rect_Type0 :
1891    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1892    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1893    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1894    'a1 **)
1895let rec params_rect_Type0 h_mk_params x_18022 =
1896  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1897    point_of_label0; point_of_succ = point_of_succ0 } = x_18022
1898  in
1899  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1900
1901(** val stmt_pars : params -> stmt_params **)
1902let rec stmt_pars xxx =
1903  xxx.stmt_pars
1904
1905type codeT = __
1906
1907type code_point = __
1908
1909(** val stmt_at :
1910    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1911let rec stmt_at xxx =
1912  xxx.stmt_at
1913
1914(** val point_of_label :
1915    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1916let rec point_of_label xxx =
1917  xxx.point_of_label
1918
1919(** val point_of_succ : params -> __ -> __ -> __ **)
1920let rec point_of_succ xxx =
1921  xxx.point_of_succ
1922
1923(** val params_inv_rect_Type4 :
1924    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1925    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1926    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1927let params_inv_rect_Type4 hterm h1 =
1928  let hcut = params_rect_Type4 h1 hterm in hcut __
1929
1930(** val params_inv_rect_Type3 :
1931    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1932    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1933    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1934let params_inv_rect_Type3 hterm h1 =
1935  let hcut = params_rect_Type3 h1 hterm in hcut __
1936
1937(** val params_inv_rect_Type2 :
1938    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1939    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1940    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1941let params_inv_rect_Type2 hterm h1 =
1942  let hcut = params_rect_Type2 h1 hterm in hcut __
1943
1944(** val params_inv_rect_Type1 :
1945    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1946    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1947    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1948let params_inv_rect_Type1 hterm h1 =
1949  let hcut = params_rect_Type1 h1 hterm in hcut __
1950
1951(** val params_inv_rect_Type0 :
1952    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1953    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1954    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1955let params_inv_rect_Type0 hterm h1 =
1956  let hcut = params_rect_Type0 h1 hterm in hcut __
1957
1958(** val params_jmdiscr : params -> params -> __ **)
1959let params_jmdiscr x y =
1960  Logic.eq_rect_Type2 x
1961    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1962       a5 } = x
1963     in
1964    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1965
1966(** val stmt_pars__o__uns_pars : params -> uns_params **)
1967let stmt_pars__o__uns_pars x0 =
1968  x0.stmt_pars.uns_pars
1969
1970(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1971let stmt_pars__o__uns_pars__o__u_pars x0 =
1972  uns_pars__o__u_pars x0.stmt_pars
1973
1974(** val code_has_point :
1975    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1976let code_has_point p globals c pt =
1977  match p.stmt_at globals c pt with
1978  | Types.None -> Bool.False
1979  | Types.Some x -> Bool.True
1980
1981(** val code_has_label :
1982    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1983let code_has_label p globals c l =
1984  match p.point_of_label globals c l with
1985  | Types.None -> Bool.False
1986  | Types.Some pt -> code_has_point p globals c pt
1987
1988(** val stmt_explicit_labels :
1989    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1990    List.list **)
1991let stmt_explicit_labels p globals = function
1992| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1993| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
1994| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1995
1996(** val stmt_implicit_label :
1997    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1998    Types.option **)
1999let stmt_implicit_label p globals = function
2000| Sequential (x, s0) -> p.succ_label s0
2001| Final x -> Types.None
2002| FCOND (x0, x1, x2) -> Types.None
2003
2004(** val stmt_labels :
2005    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2006    List.list **)
2007let stmt_labels p g stmt =
2008  List.append
2009    (match stmt_implicit_label p g stmt with
2010     | Types.None -> List.Nil
2011     | Types.Some l -> List.Cons (l, List.Nil))
2012    (stmt_explicit_labels p g stmt)
2013
2014(** val stmt_registers :
2015    stmt_params -> AST.ident List.list -> joint_statement ->
2016    Registers.register List.list **)
2017let stmt_registers p globals = function
2018| Sequential (c, x) ->
2019  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2020| Final c ->
2021  (match c with
2022   | GOTO x -> List.Nil
2023   | RETURN -> List.Nil
2024   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2025| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2026
2027type lin_params =
2028  uns_params
2029  (* singleton inductive, whose constructor was mk_lin_params *)
2030
2031(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2032let rec lin_params_rect_Type4 h_mk_lin_params x_18045 =
2033  let l_u_pars = x_18045 in h_mk_lin_params l_u_pars
2034
2035(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2036let rec lin_params_rect_Type5 h_mk_lin_params x_18047 =
2037  let l_u_pars = x_18047 in h_mk_lin_params l_u_pars
2038
2039(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2040let rec lin_params_rect_Type3 h_mk_lin_params x_18049 =
2041  let l_u_pars = x_18049 in h_mk_lin_params l_u_pars
2042
2043(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2044let rec lin_params_rect_Type2 h_mk_lin_params x_18051 =
2045  let l_u_pars = x_18051 in h_mk_lin_params l_u_pars
2046
2047(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2048let rec lin_params_rect_Type1 h_mk_lin_params x_18053 =
2049  let l_u_pars = x_18053 in h_mk_lin_params l_u_pars
2050
2051(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2052let rec lin_params_rect_Type0 h_mk_lin_params x_18055 =
2053  let l_u_pars = x_18055 in h_mk_lin_params l_u_pars
2054
2055(** val l_u_pars : lin_params -> uns_params **)
2056let rec l_u_pars xxx =
2057  let yyy = xxx in yyy
2058
2059(** val lin_params_inv_rect_Type4 :
2060    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2061let lin_params_inv_rect_Type4 hterm h1 =
2062  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2063
2064(** val lin_params_inv_rect_Type3 :
2065    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2066let lin_params_inv_rect_Type3 hterm h1 =
2067  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2068
2069(** val lin_params_inv_rect_Type2 :
2070    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2071let lin_params_inv_rect_Type2 hterm h1 =
2072  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2073
2074(** val lin_params_inv_rect_Type1 :
2075    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2076let lin_params_inv_rect_Type1 hterm h1 =
2077  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2078
2079(** val lin_params_inv_rect_Type0 :
2080    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2081let lin_params_inv_rect_Type0 hterm h1 =
2082  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2083
2084(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2085let lin_params_jmdiscr x y =
2086  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2087
2088(** val lin_params_to_params : lin_params -> params **)
2089let lin_params_to_params lp =
2090  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2091    Types.None); has_fcond = Bool.True }; stmt_at =
2092    (fun globals code point ->
2093    Obj.magic
2094      (Monad.m_bind0 (Monad.max_def Option.option)
2095        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2096        (fun ls ->
2097        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2098    point_of_label = (fun globals c lbl ->
2099    Util.if_then_else_safe
2100      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2101        (Obj.magic c)) (fun _ ->
2102      Obj.magic
2103        (Monad.m_return0 (Monad.max_def Option.option)
2104          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2105            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2106    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2107
2108(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2109let lp_to_p__o__stmt_pars x0 =
2110  (lin_params_to_params x0).stmt_pars
2111
2112(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2113let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2114  stmt_pars__o__uns_pars (lin_params_to_params x0)
2115
2116(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2117    lin_params -> unserialized_params **)
2118let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2119  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2120
2121type graph_params =
2122  uns_params
2123  (* singleton inductive, whose constructor was mk_graph_params *)
2124
2125(** val graph_params_rect_Type4 :
2126    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2127let rec graph_params_rect_Type4 h_mk_graph_params x_18071 =
2128  let g_u_pars = x_18071 in h_mk_graph_params g_u_pars
2129
2130(** val graph_params_rect_Type5 :
2131    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2132let rec graph_params_rect_Type5 h_mk_graph_params x_18073 =
2133  let g_u_pars = x_18073 in h_mk_graph_params g_u_pars
2134
2135(** val graph_params_rect_Type3 :
2136    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2137let rec graph_params_rect_Type3 h_mk_graph_params x_18075 =
2138  let g_u_pars = x_18075 in h_mk_graph_params g_u_pars
2139
2140(** val graph_params_rect_Type2 :
2141    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2142let rec graph_params_rect_Type2 h_mk_graph_params x_18077 =
2143  let g_u_pars = x_18077 in h_mk_graph_params g_u_pars
2144
2145(** val graph_params_rect_Type1 :
2146    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2147let rec graph_params_rect_Type1 h_mk_graph_params x_18079 =
2148  let g_u_pars = x_18079 in h_mk_graph_params g_u_pars
2149
2150(** val graph_params_rect_Type0 :
2151    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2152let rec graph_params_rect_Type0 h_mk_graph_params x_18081 =
2153  let g_u_pars = x_18081 in h_mk_graph_params g_u_pars
2154
2155(** val g_u_pars : graph_params -> uns_params **)
2156let rec g_u_pars xxx =
2157  let yyy = xxx in yyy
2158
2159(** val graph_params_inv_rect_Type4 :
2160    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2161let graph_params_inv_rect_Type4 hterm h1 =
2162  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2163
2164(** val graph_params_inv_rect_Type3 :
2165    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2166let graph_params_inv_rect_Type3 hterm h1 =
2167  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2168
2169(** val graph_params_inv_rect_Type2 :
2170    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2171let graph_params_inv_rect_Type2 hterm h1 =
2172  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2173
2174(** val graph_params_inv_rect_Type1 :
2175    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2176let graph_params_inv_rect_Type1 hterm h1 =
2177  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2178
2179(** val graph_params_inv_rect_Type0 :
2180    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2181let graph_params_inv_rect_Type0 hterm h1 =
2182  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2183
2184(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2185let graph_params_jmdiscr x y =
2186  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2187
2188(** val graph_params_to_params : graph_params -> params **)
2189let graph_params_to_params gp =
2190  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2191    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2192    (fun globals code ->
2193    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2194    point_of_label = (fun x x0 lbl ->
2195    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2196    point_of_succ = (fun x lbl -> lbl) }
2197
2198(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2199let gp_to_p__o__stmt_pars x0 =
2200  (graph_params_to_params x0).stmt_pars
2201
2202(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2203let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2204  stmt_pars__o__uns_pars (graph_params_to_params x0)
2205
2206(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2207    graph_params -> unserialized_params **)
2208let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2209  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2210
2211type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2212                                 joint_if_runiverse : Identifiers.universe;
2213                                 joint_if_result : __; joint_if_params : 
2214                                 __; joint_if_stacksize : Nat.nat;
2215                                 joint_if_local_stacksize : Nat.nat;
2216                                 joint_if_code : __; joint_if_entry : 
2217                                 __ }
2218
2219(** val joint_internal_function_rect_Type4 :
2220    params -> AST.ident List.list -> (Identifiers.universe ->
2221    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2222    'a1) -> joint_internal_function -> 'a1 **)
2223let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18097 =
2224  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2225    joint_if_runiverse0; joint_if_result = joint_if_result0;
2226    joint_if_params = joint_if_params0; joint_if_stacksize =
2227    joint_if_stacksize0; joint_if_local_stacksize =
2228    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2229    joint_if_entry = joint_if_entry0 } = x_18097
2230  in
2231  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2232    joint_if_result0 joint_if_params0 joint_if_stacksize0
2233    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2234
2235(** val joint_internal_function_rect_Type5 :
2236    params -> AST.ident List.list -> (Identifiers.universe ->
2237    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2238    'a1) -> joint_internal_function -> 'a1 **)
2239let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18099 =
2240  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2241    joint_if_runiverse0; joint_if_result = joint_if_result0;
2242    joint_if_params = joint_if_params0; joint_if_stacksize =
2243    joint_if_stacksize0; joint_if_local_stacksize =
2244    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2245    joint_if_entry = joint_if_entry0 } = x_18099
2246  in
2247  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2248    joint_if_result0 joint_if_params0 joint_if_stacksize0
2249    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2250
2251(** val joint_internal_function_rect_Type3 :
2252    params -> AST.ident List.list -> (Identifiers.universe ->
2253    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2254    'a1) -> joint_internal_function -> 'a1 **)
2255let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18101 =
2256  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2257    joint_if_runiverse0; joint_if_result = joint_if_result0;
2258    joint_if_params = joint_if_params0; joint_if_stacksize =
2259    joint_if_stacksize0; joint_if_local_stacksize =
2260    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2261    joint_if_entry = joint_if_entry0 } = x_18101
2262  in
2263  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2264    joint_if_result0 joint_if_params0 joint_if_stacksize0
2265    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2266
2267(** val joint_internal_function_rect_Type2 :
2268    params -> AST.ident List.list -> (Identifiers.universe ->
2269    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2270    'a1) -> joint_internal_function -> 'a1 **)
2271let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18103 =
2272  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2273    joint_if_runiverse0; joint_if_result = joint_if_result0;
2274    joint_if_params = joint_if_params0; joint_if_stacksize =
2275    joint_if_stacksize0; joint_if_local_stacksize =
2276    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2277    joint_if_entry = joint_if_entry0 } = x_18103
2278  in
2279  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2280    joint_if_result0 joint_if_params0 joint_if_stacksize0
2281    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2282
2283(** val joint_internal_function_rect_Type1 :
2284    params -> AST.ident List.list -> (Identifiers.universe ->
2285    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2286    'a1) -> joint_internal_function -> 'a1 **)
2287let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18105 =
2288  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2289    joint_if_runiverse0; joint_if_result = joint_if_result0;
2290    joint_if_params = joint_if_params0; joint_if_stacksize =
2291    joint_if_stacksize0; joint_if_local_stacksize =
2292    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2293    joint_if_entry = joint_if_entry0 } = x_18105
2294  in
2295  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2296    joint_if_result0 joint_if_params0 joint_if_stacksize0
2297    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2298
2299(** val joint_internal_function_rect_Type0 :
2300    params -> AST.ident List.list -> (Identifiers.universe ->
2301    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2302    'a1) -> joint_internal_function -> 'a1 **)
2303let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18107 =
2304  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2305    joint_if_runiverse0; joint_if_result = joint_if_result0;
2306    joint_if_params = joint_if_params0; joint_if_stacksize =
2307    joint_if_stacksize0; joint_if_local_stacksize =
2308    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2309    joint_if_entry = joint_if_entry0 } = x_18107
2310  in
2311  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2312    joint_if_result0 joint_if_params0 joint_if_stacksize0
2313    joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2314
2315(** val joint_if_luniverse :
2316    params -> AST.ident List.list -> joint_internal_function ->
2317    Identifiers.universe **)
2318let rec joint_if_luniverse p globals xxx =
2319  xxx.joint_if_luniverse
2320
2321(** val joint_if_runiverse :
2322    params -> AST.ident List.list -> joint_internal_function ->
2323    Identifiers.universe **)
2324let rec joint_if_runiverse p globals xxx =
2325  xxx.joint_if_runiverse
2326
2327(** val joint_if_result :
2328    params -> AST.ident List.list -> joint_internal_function -> __ **)
2329let rec joint_if_result p globals xxx =
2330  xxx.joint_if_result
2331
2332(** val joint_if_params :
2333    params -> AST.ident List.list -> joint_internal_function -> __ **)
2334let rec joint_if_params p globals xxx =
2335  xxx.joint_if_params
2336
2337(** val joint_if_stacksize :
2338    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2339let rec joint_if_stacksize p globals xxx =
2340  xxx.joint_if_stacksize
2341
2342(** val joint_if_local_stacksize :
2343    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2344let rec joint_if_local_stacksize p globals xxx =
2345  xxx.joint_if_local_stacksize
2346
2347(** val joint_if_code :
2348    params -> AST.ident List.list -> joint_internal_function -> __ **)
2349let rec joint_if_code p globals xxx =
2350  xxx.joint_if_code
2351
2352(** val joint_if_entry :
2353    params -> AST.ident List.list -> joint_internal_function -> __ **)
2354let rec joint_if_entry p globals xxx =
2355  xxx.joint_if_entry
2356
2357(** val joint_internal_function_inv_rect_Type4 :
2358    params -> AST.ident List.list -> joint_internal_function ->
2359    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2360    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2361let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2362  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2363
2364(** val joint_internal_function_inv_rect_Type3 :
2365    params -> AST.ident List.list -> joint_internal_function ->
2366    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2367    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2368let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2369  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2370
2371(** val joint_internal_function_inv_rect_Type2 :
2372    params -> AST.ident List.list -> joint_internal_function ->
2373    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2374    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2375let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2376  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2377
2378(** val joint_internal_function_inv_rect_Type1 :
2379    params -> AST.ident List.list -> joint_internal_function ->
2380    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2381    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2382let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2383  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2384
2385(** val joint_internal_function_inv_rect_Type0 :
2386    params -> AST.ident List.list -> joint_internal_function ->
2387    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2388    Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2389let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2390  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2391
2392(** val joint_internal_function_jmdiscr :
2393    params -> AST.ident List.list -> joint_internal_function ->
2394    joint_internal_function -> __ **)
2395let joint_internal_function_jmdiscr a1 a2 x y =
2396  Logic.eq_rect_Type2 x
2397    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2398       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2399       joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2400       a7 } = x
2401     in
2402    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2403
2404(** val good_if_rect_Type4 :
2405    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2406    __ -> __ -> __ -> 'a1) -> 'a1 **)
2407let rec good_if_rect_Type4 p globals def h_mk_good_if =
2408  h_mk_good_if __ __ __ __ __
2409
2410(** val good_if_rect_Type5 :
2411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412    __ -> __ -> __ -> 'a1) -> 'a1 **)
2413let rec good_if_rect_Type5 p globals def h_mk_good_if =
2414  h_mk_good_if __ __ __ __ __
2415
2416(** val good_if_rect_Type3 :
2417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418    __ -> __ -> __ -> 'a1) -> 'a1 **)
2419let rec good_if_rect_Type3 p globals def h_mk_good_if =
2420  h_mk_good_if __ __ __ __ __
2421
2422(** val good_if_rect_Type2 :
2423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424    __ -> __ -> __ -> 'a1) -> 'a1 **)
2425let rec good_if_rect_Type2 p globals def h_mk_good_if =
2426  h_mk_good_if __ __ __ __ __
2427
2428(** val good_if_rect_Type1 :
2429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430    __ -> __ -> __ -> 'a1) -> 'a1 **)
2431let rec good_if_rect_Type1 p globals def h_mk_good_if =
2432  h_mk_good_if __ __ __ __ __
2433
2434(** val good_if_rect_Type0 :
2435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436    __ -> __ -> __ -> 'a1) -> 'a1 **)
2437let rec good_if_rect_Type0 p globals def h_mk_good_if =
2438  h_mk_good_if __ __ __ __ __
2439
2440(** val good_if_inv_rect_Type4 :
2441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2443let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2444  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2445
2446(** val good_if_inv_rect_Type3 :
2447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2450  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2451
2452(** val good_if_inv_rect_Type2 :
2453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2456  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2457
2458(** val good_if_inv_rect_Type1 :
2459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2462  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2463
2464(** val good_if_inv_rect_Type0 :
2465    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2466    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2467let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2468  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2469
2470(** val good_if_discr :
2471    params -> AST.ident List.list -> joint_internal_function -> __ **)
2472let good_if_discr a1 a2 a3 =
2473  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2474
2475(** val good_if_jmdiscr :
2476    params -> AST.ident List.list -> joint_internal_function -> __ **)
2477let good_if_jmdiscr a1 a2 a3 =
2478  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2479
2480type joint_closed_internal_function = joint_internal_function Types.sig0
2481
2482(** val set_joint_code :
2483    AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2484    joint_internal_function **)
2485let set_joint_code globals pars int_fun graph entry =
2486  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2487    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2488    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2489    int_fun.joint_if_stacksize; joint_if_local_stacksize =
2490    int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2491    entry }
2492
2493(** val set_luniverse :
2494    params -> AST.ident List.list -> joint_internal_function ->
2495    Identifiers.universe -> joint_internal_function **)
2496let set_luniverse globals pars p luniverse =
2497  { joint_if_luniverse = luniverse; joint_if_runiverse =
2498    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2499    joint_if_params = p.joint_if_params; joint_if_stacksize =
2500    p.joint_if_stacksize; joint_if_local_stacksize =
2501    p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2502    joint_if_entry = p.joint_if_entry }
2503
2504(** val set_runiverse :
2505    params -> AST.ident List.list -> joint_internal_function ->
2506    Identifiers.universe -> joint_internal_function **)
2507let set_runiverse globals pars p runiverse =
2508  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2509    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2510    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2511    joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2512    p.joint_if_code; joint_if_entry = p.joint_if_entry }
2513
2514(** val add_graph :
2515    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2516    joint_internal_function -> joint_internal_function **)
2517let add_graph g_pars globals l stmt p =
2518  let code =
2519    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2520      stmt
2521  in
2522  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2523  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2524  joint_if_params = p.joint_if_params; joint_if_stacksize =
2525  p.joint_if_stacksize; joint_if_local_stacksize =
2526  p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2527  joint_if_entry = p.joint_if_entry }
2528
2529type joint_function = joint_closed_internal_function AST.fundef
2530
2531type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
2532                                    AST.program;
2533                       init_cost_label : CostLabel.costlabel }
2534
2535(** val joint_program_rect_Type4 :
2536    params -> ((joint_function, AST.init_data List.list) AST.program ->
2537    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2538let rec joint_program_rect_Type4 p h_mk_joint_program x_18149 =
2539  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2540    x_18149
2541  in
2542  h_mk_joint_program joint_prog0 init_cost_label0
2543
2544(** val joint_program_rect_Type5 :
2545    params -> ((joint_function, AST.init_data List.list) AST.program ->
2546    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2547let rec joint_program_rect_Type5 p h_mk_joint_program x_18151 =
2548  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2549    x_18151
2550  in
2551  h_mk_joint_program joint_prog0 init_cost_label0
2552
2553(** val joint_program_rect_Type3 :
2554    params -> ((joint_function, AST.init_data List.list) AST.program ->
2555    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2556let rec joint_program_rect_Type3 p h_mk_joint_program x_18153 =
2557  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2558    x_18153
2559  in
2560  h_mk_joint_program joint_prog0 init_cost_label0
2561
2562(** val joint_program_rect_Type2 :
2563    params -> ((joint_function, AST.init_data List.list) AST.program ->
2564    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2565let rec joint_program_rect_Type2 p h_mk_joint_program x_18155 =
2566  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2567    x_18155
2568  in
2569  h_mk_joint_program joint_prog0 init_cost_label0
2570
2571(** val joint_program_rect_Type1 :
2572    params -> ((joint_function, AST.init_data List.list) AST.program ->
2573    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2574let rec joint_program_rect_Type1 p h_mk_joint_program x_18157 =
2575  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2576    x_18157
2577  in
2578  h_mk_joint_program joint_prog0 init_cost_label0
2579
2580(** val joint_program_rect_Type0 :
2581    params -> ((joint_function, AST.init_data List.list) AST.program ->
2582    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
2583let rec joint_program_rect_Type0 p h_mk_joint_program x_18159 =
2584  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
2585    x_18159
2586  in
2587  h_mk_joint_program joint_prog0 init_cost_label0
2588
2589(** val joint_prog :
2590    params -> joint_program -> (joint_function, AST.init_data List.list)
2591    AST.program **)
2592let rec joint_prog p xxx =
2593  xxx.joint_prog
2594
2595(** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2596let rec init_cost_label p xxx =
2597  xxx.init_cost_label
2598
2599(** val joint_program_inv_rect_Type4 :
2600    params -> joint_program -> ((joint_function, AST.init_data List.list)
2601    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2602let joint_program_inv_rect_Type4 x1 hterm h1 =
2603  let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2604
2605(** val joint_program_inv_rect_Type3 :
2606    params -> joint_program -> ((joint_function, AST.init_data List.list)
2607    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2608let joint_program_inv_rect_Type3 x1 hterm h1 =
2609  let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2610
2611(** val joint_program_inv_rect_Type2 :
2612    params -> joint_program -> ((joint_function, AST.init_data List.list)
2613    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2614let joint_program_inv_rect_Type2 x1 hterm h1 =
2615  let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2616
2617(** val joint_program_inv_rect_Type1 :
2618    params -> joint_program -> ((joint_function, AST.init_data List.list)
2619    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2620let joint_program_inv_rect_Type1 x1 hterm h1 =
2621  let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2622
2623(** val joint_program_inv_rect_Type0 :
2624    params -> joint_program -> ((joint_function, AST.init_data List.list)
2625    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
2626let joint_program_inv_rect_Type0 x1 hterm h1 =
2627  let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2628
2629(** val joint_program_discr :
2630    params -> joint_program -> joint_program -> __ **)
2631let joint_program_discr a1 x y =
2632  Logic.eq_rect_Type2 x
2633    (let { joint_prog = a0; init_cost_label = a10 } = x in
2634    Obj.magic (fun _ dH -> dH __ __)) y
2635
2636(** val joint_program_jmdiscr :
2637    params -> joint_program -> joint_program -> __ **)
2638let joint_program_jmdiscr a1 x y =
2639  Logic.eq_rect_Type2 x
2640    (let { joint_prog = a0; init_cost_label = a10 } = x in
2641    Obj.magic (fun _ dH -> dH __ __)) y
2642
2643(** val dpi1__o__joint_prog__o__inject :
2644    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2645    AST.init_data List.list) AST.program Types.sig0 **)
2646let dpi1__o__joint_prog__o__inject x0 x3 =
2647  x3.Types.dpi1.joint_prog
2648
2649(** val eject__o__joint_prog__o__inject :
2650    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2651    List.list) AST.program Types.sig0 **)
2652let eject__o__joint_prog__o__inject x0 x3 =
2653  (Types.pi1 x3).joint_prog
2654
2655(** val joint_prog__o__inject :
2656    params -> joint_program -> (joint_function, AST.init_data List.list)
2657    AST.program Types.sig0 **)
2658let joint_prog__o__inject x0 x2 =
2659  x2.joint_prog
2660
2661(** val dpi1__o__joint_prog :
2662    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2663    AST.init_data List.list) AST.program **)
2664let dpi1__o__joint_prog x0 x2 =
2665  x2.Types.dpi1.joint_prog
2666
2667(** val eject__o__joint_prog :
2668    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2669    List.list) AST.program **)
2670let eject__o__joint_prog x0 x2 =
2671  (Types.pi1 x2).joint_prog
2672
2673type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2674
2675(** val stack_cost : params -> joint_program -> stack_cost_model **)
2676let stack_cost p pr =
2677  List.foldr (fun id_fun acc ->
2678    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2679    (match fun0 with
2680     | AST.Internal jif ->
2681       List.Cons ({ Types.fst = id; Types.snd =
2682         (Types.pi1 jif).joint_if_stacksize }, acc)
2683     | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
2684
2685open Extra_bool
2686
2687open Coqlib
2688
2689open Values
2690
2691open FrontEndVal
2692
2693open GenMem
2694
2695open FrontEndMem
2696
2697open Globalenvs
2698
2699(** val globals_stacksize : params -> joint_program -> Nat.nat **)
2700let globals_stacksize pars p =
2701  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2702    Globalenvs.size_init_data_list entry.Types.snd)
2703    p.joint_prog.AST.prog_vars
2704
Note: See TracBrowser for help on using the repository browser.