65 open Hints_declaration
107 | Imm of BitVector.byte
109 (** val argument_rect_Type4 :
110 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
111 let rec argument_rect_Type4 h_Reg h_Imm = function
112 | Reg x_16867 -> h_Reg x_16867
113 | Imm x_16868 -> h_Imm x_16868
115 (** val argument_rect_Type5 :
116 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
117 let rec argument_rect_Type5 h_Reg h_Imm = function
118 | Reg x_16872 -> h_Reg x_16872
119 | Imm x_16873 -> h_Imm x_16873
121 (** val argument_rect_Type3 :
122 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
123 let rec argument_rect_Type3 h_Reg h_Imm = function
124 | Reg x_16877 -> h_Reg x_16877
125 | Imm x_16878 -> h_Imm x_16878
127 (** val argument_rect_Type2 :
128 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
129 let rec argument_rect_Type2 h_Reg h_Imm = function
130 | Reg x_16882 -> h_Reg x_16882
131 | Imm x_16883 -> h_Imm x_16883
133 (** val argument_rect_Type1 :
134 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
135 let rec argument_rect_Type1 h_Reg h_Imm = function
136 | Reg x_16887 -> h_Reg x_16887
137 | Imm x_16888 -> h_Imm x_16888
139 (** val argument_rect_Type0 :
140 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
141 let rec argument_rect_Type0 h_Reg h_Imm = function
142 | Reg x_16892 -> h_Reg x_16892
143 | Imm x_16893 -> h_Imm x_16893
145 (** val argument_inv_rect_Type4 :
146 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
148 let argument_inv_rect_Type4 hterm h1 h2 =
149 let hcut = argument_rect_Type4 h1 h2 hterm in hcut __
151 (** val argument_inv_rect_Type3 :
152 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
154 let argument_inv_rect_Type3 hterm h1 h2 =
155 let hcut = argument_rect_Type3 h1 h2 hterm in hcut __
157 (** val argument_inv_rect_Type2 :
158 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
160 let argument_inv_rect_Type2 hterm h1 h2 =
161 let hcut = argument_rect_Type2 h1 h2 hterm in hcut __
163 (** val argument_inv_rect_Type1 :
164 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
166 let argument_inv_rect_Type1 hterm h1 h2 =
167 let hcut = argument_rect_Type1 h1 h2 hterm in hcut __
169 (** val argument_inv_rect_Type0 :
170 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
172 let argument_inv_rect_Type0 hterm h1 h2 =
173 let hcut = argument_rect_Type0 h1 h2 hterm in hcut __
175 (** val argument_discr : 'a1 argument -> 'a1 argument -> __ **)
176 let argument_discr x y =
177 Logic.eq_rect_Type2 x
179 | Reg a0 -> Obj.magic (fun _ dH -> dH __)
180 | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
182 (** val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __ **)
183 let argument_jmdiscr x y =
184 Logic.eq_rect_Type2 x
186 | Reg a0 -> Obj.magic (fun _ dH -> dH __)
187 | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
189 type psd_argument = Registers.register argument
191 (** val psd_argument_from_reg : Registers.register -> psd_argument **)
192 let psd_argument_from_reg x =
195 (** val dpi1__o__reg_to_psd_argument__o__inject :
196 (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0 **)
197 let dpi1__o__reg_to_psd_argument__o__inject x2 =
198 psd_argument_from_reg x2.Types.dpi1
200 (** val eject__o__reg_to_psd_argument__o__inject :
201 Registers.register Types.sig0 -> psd_argument Types.sig0 **)
202 let eject__o__reg_to_psd_argument__o__inject x2 =
203 psd_argument_from_reg (Types.pi1 x2)
205 (** val reg_to_psd_argument__o__inject :
206 Registers.register -> psd_argument Types.sig0 **)
207 let reg_to_psd_argument__o__inject x1 =
208 psd_argument_from_reg x1
210 (** val dpi1__o__reg_to_psd_argument :
211 (Registers.register, 'a1) Types.dPair -> psd_argument **)
212 let dpi1__o__reg_to_psd_argument x1 =
213 psd_argument_from_reg x1.Types.dpi1
215 (** val eject__o__reg_to_psd_argument :
216 Registers.register Types.sig0 -> psd_argument **)
217 let eject__o__reg_to_psd_argument x1 =
218 psd_argument_from_reg (Types.pi1 x1)
220 (** val psd_argument_from_byte : BitVector.byte -> psd_argument **)
221 let psd_argument_from_byte x =
224 (** val dpi1__o__byte_to_psd_argument__o__inject :
225 (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
226 let dpi1__o__byte_to_psd_argument__o__inject x2 =
227 psd_argument_from_byte x2.Types.dpi1
229 (** val eject__o__byte_to_psd_argument__o__inject :
230 BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
231 let eject__o__byte_to_psd_argument__o__inject x2 =
232 psd_argument_from_byte (Types.pi1 x2)
234 (** val byte_to_psd_argument__o__inject :
235 BitVector.byte -> psd_argument Types.sig0 **)
236 let byte_to_psd_argument__o__inject x1 =
237 psd_argument_from_byte x1
239 (** val dpi1__o__byte_to_psd_argument :
240 (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
241 let dpi1__o__byte_to_psd_argument x1 =
242 psd_argument_from_byte x1.Types.dpi1
244 (** val eject__o__byte_to_psd_argument :
245 BitVector.byte Types.sig0 -> psd_argument **)
246 let eject__o__byte_to_psd_argument x1 =
247 psd_argument_from_byte (Types.pi1 x1)
249 type hdw_argument = I8051.register argument
251 (** val hdw_argument_from_reg : I8051.register -> hdw_argument **)
252 let hdw_argument_from_reg x =
255 (** val dpi1__o__reg_to_hdw_argument__o__inject :
256 (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0 **)
257 let dpi1__o__reg_to_hdw_argument__o__inject x2 =
258 hdw_argument_from_reg x2.Types.dpi1
260 (** val eject__o__reg_to_hdw_argument__o__inject :
261 I8051.register Types.sig0 -> hdw_argument Types.sig0 **)
262 let eject__o__reg_to_hdw_argument__o__inject x2 =
263 hdw_argument_from_reg (Types.pi1 x2)
265 (** val reg_to_hdw_argument__o__inject :
266 I8051.register -> hdw_argument Types.sig0 **)
267 let reg_to_hdw_argument__o__inject x1 =
268 hdw_argument_from_reg x1
270 (** val dpi1__o__reg_to_hdw_argument :
271 (I8051.register, 'a1) Types.dPair -> hdw_argument **)
272 let dpi1__o__reg_to_hdw_argument x1 =
273 hdw_argument_from_reg x1.Types.dpi1
275 (** val eject__o__reg_to_hdw_argument :
276 I8051.register Types.sig0 -> hdw_argument **)
277 let eject__o__reg_to_hdw_argument x1 =
278 hdw_argument_from_reg (Types.pi1 x1)
280 (** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **)
281 let hdw_argument_from_byte x =
284 (** val dpi1__o__byte_to_hdw_argument__o__inject :
285 (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
286 let dpi1__o__byte_to_hdw_argument__o__inject x2 =
287 psd_argument_from_byte x2.Types.dpi1
289 (** val eject__o__byte_to_hdw_argument__o__inject :
290 BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
291 let eject__o__byte_to_hdw_argument__o__inject x2 =
292 psd_argument_from_byte (Types.pi1 x2)
294 (** val byte_to_hdw_argument__o__inject :
295 BitVector.byte -> psd_argument Types.sig0 **)
296 let byte_to_hdw_argument__o__inject x1 =
297 psd_argument_from_byte x1
299 (** val dpi1__o__byte_to_hdw_argument :
300 (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
301 let dpi1__o__byte_to_hdw_argument x1 =
302 psd_argument_from_byte x1.Types.dpi1
304 (** val eject__o__byte_to_hdw_argument :
305 BitVector.byte Types.sig0 -> psd_argument **)
306 let eject__o__byte_to_hdw_argument x1 =
307 psd_argument_from_byte (Types.pi1 x1)
309 (** val byte_of_nat : Nat.nat -> BitVector.byte **)
311 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
312 (Nat.S (Nat.S Nat.O))))))))
314 (** val zero_byte : BitVector.byte **)
316 BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
319 type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
320 has_tailcalls : Bool.bool }
322 (** val unserialized_params_rect_Type4 :
323 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
324 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
325 unserialized_params -> 'a1 **)
326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16928 =
327 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
330 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
331 ext_seq_labels0 has_tailcalls0 __
333 (** val unserialized_params_rect_Type5 :
334 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
335 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
336 unserialized_params -> 'a1 **)
337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16930 =
338 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
341 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
342 ext_seq_labels0 has_tailcalls0 __
344 (** val unserialized_params_rect_Type3 :
345 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
346 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
347 unserialized_params -> 'a1 **)
348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16932 =
349 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
352 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
353 ext_seq_labels0 has_tailcalls0 __
355 (** val unserialized_params_rect_Type2 :
356 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
357 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
358 unserialized_params -> 'a1 **)
359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16934 =
360 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
363 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
364 ext_seq_labels0 has_tailcalls0 __
366 (** val unserialized_params_rect_Type1 :
367 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
368 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
369 unserialized_params -> 'a1 **)
370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16936 =
371 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
374 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
375 ext_seq_labels0 has_tailcalls0 __
377 (** val unserialized_params_rect_Type0 :
378 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
379 __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
380 unserialized_params -> 'a1 **)
381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16938 =
382 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
385 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
386 ext_seq_labels0 has_tailcalls0 __
414 (** val ext_seq_labels :
415 unserialized_params -> __ -> Graphs.label List.list **)
416 let rec ext_seq_labels xxx =
419 (** val has_tailcalls : unserialized_params -> Bool.bool **)
420 let rec has_tailcalls xxx =
425 (** val unserialized_params_inv_rect_Type4 :
426 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
427 __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
428 -> __ -> __ -> 'a1) -> 'a1 **)
429 let unserialized_params_inv_rect_Type4 hterm h1 =
430 let hcut = unserialized_params_rect_Type4 h1 hterm in hcut __
432 (** val unserialized_params_inv_rect_Type3 :
433 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
434 __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
435 -> __ -> __ -> 'a1) -> 'a1 **)
436 let unserialized_params_inv_rect_Type3 hterm h1 =
437 let hcut = unserialized_params_rect_Type3 h1 hterm in hcut __
439 (** val unserialized_params_inv_rect_Type2 :
440 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
441 __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
442 -> __ -> __ -> 'a1) -> 'a1 **)
443 let unserialized_params_inv_rect_Type2 hterm h1 =
444 let hcut = unserialized_params_rect_Type2 h1 hterm in hcut __
446 (** val unserialized_params_inv_rect_Type1 :
447 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
448 __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
449 -> __ -> __ -> 'a1) -> 'a1 **)
450 let unserialized_params_inv_rect_Type1 hterm h1 =
451 let hcut = unserialized_params_rect_Type1 h1 hterm in hcut __
453 (** val unserialized_params_inv_rect_Type0 :
454 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
455 __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
456 -> __ -> __ -> 'a1) -> 'a1 **)
457 let unserialized_params_inv_rect_Type0 hterm h1 =
458 let hcut = unserialized_params_rect_Type0 h1 hterm in hcut __
460 (** val unserialized_params_jmdiscr :
461 unserialized_params -> unserialized_params -> __ **)
462 let unserialized_params_jmdiscr x y =
463 Logic.eq_rect_Type2 x
464 (let { ext_seq_labels = a13; has_tailcalls = a14 } = x in
465 Obj.magic (fun _ dH ->
466 dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
468 type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
470 acc_b_regs : (__ -> Registers.register
472 acc_a_args : (__ -> Registers.register
474 acc_b_args : (__ -> Registers.register
476 dpl_regs : (__ -> Registers.register
478 dph_regs : (__ -> Registers.register
480 dpl_args : (__ -> Registers.register
482 dph_args : (__ -> Registers.register
484 snd_args : (__ -> Registers.register
486 pair_move_regs : (__ -> Registers.register
488 f_call_args : (__ -> Registers.register
490 f_call_dest : (__ -> Registers.register
492 ext_seq_regs : (__ -> Registers.register
494 params_regs : (__ -> Registers.register
497 (** val get_pseudo_reg_functs_rect_Type4 :
498 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
499 Registers.register List.list) -> (__ -> Registers.register List.list) ->
500 (__ -> Registers.register List.list) -> (__ -> Registers.register
501 List.list) -> (__ -> Registers.register List.list) -> (__ ->
502 Registers.register List.list) -> (__ -> Registers.register List.list) ->
503 (__ -> Registers.register List.list) -> (__ -> Registers.register
504 List.list) -> (__ -> Registers.register List.list) -> (__ ->
505 Registers.register List.list) -> (__ -> Registers.register List.list) ->
506 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_16955 =
509 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
510 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
511 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
512 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
513 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
514 params_regs0 } = x_16955
516 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
517 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
518 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
520 (** val get_pseudo_reg_functs_rect_Type5 :
521 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
522 Registers.register List.list) -> (__ -> Registers.register List.list) ->
523 (__ -> Registers.register List.list) -> (__ -> Registers.register
524 List.list) -> (__ -> Registers.register List.list) -> (__ ->
525 Registers.register List.list) -> (__ -> Registers.register List.list) ->
526 (__ -> Registers.register List.list) -> (__ -> Registers.register
527 List.list) -> (__ -> Registers.register List.list) -> (__ ->
528 Registers.register List.list) -> (__ -> Registers.register List.list) ->
529 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_16957 =
532 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
533 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
534 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
535 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
536 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
537 params_regs0 } = x_16957
539 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
540 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
541 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
543 (** val get_pseudo_reg_functs_rect_Type3 :
544 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
545 Registers.register List.list) -> (__ -> Registers.register List.list) ->
546 (__ -> Registers.register List.list) -> (__ -> Registers.register
547 List.list) -> (__ -> Registers.register List.list) -> (__ ->
548 Registers.register List.list) -> (__ -> Registers.register List.list) ->
549 (__ -> Registers.register List.list) -> (__ -> Registers.register
550 List.list) -> (__ -> Registers.register List.list) -> (__ ->
551 Registers.register List.list) -> (__ -> Registers.register List.list) ->
552 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_16959 =
555 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
556 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
557 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
558 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
559 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
560 params_regs0 } = x_16959
562 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
563 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
564 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
566 (** val get_pseudo_reg_functs_rect_Type2 :
567 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
568 Registers.register List.list) -> (__ -> Registers.register List.list) ->
569 (__ -> Registers.register List.list) -> (__ -> Registers.register
570 List.list) -> (__ -> Registers.register List.list) -> (__ ->
571 Registers.register List.list) -> (__ -> Registers.register List.list) ->
572 (__ -> Registers.register List.list) -> (__ -> Registers.register
573 List.list) -> (__ -> Registers.register List.list) -> (__ ->
574 Registers.register List.list) -> (__ -> Registers.register List.list) ->
575 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_16961 =
578 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
579 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
580 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
581 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
582 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
583 params_regs0 } = x_16961
585 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
586 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
587 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
589 (** val get_pseudo_reg_functs_rect_Type1 :
590 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
591 Registers.register List.list) -> (__ -> Registers.register List.list) ->
592 (__ -> Registers.register List.list) -> (__ -> Registers.register
593 List.list) -> (__ -> Registers.register List.list) -> (__ ->
594 Registers.register List.list) -> (__ -> Registers.register List.list) ->
595 (__ -> Registers.register List.list) -> (__ -> Registers.register
596 List.list) -> (__ -> Registers.register List.list) -> (__ ->
597 Registers.register List.list) -> (__ -> Registers.register List.list) ->
598 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_16963 =
601 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
602 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
603 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
604 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
605 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
606 params_regs0 } = x_16963
608 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
609 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
610 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
612 (** val get_pseudo_reg_functs_rect_Type0 :
613 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
614 Registers.register List.list) -> (__ -> Registers.register List.list) ->
615 (__ -> Registers.register List.list) -> (__ -> Registers.register
616 List.list) -> (__ -> Registers.register List.list) -> (__ ->
617 Registers.register List.list) -> (__ -> Registers.register List.list) ->
618 (__ -> Registers.register List.list) -> (__ -> Registers.register
619 List.list) -> (__ -> Registers.register List.list) -> (__ ->
620 Registers.register List.list) -> (__ -> Registers.register List.list) ->
621 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_16965 =
624 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
625 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
626 dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
627 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
628 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
629 params_regs0 } = x_16965
631 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
632 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
633 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
636 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
638 let rec acc_a_regs p xxx =
642 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
644 let rec acc_b_regs p xxx =
648 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
650 let rec acc_a_args p xxx =
654 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
656 let rec acc_b_args p xxx =
660 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
662 let rec dpl_regs p xxx =
666 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
668 let rec dph_regs p xxx =
672 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
674 let rec dpl_args p xxx =
678 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
680 let rec dph_args p xxx =
684 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
686 let rec snd_args p xxx =
689 (** val pair_move_regs :
690 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
692 let rec pair_move_regs p xxx =
695 (** val f_call_args :
696 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
698 let rec f_call_args p xxx =
701 (** val f_call_dest :
702 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
704 let rec f_call_dest p xxx =
707 (** val ext_seq_regs :
708 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
710 let rec ext_seq_regs p xxx =
713 (** val params_regs :
714 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
716 let rec params_regs p xxx =
719 (** val get_pseudo_reg_functs_inv_rect_Type4 :
720 unserialized_params -> get_pseudo_reg_functs -> ((__ ->
721 Registers.register List.list) -> (__ -> Registers.register List.list) ->
722 (__ -> Registers.register List.list) -> (__ -> Registers.register
723 List.list) -> (__ -> Registers.register List.list) -> (__ ->
724 Registers.register List.list) -> (__ -> Registers.register List.list) ->
725 (__ -> Registers.register List.list) -> (__ -> Registers.register
726 List.list) -> (__ -> Registers.register List.list) -> (__ ->
727 Registers.register List.list) -> (__ -> Registers.register List.list) ->
728 (__ -> Registers.register List.list) -> (__ -> Registers.register
729 List.list) -> __ -> 'a1) -> 'a1 **)
730 let get_pseudo_reg_functs_inv_rect_Type4 x1 hterm h1 =
731 let hcut = get_pseudo_reg_functs_rect_Type4 x1 h1 hterm in hcut __
733 (** val get_pseudo_reg_functs_inv_rect_Type3 :
734 unserialized_params -> get_pseudo_reg_functs -> ((__ ->
735 Registers.register List.list) -> (__ -> Registers.register List.list) ->
736 (__ -> Registers.register List.list) -> (__ -> Registers.register
737 List.list) -> (__ -> Registers.register List.list) -> (__ ->
738 Registers.register List.list) -> (__ -> Registers.register List.list) ->
739 (__ -> Registers.register List.list) -> (__ -> Registers.register
740 List.list) -> (__ -> Registers.register List.list) -> (__ ->
741 Registers.register List.list) -> (__ -> Registers.register List.list) ->
742 (__ -> Registers.register List.list) -> (__ -> Registers.register
743 List.list) -> __ -> 'a1) -> 'a1 **)
744 let get_pseudo_reg_functs_inv_rect_Type3 x1 hterm h1 =
745 let hcut = get_pseudo_reg_functs_rect_Type3 x1 h1 hterm in hcut __
747 (** val get_pseudo_reg_functs_inv_rect_Type2 :
748 unserialized_params -> get_pseudo_reg_functs -> ((__ ->
749 Registers.register List.list) -> (__ -> Registers.register List.list) ->
750 (__ -> Registers.register List.list) -> (__ -> Registers.register
751 List.list) -> (__ -> Registers.register List.list) -> (__ ->
752 Registers.register List.list) -> (__ -> Registers.register List.list) ->
753 (__ -> Registers.register List.list) -> (__ -> Registers.register
754 List.list) -> (__ -> Registers.register List.list) -> (__ ->
755 Registers.register List.list) -> (__ -> Registers.register List.list) ->
756 (__ -> Registers.register List.list) -> (__ -> Registers.register
757 List.list) -> __ -> 'a1) -> 'a1 **)
758 let get_pseudo_reg_functs_inv_rect_Type2 x1 hterm h1 =
759 let hcut = get_pseudo_reg_functs_rect_Type2 x1 h1 hterm in hcut __
761 (** val get_pseudo_reg_functs_inv_rect_Type1 :
762 unserialized_params -> get_pseudo_reg_functs -> ((__ ->
763 Registers.register List.list) -> (__ -> Registers.register List.list) ->
764 (__ -> Registers.register List.list) -> (__ -> Registers.register
765 List.list) -> (__ -> Registers.register List.list) -> (__ ->
766 Registers.register List.list) -> (__ -> Registers.register List.list) ->
767 (__ -> Registers.register List.list) -> (__ -> Registers.register
768 List.list) -> (__ -> Registers.register List.list) -> (__ ->
769 Registers.register List.list) -> (__ -> Registers.register List.list) ->
770 (__ -> Registers.register List.list) -> (__ -> Registers.register
771 List.list) -> __ -> 'a1) -> 'a1 **)
772 let get_pseudo_reg_functs_inv_rect_Type1 x1 hterm h1 =
773 let hcut = get_pseudo_reg_functs_rect_Type1 x1 h1 hterm in hcut __
775 (** val get_pseudo_reg_functs_inv_rect_Type0 :
776 unserialized_params -> get_pseudo_reg_functs -> ((__ ->
777 Registers.register List.list) -> (__ -> Registers.register List.list) ->
778 (__ -> Registers.register List.list) -> (__ -> Registers.register
779 List.list) -> (__ -> Registers.register List.list) -> (__ ->
780 Registers.register List.list) -> (__ -> Registers.register List.list) ->
781 (__ -> Registers.register List.list) -> (__ -> Registers.register
782 List.list) -> (__ -> Registers.register List.list) -> (__ ->
783 Registers.register List.list) -> (__ -> Registers.register List.list) ->
784 (__ -> Registers.register List.list) -> (__ -> Registers.register
785 List.list) -> __ -> 'a1) -> 'a1 **)
786 let get_pseudo_reg_functs_inv_rect_Type0 x1 hterm h1 =
787 let hcut = get_pseudo_reg_functs_rect_Type0 x1 h1 hterm in hcut __
789 (** val get_pseudo_reg_functs_jmdiscr :
790 unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs ->
792 let get_pseudo_reg_functs_jmdiscr a1 x y =
793 Logic.eq_rect_Type2 x
794 (let { acc_a_regs = a0; acc_b_regs = a10; acc_a_args = a2; acc_b_args =
795 a3; dpl_regs = a4; dph_regs = a5; dpl_args = a6; dph_args = a7;
796 snd_args = a8; pair_move_regs = a9; f_call_args = a100; f_call_dest =
797 a11; ext_seq_regs = a12; params_regs = a13 } = x
799 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
801 type uns_params = { u_pars : unserialized_params;
802 functs : get_pseudo_reg_functs }
804 (** val uns_params_rect_Type4 :
805 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
807 let rec uns_params_rect_Type4 h_mk_uns_params x_16995 =
808 let { u_pars = u_pars0; functs = functs0 } = x_16995 in
809 h_mk_uns_params u_pars0 functs0
811 (** val uns_params_rect_Type5 :
812 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
814 let rec uns_params_rect_Type5 h_mk_uns_params x_16997 =
815 let { u_pars = u_pars0; functs = functs0 } = x_16997 in
816 h_mk_uns_params u_pars0 functs0
818 (** val uns_params_rect_Type3 :
819 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
821 let rec uns_params_rect_Type3 h_mk_uns_params x_16999 =
822 let { u_pars = u_pars0; functs = functs0 } = x_16999 in
823 h_mk_uns_params u_pars0 functs0
825 (** val uns_params_rect_Type2 :
826 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
828 let rec uns_params_rect_Type2 h_mk_uns_params x_17001 =
829 let { u_pars = u_pars0; functs = functs0 } = x_17001 in
830 h_mk_uns_params u_pars0 functs0
832 (** val uns_params_rect_Type1 :
833 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
835 let rec uns_params_rect_Type1 h_mk_uns_params x_17003 =
836 let { u_pars = u_pars0; functs = functs0 } = x_17003 in
837 h_mk_uns_params u_pars0 functs0
839 (** val uns_params_rect_Type0 :
840 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
842 let rec uns_params_rect_Type0 h_mk_uns_params x_17005 =
843 let { u_pars = u_pars0; functs = functs0 } = x_17005 in
844 h_mk_uns_params u_pars0 functs0
846 (** val u_pars : uns_params -> unserialized_params **)
850 (** val functs : uns_params -> get_pseudo_reg_functs **)
854 (** val uns_params_inv_rect_Type4 :
855 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
857 let uns_params_inv_rect_Type4 hterm h1 =
858 let hcut = uns_params_rect_Type4 h1 hterm in hcut __
860 (** val uns_params_inv_rect_Type3 :
861 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
863 let uns_params_inv_rect_Type3 hterm h1 =
864 let hcut = uns_params_rect_Type3 h1 hterm in hcut __
866 (** val uns_params_inv_rect_Type2 :
867 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
869 let uns_params_inv_rect_Type2 hterm h1 =
870 let hcut = uns_params_rect_Type2 h1 hterm in hcut __
872 (** val uns_params_inv_rect_Type1 :
873 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
875 let uns_params_inv_rect_Type1 hterm h1 =
876 let hcut = uns_params_rect_Type1 h1 hterm in hcut __
878 (** val uns_params_inv_rect_Type0 :
879 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
881 let uns_params_inv_rect_Type0 hterm h1 =
882 let hcut = uns_params_rect_Type0 h1 hterm in hcut __
884 (** val uns_params_jmdiscr : uns_params -> uns_params -> __ **)
885 let uns_params_jmdiscr x y =
886 Logic.eq_rect_Type2 x
887 (let { u_pars = a0; functs = a1 } = x in
888 Obj.magic (fun _ dH -> dH __ __)) y
891 | COMMENT of String.string
895 | ADDRESS of AST.ident * BitVector.word * __ * __
896 | OPACCS of BackEndOps.opAccs * __ * __ * __ * __
897 | OP1 of BackEndOps.op1 * __ * __
898 | OP2 of BackEndOps.op2 * __ * __ * __
901 | LOAD of __ * __ * __
902 | STORE of __ * __ * __
903 | Extension_seq of __
905 (** val joint_seq_rect_Type4 :
906 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
907 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
908 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
909 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
910 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
911 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
912 let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
913 | COMMENT x_17061 -> h_COMMENT x_17061
914 | MOVE x_17062 -> h_MOVE x_17062
915 | POP x_17063 -> h_POP x_17063
916 | PUSH x_17064 -> h_PUSH x_17064
917 | ADDRESS (i, x_17067, x_17066, x_17065) ->
918 h_ADDRESS i __ x_17067 x_17066 x_17065
919 | OPACCS (x_17073, x_17072, x_17071, x_17070, x_17069) ->
920 h_OPACCS x_17073 x_17072 x_17071 x_17070 x_17069
921 | OP1 (x_17076, x_17075, x_17074) -> h_OP1 x_17076 x_17075 x_17074
922 | OP2 (x_17080, x_17079, x_17078, x_17077) ->
923 h_OP2 x_17080 x_17079 x_17078 x_17077
924 | CLEAR_CARRY -> h_CLEAR_CARRY
925 | SET_CARRY -> h_SET_CARRY
926 | LOAD (x_17083, x_17082, x_17081) -> h_LOAD x_17083 x_17082 x_17081
927 | STORE (x_17086, x_17085, x_17084) -> h_STORE x_17086 x_17085 x_17084
928 | Extension_seq x_17087 -> h_extension_seq x_17087
930 (** val joint_seq_rect_Type5 :
931 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
932 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
933 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
934 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
935 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
936 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
937 let 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
938 | COMMENT x_17102 -> h_COMMENT x_17102
939 | MOVE x_17103 -> h_MOVE x_17103
940 | POP x_17104 -> h_POP x_17104
941 | PUSH x_17105 -> h_PUSH x_17105
942 | ADDRESS (i, x_17108, x_17107, x_17106) ->
943 h_ADDRESS i __ x_17108 x_17107 x_17106
944 | OPACCS (x_17114, x_17113, x_17112, x_17111, x_17110) ->
945 h_OPACCS x_17114 x_17113 x_17112 x_17111 x_17110
946 | OP1 (x_17117, x_17116, x_17115) -> h_OP1 x_17117 x_17116 x_17115
947 | OP2 (x_17121, x_17120, x_17119, x_17118) ->
948 h_OP2 x_17121 x_17120 x_17119 x_17118
949 | CLEAR_CARRY -> h_CLEAR_CARRY
950 | SET_CARRY -> h_SET_CARRY
951 | LOAD (x_17124, x_17123, x_17122) -> h_LOAD x_17124 x_17123 x_17122
952 | STORE (x_17127, x_17126, x_17125) -> h_STORE x_17127 x_17126 x_17125
953 | Extension_seq x_17128 -> h_extension_seq x_17128
955 (** val joint_seq_rect_Type3 :
956 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
957 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
958 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
959 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
960 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
961 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
962 let 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
963 | COMMENT x_17143 -> h_COMMENT x_17143
964 | MOVE x_17144 -> h_MOVE x_17144
965 | POP x_17145 -> h_POP x_17145
966 | PUSH x_17146 -> h_PUSH x_17146
967 | ADDRESS (i, x_17149, x_17148, x_17147) ->
968 h_ADDRESS i __ x_17149 x_17148 x_17147
969 | OPACCS (x_17155, x_17154, x_17153, x_17152, x_17151) ->
970 h_OPACCS x_17155 x_17154 x_17153 x_17152 x_17151
971 | OP1 (x_17158, x_17157, x_17156) -> h_OP1 x_17158 x_17157 x_17156
972 | OP2 (x_17162, x_17161, x_17160, x_17159) ->
973 h_OP2 x_17162 x_17161 x_17160 x_17159
974 | CLEAR_CARRY -> h_CLEAR_CARRY
975 | SET_CARRY -> h_SET_CARRY
976 | LOAD (x_17165, x_17164, x_17163) -> h_LOAD x_17165 x_17164 x_17163
977 | STORE (x_17168, x_17167, x_17166) -> h_STORE x_17168 x_17167 x_17166
978 | Extension_seq x_17169 -> h_extension_seq x_17169
980 (** val joint_seq_rect_Type2 :
981 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
982 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
983 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
984 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
985 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
986 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
987 let 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
988 | COMMENT x_17184 -> h_COMMENT x_17184
989 | MOVE x_17185 -> h_MOVE x_17185
990 | POP x_17186 -> h_POP x_17186
991 | PUSH x_17187 -> h_PUSH x_17187
992 | ADDRESS (i, x_17190, x_17189, x_17188) ->
993 h_ADDRESS i __ x_17190 x_17189 x_17188
994 | OPACCS (x_17196, x_17195, x_17194, x_17193, x_17192) ->
995 h_OPACCS x_17196 x_17195 x_17194 x_17193 x_17192
996 | OP1 (x_17199, x_17198, x_17197) -> h_OP1 x_17199 x_17198 x_17197
997 | OP2 (x_17203, x_17202, x_17201, x_17200) ->
998 h_OP2 x_17203 x_17202 x_17201 x_17200
999 | CLEAR_CARRY -> h_CLEAR_CARRY
1000 | SET_CARRY -> h_SET_CARRY
1001 | LOAD (x_17206, x_17205, x_17204) -> h_LOAD x_17206 x_17205 x_17204
1002 | STORE (x_17209, x_17208, x_17207) -> h_STORE x_17209 x_17208 x_17207
1003 | Extension_seq x_17210 -> h_extension_seq x_17210
1005 (** val joint_seq_rect_Type1 :
1006 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1007 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1008 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1009 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1010 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1011 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1012 let 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
1013 | COMMENT x_17225 -> h_COMMENT x_17225
1014 | MOVE x_17226 -> h_MOVE x_17226
1015 | POP x_17227 -> h_POP x_17227
1016 | PUSH x_17228 -> h_PUSH x_17228
1017 | ADDRESS (i, x_17231, x_17230, x_17229) ->
1018 h_ADDRESS i __ x_17231 x_17230 x_17229
1019 | OPACCS (x_17237, x_17236, x_17235, x_17234, x_17233) ->
1020 h_OPACCS x_17237 x_17236 x_17235 x_17234 x_17233
1021 | OP1 (x_17240, x_17239, x_17238) -> h_OP1 x_17240 x_17239 x_17238
1022 | OP2 (x_17244, x_17243, x_17242, x_17241) ->
1023 h_OP2 x_17244 x_17243 x_17242 x_17241
1024 | CLEAR_CARRY -> h_CLEAR_CARRY
1025 | SET_CARRY -> h_SET_CARRY
1026 | LOAD (x_17247, x_17246, x_17245) -> h_LOAD x_17247 x_17246 x_17245
1027 | STORE (x_17250, x_17249, x_17248) -> h_STORE x_17250 x_17249 x_17248
1028 | Extension_seq x_17251 -> h_extension_seq x_17251
1030 (** val joint_seq_rect_Type0 :
1031 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1032 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1033 BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1034 __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1035 (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1036 __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1037 let 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
1038 | COMMENT x_17266 -> h_COMMENT x_17266
1039 | MOVE x_17267 -> h_MOVE x_17267
1040 | POP x_17268 -> h_POP x_17268
1041 | PUSH x_17269 -> h_PUSH x_17269
1042 | ADDRESS (i, x_17272, x_17271, x_17270) ->
1043 h_ADDRESS i __ x_17272 x_17271 x_17270
1044 | OPACCS (x_17278, x_17277, x_17276, x_17275, x_17274) ->
1045 h_OPACCS x_17278 x_17277 x_17276 x_17275 x_17274
1046 | OP1 (x_17281, x_17280, x_17279) -> h_OP1 x_17281 x_17280 x_17279
1047 | OP2 (x_17285, x_17284, x_17283, x_17282) ->
1048 h_OP2 x_17285 x_17284 x_17283 x_17282
1049 | CLEAR_CARRY -> h_CLEAR_CARRY
1050 | SET_CARRY -> h_SET_CARRY
1051 | LOAD (x_17288, x_17287, x_17286) -> h_LOAD x_17288 x_17287 x_17286
1052 | STORE (x_17291, x_17290, x_17289) -> h_STORE x_17291 x_17290 x_17289
1053 | Extension_seq x_17292 -> h_extension_seq x_17292
1055 (** val joint_seq_inv_rect_Type4 :
1056 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1057 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1058 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1059 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1060 (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1061 -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1062 __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1063 let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1065 joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1070 (** val joint_seq_inv_rect_Type3 :
1071 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1072 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1073 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1074 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1075 (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1076 -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1077 __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1078 let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1080 joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1085 (** val joint_seq_inv_rect_Type2 :
1086 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1087 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1088 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1089 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1090 (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1091 -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1092 __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1093 let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1095 joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1100 (** val joint_seq_inv_rect_Type1 :
1101 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1102 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1103 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1104 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1105 (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1106 -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1107 __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1108 let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1110 joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1115 (** val joint_seq_inv_rect_Type0 :
1116 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1117 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1118 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1119 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1120 (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1121 -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1122 __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1123 let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1125 joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1130 (** val joint_seq_discr :
1131 unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1133 let joint_seq_discr a1 a2 x y =
1134 Logic.eq_rect_Type2 x
1136 | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1137 | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1138 | POP a0 -> Obj.magic (fun _ dH -> dH __)
1139 | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1140 | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1141 | OPACCS (a0, a10, a20, a3, a4) ->
1142 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1143 | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1144 | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1145 | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1146 | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1147 | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1148 | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1149 | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1151 (** val joint_seq_jmdiscr :
1152 unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1154 let joint_seq_jmdiscr a1 a2 x y =
1155 Logic.eq_rect_Type2 x
1157 | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1158 | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1159 | POP a0 -> Obj.magic (fun _ dH -> dH __)
1160 | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1161 | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1162 | OPACCS (a0, a10, a20, a3, a4) ->
1163 Obj.magic (fun _ dH -> dH __ __ __ __ __)
1164 | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1165 | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1166 | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1167 | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1168 | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1169 | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1170 | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1172 (** val get_used_registers_from_seq :
1173 unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1174 joint_seq -> Registers.register List.list **)
1175 let get_used_registers_from_seq p globals functs0 = function
1176 | COMMENT x -> List.Nil
1177 | MOVE pm -> functs0.pair_move_regs pm
1178 | POP r -> functs0.acc_a_regs r
1179 | PUSH r -> functs0.acc_a_args r
1180 | ADDRESS (x, x1, r1, r2) ->
1181 List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1182 | OPACCS (o, r1, r2, r3, r4) ->
1183 List.append (functs0.acc_a_regs r1)
1184 (List.append (functs0.acc_b_regs r2)
1185 (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1186 | OP1 (o, r1, r2) ->
1187 List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1188 | OP2 (o, r1, r2, r3) ->
1189 List.append (functs0.acc_a_regs r1)
1190 (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1191 | CLEAR_CARRY -> List.Nil
1192 | SET_CARRY -> List.Nil
1193 | LOAD (r1, r2, r3) ->
1194 List.append (functs0.acc_a_regs r1)
1195 (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1196 | STORE (r1, r2, r3) ->
1197 List.append (functs0.dpl_args r1)
1198 (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1199 | Extension_seq ext -> functs0.ext_seq_regs ext
1201 (** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1202 let nOOP p globals =
1203 COMMENT String.EmptyString
1205 (** val dpi1__o__extension_seq_to_seq__o__inject :
1206 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1207 joint_seq Types.sig0 **)
1208 let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1209 Extension_seq x4.Types.dpi1
1211 (** val eject__o__extension_seq_to_seq__o__inject :
1212 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1214 let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1215 Extension_seq (Types.pi1 x4)
1217 (** val extension_seq_to_seq__o__inject :
1218 unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1219 let extension_seq_to_seq__o__inject x0 x1 x3 =
1222 (** val dpi1__o__extension_seq_to_seq :
1223 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1225 let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1226 Extension_seq x3.Types.dpi1
1228 (** val eject__o__extension_seq_to_seq :
1229 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1230 let eject__o__extension_seq_to_seq x0 x1 x3 =
1231 Extension_seq (Types.pi1 x3)
1234 | COST_LABEL of CostLabel.costlabel
1235 | CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1236 | COND of __ * Graphs.label
1237 | Step_seq of joint_seq
1239 (** val joint_step_rect_Type4 :
1240 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1241 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1242 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1243 let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1244 | COST_LABEL x_17565 -> h_COST_LABEL x_17565
1245 | CALL (x_17568, x_17567, x_17566) -> h_CALL x_17568 x_17567 x_17566
1246 | COND (x_17570, x_17569) -> h_COND x_17570 x_17569
1247 | Step_seq x_17571 -> h_step_seq x_17571
1249 (** val joint_step_rect_Type5 :
1250 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1251 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1252 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1253 let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1254 | COST_LABEL x_17577 -> h_COST_LABEL x_17577
1255 | CALL (x_17580, x_17579, x_17578) -> h_CALL x_17580 x_17579 x_17578
1256 | COND (x_17582, x_17581) -> h_COND x_17582 x_17581
1257 | Step_seq x_17583 -> h_step_seq x_17583
1259 (** val joint_step_rect_Type3 :
1260 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1261 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1262 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1263 let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1264 | COST_LABEL x_17589 -> h_COST_LABEL x_17589
1265 | CALL (x_17592, x_17591, x_17590) -> h_CALL x_17592 x_17591 x_17590
1266 | COND (x_17594, x_17593) -> h_COND x_17594 x_17593
1267 | Step_seq x_17595 -> h_step_seq x_17595
1269 (** val joint_step_rect_Type2 :
1270 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1271 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1272 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1273 let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1274 | COST_LABEL x_17601 -> h_COST_LABEL x_17601
1275 | CALL (x_17604, x_17603, x_17602) -> h_CALL x_17604 x_17603 x_17602
1276 | COND (x_17606, x_17605) -> h_COND x_17606 x_17605
1277 | Step_seq x_17607 -> h_step_seq x_17607
1279 (** val joint_step_rect_Type1 :
1280 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1281 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1282 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1283 let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1284 | COST_LABEL x_17613 -> h_COST_LABEL x_17613
1285 | CALL (x_17616, x_17615, x_17614) -> h_CALL x_17616 x_17615 x_17614
1286 | COND (x_17618, x_17617) -> h_COND x_17618 x_17617
1287 | Step_seq x_17619 -> h_step_seq x_17619
1289 (** val joint_step_rect_Type0 :
1290 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1291 'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1292 -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1293 let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1294 | COST_LABEL x_17625 -> h_COST_LABEL x_17625
1295 | CALL (x_17628, x_17627, x_17626) -> h_CALL x_17628 x_17627 x_17626
1296 | COND (x_17630, x_17629) -> h_COND x_17630 x_17629
1297 | Step_seq x_17631 -> h_step_seq x_17631
1299 (** val joint_step_inv_rect_Type4 :
1300 unserialized_params -> AST.ident List.list -> joint_step ->
1301 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1302 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1303 -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1304 let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1305 let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1307 (** val joint_step_inv_rect_Type3 :
1308 unserialized_params -> AST.ident List.list -> joint_step ->
1309 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1310 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1311 -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1312 let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1313 let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1315 (** val joint_step_inv_rect_Type2 :
1316 unserialized_params -> AST.ident List.list -> joint_step ->
1317 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1318 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1319 -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1320 let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1321 let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1323 (** val joint_step_inv_rect_Type1 :
1324 unserialized_params -> AST.ident List.list -> joint_step ->
1325 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1326 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1327 -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1328 let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1329 let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1331 (** val joint_step_inv_rect_Type0 :
1332 unserialized_params -> AST.ident List.list -> joint_step ->
1333 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1334 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1335 -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1336 let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1337 let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1339 (** val joint_step_discr :
1340 unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1342 let joint_step_discr a1 a2 x y =
1343 Logic.eq_rect_Type2 x
1345 | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1346 | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1347 | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1348 | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1350 (** val joint_step_jmdiscr :
1351 unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1353 let joint_step_jmdiscr a1 a2 x y =
1354 Logic.eq_rect_Type2 x
1356 | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1357 | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1358 | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1359 | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1361 (** val get_used_registers_from_step :
1362 unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1363 joint_step -> Registers.register List.list **)
1364 let get_used_registers_from_step p globals functs0 = function
1365 | COST_LABEL c -> List.Nil
1366 | CALL (id, args, dest) ->
1369 | Types.Inl x -> List.Nil
1371 List.append (functs0.dpl_args ptr.Types.fst)
1372 (functs0.dph_args ptr.Types.snd)
1375 (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1376 | COND (r, lbl) -> functs0.acc_a_regs r
1377 | Step_seq s -> get_used_registers_from_seq p globals functs0 s
1379 (** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1380 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1381 joint_step Types.sig0 **)
1382 let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1383 Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1385 (** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1386 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1388 let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1389 Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1391 (** val extension_seq_to_seq__o__seq_to_step__o__inject :
1392 unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1393 let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1394 Step_seq (Extension_seq x2)
1396 (** val dpi1__o__seq_to_step__o__inject :
1397 unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1398 Types.dPair -> joint_step Types.sig0 **)
1399 let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1400 Step_seq x4.Types.dpi1
1402 (** val eject__o__seq_to_step__o__inject :
1403 unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1404 joint_step Types.sig0 **)
1405 let eject__o__seq_to_step__o__inject x0 x1 x4 =
1406 Step_seq (Types.pi1 x4)
1408 (** val seq_to_step__o__inject :
1409 unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1411 let seq_to_step__o__inject x0 x1 x3 =
1414 (** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1415 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1417 let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1418 Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1420 (** val eject__o__extension_seq_to_seq__o__seq_to_step :
1421 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1422 let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1423 Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1425 (** val extension_seq_to_seq__o__seq_to_step :
1426 unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1427 let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1428 Step_seq (Extension_seq x2)
1430 (** val dpi1__o__seq_to_step :
1431 unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1432 Types.dPair -> joint_step **)
1433 let dpi1__o__seq_to_step x0 x1 x3 =
1434 Step_seq x3.Types.dpi1
1436 (** val eject__o__seq_to_step :
1437 unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1439 let eject__o__seq_to_step x0 x1 x3 =
1440 Step_seq (Types.pi1 x3)
1442 (** val step_labels :
1443 unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1445 let step_labels p globals = function
1446 | COST_LABEL x -> List.Nil
1447 | CALL (x, x0, x1) -> List.Nil
1448 | COND (x, l) -> List.Cons (l, List.Nil)
1451 | COMMENT x -> List.Nil
1452 | MOVE x -> List.Nil
1454 | PUSH x -> List.Nil
1455 | ADDRESS (x, x1, x2, x3) -> List.Nil
1456 | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1457 | OP1 (x, x0, x1) -> List.Nil
1458 | OP2 (x, x0, x1, x2) -> List.Nil
1459 | CLEAR_CARRY -> List.Nil
1460 | SET_CARRY -> List.Nil
1461 | LOAD (x, x0, x1) -> List.Nil
1462 | STORE (x, x0, x1) -> List.Nil
1463 | Extension_seq ext -> p.ext_seq_labels ext)
1465 type stmt_params = { uns_pars : uns_params;
1466 succ_label : (__ -> Graphs.label Types.option);
1467 has_fcond : Bool.bool }
1469 (** val stmt_params_rect_Type4 :
1470 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1471 'a1) -> stmt_params -> 'a1 **)
1472 let rec stmt_params_rect_Type4 h_mk_stmt_params x_17710 =
1473 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1474 has_fcond0 } = x_17710
1476 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1478 (** val stmt_params_rect_Type5 :
1479 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1480 'a1) -> stmt_params -> 'a1 **)
1481 let rec stmt_params_rect_Type5 h_mk_stmt_params x_17712 =
1482 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1483 has_fcond0 } = x_17712
1485 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1487 (** val stmt_params_rect_Type3 :
1488 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1489 'a1) -> stmt_params -> 'a1 **)
1490 let rec stmt_params_rect_Type3 h_mk_stmt_params x_17714 =
1491 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1492 has_fcond0 } = x_17714
1494 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1496 (** val stmt_params_rect_Type2 :
1497 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1498 'a1) -> stmt_params -> 'a1 **)
1499 let rec stmt_params_rect_Type2 h_mk_stmt_params x_17716 =
1500 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1501 has_fcond0 } = x_17716
1503 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1505 (** val stmt_params_rect_Type1 :
1506 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1507 'a1) -> stmt_params -> 'a1 **)
1508 let rec stmt_params_rect_Type1 h_mk_stmt_params x_17718 =
1509 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1510 has_fcond0 } = x_17718
1512 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1514 (** val stmt_params_rect_Type0 :
1515 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1516 'a1) -> stmt_params -> 'a1 **)
1517 let rec stmt_params_rect_Type0 h_mk_stmt_params x_17720 =
1518 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1519 has_fcond0 } = x_17720
1521 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1523 (** val uns_pars : stmt_params -> uns_params **)
1524 let rec uns_pars xxx =
1529 (** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1530 let rec succ_label xxx =
1533 (** val has_fcond : stmt_params -> Bool.bool **)
1534 let rec has_fcond xxx =
1537 (** val stmt_params_inv_rect_Type4 :
1538 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539 Bool.bool -> __ -> 'a1) -> 'a1 **)
1540 let stmt_params_inv_rect_Type4 hterm h1 =
1541 let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1543 (** val stmt_params_inv_rect_Type3 :
1544 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545 Bool.bool -> __ -> 'a1) -> 'a1 **)
1546 let stmt_params_inv_rect_Type3 hterm h1 =
1547 let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1549 (** val stmt_params_inv_rect_Type2 :
1550 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551 Bool.bool -> __ -> 'a1) -> 'a1 **)
1552 let stmt_params_inv_rect_Type2 hterm h1 =
1553 let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1555 (** val stmt_params_inv_rect_Type1 :
1556 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1557 Bool.bool -> __ -> 'a1) -> 'a1 **)
1558 let stmt_params_inv_rect_Type1 hterm h1 =
1559 let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1561 (** val stmt_params_inv_rect_Type0 :
1562 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1563 Bool.bool -> __ -> 'a1) -> 'a1 **)
1564 let stmt_params_inv_rect_Type0 hterm h1 =
1565 let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1567 (** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1568 let stmt_params_jmdiscr x y =
1569 Logic.eq_rect_Type2 x
1570 (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1571 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1573 (** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1574 let uns_pars__o__u_pars x0 =
1577 type joint_fin_step =
1578 | GOTO of Graphs.label
1580 | TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1582 (** val joint_fin_step_rect_Type4 :
1583 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1584 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1585 let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1586 | GOTO x_17744 -> h_GOTO x_17744
1587 | RETURN -> h_RETURN
1588 | TAILCALL (x_17746, x_17745) -> h_TAILCALL __ x_17746 x_17745
1590 (** val joint_fin_step_rect_Type5 :
1591 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1592 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1593 let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1594 | GOTO x_17752 -> h_GOTO x_17752
1595 | RETURN -> h_RETURN
1596 | TAILCALL (x_17754, x_17753) -> h_TAILCALL __ x_17754 x_17753
1598 (** val joint_fin_step_rect_Type3 :
1599 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1600 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1601 let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1602 | GOTO x_17760 -> h_GOTO x_17760
1603 | RETURN -> h_RETURN
1604 | TAILCALL (x_17762, x_17761) -> h_TAILCALL __ x_17762 x_17761
1606 (** val joint_fin_step_rect_Type2 :
1607 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1608 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1609 let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1610 | GOTO x_17768 -> h_GOTO x_17768
1611 | RETURN -> h_RETURN
1612 | TAILCALL (x_17770, x_17769) -> h_TAILCALL __ x_17770 x_17769
1614 (** val joint_fin_step_rect_Type1 :
1615 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1616 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1617 let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1618 | GOTO x_17776 -> h_GOTO x_17776
1619 | RETURN -> h_RETURN
1620 | TAILCALL (x_17778, x_17777) -> h_TAILCALL __ x_17778 x_17777
1622 (** val joint_fin_step_rect_Type0 :
1623 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1624 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1625 let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1626 | GOTO x_17784 -> h_GOTO x_17784
1627 | RETURN -> h_RETURN
1628 | TAILCALL (x_17786, x_17785) -> h_TAILCALL __ x_17786 x_17785
1630 (** val joint_fin_step_inv_rect_Type4 :
1631 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1632 (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1633 __ -> 'a1) -> 'a1 **)
1634 let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1635 let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1637 (** val joint_fin_step_inv_rect_Type3 :
1638 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1639 (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1640 __ -> 'a1) -> 'a1 **)
1641 let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1642 let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1644 (** val joint_fin_step_inv_rect_Type2 :
1645 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1646 (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1647 __ -> 'a1) -> 'a1 **)
1648 let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1649 let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1651 (** val joint_fin_step_inv_rect_Type1 :
1652 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1653 (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1654 __ -> 'a1) -> 'a1 **)
1655 let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1656 let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1658 (** val joint_fin_step_inv_rect_Type0 :
1659 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1660 (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1661 __ -> 'a1) -> 'a1 **)
1662 let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1663 let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1665 (** val joint_fin_step_discr :
1666 unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1667 let joint_fin_step_discr a1 x y =
1668 Logic.eq_rect_Type2 x
1670 | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1671 | RETURN -> Obj.magic (fun _ dH -> dH)
1672 | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1674 (** val joint_fin_step_jmdiscr :
1675 unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1676 let joint_fin_step_jmdiscr a1 x y =
1677 Logic.eq_rect_Type2 x
1679 | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1680 | RETURN -> Obj.magic (fun _ dH -> dH)
1681 | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1683 (** val fin_step_labels :
1684 unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1685 let fin_step_labels p = function
1686 | GOTO l -> List.Cons (l, List.Nil)
1687 | RETURN -> List.Nil
1688 | TAILCALL (x0, x1) -> List.Nil
1690 type joint_statement =
1691 | Sequential of joint_step * __
1692 | Final of joint_fin_step
1693 | FCOND of __ * Graphs.label * Graphs.label
1695 (** val joint_statement_rect_Type4 :
1696 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1697 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1698 'a1) -> joint_statement -> 'a1 **)
1699 let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1700 | Sequential (x_17852, x_17851) -> h_sequential x_17852 x_17851
1701 | Final x_17853 -> h_final x_17853
1702 | FCOND (x_17856, x_17855, x_17854) -> h_FCOND __ x_17856 x_17855 x_17854
1704 (** val joint_statement_rect_Type5 :
1705 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1706 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1707 'a1) -> joint_statement -> 'a1 **)
1708 let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1709 | Sequential (x_17863, x_17862) -> h_sequential x_17863 x_17862
1710 | Final x_17864 -> h_final x_17864
1711 | FCOND (x_17867, x_17866, x_17865) -> h_FCOND __ x_17867 x_17866 x_17865
1713 (** val joint_statement_rect_Type3 :
1714 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1715 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1716 'a1) -> joint_statement -> 'a1 **)
1717 let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1718 | Sequential (x_17874, x_17873) -> h_sequential x_17874 x_17873
1719 | Final x_17875 -> h_final x_17875
1720 | FCOND (x_17878, x_17877, x_17876) -> h_FCOND __ x_17878 x_17877 x_17876
1722 (** val joint_statement_rect_Type2 :
1723 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1724 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1725 'a1) -> joint_statement -> 'a1 **)
1726 let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1727 | Sequential (x_17885, x_17884) -> h_sequential x_17885 x_17884
1728 | Final x_17886 -> h_final x_17886
1729 | FCOND (x_17889, x_17888, x_17887) -> h_FCOND __ x_17889 x_17888 x_17887
1731 (** val joint_statement_rect_Type1 :
1732 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1733 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1734 'a1) -> joint_statement -> 'a1 **)
1735 let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1736 | Sequential (x_17896, x_17895) -> h_sequential x_17896 x_17895
1737 | Final x_17897 -> h_final x_17897
1738 | FCOND (x_17900, x_17899, x_17898) -> h_FCOND __ x_17900 x_17899 x_17898
1740 (** val joint_statement_rect_Type0 :
1741 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1742 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1743 'a1) -> joint_statement -> 'a1 **)
1744 let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1745 | Sequential (x_17907, x_17906) -> h_sequential x_17907 x_17906
1746 | Final x_17908 -> h_final x_17908
1747 | FCOND (x_17911, x_17910, x_17909) -> h_FCOND __ x_17911 x_17910 x_17909
1749 (** val joint_statement_inv_rect_Type4 :
1750 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1751 __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1752 Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1753 let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1754 let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1756 (** val joint_statement_inv_rect_Type3 :
1757 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1758 __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1759 Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1760 let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1761 let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1763 (** val joint_statement_inv_rect_Type2 :
1764 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1765 __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1766 Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1767 let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1768 let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1770 (** val joint_statement_inv_rect_Type1 :
1771 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1772 __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1773 Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1774 let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1775 let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1777 (** val joint_statement_inv_rect_Type0 :
1778 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1779 __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1780 Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1781 let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1782 let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1784 (** val joint_statement_discr :
1785 stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1787 let joint_statement_discr a1 a2 x y =
1788 Logic.eq_rect_Type2 x
1790 | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1791 | Final a0 -> Obj.magic (fun _ dH -> dH __)
1792 | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1794 (** val joint_statement_jmdiscr :
1795 stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1797 let joint_statement_jmdiscr a1 a2 x y =
1798 Logic.eq_rect_Type2 x
1800 | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1801 | Final a0 -> Obj.magic (fun _ dH -> dH __)
1802 | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1804 (** val dpi1__o__fin_step_to_stmt__o__inject :
1805 stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1806 -> joint_statement Types.sig0 **)
1807 let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1810 (** val eject__o__fin_step_to_stmt__o__inject :
1811 stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1812 joint_statement Types.sig0 **)
1813 let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1814 Final (Types.pi1 x4)
1816 (** val fin_step_to_stmt__o__inject :
1817 stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1819 let fin_step_to_stmt__o__inject x0 x1 x3 =
1822 (** val dpi1__o__fin_step_to_stmt :
1823 stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1824 -> joint_statement **)
1825 let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1828 (** val eject__o__fin_step_to_stmt :
1829 stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1831 let eject__o__fin_step_to_stmt x0 x1 x3 =
1832 Final (Types.pi1 x3)
1834 type params = { stmt_pars : stmt_params;
1835 stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1837 point_of_label : (AST.ident List.list -> __ -> Graphs.label
1838 -> __ Types.option);
1839 point_of_succ : (__ -> __ -> __) }
1841 (** val params_rect_Type4 :
1842 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1843 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1844 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1846 let rec params_rect_Type4 h_mk_params x_17984 =
1847 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1848 point_of_label0; point_of_succ = point_of_succ0 } = x_17984
1850 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1852 (** val params_rect_Type5 :
1853 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1854 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1855 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1857 let rec params_rect_Type5 h_mk_params x_17986 =
1858 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1859 point_of_label0; point_of_succ = point_of_succ0 } = x_17986
1861 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1863 (** val params_rect_Type3 :
1864 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1865 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1866 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1868 let rec params_rect_Type3 h_mk_params x_17988 =
1869 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1870 point_of_label0; point_of_succ = point_of_succ0 } = x_17988
1872 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1874 (** val params_rect_Type2 :
1875 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1876 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1877 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1879 let rec params_rect_Type2 h_mk_params x_17990 =
1880 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1881 point_of_label0; point_of_succ = point_of_succ0 } = x_17990
1883 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1885 (** val params_rect_Type1 :
1886 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1887 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1888 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1890 let rec params_rect_Type1 h_mk_params x_17992 =
1891 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1892 point_of_label0; point_of_succ = point_of_succ0 } = x_17992
1894 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1896 (** val params_rect_Type0 :
1897 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1898 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1899 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1901 let rec params_rect_Type0 h_mk_params x_17994 =
1902 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1903 point_of_label0; point_of_succ = point_of_succ0 } = x_17994
1905 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1907 (** val stmt_pars : params -> stmt_params **)
1908 let rec stmt_pars xxx =
1913 type code_point = __
1916 params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1917 let rec stmt_at xxx =
1920 (** val point_of_label :
1921 params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1922 let rec point_of_label xxx =
1925 (** val point_of_succ : params -> __ -> __ -> __ **)
1926 let rec point_of_succ xxx =
1929 (** val params_inv_rect_Type4 :
1930 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1931 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1932 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1933 let params_inv_rect_Type4 hterm h1 =
1934 let hcut = params_rect_Type4 h1 hterm in hcut __
1936 (** val params_inv_rect_Type3 :
1937 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1938 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1939 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1940 let params_inv_rect_Type3 hterm h1 =
1941 let hcut = params_rect_Type3 h1 hterm in hcut __
1943 (** val params_inv_rect_Type2 :
1944 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1945 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1946 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1947 let params_inv_rect_Type2 hterm h1 =
1948 let hcut = params_rect_Type2 h1 hterm in hcut __
1950 (** val params_inv_rect_Type1 :
1951 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1952 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1953 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1954 let params_inv_rect_Type1 hterm h1 =
1955 let hcut = params_rect_Type1 h1 hterm in hcut __
1957 (** val params_inv_rect_Type0 :
1958 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1959 joint_statement Types.option) -> (AST.ident List.list -> __ ->
1960 Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1961 let params_inv_rect_Type0 hterm h1 =
1962 let hcut = params_rect_Type0 h1 hterm in hcut __
1964 (** val params_jmdiscr : params -> params -> __ **)
1965 let params_jmdiscr x y =
1966 Logic.eq_rect_Type2 x
1967 (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1970 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1972 (** val stmt_pars__o__uns_pars : params -> uns_params **)
1973 let stmt_pars__o__uns_pars x0 =
1974 x0.stmt_pars.uns_pars
1976 (** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1977 let stmt_pars__o__uns_pars__o__u_pars x0 =
1978 uns_pars__o__u_pars x0.stmt_pars
1980 (** val code_has_point :
1981 params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1982 let code_has_point p globals c pt =
1983 match p.stmt_at globals c pt with
1984 | Types.None -> Bool.False
1985 | Types.Some x -> Bool.True
1987 (** val code_has_label :
1988 params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1989 let code_has_label p globals c l =
1990 match p.point_of_label globals c l with
1991 | Types.None -> Bool.False
1992 | Types.Some pt -> code_has_point p globals c pt
1994 (** val stmt_explicit_labels :
1995 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1997 let stmt_explicit_labels p globals = function
1998 | Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1999 | Final c -> fin_step_labels (uns_pars__o__u_pars p) c
2000 | FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
2002 (** val stmt_implicit_label :
2003 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2005 let stmt_implicit_label p globals = function
2006 | Sequential (x, s0) -> p.succ_label s0
2007 | Final x -> Types.None
2008 | FCOND (x0, x1, x2) -> Types.None
2010 (** val stmt_labels :
2011 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2013 let stmt_labels p g stmt =
2015 (match stmt_implicit_label p g stmt with
2016 | Types.None -> List.Nil
2017 | Types.Some l -> List.Cons (l, List.Nil))
2018 (stmt_explicit_labels p g stmt)
2020 (** val stmt_registers :
2021 stmt_params -> AST.ident List.list -> joint_statement ->
2022 Registers.register List.list **)
2023 let stmt_registers p globals = function
2024 | Sequential (c, x) ->
2025 get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2028 | GOTO x -> List.Nil
2029 | RETURN -> List.Nil
2030 | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2031 | FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2035 (* singleton inductive, whose constructor was mk_lin_params *)
2037 (** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2038 let rec lin_params_rect_Type4 h_mk_lin_params x_18017 =
2039 let l_u_pars = x_18017 in h_mk_lin_params l_u_pars
2041 (** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2042 let rec lin_params_rect_Type5 h_mk_lin_params x_18019 =
2043 let l_u_pars = x_18019 in h_mk_lin_params l_u_pars
2045 (** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2046 let rec lin_params_rect_Type3 h_mk_lin_params x_18021 =
2047 let l_u_pars = x_18021 in h_mk_lin_params l_u_pars
2049 (** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2050 let rec lin_params_rect_Type2 h_mk_lin_params x_18023 =
2051 let l_u_pars = x_18023 in h_mk_lin_params l_u_pars
2053 (** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2054 let rec lin_params_rect_Type1 h_mk_lin_params x_18025 =
2055 let l_u_pars = x_18025 in h_mk_lin_params l_u_pars
2057 (** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2058 let rec lin_params_rect_Type0 h_mk_lin_params x_18027 =
2059 let l_u_pars = x_18027 in h_mk_lin_params l_u_pars
2061 (** val l_u_pars : lin_params -> uns_params **)
2062 let rec l_u_pars xxx =
2063 let yyy = xxx in yyy
2065 (** val lin_params_inv_rect_Type4 :
2066 lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2067 let lin_params_inv_rect_Type4 hterm h1 =
2068 let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2070 (** val lin_params_inv_rect_Type3 :
2071 lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2072 let lin_params_inv_rect_Type3 hterm h1 =
2073 let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2075 (** val lin_params_inv_rect_Type2 :
2076 lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2077 let lin_params_inv_rect_Type2 hterm h1 =
2078 let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2080 (** val lin_params_inv_rect_Type1 :
2081 lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2082 let lin_params_inv_rect_Type1 hterm h1 =
2083 let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2085 (** val lin_params_inv_rect_Type0 :
2086 lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2087 let lin_params_inv_rect_Type0 hterm h1 =
2088 let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2090 (** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2091 let lin_params_jmdiscr x y =
2092 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2094 (** val lin_params_to_params : lin_params -> params **)
2095 let lin_params_to_params lp =
2096 { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2097 Types.None); has_fcond = Bool.True }; stmt_at =
2098 (fun globals code point ->
2100 (Monad.m_bind0 (Monad.max_def Option.option)
2101 (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2103 Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2104 point_of_label = (fun globals c lbl ->
2105 Util.if_then_else_safe
2106 (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2107 (Obj.magic c)) (fun _ ->
2109 (Monad.m_return0 (Monad.max_def Option.option)
2110 (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2111 (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2112 (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2114 (** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2115 let lp_to_p__o__stmt_pars x0 =
2116 (lin_params_to_params x0).stmt_pars
2118 (** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2119 let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2120 stmt_pars__o__uns_pars (lin_params_to_params x0)
2122 (** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2123 lin_params -> unserialized_params **)
2124 let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2125 stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2129 (* singleton inductive, whose constructor was mk_graph_params *)
2131 (** val graph_params_rect_Type4 :
2132 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2133 let rec graph_params_rect_Type4 h_mk_graph_params x_18043 =
2134 let g_u_pars = x_18043 in h_mk_graph_params g_u_pars
2136 (** val graph_params_rect_Type5 :
2137 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2138 let rec graph_params_rect_Type5 h_mk_graph_params x_18045 =
2139 let g_u_pars = x_18045 in h_mk_graph_params g_u_pars
2141 (** val graph_params_rect_Type3 :
2142 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2143 let rec graph_params_rect_Type3 h_mk_graph_params x_18047 =
2144 let g_u_pars = x_18047 in h_mk_graph_params g_u_pars
2146 (** val graph_params_rect_Type2 :
2147 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2148 let rec graph_params_rect_Type2 h_mk_graph_params x_18049 =
2149 let g_u_pars = x_18049 in h_mk_graph_params g_u_pars
2151 (** val graph_params_rect_Type1 :
2152 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2153 let rec graph_params_rect_Type1 h_mk_graph_params x_18051 =
2154 let g_u_pars = x_18051 in h_mk_graph_params g_u_pars
2156 (** val graph_params_rect_Type0 :
2157 (uns_params -> 'a1) -> graph_params -> 'a1 **)
2158 let rec graph_params_rect_Type0 h_mk_graph_params x_18053 =
2159 let g_u_pars = x_18053 in h_mk_graph_params g_u_pars
2161 (** val g_u_pars : graph_params -> uns_params **)
2162 let rec g_u_pars xxx =
2163 let yyy = xxx in yyy
2165 (** val graph_params_inv_rect_Type4 :
2166 graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2167 let graph_params_inv_rect_Type4 hterm h1 =
2168 let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2170 (** val graph_params_inv_rect_Type3 :
2171 graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2172 let graph_params_inv_rect_Type3 hterm h1 =
2173 let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2175 (** val graph_params_inv_rect_Type2 :
2176 graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2177 let graph_params_inv_rect_Type2 hterm h1 =
2178 let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2180 (** val graph_params_inv_rect_Type1 :
2181 graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2182 let graph_params_inv_rect_Type1 hterm h1 =
2183 let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2185 (** val graph_params_inv_rect_Type0 :
2186 graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2187 let graph_params_inv_rect_Type0 hterm h1 =
2188 let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2190 (** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2191 let graph_params_jmdiscr x y =
2192 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2194 (** val graph_params_to_params : graph_params -> params **)
2195 let graph_params_to_params gp =
2196 { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2197 (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2198 (fun globals code ->
2199 Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2200 point_of_label = (fun x x0 lbl ->
2201 Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2202 point_of_succ = (fun x lbl -> lbl) }
2204 (** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2205 let gp_to_p__o__stmt_pars x0 =
2206 (graph_params_to_params x0).stmt_pars
2208 (** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2209 let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2210 stmt_pars__o__uns_pars (graph_params_to_params x0)
2212 (** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2213 graph_params -> unserialized_params **)
2214 let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2215 stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2217 type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2218 joint_if_runiverse : Identifiers.universe;
2219 joint_if_result : __; joint_if_params :
2220 __; joint_if_stacksize : Nat.nat;
2221 joint_if_local_stacksize : Nat.nat;
2222 joint_if_code : __; joint_if_entry :
2225 (** val joint_internal_function_rect_Type4 :
2226 params -> AST.ident List.list -> (Identifiers.universe ->
2227 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2228 'a1) -> joint_internal_function -> 'a1 **)
2229 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18069 =
2230 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2231 joint_if_runiverse0; joint_if_result = joint_if_result0;
2232 joint_if_params = joint_if_params0; joint_if_stacksize =
2233 joint_if_stacksize0; joint_if_local_stacksize =
2234 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2235 joint_if_entry = joint_if_entry0 } = x_18069
2237 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2238 joint_if_result0 joint_if_params0 joint_if_stacksize0
2239 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2241 (** val joint_internal_function_rect_Type5 :
2242 params -> AST.ident List.list -> (Identifiers.universe ->
2243 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2244 'a1) -> joint_internal_function -> 'a1 **)
2245 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18071 =
2246 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2247 joint_if_runiverse0; joint_if_result = joint_if_result0;
2248 joint_if_params = joint_if_params0; joint_if_stacksize =
2249 joint_if_stacksize0; joint_if_local_stacksize =
2250 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2251 joint_if_entry = joint_if_entry0 } = x_18071
2253 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2254 joint_if_result0 joint_if_params0 joint_if_stacksize0
2255 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2257 (** val joint_internal_function_rect_Type3 :
2258 params -> AST.ident List.list -> (Identifiers.universe ->
2259 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2260 'a1) -> joint_internal_function -> 'a1 **)
2261 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18073 =
2262 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2263 joint_if_runiverse0; joint_if_result = joint_if_result0;
2264 joint_if_params = joint_if_params0; joint_if_stacksize =
2265 joint_if_stacksize0; joint_if_local_stacksize =
2266 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2267 joint_if_entry = joint_if_entry0 } = x_18073
2269 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2270 joint_if_result0 joint_if_params0 joint_if_stacksize0
2271 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2273 (** val joint_internal_function_rect_Type2 :
2274 params -> AST.ident List.list -> (Identifiers.universe ->
2275 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2276 'a1) -> joint_internal_function -> 'a1 **)
2277 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18075 =
2278 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2279 joint_if_runiverse0; joint_if_result = joint_if_result0;
2280 joint_if_params = joint_if_params0; joint_if_stacksize =
2281 joint_if_stacksize0; joint_if_local_stacksize =
2282 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2283 joint_if_entry = joint_if_entry0 } = x_18075
2285 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2286 joint_if_result0 joint_if_params0 joint_if_stacksize0
2287 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2289 (** val joint_internal_function_rect_Type1 :
2290 params -> AST.ident List.list -> (Identifiers.universe ->
2291 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2292 'a1) -> joint_internal_function -> 'a1 **)
2293 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18077 =
2294 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2295 joint_if_runiverse0; joint_if_result = joint_if_result0;
2296 joint_if_params = joint_if_params0; joint_if_stacksize =
2297 joint_if_stacksize0; joint_if_local_stacksize =
2298 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2299 joint_if_entry = joint_if_entry0 } = x_18077
2301 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2302 joint_if_result0 joint_if_params0 joint_if_stacksize0
2303 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2305 (** val joint_internal_function_rect_Type0 :
2306 params -> AST.ident List.list -> (Identifiers.universe ->
2307 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2308 'a1) -> joint_internal_function -> 'a1 **)
2309 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18079 =
2310 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2311 joint_if_runiverse0; joint_if_result = joint_if_result0;
2312 joint_if_params = joint_if_params0; joint_if_stacksize =
2313 joint_if_stacksize0; joint_if_local_stacksize =
2314 joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2315 joint_if_entry = joint_if_entry0 } = x_18079
2317 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2318 joint_if_result0 joint_if_params0 joint_if_stacksize0
2319 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2321 (** val joint_if_luniverse :
2322 params -> AST.ident List.list -> joint_internal_function ->
2323 Identifiers.universe **)
2324 let rec joint_if_luniverse p globals xxx =
2325 xxx.joint_if_luniverse
2327 (** val joint_if_runiverse :
2328 params -> AST.ident List.list -> joint_internal_function ->
2329 Identifiers.universe **)
2330 let rec joint_if_runiverse p globals xxx =
2331 xxx.joint_if_runiverse
2333 (** val joint_if_result :
2334 params -> AST.ident List.list -> joint_internal_function -> __ **)
2335 let rec joint_if_result p globals xxx =
2338 (** val joint_if_params :
2339 params -> AST.ident List.list -> joint_internal_function -> __ **)
2340 let rec joint_if_params p globals xxx =
2343 (** val joint_if_stacksize :
2344 params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2345 let rec joint_if_stacksize p globals xxx =
2346 xxx.joint_if_stacksize
2348 (** val joint_if_local_stacksize :
2349 params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2350 let rec joint_if_local_stacksize p globals xxx =
2351 xxx.joint_if_local_stacksize
2353 (** val joint_if_code :
2354 params -> AST.ident List.list -> joint_internal_function -> __ **)
2355 let rec joint_if_code p globals xxx =
2358 (** val joint_if_entry :
2359 params -> AST.ident List.list -> joint_internal_function -> __ **)
2360 let rec joint_if_entry p globals xxx =
2363 (** val joint_internal_function_inv_rect_Type4 :
2364 params -> AST.ident List.list -> joint_internal_function ->
2365 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2366 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2367 let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2368 let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2370 (** val joint_internal_function_inv_rect_Type3 :
2371 params -> AST.ident List.list -> joint_internal_function ->
2372 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2373 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2374 let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2375 let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2377 (** val joint_internal_function_inv_rect_Type2 :
2378 params -> AST.ident List.list -> joint_internal_function ->
2379 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2380 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2381 let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2382 let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2384 (** val joint_internal_function_inv_rect_Type1 :
2385 params -> AST.ident List.list -> joint_internal_function ->
2386 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2387 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2388 let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2389 let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2391 (** val joint_internal_function_inv_rect_Type0 :
2392 params -> AST.ident List.list -> joint_internal_function ->
2393 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2394 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2395 let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2396 let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2398 (** val joint_internal_function_jmdiscr :
2399 params -> AST.ident List.list -> joint_internal_function ->
2400 joint_internal_function -> __ **)
2401 let joint_internal_function_jmdiscr a1 a2 x y =
2402 Logic.eq_rect_Type2 x
2403 (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2404 joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2405 joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2408 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2410 (** val good_if_rect_Type4 :
2411 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412 __ -> __ -> __ -> 'a1) -> 'a1 **)
2413 let rec good_if_rect_Type4 p globals def h_mk_good_if =
2414 h_mk_good_if __ __ __ __ __
2416 (** val good_if_rect_Type5 :
2417 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418 __ -> __ -> __ -> 'a1) -> 'a1 **)
2419 let rec good_if_rect_Type5 p globals def h_mk_good_if =
2420 h_mk_good_if __ __ __ __ __
2422 (** val good_if_rect_Type3 :
2423 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424 __ -> __ -> __ -> 'a1) -> 'a1 **)
2425 let rec good_if_rect_Type3 p globals def h_mk_good_if =
2426 h_mk_good_if __ __ __ __ __
2428 (** val good_if_rect_Type2 :
2429 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430 __ -> __ -> __ -> 'a1) -> 'a1 **)
2431 let rec good_if_rect_Type2 p globals def h_mk_good_if =
2432 h_mk_good_if __ __ __ __ __
2434 (** val good_if_rect_Type1 :
2435 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436 __ -> __ -> __ -> 'a1) -> 'a1 **)
2437 let rec good_if_rect_Type1 p globals def h_mk_good_if =
2438 h_mk_good_if __ __ __ __ __
2440 (** val good_if_rect_Type0 :
2441 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442 __ -> __ -> __ -> 'a1) -> 'a1 **)
2443 let rec good_if_rect_Type0 p globals def h_mk_good_if =
2444 h_mk_good_if __ __ __ __ __
2446 (** val good_if_inv_rect_Type4 :
2447 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448 __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449 let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2450 let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2452 (** val good_if_inv_rect_Type3 :
2453 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454 __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455 let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2456 let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2458 (** val good_if_inv_rect_Type2 :
2459 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460 __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461 let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2462 let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2464 (** val good_if_inv_rect_Type1 :
2465 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2466 __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2467 let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2468 let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2470 (** val good_if_inv_rect_Type0 :
2471 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2472 __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2473 let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2474 let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2476 (** val good_if_discr :
2477 params -> AST.ident List.list -> joint_internal_function -> __ **)
2478 let good_if_discr a1 a2 a3 =
2479 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2481 (** val good_if_jmdiscr :
2482 params -> AST.ident List.list -> joint_internal_function -> __ **)
2483 let good_if_jmdiscr a1 a2 a3 =
2484 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2486 type joint_closed_internal_function = joint_internal_function Types.sig0
2488 (** val set_joint_code :
2489 AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2490 joint_internal_function **)
2491 let set_joint_code globals pars int_fun graph entry =
2492 { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2493 int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2494 joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2495 int_fun.joint_if_stacksize; joint_if_local_stacksize =
2496 int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2499 (** val set_luniverse :
2500 params -> AST.ident List.list -> joint_internal_function ->
2501 Identifiers.universe -> joint_internal_function **)
2502 let set_luniverse globals pars p luniverse =
2503 { joint_if_luniverse = luniverse; joint_if_runiverse =
2504 p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2505 joint_if_params = p.joint_if_params; joint_if_stacksize =
2506 p.joint_if_stacksize; joint_if_local_stacksize =
2507 p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2508 joint_if_entry = p.joint_if_entry }
2510 (** val set_runiverse :
2511 params -> AST.ident List.list -> joint_internal_function ->
2512 Identifiers.universe -> joint_internal_function **)
2513 let set_runiverse globals pars p runiverse =
2514 { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2515 runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2516 p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2517 joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2518 p.joint_if_code; joint_if_entry = p.joint_if_entry }
2521 graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2522 joint_internal_function -> joint_internal_function **)
2523 let add_graph g_pars globals l stmt p =
2525 Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2528 { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2529 p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2530 joint_if_params = p.joint_if_params; joint_if_stacksize =
2531 p.joint_if_stacksize; joint_if_local_stacksize =
2532 p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2533 joint_if_entry = p.joint_if_entry }
2535 type joint_function = joint_closed_internal_function AST.fundef
2537 type joint_program = { jp_functions : AST.ident List.list;
2538 joint_prog : (joint_function, AST.init_data List.list)
2540 init_cost_label : CostLabel.costlabel }
2542 (** val joint_program_rect_Type4 :
2543 params -> (AST.ident List.list -> (joint_function, AST.init_data
2544 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2545 joint_program -> 'a1 **)
2546 let rec joint_program_rect_Type4 p h_mk_joint_program x_18121 =
2547 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2548 init_cost_label = init_cost_label0 } = x_18121
2550 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2552 (** val joint_program_rect_Type5 :
2553 params -> (AST.ident List.list -> (joint_function, AST.init_data
2554 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2555 joint_program -> 'a1 **)
2556 let rec joint_program_rect_Type5 p h_mk_joint_program x_18123 =
2557 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2558 init_cost_label = init_cost_label0 } = x_18123
2560 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2562 (** val joint_program_rect_Type3 :
2563 params -> (AST.ident List.list -> (joint_function, AST.init_data
2564 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2565 joint_program -> 'a1 **)
2566 let rec joint_program_rect_Type3 p h_mk_joint_program x_18125 =
2567 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2568 init_cost_label = init_cost_label0 } = x_18125
2570 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2572 (** val joint_program_rect_Type2 :
2573 params -> (AST.ident List.list -> (joint_function, AST.init_data
2574 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2575 joint_program -> 'a1 **)
2576 let rec joint_program_rect_Type2 p h_mk_joint_program x_18127 =
2577 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2578 init_cost_label = init_cost_label0 } = x_18127
2580 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2582 (** val joint_program_rect_Type1 :
2583 params -> (AST.ident List.list -> (joint_function, AST.init_data
2584 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2585 joint_program -> 'a1 **)
2586 let rec joint_program_rect_Type1 p h_mk_joint_program x_18129 =
2587 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2588 init_cost_label = init_cost_label0 } = x_18129
2590 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2592 (** val joint_program_rect_Type0 :
2593 params -> (AST.ident List.list -> (joint_function, AST.init_data
2594 List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2595 joint_program -> 'a1 **)
2596 let rec joint_program_rect_Type0 p h_mk_joint_program x_18131 =
2597 let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2598 init_cost_label = init_cost_label0 } = x_18131
2600 h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2602 (** val jp_functions : params -> joint_program -> AST.ident List.list **)
2603 let rec jp_functions p xxx =
2606 (** val joint_prog :
2607 params -> joint_program -> (joint_function, AST.init_data List.list)
2609 let rec joint_prog p xxx =
2612 (** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2613 let rec init_cost_label p xxx =
2616 (** val joint_program_inv_rect_Type4 :
2617 params -> joint_program -> (AST.ident List.list -> (joint_function,
2618 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2620 let joint_program_inv_rect_Type4 x1 hterm h1 =
2621 let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2623 (** val joint_program_inv_rect_Type3 :
2624 params -> joint_program -> (AST.ident List.list -> (joint_function,
2625 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2627 let joint_program_inv_rect_Type3 x1 hterm h1 =
2628 let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2630 (** val joint_program_inv_rect_Type2 :
2631 params -> joint_program -> (AST.ident List.list -> (joint_function,
2632 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2634 let joint_program_inv_rect_Type2 x1 hterm h1 =
2635 let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2637 (** val joint_program_inv_rect_Type1 :
2638 params -> joint_program -> (AST.ident List.list -> (joint_function,
2639 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2641 let joint_program_inv_rect_Type1 x1 hterm h1 =
2642 let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2644 (** val joint_program_inv_rect_Type0 :
2645 params -> joint_program -> (AST.ident List.list -> (joint_function,
2646 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2648 let joint_program_inv_rect_Type0 x1 hterm h1 =
2649 let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2651 (** val joint_program_discr :
2652 params -> joint_program -> joint_program -> __ **)
2653 let joint_program_discr a1 x y =
2654 Logic.eq_rect_Type2 x
2655 (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2656 Obj.magic (fun _ dH -> dH __ __ __ __)) y
2658 (** val joint_program_jmdiscr :
2659 params -> joint_program -> joint_program -> __ **)
2660 let joint_program_jmdiscr a1 x y =
2661 Logic.eq_rect_Type2 x
2662 (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2663 Obj.magic (fun _ dH -> dH __ __ __ __)) y
2665 (** val dpi1__o__joint_prog__o__inject :
2666 params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2667 AST.init_data List.list) AST.program Types.sig0 **)
2668 let dpi1__o__joint_prog__o__inject x0 x2 =
2669 x2.Types.dpi1.joint_prog
2671 (** val eject__o__joint_prog__o__inject :
2672 params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2673 List.list) AST.program Types.sig0 **)
2674 let eject__o__joint_prog__o__inject x0 x2 =
2675 (Types.pi1 x2).joint_prog
2677 (** val joint_prog__o__inject :
2678 params -> joint_program -> (joint_function, AST.init_data List.list)
2679 AST.program Types.sig0 **)
2680 let joint_prog__o__inject x0 x1 =
2683 (** val dpi1__o__joint_prog :
2684 params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2685 AST.init_data List.list) AST.program **)
2686 let dpi1__o__joint_prog x0 x2 =
2687 x2.Types.dpi1.joint_prog
2689 (** val eject__o__joint_prog :
2690 params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2691 List.list) AST.program **)
2692 let eject__o__joint_prog x0 x2 =
2693 (Types.pi1 x2).joint_prog
2695 (** val prog_names : params -> joint_program -> AST.ident List.list **)
2696 let prog_names pars p =
2697 List.append (AST.prog_var_names p.joint_prog) p.jp_functions
2699 (** val transform_joint_program :
2700 params -> params -> (AST.ident List.list ->
2701 joint_closed_internal_function -> joint_closed_internal_function) ->
2702 joint_program -> joint_program **)
2703 let transform_joint_program src dst trans prog_in =
2704 { jp_functions = prog_in.jp_functions; joint_prog =
2705 (AST.transform_program prog_in.joint_prog (fun vars ->
2706 AST.transf_fundef (trans (List.append vars prog_in.jp_functions))));
2707 init_cost_label = prog_in.init_cost_label }
2709 type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2711 (** val stack_cost : params -> joint_program -> stack_cost_model **)
2712 let stack_cost p pr =
2713 List.foldr (fun id_fun acc ->
2714 let { Types.fst = id; Types.snd = fun0 } = id_fun in
2716 | AST.Internal jif ->
2717 List.Cons ({ Types.fst = id; Types.snd =
2718 (Types.pi1 jif).joint_if_stacksize }, acc)
2719 | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
2735 (** val globals_stacksize : params -> joint_program -> Nat.nat **)
2736 let globals_stacksize pars p =
2737 List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2738 Globalenvs.size_init_data_list entry.Types.snd)
2739 p.joint_prog.AST.prog_vars