99 open Hints_declaration
122 | PSD of Registers.register
123 | HDW of I8051.register
125 (** val move_dst_rect_Type4 :
126 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
127 let rec move_dst_rect_Type4 h_PSD h_HDW = function
128 | PSD x_18499 -> h_PSD x_18499
129 | HDW x_18500 -> h_HDW x_18500
131 (** val move_dst_rect_Type5 :
132 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
133 let rec move_dst_rect_Type5 h_PSD h_HDW = function
134 | PSD x_18504 -> h_PSD x_18504
135 | HDW x_18505 -> h_HDW x_18505
137 (** val move_dst_rect_Type3 :
138 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
139 let rec move_dst_rect_Type3 h_PSD h_HDW = function
140 | PSD x_18509 -> h_PSD x_18509
141 | HDW x_18510 -> h_HDW x_18510
143 (** val move_dst_rect_Type2 :
144 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
145 let rec move_dst_rect_Type2 h_PSD h_HDW = function
146 | PSD x_18514 -> h_PSD x_18514
147 | HDW x_18515 -> h_HDW x_18515
149 (** val move_dst_rect_Type1 :
150 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
151 let rec move_dst_rect_Type1 h_PSD h_HDW = function
152 | PSD x_18519 -> h_PSD x_18519
153 | HDW x_18520 -> h_HDW x_18520
155 (** val move_dst_rect_Type0 :
156 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
157 let rec move_dst_rect_Type0 h_PSD h_HDW = function
158 | PSD x_18524 -> h_PSD x_18524
159 | HDW x_18525 -> h_HDW x_18525
161 (** val move_dst_inv_rect_Type4 :
162 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
164 let move_dst_inv_rect_Type4 hterm h1 h2 =
165 let hcut = move_dst_rect_Type4 h1 h2 hterm in hcut __
167 (** val move_dst_inv_rect_Type3 :
168 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
170 let move_dst_inv_rect_Type3 hterm h1 h2 =
171 let hcut = move_dst_rect_Type3 h1 h2 hterm in hcut __
173 (** val move_dst_inv_rect_Type2 :
174 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
176 let move_dst_inv_rect_Type2 hterm h1 h2 =
177 let hcut = move_dst_rect_Type2 h1 h2 hterm in hcut __
179 (** val move_dst_inv_rect_Type1 :
180 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
182 let move_dst_inv_rect_Type1 hterm h1 h2 =
183 let hcut = move_dst_rect_Type1 h1 h2 hterm in hcut __
185 (** val move_dst_inv_rect_Type0 :
186 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
188 let move_dst_inv_rect_Type0 hterm h1 h2 =
189 let hcut = move_dst_rect_Type0 h1 h2 hterm in hcut __
191 (** val move_dst_discr : move_dst -> move_dst -> __ **)
192 let move_dst_discr x y =
193 Logic.eq_rect_Type2 x
195 | PSD a0 -> Obj.magic (fun _ dH -> dH __)
196 | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
198 (** val move_dst_jmdiscr : move_dst -> move_dst -> __ **)
199 let move_dst_jmdiscr x y =
200 Logic.eq_rect_Type2 x
202 | PSD a0 -> Obj.magic (fun _ dH -> dH __)
203 | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
205 type move_src = move_dst Joint.argument
207 (** val move_src_from_dst : move_dst -> move_src **)
208 let move_src_from_dst x =
211 (** val dpi1__o__move_dst_to_src__o__inject :
212 (move_dst, 'a1) Types.dPair -> move_src Types.sig0 **)
213 let dpi1__o__move_dst_to_src__o__inject x2 =
214 move_src_from_dst x2.Types.dpi1
216 (** val eject__o__move_dst_to_src__o__inject :
217 move_dst Types.sig0 -> move_src Types.sig0 **)
218 let eject__o__move_dst_to_src__o__inject x2 =
219 move_src_from_dst (Types.pi1 x2)
221 (** val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0 **)
222 let move_dst_to_src__o__inject x1 =
225 (** val dpi1__o__move_dst_to_src :
226 (move_dst, 'a1) Types.dPair -> move_src **)
227 let dpi1__o__move_dst_to_src x1 =
228 move_src_from_dst x1.Types.dpi1
230 (** val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src **)
231 let eject__o__move_dst_to_src x1 =
232 move_src_from_dst (Types.pi1 x1)
234 (** val psd_argument_move_src : Joint.psd_argument -> move_src **)
235 let psd_argument_move_src = function
236 | Joint.Reg r -> Joint.Reg (PSD r)
237 | Joint.Imm b -> Joint.Imm b
239 (** val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
240 BitVector.byte -> move_src Types.sig0 **)
241 let byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
242 psd_argument_move_src (Joint.psd_argument_from_byte x0)
244 (** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
245 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
246 let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
247 psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x2)
249 (** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
250 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
251 let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
252 psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x2)
254 (** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
255 (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
256 let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
257 psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x2)
259 (** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
260 BitVector.byte Types.sig0 -> move_src Types.sig0 **)
261 let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
262 psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x2)
264 (** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
265 BitVector.byte Types.sig0 -> move_src Types.sig0 **)
266 let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
267 psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x2)
269 (** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
270 Registers.register Types.sig0 -> move_src Types.sig0 **)
271 let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
272 psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x2)
274 (** val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
275 Registers.register -> move_src Types.sig0 **)
276 let reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
277 psd_argument_move_src (Joint.psd_argument_from_reg x0)
279 (** val dpi1__o__psd_argument_to_move_src__o__inject :
280 (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0 **)
281 let dpi1__o__psd_argument_to_move_src__o__inject x2 =
282 psd_argument_move_src x2.Types.dpi1
284 (** val eject__o__psd_argument_to_move_src__o__inject :
285 Joint.psd_argument Types.sig0 -> move_src Types.sig0 **)
286 let eject__o__psd_argument_to_move_src__o__inject x2 =
287 psd_argument_move_src (Types.pi1 x2)
289 (** val psd_argument_to_move_src__o__inject :
290 Joint.psd_argument -> move_src Types.sig0 **)
291 let psd_argument_to_move_src__o__inject x1 =
292 psd_argument_move_src x1
294 (** val byte_to_psd_argument__o__psd_argument_to_move_src :
295 BitVector.byte -> move_src **)
296 let byte_to_psd_argument__o__psd_argument_to_move_src x0 =
297 psd_argument_move_src (Joint.psd_argument_from_byte x0)
299 (** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
300 (BitVector.byte, 'a1) Types.dPair -> move_src **)
301 let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
302 psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x1)
304 (** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
305 (BitVector.byte, 'a1) Types.dPair -> move_src **)
306 let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
307 psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x1)
309 (** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
310 (Registers.register, 'a1) Types.dPair -> move_src **)
311 let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
312 psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x1)
314 (** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
315 BitVector.byte Types.sig0 -> move_src **)
316 let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
317 psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x1)
319 (** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
320 BitVector.byte Types.sig0 -> move_src **)
321 let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
322 psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x1)
324 (** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
325 Registers.register Types.sig0 -> move_src **)
326 let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
327 psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x1)
329 (** val reg_to_psd_argument__o__psd_argument_to_move_src :
330 Registers.register -> move_src **)
331 let reg_to_psd_argument__o__psd_argument_to_move_src x0 =
332 psd_argument_move_src (Joint.psd_argument_from_reg x0)
334 (** val dpi1__o__psd_argument_to_move_src :
335 (Joint.psd_argument, 'a1) Types.dPair -> move_src **)
336 let dpi1__o__psd_argument_to_move_src x1 =
337 psd_argument_move_src x1.Types.dpi1
339 (** val eject__o__psd_argument_to_move_src :
340 Joint.psd_argument Types.sig0 -> move_src **)
341 let eject__o__psd_argument_to_move_src x1 =
342 psd_argument_move_src (Types.pi1 x1)
347 | Ertl_frame_size of Registers.register
349 (** val ertl_seq_rect_Type4 :
350 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
351 let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
352 | Ertl_new_frame -> h_ertl_new_frame
353 | Ertl_del_frame -> h_ertl_del_frame
354 | Ertl_frame_size x_18564 -> h_ertl_frame_size x_18564
356 (** val ertl_seq_rect_Type5 :
357 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
358 let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
359 | Ertl_new_frame -> h_ertl_new_frame
360 | Ertl_del_frame -> h_ertl_del_frame
361 | Ertl_frame_size x_18569 -> h_ertl_frame_size x_18569
363 (** val ertl_seq_rect_Type3 :
364 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
365 let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
366 | Ertl_new_frame -> h_ertl_new_frame
367 | Ertl_del_frame -> h_ertl_del_frame
368 | Ertl_frame_size x_18574 -> h_ertl_frame_size x_18574
370 (** val ertl_seq_rect_Type2 :
371 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
372 let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
373 | Ertl_new_frame -> h_ertl_new_frame
374 | Ertl_del_frame -> h_ertl_del_frame
375 | Ertl_frame_size x_18579 -> h_ertl_frame_size x_18579
377 (** val ertl_seq_rect_Type1 :
378 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
379 let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
380 | Ertl_new_frame -> h_ertl_new_frame
381 | Ertl_del_frame -> h_ertl_del_frame
382 | Ertl_frame_size x_18584 -> h_ertl_frame_size x_18584
384 (** val ertl_seq_rect_Type0 :
385 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
386 let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
387 | Ertl_new_frame -> h_ertl_new_frame
388 | Ertl_del_frame -> h_ertl_del_frame
389 | Ertl_frame_size x_18589 -> h_ertl_frame_size x_18589
391 (** val ertl_seq_inv_rect_Type4 :
392 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
394 let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
395 let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __
397 (** val ertl_seq_inv_rect_Type3 :
398 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
400 let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
401 let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __
403 (** val ertl_seq_inv_rect_Type2 :
404 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
406 let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
407 let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __
409 (** val ertl_seq_inv_rect_Type1 :
410 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
412 let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
413 let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __
415 (** val ertl_seq_inv_rect_Type0 :
416 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
418 let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
419 let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __
421 (** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
422 let ertl_seq_discr x y =
423 Logic.eq_rect_Type2 x
425 | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
426 | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
427 | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
429 (** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
430 let ertl_seq_jmdiscr x y =
431 Logic.eq_rect_Type2 x
433 | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
434 | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
435 | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
437 (** val eRTL_uns : Joint.unserialized_params **)
439 { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
442 (** val regs_from_move_dst : move_dst -> Registers.register List.list **)
443 let regs_from_move_dst = function
444 | PSD r -> List.Cons (r, List.Nil)
447 (** val regs_from_move_src : move_src -> Registers.register List.list **)
448 let regs_from_move_src = function
451 | PSD r1 -> List.Cons (r1, List.Nil)
453 | Joint.Imm x -> List.Nil
455 (** val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list **)
456 let ertl_ext_seq_regs = function
457 | Ertl_new_frame -> List.Nil
458 | Ertl_del_frame -> List.Nil
459 | Ertl_frame_size r -> List.Cons (r, List.Nil)
461 (** val eRTL_functs : Joint.get_pseudo_reg_functs **)
463 { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
464 Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
465 Joint.acc_a_args = (fun arg ->
466 match Obj.magic arg with
467 | Joint.Reg r -> List.Cons (r, List.Nil)
468 | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
469 match Obj.magic arg with
470 | Joint.Reg r -> List.Cons (r, List.Nil)
471 | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
472 ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
473 ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
474 match Obj.magic arg with
475 | Joint.Reg r -> List.Cons (r, List.Nil)
476 | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
477 match Obj.magic arg with
478 | Joint.Reg r -> List.Cons (r, List.Nil)
479 | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
480 match Obj.magic arg with
481 | Joint.Reg r -> List.Cons (r, List.Nil)
482 | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
483 List.append (regs_from_move_dst (Obj.magic x).Types.fst)
484 (regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
485 (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
486 Joint.ext_seq_regs = (Obj.magic ertl_ext_seq_regs); Joint.params_regs =
487 (fun x -> List.Nil) }
489 (** val eRTL : Joint.graph_params **)
491 { Joint.u_pars = eRTL_uns; Joint.functs = eRTL_functs }
493 type ertl_program = Joint.joint_program
495 (** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
496 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
497 let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
498 Joint.psd_argument_from_reg x2.Types.dpi1
500 (** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
501 (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
502 let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
503 psd_argument_to_move_src__o__inject
504 (Joint.psd_argument_from_reg x2.Types.dpi1)
506 (** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
507 (Registers.register, 'a1) Types.dPair -> move_src **)
508 let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
509 psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)
511 (** val eject__o__reg_to_ertl_snd_argument__o__inject :
512 Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
513 let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
514 Joint.psd_argument_from_reg (Types.pi1 x2)
516 (** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
517 Registers.register Types.sig0 -> move_src Types.sig0 **)
518 let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
519 psd_argument_to_move_src__o__inject
520 (Joint.psd_argument_from_reg (Types.pi1 x2))
522 (** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
523 Registers.register Types.sig0 -> move_src **)
524 let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
525 psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))
527 (** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
528 Registers.register -> move_src **)
529 let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
530 psd_argument_move_src (Joint.psd_argument_from_reg x0)
532 (** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
533 Registers.register -> move_src Types.sig0 **)
534 let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
535 psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)
537 (** val reg_to_ertl_snd_argument__o__inject :
538 Registers.register -> Joint.psd_argument Types.sig0 **)
539 let reg_to_ertl_snd_argument__o__inject x1 =
540 Joint.psd_argument_from_reg x1
542 (** val dpi1__o__reg_to_ertl_snd_argument :
543 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
544 let dpi1__o__reg_to_ertl_snd_argument x1 =
545 Joint.psd_argument_from_reg x1.Types.dpi1
547 (** val eject__o__reg_to_ertl_snd_argument :
548 Registers.register Types.sig0 -> Joint.psd_argument **)
549 let eject__o__reg_to_ertl_snd_argument x1 =
550 Joint.psd_argument_from_reg (Types.pi1 x1)
552 (** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
553 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
554 let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
555 Joint.psd_argument_from_byte x2.Types.dpi1
557 (** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
558 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
559 let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
560 psd_argument_to_move_src__o__inject
561 (Joint.psd_argument_from_byte x2.Types.dpi1)
563 (** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
564 (BitVector.byte, 'a1) Types.dPair -> move_src **)
565 let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
566 psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)
568 (** val eject__o__byte_to_ertl_snd_argument__o__inject :
569 BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
570 let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
571 Joint.psd_argument_from_byte (Types.pi1 x2)
573 (** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
574 BitVector.byte Types.sig0 -> move_src Types.sig0 **)
575 let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
576 psd_argument_to_move_src__o__inject
577 (Joint.psd_argument_from_byte (Types.pi1 x2))
579 (** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
580 BitVector.byte Types.sig0 -> move_src **)
581 let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
582 psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))
584 (** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
585 BitVector.byte -> move_src **)
586 let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
587 psd_argument_move_src (Joint.psd_argument_from_byte x0)
589 (** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
590 BitVector.byte -> move_src Types.sig0 **)
591 let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
592 psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)
594 (** val byte_to_ertl_snd_argument__o__inject :
595 BitVector.byte -> Joint.psd_argument Types.sig0 **)
596 let byte_to_ertl_snd_argument__o__inject x1 =
597 Joint.psd_argument_from_byte x1
599 (** val dpi1__o__byte_to_ertl_snd_argument :
600 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
601 let dpi1__o__byte_to_ertl_snd_argument x1 =
602 Joint.psd_argument_from_byte x1.Types.dpi1
604 (** val eject__o__byte_to_ertl_snd_argument :
605 BitVector.byte Types.sig0 -> Joint.psd_argument **)
606 let eject__o__byte_to_ertl_snd_argument x1 =
607 Joint.psd_argument_from_byte (Types.pi1 x1)
609 (** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
611 Obj.magic (fun _ x -> Joint.Extension_seq x)
613 (** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
614 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
616 let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
617 ertl_seq_joint x1 x2.Types.dpi1
619 (** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
620 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
622 let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
623 Joint.seq_to_step__o__inject
624 (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
625 (ertl_seq_joint x1 x2.Types.dpi1)
627 (** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
628 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
629 let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
630 Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)
632 (** val eject__o__ertl_seq_to_joint_seq__o__inject :
633 AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
634 let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
635 ertl_seq_joint x1 (Types.pi1 x2)
637 (** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
638 AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
639 let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
640 Joint.seq_to_step__o__inject
641 (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
642 (ertl_seq_joint x1 (Types.pi1 x2))
644 (** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
645 AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
646 let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
647 Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))
649 (** val ertl_seq_to_joint_seq__o__seq_to_step :
650 AST.ident List.list -> __ -> Joint.joint_step **)
651 let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
652 Joint.Step_seq (ertl_seq_joint x0 x1)
654 (** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
655 AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
656 let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
657 Joint.seq_to_step__o__inject
658 (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x0
659 (ertl_seq_joint x0 x1)
661 (** val ertl_seq_to_joint_seq__o__inject :
662 AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
663 let ertl_seq_to_joint_seq__o__inject x0 x1 =
666 (** val dpi1__o__ertl_seq_to_joint_seq :
667 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
668 let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
669 ertl_seq_joint x1 x2.Types.dpi1
671 (** val eject__o__ertl_seq_to_joint_seq :
672 AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
673 let eject__o__ertl_seq_to_joint_seq x1 x2 =
674 ertl_seq_joint x1 (Types.pi1 x2)
676 (** val eRTL_premain :
677 ertl_program -> Joint.joint_closed_internal_function **)
679 let l1 = Positive.One in
680 let l2 = Positive.P0 Positive.One in
681 let l3 = Positive.P1 Positive.One in
682 let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
683 Positive.One)); Joint.joint_if_runiverse = Positive.One;
684 Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
685 (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
686 Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
687 Joint.joint_if_code =
688 (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
689 Joint.joint_if_entry = (Obj.magic l1) }
693 (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l1
694 (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
699 (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l2
700 (Joint.Sequential ((Joint.CALL ((Types.Inl
701 p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
702 (Obj.magic Types.It))), (Obj.magic l3))) res0
706 (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l3
707 (Joint.Final (Joint.GOTO l3)) res1