source: extracted/joint.ml @ 2731

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

Exported again.

File size: 72.4 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_6298 -> h_Reg x_6298
113| Imm x_6299 -> h_Imm x_6299
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_6303 -> h_Reg x_6303
119| Imm x_6304 -> h_Imm x_6304
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_6308 -> h_Reg x_6308
125| Imm x_6309 -> h_Imm x_6309
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_6313 -> h_Reg x_6313
131| Imm x_6314 -> h_Imm x_6314
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_6318 -> h_Reg x_6318
137| Imm x_6319 -> h_Imm x_6319
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_6323 -> h_Reg x_6323
143| Imm x_6324 -> h_Imm x_6324
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 psd_argument_from_byte : BitVector.byte -> psd_argument **)
196let psd_argument_from_byte x =
197  Imm x
198
199type hdw_argument = I8051.register argument
200
201(** val hdw_argument_from_reg : I8051.register -> hdw_argument **)
202let hdw_argument_from_reg x =
203  Reg x
204
205(** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **)
206let hdw_argument_from_byte x =
207  Imm x
208
209(** val byte_of_nat : Nat.nat -> BitVector.byte **)
210let byte_of_nat =
211  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
212    (Nat.S (Nat.S Nat.O))))))))
213
214(** val zero_byte : BitVector.byte **)
215let zero_byte =
216  BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
217    Nat.O))))))))
218
219type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
220                             has_tailcalls : Bool.bool }
221
222(** val unserialized_params_rect_Type4 :
223    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
224    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
225    unserialized_params -> 'a1 **)
226let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_6359 =
227  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
228    x_6359
229  in
230  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
231    ext_seq_labels0 has_tailcalls0 __
232
233(** val unserialized_params_rect_Type5 :
234    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
235    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
236    unserialized_params -> 'a1 **)
237let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_6361 =
238  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
239    x_6361
240  in
241  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
242    ext_seq_labels0 has_tailcalls0 __
243
244(** val unserialized_params_rect_Type3 :
245    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
246    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
247    unserialized_params -> 'a1 **)
248let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_6363 =
249  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
250    x_6363
251  in
252  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
253    ext_seq_labels0 has_tailcalls0 __
254
255(** val unserialized_params_rect_Type2 :
256    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
257    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
258    unserialized_params -> 'a1 **)
259let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_6365 =
260  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
261    x_6365
262  in
263  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
264    ext_seq_labels0 has_tailcalls0 __
265
266(** val unserialized_params_rect_Type1 :
267    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
268    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
269    unserialized_params -> 'a1 **)
270let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_6367 =
271  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
272    x_6367
273  in
274  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
275    ext_seq_labels0 has_tailcalls0 __
276
277(** val unserialized_params_rect_Type0 :
278    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
279    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
280    unserialized_params -> 'a1 **)
281let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_6369 =
282  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
283    x_6369
284  in
285  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
286    ext_seq_labels0 has_tailcalls0 __
287
288type acc_a_reg = __
289
290type acc_b_reg = __
291
292type acc_a_arg = __
293
294type acc_b_arg = __
295
296type dpl_reg = __
297
298type dph_reg = __
299
300type dpl_arg = __
301
302type dph_arg = __
303
304type snd_arg = __
305
306type pair_move = __
307
308type call_args = __
309
310type call_dest = __
311
312type ext_seq = __
313
314(** val ext_seq_labels :
315    unserialized_params -> __ -> Graphs.label List.list **)
316let rec ext_seq_labels xxx =
317  xxx.ext_seq_labels
318
319(** val has_tailcalls : unserialized_params -> Bool.bool **)
320let rec has_tailcalls xxx =
321  xxx.has_tailcalls
322
323type paramsT = __
324
325(** val unserialized_params_inv_rect_Type4 :
326    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
327    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
328    -> __ -> __ -> 'a1) -> 'a1 **)
329let unserialized_params_inv_rect_Type4 hterm h1 =
330  let hcut = unserialized_params_rect_Type4 h1 hterm in hcut __
331
332(** val unserialized_params_inv_rect_Type3 :
333    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
334    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
335    -> __ -> __ -> 'a1) -> 'a1 **)
336let unserialized_params_inv_rect_Type3 hterm h1 =
337  let hcut = unserialized_params_rect_Type3 h1 hterm in hcut __
338
339(** val unserialized_params_inv_rect_Type2 :
340    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
341    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
342    -> __ -> __ -> 'a1) -> 'a1 **)
343let unserialized_params_inv_rect_Type2 hterm h1 =
344  let hcut = unserialized_params_rect_Type2 h1 hterm in hcut __
345
346(** val unserialized_params_inv_rect_Type1 :
347    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
348    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
349    -> __ -> __ -> 'a1) -> 'a1 **)
350let unserialized_params_inv_rect_Type1 hterm h1 =
351  let hcut = unserialized_params_rect_Type1 h1 hterm in hcut __
352
353(** val unserialized_params_inv_rect_Type0 :
354    unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
355    __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
356    -> __ -> __ -> 'a1) -> 'a1 **)
357let unserialized_params_inv_rect_Type0 hterm h1 =
358  let hcut = unserialized_params_rect_Type0 h1 hterm in hcut __
359
360(** val unserialized_params_jmdiscr :
361    unserialized_params -> unserialized_params -> __ **)
362let unserialized_params_jmdiscr x y =
363  Logic.eq_rect_Type2 x
364    (let { ext_seq_labels = a13; has_tailcalls = a14 } = x in
365    Obj.magic (fun _ dH ->
366      dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
367
368type joint_seq =
369| COMMENT of String.string
370| MOVE of __
371| POP of __
372| PUSH of __
373| ADDRESS of AST.ident * __ * __
374| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
375| OP1 of BackEndOps.op1 * __ * __
376| OP2 of BackEndOps.op2 * __ * __ * __
377| CLEAR_CARRY
378| SET_CARRY
379| LOAD of __ * __ * __
380| STORE of __ * __ * __
381| Extension_seq of __
382
383(** val joint_seq_rect_Type4 :
384    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
385    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
386    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
387    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
388    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
389    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
390let 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
391| COMMENT x_6425 -> h_COMMENT x_6425
392| MOVE x_6426 -> h_MOVE x_6426
393| POP x_6427 -> h_POP x_6427
394| PUSH x_6428 -> h_PUSH x_6428
395| ADDRESS (i, x_6430, x_6429) -> h_ADDRESS i __ x_6430 x_6429
396| OPACCS (x_6436, x_6435, x_6434, x_6433, x_6432) ->
397  h_OPACCS x_6436 x_6435 x_6434 x_6433 x_6432
398| OP1 (x_6439, x_6438, x_6437) -> h_OP1 x_6439 x_6438 x_6437
399| OP2 (x_6443, x_6442, x_6441, x_6440) -> h_OP2 x_6443 x_6442 x_6441 x_6440
400| CLEAR_CARRY -> h_CLEAR_CARRY
401| SET_CARRY -> h_SET_CARRY
402| LOAD (x_6446, x_6445, x_6444) -> h_LOAD x_6446 x_6445 x_6444
403| STORE (x_6449, x_6448, x_6447) -> h_STORE x_6449 x_6448 x_6447
404| Extension_seq x_6450 -> h_extension_seq x_6450
405
406(** val joint_seq_rect_Type5 :
407    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
408    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
409    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
410    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
411    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
412    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
413let 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
414| COMMENT x_6465 -> h_COMMENT x_6465
415| MOVE x_6466 -> h_MOVE x_6466
416| POP x_6467 -> h_POP x_6467
417| PUSH x_6468 -> h_PUSH x_6468
418| ADDRESS (i, x_6470, x_6469) -> h_ADDRESS i __ x_6470 x_6469
419| OPACCS (x_6476, x_6475, x_6474, x_6473, x_6472) ->
420  h_OPACCS x_6476 x_6475 x_6474 x_6473 x_6472
421| OP1 (x_6479, x_6478, x_6477) -> h_OP1 x_6479 x_6478 x_6477
422| OP2 (x_6483, x_6482, x_6481, x_6480) -> h_OP2 x_6483 x_6482 x_6481 x_6480
423| CLEAR_CARRY -> h_CLEAR_CARRY
424| SET_CARRY -> h_SET_CARRY
425| LOAD (x_6486, x_6485, x_6484) -> h_LOAD x_6486 x_6485 x_6484
426| STORE (x_6489, x_6488, x_6487) -> h_STORE x_6489 x_6488 x_6487
427| Extension_seq x_6490 -> h_extension_seq x_6490
428
429(** val joint_seq_rect_Type3 :
430    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
431    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
432    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
433    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
434    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
435    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
436let 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
437| COMMENT x_6505 -> h_COMMENT x_6505
438| MOVE x_6506 -> h_MOVE x_6506
439| POP x_6507 -> h_POP x_6507
440| PUSH x_6508 -> h_PUSH x_6508
441| ADDRESS (i, x_6510, x_6509) -> h_ADDRESS i __ x_6510 x_6509
442| OPACCS (x_6516, x_6515, x_6514, x_6513, x_6512) ->
443  h_OPACCS x_6516 x_6515 x_6514 x_6513 x_6512
444| OP1 (x_6519, x_6518, x_6517) -> h_OP1 x_6519 x_6518 x_6517
445| OP2 (x_6523, x_6522, x_6521, x_6520) -> h_OP2 x_6523 x_6522 x_6521 x_6520
446| CLEAR_CARRY -> h_CLEAR_CARRY
447| SET_CARRY -> h_SET_CARRY
448| LOAD (x_6526, x_6525, x_6524) -> h_LOAD x_6526 x_6525 x_6524
449| STORE (x_6529, x_6528, x_6527) -> h_STORE x_6529 x_6528 x_6527
450| Extension_seq x_6530 -> h_extension_seq x_6530
451
452(** val joint_seq_rect_Type2 :
453    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
454    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
455    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
456    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
457    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
458    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
459let 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
460| COMMENT x_6545 -> h_COMMENT x_6545
461| MOVE x_6546 -> h_MOVE x_6546
462| POP x_6547 -> h_POP x_6547
463| PUSH x_6548 -> h_PUSH x_6548
464| ADDRESS (i, x_6550, x_6549) -> h_ADDRESS i __ x_6550 x_6549
465| OPACCS (x_6556, x_6555, x_6554, x_6553, x_6552) ->
466  h_OPACCS x_6556 x_6555 x_6554 x_6553 x_6552
467| OP1 (x_6559, x_6558, x_6557) -> h_OP1 x_6559 x_6558 x_6557
468| OP2 (x_6563, x_6562, x_6561, x_6560) -> h_OP2 x_6563 x_6562 x_6561 x_6560
469| CLEAR_CARRY -> h_CLEAR_CARRY
470| SET_CARRY -> h_SET_CARRY
471| LOAD (x_6566, x_6565, x_6564) -> h_LOAD x_6566 x_6565 x_6564
472| STORE (x_6569, x_6568, x_6567) -> h_STORE x_6569 x_6568 x_6567
473| Extension_seq x_6570 -> h_extension_seq x_6570
474
475(** val joint_seq_rect_Type1 :
476    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
477    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
478    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
479    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
480    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
481    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
482let 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
483| COMMENT x_6585 -> h_COMMENT x_6585
484| MOVE x_6586 -> h_MOVE x_6586
485| POP x_6587 -> h_POP x_6587
486| PUSH x_6588 -> h_PUSH x_6588
487| ADDRESS (i, x_6590, x_6589) -> h_ADDRESS i __ x_6590 x_6589
488| OPACCS (x_6596, x_6595, x_6594, x_6593, x_6592) ->
489  h_OPACCS x_6596 x_6595 x_6594 x_6593 x_6592
490| OP1 (x_6599, x_6598, x_6597) -> h_OP1 x_6599 x_6598 x_6597
491| OP2 (x_6603, x_6602, x_6601, x_6600) -> h_OP2 x_6603 x_6602 x_6601 x_6600
492| CLEAR_CARRY -> h_CLEAR_CARRY
493| SET_CARRY -> h_SET_CARRY
494| LOAD (x_6606, x_6605, x_6604) -> h_LOAD x_6606 x_6605 x_6604
495| STORE (x_6609, x_6608, x_6607) -> h_STORE x_6609 x_6608 x_6607
496| Extension_seq x_6610 -> h_extension_seq x_6610
497
498(** val joint_seq_rect_Type0 :
499    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
500    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
501    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
502    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
503    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
504    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
505let 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
506| COMMENT x_6625 -> h_COMMENT x_6625
507| MOVE x_6626 -> h_MOVE x_6626
508| POP x_6627 -> h_POP x_6627
509| PUSH x_6628 -> h_PUSH x_6628
510| ADDRESS (i, x_6630, x_6629) -> h_ADDRESS i __ x_6630 x_6629
511| OPACCS (x_6636, x_6635, x_6634, x_6633, x_6632) ->
512  h_OPACCS x_6636 x_6635 x_6634 x_6633 x_6632
513| OP1 (x_6639, x_6638, x_6637) -> h_OP1 x_6639 x_6638 x_6637
514| OP2 (x_6643, x_6642, x_6641, x_6640) -> h_OP2 x_6643 x_6642 x_6641 x_6640
515| CLEAR_CARRY -> h_CLEAR_CARRY
516| SET_CARRY -> h_SET_CARRY
517| LOAD (x_6646, x_6645, x_6644) -> h_LOAD x_6646 x_6645 x_6644
518| STORE (x_6649, x_6648, x_6647) -> h_STORE x_6649 x_6648 x_6647
519| Extension_seq x_6650 -> h_extension_seq x_6650
520
521(** val joint_seq_inv_rect_Type4 :
522    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
523    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
524    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
525    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
526    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
527    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
528    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
529let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
530  let hcut =
531    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
532      hterm
533  in
534  hcut __
535
536(** val joint_seq_inv_rect_Type3 :
537    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
538    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
539    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
540    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
541    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
542    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
543    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
544let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
545  let hcut =
546    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
547      hterm
548  in
549  hcut __
550
551(** val joint_seq_inv_rect_Type2 :
552    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
553    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
554    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
555    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
556    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
557    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
558    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
559let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
560  let hcut =
561    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
562      hterm
563  in
564  hcut __
565
566(** val joint_seq_inv_rect_Type1 :
567    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
568    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
569    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
570    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
571    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
572    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
573    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
574let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
575  let hcut =
576    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
577      hterm
578  in
579  hcut __
580
581(** val joint_seq_inv_rect_Type0 :
582    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
583    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
584    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
585    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
586    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
587    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
588    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
589let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
590  let hcut =
591    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
592      hterm
593  in
594  hcut __
595
596(** val joint_seq_discr :
597    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
598    __ **)
599let joint_seq_discr a1 a2 x y =
600  Logic.eq_rect_Type2 x
601    (match x with
602     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
603     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
604     | POP a0 -> Obj.magic (fun _ dH -> dH __)
605     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
606     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
607     | OPACCS (a0, a10, a20, a3, a4) ->
608       Obj.magic (fun _ dH -> dH __ __ __ __ __)
609     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
610     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
611     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
612     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
613     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
614     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
615     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
616
617(** val joint_seq_jmdiscr :
618    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
619    __ **)
620let joint_seq_jmdiscr a1 a2 x y =
621  Logic.eq_rect_Type2 x
622    (match x with
623     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
624     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
625     | POP a0 -> Obj.magic (fun _ dH -> dH __)
626     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
627     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
628     | OPACCS (a0, a10, a20, a3, a4) ->
629       Obj.magic (fun _ dH -> dH __ __ __ __ __)
630     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
631     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
632     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
633     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
634     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
635     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
636     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
637
638(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
639let nOOP p globals =
640  COMMENT String.EmptyString
641
642type joint_step =
643| COST_LABEL of CostLabel.costlabel
644| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
645| COND of __ * Graphs.label
646| Step_seq of joint_seq
647
648(** val joint_step_rect_Type4 :
649    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
650    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
651    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
652let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
653| COST_LABEL x_6917 -> h_COST_LABEL x_6917
654| CALL (x_6920, x_6919, x_6918) -> h_CALL x_6920 x_6919 x_6918
655| COND (x_6922, x_6921) -> h_COND x_6922 x_6921
656| Step_seq x_6923 -> h_step_seq x_6923
657
658(** val joint_step_rect_Type5 :
659    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
660    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
661    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
662let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
663| COST_LABEL x_6929 -> h_COST_LABEL x_6929
664| CALL (x_6932, x_6931, x_6930) -> h_CALL x_6932 x_6931 x_6930
665| COND (x_6934, x_6933) -> h_COND x_6934 x_6933
666| Step_seq x_6935 -> h_step_seq x_6935
667
668(** val joint_step_rect_Type3 :
669    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
670    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
671    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
672let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
673| COST_LABEL x_6941 -> h_COST_LABEL x_6941
674| CALL (x_6944, x_6943, x_6942) -> h_CALL x_6944 x_6943 x_6942
675| COND (x_6946, x_6945) -> h_COND x_6946 x_6945
676| Step_seq x_6947 -> h_step_seq x_6947
677
678(** val joint_step_rect_Type2 :
679    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
680    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
681    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
682let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
683| COST_LABEL x_6953 -> h_COST_LABEL x_6953
684| CALL (x_6956, x_6955, x_6954) -> h_CALL x_6956 x_6955 x_6954
685| COND (x_6958, x_6957) -> h_COND x_6958 x_6957
686| Step_seq x_6959 -> h_step_seq x_6959
687
688(** val joint_step_rect_Type1 :
689    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
690    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
691    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
692let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
693| COST_LABEL x_6965 -> h_COST_LABEL x_6965
694| CALL (x_6968, x_6967, x_6966) -> h_CALL x_6968 x_6967 x_6966
695| COND (x_6970, x_6969) -> h_COND x_6970 x_6969
696| Step_seq x_6971 -> h_step_seq x_6971
697
698(** val joint_step_rect_Type0 :
699    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
700    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
701    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
702let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
703| COST_LABEL x_6977 -> h_COST_LABEL x_6977
704| CALL (x_6980, x_6979, x_6978) -> h_CALL x_6980 x_6979 x_6978
705| COND (x_6982, x_6981) -> h_COND x_6982 x_6981
706| Step_seq x_6983 -> h_step_seq x_6983
707
708(** val joint_step_inv_rect_Type4 :
709    unserialized_params -> AST.ident List.list -> joint_step ->
710    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
711    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
712    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
713let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
714  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
715
716(** val joint_step_inv_rect_Type3 :
717    unserialized_params -> AST.ident List.list -> joint_step ->
718    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
719    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
720    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
721let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
722  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
723
724(** val joint_step_inv_rect_Type2 :
725    unserialized_params -> AST.ident List.list -> joint_step ->
726    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
727    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
728    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
729let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
730  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
731
732(** val joint_step_inv_rect_Type1 :
733    unserialized_params -> AST.ident List.list -> joint_step ->
734    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
735    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
736    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
737let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
738  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
739
740(** val joint_step_inv_rect_Type0 :
741    unserialized_params -> AST.ident List.list -> joint_step ->
742    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
743    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
744    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
745let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
746  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
747
748(** val joint_step_discr :
749    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
750    __ **)
751let joint_step_discr a1 a2 x y =
752  Logic.eq_rect_Type2 x
753    (match x with
754     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
755     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
756     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
757     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
758
759(** val joint_step_jmdiscr :
760    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
761    __ **)
762let joint_step_jmdiscr a1 a2 x y =
763  Logic.eq_rect_Type2 x
764    (match x with
765     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
766     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
767     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
768     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
769
770(** val step_labels :
771    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
772    List.list **)
773let step_labels p globals = function
774| COST_LABEL x -> List.Nil
775| CALL (x, x0, x1) -> List.Nil
776| COND (x, l) -> List.Cons (l, List.Nil)
777| Step_seq s0 ->
778  (match s0 with
779   | COMMENT x -> List.Nil
780   | MOVE x -> List.Nil
781   | POP x -> List.Nil
782   | PUSH x -> List.Nil
783   | ADDRESS (x, x1, x2) -> List.Nil
784   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
785   | OP1 (x, x0, x1) -> List.Nil
786   | OP2 (x, x0, x1, x2) -> List.Nil
787   | CLEAR_CARRY -> List.Nil
788   | SET_CARRY -> List.Nil
789   | LOAD (x, x0, x1) -> List.Nil
790   | STORE (x, x0, x1) -> List.Nil
791   | Extension_seq ext -> p.ext_seq_labels ext)
792
793type stmt_params = { uns_pars : unserialized_params;
794                     succ_label : (__ -> Graphs.label Types.option);
795                     has_fcond : Bool.bool }
796
797(** val stmt_params_rect_Type4 :
798    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
799    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
800let rec stmt_params_rect_Type4 h_mk_stmt_params x_7062 =
801  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
802    has_fcond0 } = x_7062
803  in
804  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
805
806(** val stmt_params_rect_Type5 :
807    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
808    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
809let rec stmt_params_rect_Type5 h_mk_stmt_params x_7064 =
810  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
811    has_fcond0 } = x_7064
812  in
813  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
814
815(** val stmt_params_rect_Type3 :
816    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
817    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
818let rec stmt_params_rect_Type3 h_mk_stmt_params x_7066 =
819  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
820    has_fcond0 } = x_7066
821  in
822  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
823
824(** val stmt_params_rect_Type2 :
825    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
826    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
827let rec stmt_params_rect_Type2 h_mk_stmt_params x_7068 =
828  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
829    has_fcond0 } = x_7068
830  in
831  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
832
833(** val stmt_params_rect_Type1 :
834    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
835    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
836let rec stmt_params_rect_Type1 h_mk_stmt_params x_7070 =
837  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
838    has_fcond0 } = x_7070
839  in
840  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
841
842(** val stmt_params_rect_Type0 :
843    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
844    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
845let rec stmt_params_rect_Type0 h_mk_stmt_params x_7072 =
846  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
847    has_fcond0 } = x_7072
848  in
849  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
850
851(** val uns_pars : stmt_params -> unserialized_params **)
852let rec uns_pars xxx =
853  xxx.uns_pars
854
855type succ0 = __
856
857(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
858let rec succ_label xxx =
859  xxx.succ_label
860
861(** val has_fcond : stmt_params -> Bool.bool **)
862let rec has_fcond xxx =
863  xxx.has_fcond
864
865(** val stmt_params_inv_rect_Type4 :
866    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
867    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
868let stmt_params_inv_rect_Type4 hterm h1 =
869  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
870
871(** val stmt_params_inv_rect_Type3 :
872    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
873    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
874let stmt_params_inv_rect_Type3 hterm h1 =
875  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
876
877(** val stmt_params_inv_rect_Type2 :
878    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
879    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
880let stmt_params_inv_rect_Type2 hterm h1 =
881  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
882
883(** val stmt_params_inv_rect_Type1 :
884    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
885    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
886let stmt_params_inv_rect_Type1 hterm h1 =
887  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
888
889(** val stmt_params_inv_rect_Type0 :
890    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
891    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
892let stmt_params_inv_rect_Type0 hterm h1 =
893  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
894
895(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
896let stmt_params_jmdiscr x y =
897  Logic.eq_rect_Type2 x
898    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
899    Obj.magic (fun _ dH -> dH __ __ __ __)) y
900
901type joint_fin_step =
902| GOTO of Graphs.label
903| RETURN
904| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
905
906(** val joint_fin_step_rect_Type4 :
907    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
908    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
909let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
910| GOTO x_7096 -> h_GOTO x_7096
911| RETURN -> h_RETURN
912| TAILCALL (x_7098, x_7097) -> h_TAILCALL __ x_7098 x_7097
913
914(** val joint_fin_step_rect_Type5 :
915    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
916    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
917let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
918| GOTO x_7104 -> h_GOTO x_7104
919| RETURN -> h_RETURN
920| TAILCALL (x_7106, x_7105) -> h_TAILCALL __ x_7106 x_7105
921
922(** val joint_fin_step_rect_Type3 :
923    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
924    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
925let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
926| GOTO x_7112 -> h_GOTO x_7112
927| RETURN -> h_RETURN
928| TAILCALL (x_7114, x_7113) -> h_TAILCALL __ x_7114 x_7113
929
930(** val joint_fin_step_rect_Type2 :
931    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
932    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
933let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
934| GOTO x_7120 -> h_GOTO x_7120
935| RETURN -> h_RETURN
936| TAILCALL (x_7122, x_7121) -> h_TAILCALL __ x_7122 x_7121
937
938(** val joint_fin_step_rect_Type1 :
939    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
940    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
941let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
942| GOTO x_7128 -> h_GOTO x_7128
943| RETURN -> h_RETURN
944| TAILCALL (x_7130, x_7129) -> h_TAILCALL __ x_7130 x_7129
945
946(** val joint_fin_step_rect_Type0 :
947    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
948    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
949let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
950| GOTO x_7136 -> h_GOTO x_7136
951| RETURN -> h_RETURN
952| TAILCALL (x_7138, x_7137) -> h_TAILCALL __ x_7138 x_7137
953
954(** val joint_fin_step_inv_rect_Type4 :
955    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
956    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
957    __ -> 'a1) -> 'a1 **)
958let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
959  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
960
961(** val joint_fin_step_inv_rect_Type3 :
962    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
963    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
964    __ -> 'a1) -> 'a1 **)
965let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
966  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
967
968(** val joint_fin_step_inv_rect_Type2 :
969    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
970    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
971    __ -> 'a1) -> 'a1 **)
972let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
973  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
974
975(** val joint_fin_step_inv_rect_Type1 :
976    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
977    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
978    __ -> 'a1) -> 'a1 **)
979let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
980  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
981
982(** val joint_fin_step_inv_rect_Type0 :
983    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
984    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
985    __ -> 'a1) -> 'a1 **)
986let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
987  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
988
989(** val joint_fin_step_discr :
990    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
991let joint_fin_step_discr a1 x y =
992  Logic.eq_rect_Type2 x
993    (match x with
994     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
995     | RETURN -> Obj.magic (fun _ dH -> dH)
996     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
997
998(** val joint_fin_step_jmdiscr :
999    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1000let joint_fin_step_jmdiscr a1 x y =
1001  Logic.eq_rect_Type2 x
1002    (match x with
1003     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1004     | RETURN -> Obj.magic (fun _ dH -> dH)
1005     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1006
1007(** val fin_step_labels :
1008    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1009let fin_step_labels p = function
1010| GOTO l -> List.Cons (l, List.Nil)
1011| RETURN -> List.Nil
1012| TAILCALL (x0, x1) -> List.Nil
1013
1014type joint_statement =
1015| Sequential of joint_step * __
1016| Final of joint_fin_step
1017| FCOND of __ * Graphs.label * Graphs.label
1018
1019(** val joint_statement_rect_Type4 :
1020    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1021    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1022    'a1) -> joint_statement -> 'a1 **)
1023let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1024| Sequential (x_7204, x_7203) -> h_sequential x_7204 x_7203
1025| Final x_7205 -> h_final x_7205
1026| FCOND (x_7208, x_7207, x_7206) -> h_FCOND __ x_7208 x_7207 x_7206
1027
1028(** val joint_statement_rect_Type5 :
1029    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1030    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1031    'a1) -> joint_statement -> 'a1 **)
1032let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1033| Sequential (x_7215, x_7214) -> h_sequential x_7215 x_7214
1034| Final x_7216 -> h_final x_7216
1035| FCOND (x_7219, x_7218, x_7217) -> h_FCOND __ x_7219 x_7218 x_7217
1036
1037(** val joint_statement_rect_Type3 :
1038    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1039    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1040    'a1) -> joint_statement -> 'a1 **)
1041let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1042| Sequential (x_7226, x_7225) -> h_sequential x_7226 x_7225
1043| Final x_7227 -> h_final x_7227
1044| FCOND (x_7230, x_7229, x_7228) -> h_FCOND __ x_7230 x_7229 x_7228
1045
1046(** val joint_statement_rect_Type2 :
1047    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1048    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1049    'a1) -> joint_statement -> 'a1 **)
1050let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1051| Sequential (x_7237, x_7236) -> h_sequential x_7237 x_7236
1052| Final x_7238 -> h_final x_7238
1053| FCOND (x_7241, x_7240, x_7239) -> h_FCOND __ x_7241 x_7240 x_7239
1054
1055(** val joint_statement_rect_Type1 :
1056    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1057    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1058    'a1) -> joint_statement -> 'a1 **)
1059let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1060| Sequential (x_7248, x_7247) -> h_sequential x_7248 x_7247
1061| Final x_7249 -> h_final x_7249
1062| FCOND (x_7252, x_7251, x_7250) -> h_FCOND __ x_7252 x_7251 x_7250
1063
1064(** val joint_statement_rect_Type0 :
1065    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1066    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1067    'a1) -> joint_statement -> 'a1 **)
1068let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1069| Sequential (x_7259, x_7258) -> h_sequential x_7259 x_7258
1070| Final x_7260 -> h_final x_7260
1071| FCOND (x_7263, x_7262, x_7261) -> h_FCOND __ x_7263 x_7262 x_7261
1072
1073(** val joint_statement_inv_rect_Type4 :
1074    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1075    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1076    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1077let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1078  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1079
1080(** val joint_statement_inv_rect_Type3 :
1081    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1082    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1083    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1084let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1085  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1086
1087(** val joint_statement_inv_rect_Type2 :
1088    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1089    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1090    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1091let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1092  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1093
1094(** val joint_statement_inv_rect_Type1 :
1095    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1096    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1097    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1098let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1099  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1100
1101(** val joint_statement_inv_rect_Type0 :
1102    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1103    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1104    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1105let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1106  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1107
1108(** val joint_statement_discr :
1109    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1110    -> __ **)
1111let joint_statement_discr a1 a2 x y =
1112  Logic.eq_rect_Type2 x
1113    (match x with
1114     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1115     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1116     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1117
1118(** val joint_statement_jmdiscr :
1119    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1120    -> __ **)
1121let joint_statement_jmdiscr a1 a2 x y =
1122  Logic.eq_rect_Type2 x
1123    (match x with
1124     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1125     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1126     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1127
1128type params = { stmt_pars : stmt_params;
1129                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1130                          Types.option);
1131                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1132                                 -> __ Types.option);
1133                point_of_succ : (__ -> __ -> __) }
1134
1135(** val params_rect_Type4 :
1136    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1137    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1138    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1139    'a1 **)
1140let rec params_rect_Type4 h_mk_params x_7336 =
1141  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1142    point_of_label0; point_of_succ = point_of_succ0 } = x_7336
1143  in
1144  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1145
1146(** val params_rect_Type5 :
1147    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1148    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1149    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1150    'a1 **)
1151let rec params_rect_Type5 h_mk_params x_7338 =
1152  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1153    point_of_label0; point_of_succ = point_of_succ0 } = x_7338
1154  in
1155  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1156
1157(** val params_rect_Type3 :
1158    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1159    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1160    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1161    'a1 **)
1162let rec params_rect_Type3 h_mk_params x_7340 =
1163  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1164    point_of_label0; point_of_succ = point_of_succ0 } = x_7340
1165  in
1166  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1167
1168(** val params_rect_Type2 :
1169    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1170    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1171    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1172    'a1 **)
1173let rec params_rect_Type2 h_mk_params x_7342 =
1174  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1175    point_of_label0; point_of_succ = point_of_succ0 } = x_7342
1176  in
1177  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1178
1179(** val params_rect_Type1 :
1180    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1181    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1182    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1183    'a1 **)
1184let rec params_rect_Type1 h_mk_params x_7344 =
1185  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1186    point_of_label0; point_of_succ = point_of_succ0 } = x_7344
1187  in
1188  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1189
1190(** val params_rect_Type0 :
1191    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1192    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1193    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1194    'a1 **)
1195let rec params_rect_Type0 h_mk_params x_7346 =
1196  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1197    point_of_label0; point_of_succ = point_of_succ0 } = x_7346
1198  in
1199  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1200
1201(** val stmt_pars : params -> stmt_params **)
1202let rec stmt_pars xxx =
1203  xxx.stmt_pars
1204
1205type codeT = __
1206
1207type code_point = __
1208
1209(** val stmt_at :
1210    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1211let rec stmt_at xxx =
1212  xxx.stmt_at
1213
1214(** val point_of_label :
1215    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1216let rec point_of_label xxx =
1217  xxx.point_of_label
1218
1219(** val point_of_succ : params -> __ -> __ -> __ **)
1220let rec point_of_succ xxx =
1221  xxx.point_of_succ
1222
1223(** val params_inv_rect_Type4 :
1224    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1225    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1226    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1227let params_inv_rect_Type4 hterm h1 =
1228  let hcut = params_rect_Type4 h1 hterm in hcut __
1229
1230(** val params_inv_rect_Type3 :
1231    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1232    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1233    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1234let params_inv_rect_Type3 hterm h1 =
1235  let hcut = params_rect_Type3 h1 hterm in hcut __
1236
1237(** val params_inv_rect_Type2 :
1238    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1239    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1240    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1241let params_inv_rect_Type2 hterm h1 =
1242  let hcut = params_rect_Type2 h1 hterm in hcut __
1243
1244(** val params_inv_rect_Type1 :
1245    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1246    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1247    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1248let params_inv_rect_Type1 hterm h1 =
1249  let hcut = params_rect_Type1 h1 hterm in hcut __
1250
1251(** val params_inv_rect_Type0 :
1252    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1253    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1254    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1255let params_inv_rect_Type0 hterm h1 =
1256  let hcut = params_rect_Type0 h1 hterm in hcut __
1257
1258(** val params_jmdiscr : params -> params -> __ **)
1259let params_jmdiscr x y =
1260  Logic.eq_rect_Type2 x
1261    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1262       a5 } = x
1263     in
1264    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1265
1266(** val stmt_pars__o__uns_pars : params -> unserialized_params **)
1267let stmt_pars__o__uns_pars x0 =
1268  x0.stmt_pars.uns_pars
1269
1270(** val code_has_point :
1271    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1272let code_has_point p globals c pt =
1273  match p.stmt_at globals c pt with
1274  | Types.None -> Bool.False
1275  | Types.Some x -> Bool.True
1276
1277(** val code_has_label :
1278    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1279let code_has_label p globals c l =
1280  match p.point_of_label globals c l with
1281  | Types.None -> Bool.False
1282  | Types.Some pt -> code_has_point p globals c pt
1283
1284(** val stmt_explicit_labels :
1285    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1286    List.list **)
1287let stmt_explicit_labels p globals = function
1288| Sequential (c, x) -> step_labels p.uns_pars globals c
1289| Final c -> fin_step_labels p.uns_pars c
1290| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1291
1292(** val stmt_implicit_label :
1293    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1294    Types.option **)
1295let stmt_implicit_label p globals = function
1296| Sequential (x, s0) -> p.succ_label s0
1297| Final x -> Types.None
1298| FCOND (x0, x1, x2) -> Types.None
1299
1300(** val stmt_labels :
1301    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1302    List.list **)
1303let stmt_labels p g0 stmt =
1304  List.append
1305    (match stmt_implicit_label p g0 stmt with
1306     | Types.None -> List.Nil
1307     | Types.Some l -> List.Cons (l, List.Nil))
1308    (stmt_explicit_labels p g0 stmt)
1309
1310type lin_params =
1311  unserialized_params
1312  (* singleton inductive, whose constructor was mk_lin_params *)
1313
1314(** val lin_params_rect_Type4 :
1315    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1316let rec lin_params_rect_Type4 h_mk_lin_params x_7369 =
1317  let l_u_pars = x_7369 in h_mk_lin_params l_u_pars
1318
1319(** val lin_params_rect_Type5 :
1320    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1321let rec lin_params_rect_Type5 h_mk_lin_params x_7371 =
1322  let l_u_pars = x_7371 in h_mk_lin_params l_u_pars
1323
1324(** val lin_params_rect_Type3 :
1325    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1326let rec lin_params_rect_Type3 h_mk_lin_params x_7373 =
1327  let l_u_pars = x_7373 in h_mk_lin_params l_u_pars
1328
1329(** val lin_params_rect_Type2 :
1330    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1331let rec lin_params_rect_Type2 h_mk_lin_params x_7375 =
1332  let l_u_pars = x_7375 in h_mk_lin_params l_u_pars
1333
1334(** val lin_params_rect_Type1 :
1335    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1336let rec lin_params_rect_Type1 h_mk_lin_params x_7377 =
1337  let l_u_pars = x_7377 in h_mk_lin_params l_u_pars
1338
1339(** val lin_params_rect_Type0 :
1340    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1341let rec lin_params_rect_Type0 h_mk_lin_params x_7379 =
1342  let l_u_pars = x_7379 in h_mk_lin_params l_u_pars
1343
1344(** val l_u_pars : lin_params -> unserialized_params **)
1345let rec l_u_pars xxx =
1346  let yyy = xxx in yyy
1347
1348(** val lin_params_inv_rect_Type4 :
1349    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1350let lin_params_inv_rect_Type4 hterm h1 =
1351  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
1352
1353(** val lin_params_inv_rect_Type3 :
1354    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1355let lin_params_inv_rect_Type3 hterm h1 =
1356  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
1357
1358(** val lin_params_inv_rect_Type2 :
1359    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1360let lin_params_inv_rect_Type2 hterm h1 =
1361  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
1362
1363(** val lin_params_inv_rect_Type1 :
1364    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1365let lin_params_inv_rect_Type1 hterm h1 =
1366  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
1367
1368(** val lin_params_inv_rect_Type0 :
1369    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1370let lin_params_inv_rect_Type0 hterm h1 =
1371  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
1372
1373(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
1374let lin_params_jmdiscr x y =
1375  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1376
1377(** val lin_params_to_params : lin_params -> params **)
1378let lin_params_to_params lp =
1379  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
1380    Types.None); has_fcond = Bool.True }; stmt_at =
1381    (fun globals code point ->
1382    Obj.magic
1383      (Monad.m_bind0 (Monad.max_def Option.option0)
1384        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
1385        (fun ls ->
1386        Monad.m_return0 (Monad.max_def Option.option0) ls.Types.snd)));
1387    point_of_label = (fun globals c lbl ->
1388    Util.if_then_else_safe
1389      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
1390        (Obj.magic c)) (fun _ ->
1391      Obj.magic
1392        (Monad.m_return0 (Monad.max_def Option.option0)
1393          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
1394            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
1395    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
1396
1397type graph_params =
1398  unserialized_params
1399  (* singleton inductive, whose constructor was mk_graph_params *)
1400
1401(** val graph_params_rect_Type4 :
1402    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1403let rec graph_params_rect_Type4 h_mk_graph_params x_7395 =
1404  let g_u_pars = x_7395 in h_mk_graph_params g_u_pars
1405
1406(** val graph_params_rect_Type5 :
1407    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1408let rec graph_params_rect_Type5 h_mk_graph_params x_7397 =
1409  let g_u_pars = x_7397 in h_mk_graph_params g_u_pars
1410
1411(** val graph_params_rect_Type3 :
1412    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1413let rec graph_params_rect_Type3 h_mk_graph_params x_7399 =
1414  let g_u_pars = x_7399 in h_mk_graph_params g_u_pars
1415
1416(** val graph_params_rect_Type2 :
1417    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1418let rec graph_params_rect_Type2 h_mk_graph_params x_7401 =
1419  let g_u_pars = x_7401 in h_mk_graph_params g_u_pars
1420
1421(** val graph_params_rect_Type1 :
1422    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1423let rec graph_params_rect_Type1 h_mk_graph_params x_7403 =
1424  let g_u_pars = x_7403 in h_mk_graph_params g_u_pars
1425
1426(** val graph_params_rect_Type0 :
1427    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1428let rec graph_params_rect_Type0 h_mk_graph_params x_7405 =
1429  let g_u_pars = x_7405 in h_mk_graph_params g_u_pars
1430
1431(** val g_u_pars : graph_params -> unserialized_params **)
1432let rec g_u_pars xxx =
1433  let yyy = xxx in yyy
1434
1435(** val graph_params_inv_rect_Type4 :
1436    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1437let graph_params_inv_rect_Type4 hterm h1 =
1438  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
1439
1440(** val graph_params_inv_rect_Type3 :
1441    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1442let graph_params_inv_rect_Type3 hterm h1 =
1443  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
1444
1445(** val graph_params_inv_rect_Type2 :
1446    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1447let graph_params_inv_rect_Type2 hterm h1 =
1448  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
1449
1450(** val graph_params_inv_rect_Type1 :
1451    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1452let graph_params_inv_rect_Type1 hterm h1 =
1453  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
1454
1455(** val graph_params_inv_rect_Type0 :
1456    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1457let graph_params_inv_rect_Type0 hterm h1 =
1458  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
1459
1460(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
1461let graph_params_jmdiscr x y =
1462  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1463
1464(** val graph_params_to_params : graph_params -> params **)
1465let graph_params_to_params gp =
1466  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
1467    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
1468    (fun globals code ->
1469    Obj.magic (Identifiers.lookup0 PreIdentifiers.LabelTag (Obj.magic code)));
1470    point_of_label = (fun x x0 lbl ->
1471    Obj.magic (Monad.m_return0 (Monad.max_def Option.option0) lbl));
1472    point_of_succ = (fun x lbl -> lbl) }
1473
1474type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1475                                 joint_if_runiverse : Identifiers.universe;
1476                                 joint_if_result : __; joint_if_params : 
1477                                 __; joint_if_stacksize : Nat.nat;
1478                                 joint_if_code : __;
1479                                 joint_if_entry : __ Types.sig0 }
1480
1481(** val joint_internal_function_rect_Type4 :
1482    params -> AST.ident List.list -> (Identifiers.universe ->
1483    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1484    'a1) -> joint_internal_function -> 'a1 **)
1485let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_7421 =
1486  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1487    joint_if_runiverse0; joint_if_result = joint_if_result0;
1488    joint_if_params = joint_if_params0; joint_if_stacksize =
1489    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1490    joint_if_entry0 } = x_7421
1491  in
1492  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1493    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1494    joint_if_entry0
1495
1496(** val joint_internal_function_rect_Type5 :
1497    params -> AST.ident List.list -> (Identifiers.universe ->
1498    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1499    'a1) -> joint_internal_function -> 'a1 **)
1500let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_7423 =
1501  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1502    joint_if_runiverse0; joint_if_result = joint_if_result0;
1503    joint_if_params = joint_if_params0; joint_if_stacksize =
1504    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1505    joint_if_entry0 } = x_7423
1506  in
1507  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1508    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1509    joint_if_entry0
1510
1511(** val joint_internal_function_rect_Type3 :
1512    params -> AST.ident List.list -> (Identifiers.universe ->
1513    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1514    'a1) -> joint_internal_function -> 'a1 **)
1515let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_7425 =
1516  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1517    joint_if_runiverse0; joint_if_result = joint_if_result0;
1518    joint_if_params = joint_if_params0; joint_if_stacksize =
1519    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1520    joint_if_entry0 } = x_7425
1521  in
1522  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1523    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1524    joint_if_entry0
1525
1526(** val joint_internal_function_rect_Type2 :
1527    params -> AST.ident List.list -> (Identifiers.universe ->
1528    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1529    'a1) -> joint_internal_function -> 'a1 **)
1530let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_7427 =
1531  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1532    joint_if_runiverse0; joint_if_result = joint_if_result0;
1533    joint_if_params = joint_if_params0; joint_if_stacksize =
1534    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1535    joint_if_entry0 } = x_7427
1536  in
1537  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1538    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1539    joint_if_entry0
1540
1541(** val joint_internal_function_rect_Type1 :
1542    params -> AST.ident List.list -> (Identifiers.universe ->
1543    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1544    'a1) -> joint_internal_function -> 'a1 **)
1545let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_7429 =
1546  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1547    joint_if_runiverse0; joint_if_result = joint_if_result0;
1548    joint_if_params = joint_if_params0; joint_if_stacksize =
1549    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1550    joint_if_entry0 } = x_7429
1551  in
1552  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1553    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1554    joint_if_entry0
1555
1556(** val joint_internal_function_rect_Type0 :
1557    params -> AST.ident List.list -> (Identifiers.universe ->
1558    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1559    'a1) -> joint_internal_function -> 'a1 **)
1560let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_7431 =
1561  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1562    joint_if_runiverse0; joint_if_result = joint_if_result0;
1563    joint_if_params = joint_if_params0; joint_if_stacksize =
1564    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1565    joint_if_entry0 } = x_7431
1566  in
1567  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1568    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1569    joint_if_entry0
1570
1571(** val joint_if_luniverse :
1572    params -> AST.ident List.list -> joint_internal_function ->
1573    Identifiers.universe **)
1574let rec joint_if_luniverse p globals xxx =
1575  xxx.joint_if_luniverse
1576
1577(** val joint_if_runiverse :
1578    params -> AST.ident List.list -> joint_internal_function ->
1579    Identifiers.universe **)
1580let rec joint_if_runiverse p globals xxx =
1581  xxx.joint_if_runiverse
1582
1583(** val joint_if_result :
1584    params -> AST.ident List.list -> joint_internal_function -> __ **)
1585let rec joint_if_result p globals xxx =
1586  xxx.joint_if_result
1587
1588(** val joint_if_params :
1589    params -> AST.ident List.list -> joint_internal_function -> __ **)
1590let rec joint_if_params p globals xxx =
1591  xxx.joint_if_params
1592
1593(** val joint_if_stacksize :
1594    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
1595let rec joint_if_stacksize p globals xxx =
1596  xxx.joint_if_stacksize
1597
1598(** val joint_if_code :
1599    params -> AST.ident List.list -> joint_internal_function -> __ **)
1600let rec joint_if_code p globals xxx =
1601  xxx.joint_if_code
1602
1603(** val joint_if_entry :
1604    params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0 **)
1605let rec joint_if_entry p globals xxx =
1606  xxx.joint_if_entry
1607
1608(** val joint_internal_function_inv_rect_Type4 :
1609    params -> AST.ident List.list -> joint_internal_function ->
1610    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1611    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1612let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
1613  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
1614
1615(** val joint_internal_function_inv_rect_Type3 :
1616    params -> AST.ident List.list -> joint_internal_function ->
1617    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1618    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1619let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
1620  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
1621
1622(** val joint_internal_function_inv_rect_Type2 :
1623    params -> AST.ident List.list -> joint_internal_function ->
1624    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1625    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1626let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
1627  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
1628
1629(** val joint_internal_function_inv_rect_Type1 :
1630    params -> AST.ident List.list -> joint_internal_function ->
1631    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1632    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1633let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
1634  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
1635
1636(** val joint_internal_function_inv_rect_Type0 :
1637    params -> AST.ident List.list -> joint_internal_function ->
1638    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1639    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1640let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
1641  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
1642
1643(** val joint_internal_function_jmdiscr :
1644    params -> AST.ident List.list -> joint_internal_function ->
1645    joint_internal_function -> __ **)
1646let joint_internal_function_jmdiscr a1 a2 x y =
1647  Logic.eq_rect_Type2 x
1648    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
1649       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
1650       joint_if_code = a5; joint_if_entry = a6 } = x
1651     in
1652    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1653
1654(** val good_if_rect_Type4 :
1655    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1656    __ -> __ -> 'a1) -> 'a1 **)
1657let rec good_if_rect_Type4 p globals def h_mk_good_if =
1658  h_mk_good_if __ __ __ __
1659
1660(** val good_if_rect_Type5 :
1661    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1662    __ -> __ -> 'a1) -> 'a1 **)
1663let rec good_if_rect_Type5 p globals def h_mk_good_if =
1664  h_mk_good_if __ __ __ __
1665
1666(** val good_if_rect_Type3 :
1667    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1668    __ -> __ -> 'a1) -> 'a1 **)
1669let rec good_if_rect_Type3 p globals def h_mk_good_if =
1670  h_mk_good_if __ __ __ __
1671
1672(** val good_if_rect_Type2 :
1673    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1674    __ -> __ -> 'a1) -> 'a1 **)
1675let rec good_if_rect_Type2 p globals def h_mk_good_if =
1676  h_mk_good_if __ __ __ __
1677
1678(** val good_if_rect_Type1 :
1679    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1680    __ -> __ -> 'a1) -> 'a1 **)
1681let rec good_if_rect_Type1 p globals def h_mk_good_if =
1682  h_mk_good_if __ __ __ __
1683
1684(** val good_if_rect_Type0 :
1685    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1686    __ -> __ -> 'a1) -> 'a1 **)
1687let rec good_if_rect_Type0 p globals def h_mk_good_if =
1688  h_mk_good_if __ __ __ __
1689
1690(** val good_if_inv_rect_Type4 :
1691    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1692    __ -> __ -> __ -> 'a1) -> 'a1 **)
1693let good_if_inv_rect_Type4 x1 x2 x3 h1 =
1694  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
1695
1696(** val good_if_inv_rect_Type3 :
1697    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1698    __ -> __ -> __ -> 'a1) -> 'a1 **)
1699let good_if_inv_rect_Type3 x1 x2 x3 h1 =
1700  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
1701
1702(** val good_if_inv_rect_Type2 :
1703    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1704    __ -> __ -> __ -> 'a1) -> 'a1 **)
1705let good_if_inv_rect_Type2 x1 x2 x3 h1 =
1706  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
1707
1708(** val good_if_inv_rect_Type1 :
1709    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1710    __ -> __ -> __ -> 'a1) -> 'a1 **)
1711let good_if_inv_rect_Type1 x1 x2 x3 h1 =
1712  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
1713
1714(** val good_if_inv_rect_Type0 :
1715    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1716    __ -> __ -> __ -> 'a1) -> 'a1 **)
1717let good_if_inv_rect_Type0 x1 x2 x3 h1 =
1718  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
1719
1720(** val good_if_discr :
1721    params -> AST.ident List.list -> joint_internal_function -> __ **)
1722let good_if_discr a1 a2 a3 =
1723  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1724
1725(** val good_if_jmdiscr :
1726    params -> AST.ident List.list -> joint_internal_function -> __ **)
1727let good_if_jmdiscr a1 a2 a3 =
1728  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1729
1730type joint_closed_internal_function = joint_internal_function Types.sig0
1731
1732(** val set_joint_code :
1733    AST.ident List.list -> params -> joint_internal_function -> __ -> __
1734    Types.sig0 -> joint_internal_function **)
1735let set_joint_code globals pars int_fun graph0 entry =
1736  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
1737    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
1738    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
1739    int_fun.joint_if_stacksize; joint_if_code = graph0; joint_if_entry =
1740    entry }
1741
1742(** val set_joint_if_graph :
1743    AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
1744    joint_internal_function **)
1745let set_joint_if_graph globals pars graph0 p =
1746  set_joint_code globals (graph_params_to_params pars) p graph0
1747    (Types.pi1 p.joint_if_entry)
1748
1749(** val set_luniverse :
1750    params -> AST.ident List.list -> joint_internal_function ->
1751    Identifiers.universe -> joint_internal_function **)
1752let set_luniverse globals pars p luniverse =
1753  { joint_if_luniverse = luniverse; joint_if_runiverse =
1754    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
1755    joint_if_params = p.joint_if_params; joint_if_stacksize =
1756    p.joint_if_stacksize; joint_if_code = p.joint_if_code; joint_if_entry =
1757    p.joint_if_entry }
1758
1759(** val set_runiverse :
1760    params -> AST.ident List.list -> joint_internal_function ->
1761    Identifiers.universe -> joint_internal_function **)
1762let set_runiverse globals pars p runiverse =
1763  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
1764    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
1765    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
1766    joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry }
1767
1768(** val add_graph :
1769    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1770    joint_internal_function -> joint_internal_function **)
1771let add_graph g_pars globals l stmt p =
1772  let code =
1773    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
1774      stmt
1775  in
1776  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
1777  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
1778  joint_if_params = p.joint_if_params; joint_if_stacksize =
1779  p.joint_if_stacksize; joint_if_code = (Obj.magic code); joint_if_entry =
1780  (Types.pi1 p.joint_if_entry) }
1781
1782type joint_function = joint_closed_internal_function AST.fundef
1783
1784type joint_program = (joint_function, Nat.nat) AST.program
1785
1786let lp_to_p__o__stmt_pars _ = assert false
Note: See TracBrowser for help on using the repository browser.