[1378] | 1 | include "joint/Joint.ma". |
---|

| 2 | |
---|

| 3 | inductive registers_move: Type[0] ≝ |
---|

[2286] | 4 | | from_acc: Register → unit → registers_move |
---|

| 5 | | to_acc: unit → Register → registers_move |
---|

[2490] | 6 | | int_to_reg : Register → Byte → registers_move |
---|

| 7 | | int_to_acc : unit → Byte → registers_move. |
---|

[2286] | 8 | (* the last is redudant, but kept for notation's sake *) |
---|

[1378] | 9 | |
---|

[2286] | 10 | inductive ltl_lin_seq : Type[0] ≝ |
---|

| 11 | | SAVE_CARRY : ltl_lin_seq |
---|

[2537] | 12 | | RESTORE_CARRY : ltl_lin_seq |
---|

| 13 | | LOW_ADDRESS : Register → label → ltl_lin_seq |
---|

| 14 | | HIGH_ADDRESS : Register → label → ltl_lin_seq. |
---|

[2286] | 15 | |
---|

[2537] | 16 | definition ltl_lin_seq_labels ≝ λs.match s with |
---|

| 17 | [ LOW_ADDRESS _ lbl ⇒ [ lbl ] |
---|

| 18 | | HIGH_ADDRESS _ lbl ⇒ [ lbl ] |
---|

| 19 | | _ ⇒ [ ] |
---|

| 20 | ]. |
---|

| 21 | |
---|

[2783] | 22 | definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params |
---|

[2286] | 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 |
---|

[2537] | 36 | (* ext_seq_labels ≝ *) ltl_lin_seq_labels |
---|

[2490] | 37 | (* has_tailcalls ≝ *) false |
---|

[2645] | 38 | (* paramsT ≝ *) unit. |
---|

[2286] | 39 | |
---|

[2783] | 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 | |
---|

[2286] | 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)). |
---|