source: extracted/joint.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 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_14700 -> h_Reg x_14700
113| Imm x_14701 -> h_Imm x_14701
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_14705 -> h_Reg x_14705
119| Imm x_14706 -> h_Imm x_14706
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_14710 -> h_Reg x_14710
125| Imm x_14711 -> h_Imm x_14711
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_14715 -> h_Reg x_14715
131| Imm x_14716 -> h_Imm x_14716
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_14720 -> h_Reg x_14720
137| Imm x_14721 -> h_Imm x_14721
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_14725 -> h_Reg x_14725
143| Imm x_14726 -> h_Imm x_14726
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_14761 =
327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
328    x_14761
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_14763 =
338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
339    x_14763
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_14765 =
349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
350    x_14765
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_14767 =
360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
361    x_14767
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_14769 =
371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
372    x_14769
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_14771 =
382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
383    x_14771
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_14827 -> h_COMMENT x_14827
492| MOVE x_14828 -> h_MOVE x_14828
493| POP x_14829 -> h_POP x_14829
494| PUSH x_14830 -> h_PUSH x_14830
495| ADDRESS (i, x_14832, x_14831) -> h_ADDRESS i __ x_14832 x_14831
496| OPACCS (x_14838, x_14837, x_14836, x_14835, x_14834) ->
497  h_OPACCS x_14838 x_14837 x_14836 x_14835 x_14834
498| OP1 (x_14841, x_14840, x_14839) -> h_OP1 x_14841 x_14840 x_14839
499| OP2 (x_14845, x_14844, x_14843, x_14842) ->
500  h_OP2 x_14845 x_14844 x_14843 x_14842
501| CLEAR_CARRY -> h_CLEAR_CARRY
502| SET_CARRY -> h_SET_CARRY
503| LOAD (x_14848, x_14847, x_14846) -> h_LOAD x_14848 x_14847 x_14846
504| STORE (x_14851, x_14850, x_14849) -> h_STORE x_14851 x_14850 x_14849
505| Extension_seq x_14852 -> h_extension_seq x_14852
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_14867 -> h_COMMENT x_14867
516| MOVE x_14868 -> h_MOVE x_14868
517| POP x_14869 -> h_POP x_14869
518| PUSH x_14870 -> h_PUSH x_14870
519| ADDRESS (i, x_14872, x_14871) -> h_ADDRESS i __ x_14872 x_14871
520| OPACCS (x_14878, x_14877, x_14876, x_14875, x_14874) ->
521  h_OPACCS x_14878 x_14877 x_14876 x_14875 x_14874
522| OP1 (x_14881, x_14880, x_14879) -> h_OP1 x_14881 x_14880 x_14879
523| OP2 (x_14885, x_14884, x_14883, x_14882) ->
524  h_OP2 x_14885 x_14884 x_14883 x_14882
525| CLEAR_CARRY -> h_CLEAR_CARRY
526| SET_CARRY -> h_SET_CARRY
527| LOAD (x_14888, x_14887, x_14886) -> h_LOAD x_14888 x_14887 x_14886
528| STORE (x_14891, x_14890, x_14889) -> h_STORE x_14891 x_14890 x_14889
529| Extension_seq x_14892 -> h_extension_seq x_14892
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_14907 -> h_COMMENT x_14907
540| MOVE x_14908 -> h_MOVE x_14908
541| POP x_14909 -> h_POP x_14909
542| PUSH x_14910 -> h_PUSH x_14910
543| ADDRESS (i, x_14912, x_14911) -> h_ADDRESS i __ x_14912 x_14911
544| OPACCS (x_14918, x_14917, x_14916, x_14915, x_14914) ->
545  h_OPACCS x_14918 x_14917 x_14916 x_14915 x_14914
546| OP1 (x_14921, x_14920, x_14919) -> h_OP1 x_14921 x_14920 x_14919
547| OP2 (x_14925, x_14924, x_14923, x_14922) ->
548  h_OP2 x_14925 x_14924 x_14923 x_14922
549| CLEAR_CARRY -> h_CLEAR_CARRY
550| SET_CARRY -> h_SET_CARRY
551| LOAD (x_14928, x_14927, x_14926) -> h_LOAD x_14928 x_14927 x_14926
552| STORE (x_14931, x_14930, x_14929) -> h_STORE x_14931 x_14930 x_14929
553| Extension_seq x_14932 -> h_extension_seq x_14932
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_14947 -> h_COMMENT x_14947
564| MOVE x_14948 -> h_MOVE x_14948
565| POP x_14949 -> h_POP x_14949
566| PUSH x_14950 -> h_PUSH x_14950
567| ADDRESS (i, x_14952, x_14951) -> h_ADDRESS i __ x_14952 x_14951
568| OPACCS (x_14958, x_14957, x_14956, x_14955, x_14954) ->
569  h_OPACCS x_14958 x_14957 x_14956 x_14955 x_14954
570| OP1 (x_14961, x_14960, x_14959) -> h_OP1 x_14961 x_14960 x_14959
571| OP2 (x_14965, x_14964, x_14963, x_14962) ->
572  h_OP2 x_14965 x_14964 x_14963 x_14962
573| CLEAR_CARRY -> h_CLEAR_CARRY
574| SET_CARRY -> h_SET_CARRY
575| LOAD (x_14968, x_14967, x_14966) -> h_LOAD x_14968 x_14967 x_14966
576| STORE (x_14971, x_14970, x_14969) -> h_STORE x_14971 x_14970 x_14969
577| Extension_seq x_14972 -> h_extension_seq x_14972
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_14987 -> h_COMMENT x_14987
588| MOVE x_14988 -> h_MOVE x_14988
589| POP x_14989 -> h_POP x_14989
590| PUSH x_14990 -> h_PUSH x_14990
591| ADDRESS (i, x_14992, x_14991) -> h_ADDRESS i __ x_14992 x_14991
592| OPACCS (x_14998, x_14997, x_14996, x_14995, x_14994) ->
593  h_OPACCS x_14998 x_14997 x_14996 x_14995 x_14994
594| OP1 (x_15001, x_15000, x_14999) -> h_OP1 x_15001 x_15000 x_14999
595| OP2 (x_15005, x_15004, x_15003, x_15002) ->
596  h_OP2 x_15005 x_15004 x_15003 x_15002
597| CLEAR_CARRY -> h_CLEAR_CARRY
598| SET_CARRY -> h_SET_CARRY
599| LOAD (x_15008, x_15007, x_15006) -> h_LOAD x_15008 x_15007 x_15006
600| STORE (x_15011, x_15010, x_15009) -> h_STORE x_15011 x_15010 x_15009
601| Extension_seq x_15012 -> h_extension_seq x_15012
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_15027 -> h_COMMENT x_15027
612| MOVE x_15028 -> h_MOVE x_15028
613| POP x_15029 -> h_POP x_15029
614| PUSH x_15030 -> h_PUSH x_15030
615| ADDRESS (i, x_15032, x_15031) -> h_ADDRESS i __ x_15032 x_15031
616| OPACCS (x_15038, x_15037, x_15036, x_15035, x_15034) ->
617  h_OPACCS x_15038 x_15037 x_15036 x_15035 x_15034
618| OP1 (x_15041, x_15040, x_15039) -> h_OP1 x_15041 x_15040 x_15039
619| OP2 (x_15045, x_15044, x_15043, x_15042) ->
620  h_OP2 x_15045 x_15044 x_15043 x_15042
621| CLEAR_CARRY -> h_CLEAR_CARRY
622| SET_CARRY -> h_SET_CARRY
623| LOAD (x_15048, x_15047, x_15046) -> h_LOAD x_15048 x_15047 x_15046
624| STORE (x_15051, x_15050, x_15049) -> h_STORE x_15051 x_15050 x_15049
625| Extension_seq x_15052 -> h_extension_seq x_15052
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_15319 -> h_COST_LABEL x_15319
788| CALL (x_15322, x_15321, x_15320) -> h_CALL x_15322 x_15321 x_15320
789| COND (x_15324, x_15323) -> h_COND x_15324 x_15323
790| Step_seq x_15325 -> h_step_seq x_15325
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_15331 -> h_COST_LABEL x_15331
798| CALL (x_15334, x_15333, x_15332) -> h_CALL x_15334 x_15333 x_15332
799| COND (x_15336, x_15335) -> h_COND x_15336 x_15335
800| Step_seq x_15337 -> h_step_seq x_15337
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_15343 -> h_COST_LABEL x_15343
808| CALL (x_15346, x_15345, x_15344) -> h_CALL x_15346 x_15345 x_15344
809| COND (x_15348, x_15347) -> h_COND x_15348 x_15347
810| Step_seq x_15349 -> h_step_seq x_15349
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_15355 -> h_COST_LABEL x_15355
818| CALL (x_15358, x_15357, x_15356) -> h_CALL x_15358 x_15357 x_15356
819| COND (x_15360, x_15359) -> h_COND x_15360 x_15359
820| Step_seq x_15361 -> h_step_seq x_15361
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_15367 -> h_COST_LABEL x_15367
828| CALL (x_15370, x_15369, x_15368) -> h_CALL x_15370 x_15369 x_15368
829| COND (x_15372, x_15371) -> h_COND x_15372 x_15371
830| Step_seq x_15373 -> h_step_seq x_15373
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_15379 -> h_COST_LABEL x_15379
838| CALL (x_15382, x_15381, x_15380) -> h_CALL x_15382 x_15381 x_15380
839| COND (x_15384, x_15383) -> h_COND x_15384 x_15383
840| Step_seq x_15385 -> h_step_seq x_15385
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_15464 =
998  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
999    has_fcond0 } = x_15464
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_15466 =
1007  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1008    has_fcond0 } = x_15466
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_15468 =
1016  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1017    has_fcond0 } = x_15468
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_15470 =
1025  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1026    has_fcond0 } = x_15470
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_15472 =
1034  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1035    has_fcond0 } = x_15472
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_15474 =
1043  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1044    has_fcond0 } = x_15474
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 succ = __
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_15498 -> h_GOTO x_15498
1108| RETURN -> h_RETURN
1109| TAILCALL (x_15500, x_15499) -> h_TAILCALL __ x_15500 x_15499
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_15506 -> h_GOTO x_15506
1116| RETURN -> h_RETURN
1117| TAILCALL (x_15508, x_15507) -> h_TAILCALL __ x_15508 x_15507
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_15514 -> h_GOTO x_15514
1124| RETURN -> h_RETURN
1125| TAILCALL (x_15516, x_15515) -> h_TAILCALL __ x_15516 x_15515
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_15522 -> h_GOTO x_15522
1132| RETURN -> h_RETURN
1133| TAILCALL (x_15524, x_15523) -> h_TAILCALL __ x_15524 x_15523
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_15530 -> h_GOTO x_15530
1140| RETURN -> h_RETURN
1141| TAILCALL (x_15532, x_15531) -> h_TAILCALL __ x_15532 x_15531
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_15538 -> h_GOTO x_15538
1148| RETURN -> h_RETURN
1149| TAILCALL (x_15540, x_15539) -> h_TAILCALL __ x_15540 x_15539
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_15606, x_15605) -> h_sequential x_15606 x_15605
1222| Final x_15607 -> h_final x_15607
1223| FCOND (x_15610, x_15609, x_15608) -> h_FCOND __ x_15610 x_15609 x_15608
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_15617, x_15616) -> h_sequential x_15617 x_15616
1231| Final x_15618 -> h_final x_15618
1232| FCOND (x_15621, x_15620, x_15619) -> h_FCOND __ x_15621 x_15620 x_15619
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_15628, x_15627) -> h_sequential x_15628 x_15627
1240| Final x_15629 -> h_final x_15629
1241| FCOND (x_15632, x_15631, x_15630) -> h_FCOND __ x_15632 x_15631 x_15630
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_15639, x_15638) -> h_sequential x_15639 x_15638
1249| Final x_15640 -> h_final x_15640
1250| FCOND (x_15643, x_15642, x_15641) -> h_FCOND __ x_15643 x_15642 x_15641
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_15650, x_15649) -> h_sequential x_15650 x_15649
1258| Final x_15651 -> h_final x_15651
1259| FCOND (x_15654, x_15653, x_15652) -> h_FCOND __ x_15654 x_15653 x_15652
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_15661, x_15660) -> h_sequential x_15661 x_15660
1267| Final x_15662 -> h_final x_15662
1268| FCOND (x_15665, x_15664, x_15663) -> h_FCOND __ x_15665 x_15664 x_15663
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_15738 =
1368  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1369    point_of_label0; point_of_succ = point_of_succ0 } = x_15738
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_15740 =
1379  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1380    point_of_label0; point_of_succ = point_of_succ0 } = x_15740
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_15742 =
1390  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1391    point_of_label0; point_of_succ = point_of_succ0 } = x_15742
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_15744 =
1401  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1402    point_of_label0; point_of_succ = point_of_succ0 } = x_15744
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_15746 =
1412  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1413    point_of_label0; point_of_succ = point_of_succ0 } = x_15746
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_15748 =
1423  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1424    point_of_label0; point_of_succ = point_of_succ0 } = x_15748
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 g stmt =
1531  List.append
1532    (match stmt_implicit_label p g stmt with
1533     | Types.None -> List.Nil
1534     | Types.Some l -> List.Cons (l, List.Nil))
1535    (stmt_explicit_labels p g 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_15771 =
1544  let l_u_pars = x_15771 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_15773 =
1549  let l_u_pars = x_15773 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_15775 =
1554  let l_u_pars = x_15775 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_15777 =
1559  let l_u_pars = x_15777 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_15779 =
1564  let l_u_pars = x_15779 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_15781 =
1569  let l_u_pars = x_15781 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.option)
1611        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
1612        (fun ls ->
1613        Monad.m_return0 (Monad.max_def Option.option) 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.option)
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_15797 =
1640  let g_u_pars = x_15797 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_15799 =
1645  let g_u_pars = x_15799 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_15801 =
1650  let g_u_pars = x_15801 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_15803 =
1655  let g_u_pars = x_15803 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_15805 =
1660  let g_u_pars = x_15805 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_15807 =
1665  let g_u_pars = x_15807 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.lookup PreIdentifiers.LabelTag (Obj.magic code)));
1706    point_of_label = (fun x x0 lbl ->
1707    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) 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_15823 =
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_15823
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_15825 =
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_15825
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_15827 =
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_15827
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_15829 =
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_15829
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_15831 =
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_15831
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_15833 =
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_15833
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 graph 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 = graph; 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 graph p =
1991  set_joint_code globals (graph_params_to_params pars) p graph
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.