source: extracted/joint.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 73.0 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_16310 -> h_Reg x_16310
113| Imm x_16311 -> h_Imm x_16311
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_16315 -> h_Reg x_16315
119| Imm x_16316 -> h_Imm x_16316
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_16320 -> h_Reg x_16320
125| Imm x_16321 -> h_Imm x_16321
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_16325 -> h_Reg x_16325
131| Imm x_16326 -> h_Imm x_16326
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_16330 -> h_Reg x_16330
137| Imm x_16331 -> h_Imm x_16331
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_16335 -> h_Reg x_16335
143| Imm x_16336 -> h_Imm x_16336
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_16371 =
227  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
228    x_16371
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_16373 =
238  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
239    x_16373
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_16375 =
249  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
250    x_16375
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_16377 =
260  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
261    x_16377
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_16379 =
271  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
272    x_16379
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_16381 =
282  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
283    x_16381
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_16437 -> h_COMMENT x_16437
392| MOVE x_16438 -> h_MOVE x_16438
393| POP x_16439 -> h_POP x_16439
394| PUSH x_16440 -> h_PUSH x_16440
395| ADDRESS (i, x_16442, x_16441) -> h_ADDRESS i __ x_16442 x_16441
396| OPACCS (x_16448, x_16447, x_16446, x_16445, x_16444) ->
397  h_OPACCS x_16448 x_16447 x_16446 x_16445 x_16444
398| OP1 (x_16451, x_16450, x_16449) -> h_OP1 x_16451 x_16450 x_16449
399| OP2 (x_16455, x_16454, x_16453, x_16452) ->
400  h_OP2 x_16455 x_16454 x_16453 x_16452
401| CLEAR_CARRY -> h_CLEAR_CARRY
402| SET_CARRY -> h_SET_CARRY
403| LOAD (x_16458, x_16457, x_16456) -> h_LOAD x_16458 x_16457 x_16456
404| STORE (x_16461, x_16460, x_16459) -> h_STORE x_16461 x_16460 x_16459
405| Extension_seq x_16462 -> h_extension_seq x_16462
406
407(** val joint_seq_rect_Type5 :
408    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
409    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
410    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
411    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
412    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
413    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
414let 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
415| COMMENT x_16477 -> h_COMMENT x_16477
416| MOVE x_16478 -> h_MOVE x_16478
417| POP x_16479 -> h_POP x_16479
418| PUSH x_16480 -> h_PUSH x_16480
419| ADDRESS (i, x_16482, x_16481) -> h_ADDRESS i __ x_16482 x_16481
420| OPACCS (x_16488, x_16487, x_16486, x_16485, x_16484) ->
421  h_OPACCS x_16488 x_16487 x_16486 x_16485 x_16484
422| OP1 (x_16491, x_16490, x_16489) -> h_OP1 x_16491 x_16490 x_16489
423| OP2 (x_16495, x_16494, x_16493, x_16492) ->
424  h_OP2 x_16495 x_16494 x_16493 x_16492
425| CLEAR_CARRY -> h_CLEAR_CARRY
426| SET_CARRY -> h_SET_CARRY
427| LOAD (x_16498, x_16497, x_16496) -> h_LOAD x_16498 x_16497 x_16496
428| STORE (x_16501, x_16500, x_16499) -> h_STORE x_16501 x_16500 x_16499
429| Extension_seq x_16502 -> h_extension_seq x_16502
430
431(** val joint_seq_rect_Type3 :
432    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
433    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
434    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
435    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
436    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
437    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
438let 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
439| COMMENT x_16517 -> h_COMMENT x_16517
440| MOVE x_16518 -> h_MOVE x_16518
441| POP x_16519 -> h_POP x_16519
442| PUSH x_16520 -> h_PUSH x_16520
443| ADDRESS (i, x_16522, x_16521) -> h_ADDRESS i __ x_16522 x_16521
444| OPACCS (x_16528, x_16527, x_16526, x_16525, x_16524) ->
445  h_OPACCS x_16528 x_16527 x_16526 x_16525 x_16524
446| OP1 (x_16531, x_16530, x_16529) -> h_OP1 x_16531 x_16530 x_16529
447| OP2 (x_16535, x_16534, x_16533, x_16532) ->
448  h_OP2 x_16535 x_16534 x_16533 x_16532
449| CLEAR_CARRY -> h_CLEAR_CARRY
450| SET_CARRY -> h_SET_CARRY
451| LOAD (x_16538, x_16537, x_16536) -> h_LOAD x_16538 x_16537 x_16536
452| STORE (x_16541, x_16540, x_16539) -> h_STORE x_16541 x_16540 x_16539
453| Extension_seq x_16542 -> h_extension_seq x_16542
454
455(** val joint_seq_rect_Type2 :
456    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
457    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
458    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
459    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
460    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
461    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
462let 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
463| COMMENT x_16557 -> h_COMMENT x_16557
464| MOVE x_16558 -> h_MOVE x_16558
465| POP x_16559 -> h_POP x_16559
466| PUSH x_16560 -> h_PUSH x_16560
467| ADDRESS (i, x_16562, x_16561) -> h_ADDRESS i __ x_16562 x_16561
468| OPACCS (x_16568, x_16567, x_16566, x_16565, x_16564) ->
469  h_OPACCS x_16568 x_16567 x_16566 x_16565 x_16564
470| OP1 (x_16571, x_16570, x_16569) -> h_OP1 x_16571 x_16570 x_16569
471| OP2 (x_16575, x_16574, x_16573, x_16572) ->
472  h_OP2 x_16575 x_16574 x_16573 x_16572
473| CLEAR_CARRY -> h_CLEAR_CARRY
474| SET_CARRY -> h_SET_CARRY
475| LOAD (x_16578, x_16577, x_16576) -> h_LOAD x_16578 x_16577 x_16576
476| STORE (x_16581, x_16580, x_16579) -> h_STORE x_16581 x_16580 x_16579
477| Extension_seq x_16582 -> h_extension_seq x_16582
478
479(** val joint_seq_rect_Type1 :
480    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
481    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
482    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
483    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
484    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
485    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
486let 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
487| COMMENT x_16597 -> h_COMMENT x_16597
488| MOVE x_16598 -> h_MOVE x_16598
489| POP x_16599 -> h_POP x_16599
490| PUSH x_16600 -> h_PUSH x_16600
491| ADDRESS (i, x_16602, x_16601) -> h_ADDRESS i __ x_16602 x_16601
492| OPACCS (x_16608, x_16607, x_16606, x_16605, x_16604) ->
493  h_OPACCS x_16608 x_16607 x_16606 x_16605 x_16604
494| OP1 (x_16611, x_16610, x_16609) -> h_OP1 x_16611 x_16610 x_16609
495| OP2 (x_16615, x_16614, x_16613, x_16612) ->
496  h_OP2 x_16615 x_16614 x_16613 x_16612
497| CLEAR_CARRY -> h_CLEAR_CARRY
498| SET_CARRY -> h_SET_CARRY
499| LOAD (x_16618, x_16617, x_16616) -> h_LOAD x_16618 x_16617 x_16616
500| STORE (x_16621, x_16620, x_16619) -> h_STORE x_16621 x_16620 x_16619
501| Extension_seq x_16622 -> h_extension_seq x_16622
502
503(** val joint_seq_rect_Type0 :
504    unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
505    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __
506    -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
507    (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
508    -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
509    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
510let 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
511| COMMENT x_16637 -> h_COMMENT x_16637
512| MOVE x_16638 -> h_MOVE x_16638
513| POP x_16639 -> h_POP x_16639
514| PUSH x_16640 -> h_PUSH x_16640
515| ADDRESS (i, x_16642, x_16641) -> h_ADDRESS i __ x_16642 x_16641
516| OPACCS (x_16648, x_16647, x_16646, x_16645, x_16644) ->
517  h_OPACCS x_16648 x_16647 x_16646 x_16645 x_16644
518| OP1 (x_16651, x_16650, x_16649) -> h_OP1 x_16651 x_16650 x_16649
519| OP2 (x_16655, x_16654, x_16653, x_16652) ->
520  h_OP2 x_16655 x_16654 x_16653 x_16652
521| CLEAR_CARRY -> h_CLEAR_CARRY
522| SET_CARRY -> h_SET_CARRY
523| LOAD (x_16658, x_16657, x_16656) -> h_LOAD x_16658 x_16657 x_16656
524| STORE (x_16661, x_16660, x_16659) -> h_STORE x_16661 x_16660 x_16659
525| Extension_seq x_16662 -> h_extension_seq x_16662
526
527(** val joint_seq_inv_rect_Type4 :
528    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
529    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
530    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
531    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
532    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
533    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
534    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
535let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
536  let hcut =
537    joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
538      hterm
539  in
540  hcut __
541
542(** val joint_seq_inv_rect_Type3 :
543    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
544    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
545    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
546    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
547    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
548    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
549    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
550let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
551  let hcut =
552    joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
553      hterm
554  in
555  hcut __
556
557(** val joint_seq_inv_rect_Type2 :
558    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
559    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
560    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
561    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
562    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
563    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
564    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
565let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
566  let hcut =
567    joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
568      hterm
569  in
570  hcut __
571
572(** val joint_seq_inv_rect_Type1 :
573    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
574    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
575    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
576    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
577    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
578    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
579    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
580let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
581  let hcut =
582    joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
583      hterm
584  in
585  hcut __
586
587(** val joint_seq_inv_rect_Type0 :
588    unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
589    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
590    'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs
591    -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ ->
592    __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ ->
593    'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __
594    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
595let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
596  let hcut =
597    joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
598      hterm
599  in
600  hcut __
601
602(** val joint_seq_discr :
603    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
604    __ **)
605let joint_seq_discr a1 a2 x y =
606  Logic.eq_rect_Type2 x
607    (match x with
608     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
609     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
610     | POP a0 -> Obj.magic (fun _ dH -> dH __)
611     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
612     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
613     | OPACCS (a0, a10, a20, a3, a4) ->
614       Obj.magic (fun _ dH -> dH __ __ __ __ __)
615     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
616     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
617     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
618     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
619     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
620     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
621     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
622
623(** val joint_seq_jmdiscr :
624    unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
625    __ **)
626let joint_seq_jmdiscr a1 a2 x y =
627  Logic.eq_rect_Type2 x
628    (match x with
629     | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
630     | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
631     | POP a0 -> Obj.magic (fun _ dH -> dH __)
632     | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
633     | ADDRESS (a0, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
634     | OPACCS (a0, a10, a20, a3, a4) ->
635       Obj.magic (fun _ dH -> dH __ __ __ __ __)
636     | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
637     | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
638     | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
639     | SET_CARRY -> Obj.magic (fun _ dH -> dH)
640     | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
641     | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
642     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
643
644(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
645let nOOP p globals =
646  COMMENT String.EmptyString
647
648type joint_step =
649| COST_LABEL of CostLabel.costlabel
650| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
651| COND of __ * Graphs.label
652| Step_seq of joint_seq
653
654(** val joint_step_rect_Type4 :
655    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
656    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
657    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
658let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
659| COST_LABEL x_16929 -> h_COST_LABEL x_16929
660| CALL (x_16932, x_16931, x_16930) -> h_CALL x_16932 x_16931 x_16930
661| COND (x_16934, x_16933) -> h_COND x_16934 x_16933
662| Step_seq x_16935 -> h_step_seq x_16935
663
664(** val joint_step_rect_Type5 :
665    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
666    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
667    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
668let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
669| COST_LABEL x_16941 -> h_COST_LABEL x_16941
670| CALL (x_16944, x_16943, x_16942) -> h_CALL x_16944 x_16943 x_16942
671| COND (x_16946, x_16945) -> h_COND x_16946 x_16945
672| Step_seq x_16947 -> h_step_seq x_16947
673
674(** val joint_step_rect_Type3 :
675    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
676    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
677    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
678let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
679| COST_LABEL x_16953 -> h_COST_LABEL x_16953
680| CALL (x_16956, x_16955, x_16954) -> h_CALL x_16956 x_16955 x_16954
681| COND (x_16958, x_16957) -> h_COND x_16958 x_16957
682| Step_seq x_16959 -> h_step_seq x_16959
683
684(** val joint_step_rect_Type2 :
685    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
686    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
687    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
688let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
689| COST_LABEL x_16965 -> h_COST_LABEL x_16965
690| CALL (x_16968, x_16967, x_16966) -> h_CALL x_16968 x_16967 x_16966
691| COND (x_16970, x_16969) -> h_COND x_16970 x_16969
692| Step_seq x_16971 -> h_step_seq x_16971
693
694(** val joint_step_rect_Type1 :
695    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
696    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
697    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
698let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
699| COST_LABEL x_16977 -> h_COST_LABEL x_16977
700| CALL (x_16980, x_16979, x_16978) -> h_CALL x_16980 x_16979 x_16978
701| COND (x_16982, x_16981) -> h_COND x_16982 x_16981
702| Step_seq x_16983 -> h_step_seq x_16983
703
704(** val joint_step_rect_Type0 :
705    unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
706    'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
707    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
708let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
709| COST_LABEL x_16989 -> h_COST_LABEL x_16989
710| CALL (x_16992, x_16991, x_16990) -> h_CALL x_16992 x_16991 x_16990
711| COND (x_16994, x_16993) -> h_COND x_16994 x_16993
712| Step_seq x_16995 -> h_step_seq x_16995
713
714(** val joint_step_inv_rect_Type4 :
715    unserialized_params -> AST.ident List.list -> joint_step ->
716    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
717    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
718    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
719let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
720  let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
721
722(** val joint_step_inv_rect_Type3 :
723    unserialized_params -> AST.ident List.list -> joint_step ->
724    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
725    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
726    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
727let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
728  let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
729
730(** val joint_step_inv_rect_Type2 :
731    unserialized_params -> AST.ident List.list -> joint_step ->
732    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
733    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
734    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
735let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
736  let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
737
738(** val joint_step_inv_rect_Type1 :
739    unserialized_params -> AST.ident List.list -> joint_step ->
740    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
741    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
742    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
743let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
744  let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
745
746(** val joint_step_inv_rect_Type0 :
747    unserialized_params -> AST.ident List.list -> joint_step ->
748    (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
749    Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
750    -> (joint_seq -> __ -> 'a1) -> 'a1 **)
751let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
752  let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
753
754(** val joint_step_discr :
755    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
756    __ **)
757let joint_step_discr a1 a2 x y =
758  Logic.eq_rect_Type2 x
759    (match x with
760     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
761     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
762     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
763     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
764
765(** val joint_step_jmdiscr :
766    unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
767    __ **)
768let joint_step_jmdiscr a1 a2 x y =
769  Logic.eq_rect_Type2 x
770    (match x with
771     | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
772     | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
773     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
774     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
775
776(** val step_labels :
777    unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
778    List.list **)
779let step_labels p globals = function
780| COST_LABEL x -> List.Nil
781| CALL (x, x0, x1) -> List.Nil
782| COND (x, l) -> List.Cons (l, List.Nil)
783| Step_seq s0 ->
784  (match s0 with
785   | COMMENT x -> List.Nil
786   | MOVE x -> List.Nil
787   | POP x -> List.Nil
788   | PUSH x -> List.Nil
789   | ADDRESS (x, x1, x2) -> List.Nil
790   | OPACCS (x, x0, x1, x2, x3) -> List.Nil
791   | OP1 (x, x0, x1) -> List.Nil
792   | OP2 (x, x0, x1, x2) -> List.Nil
793   | CLEAR_CARRY -> List.Nil
794   | SET_CARRY -> List.Nil
795   | LOAD (x, x0, x1) -> List.Nil
796   | STORE (x, x0, x1) -> List.Nil
797   | Extension_seq ext -> p.ext_seq_labels ext)
798
799type stmt_params = { uns_pars : unserialized_params;
800                     succ_label : (__ -> Graphs.label Types.option);
801                     has_fcond : Bool.bool }
802
803(** val stmt_params_rect_Type4 :
804    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
805    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
806let rec stmt_params_rect_Type4 h_mk_stmt_params x_17074 =
807  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
808    has_fcond0 } = x_17074
809  in
810  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
811
812(** val stmt_params_rect_Type5 :
813    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
814    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
815let rec stmt_params_rect_Type5 h_mk_stmt_params x_17076 =
816  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
817    has_fcond0 } = x_17076
818  in
819  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
820
821(** val stmt_params_rect_Type3 :
822    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
823    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
824let rec stmt_params_rect_Type3 h_mk_stmt_params x_17078 =
825  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
826    has_fcond0 } = x_17078
827  in
828  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
829
830(** val stmt_params_rect_Type2 :
831    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
832    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
833let rec stmt_params_rect_Type2 h_mk_stmt_params x_17080 =
834  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
835    has_fcond0 } = x_17080
836  in
837  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
838
839(** val stmt_params_rect_Type1 :
840    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
841    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
842let rec stmt_params_rect_Type1 h_mk_stmt_params x_17082 =
843  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
844    has_fcond0 } = x_17082
845  in
846  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
847
848(** val stmt_params_rect_Type0 :
849    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
850    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
851let rec stmt_params_rect_Type0 h_mk_stmt_params x_17084 =
852  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
853    has_fcond0 } = x_17084
854  in
855  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
856
857(** val uns_pars : stmt_params -> unserialized_params **)
858let rec uns_pars xxx =
859  xxx.uns_pars
860
861type succ0 = __
862
863(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
864let rec succ_label xxx =
865  xxx.succ_label
866
867(** val has_fcond : stmt_params -> Bool.bool **)
868let rec has_fcond xxx =
869  xxx.has_fcond
870
871(** val stmt_params_inv_rect_Type4 :
872    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
873    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
874let stmt_params_inv_rect_Type4 hterm h1 =
875  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
876
877(** val stmt_params_inv_rect_Type3 :
878    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
879    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
880let stmt_params_inv_rect_Type3 hterm h1 =
881  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
882
883(** val stmt_params_inv_rect_Type2 :
884    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
885    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
886let stmt_params_inv_rect_Type2 hterm h1 =
887  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
888
889(** val stmt_params_inv_rect_Type1 :
890    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
891    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
892let stmt_params_inv_rect_Type1 hterm h1 =
893  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
894
895(** val stmt_params_inv_rect_Type0 :
896    stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
897    Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
898let stmt_params_inv_rect_Type0 hterm h1 =
899  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
900
901(** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
902let stmt_params_jmdiscr x y =
903  Logic.eq_rect_Type2 x
904    (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
905    Obj.magic (fun _ dH -> dH __ __ __ __)) y
906
907type joint_fin_step =
908| GOTO of Graphs.label
909| RETURN
910| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
911
912(** val joint_fin_step_rect_Type4 :
913    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
914    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
915let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
916| GOTO x_17108 -> h_GOTO x_17108
917| RETURN -> h_RETURN
918| TAILCALL (x_17110, x_17109) -> h_TAILCALL __ x_17110 x_17109
919
920(** val joint_fin_step_rect_Type5 :
921    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
922    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
923let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
924| GOTO x_17116 -> h_GOTO x_17116
925| RETURN -> h_RETURN
926| TAILCALL (x_17118, x_17117) -> h_TAILCALL __ x_17118 x_17117
927
928(** val joint_fin_step_rect_Type3 :
929    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
930    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
931let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
932| GOTO x_17124 -> h_GOTO x_17124
933| RETURN -> h_RETURN
934| TAILCALL (x_17126, x_17125) -> h_TAILCALL __ x_17126 x_17125
935
936(** val joint_fin_step_rect_Type2 :
937    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
938    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
939let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
940| GOTO x_17132 -> h_GOTO x_17132
941| RETURN -> h_RETURN
942| TAILCALL (x_17134, x_17133) -> h_TAILCALL __ x_17134 x_17133
943
944(** val joint_fin_step_rect_Type1 :
945    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
946    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
947let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
948| GOTO x_17140 -> h_GOTO x_17140
949| RETURN -> h_RETURN
950| TAILCALL (x_17142, x_17141) -> h_TAILCALL __ x_17142 x_17141
951
952(** val joint_fin_step_rect_Type0 :
953    unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
954    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
955let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
956| GOTO x_17148 -> h_GOTO x_17148
957| RETURN -> h_RETURN
958| TAILCALL (x_17150, x_17149) -> h_TAILCALL __ x_17150 x_17149
959
960(** val joint_fin_step_inv_rect_Type4 :
961    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
962    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
963    __ -> 'a1) -> 'a1 **)
964let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
965  let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
966
967(** val joint_fin_step_inv_rect_Type3 :
968    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
969    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
970    __ -> 'a1) -> 'a1 **)
971let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
972  let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
973
974(** val joint_fin_step_inv_rect_Type2 :
975    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
976    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
977    __ -> 'a1) -> 'a1 **)
978let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
979  let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
980
981(** val joint_fin_step_inv_rect_Type1 :
982    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
983    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
984    __ -> 'a1) -> 'a1 **)
985let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
986  let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
987
988(** val joint_fin_step_inv_rect_Type0 :
989    unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
990    (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
991    __ -> 'a1) -> 'a1 **)
992let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
993  let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
994
995(** val joint_fin_step_discr :
996    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
997let joint_fin_step_discr a1 x y =
998  Logic.eq_rect_Type2 x
999    (match x with
1000     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1001     | RETURN -> Obj.magic (fun _ dH -> dH)
1002     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1003
1004(** val joint_fin_step_jmdiscr :
1005    unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1006let joint_fin_step_jmdiscr a1 x y =
1007  Logic.eq_rect_Type2 x
1008    (match x with
1009     | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1010     | RETURN -> Obj.magic (fun _ dH -> dH)
1011     | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1012
1013(** val fin_step_labels :
1014    unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1015let fin_step_labels p = function
1016| GOTO l -> List.Cons (l, List.Nil)
1017| RETURN -> List.Nil
1018| TAILCALL (x0, x1) -> List.Nil
1019
1020type joint_statement =
1021| Sequential of joint_step * __
1022| Final of joint_fin_step
1023| FCOND of __ * Graphs.label * Graphs.label
1024
1025(** val joint_statement_rect_Type4 :
1026    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1027    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1028    'a1) -> joint_statement -> 'a1 **)
1029let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1030| Sequential (x_17216, x_17215) -> h_sequential x_17216 x_17215
1031| Final x_17217 -> h_final x_17217
1032| FCOND (x_17220, x_17219, x_17218) -> h_FCOND __ x_17220 x_17219 x_17218
1033
1034(** val joint_statement_rect_Type5 :
1035    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1036    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1037    'a1) -> joint_statement -> 'a1 **)
1038let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1039| Sequential (x_17227, x_17226) -> h_sequential x_17227 x_17226
1040| Final x_17228 -> h_final x_17228
1041| FCOND (x_17231, x_17230, x_17229) -> h_FCOND __ x_17231 x_17230 x_17229
1042
1043(** val joint_statement_rect_Type3 :
1044    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1045    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1046    'a1) -> joint_statement -> 'a1 **)
1047let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1048| Sequential (x_17238, x_17237) -> h_sequential x_17238 x_17237
1049| Final x_17239 -> h_final x_17239
1050| FCOND (x_17242, x_17241, x_17240) -> h_FCOND __ x_17242 x_17241 x_17240
1051
1052(** val joint_statement_rect_Type2 :
1053    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1054    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1055    'a1) -> joint_statement -> 'a1 **)
1056let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1057| Sequential (x_17249, x_17248) -> h_sequential x_17249 x_17248
1058| Final x_17250 -> h_final x_17250
1059| FCOND (x_17253, x_17252, x_17251) -> h_FCOND __ x_17253 x_17252 x_17251
1060
1061(** val joint_statement_rect_Type1 :
1062    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1063    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1064    'a1) -> joint_statement -> 'a1 **)
1065let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1066| Sequential (x_17260, x_17259) -> h_sequential x_17260 x_17259
1067| Final x_17261 -> h_final x_17261
1068| FCOND (x_17264, x_17263, x_17262) -> h_FCOND __ x_17264 x_17263 x_17262
1069
1070(** val joint_statement_rect_Type0 :
1071    stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1072    (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1073    'a1) -> joint_statement -> 'a1 **)
1074let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1075| Sequential (x_17271, x_17270) -> h_sequential x_17271 x_17270
1076| Final x_17272 -> h_final x_17272
1077| FCOND (x_17275, x_17274, x_17273) -> h_FCOND __ x_17275 x_17274 x_17273
1078
1079(** val joint_statement_inv_rect_Type4 :
1080    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1081    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1082    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1083let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1084  let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1085
1086(** val joint_statement_inv_rect_Type3 :
1087    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1088    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1089    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1090let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1091  let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1092
1093(** val joint_statement_inv_rect_Type2 :
1094    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1095    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1096    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1097let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1098  let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1099
1100(** val joint_statement_inv_rect_Type1 :
1101    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1102    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1103    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1104let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1105  let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1106
1107(** val joint_statement_inv_rect_Type0 :
1108    stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1109    __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1110    Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1111let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1112  let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1113
1114(** val joint_statement_discr :
1115    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1116    -> __ **)
1117let joint_statement_discr a1 a2 x y =
1118  Logic.eq_rect_Type2 x
1119    (match x with
1120     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1121     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1122     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1123
1124(** val joint_statement_jmdiscr :
1125    stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1126    -> __ **)
1127let joint_statement_jmdiscr a1 a2 x y =
1128  Logic.eq_rect_Type2 x
1129    (match x with
1130     | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1131     | Final a0 -> Obj.magic (fun _ dH -> dH __)
1132     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1133
1134type params = { stmt_pars : stmt_params;
1135                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1136                          Types.option);
1137                point_of_label : (AST.ident List.list -> __ -> Graphs.label
1138                                 -> __ Types.option);
1139                point_of_succ : (__ -> __ -> __) }
1140
1141(** val params_rect_Type4 :
1142    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1143    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1144    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1145    'a1 **)
1146let rec params_rect_Type4 h_mk_params x_17348 =
1147  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1148    point_of_label0; point_of_succ = point_of_succ0 } = x_17348
1149  in
1150  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1151
1152(** val params_rect_Type5 :
1153    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1154    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1155    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1156    'a1 **)
1157let rec params_rect_Type5 h_mk_params x_17350 =
1158  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1159    point_of_label0; point_of_succ = point_of_succ0 } = x_17350
1160  in
1161  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1162
1163(** val params_rect_Type3 :
1164    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1165    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1166    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1167    'a1 **)
1168let rec params_rect_Type3 h_mk_params x_17352 =
1169  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1170    point_of_label0; point_of_succ = point_of_succ0 } = x_17352
1171  in
1172  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1173
1174(** val params_rect_Type2 :
1175    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1176    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1177    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1178    'a1 **)
1179let rec params_rect_Type2 h_mk_params x_17354 =
1180  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1181    point_of_label0; point_of_succ = point_of_succ0 } = x_17354
1182  in
1183  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1184
1185(** val params_rect_Type1 :
1186    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1187    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1188    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1189    'a1 **)
1190let rec params_rect_Type1 h_mk_params x_17356 =
1191  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1192    point_of_label0; point_of_succ = point_of_succ0 } = x_17356
1193  in
1194  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1195
1196(** val params_rect_Type0 :
1197    (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1198    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1199    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1200    'a1 **)
1201let rec params_rect_Type0 h_mk_params x_17358 =
1202  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1203    point_of_label0; point_of_succ = point_of_succ0 } = x_17358
1204  in
1205  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1206
1207(** val stmt_pars : params -> stmt_params **)
1208let rec stmt_pars xxx =
1209  xxx.stmt_pars
1210
1211type codeT = __
1212
1213type code_point = __
1214
1215(** val stmt_at :
1216    params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1217let rec stmt_at xxx =
1218  xxx.stmt_at
1219
1220(** val point_of_label :
1221    params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1222let rec point_of_label xxx =
1223  xxx.point_of_label
1224
1225(** val point_of_succ : params -> __ -> __ -> __ **)
1226let rec point_of_succ xxx =
1227  xxx.point_of_succ
1228
1229(** val params_inv_rect_Type4 :
1230    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1231    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1232    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1233let params_inv_rect_Type4 hterm h1 =
1234  let hcut = params_rect_Type4 h1 hterm in hcut __
1235
1236(** val params_inv_rect_Type3 :
1237    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1238    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1239    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1240let params_inv_rect_Type3 hterm h1 =
1241  let hcut = params_rect_Type3 h1 hterm in hcut __
1242
1243(** val params_inv_rect_Type2 :
1244    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1245    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1246    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1247let params_inv_rect_Type2 hterm h1 =
1248  let hcut = params_rect_Type2 h1 hterm in hcut __
1249
1250(** val params_inv_rect_Type1 :
1251    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1252    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1253    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1254let params_inv_rect_Type1 hterm h1 =
1255  let hcut = params_rect_Type1 h1 hterm in hcut __
1256
1257(** val params_inv_rect_Type0 :
1258    params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1259    joint_statement Types.option) -> (AST.ident List.list -> __ ->
1260    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1261let params_inv_rect_Type0 hterm h1 =
1262  let hcut = params_rect_Type0 h1 hterm in hcut __
1263
1264(** val params_jmdiscr : params -> params -> __ **)
1265let params_jmdiscr x y =
1266  Logic.eq_rect_Type2 x
1267    (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1268       a5 } = x
1269     in
1270    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1271
1272(** val stmt_pars__o__uns_pars : params -> unserialized_params **)
1273let stmt_pars__o__uns_pars x0 =
1274  x0.stmt_pars.uns_pars
1275
1276(** val code_has_point :
1277    params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1278let code_has_point p globals c pt =
1279  match p.stmt_at globals c pt with
1280  | Types.None -> Bool.False
1281  | Types.Some x -> Bool.True
1282
1283(** val code_has_label :
1284    params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1285let code_has_label p globals c l =
1286  match p.point_of_label globals c l with
1287  | Types.None -> Bool.False
1288  | Types.Some pt -> code_has_point p globals c pt
1289
1290(** val stmt_explicit_labels :
1291    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1292    List.list **)
1293let stmt_explicit_labels p globals = function
1294| Sequential (c, x) -> step_labels p.uns_pars globals c
1295| Final c -> fin_step_labels p.uns_pars c
1296| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
1297
1298(** val stmt_implicit_label :
1299    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1300    Types.option **)
1301let stmt_implicit_label p globals = function
1302| Sequential (x, s0) -> p.succ_label s0
1303| Final x -> Types.None
1304| FCOND (x0, x1, x2) -> Types.None
1305
1306(** val stmt_labels :
1307    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1308    List.list **)
1309let stmt_labels p g0 stmt =
1310  List.append
1311    (match stmt_implicit_label p g0 stmt with
1312     | Types.None -> List.Nil
1313     | Types.Some l -> List.Cons (l, List.Nil))
1314    (stmt_explicit_labels p g0 stmt)
1315
1316type lin_params =
1317  unserialized_params
1318  (* singleton inductive, whose constructor was mk_lin_params *)
1319
1320(** val lin_params_rect_Type4 :
1321    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1322let rec lin_params_rect_Type4 h_mk_lin_params x_17381 =
1323  let l_u_pars = x_17381 in h_mk_lin_params l_u_pars
1324
1325(** val lin_params_rect_Type5 :
1326    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1327let rec lin_params_rect_Type5 h_mk_lin_params x_17383 =
1328  let l_u_pars = x_17383 in h_mk_lin_params l_u_pars
1329
1330(** val lin_params_rect_Type3 :
1331    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1332let rec lin_params_rect_Type3 h_mk_lin_params x_17385 =
1333  let l_u_pars = x_17385 in h_mk_lin_params l_u_pars
1334
1335(** val lin_params_rect_Type2 :
1336    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1337let rec lin_params_rect_Type2 h_mk_lin_params x_17387 =
1338  let l_u_pars = x_17387 in h_mk_lin_params l_u_pars
1339
1340(** val lin_params_rect_Type1 :
1341    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1342let rec lin_params_rect_Type1 h_mk_lin_params x_17389 =
1343  let l_u_pars = x_17389 in h_mk_lin_params l_u_pars
1344
1345(** val lin_params_rect_Type0 :
1346    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
1347let rec lin_params_rect_Type0 h_mk_lin_params x_17391 =
1348  let l_u_pars = x_17391 in h_mk_lin_params l_u_pars
1349
1350(** val l_u_pars : lin_params -> unserialized_params **)
1351let rec l_u_pars xxx =
1352  let yyy = xxx in yyy
1353
1354(** val lin_params_inv_rect_Type4 :
1355    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1356let lin_params_inv_rect_Type4 hterm h1 =
1357  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
1358
1359(** val lin_params_inv_rect_Type3 :
1360    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1361let lin_params_inv_rect_Type3 hterm h1 =
1362  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
1363
1364(** val lin_params_inv_rect_Type2 :
1365    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1366let lin_params_inv_rect_Type2 hterm h1 =
1367  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
1368
1369(** val lin_params_inv_rect_Type1 :
1370    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1371let lin_params_inv_rect_Type1 hterm h1 =
1372  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
1373
1374(** val lin_params_inv_rect_Type0 :
1375    lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1376let lin_params_inv_rect_Type0 hterm h1 =
1377  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
1378
1379(** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
1380let lin_params_jmdiscr x y =
1381  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1382
1383(** val lin_params_to_params : lin_params -> params **)
1384let lin_params_to_params lp =
1385  { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
1386    Types.None); has_fcond = Bool.True }; stmt_at =
1387    (fun globals code point ->
1388    Obj.magic
1389      (Monad.m_bind0 (Monad.max_def Option.option0)
1390        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
1391        (fun ls ->
1392        Monad.m_return0 (Monad.max_def Option.option0) ls.Types.snd)));
1393    point_of_label = (fun globals c lbl ->
1394    Util.if_then_else_safe
1395      (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
1396        (Obj.magic c)) (fun _ ->
1397      Obj.magic
1398        (Monad.m_return0 (Monad.max_def Option.option0)
1399          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
1400            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
1401    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
1402
1403type graph_params =
1404  unserialized_params
1405  (* singleton inductive, whose constructor was mk_graph_params *)
1406
1407(** val graph_params_rect_Type4 :
1408    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1409let rec graph_params_rect_Type4 h_mk_graph_params x_17407 =
1410  let g_u_pars = x_17407 in h_mk_graph_params g_u_pars
1411
1412(** val graph_params_rect_Type5 :
1413    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1414let rec graph_params_rect_Type5 h_mk_graph_params x_17409 =
1415  let g_u_pars = x_17409 in h_mk_graph_params g_u_pars
1416
1417(** val graph_params_rect_Type3 :
1418    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1419let rec graph_params_rect_Type3 h_mk_graph_params x_17411 =
1420  let g_u_pars = x_17411 in h_mk_graph_params g_u_pars
1421
1422(** val graph_params_rect_Type2 :
1423    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1424let rec graph_params_rect_Type2 h_mk_graph_params x_17413 =
1425  let g_u_pars = x_17413 in h_mk_graph_params g_u_pars
1426
1427(** val graph_params_rect_Type1 :
1428    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1429let rec graph_params_rect_Type1 h_mk_graph_params x_17415 =
1430  let g_u_pars = x_17415 in h_mk_graph_params g_u_pars
1431
1432(** val graph_params_rect_Type0 :
1433    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
1434let rec graph_params_rect_Type0 h_mk_graph_params x_17417 =
1435  let g_u_pars = x_17417 in h_mk_graph_params g_u_pars
1436
1437(** val g_u_pars : graph_params -> unserialized_params **)
1438let rec g_u_pars xxx =
1439  let yyy = xxx in yyy
1440
1441(** val graph_params_inv_rect_Type4 :
1442    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1443let graph_params_inv_rect_Type4 hterm h1 =
1444  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
1445
1446(** val graph_params_inv_rect_Type3 :
1447    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1448let graph_params_inv_rect_Type3 hterm h1 =
1449  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
1450
1451(** val graph_params_inv_rect_Type2 :
1452    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1453let graph_params_inv_rect_Type2 hterm h1 =
1454  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
1455
1456(** val graph_params_inv_rect_Type1 :
1457    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1458let graph_params_inv_rect_Type1 hterm h1 =
1459  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
1460
1461(** val graph_params_inv_rect_Type0 :
1462    graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
1463let graph_params_inv_rect_Type0 hterm h1 =
1464  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
1465
1466(** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
1467let graph_params_jmdiscr x y =
1468  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
1469
1470(** val graph_params_to_params : graph_params -> params **)
1471let graph_params_to_params gp =
1472  { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
1473    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
1474    (fun globals code ->
1475    Obj.magic (Identifiers.lookup0 PreIdentifiers.LabelTag (Obj.magic code)));
1476    point_of_label = (fun x x0 lbl ->
1477    Obj.magic (Monad.m_return0 (Monad.max_def Option.option0) lbl));
1478    point_of_succ = (fun x lbl -> lbl) }
1479
1480type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1481                                 joint_if_runiverse : Identifiers.universe;
1482                                 joint_if_result : __; joint_if_params : 
1483                                 __; joint_if_stacksize : Nat.nat;
1484                                 joint_if_code : __;
1485                                 joint_if_entry : __ Types.sig0 }
1486
1487(** val joint_internal_function_rect_Type4 :
1488    params -> AST.ident List.list -> (Identifiers.universe ->
1489    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1490    'a1) -> joint_internal_function -> 'a1 **)
1491let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_17433 =
1492  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1493    joint_if_runiverse0; joint_if_result = joint_if_result0;
1494    joint_if_params = joint_if_params0; joint_if_stacksize =
1495    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1496    joint_if_entry0 } = x_17433
1497  in
1498  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1499    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1500    joint_if_entry0
1501
1502(** val joint_internal_function_rect_Type5 :
1503    params -> AST.ident List.list -> (Identifiers.universe ->
1504    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1505    'a1) -> joint_internal_function -> 'a1 **)
1506let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_17435 =
1507  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1508    joint_if_runiverse0; joint_if_result = joint_if_result0;
1509    joint_if_params = joint_if_params0; joint_if_stacksize =
1510    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1511    joint_if_entry0 } = x_17435
1512  in
1513  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1514    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1515    joint_if_entry0
1516
1517(** val joint_internal_function_rect_Type3 :
1518    params -> AST.ident List.list -> (Identifiers.universe ->
1519    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1520    'a1) -> joint_internal_function -> 'a1 **)
1521let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_17437 =
1522  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1523    joint_if_runiverse0; joint_if_result = joint_if_result0;
1524    joint_if_params = joint_if_params0; joint_if_stacksize =
1525    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1526    joint_if_entry0 } = x_17437
1527  in
1528  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1529    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1530    joint_if_entry0
1531
1532(** val joint_internal_function_rect_Type2 :
1533    params -> AST.ident List.list -> (Identifiers.universe ->
1534    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1535    'a1) -> joint_internal_function -> 'a1 **)
1536let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_17439 =
1537  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1538    joint_if_runiverse0; joint_if_result = joint_if_result0;
1539    joint_if_params = joint_if_params0; joint_if_stacksize =
1540    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1541    joint_if_entry0 } = x_17439
1542  in
1543  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1544    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1545    joint_if_entry0
1546
1547(** val joint_internal_function_rect_Type1 :
1548    params -> AST.ident List.list -> (Identifiers.universe ->
1549    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1550    'a1) -> joint_internal_function -> 'a1 **)
1551let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_17441 =
1552  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1553    joint_if_runiverse0; joint_if_result = joint_if_result0;
1554    joint_if_params = joint_if_params0; joint_if_stacksize =
1555    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1556    joint_if_entry0 } = x_17441
1557  in
1558  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1559    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1560    joint_if_entry0
1561
1562(** val joint_internal_function_rect_Type0 :
1563    params -> AST.ident List.list -> (Identifiers.universe ->
1564    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
1565    'a1) -> joint_internal_function -> 'a1 **)
1566let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_17443 =
1567  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
1568    joint_if_runiverse0; joint_if_result = joint_if_result0;
1569    joint_if_params = joint_if_params0; joint_if_stacksize =
1570    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
1571    joint_if_entry0 } = x_17443
1572  in
1573  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
1574    joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_code0
1575    joint_if_entry0
1576
1577(** val joint_if_luniverse :
1578    params -> AST.ident List.list -> joint_internal_function ->
1579    Identifiers.universe **)
1580let rec joint_if_luniverse p globals xxx =
1581  xxx.joint_if_luniverse
1582
1583(** val joint_if_runiverse :
1584    params -> AST.ident List.list -> joint_internal_function ->
1585    Identifiers.universe **)
1586let rec joint_if_runiverse p globals xxx =
1587  xxx.joint_if_runiverse
1588
1589(** val joint_if_result :
1590    params -> AST.ident List.list -> joint_internal_function -> __ **)
1591let rec joint_if_result p globals xxx =
1592  xxx.joint_if_result
1593
1594(** val joint_if_params :
1595    params -> AST.ident List.list -> joint_internal_function -> __ **)
1596let rec joint_if_params p globals xxx =
1597  xxx.joint_if_params
1598
1599(** val joint_if_stacksize :
1600    params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
1601let rec joint_if_stacksize p globals xxx =
1602  xxx.joint_if_stacksize
1603
1604(** val joint_if_code :
1605    params -> AST.ident List.list -> joint_internal_function -> __ **)
1606let rec joint_if_code p globals xxx =
1607  xxx.joint_if_code
1608
1609(** val joint_if_entry :
1610    params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0 **)
1611let rec joint_if_entry p globals xxx =
1612  xxx.joint_if_entry
1613
1614(** val joint_internal_function_inv_rect_Type4 :
1615    params -> AST.ident List.list -> joint_internal_function ->
1616    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1617    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1618let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
1619  let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
1620
1621(** val joint_internal_function_inv_rect_Type3 :
1622    params -> AST.ident List.list -> joint_internal_function ->
1623    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1624    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1625let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
1626  let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
1627
1628(** val joint_internal_function_inv_rect_Type2 :
1629    params -> AST.ident List.list -> joint_internal_function ->
1630    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1631    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1632let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
1633  let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
1634
1635(** val joint_internal_function_inv_rect_Type1 :
1636    params -> AST.ident List.list -> joint_internal_function ->
1637    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1638    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1639let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
1640  let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
1641
1642(** val joint_internal_function_inv_rect_Type0 :
1643    params -> AST.ident List.list -> joint_internal_function ->
1644    (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1645    __ -> __ Types.sig0 -> __ -> 'a1) -> 'a1 **)
1646let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
1647  let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
1648
1649(** val joint_internal_function_jmdiscr :
1650    params -> AST.ident List.list -> joint_internal_function ->
1651    joint_internal_function -> __ **)
1652let joint_internal_function_jmdiscr a1 a2 x y =
1653  Logic.eq_rect_Type2 x
1654    (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
1655       joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
1656       joint_if_code = a5; joint_if_entry = a6 } = x
1657     in
1658    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1659
1660(** val good_if_rect_Type4 :
1661    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1662    __ -> __ -> 'a1) -> 'a1 **)
1663let rec good_if_rect_Type4 p globals def h_mk_good_if =
1664  h_mk_good_if __ __ __ __
1665
1666(** val good_if_rect_Type5 :
1667    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1668    __ -> __ -> 'a1) -> 'a1 **)
1669let rec good_if_rect_Type5 p globals def h_mk_good_if =
1670  h_mk_good_if __ __ __ __
1671
1672(** val good_if_rect_Type3 :
1673    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1674    __ -> __ -> 'a1) -> 'a1 **)
1675let rec good_if_rect_Type3 p globals def h_mk_good_if =
1676  h_mk_good_if __ __ __ __
1677
1678(** val good_if_rect_Type2 :
1679    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1680    __ -> __ -> 'a1) -> 'a1 **)
1681let rec good_if_rect_Type2 p globals def h_mk_good_if =
1682  h_mk_good_if __ __ __ __
1683
1684(** val good_if_rect_Type1 :
1685    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1686    __ -> __ -> 'a1) -> 'a1 **)
1687let rec good_if_rect_Type1 p globals def h_mk_good_if =
1688  h_mk_good_if __ __ __ __
1689
1690(** val good_if_rect_Type0 :
1691    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1692    __ -> __ -> 'a1) -> 'a1 **)
1693let rec good_if_rect_Type0 p globals def h_mk_good_if =
1694  h_mk_good_if __ __ __ __
1695
1696(** val good_if_inv_rect_Type4 :
1697    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1698    __ -> __ -> __ -> 'a1) -> 'a1 **)
1699let good_if_inv_rect_Type4 x1 x2 x3 h1 =
1700  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
1701
1702(** val good_if_inv_rect_Type3 :
1703    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1704    __ -> __ -> __ -> 'a1) -> 'a1 **)
1705let good_if_inv_rect_Type3 x1 x2 x3 h1 =
1706  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
1707
1708(** val good_if_inv_rect_Type2 :
1709    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1710    __ -> __ -> __ -> 'a1) -> 'a1 **)
1711let good_if_inv_rect_Type2 x1 x2 x3 h1 =
1712  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
1713
1714(** val good_if_inv_rect_Type1 :
1715    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1716    __ -> __ -> __ -> 'a1) -> 'a1 **)
1717let good_if_inv_rect_Type1 x1 x2 x3 h1 =
1718  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
1719
1720(** val good_if_inv_rect_Type0 :
1721    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
1722    __ -> __ -> __ -> 'a1) -> 'a1 **)
1723let good_if_inv_rect_Type0 x1 x2 x3 h1 =
1724  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
1725
1726(** val good_if_discr :
1727    params -> AST.ident List.list -> joint_internal_function -> __ **)
1728let good_if_discr a1 a2 a3 =
1729  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1730
1731(** val good_if_jmdiscr :
1732    params -> AST.ident List.list -> joint_internal_function -> __ **)
1733let good_if_jmdiscr a1 a2 a3 =
1734  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
1735
1736type joint_closed_internal_function = joint_internal_function Types.sig0
1737
1738(** val set_joint_code :
1739    AST.ident List.list -> params -> joint_internal_function -> __ -> __
1740    Types.sig0 -> joint_internal_function **)
1741let set_joint_code globals pars int_fun graph0 entry =
1742  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
1743    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
1744    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
1745    int_fun.joint_if_stacksize; joint_if_code = graph0; joint_if_entry =
1746    entry }
1747
1748(** val set_joint_if_graph :
1749    AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
1750    joint_internal_function **)
1751let set_joint_if_graph globals pars graph0 p =
1752  set_joint_code globals (graph_params_to_params pars) p graph0
1753    (Types.pi1 p.joint_if_entry)
1754
1755(** val set_luniverse :
1756    params -> AST.ident List.list -> joint_internal_function ->
1757    Identifiers.universe -> joint_internal_function **)
1758let set_luniverse globals pars p luniverse =
1759  { joint_if_luniverse = luniverse; joint_if_runiverse =
1760    p.joint_if_runiverse; joint_if_result = p.joint_if_result;
1761    joint_if_params = p.joint_if_params; joint_if_stacksize =
1762    p.joint_if_stacksize; joint_if_code = p.joint_if_code; joint_if_entry =
1763    p.joint_if_entry }
1764
1765(** val set_runiverse :
1766    params -> AST.ident List.list -> joint_internal_function ->
1767    Identifiers.universe -> joint_internal_function **)
1768let set_runiverse globals pars p runiverse =
1769  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
1770    runiverse; joint_if_result = p.joint_if_result; joint_if_params =
1771    p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
1772    joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry }
1773
1774(** val add_graph :
1775    graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1776    joint_internal_function -> joint_internal_function **)
1777let add_graph g_pars globals l stmt p =
1778  let code =
1779    Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
1780      stmt
1781  in
1782  { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
1783  p.joint_if_runiverse; joint_if_result = p.joint_if_result;
1784  joint_if_params = p.joint_if_params; joint_if_stacksize =
1785  p.joint_if_stacksize; joint_if_code = (Obj.magic code); joint_if_entry =
1786  (Types.pi1 p.joint_if_entry) }
1787
1788type joint_function = joint_closed_internal_function AST.fundef
1789
1790type joint_program = (joint_function, Nat.nat) AST.program
1791
1792let lp_to_p__o__stmt_pars _ = assert false
Note: See TracBrowser for help on using the repository browser.