include "joint/Joint.ma".

(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
  are not sequential. Thus there is a dummy label at the moment in the code.
  To be fixed once we understand exactly what to do with tail calls. *)
inductive rtl_statement_extension: Type[0] ≝
  | rtl_st_ext_stack_address: register → register → rtl_statement_extension
  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.

definition rtl_params__: params__ ≝
 mk_params__ register register register register (register × register) register
  (list register) (list register) rtl_statement_extension.
definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.

definition rtl_statement ≝ joint_statement rtl_params_.

definition rtl_internal_function ≝
  λglobals. joint_internal_function … (rtl_params globals).

definition rtl_program ≝ joint_program rtl_params.

(************ Same without tail calls ****************)

(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
  are not sequential. Thus there is a dummy label at the moment in the code.
  To be fixed once we understand exactly what to do with tail calls. *)
inductive rtlntc_statement_extension: Type[0] ≝
  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.

definition rtlntc_params__: params__ ≝
 mk_params__ register register register register (register × register) register
  (list register) (list register) rtlntc_statement_extension.
definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.

definition rtlntc_statement ≝ joint_statement rtlntc_params_.

definition rtlntc_internal_function ≝
  λglobals. joint_internal_function … (rtlntc_params globals).

definition rtlntc_program ≝ joint_program rtlntc_params.