include "joint/Joint.ma".

inductive registers_move: Type[0] ≝
 | from_acc: Register → unit → registers_move
 | to_acc: unit → Register → registers_move
 | int_to_reg : Register → Byte → registers_move
 | int_to_acc : unit → Byte → registers_move.
(* the last is redudant, but kept for notation's sake *)

inductive ltl_lin_seq : Type[0] ≝
| SAVE_CARRY : ltl_lin_seq
| RESTORE_CARRY : ltl_lin_seq
(* store low/high parts of label address in the accumulator *)
| LOW_ADDRESS : label → ltl_lin_seq
| HIGH_ADDRESS : label → ltl_lin_seq.

definition ltl_lin_seq_labels ≝ λs.match s with
[ LOW_ADDRESS lbl ⇒ [ lbl ]
| HIGH_ADDRESS lbl ⇒ [ lbl ]
| _ ⇒ [ ]
].

definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params
    (* acc_a_reg ≝ *) unit
    (* acc_b_reg ≝ *) unit
    (* acc_a_arg ≝ *) unit
    (* acc_b_arg ≝ *) unit
    (* dpl_reg   ≝ *) unit
    (* dph_reg   ≝ *) unit
    (* dpl_arg   ≝ *) unit
    (* dph_arg   ≝ *) unit
    (* snd_arg   ≝ *) hdw_argument
    (* pair_move ≝ *) registers_move
    (* call_args ≝ *) ℕ
    (* call_dest ≝ *) unit
    (* ext_seq ≝ *) ltl_lin_seq
    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
    (* has_tailcalls ≝ *) false
    (* paramsT ≝ *) unit.

definition LTL_LIN_functs : get_pseudo_reg_functs LTL_LIN_uns ≝ 
mk_get_pseudo_reg_functs ? 
(* acc_a_regs *) (λ_.[ ])
(* acc_b_regs *) (λ_.[ ])
(* acc_a_args *) (λ_.[ ])
(* acc_b_args *) (λ_.[ ])
(* dpl_regs *) (λ_.[ ])
(* dph_regs *) (λ_.[ ])
(* dpl_args *) (λ_.[ ])
(* dph_args *) (λ_.[ ])
(* snd_args *) (λ_.[ ])
(* pair_move_regs *) (λ_.[ ])
(* f_call_args *) (λ_.[ ])
(* f_call_dest *) (λ_.[ ])
(* ext_seq_regs *) (λ_.[ ])
(* params_regs *) (λ_.[ ]).

definition LTL_LIN ≝  mk_uns_params LTL_LIN_uns LTL_LIN_functs.

interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).