include "joint/Joint_paolo.ma".

inductive rtl_argument : Type[0] ≝ 
  | Reg : register → rtl_argument
  | Imm : Byte → rtl_argument.
  
coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
  on _r : register to rtl_argument.

coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
  on _b : Byte to rtl_argument.

definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
  
coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
  on _n : nat to rtl_argument.

inductive rtl_step_extension: Type[0] ≝
  | rtl_st_ext_stack_address: register → register → rtl_step_extension
  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.

inductive rtl_statement_extension : Type[0] ≝
  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.

definition rtl_uns_params ≝ mk_unserialized_params
  (mk_step_params
    (* acc_a_reg ≝ *) register
    (* acc_b_reg ≝ *) register
    (* acc_a_arg ≝ *) rtl_argument
    (* acc_b_arg ≝ *) rtl_argument
    (* dpl_reg   ≝ *) register
    (* dph_reg   ≝ *) register
    (* dpl_arg   ≝ *) rtl_argument
    (* dph_arg   ≝ *) rtl_argument
    (* snd_arg   ≝ *) rtl_argument
    (* pair_move ≝ *) (register × rtl_argument)
    (* call_args ≝ *) (list rtl_argument)
    (* call_dest ≝ *) (list register)
    (* ext_step ≝ *) rtl_step_extension
    (* ext_step_labels ≝ *) (λes.[ ])
    (* ext_fin_stmt ≝ *) rtl_statement_extension
    (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
  (mk_local_params
    (mk_funct_params
      (* resultT ≝ *) (list register)
      (* paramsT ≝ *) (list register))
      (* localsT ≝ *) (list register)).

definition rtl_params ≝ mk_graph_params rtl_uns_params.
definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
definition rtl_internal_function ≝
  λglobals. joint_internal_function globals rtl_params.
definition rtl_program ≝ joint_program rtl_params.
definition rtl_step ≝ joint_step rtl_params.
definition rtl_statement ≝ joint_statement rtl_params.


interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).

(* aid unification *)
include "hints_declaration.ma".
unification hint 0 ≔
(*---------------*) ⊢
acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
unification hint 0 ≔
(*---------------*) ⊢
acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
unification hint 0 ≔
(*---------------*) ⊢
acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
unification hint 0 ≔
(*---------------*) ⊢
dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
unification hint 0 ≔
(*---------------*) ⊢
dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
unification hint 0 ≔
(*---------------*) ⊢
call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.

unification hint 0 ≔
(*---------------*) ⊢
ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
unification hint 0 ≔ globals
(*---------------*) ⊢
joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.

unification hint 0 ≔
(*---------------*) ⊢
ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
unification hint 0 ≔ globals
(*---------------*) ⊢
joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.

(************ Same without 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 ≝ mk_graph_params (mk_unserialized_params
  (mk_step_params
    (* acc_a_reg ≝ *) register
    (* acc_b_reg ≝ *) register
    (* acc_a_arg ≝ *) rtl_argument
    (* acc_b_arg ≝ *) rtl_argument
    (* dpl_reg   ≝ *) register
    (* dph_reg   ≝ *) register
    (* dpl_arg   ≝ *) rtl_argument
    (* dph_arg   ≝ *) rtl_argument
    (* snd_arg   ≝ *) rtl_argument
    (* pair_move ≝ *) (register × rtl_argument)
    (* call_args ≝ *) (list rtl_argument)
    (* call_dest ≝ *) (list register)
    (* extend_statements ≝ *) rtlntc_statement_extension
    (* ext_forall_labels ≝ *) (λes.[ ])
    void (λes.[ ]))
  (mk_local_params
    (mk_funct_params
      (* resultT ≝ *) (list register)
      (* paramsT ≝ *) (list register))
      (* localsT ≝ *) (list register))).

definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).

definition rtlntc_internal_function ≝
  λglobals. joint_internal_function … globals rtlntc_params.

definition rtlntc_program ≝ joint_program rtlntc_params.