source: extracted/joint.ml @ 2817

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 104.6 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_19544 -> h_Reg x_19544
113| Imm x_19545 -> h_Imm x_19545
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_19549 -> h_Reg x_19549
119| Imm x_19550 -> h_Imm x_19550
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_19554 -> h_Reg x_19554
125| Imm x_19555 -> h_Imm x_19555
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_19559 -> h_Reg x_19559
131| Imm x_19560 -> h_Imm x_19560
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_19564 -> h_Reg x_19564
137| Imm x_19565 -> h_Imm x_19565
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_19569 -> h_Reg x_19569
143| Imm x_19570 -> h_Imm x_19570
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_19605 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_19605
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_19607 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_19607
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_19609 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_19609
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_19611 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_19611
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_19613 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_19613
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_19615 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_19615
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_19632 =
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_19632
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_19634 =
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_19634
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_19636 =
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_19636
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_19638 =
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_19638
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_19640 =
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_19640
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_19642 =
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_19642
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_19672 =
808  let { u_pars = u_pars0; functs = functs0 } = x_19672 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_19674 =
815  let { u_pars = u_pars0; functs = functs0 } = x_19674 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_19676 =
822  let { u_pars = u_pars0; functs = functs0 } = x_19676 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_19678 =
829  let { u_pars = u_pars0; functs = functs0 } = x_19678 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_19680 =
836  let { u_pars = u_pars0; functs = functs0 } = x_19680 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_19682 =
843  let { u_pars = u_pars0; functs = functs0 } = x_19682 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_19737 -> h_COMMENT x_19737
914| MOVE x_19738 -> h_MOVE x_19738
915| POP x_19739 -> h_POP x_19739
916| PUSH x_19740 -> h_PUSH x_19740
917| ADDRESS (i, x_19742, x_19741) -> h_ADDRESS i __ x_19742 x_19741
918| OPACCS (x_19748, x_19747, x_19746, x_19745, x_19744) ->
919  h_OPACCS x_19748 x_19747 x_19746 x_19745 x_19744
920| OP1 (x_19751, x_19750, x_19749) -> h_OP1 x_19751 x_19750 x_19749
921| OP2 (x_19755, x_19754, x_19753, x_19752) ->
922  h_OP2 x_19755 x_19754 x_19753 x_19752
923| CLEAR_CARRY -> h_CLEAR_CARRY
924| SET_CARRY -> h_SET_CARRY
925| LOAD (x_19758, x_19757, x_19756) -> h_LOAD x_19758 x_19757 x_19756
926| STORE (x_19761, x_19760, x_19759) -> h_STORE x_19761 x_19760 x_19759
927| Extension_seq x_19762 -> h_extension_seq x_19762
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_19777 -> h_COMMENT x_19777
938| MOVE x_19778 -> h_MOVE x_19778
939| POP x_19779 -> h_POP x_19779
940| PUSH x_19780 -> h_PUSH x_19780
941| ADDRESS (i, x_19782, x_19781) -> h_ADDRESS i __ x_19782 x_19781
942| OPACCS (x_19788, x_19787, x_19786, x_19785, x_19784) ->
943  h_OPACCS x_19788 x_19787 x_19786 x_19785 x_19784
944| OP1 (x_19791, x_19790, x_19789) -> h_OP1 x_19791 x_19790 x_19789
945| OP2 (x_19795, x_19794, x_19793, x_19792) ->
946  h_OP2 x_19795 x_19794 x_19793 x_19792
947| CLEAR_CARRY -> h_CLEAR_CARRY
948| SET_CARRY -> h_SET_CARRY
949| LOAD (x_19798, x_19797, x_19796) -> h_LOAD x_19798 x_19797 x_19796
950| STORE (x_19801, x_19800, x_19799) -> h_STORE x_19801 x_19800 x_19799
951| Extension_seq x_19802 -> h_extension_seq x_19802
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_19817 -> h_COMMENT x_19817
962| MOVE x_19818 -> h_MOVE x_19818
963| POP x_19819 -> h_POP x_19819
964| PUSH x_19820 -> h_PUSH x_19820
965| ADDRESS (i, x_19822, x_19821) -> h_ADDRESS i __ x_19822 x_19821
966| OPACCS (x_19828, x_19827, x_19826, x_19825, x_19824) ->
967  h_OPACCS x_19828 x_19827 x_19826 x_19825 x_19824
968| OP1 (x_19831, x_19830, x_19829) -> h_OP1 x_19831 x_19830 x_19829
969| OP2 (x_19835, x_19834, x_19833, x_19832) ->
970  h_OP2 x_19835 x_19834 x_19833 x_19832
971| CLEAR_CARRY -> h_CLEAR_CARRY
972| SET_CARRY -> h_SET_CARRY
973| LOAD (x_19838, x_19837, x_19836) -> h_LOAD x_19838 x_19837 x_19836
974| STORE (x_19841, x_19840, x_19839) -> h_STORE x_19841 x_19840 x_19839
975| Extension_seq x_19842 -> h_extension_seq x_19842
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_19857 -> h_COMMENT x_19857
986| MOVE x_19858 -> h_MOVE x_19858
987| POP x_19859 -> h_POP x_19859
988| PUSH x_19860 -> h_PUSH x_19860
989| ADDRESS (i, x_19862, x_19861) -> h_ADDRESS i __ x_19862 x_19861
990| OPACCS (x_19868, x_19867, x_19866, x_19865, x_19864) ->
991  h_OPACCS x_19868 x_19867 x_19866 x_19865 x_19864
992| OP1 (x_19871, x_19870, x_19869) -> h_OP1 x_19871 x_19870 x_19869
993| OP2 (x_19875, x_19874, x_19873, x_19872) ->
994  h_OP2 x_19875 x_19874 x_19873 x_19872
995| CLEAR_CARRY -> h_CLEAR_CARRY
996| SET_CARRY -> h_SET_CARRY
997| LOAD (x_19878, x_19877, x_19876) -> h_LOAD x_19878 x_19877 x_19876
998| STORE (x_19881, x_19880, x_19879) -> h_STORE x_19881 x_19880 x_19879
999| Extension_seq x_19882 -> h_extension_seq x_19882
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_19897 -> h_COMMENT x_19897
1010| MOVE x_19898 -> h_MOVE x_19898
1011| POP x_19899 -> h_POP x_19899
1012| PUSH x_19900 -> h_PUSH x_19900
1013| ADDRESS (i, x_19902, x_19901) -> h_ADDRESS i __ x_19902 x_19901
1014| OPACCS (x_19908, x_19907, x_19906, x_19905, x_19904) ->
1015  h_OPACCS x_19908 x_19907 x_19906 x_19905 x_19904
1016| OP1 (x_19911, x_19910, x_19909) -> h_OP1 x_19911 x_19910 x_19909
1017| OP2 (x_19915, x_19914, x_19913, x_19912) ->
1018  h_OP2 x_19915 x_19914 x_19913 x_19912
1019| CLEAR_CARRY -> h_CLEAR_CARRY
1020| SET_CARRY -> h_SET_CARRY
1021| LOAD (x_19918, x_19917, x_19916) -> h_LOAD x_19918 x_19917 x_19916
1022| STORE (x_19921, x_19920, x_19919) -> h_STORE x_19921 x_19920 x_19919
1023| Extension_seq x_19922 -> h_extension_seq x_19922
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_19937 -> h_COMMENT x_19937
1034| MOVE x_19938 -> h_MOVE x_19938
1035| POP x_19939 -> h_POP x_19939
1036| PUSH x_19940 -> h_PUSH x_19940
1037| ADDRESS (i, x_19942, x_19941) -> h_ADDRESS i __ x_19942 x_19941
1038| OPACCS (x_19948, x_19947, x_19946, x_19945, x_19944) ->
1039  h_OPACCS x_19948 x_19947 x_19946 x_19945 x_19944
1040| OP1 (x_19951, x_19950, x_19949) -> h_OP1 x_19951 x_19950 x_19949
1041| OP2 (x_19955, x_19954, x_19953, x_19952) ->
1042  h_OP2 x_19955 x_19954 x_19953 x_19952
1043| CLEAR_CARRY -> h_CLEAR_CARRY
1044| SET_CARRY -> h_SET_CARRY
1045| LOAD (x_19958, x_19957, x_19956) -> h_LOAD x_19958 x_19957 x_19956
1046| STORE (x_19961, x_19960, x_19959) -> h_STORE x_19961 x_19960 x_19959
1047| Extension_seq x_19962 -> h_extension_seq x_19962
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_20229 -> h_COST_LABEL x_20229
1239| CALL (x_20232, x_20231, x_20230) -> h_CALL x_20232 x_20231 x_20230
1240| COND (x_20234, x_20233) -> h_COND x_20234 x_20233
1241| Step_seq x_20235 -> h_step_seq x_20235
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_20241 -> h_COST_LABEL x_20241
1249| CALL (x_20244, x_20243, x_20242) -> h_CALL x_20244 x_20243 x_20242
1250| COND (x_20246, x_20245) -> h_COND x_20246 x_20245
1251| Step_seq x_20247 -> h_step_seq x_20247
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_20253 -> h_COST_LABEL x_20253
1259| CALL (x_20256, x_20255, x_20254) -> h_CALL x_20256 x_20255 x_20254
1260| COND (x_20258, x_20257) -> h_COND x_20258 x_20257
1261| Step_seq x_20259 -> h_step_seq x_20259
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_20265 -> h_COST_LABEL x_20265
1269| CALL (x_20268, x_20267, x_20266) -> h_CALL x_20268 x_20267 x_20266
1270| COND (x_20270, x_20269) -> h_COND x_20270 x_20269
1271| Step_seq x_20271 -> h_step_seq x_20271
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_20277 -> h_COST_LABEL x_20277
1279| CALL (x_20280, x_20279, x_20278) -> h_CALL x_20280 x_20279 x_20278
1280| COND (x_20282, x_20281) -> h_COND x_20282 x_20281
1281| Step_seq x_20283 -> h_step_seq x_20283
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_20289 -> h_COST_LABEL x_20289
1289| CALL (x_20292, x_20291, x_20290) -> h_CALL x_20292 x_20291 x_20290
1290| COND (x_20294, x_20293) -> h_COND x_20294 x_20293
1291| Step_seq x_20295 -> h_step_seq x_20295
1292
1293(** val joint_step_inv_rect_Type4 :
1294    unserialized_params -> AST.ident List.list -> joint_step ->
1295    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1296    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1297    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1298let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1299  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1300
1301(** val joint_step_inv_rect_Type3 :
1302    unserialized_params -> AST.ident List.list -> joint_step ->
1303    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1304    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1305    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1306let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1307  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1308
1309(** val joint_step_inv_rect_Type2 :
1310    unserialized_params -> AST.ident List.list -> joint_step ->
1311    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1312    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1313    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1314let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1315  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1316
1317(** val joint_step_inv_rect_Type1 :
1318    unserialized_params -> AST.ident List.list -> joint_step ->
1319    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1320    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1321    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1322let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1323  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1324
1325(** val joint_step_inv_rect_Type0 :
1326    unserialized_params -> AST.ident List.list -> joint_step ->
1327    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1328    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1329    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1330let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1331  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1332
1333(** val joint_step_discr :
1334    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1335    __ **)
1336let joint_step_discr a1 a2 x y =
1337  Logic.eq_rect_Type2 x
1338    (match x with
1339     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1340     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1341     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1342     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1343
1344(** val joint_step_jmdiscr :
1345    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1346    __ **)
1347let joint_step_jmdiscr a1 a2 x y =
1348  Logic.eq_rect_Type2 x
1349    (match x with
1350     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1351     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1352     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1353     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1354
1355(** val get_used_registers_from_step :
1356    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1357    joint_step -> Registers.register List.list **)
1358let get_used_registers_from_step p globals functs0 = function
1359| COST_LABEL c -> List.Nil
1360| CALL (id, args, dest) ->
1361  List.append (functs0.f_call_args args) (functs0.f_call_dest dest)
1362| COND (r, lbl) -> functs0.acc_a_regs r
1363| Step_seq s -> get_used_registers_from_seq p globals functs0 s
1364
1365(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1366    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1367    joint_step Types.sig0 **)
1368let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1369  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1370
1371(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1372    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1373    Types.sig0 **)
1374let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1375  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1376
1377(** val extension_seq_to_seq__o__seq_to_step__o__inject :
1378    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1379let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1380  Step_seq (Extension_seq x2)
1381
1382(** val dpi1__o__seq_to_step__o__inject :
1383    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1384    Types.dPair -> joint_step Types.sig0 **)
1385let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1386  Step_seq x4.Types.dpi1
1387
1388(** val eject__o__seq_to_step__o__inject :
1389    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1390    joint_step Types.sig0 **)
1391let eject__o__seq_to_step__o__inject x0 x1 x4 =
1392  Step_seq (Types.pi1 x4)
1393
1394(** val seq_to_step__o__inject :
1395    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1396    Types.sig0 **)
1397let seq_to_step__o__inject x0 x1 x3 =
1398  Step_seq x3
1399
1400(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1401    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1402    joint_step **)
1403let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1404  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1405
1406(** val eject__o__extension_seq_to_seq__o__seq_to_step :
1407    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1408let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1409  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1410
1411(** val extension_seq_to_seq__o__seq_to_step :
1412    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1413let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1414  Step_seq (Extension_seq x2)
1415
1416(** val dpi1__o__seq_to_step :
1417    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1418    Types.dPair -> joint_step **)
1419let dpi1__o__seq_to_step x0 x1 x3 =
1420  Step_seq x3.Types.dpi1
1421
1422(** val eject__o__seq_to_step :
1423    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1424    joint_step **)
1425let eject__o__seq_to_step x0 x1 x3 =
1426  Step_seq (Types.pi1 x3)
1427
1428(** val step_labels :
1429    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1430    List.list **)
1431let step_labels p globals = function
1432| COST_LABEL x -> List.Nil
1433| CALL (x, x0, x1) -> List.Nil
1434| COND (x, l) -> List.Cons (l, List.Nil)
1435| Step_seq s0 ->
1436  (match s0 with
1437   | COMMENT x -> List.Nil
1438   | MOVE x -> List.Nil
1439   | POP x -> List.Nil
1440   | PUSH x -> List.Nil
1441   | ADDRESS (x, x1, x2) -> List.Nil
1442   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1443   | OP1 (x, x0, x1) -> List.Nil
1444   | OP2 (x, x0, x1, x2) -> List.Nil
1445   | CLEAR_CARRY -> List.Nil
1446   | SET_CARRY -> List.Nil
1447   | LOAD (x, x0, x1) -> List.Nil
1448   | STORE (x, x0, x1) -> List.Nil
1449   | Extension_seq ext -> p.ext_seq_labels ext)
1450
1451type stmt_params = { uns_pars : uns_params;
1452                     succ_label : (__ -> Graphs.label Types.option);
1453                     has_fcond : Bool.bool }
1454
1455(** val stmt_params_rect_Type4 :
1456    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1457    'a1) -> stmt_params -> 'a1 **)
1458let rec stmt_params_rect_Type4 h_mk_stmt_params x_20374 =
1459  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1460    has_fcond0 } = x_20374
1461  in
1462  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1463
1464(** val stmt_params_rect_Type5 :
1465    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1466    'a1) -> stmt_params -> 'a1 **)
1467let rec stmt_params_rect_Type5 h_mk_stmt_params x_20376 =
1468  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1469    has_fcond0 } = x_20376
1470  in
1471  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1472
1473(** val stmt_params_rect_Type3 :
1474    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1475    'a1) -> stmt_params -> 'a1 **)
1476let rec stmt_params_rect_Type3 h_mk_stmt_params x_20378 =
1477  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1478    has_fcond0 } = x_20378
1479  in
1480  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1481
1482(** val stmt_params_rect_Type2 :
1483    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1484    'a1) -> stmt_params -> 'a1 **)
1485let rec stmt_params_rect_Type2 h_mk_stmt_params x_20380 =
1486  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1487    has_fcond0 } = x_20380
1488  in
1489  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1490
1491(** val stmt_params_rect_Type1 :
1492    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1493    'a1) -> stmt_params -> 'a1 **)
1494let rec stmt_params_rect_Type1 h_mk_stmt_params x_20382 =
1495  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1496    has_fcond0 } = x_20382
1497  in
1498  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1499
1500(** val stmt_params_rect_Type0 :
1501    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1502    'a1) -> stmt_params -> 'a1 **)
1503let rec stmt_params_rect_Type0 h_mk_stmt_params x_20384 =
1504  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1505    has_fcond0 } = x_20384
1506  in
1507  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1508
1509(** val uns_pars : stmt_params -> uns_params **)
1510let rec uns_pars xxx =
1511  xxx.uns_pars
1512
1513type succ = __
1514
1515(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1516let rec succ_label xxx =
1517  xxx.succ_label
1518
1519(** val has_fcond : stmt_params -> Bool.bool **)
1520let rec has_fcond xxx =
1521  xxx.has_fcond
1522
1523(** val stmt_params_inv_rect_Type4 :
1524    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1525    Bool.bool -> __ -> 'a1) -> 'a1 **)
1526let stmt_params_inv_rect_Type4 hterm h1 =
1527  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1528
1529(** val stmt_params_inv_rect_Type3 :
1530    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1531    Bool.bool -> __ -> 'a1) -> 'a1 **)
1532let stmt_params_inv_rect_Type3 hterm h1 =
1533  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1534
1535(** val stmt_params_inv_rect_Type2 :
1536    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1537    Bool.bool -> __ -> 'a1) -> 'a1 **)
1538let stmt_params_inv_rect_Type2 hterm h1 =
1539  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1540
1541(** val stmt_params_inv_rect_Type1 :
1542    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1543    Bool.bool -> __ -> 'a1) -> 'a1 **)
1544let stmt_params_inv_rect_Type1 hterm h1 =
1545  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1546
1547(** val stmt_params_inv_rect_Type0 :
1548    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1549    Bool.bool -> __ -> 'a1) -> 'a1 **)
1550let stmt_params_inv_rect_Type0 hterm h1 =
1551  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1552
1553(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1554let stmt_params_jmdiscr x y =
1555  Logic.eq_rect_Type2 x
1556    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1557    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1558
1559(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1560let uns_pars__o__u_pars x0 =
1561  x0.uns_pars.u_pars
1562
1563type joint_fin_step =
1564| GOTO of Graphs.label
1565| RETURN
1566| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1567
1568(** val joint_fin_step_rect_Type4 :
1569    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1570    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1571let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1572| GOTO x_20408 -> h_GOTO x_20408
1573| RETURN -> h_RETURN
1574| TAILCALL (x_20410, x_20409) -> h_TAILCALL __ x_20410 x_20409
1575
1576(** val joint_fin_step_rect_Type5 :
1577    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1579let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1580| GOTO x_20416 -> h_GOTO x_20416
1581| RETURN -> h_RETURN
1582| TAILCALL (x_20418, x_20417) -> h_TAILCALL __ x_20418 x_20417
1583
1584(** val joint_fin_step_rect_Type3 :
1585    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1587let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1588| GOTO x_20424 -> h_GOTO x_20424
1589| RETURN -> h_RETURN
1590| TAILCALL (x_20426, x_20425) -> h_TAILCALL __ x_20426 x_20425
1591
1592(** val joint_fin_step_rect_Type2 :
1593    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1595let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1596| GOTO x_20432 -> h_GOTO x_20432
1597| RETURN -> h_RETURN
1598| TAILCALL (x_20434, x_20433) -> h_TAILCALL __ x_20434 x_20433
1599
1600(** val joint_fin_step_rect_Type1 :
1601    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1603let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1604| GOTO x_20440 -> h_GOTO x_20440
1605| RETURN -> h_RETURN
1606| TAILCALL (x_20442, x_20441) -> h_TAILCALL __ x_20442 x_20441
1607
1608(** val joint_fin_step_rect_Type0 :
1609    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1611let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1612| GOTO x_20448 -> h_GOTO x_20448
1613| RETURN -> h_RETURN
1614| TAILCALL (x_20450, x_20449) -> h_TAILCALL __ x_20450 x_20449
1615
1616(** val joint_fin_step_inv_rect_Type4 :
1617    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1618    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1619    __ -> 'a1) -> 'a1 **)
1620let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1621  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1622
1623(** val joint_fin_step_inv_rect_Type3 :
1624    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1625    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1626    __ -> 'a1) -> 'a1 **)
1627let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1628  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1629
1630(** val joint_fin_step_inv_rect_Type2 :
1631    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1632    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1633    __ -> 'a1) -> 'a1 **)
1634let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1635  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1636
1637(** val joint_fin_step_inv_rect_Type1 :
1638    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1639    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1640    __ -> 'a1) -> 'a1 **)
1641let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1642  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1643
1644(** val joint_fin_step_inv_rect_Type0 :
1645    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1646    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1647    __ -> 'a1) -> 'a1 **)
1648let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1649  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1650
1651(** val joint_fin_step_discr :
1652    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1653let joint_fin_step_discr a1 x y =
1654  Logic.eq_rect_Type2 x
1655    (match x with
1656     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1657     | RETURN -> Obj.magic (fun _ dH -> dH)
1658     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1659
1660(** val joint_fin_step_jmdiscr :
1661    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1662let joint_fin_step_jmdiscr a1 x y =
1663  Logic.eq_rect_Type2 x
1664    (match x with
1665     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1666     | RETURN -> Obj.magic (fun _ dH -> dH)
1667     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1668
1669(** val fin_step_labels :
1670    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1671let fin_step_labels p = function
1672| GOTO l -> List.Cons (l, List.Nil)
1673| RETURN -> List.Nil
1674| TAILCALL (x0, x1) -> List.Nil
1675
1676type joint_statement =
1677| Sequential of joint_step * __
1678| Final of joint_fin_step
1679| FCOND of __ * Graphs.label * Graphs.label
1680
1681(** val joint_statement_rect_Type4 :
1682    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1683    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1684    'a1) -> joint_statement -> 'a1 **)
1685let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1686| Sequential (x_20516, x_20515) -> h_sequential x_20516 x_20515
1687| Final x_20517 -> h_final x_20517
1688| FCOND (x_20520, x_20519, x_20518) -> h_FCOND __ x_20520 x_20519 x_20518
1689
1690(** val joint_statement_rect_Type5 :
1691    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1692    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1693    'a1) -> joint_statement -> 'a1 **)
1694let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1695| Sequential (x_20527, x_20526) -> h_sequential x_20527 x_20526
1696| Final x_20528 -> h_final x_20528
1697| FCOND (x_20531, x_20530, x_20529) -> h_FCOND __ x_20531 x_20530 x_20529
1698
1699(** val joint_statement_rect_Type3 :
1700    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1701    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1702    'a1) -> joint_statement -> 'a1 **)
1703let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1704| Sequential (x_20538, x_20537) -> h_sequential x_20538 x_20537
1705| Final x_20539 -> h_final x_20539
1706| FCOND (x_20542, x_20541, x_20540) -> h_FCOND __ x_20542 x_20541 x_20540
1707
1708(** val joint_statement_rect_Type2 :
1709    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1710    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1711    'a1) -> joint_statement -> 'a1 **)
1712let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1713| Sequential (x_20549, x_20548) -> h_sequential x_20549 x_20548
1714| Final x_20550 -> h_final x_20550
1715| FCOND (x_20553, x_20552, x_20551) -> h_FCOND __ x_20553 x_20552 x_20551
1716
1717(** val joint_statement_rect_Type1 :
1718    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1719    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1720    'a1) -> joint_statement -> 'a1 **)
1721let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1722| Sequential (x_20560, x_20559) -> h_sequential x_20560 x_20559
1723| Final x_20561 -> h_final x_20561
1724| FCOND (x_20564, x_20563, x_20562) -> h_FCOND __ x_20564 x_20563 x_20562
1725
1726(** val joint_statement_rect_Type0 :
1727    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1728    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1729    'a1) -> joint_statement -> 'a1 **)
1730let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1731| Sequential (x_20571, x_20570) -> h_sequential x_20571 x_20570
1732| Final x_20572 -> h_final x_20572
1733| FCOND (x_20575, x_20574, x_20573) -> h_FCOND __ x_20575 x_20574 x_20573
1734
1735(** val joint_statement_inv_rect_Type4 :
1736    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1737    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1738    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1739let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1740  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1741
1742(** val joint_statement_inv_rect_Type3 :
1743    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1744    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1745    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1746let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1747  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1748
1749(** val joint_statement_inv_rect_Type2 :
1750    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1751    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1752    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1753let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1754  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1755
1756(** val joint_statement_inv_rect_Type1 :
1757    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1758    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1759    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1760let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1761  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1762
1763(** val joint_statement_inv_rect_Type0 :
1764    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1765    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1766    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1767let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1768  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1769
1770(** val joint_statement_discr :
1771    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1772    -> __ **)
1773let joint_statement_discr a1 a2 x y =
1774  Logic.eq_rect_Type2 x
1775    (match x with
1776     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1777     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1778     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1779
1780(** val joint_statement_jmdiscr :
1781    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1782    -> __ **)
1783let joint_statement_jmdiscr a1 a2 x y =
1784  Logic.eq_rect_Type2 x
1785    (match x with
1786     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1787     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1788     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1789
1790(** val dpi1__o__fin_step_to_stmt__o__inject :
1791    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1792    -> joint_statement Types.sig0 **)
1793let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1794  Final x4.Types.dpi1
1795
1796(** val eject__o__fin_step_to_stmt__o__inject :
1797    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1798    joint_statement Types.sig0 **)
1799let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1800  Final (Types.pi1 x4)
1801
1802(** val fin_step_to_stmt__o__inject :
1803    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1804    Types.sig0 **)
1805let fin_step_to_stmt__o__inject x0 x1 x3 =
1806  Final x3
1807
1808(** val dpi1__o__fin_step_to_stmt :
1809    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1810    -> joint_statement **)
1811let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1812  Final x3.Types.dpi1
1813
1814(** val eject__o__fin_step_to_stmt :
1815    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1816    joint_statement **)
1817let eject__o__fin_step_to_stmt x0 x1 x3 =
1818  Final (Types.pi1 x3)
1819
1820type params = { stmt_pars : stmt_params;
1821                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1822                          Types.option);
1823                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1824                                 -> __ Types.option);
1825                point_of_succ : (__ -> __ -> __) }
1826
1827(** val params_rect_Type4 :
1828    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1829    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1830    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1831    'a1 **)
1832let rec params_rect_Type4 h_mk_params x_20648 =
1833  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1834    point_of_label0; point_of_succ = point_of_succ0 } = x_20648
1835  in
1836  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1837
1838(** val params_rect_Type5 :
1839    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1840    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1841    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1842    'a1 **)
1843let rec params_rect_Type5 h_mk_params x_20650 =
1844  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1845    point_of_label0; point_of_succ = point_of_succ0 } = x_20650
1846  in
1847  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1848
1849(** val params_rect_Type3 :
1850    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1851    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1852    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1853    'a1 **)
1854let rec params_rect_Type3 h_mk_params x_20652 =
1855  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1856    point_of_label0; point_of_succ = point_of_succ0 } = x_20652
1857  in
1858  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1859
1860(** val params_rect_Type2 :
1861    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1862    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1863    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1864    'a1 **)
1865let rec params_rect_Type2 h_mk_params x_20654 =
1866  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1867    point_of_label0; point_of_succ = point_of_succ0 } = x_20654
1868  in
1869  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1870
1871(** val params_rect_Type1 :
1872    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1873    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1874    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1875    'a1 **)
1876let rec params_rect_Type1 h_mk_params x_20656 =
1877  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1878    point_of_label0; point_of_succ = point_of_succ0 } = x_20656
1879  in
1880  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1881
1882(** val params_rect_Type0 :
1883    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1884    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1885    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1886    'a1 **)
1887let rec params_rect_Type0 h_mk_params x_20658 =
1888  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1889    point_of_label0; point_of_succ = point_of_succ0 } = x_20658
1890  in
1891  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1892
1893(** val stmt_pars : params -> stmt_params **)
1894let rec stmt_pars xxx =
1895  xxx.stmt_pars
1896
1897type codeT = __
1898
1899type code_point = __
1900
1901(** val stmt_at :
1902    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1903let rec stmt_at xxx =
1904  xxx.stmt_at
1905
1906(** val point_of_label :
1907    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1908let rec point_of_label xxx =
1909  xxx.point_of_label
1910
1911(** val point_of_succ : params -> __ -> __ -> __ **)
1912let rec point_of_succ xxx =
1913  xxx.point_of_succ
1914
1915(** val params_inv_rect_Type4 :
1916    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1917    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1918    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1919let params_inv_rect_Type4 hterm h1 =
1920  let hcut = params_rect_Type4 h1 hterm in hcut __
1921
1922(** val params_inv_rect_Type3 :
1923    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1924    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1925    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1926let params_inv_rect_Type3 hterm h1 =
1927  let hcut = params_rect_Type3 h1 hterm in hcut __
1928
1929(** val params_inv_rect_Type2 :
1930    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1931    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1932    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1933let params_inv_rect_Type2 hterm h1 =
1934  let hcut = params_rect_Type2 h1 hterm in hcut __
1935
1936(** val params_inv_rect_Type1 :
1937    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1938    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1939    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1940let params_inv_rect_Type1 hterm h1 =
1941  let hcut = params_rect_Type1 h1 hterm in hcut __
1942
1943(** val params_inv_rect_Type0 :
1944    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1945    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1946    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1947let params_inv_rect_Type0 hterm h1 =
1948  let hcut = params_rect_Type0 h1 hterm in hcut __
1949
1950(** val params_jmdiscr : params -> params -> __ **)
1951let params_jmdiscr x y =
1952  Logic.eq_rect_Type2 x
1953    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1954       a5 } = x
1955     in
1956    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1957
1958(** val stmt_pars__o__uns_pars : params -> uns_params **)
1959let stmt_pars__o__uns_pars x0 =
1960  x0.stmt_pars.uns_pars
1961
1962(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1963let stmt_pars__o__uns_pars__o__u_pars x0 =
1964  uns_pars__o__u_pars x0.stmt_pars
1965
1966(** val code_has_point :
1967    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1968let code_has_point p globals c pt =
1969  match p.stmt_at globals c pt with
1970  | Types.None -> Bool.False
1971  | Types.Some x -> Bool.True
1972
1973(** val code_has_label :
1974    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1975let code_has_label p globals c l =
1976  match p.point_of_label globals c l with
1977  | Types.None -> Bool.False
1978  | Types.Some pt -> code_has_point p globals c pt
1979
1980(** val stmt_explicit_labels :
1981    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1982    List.list **)
1983let stmt_explicit_labels p globals = function
1984| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1985| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
1986| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1987
1988(** val stmt_implicit_label :
1989    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1990    Types.option **)
1991let stmt_implicit_label p globals = function
1992| Sequential (x, s0) -> p.succ_label s0
1993| Final x -> Types.None
1994| FCOND (x0, x1, x2) -> Types.None
1995
1996(** val stmt_labels :
1997    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1998    List.list **)
1999let stmt_labels p g stmt =
2000  List.append
2001    (match stmt_implicit_label p g stmt with
2002     | Types.None -> List.Nil
2003     | Types.Some l -> List.Cons (l, List.Nil))
2004    (stmt_explicit_labels p g stmt)
2005
2006(** val stmt_registers :
2007    stmt_params -> AST.ident List.list -> joint_statement ->
2008    Registers.register List.list **)
2009let stmt_registers p globals = function
2010| Sequential (c, x) ->
2011  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2012| Final c ->
2013  (match c with
2014   | GOTO x -> List.Nil
2015   | RETURN -> List.Nil
2016   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2017| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2018
2019type lin_params =
2020  uns_params
2021  (* singleton inductive, whose constructor was mk_lin_params *)
2022
2023(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2024let rec lin_params_rect_Type4 h_mk_lin_params x_20681 =
2025  let l_u_pars = x_20681 in h_mk_lin_params l_u_pars
2026
2027(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2028let rec lin_params_rect_Type5 h_mk_lin_params x_20683 =
2029  let l_u_pars = x_20683 in h_mk_lin_params l_u_pars
2030
2031(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2032let rec lin_params_rect_Type3 h_mk_lin_params x_20685 =
2033  let l_u_pars = x_20685 in h_mk_lin_params l_u_pars
2034
2035(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2036let rec lin_params_rect_Type2 h_mk_lin_params x_20687 =
2037  let l_u_pars = x_20687 in h_mk_lin_params l_u_pars
2038
2039(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2040let rec lin_params_rect_Type1 h_mk_lin_params x_20689 =
2041  let l_u_pars = x_20689 in h_mk_lin_params l_u_pars
2042
2043(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2044let rec lin_params_rect_Type0 h_mk_lin_params x_20691 =
2045  let l_u_pars = x_20691 in h_mk_lin_params l_u_pars
2046
2047(** val l_u_pars : lin_params -> uns_params **)
2048let rec l_u_pars xxx =
2049  let yyy = xxx in yyy
2050
2051(** val lin_params_inv_rect_Type4 :
2052    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2053let lin_params_inv_rect_Type4 hterm h1 =
2054  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2055
2056(** val lin_params_inv_rect_Type3 :
2057    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2058let lin_params_inv_rect_Type3 hterm h1 =
2059  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2060
2061(** val lin_params_inv_rect_Type2 :
2062    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2063let lin_params_inv_rect_Type2 hterm h1 =
2064  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2065
2066(** val lin_params_inv_rect_Type1 :
2067    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2068let lin_params_inv_rect_Type1 hterm h1 =
2069  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2070
2071(** val lin_params_inv_rect_Type0 :
2072    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2073let lin_params_inv_rect_Type0 hterm h1 =
2074  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2075
2076(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2077let lin_params_jmdiscr x y =
2078  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2079
2080(** val lin_params_to_params : lin_params -> params **)
2081let lin_params_to_params lp =
2082  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2083    Types.None); has_fcond = Bool.True }; stmt_at =
2084    (fun globals code point ->
2085    Obj.magic
2086      (Monad.m_bind0 (Monad.max_def Option.option)
2087        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2088        (fun ls ->
2089        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2090    point_of_label = (fun globals c lbl ->
2091    Util.if_then_else_safe
2092      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2093        (Obj.magic c)) (fun _ ->
2094      Obj.magic
2095        (Monad.m_return0 (Monad.max_def Option.option)
2096          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2097            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2098    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2099
2100(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2101let lp_to_p__o__stmt_pars x0 =
2102  (lin_params_to_params x0).stmt_pars
2103
2104(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2105let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2106  stmt_pars__o__uns_pars (lin_params_to_params x0)
2107
2108(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2109    lin_params -> unserialized_params **)
2110let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2111  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2112
2113type graph_params =
2114  uns_params
2115  (* singleton inductive, whose constructor was mk_graph_params *)
2116
2117(** val graph_params_rect_Type4 :
2118    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2119let rec graph_params_rect_Type4 h_mk_graph_params x_20707 =
2120  let g_u_pars = x_20707 in h_mk_graph_params g_u_pars
2121
2122(** val graph_params_rect_Type5 :
2123    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2124let rec graph_params_rect_Type5 h_mk_graph_params x_20709 =
2125  let g_u_pars = x_20709 in h_mk_graph_params g_u_pars
2126
2127(** val graph_params_rect_Type3 :
2128    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2129let rec graph_params_rect_Type3 h_mk_graph_params x_20711 =
2130  let g_u_pars = x_20711 in h_mk_graph_params g_u_pars
2131
2132(** val graph_params_rect_Type2 :
2133    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2134let rec graph_params_rect_Type2 h_mk_graph_params x_20713 =
2135  let g_u_pars = x_20713 in h_mk_graph_params g_u_pars
2136
2137(** val graph_params_rect_Type1 :
2138    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2139let rec graph_params_rect_Type1 h_mk_graph_params x_20715 =
2140  let g_u_pars = x_20715 in h_mk_graph_params g_u_pars
2141
2142(** val graph_params_rect_Type0 :
2143    (uns_params -> 'a1) -> graph_params -> 'a1 **)
2144let rec graph_params_rect_Type0 h_mk_graph_params x_20717 =
2145  let g_u_pars = x_20717 in h_mk_graph_params g_u_pars
2146
2147(** val g_u_pars : graph_params -> uns_params **)
2148let rec g_u_pars xxx =
2149  let yyy = xxx in yyy
2150
2151(** val graph_params_inv_rect_Type4 :
2152    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2153let graph_params_inv_rect_Type4 hterm h1 =
2154  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2155
2156(** val graph_params_inv_rect_Type3 :
2157    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2158let graph_params_inv_rect_Type3 hterm h1 =
2159  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2160
2161(** val graph_params_inv_rect_Type2 :
2162    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2163let graph_params_inv_rect_Type2 hterm h1 =
2164  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2165
2166(** val graph_params_inv_rect_Type1 :
2167    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2168let graph_params_inv_rect_Type1 hterm h1 =
2169  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2170
2171(** val graph_params_inv_rect_Type0 :
2172    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2173let graph_params_inv_rect_Type0 hterm h1 =
2174  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2175
2176(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2177let graph_params_jmdiscr x y =
2178  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2179
2180(** val graph_params_to_params : graph_params -> params **)
2181let graph_params_to_params gp =
2182  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2183    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2184    (fun globals code ->
2185    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2186    point_of_label = (fun x x0 lbl ->
2187    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2188    point_of_succ = (fun x lbl -> lbl) }
2189
2190(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2191let gp_to_p__o__stmt_pars x0 =
2192  (graph_params_to_params x0).stmt_pars
2193
2194(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2195let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2196  stmt_pars__o__uns_pars (graph_params_to_params x0)
2197
2198(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2199    graph_params -> unserialized_params **)
2200let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2201  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2202
2203type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2204                                 joint_if_runiverse : Identifiers.universe;
2205                                 joint_if_result : __; joint_if_params : 
2206                                 __; joint_if_stacksize : Nat.nat;
2207                                 joint_if_code : __;
2208                                 joint_if_entry : __ Types.sig0 }
2209
2210(** val joint_internal_function_rect_Type4 :
2211    params -> AST.ident List.list -> (Identifiers.universe ->
2212    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2213    'a1) -> joint_internal_function -> 'a1 **)
2214let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20733 =
2215  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2216    joint_if_runiverse0; joint_if_result = joint_if_result0;
2217    joint_if_params = joint_if_params0; joint_if_stacksize =
2218    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2219    joint_if_entry0 } = x_20733
2220  in
2221  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2222    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2223    joint_if_entry0
2224
2225(** val joint_internal_function_rect_Type5 :
2226    params -> AST.ident List.list -> (Identifiers.universe ->
2227    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2228    'a1) -> joint_internal_function -> 'a1 **)
2229let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20735 =
2230  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2231    joint_if_runiverse0; joint_if_result = joint_if_result0;
2232    joint_if_params = joint_if_params0; joint_if_stacksize =
2233    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2234    joint_if_entry0 } = x_20735
2235  in
2236  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2237    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2238    joint_if_entry0
2239
2240(** val joint_internal_function_rect_Type3 :
2241    params -> AST.ident List.list -> (Identifiers.universe ->
2242    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2243    'a1) -> joint_internal_function -> 'a1 **)
2244let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20737 =
2245  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2246    joint_if_runiverse0; joint_if_result = joint_if_result0;
2247    joint_if_params = joint_if_params0; joint_if_stacksize =
2248    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2249    joint_if_entry0 } = x_20737
2250  in
2251  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2252    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2253    joint_if_entry0
2254
2255(** val joint_internal_function_rect_Type2 :
2256    params -> AST.ident List.list -> (Identifiers.universe ->
2257    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2258    'a1) -> joint_internal_function -> 'a1 **)
2259let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20739 =
2260  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2261    joint_if_runiverse0; joint_if_result = joint_if_result0;
2262    joint_if_params = joint_if_params0; joint_if_stacksize =
2263    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2264    joint_if_entry0 } = x_20739
2265  in
2266  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2267    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2268    joint_if_entry0
2269
2270(** val joint_internal_function_rect_Type1 :
2271    params -> AST.ident List.list -> (Identifiers.universe ->
2272    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2273    'a1) -> joint_internal_function -> 'a1 **)
2274let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20741 =
2275  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2276    joint_if_runiverse0; joint_if_result = joint_if_result0;
2277    joint_if_params = joint_if_params0; joint_if_stacksize =
2278    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2279    joint_if_entry0 } = x_20741
2280  in
2281  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2282    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2283    joint_if_entry0
2284
2285(** val joint_internal_function_rect_Type0 :
2286    params -> AST.ident List.list -> (Identifiers.universe ->
2287    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
2288    'a1) -> joint_internal_function -> 'a1 **)
2289let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20743 =
2290  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2291    joint_if_runiverse0; joint_if_result = joint_if_result0;
2292    joint_if_params = joint_if_params0; joint_if_stacksize =
2293    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
2294    joint_if_entry0 } = x_20743
2295  in
2296  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2297    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
2298    joint_if_entry0
2299
2300(** val joint_if_luniverse :
2301    params -> AST.ident List.list -> joint_internal_function ->
2302    Identifiers.universe **)
2303let rec joint_if_luniverse p globals xxx =
2304  xxx.joint_if_luniverse
2305
2306(** val joint_if_runiverse :
2307    params -> AST.ident List.list -> joint_internal_function ->
2308    Identifiers.universe **)
2309let rec joint_if_runiverse p globals xxx =
2310  xxx.joint_if_runiverse
2311
2312(** val joint_if_result :
2313    params -> AST.ident List.list -> joint_internal_function -> __ **)
2314let rec joint_if_result p globals xxx =
2315  xxx.joint_if_result
2316
2317(** val joint_if_params :
2318    params -> AST.ident List.list -> joint_internal_function -> __ **)
2319let rec joint_if_params p globals xxx =
2320  xxx.joint_if_params
2321
2322(** val joint_if_stacksize :
2323    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2324let rec joint_if_stacksize p globals xxx =
2325  xxx.joint_if_stacksize
2326
2327(** val joint_if_code :
2328    params -> AST.ident List.list -> joint_internal_function -> __ **)
2329let rec joint_if_code p globals xxx =
2330  xxx.joint_if_code
2331
2332(** val joint_if_entry :
2333    params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0 **)
2334let rec joint_if_entry p globals xxx =
2335  xxx.joint_if_entry
2336
2337(** val joint_internal_function_inv_rect_Type4 :
2338    params -> AST.ident List.list -> joint_internal_function ->
2339    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2340    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
2341let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2342  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2343
2344(** val joint_internal_function_inv_rect_Type3 :
2345    params -> AST.ident List.list -> joint_internal_function ->
2346    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2347    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
2348let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2349  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2350
2351(** val joint_internal_function_inv_rect_Type2 :
2352    params -> AST.ident List.list -> joint_internal_function ->
2353    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2354    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
2355let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2356  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2357
2358(** val joint_internal_function_inv_rect_Type1 :
2359    params -> AST.ident List.list -> joint_internal_function ->
2360    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2361    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
2362let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2363  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2364
2365(** val joint_internal_function_inv_rect_Type0 :
2366    params -> AST.ident List.list -> joint_internal_function ->
2367    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2368    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
2369let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2370  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2371
2372(** val joint_internal_function_jmdiscr :
2373    params -> AST.ident List.list -> joint_internal_function ->
2374    joint_internal_function -> __ **)
2375let joint_internal_function_jmdiscr a1 a2 x y =
2376  Logic.eq_rect_Type2 x
2377    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2378       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2379       joint_if_code = a5; joint_if_entry = a6 } = x
2380     in
2381    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
2382
2383(** val good_if_rect_Type4 :
2384    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2385    __ -> __ -> __ -> 'a1) -> 'a1 **)
2386let rec good_if_rect_Type4 p globals def h_mk_good_if =
2387  h_mk_good_if __ __ __ __ __
2388
2389(** val good_if_rect_Type5 :
2390    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2391    __ -> __ -> __ -> 'a1) -> 'a1 **)
2392let rec good_if_rect_Type5 p globals def h_mk_good_if =
2393  h_mk_good_if __ __ __ __ __
2394
2395(** val good_if_rect_Type3 :
2396    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2397    __ -> __ -> __ -> 'a1) -> 'a1 **)
2398let rec good_if_rect_Type3 p globals def h_mk_good_if =
2399  h_mk_good_if __ __ __ __ __
2400
2401(** val good_if_rect_Type2 :
2402    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2403    __ -> __ -> __ -> 'a1) -> 'a1 **)
2404let rec good_if_rect_Type2 p globals def h_mk_good_if =
2405  h_mk_good_if __ __ __ __ __
2406
2407(** val good_if_rect_Type1 :
2408    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2409    __ -> __ -> __ -> 'a1) -> 'a1 **)
2410let rec good_if_rect_Type1 p globals def h_mk_good_if =
2411  h_mk_good_if __ __ __ __ __
2412
2413(** val good_if_rect_Type0 :
2414    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2415    __ -> __ -> __ -> 'a1) -> 'a1 **)
2416let rec good_if_rect_Type0 p globals def h_mk_good_if =
2417  h_mk_good_if __ __ __ __ __
2418
2419(** val good_if_inv_rect_Type4 :
2420    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2421    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2422let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2423  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2424
2425(** val good_if_inv_rect_Type3 :
2426    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2427    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2428let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2429  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2430
2431(** val good_if_inv_rect_Type2 :
2432    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2433    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2434let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2435  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2436
2437(** val good_if_inv_rect_Type1 :
2438    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2439    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2440let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2441  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2442
2443(** val good_if_inv_rect_Type0 :
2444    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2445    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2446let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2447  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2448
2449(** val good_if_discr :
2450    params -> AST.ident List.list -> joint_internal_function -> __ **)
2451let good_if_discr a1 a2 a3 =
2452  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2453
2454(** val good_if_jmdiscr :
2455    params -> AST.ident List.list -> joint_internal_function -> __ **)
2456let good_if_jmdiscr a1 a2 a3 =
2457  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2458
2459type joint_closed_internal_function = joint_internal_function Types.sig0
2460
2461(** val set_joint_code :
2462    AST.ident List.list -> params -> joint_internal_function -> __ -> __
2463    Types.sig0 -> joint_internal_function **)
2464let set_joint_code globals pars int_fun graph entry =
2465  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2466    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2467    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2468    int_fun.joint_if_stacksize; joint_if_code = graph; joint_if_entry =
2469    entry }
2470
2471(** val set_joint_if_graph :
2472    AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
2473    joint_internal_function **)
2474let set_joint_if_graph globals pars graph p =
2475  set_joint_code globals (graph_params_to_params pars) p graph
2476    (Types.pi1 p.joint_if_entry)
2477
2478(** val set_luniverse :
2479    params -> AST.ident List.list -> joint_internal_function ->
2480    Identifiers.universe -> joint_internal_function **)
2481let set_luniverse globals pars p luniverse =
2482  { joint_if_luniverse = luniverse; joint_if_runiverse =
2483    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2484    joint_if_params = p.joint_if_params; joint_if_stacksize =
2485    p.joint_if_stacksize; joint_if_code = p.joint_if_code; joint_if_entry =
2486    p.joint_if_entry }
2487
2488(** val set_runiverse :
2489    params -> AST.ident List.list -> joint_internal_function ->
2490    Identifiers.universe -> joint_internal_function **)
2491let set_runiverse globals pars p runiverse =
2492  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2493    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2494    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2495    joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry }
2496
2497(** val add_graph :
2498    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2499    joint_internal_function -> joint_internal_function **)
2500let add_graph g_pars globals l stmt p =
2501  let code =
2502    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2503      stmt
2504  in
2505  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2506  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2507  joint_if_params = p.joint_if_params; joint_if_stacksize =
2508  p.joint_if_stacksize; joint_if_code = (Obj.magic code); joint_if_entry =
2509  (Types.pi1 p.joint_if_entry) }
2510
2511type joint_function = joint_closed_internal_function AST.fundef
2512
2513type joint_program = (joint_function, Nat.nat) AST.program
2514
2515type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2516
2517(** val stack_cost : params -> joint_program -> stack_cost_model **)
2518let stack_cost p pr =
2519  List.foldr (fun id_fun acc ->
2520    let { Types.fst = id; Types.snd = fun0 } = id_fun in
2521    (match fun0 with
2522     | AST.Internal jif ->
2523       List.Cons ({ Types.fst = id; Types.snd =
2524         (Types.pi1 jif).joint_if_stacksize }, acc)
2525     | AST.External x -> acc)) List.Nil pr.AST.prog_funct
2526
Note: See TracBrowser for help on using the repository browser.