include "joint/Joint.ma".

inductive move_registers: Type[0] ≝
  | pseudo: register → move_registers
  | hardware: Register → move_registers.
                  
inductive ertl_statement_extension: Type[0] ≝
  | ertl_st_ext_new_frame: ertl_statement_extension
  | ertl_st_ext_del_frame: ertl_statement_extension
  | ertl_st_ext_frame_size: register → ertl_statement_extension.

definition ertl_params__: params__ ≝
 mk_params__ register register register register (move_registers × move_registers)
  register nat unit ertl_statement_extension.
definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.

definition ertl_statement ≝ joint_statement ertl_params_.

definition ertl_internal_function ≝
  λglobals.joint_internal_function … (ertl_params globals).

definition ertl_program ≝ joint_program ertl_params.