source: extracted/joint.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 81.8 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 Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
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 BitVectorTrie
86
87open CostLabel
88
89open Order
90
91open Registers
92
93open I8051
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_19390 -> h_Reg x_19390
113| Imm x_19391 -> h_Imm x_19391
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_19395 -> h_Reg x_19395
119| Imm x_19396 -> h_Imm x_19396
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_19400 -> h_Reg x_19400
125| Imm x_19401 -> h_Imm x_19401
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_19405 -> h_Reg x_19405
131| Imm x_19406 -> h_Imm x_19406
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_19410 -> h_Reg x_19410
137| Imm x_19411 -> h_Imm x_19411
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_19415 -> h_Reg x_19415
143| Imm x_19416 -> h_Imm x_19416
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_19451 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_19451
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_19453 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_19453
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_19455 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_19455
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_19457 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_19457
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_19459 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_19459
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_19461 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_19461
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 joint_seq =
469| COMMENT of String.string
470| MOVE of __
471| POP of __
472| PUSH of __
473| ADDRESS of AST.ident * __ * __
474| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
475| OP1 of BackEndOps.op1 * __ * __
476| OP2 of BackEndOps.op2 * __ * __ * __
477| CLEAR_CARRY
478| SET_CARRY
479| LOAD of __ * __ * __
480| STORE of __ * __ * __
481| Extension_seq of __
482
483(** val joint_seq_rect_Type4 :
484    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
485    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
486    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
487    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
488    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
489    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
490let 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
491| COMMENT x_19517 -> h_COMMENT x_19517
492| MOVE x_19518 -> h_MOVE x_19518
493| POP x_19519 -> h_POP x_19519
494| PUSH x_19520 -> h_PUSH x_19520
495| ADDRESS (i, x_19522, x_19521) -> h_ADDRESS i __ x_19522 x_19521
496| OPACCS (x_19528, x_19527, x_19526, x_19525, x_19524) ->
497  h_OPACCS x_19528 x_19527 x_19526 x_19525 x_19524
498| OP1 (x_19531, x_19530, x_19529) -> h_OP1 x_19531 x_19530 x_19529
499| OP2 (x_19535, x_19534, x_19533, x_19532) ->
500  h_OP2 x_19535 x_19534 x_19533 x_19532
501| CLEAR_CARRY -> h_CLEAR_CARRY
502| SET_CARRY -> h_SET_CARRY
503| LOAD (x_19538, x_19537, x_19536) -> h_LOAD x_19538 x_19537 x_19536
504| STORE (x_19541, x_19540, x_19539) -> h_STORE x_19541 x_19540 x_19539
505| Extension_seq x_19542 -> h_extension_seq x_19542
506
507(** val joint_seq_rect_Type5 :
508    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
509    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
510    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
511    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
512    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
513    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
514let 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
515| COMMENT x_19557 -> h_COMMENT x_19557
516| MOVE x_19558 -> h_MOVE x_19558
517| POP x_19559 -> h_POP x_19559
518| PUSH x_19560 -> h_PUSH x_19560
519| ADDRESS (i, x_19562, x_19561) -> h_ADDRESS i __ x_19562 x_19561
520| OPACCS (x_19568, x_19567, x_19566, x_19565, x_19564) ->
521  h_OPACCS x_19568 x_19567 x_19566 x_19565 x_19564
522| OP1 (x_19571, x_19570, x_19569) -> h_OP1 x_19571 x_19570 x_19569
523| OP2 (x_19575, x_19574, x_19573, x_19572) ->
524  h_OP2 x_19575 x_19574 x_19573 x_19572
525| CLEAR_CARRY -> h_CLEAR_CARRY
526| SET_CARRY -> h_SET_CARRY
527| LOAD (x_19578, x_19577, x_19576) -> h_LOAD x_19578 x_19577 x_19576
528| STORE (x_19581, x_19580, x_19579) -> h_STORE x_19581 x_19580 x_19579
529| Extension_seq x_19582 -> h_extension_seq x_19582
530
531(** val joint_seq_rect_Type3 :
532    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
533    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
534    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
535    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
536    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
537    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
538let 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
539| COMMENT x_19597 -> h_COMMENT x_19597
540| MOVE x_19598 -> h_MOVE x_19598
541| POP x_19599 -> h_POP x_19599
542| PUSH x_19600 -> h_PUSH x_19600
543| ADDRESS (i, x_19602, x_19601) -> h_ADDRESS i __ x_19602 x_19601
544| OPACCS (x_19608, x_19607, x_19606, x_19605, x_19604) ->
545  h_OPACCS x_19608 x_19607 x_19606 x_19605 x_19604
546| OP1 (x_19611, x_19610, x_19609) -> h_OP1 x_19611 x_19610 x_19609
547| OP2 (x_19615, x_19614, x_19613, x_19612) ->
548  h_OP2 x_19615 x_19614 x_19613 x_19612
549| CLEAR_CARRY -> h_CLEAR_CARRY
550| SET_CARRY -> h_SET_CARRY
551| LOAD (x_19618, x_19617, x_19616) -> h_LOAD x_19618 x_19617 x_19616
552| STORE (x_19621, x_19620, x_19619) -> h_STORE x_19621 x_19620 x_19619
553| Extension_seq x_19622 -> h_extension_seq x_19622
554
555(** val joint_seq_rect_Type2 :
556    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
557    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
558    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
559    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
560    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
561    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
562let 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
563| COMMENT x_19637 -> h_COMMENT x_19637
564| MOVE x_19638 -> h_MOVE x_19638
565| POP x_19639 -> h_POP x_19639
566| PUSH x_19640 -> h_PUSH x_19640
567| ADDRESS (i, x_19642, x_19641) -> h_ADDRESS i __ x_19642 x_19641
568| OPACCS (x_19648, x_19647, x_19646, x_19645, x_19644) ->
569  h_OPACCS x_19648 x_19647 x_19646 x_19645 x_19644
570| OP1 (x_19651, x_19650, x_19649) -> h_OP1 x_19651 x_19650 x_19649
571| OP2 (x_19655, x_19654, x_19653, x_19652) ->
572  h_OP2 x_19655 x_19654 x_19653 x_19652
573| CLEAR_CARRY -> h_CLEAR_CARRY
574| SET_CARRY -> h_SET_CARRY
575| LOAD (x_19658, x_19657, x_19656) -> h_LOAD x_19658 x_19657 x_19656
576| STORE (x_19661, x_19660, x_19659) -> h_STORE x_19661 x_19660 x_19659
577| Extension_seq x_19662 -> h_extension_seq x_19662
578
579(** val joint_seq_rect_Type1 :
580    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
581    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
582    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
583    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
584    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
585    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
586let 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
587| COMMENT x_19677 -> h_COMMENT x_19677
588| MOVE x_19678 -> h_MOVE x_19678
589| POP x_19679 -> h_POP x_19679
590| PUSH x_19680 -> h_PUSH x_19680
591| ADDRESS (i, x_19682, x_19681) -> h_ADDRESS i __ x_19682 x_19681
592| OPACCS (x_19688, x_19687, x_19686, x_19685, x_19684) ->
593  h_OPACCS x_19688 x_19687 x_19686 x_19685 x_19684
594| OP1 (x_19691, x_19690, x_19689) -> h_OP1 x_19691 x_19690 x_19689
595| OP2 (x_19695, x_19694, x_19693, x_19692) ->
596  h_OP2 x_19695 x_19694 x_19693 x_19692
597| CLEAR_CARRY -> h_CLEAR_CARRY
598| SET_CARRY -> h_SET_CARRY
599| LOAD (x_19698, x_19697, x_19696) -> h_LOAD x_19698 x_19697 x_19696
600| STORE (x_19701, x_19700, x_19699) -> h_STORE x_19701 x_19700 x_19699
601| Extension_seq x_19702 -> h_extension_seq x_19702
602
603(** val joint_seq_rect_Type0 :
604    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
605    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
606    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
607    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
608    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
609    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
610let 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
611| COMMENT x_19717 -> h_COMMENT x_19717
612| MOVE x_19718 -> h_MOVE x_19718
613| POP x_19719 -> h_POP x_19719
614| PUSH x_19720 -> h_PUSH x_19720
615| ADDRESS (i, x_19722, x_19721) -> h_ADDRESS i __ x_19722 x_19721
616| OPACCS (x_19728, x_19727, x_19726, x_19725, x_19724) ->
617  h_OPACCS x_19728 x_19727 x_19726 x_19725 x_19724
618| OP1 (x_19731, x_19730, x_19729) -> h_OP1 x_19731 x_19730 x_19729
619| OP2 (x_19735, x_19734, x_19733, x_19732) ->
620  h_OP2 x_19735 x_19734 x_19733 x_19732
621| CLEAR_CARRY -> h_CLEAR_CARRY
622| SET_CARRY -> h_SET_CARRY
623| LOAD (x_19738, x_19737, x_19736) -> h_LOAD x_19738 x_19737 x_19736
624| STORE (x_19741, x_19740, x_19739) -> h_STORE x_19741 x_19740 x_19739
625| Extension_seq x_19742 -> h_extension_seq x_19742
626
627(** val joint_seq_inv_rect_Type4 :
628    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
629    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
630    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
631    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
632    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
633    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
634    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
635let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
636  let hcut =
637    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
638      hterm
639  in
640  hcut __
641
642(** val joint_seq_inv_rect_Type3 :
643    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
644    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
645    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
646    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
647    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
648    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
649    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
650let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
651  let hcut =
652    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
653      hterm
654  in
655  hcut __
656
657(** val joint_seq_inv_rect_Type2 :
658    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
659    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
660    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
661    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
662    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
663    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
664    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
665let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
666  let hcut =
667    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
668      hterm
669  in
670  hcut __
671
672(** val joint_seq_inv_rect_Type1 :
673    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
674    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
675    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
676    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
677    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
678    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
679    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
680let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
681  let hcut =
682    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
683      hterm
684  in
685  hcut __
686
687(** val joint_seq_inv_rect_Type0 :
688    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
689    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
690    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
691    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
692    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
693    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
694    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
695let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
696  let hcut =
697    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
698      hterm
699  in
700  hcut __
701
702(** val joint_seq_discr :
703    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
704    __ **)
705let joint_seq_discr a1 a2 x y =
706  Logic.eq_rect_Type2 x
707    (match x with
708     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
709     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
710     | POP a0 -> Obj.magic (fun _ dH -> dH __)
711     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
712     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
713     | OPACCS (a0, a10, a20, a3, a4) ->
714       Obj.magic (fun _ dH -> dH __ __ __ __ __)
715     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
716     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
717     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
718     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
719     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
720     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
721     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
722
723(** val joint_seq_jmdiscr :
724    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
725    __ **)
726let joint_seq_jmdiscr a1 a2 x y =
727  Logic.eq_rect_Type2 x
728    (match x with
729     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
730     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
731     | POP a0 -> Obj.magic (fun _ dH -> dH __)
732     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
733     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
734     | OPACCS (a0, a10, a20, a3, a4) ->
735       Obj.magic (fun _ dH -> dH __ __ __ __ __)
736     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
737     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
738     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
739     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
740     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
741     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
742     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
743
744(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
745let nOOP p globals =
746  COMMENT String.EmptyString
747
748(** val dpi1__o__extension_seq_to_seq__o__inject :
749    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
750    joint_seq Types.sig0 **)
751let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
752  Extension_seq x4.Types.dpi1
753
754(** val eject__o__extension_seq_to_seq__o__inject :
755    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
756    Types.sig0 **)
757let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
758  Extension_seq (Types.pi1 x4)
759
760(** val extension_seq_to_seq__o__inject :
761    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
762let extension_seq_to_seq__o__inject x0 x1 x3 =
763  Extension_seq x3
764
765(** val dpi1__o__extension_seq_to_seq :
766    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
767    joint_seq **)
768let dpi1__o__extension_seq_to_seq x0 x1 x3 =
769  Extension_seq x3.Types.dpi1
770
771(** val eject__o__extension_seq_to_seq :
772    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
773let eject__o__extension_seq_to_seq x0 x1 x3 =
774  Extension_seq (Types.pi1 x3)
775
776type joint_step =
777| COST_LABEL of CostLabel.costlabel
778| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
779| COND of __ * Graphs.label
780| Step_seq of joint_seq
781
782(** val joint_step_rect_Type4 :
783    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
784    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
785    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
786let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
787| COST_LABEL x_20009 -> h_COST_LABEL x_20009
788| CALL (x_20012, x_20011, x_20010) -> h_CALL x_20012 x_20011 x_20010
789| COND (x_20014, x_20013) -> h_COND x_20014 x_20013
790| Step_seq x_20015 -> h_step_seq x_20015
791
792(** val joint_step_rect_Type5 :
793    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
794    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
795    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
796let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
797| COST_LABEL x_20021 -> h_COST_LABEL x_20021
798| CALL (x_20024, x_20023, x_20022) -> h_CALL x_20024 x_20023 x_20022
799| COND (x_20026, x_20025) -> h_COND x_20026 x_20025
800| Step_seq x_20027 -> h_step_seq x_20027
801
802(** val joint_step_rect_Type3 :
803    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
804    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
805    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
806let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
807| COST_LABEL x_20033 -> h_COST_LABEL x_20033
808| CALL (x_20036, x_20035, x_20034) -> h_CALL x_20036 x_20035 x_20034
809| COND (x_20038, x_20037) -> h_COND x_20038 x_20037
810| Step_seq x_20039 -> h_step_seq x_20039
811
812(** val joint_step_rect_Type2 :
813    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
814    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
815    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
816let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
817| COST_LABEL x_20045 -> h_COST_LABEL x_20045
818| CALL (x_20048, x_20047, x_20046) -> h_CALL x_20048 x_20047 x_20046
819| COND (x_20050, x_20049) -> h_COND x_20050 x_20049
820| Step_seq x_20051 -> h_step_seq x_20051
821
822(** val joint_step_rect_Type1 :
823    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
824    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
825    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
826let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
827| COST_LABEL x_20057 -> h_COST_LABEL x_20057
828| CALL (x_20060, x_20059, x_20058) -> h_CALL x_20060 x_20059 x_20058
829| COND (x_20062, x_20061) -> h_COND x_20062 x_20061
830| Step_seq x_20063 -> h_step_seq x_20063
831
832(** val joint_step_rect_Type0 :
833    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
834    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
835    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
836let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
837| COST_LABEL x_20069 -> h_COST_LABEL x_20069
838| CALL (x_20072, x_20071, x_20070) -> h_CALL x_20072 x_20071 x_20070
839| COND (x_20074, x_20073) -> h_COND x_20074 x_20073
840| Step_seq x_20075 -> h_step_seq x_20075
841
842(** val joint_step_inv_rect_Type4 :
843    unserialized_params -> AST.ident List.list -> joint_step ->
844    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
845    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
846    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
847let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
848  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
849
850(** val joint_step_inv_rect_Type3 :
851    unserialized_params -> AST.ident List.list -> joint_step ->
852    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
853    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
854    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
855let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
856  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
857
858(** val joint_step_inv_rect_Type2 :
859    unserialized_params -> AST.ident List.list -> joint_step ->
860    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
861    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
862    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
863let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
864  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
865
866(** val joint_step_inv_rect_Type1 :
867    unserialized_params -> AST.ident List.list -> joint_step ->
868    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
869    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
870    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
871let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
872  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
873
874(** val joint_step_inv_rect_Type0 :
875    unserialized_params -> AST.ident List.list -> joint_step ->
876    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
877    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
878    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
879let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
880  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
881
882(** val joint_step_discr :
883    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
884    __ **)
885let joint_step_discr a1 a2 x y =
886  Logic.eq_rect_Type2 x
887    (match x with
888     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
889     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
890     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
891     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
892
893(** val joint_step_jmdiscr :
894    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
895    __ **)
896let joint_step_jmdiscr a1 a2 x y =
897  Logic.eq_rect_Type2 x
898    (match x with
899     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
900     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
901     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
902     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
903
904(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
905    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
906    joint_step Types.sig0 **)
907let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
908  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
909
910(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
911    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
912    Types.sig0 **)
913let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
914  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
915
916(** val extension_seq_to_seq__o__seq_to_step__o__inject :
917    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
918let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
919  Step_seq (Extension_seq x2)
920
921(** val dpi1__o__seq_to_step__o__inject :
922    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
923    Types.dPair -> joint_step Types.sig0 **)
924let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
925  Step_seq x4.Types.dpi1
926
927(** val eject__o__seq_to_step__o__inject :
928    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
929    joint_step Types.sig0 **)
930let eject__o__seq_to_step__o__inject x0 x1 x4 =
931  Step_seq (Types.pi1 x4)
932
933(** val seq_to_step__o__inject :
934    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
935    Types.sig0 **)
936let seq_to_step__o__inject x0 x1 x3 =
937  Step_seq x3
938
939(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
940    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
941    joint_step **)
942let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
943  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
944
945(** val eject__o__extension_seq_to_seq__o__seq_to_step :
946    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
947let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
948  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
949
950(** val extension_seq_to_seq__o__seq_to_step :
951    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
952let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
953  Step_seq (Extension_seq x2)
954
955(** val dpi1__o__seq_to_step :
956    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
957    Types.dPair -> joint_step **)
958let dpi1__o__seq_to_step x0 x1 x3 =
959  Step_seq x3.Types.dpi1
960
961(** val eject__o__seq_to_step :
962    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
963    joint_step **)
964let eject__o__seq_to_step x0 x1 x3 =
965  Step_seq (Types.pi1 x3)
966
967(** val step_labels :
968    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
969    List.list **)
970let step_labels p globals = function
971| COST_LABEL x -> List.Nil
972| CALL (x, x0, x1) -> List.Nil
973| COND (x, l) -> List.Cons (l, List.Nil)
974| Step_seq s0 ->
975  (match s0 with
976   | COMMENT x -> List.Nil
977   | MOVE x -> List.Nil
978   | POP x -> List.Nil
979   | PUSH x -> List.Nil
980   | ADDRESS (x, x1, x2) -> List.Nil
981   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
982   | OP1 (x, x0, x1) -> List.Nil
983   | OP2 (x, x0, x1, x2) -> List.Nil
984   | CLEAR_CARRY -> List.Nil
985   | SET_CARRY -> List.Nil
986   | LOAD (x, x0, x1) -> List.Nil
987   | STORE (x, x0, x1) -> List.Nil
988   | Extension_seq ext -> p.ext_seq_labels ext)
989
990type stmt_params = { uns_pars : unserialized_params;
991                     succ_label : (__ -> Graphs.label Types.option);
992                     has_fcond : Bool.bool }
993
994(** val stmt_params_rect_Type4 :
995    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
996    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
997let rec stmt_params_rect_Type4 h_mk_stmt_params x_20154 =
998  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
999    has_fcond0 } = x_20154
1000  in
1001  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1002
1003(** val stmt_params_rect_Type5 :
1004    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
1005    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
1006let rec stmt_params_rect_Type5 h_mk_stmt_params x_20156 =
1007  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1008    has_fcond0 } = x_20156
1009  in
1010  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1011
1012(** val stmt_params_rect_Type3 :
1013    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
1014    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
1015let rec stmt_params_rect_Type3 h_mk_stmt_params x_20158 =
1016  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1017    has_fcond0 } = x_20158
1018  in
1019  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1020
1021(** val stmt_params_rect_Type2 :
1022    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
1023    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
1024let rec stmt_params_rect_Type2 h_mk_stmt_params x_20160 =
1025  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1026    has_fcond0 } = x_20160
1027  in
1028  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1029
1030(** val stmt_params_rect_Type1 :
1031    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
1032    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
1033let rec stmt_params_rect_Type1 h_mk_stmt_params x_20162 =
1034  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1035    has_fcond0 } = x_20162
1036  in
1037  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1038
1039(** val stmt_params_rect_Type0 :
1040    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
1041    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
1042let rec stmt_params_rect_Type0 h_mk_stmt_params x_20164 =
1043  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1044    has_fcond0 } = x_20164
1045  in
1046  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1047
1048(** val uns_pars : stmt_params -> unserialized_params **)
1049let rec uns_pars xxx =
1050  xxx.uns_pars
1051
1052type succ0 = __
1053
1054(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1055let rec succ_label xxx =
1056  xxx.succ_label
1057
1058(** val has_fcond : stmt_params -> Bool.bool **)
1059let rec has_fcond xxx =
1060  xxx.has_fcond
1061
1062(** val stmt_params_inv_rect_Type4 :
1063    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
1064    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
1065let stmt_params_inv_rect_Type4 hterm h1 =
1066  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1067
1068(** val stmt_params_inv_rect_Type3 :
1069    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
1070    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
1071let stmt_params_inv_rect_Type3 hterm h1 =
1072  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1073
1074(** val stmt_params_inv_rect_Type2 :
1075    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
1076    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
1077let stmt_params_inv_rect_Type2 hterm h1 =
1078  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1079
1080(** val stmt_params_inv_rect_Type1 :
1081    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
1082    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
1083let stmt_params_inv_rect_Type1 hterm h1 =
1084  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1085
1086(** val stmt_params_inv_rect_Type0 :
1087    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
1088    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
1089let stmt_params_inv_rect_Type0 hterm h1 =
1090  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1091
1092(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1093let stmt_params_jmdiscr x y =
1094  Logic.eq_rect_Type2 x
1095    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1096    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1097
1098type joint_fin_step =
1099| GOTO of Graphs.label
1100| RETURN
1101| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1102
1103(** val joint_fin_step_rect_Type4 :
1104    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1105    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1106let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1107| GOTO x_20188 -> h_GOTO x_20188
1108| RETURN -> h_RETURN
1109| TAILCALL (x_20190, x_20189) -> h_TAILCALL __ x_20190 x_20189
1110
1111(** val joint_fin_step_rect_Type5 :
1112    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1113    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1114let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1115| GOTO x_20196 -> h_GOTO x_20196
1116| RETURN -> h_RETURN
1117| TAILCALL (x_20198, x_20197) -> h_TAILCALL __ x_20198 x_20197
1118
1119(** val joint_fin_step_rect_Type3 :
1120    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1121    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1122let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1123| GOTO x_20204 -> h_GOTO x_20204
1124| RETURN -> h_RETURN
1125| TAILCALL (x_20206, x_20205) -> h_TAILCALL __ x_20206 x_20205
1126
1127(** val joint_fin_step_rect_Type2 :
1128    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1129    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1130let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1131| GOTO x_20212 -> h_GOTO x_20212
1132| RETURN -> h_RETURN
1133| TAILCALL (x_20214, x_20213) -> h_TAILCALL __ x_20214 x_20213
1134
1135(** val joint_fin_step_rect_Type1 :
1136    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1137    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1138let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1139| GOTO x_20220 -> h_GOTO x_20220
1140| RETURN -> h_RETURN
1141| TAILCALL (x_20222, x_20221) -> h_TAILCALL __ x_20222 x_20221
1142
1143(** val joint_fin_step_rect_Type0 :
1144    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1145    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1146let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1147| GOTO x_20228 -> h_GOTO x_20228
1148| RETURN -> h_RETURN
1149| TAILCALL (x_20230, x_20229) -> h_TAILCALL __ x_20230 x_20229
1150
1151(** val joint_fin_step_inv_rect_Type4 :
1152    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1153    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1154    __ -> 'a1) -> 'a1 **)
1155let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1156  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1157
1158(** val joint_fin_step_inv_rect_Type3 :
1159    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1160    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1161    __ -> 'a1) -> 'a1 **)
1162let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1163  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1164
1165(** val joint_fin_step_inv_rect_Type2 :
1166    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1167    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1168    __ -> 'a1) -> 'a1 **)
1169let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1170  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1171
1172(** val joint_fin_step_inv_rect_Type1 :
1173    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1174    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1175    __ -> 'a1) -> 'a1 **)
1176let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1177  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1178
1179(** val joint_fin_step_inv_rect_Type0 :
1180    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1181    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1182    __ -> 'a1) -> 'a1 **)
1183let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1184  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1185
1186(** val joint_fin_step_discr :
1187    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1188let joint_fin_step_discr a1 x y =
1189  Logic.eq_rect_Type2 x
1190    (match x with
1191     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1192     | RETURN -> Obj.magic (fun _ dH -> dH)
1193     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1194
1195(** val joint_fin_step_jmdiscr :
1196    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1197let joint_fin_step_jmdiscr a1 x y =
1198  Logic.eq_rect_Type2 x
1199    (match x with
1200     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1201     | RETURN -> Obj.magic (fun _ dH -> dH)
1202     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1203
1204(** val fin_step_labels :
1205    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1206let fin_step_labels p = function
1207| GOTO l -> List.Cons (l, List.Nil)
1208| RETURN -> List.Nil
1209| TAILCALL (x0, x1) -> List.Nil
1210
1211type joint_statement =
1212| Sequential of joint_step * __
1213| Final of joint_fin_step
1214| FCOND of __ * Graphs.label * Graphs.label
1215
1216(** val joint_statement_rect_Type4 :
1217    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1218    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1219    'a1) -> joint_statement -> 'a1 **)
1220let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1221| Sequential (x_20296, x_20295) -> h_sequential x_20296 x_20295
1222| Final x_20297 -> h_final x_20297
1223| FCOND (x_20300, x_20299, x_20298) -> h_FCOND __ x_20300 x_20299 x_20298
1224
1225(** val joint_statement_rect_Type5 :
1226    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1227    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1228    'a1) -> joint_statement -> 'a1 **)
1229let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1230| Sequential (x_20307, x_20306) -> h_sequential x_20307 x_20306
1231| Final x_20308 -> h_final x_20308
1232| FCOND (x_20311, x_20310, x_20309) -> h_FCOND __ x_20311 x_20310 x_20309
1233
1234(** val joint_statement_rect_Type3 :
1235    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1236    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1237    'a1) -> joint_statement -> 'a1 **)
1238let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1239| Sequential (x_20318, x_20317) -> h_sequential x_20318 x_20317
1240| Final x_20319 -> h_final x_20319
1241| FCOND (x_20322, x_20321, x_20320) -> h_FCOND __ x_20322 x_20321 x_20320
1242
1243(** val joint_statement_rect_Type2 :
1244    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1245    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1246    'a1) -> joint_statement -> 'a1 **)
1247let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1248| Sequential (x_20329, x_20328) -> h_sequential x_20329 x_20328
1249| Final x_20330 -> h_final x_20330
1250| FCOND (x_20333, x_20332, x_20331) -> h_FCOND __ x_20333 x_20332 x_20331
1251
1252(** val joint_statement_rect_Type1 :
1253    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1254    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1255    'a1) -> joint_statement -> 'a1 **)
1256let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1257| Sequential (x_20340, x_20339) -> h_sequential x_20340 x_20339
1258| Final x_20341 -> h_final x_20341
1259| FCOND (x_20344, x_20343, x_20342) -> h_FCOND __ x_20344 x_20343 x_20342
1260
1261(** val joint_statement_rect_Type0 :
1262    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1263    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1264    'a1) -> joint_statement -> 'a1 **)
1265let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1266| Sequential (x_20351, x_20350) -> h_sequential x_20351 x_20350
1267| Final x_20352 -> h_final x_20352
1268| FCOND (x_20355, x_20354, x_20353) -> h_FCOND __ x_20355 x_20354 x_20353
1269
1270(** val joint_statement_inv_rect_Type4 :
1271    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1272    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1273    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1274let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1275  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1276
1277(** val joint_statement_inv_rect_Type3 :
1278    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1279    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1280    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1281let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1282  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1283
1284(** val joint_statement_inv_rect_Type2 :
1285    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1286    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1287    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1288let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1289  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1290
1291(** val joint_statement_inv_rect_Type1 :
1292    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1293    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1294    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1295let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1296  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1297
1298(** val joint_statement_inv_rect_Type0 :
1299    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1300    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1301    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1302let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1303  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1304
1305(** val joint_statement_discr :
1306    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1307    -> __ **)
1308let joint_statement_discr a1 a2 x y =
1309  Logic.eq_rect_Type2 x
1310    (match x with
1311     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1312     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1313     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1314
1315(** val joint_statement_jmdiscr :
1316    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1317    -> __ **)
1318let joint_statement_jmdiscr a1 a2 x y =
1319  Logic.eq_rect_Type2 x
1320    (match x with
1321     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1322     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1323     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1324
1325(** val dpi1__o__fin_step_to_stmt__o__inject :
1326    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1327    -> joint_statement Types.sig0 **)
1328let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1329  Final x4.Types.dpi1
1330
1331(** val eject__o__fin_step_to_stmt__o__inject :
1332    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1333    joint_statement Types.sig0 **)
1334let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1335  Final (Types.pi1 x4)
1336
1337(** val fin_step_to_stmt__o__inject :
1338    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1339    Types.sig0 **)
1340let fin_step_to_stmt__o__inject x0 x1 x3 =
1341  Final x3
1342
1343(** val dpi1__o__fin_step_to_stmt :
1344    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1345    -> joint_statement **)
1346let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1347  Final x3.Types.dpi1
1348
1349(** val eject__o__fin_step_to_stmt :
1350    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1351    joint_statement **)
1352let eject__o__fin_step_to_stmt x0 x1 x3 =
1353  Final (Types.pi1 x3)
1354
1355type params = { stmt_pars : stmt_params;
1356                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1357                          Types.option);
1358                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1359                                 -> __ Types.option);
1360                point_of_succ : (__ -> __ -> __) }
1361
1362(** val params_rect_Type4 :
1363    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1364    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1365    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1366    'a1 **)
1367let rec params_rect_Type4 h_mk_params x_20428 =
1368  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1369    point_of_label0; point_of_succ = point_of_succ0 } = x_20428
1370  in
1371  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1372
1373(** val params_rect_Type5 :
1374    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1375    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1376    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1377    'a1 **)
1378let rec params_rect_Type5 h_mk_params x_20430 =
1379  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1380    point_of_label0; point_of_succ = point_of_succ0 } = x_20430
1381  in
1382  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1383
1384(** val params_rect_Type3 :
1385    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1386    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1387    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1388    'a1 **)
1389let rec params_rect_Type3 h_mk_params x_20432 =
1390  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1391    point_of_label0; point_of_succ = point_of_succ0 } = x_20432
1392  in
1393  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1394
1395(** val params_rect_Type2 :
1396    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1397    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1398    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1399    'a1 **)
1400let rec params_rect_Type2 h_mk_params x_20434 =
1401  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1402    point_of_label0; point_of_succ = point_of_succ0 } = x_20434
1403  in
1404  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1405
1406(** val params_rect_Type1 :
1407    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1408    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1409    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1410    'a1 **)
1411let rec params_rect_Type1 h_mk_params x_20436 =
1412  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1413    point_of_label0; point_of_succ = point_of_succ0 } = x_20436
1414  in
1415  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1416
1417(** val params_rect_Type0 :
1418    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1419    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1420    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1421    'a1 **)
1422let rec params_rect_Type0 h_mk_params x_20438 =
1423  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1424    point_of_label0; point_of_succ = point_of_succ0 } = x_20438
1425  in
1426  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1427
1428(** val stmt_pars : params -> stmt_params **)
1429let rec stmt_pars xxx =
1430  xxx.stmt_pars
1431
1432type codeT = __
1433
1434type code_point = __
1435
1436(** val stmt_at :
1437    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1438let rec stmt_at xxx =
1439  xxx.stmt_at
1440
1441(** val point_of_label :
1442    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1443let rec point_of_label xxx =
1444  xxx.point_of_label
1445
1446(** val point_of_succ : params -> __ -> __ -> __ **)
1447let rec point_of_succ xxx =
1448  xxx.point_of_succ
1449
1450(** val params_inv_rect_Type4 :
1451    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1452    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1453    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1454let params_inv_rect_Type4 hterm h1 =
1455  let hcut = params_rect_Type4 h1 hterm in hcut __
1456
1457(** val params_inv_rect_Type3 :
1458    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1459    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1460    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1461let params_inv_rect_Type3 hterm h1 =
1462  let hcut = params_rect_Type3 h1 hterm in hcut __
1463
1464(** val params_inv_rect_Type2 :
1465    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1466    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1467    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1468let params_inv_rect_Type2 hterm h1 =
1469  let hcut = params_rect_Type2 h1 hterm in hcut __
1470
1471(** val params_inv_rect_Type1 :
1472    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1473    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1474    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1475let params_inv_rect_Type1 hterm h1 =
1476  let hcut = params_rect_Type1 h1 hterm in hcut __
1477
1478(** val params_inv_rect_Type0 :
1479    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1480    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1481    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1482let params_inv_rect_Type0 hterm h1 =
1483  let hcut = params_rect_Type0 h1 hterm in hcut __
1484
1485(** val params_jmdiscr : params -> params -> __ **)
1486let params_jmdiscr x y =
1487  Logic.eq_rect_Type2 x
1488    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1489       a5 } = x
1490     in
1491    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1492
1493(** val stmt_pars__o__uns_pars : params -> unserialized_params **)
1494let stmt_pars__o__uns_pars x0 =
1495  x0.stmt_pars.uns_pars
1496
1497(** val code_has_point :
1498    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1499let code_has_point p globals c pt =
1500  match p.stmt_at globals c pt with
1501  | Types.None -> Bool.False
1502  | Types.Some x -> Bool.True
1503
1504(** val code_has_label :
1505    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1506let code_has_label p globals c l =
1507  match p.point_of_label globals c l with
1508  | Types.None -> Bool.False
1509  | Types.Some pt -> code_has_point p globals c pt
1510
1511(** val stmt_explicit_labels :
1512    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1513    List.list **)
1514let stmt_explicit_labels p globals = function
1515| Sequential (c, x) -> step_labels p.uns_pars globals c
1516| Final c -> fin_step_labels p.uns_pars c
1517| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1518
1519(** val stmt_implicit_label :
1520    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1521    Types.option **)
1522let stmt_implicit_label p globals = function
1523| Sequential (x, s0) -> p.succ_label s0
1524| Final x -> Types.None
1525| FCOND (x0, x1, x2) -> Types.None
1526
1527(** val stmt_labels :
1528    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1529    List.list **)
1530let stmt_labels p g0 stmt =
1531  List.append
1532    (match stmt_implicit_label p g0 stmt with
1533     | Types.None -> List.Nil
1534     | Types.Some l -> List.Cons (l, List.Nil))
1535    (stmt_explicit_labels p g0 stmt)
1536
1537type lin_params =
1538  unserialized_params
1539  (* singleton inductive, whose constructor was mk_lin_params *)
1540
1541(** val lin_params_rect_Type4 :
1542    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1543let rec lin_params_rect_Type4 h_mk_lin_params x_20461 =
1544  let l_u_pars = x_20461 in h_mk_lin_params l_u_pars
1545
1546(** val lin_params_rect_Type5 :
1547    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1548let rec lin_params_rect_Type5 h_mk_lin_params x_20463 =
1549  let l_u_pars = x_20463 in h_mk_lin_params l_u_pars
1550
1551(** val lin_params_rect_Type3 :
1552    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1553let rec lin_params_rect_Type3 h_mk_lin_params x_20465 =
1554  let l_u_pars = x_20465 in h_mk_lin_params l_u_pars
1555
1556(** val lin_params_rect_Type2 :
1557    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1558let rec lin_params_rect_Type2 h_mk_lin_params x_20467 =
1559  let l_u_pars = x_20467 in h_mk_lin_params l_u_pars
1560
1561(** val lin_params_rect_Type1 :
1562    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1563let rec lin_params_rect_Type1 h_mk_lin_params x_20469 =
1564  let l_u_pars = x_20469 in h_mk_lin_params l_u_pars
1565
1566(** val lin_params_rect_Type0 :
1567    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1568let rec lin_params_rect_Type0 h_mk_lin_params x_20471 =
1569  let l_u_pars = x_20471 in h_mk_lin_params l_u_pars
1570
1571(** val l_u_pars : lin_params -> unserialized_params **)
1572let rec l_u_pars xxx =
1573  let yyy = xxx in yyy
1574
1575(** val lin_params_inv_rect_Type4 :
1576    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1577let lin_params_inv_rect_Type4 hterm h1 =
1578  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
1579
1580(** val lin_params_inv_rect_Type3 :
1581    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1582let lin_params_inv_rect_Type3 hterm h1 =
1583  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
1584
1585(** val lin_params_inv_rect_Type2 :
1586    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1587let lin_params_inv_rect_Type2 hterm h1 =
1588  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
1589
1590(** val lin_params_inv_rect_Type1 :
1591    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1592let lin_params_inv_rect_Type1 hterm h1 =
1593  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
1594
1595(** val lin_params_inv_rect_Type0 :
1596    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1597let lin_params_inv_rect_Type0 hterm h1 =
1598  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
1599
1600(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
1601let lin_params_jmdiscr x y =
1602  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1603
1604(** val lin_params_to_params : lin_params -> params **)
1605let lin_params_to_params lp =
1606  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
1607    Types.None); has_fcond = Bool.True }; stmt_at =
1608    (fun globals code point ->
1609    Obj.magic
1610      (Monad.m_bind0 (Monad.max_def Option.option0)
1611        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
1612        (fun ls ->
1613        Monad.m_return0 (Monad.max_def Option.option0) ls.Types.snd)));
1614    point_of_label = (fun globals c lbl ->
1615    Util.if_then_else_safe
1616      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
1617        (Obj.magic c)) (fun _ ->
1618      Obj.magic
1619        (Monad.m_return0 (Monad.max_def Option.option0)
1620          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
1621            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
1622    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
1623
1624(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
1625let lp_to_p__o__stmt_pars x0 =
1626  (lin_params_to_params x0).stmt_pars
1627
1628(** val lp_to_p__o__stmt_pars__o__uns_pars :
1629    lin_params -> unserialized_params **)
1630let lp_to_p__o__stmt_pars__o__uns_pars x0 =
1631  stmt_pars__o__uns_pars (lin_params_to_params x0)
1632
1633type graph_params =
1634  unserialized_params
1635  (* singleton inductive, whose constructor was mk_graph_params *)
1636
1637(** val graph_params_rect_Type4 :
1638    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1639let rec graph_params_rect_Type4 h_mk_graph_params x_20487 =
1640  let g_u_pars = x_20487 in h_mk_graph_params g_u_pars
1641
1642(** val graph_params_rect_Type5 :
1643    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1644let rec graph_params_rect_Type5 h_mk_graph_params x_20489 =
1645  let g_u_pars = x_20489 in h_mk_graph_params g_u_pars
1646
1647(** val graph_params_rect_Type3 :
1648    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1649let rec graph_params_rect_Type3 h_mk_graph_params x_20491 =
1650  let g_u_pars = x_20491 in h_mk_graph_params g_u_pars
1651
1652(** val graph_params_rect_Type2 :
1653    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1654let rec graph_params_rect_Type2 h_mk_graph_params x_20493 =
1655  let g_u_pars = x_20493 in h_mk_graph_params g_u_pars
1656
1657(** val graph_params_rect_Type1 :
1658    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1659let rec graph_params_rect_Type1 h_mk_graph_params x_20495 =
1660  let g_u_pars = x_20495 in h_mk_graph_params g_u_pars
1661
1662(** val graph_params_rect_Type0 :
1663    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1664let rec graph_params_rect_Type0 h_mk_graph_params x_20497 =
1665  let g_u_pars = x_20497 in h_mk_graph_params g_u_pars
1666
1667(** val g_u_pars : graph_params -> unserialized_params **)
1668let rec g_u_pars xxx =
1669  let yyy = xxx in yyy
1670
1671(** val graph_params_inv_rect_Type4 :
1672    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1673let graph_params_inv_rect_Type4 hterm h1 =
1674  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
1675
1676(** val graph_params_inv_rect_Type3 :
1677    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1678let graph_params_inv_rect_Type3 hterm h1 =
1679  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
1680
1681(** val graph_params_inv_rect_Type2 :
1682    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1683let graph_params_inv_rect_Type2 hterm h1 =
1684  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
1685
1686(** val graph_params_inv_rect_Type1 :
1687    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1688let graph_params_inv_rect_Type1 hterm h1 =
1689  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
1690
1691(** val graph_params_inv_rect_Type0 :
1692    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1693let graph_params_inv_rect_Type0 hterm h1 =
1694  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
1695
1696(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
1697let graph_params_jmdiscr x y =
1698  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1699
1700(** val graph_params_to_params : graph_params -> params **)
1701let graph_params_to_params gp =
1702  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
1703    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
1704    (fun globals code ->
1705    Obj.magic (Identifiers.lookup0 PreIdentifiers.LabelTag (Obj.magic code)));
1706    point_of_label = (fun x x0 lbl ->
1707    Obj.magic (Monad.m_return0 (Monad.max_def Option.option0) lbl));
1708    point_of_succ = (fun x lbl -> lbl) }
1709
1710(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
1711let gp_to_p__o__stmt_pars x0 =
1712  (graph_params_to_params x0).stmt_pars
1713
1714(** val gp_to_p__o__stmt_pars__o__uns_pars :
1715    graph_params -> unserialized_params **)
1716let gp_to_p__o__stmt_pars__o__uns_pars x0 =
1717  stmt_pars__o__uns_pars (graph_params_to_params x0)
1718
1719type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1720                                 joint_if_runiverse : Identifiers.universe;
1721                                 joint_if_result : __; joint_if_params : 
1722                                 __; joint_if_stacksize : Nat.nat;
1723                                 joint_if_code : __;
1724                                 joint_if_entry : __ Types.sig0 }
1725
1726(** val joint_internal_function_rect_Type4 :
1727    params -> AST.ident List.list -> (Identifiers.universe ->
1728    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1729    'a1) -> joint_internal_function -> 'a1 **)
1730let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20513 =
1731  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1732    joint_if_runiverse0; joint_if_result = joint_if_result0;
1733    joint_if_params = joint_if_params0; joint_if_stacksize =
1734    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1735    joint_if_entry0 } = x_20513
1736  in
1737  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1738    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1739    joint_if_entry0
1740
1741(** val joint_internal_function_rect_Type5 :
1742    params -> AST.ident List.list -> (Identifiers.universe ->
1743    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1744    'a1) -> joint_internal_function -> 'a1 **)
1745let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20515 =
1746  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1747    joint_if_runiverse0; joint_if_result = joint_if_result0;
1748    joint_if_params = joint_if_params0; joint_if_stacksize =
1749    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1750    joint_if_entry0 } = x_20515
1751  in
1752  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1753    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1754    joint_if_entry0
1755
1756(** val joint_internal_function_rect_Type3 :
1757    params -> AST.ident List.list -> (Identifiers.universe ->
1758    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1759    'a1) -> joint_internal_function -> 'a1 **)
1760let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20517 =
1761  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1762    joint_if_runiverse0; joint_if_result = joint_if_result0;
1763    joint_if_params = joint_if_params0; joint_if_stacksize =
1764    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1765    joint_if_entry0 } = x_20517
1766  in
1767  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1768    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1769    joint_if_entry0
1770
1771(** val joint_internal_function_rect_Type2 :
1772    params -> AST.ident List.list -> (Identifiers.universe ->
1773    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1774    'a1) -> joint_internal_function -> 'a1 **)
1775let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20519 =
1776  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1777    joint_if_runiverse0; joint_if_result = joint_if_result0;
1778    joint_if_params = joint_if_params0; joint_if_stacksize =
1779    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1780    joint_if_entry0 } = x_20519
1781  in
1782  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1783    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1784    joint_if_entry0
1785
1786(** val joint_internal_function_rect_Type1 :
1787    params -> AST.ident List.list -> (Identifiers.universe ->
1788    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1789    'a1) -> joint_internal_function -> 'a1 **)
1790let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20521 =
1791  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1792    joint_if_runiverse0; joint_if_result = joint_if_result0;
1793    joint_if_params = joint_if_params0; joint_if_stacksize =
1794    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1795    joint_if_entry0 } = x_20521
1796  in
1797  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1798    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1799    joint_if_entry0
1800
1801(** val joint_internal_function_rect_Type0 :
1802    params -> AST.ident List.list -> (Identifiers.universe ->
1803    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1804    'a1) -> joint_internal_function -> 'a1 **)
1805let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20523 =
1806  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1807    joint_if_runiverse0; joint_if_result = joint_if_result0;
1808    joint_if_params = joint_if_params0; joint_if_stacksize =
1809    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1810    joint_if_entry0 } = x_20523
1811  in
1812  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1813    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1814    joint_if_entry0
1815
1816(** val joint_if_luniverse :
1817    params -> AST.ident List.list -> joint_internal_function ->
1818    Identifiers.universe **)
1819let rec joint_if_luniverse p globals xxx =
1820  xxx.joint_if_luniverse
1821
1822(** val joint_if_runiverse :
1823    params -> AST.ident List.list -> joint_internal_function ->
1824    Identifiers.universe **)
1825let rec joint_if_runiverse p globals xxx =
1826  xxx.joint_if_runiverse
1827
1828(** val joint_if_result :
1829    params -> AST.ident List.list -> joint_internal_function -> __ **)
1830let rec joint_if_result p globals xxx =
1831  xxx.joint_if_result
1832
1833(** val joint_if_params :
1834    params -> AST.ident List.list -> joint_internal_function -> __ **)
1835let rec joint_if_params p globals xxx =
1836  xxx.joint_if_params
1837
1838(** val joint_if_stacksize :
1839    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
1840let rec joint_if_stacksize p globals xxx =
1841  xxx.joint_if_stacksize
1842
1843(** val joint_if_code :
1844    params -> AST.ident List.list -> joint_internal_function -> __ **)
1845let rec joint_if_code p globals xxx =
1846  xxx.joint_if_code
1847
1848(** val joint_if_entry :
1849    params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0 **)
1850let rec joint_if_entry p globals xxx =
1851  xxx.joint_if_entry
1852
1853(** val joint_internal_function_inv_rect_Type4 :
1854    params -> AST.ident List.list -> joint_internal_function ->
1855    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1856    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1857let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
1858  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
1859
1860(** val joint_internal_function_inv_rect_Type3 :
1861    params -> AST.ident List.list -> joint_internal_function ->
1862    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1863    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1864let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
1865  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
1866
1867(** val joint_internal_function_inv_rect_Type2 :
1868    params -> AST.ident List.list -> joint_internal_function ->
1869    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1870    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1871let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
1872  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
1873
1874(** val joint_internal_function_inv_rect_Type1 :
1875    params -> AST.ident List.list -> joint_internal_function ->
1876    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1877    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1878let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
1879  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
1880
1881(** val joint_internal_function_inv_rect_Type0 :
1882    params -> AST.ident List.list -> joint_internal_function ->
1883    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1884    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1885let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
1886  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
1887
1888(** val joint_internal_function_jmdiscr :
1889    params -> AST.ident List.list -> joint_internal_function ->
1890    joint_internal_function -> __ **)
1891let joint_internal_function_jmdiscr a1 a2 x y =
1892  Logic.eq_rect_Type2 x
1893    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
1894       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
1895       joint_if_code = a5; joint_if_entry = a6 } = x
1896     in
1897    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1898
1899(** val good_if_rect_Type4 :
1900    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1901    __ -> __ -> 'a1) -> 'a1 **)
1902let rec good_if_rect_Type4 p globals def h_mk_good_if =
1903  h_mk_good_if __ __ __ __
1904
1905(** val good_if_rect_Type5 :
1906    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1907    __ -> __ -> 'a1) -> 'a1 **)
1908let rec good_if_rect_Type5 p globals def h_mk_good_if =
1909  h_mk_good_if __ __ __ __
1910
1911(** val good_if_rect_Type3 :
1912    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1913    __ -> __ -> 'a1) -> 'a1 **)
1914let rec good_if_rect_Type3 p globals def h_mk_good_if =
1915  h_mk_good_if __ __ __ __
1916
1917(** val good_if_rect_Type2 :
1918    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1919    __ -> __ -> 'a1) -> 'a1 **)
1920let rec good_if_rect_Type2 p globals def h_mk_good_if =
1921  h_mk_good_if __ __ __ __
1922
1923(** val good_if_rect_Type1 :
1924    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1925    __ -> __ -> 'a1) -> 'a1 **)
1926let rec good_if_rect_Type1 p globals def h_mk_good_if =
1927  h_mk_good_if __ __ __ __
1928
1929(** val good_if_rect_Type0 :
1930    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1931    __ -> __ -> 'a1) -> 'a1 **)
1932let rec good_if_rect_Type0 p globals def h_mk_good_if =
1933  h_mk_good_if __ __ __ __
1934
1935(** val good_if_inv_rect_Type4 :
1936    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1937    __ -> __ -> __ -> 'a1) -> 'a1 **)
1938let good_if_inv_rect_Type4 x1 x2 x3 h1 =
1939  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
1940
1941(** val good_if_inv_rect_Type3 :
1942    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1943    __ -> __ -> __ -> 'a1) -> 'a1 **)
1944let good_if_inv_rect_Type3 x1 x2 x3 h1 =
1945  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
1946
1947(** val good_if_inv_rect_Type2 :
1948    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1949    __ -> __ -> __ -> 'a1) -> 'a1 **)
1950let good_if_inv_rect_Type2 x1 x2 x3 h1 =
1951  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
1952
1953(** val good_if_inv_rect_Type1 :
1954    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1955    __ -> __ -> __ -> 'a1) -> 'a1 **)
1956let good_if_inv_rect_Type1 x1 x2 x3 h1 =
1957  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
1958
1959(** val good_if_inv_rect_Type0 :
1960    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1961    __ -> __ -> __ -> 'a1) -> 'a1 **)
1962let good_if_inv_rect_Type0 x1 x2 x3 h1 =
1963  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
1964
1965(** val good_if_discr :
1966    params -> AST.ident List.list -> joint_internal_function -> __ **)
1967let good_if_discr a1 a2 a3 =
1968  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1969
1970(** val good_if_jmdiscr :
1971    params -> AST.ident List.list -> joint_internal_function -> __ **)
1972let good_if_jmdiscr a1 a2 a3 =
1973  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1974
1975type joint_closed_internal_function = joint_internal_function Types.sig0
1976
1977(** val set_joint_code :
1978    AST.ident List.list -> params -> joint_internal_function -> __ -> __
1979    Types.sig0 -> joint_internal_function **)
1980let set_joint_code globals pars int_fun graph0 entry =
1981  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
1982    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
1983    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
1984    int_fun.joint_if_stacksize; joint_if_code = graph0; joint_if_entry =
1985    entry }
1986
1987(** val set_joint_if_graph :
1988    AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
1989    joint_internal_function **)
1990let set_joint_if_graph globals pars graph0 p =
1991  set_joint_code globals (graph_params_to_params pars) p graph0
1992    (Types.pi1 p.joint_if_entry)
1993
1994(** val set_luniverse :
1995    params -> AST.ident List.list -> joint_internal_function ->
1996    Identifiers.universe -> joint_internal_function **)
1997let set_luniverse globals pars p luniverse =
1998  { joint_if_luniverse = luniverse; joint_if_runiverse =
1999    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2000    joint_if_params = p.joint_if_params; joint_if_stacksize =
2001    p.joint_if_stacksize; joint_if_code = p.joint_if_code; joint_if_entry =
2002    p.joint_if_entry }
2003
2004(** val set_runiverse :
2005    params -> AST.ident List.list -> joint_internal_function ->
2006    Identifiers.universe -> joint_internal_function **)
2007let set_runiverse globals pars p runiverse =
2008  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2009    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2010    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2011    joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry }
2012
2013(** val add_graph :
2014    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2015    joint_internal_function -> joint_internal_function **)
2016let add_graph g_pars globals l stmt p =
2017  let code =
2018    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2019      stmt
2020  in
2021  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2022  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2023  joint_if_params = p.joint_if_params; joint_if_stacksize =
2024  p.joint_if_stacksize; joint_if_code = (Obj.magic code); joint_if_entry =
2025  (Types.pi1 p.joint_if_entry) }
2026
2027type joint_function = joint_closed_internal_function AST.fundef
2028
2029type joint_program = (joint_function, Nat.nat) AST.program
2030
Note: See TracBrowser for help on using the repository browser.