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.

definition LTL_LIN : 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
    (* has_tailcalls ≝ *) false
    (* paramsT ≝ *) unit
    (* localsT ≝ *) void.

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)).