| 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 |
|---|
| 48 | (* resultT ≝ *) unit |
|---|
| 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 | |
|---|
