[2162] | 1 | include "joint/Joint_paolo.ma". |
---|
| 2 | include "RTL/RTL_paolo.ma". |
---|
| 3 | |
---|
| 4 | inductive move_dst: Type[0] ≝ |
---|
| 5 | | PSD: register → move_dst |
---|
| 6 | | HDW: Register → move_dst. |
---|
| 7 | |
---|
| 8 | inductive move_src: Type[0] ≝ |
---|
| 9 | | INT: Byte → move_src |
---|
| 10 | | REG: move_dst → move_src. |
---|
| 11 | |
---|
| 12 | coercion move_dst_to_src : ∀r : move_dst.move_src ≝ REG on _r : move_dst to move_src. |
---|
| 13 | |
---|
| 14 | definition rtl_argument_move_src : rtl_argument → move_src ≝ |
---|
| 15 | λarg.match arg with |
---|
| 16 | [ Imm b ⇒ INT b |
---|
| 17 | | Reg r ⇒ REG (PSD r) |
---|
| 18 | ]. |
---|
| 19 | |
---|
| 20 | coercion rtl_argument_to_move_src : ∀a:rtl_argument.move_src ≝ |
---|
| 21 | rtl_argument_move_src on _a : rtl_argument to move_src. |
---|
| 22 | |
---|
| 23 | inductive ertl_seq : Type[0] ≝ |
---|
| 24 | | ertl_new_frame: ertl_seq |
---|
| 25 | | ertl_del_frame: ertl_seq |
---|
| 26 | | ertl_frame_size: register → ertl_seq. |
---|
| 27 | |
---|
| 28 | definition ertl_uns_params ≝ mk_unserialized_params |
---|
| 29 | (mk_step_params |
---|
| 30 | (* acc_a_reg ≝ *) register |
---|
| 31 | (* acc_b_reg ≝ *) register |
---|
| 32 | (* acc_a_arg ≝ *) rtl_argument |
---|
| 33 | (* acc_b_arg ≝ *) rtl_argument |
---|
| 34 | (* dpl_reg ≝ *) register |
---|
| 35 | (* dph_reg ≝ *) register |
---|
| 36 | (* dpl_arg ≝ *) rtl_argument |
---|
| 37 | (* dph_arg ≝ *) rtl_argument |
---|
| 38 | (* snd_arg ≝ *) rtl_argument |
---|
| 39 | (* pair_move ≝ *) (move_dst × move_src) |
---|
| 40 | (* call_args ≝ *) ℕ |
---|
| 41 | (* call_dest ≝ *) unit |
---|
| 42 | (* ext_seq ≝ *) ertl_seq |
---|
| 43 | (* ext_call ≝ *) void |
---|
| 44 | (* ext_tailcall ≝ *) void |
---|
| 45 | ) |
---|
| 46 | (mk_local_params |
---|
| 47 | (mk_funct_params |
---|
[2174] | 48 | (* resultT ≝ *) unit |
---|
[2162] | 49 | (* paramsT ≝ *) ℕ) |
---|
| 50 | (* localsT ≝ *) register). |
---|
| 51 | |
---|
| 52 | definition ertl_params ≝ mk_graph_params ertl_uns_params. |
---|
| 53 | definition ertl_internal_function ≝ |
---|
| 54 | λglobals. joint_internal_function globals ertl_params. |
---|
| 55 | definition ertl_program ≝ joint_program ertl_params. |
---|
| 56 | |
---|
| 57 | interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). |
---|
| 58 | |
---|
| 59 | (* aid unification *) |
---|
| 60 | unification hint 0 ≔ |
---|
| 61 | (*---------------*) ⊢ |
---|
| 62 | pair_move ertl_params ≡ move_dst × move_src. |
---|
| 63 | unification hint 0 ≔ |
---|
| 64 | (*---------------*) ⊢ |
---|
| 65 | acc_a_reg ertl_params ≡ register. |
---|
| 66 | unification hint 0 ≔ |
---|
| 67 | (*---------------*) ⊢ |
---|
| 68 | acc_b_reg ertl_params ≡ register. |
---|
| 69 | unification hint 0 ≔ |
---|
| 70 | (*---------------*) ⊢ |
---|
| 71 | acc_a_arg ertl_params ≡ rtl_argument. |
---|
| 72 | unification hint 0 ≔ |
---|
| 73 | (*---------------*) ⊢ |
---|
| 74 | acc_b_arg ertl_params ≡ rtl_argument. |
---|
| 75 | unification hint 0 ≔ |
---|
| 76 | (*---------------*) ⊢ |
---|
| 77 | dpl_reg ertl_params ≡ register. |
---|
| 78 | unification hint 0 ≔ |
---|
| 79 | (*---------------*) ⊢ |
---|
| 80 | dph_reg ertl_params ≡ register. |
---|
| 81 | unification hint 0 ≔ |
---|
| 82 | (*---------------*) ⊢ |
---|
| 83 | dpl_arg ertl_params ≡ rtl_argument. |
---|
| 84 | unification hint 0 ≔ |
---|
| 85 | (*---------------*) ⊢ |
---|
| 86 | dph_arg ertl_params ≡ rtl_argument. |
---|
| 87 | unification hint 0 ≔ |
---|
| 88 | (*---------------*) ⊢ |
---|
| 89 | snd_arg ertl_params ≡ rtl_argument. |
---|
| 90 | unification hint 0 ≔ |
---|
| 91 | (*---------------*) ⊢ |
---|
| 92 | call_args ertl_params ≡ ℕ. |
---|
| 93 | unification hint 0 ≔ |
---|
| 94 | (*---------------*) ⊢ |
---|
| 95 | call_dest ertl_params ≡ unit. |
---|
| 96 | |
---|
| 97 | unification hint 0 ≔ |
---|
| 98 | (*---------------*) ⊢ |
---|
| 99 | ext_seq ertl_params ≡ ertl_seq. |
---|
| 100 | unification hint 0 ≔ |
---|
| 101 | (*---------------*) ⊢ |
---|
| 102 | ext_call ertl_params ≡ void. |
---|
| 103 | unification hint 0 ≔ |
---|
| 104 | (*---------------*) ⊢ |
---|
| 105 | ext_tailcall ertl_params ≡ void. |
---|
| 106 | |
---|
| 107 | coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝ Reg |
---|
| 108 | on _r : register to snd_arg ertl_params. |
---|
| 109 | coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝ Imm |
---|
| 110 | on _b : Byte to snd_arg ertl_params. |
---|
| 111 | |
---|
| 112 | definition ertl_seq_joint ≝ extension_seq ertl_params. |
---|
| 113 | coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint |
---|
| 114 | on _s : ertl_seq to joint_seq ertl_params. |
---|
| 115 | |
---|