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 | (* store low/high parts of label address in the accumulator *) |
---|

14 | | LOW_ADDRESS : label → ltl_lin_seq |
---|

15 | | HIGH_ADDRESS : label → ltl_lin_seq. |
---|

16 | |
---|

17 | definition ltl_lin_seq_labels ≝ λs.match s with |
---|

18 | [ LOW_ADDRESS lbl ⇒ [ lbl ] |
---|

19 | | HIGH_ADDRESS lbl ⇒ [ lbl ] |
---|

20 | | _ ⇒ [ ] |
---|

21 | ]. |
---|

22 | |
---|

23 | definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params |
---|

24 | (* acc_a_reg ≝ *) unit |
---|

25 | (* acc_b_reg ≝ *) unit |
---|

26 | (* acc_a_arg ≝ *) unit |
---|

27 | (* acc_b_arg ≝ *) unit |
---|

28 | (* dpl_reg ≝ *) unit |
---|

29 | (* dph_reg ≝ *) unit |
---|

30 | (* dpl_arg ≝ *) unit |
---|

31 | (* dph_arg ≝ *) unit |
---|

32 | (* snd_arg ≝ *) hdw_argument |
---|

33 | (* pair_move ≝ *) registers_move |
---|

34 | (* call_args ≝ *) ℕ |
---|

35 | (* call_dest ≝ *) unit |
---|

36 | (* ext_seq ≝ *) ltl_lin_seq |
---|

37 | (* ext_seq_labels ≝ *) ltl_lin_seq_labels |
---|

38 | (* has_tailcalls ≝ *) false |
---|

39 | (* paramsT ≝ *) unit. |
---|

40 | |
---|

41 | definition LTL_LIN_functs : get_pseudo_reg_functs LTL_LIN_uns ≝ |
---|

42 | mk_get_pseudo_reg_functs ? |
---|

43 | (* acc_a_regs *) (λ_.[ ]) |
---|

44 | (* acc_b_regs *) (λ_.[ ]) |
---|

45 | (* acc_a_args *) (λ_.[ ]) |
---|

46 | (* acc_b_args *) (λ_.[ ]) |
---|

47 | (* dpl_regs *) (λ_.[ ]) |
---|

48 | (* dph_regs *) (λ_.[ ]) |
---|

49 | (* dpl_args *) (λ_.[ ]) |
---|

50 | (* dph_args *) (λ_.[ ]) |
---|

51 | (* snd_args *) (λ_.[ ]) |
---|

52 | (* pair_move_regs *) (λ_.[ ]) |
---|

53 | (* f_call_args *) (λ_.[ ]) |
---|

54 | (* f_call_dest *) (λ_.[ ]) |
---|

55 | (* ext_seq_regs *) (λ_.[ ]) |
---|

56 | (* params_regs *) (λ_.[ ]). |
---|

57 | |
---|

58 | definition LTL_LIN ≝ mk_uns_params LTL_LIN_uns LTL_LIN_functs. |
---|

59 | |
---|

60 | interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). |
---|

61 | interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)). |
---|

62 | interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)). |
---|

63 | interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)). |
---|