| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | inductive registers_move: Type[0] ≝ |
|---|
| 4 | | from_acc: Register → unit → registers_move |
|---|
| 5 | | to_acc: unit → Register → registers_move |
|---|
| 6 | | int_to_reg : Register → Byte → registers_move |
|---|
| 7 | | int_to_acc : unit → Byte → registers_move. |
|---|
| 8 | (* the last is redudant, but kept for notation's sake *) |
|---|
| 9 | |
|---|
| 10 | inductive ltl_lin_seq : Type[0] ≝ |
|---|
| 11 | | SAVE_CARRY : ltl_lin_seq |
|---|
| 12 | | RESTORE_CARRY : ltl_lin_seq |
|---|
| 13 | | LOW_ADDRESS : Register → label → ltl_lin_seq |
|---|
| 14 | | HIGH_ADDRESS : Register → label → ltl_lin_seq. |
|---|
| 15 | |
|---|
| 16 | definition ltl_lin_seq_labels ≝ λs.match s with |
|---|
| 17 | [ LOW_ADDRESS _ lbl ⇒ [ lbl ] |
|---|
| 18 | | HIGH_ADDRESS _ lbl ⇒ [ lbl ] |
|---|
| 19 | | _ ⇒ [ ] |
|---|
| 20 | ]. |
|---|
| 21 | |
|---|
| 22 | definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params |
|---|
| 23 | (* acc_a_reg ≝ *) unit |
|---|
| 24 | (* acc_b_reg ≝ *) unit |
|---|
| 25 | (* acc_a_arg ≝ *) unit |
|---|
| 26 | (* acc_b_arg ≝ *) unit |
|---|
| 27 | (* dpl_reg ≝ *) unit |
|---|
| 28 | (* dph_reg ≝ *) unit |
|---|
| 29 | (* dpl_arg ≝ *) unit |
|---|
| 30 | (* dph_arg ≝ *) unit |
|---|
| 31 | (* snd_arg ≝ *) hdw_argument |
|---|
| 32 | (* pair_move ≝ *) registers_move |
|---|
| 33 | (* call_args ≝ *) ℕ |
|---|
| 34 | (* call_dest ≝ *) unit |
|---|
| 35 | (* ext_seq ≝ *) ltl_lin_seq |
|---|
| 36 | (* ext_seq_labels ≝ *) ltl_lin_seq_labels |
|---|
| 37 | (* has_tailcalls ≝ *) false |
|---|
| 38 | (* paramsT ≝ *) unit. |
|---|
| 39 | |
|---|
| 40 | definition LTL_LIN_functs : get_pseudo_reg_functs LTL_LIN_uns ≝ |
|---|
| 41 | mk_get_pseudo_reg_functs ? |
|---|
| 42 | (* acc_a_regs *) (λ_.[ ]) |
|---|
| 43 | (* acc_b_regs *) (λ_.[ ]) |
|---|
| 44 | (* acc_a_args *) (λ_.[ ]) |
|---|
| 45 | (* acc_b_args *) (λ_.[ ]) |
|---|
| 46 | (* dpl_regs *) (λ_.[ ]) |
|---|
| 47 | (* dph_regs *) (λ_.[ ]) |
|---|
| 48 | (* dpl_args *) (λ_.[ ]) |
|---|
| 49 | (* dph_args *) (λ_.[ ]) |
|---|
| 50 | (* snd_args *) (λ_.[ ]) |
|---|
| 51 | (* pair_move_regs *) (λ_.[ ]) |
|---|
| 52 | (* f_call_args *) (λ_.[ ]) |
|---|
| 53 | (* f_call_dest *) (λ_.[ ]) |
|---|
| 54 | (* ext_seq_regs *) (λ_.[ ]) |
|---|
| 55 | (* params_regs *) (λ_.[ ]). |
|---|
| 56 | |
|---|
| 57 | definition LTL_LIN ≝ mk_uns_params LTL_LIN_uns LTL_LIN_functs. |
|---|
| 58 | |
|---|
| 59 | interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). |
|---|
| 60 | interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)). |
|---|
| 61 | interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)). |
|---|
| 62 | interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)). |
|---|
