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