[1168] | 1 | include "joint/Joint.ma". |
---|
[733] | 2 | |
---|
[2286] | 3 | inductive move_dst: Type[0] ≝ |
---|
| 4 | | PSD: register → move_dst |
---|
| 5 | | HDW: Register → move_dst. |
---|
[1161] | 6 | |
---|
[2286] | 7 | definition move_src ≝ argument move_dst. |
---|
[1241] | 8 | |
---|
[2286] | 9 | definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst. |
---|
| 10 | coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src. |
---|
[1178] | 11 | |
---|
[2286] | 12 | definition psd_argument_move_src : psd_argument → move_src ≝ |
---|
| 13 | λarg.match arg with |
---|
| 14 | [ Imm b ⇒ Imm ? b |
---|
| 15 | | Reg r ⇒ Reg ? (PSD r) |
---|
| 16 | ]. |
---|
| 17 | coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝ |
---|
| 18 | psd_argument_move_src on _a : psd_argument to move_src. |
---|
[1248] | 19 | |
---|
[2286] | 20 | inductive ertl_seq : Type[0] ≝ |
---|
| 21 | | ertl_new_frame: ertl_seq |
---|
| 22 | | ertl_del_frame: ertl_seq |
---|
| 23 | | ertl_frame_size: register → ertl_seq. |
---|
| 24 | |
---|
| 25 | definition ERTL_uns ≝ mk_unserialized_params |
---|
| 26 | (* acc_a_reg ≝ *) register |
---|
| 27 | (* acc_b_reg ≝ *) register |
---|
| 28 | (* acc_a_arg ≝ *) psd_argument |
---|
| 29 | (* acc_b_arg ≝ *) psd_argument |
---|
| 30 | (* dpl_reg ≝ *) register |
---|
| 31 | (* dph_reg ≝ *) register |
---|
| 32 | (* dpl_arg ≝ *) psd_argument |
---|
| 33 | (* dph_arg ≝ *) psd_argument |
---|
| 34 | (* snd_arg ≝ *) psd_argument |
---|
| 35 | (* pair_move ≝ *) (move_dst × move_src) |
---|
| 36 | (* call_args ≝ *) ℕ |
---|
| 37 | (* call_dest ≝ *) unit |
---|
| 38 | (* ext_seq ≝ *) ertl_seq |
---|
[2563] | 39 | (* ext_seq_labels ≝ *) (λ_.[]) |
---|
[2490] | 40 | (* has_tailcall ≝ *) false |
---|
[2604] | 41 | (* paramsT ≝ *) ℕ. |
---|
[2286] | 42 | |
---|
[2783] | 43 | definition regs_from_move_dst : move_dst → list register ≝ |
---|
| 44 | λm. match m with [PSD r ⇒ [r] | HDW _ ⇒ [ ] ]. |
---|
| 45 | |
---|
| 46 | definition regs_from_move_src : move_src → list register ≝ |
---|
| 47 | λm. match m with [Imm _ ⇒ [ ] | Reg r ⇒ match r with [PSD r1 ⇒ [r1] | HDW _ ⇒ [ ] ] ]. |
---|
| 48 | |
---|
| 49 | definition ertl_ext_seq_regs : ertl_seq → list register ≝ |
---|
| 50 | λs.match s with [ertl_frame_size r ⇒ [r] | _ ⇒ [ ]]. |
---|
| 51 | |
---|
| 52 | definition ERTL_functs ≝ mk_get_pseudo_reg_functs ERTL_uns |
---|
| 53 | (* acc_a_regs *) (λr.[r]) |
---|
| 54 | (* acc_b_regs *) (λr.[r]) |
---|
| 55 | (* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 56 | (* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 57 | (* dpl_regs *) (λr.[r]) |
---|
| 58 | (* dph_regs *) (λr.[r]) |
---|
| 59 | (* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 60 | (* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 61 | (* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 62 | (* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x))) |
---|
| 63 | (* f_call_args *) (λ_.[ ]) |
---|
| 64 | (* f_call_dest *) (λ_.[ ]) |
---|
| 65 | (* ext_seq_regs *) ertl_ext_seq_regs |
---|
| 66 | (* params_regs *) (λ_.[ ]). |
---|
| 67 | |
---|
| 68 | definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs). |
---|
[2286] | 69 | definition ertl_program ≝ joint_program ERTL. |
---|
[2946] | 70 | unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL. |
---|
[2286] | 71 | |
---|
| 72 | interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). |
---|
| 73 | |
---|
| 74 | (* aid unification *) |
---|
| 75 | unification hint 0 ≔ |
---|
| 76 | (*---------------*) ⊢ |
---|
| 77 | pair_move ERTL ≡ move_dst × move_src. |
---|
| 78 | unification hint 0 ≔ |
---|
| 79 | (*---------------*) ⊢ |
---|
| 80 | acc_a_reg ERTL ≡ register. |
---|
| 81 | unification hint 0 ≔ |
---|
| 82 | (*---------------*) ⊢ |
---|
| 83 | acc_b_reg ERTL ≡ register. |
---|
| 84 | unification hint 0 ≔ |
---|
| 85 | (*---------------*) ⊢ |
---|
| 86 | acc_a_arg ERTL ≡ psd_argument. |
---|
| 87 | unification hint 0 ≔ |
---|
| 88 | (*---------------*) ⊢ |
---|
| 89 | acc_b_arg ERTL ≡ psd_argument. |
---|
| 90 | unification hint 0 ≔ |
---|
| 91 | (*---------------*) ⊢ |
---|
| 92 | dpl_reg ERTL ≡ register. |
---|
| 93 | unification hint 0 ≔ |
---|
| 94 | (*---------------*) ⊢ |
---|
| 95 | dph_reg ERTL ≡ register. |
---|
| 96 | unification hint 0 ≔ |
---|
| 97 | (*---------------*) ⊢ |
---|
| 98 | dpl_arg ERTL ≡ psd_argument. |
---|
| 99 | unification hint 0 ≔ |
---|
| 100 | (*---------------*) ⊢ |
---|
| 101 | dph_arg ERTL ≡ psd_argument. |
---|
| 102 | unification hint 0 ≔ |
---|
| 103 | (*---------------*) ⊢ |
---|
| 104 | snd_arg ERTL ≡ psd_argument. |
---|
| 105 | unification hint 0 ≔ |
---|
| 106 | (*---------------*) ⊢ |
---|
| 107 | call_args ERTL ≡ ℕ. |
---|
| 108 | unification hint 0 ≔ |
---|
| 109 | (*---------------*) ⊢ |
---|
| 110 | call_dest ERTL ≡ unit. |
---|
| 111 | |
---|
| 112 | unification hint 0 ≔ |
---|
| 113 | (*---------------*) ⊢ |
---|
| 114 | ext_seq ERTL ≡ ertl_seq. |
---|
| 115 | |
---|
| 116 | coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝ |
---|
| 117 | psd_argument_from_reg |
---|
| 118 | on _r : register to snd_arg ERTL. |
---|
| 119 | coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝ |
---|
| 120 | psd_argument_from_byte |
---|
| 121 | on _b : Byte to snd_arg ERTL. |
---|
| 122 | |
---|
| 123 | definition ertl_seq_joint ≝ extension_seq ERTL. |
---|
| 124 | coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint |
---|
[2946] | 125 | on _s : ertl_seq to joint_seq ERTL ?. |
---|
| 126 | |
---|
| 127 | definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝ |
---|
| 128 | λp. |
---|
| 129 | let l1 : label ≝ an_identifier … one in |
---|
| 130 | let l2 : label ≝ an_identifier … (p0 one) in |
---|
| 131 | let l3 : label ≝ an_identifier … (p1 one) in |
---|
| 132 | let res ≝ |
---|
| 133 | mk_joint_internal_function ERTL (prog_var_names … p) |
---|
| 134 | (mk_universe … (p0 (p0 one))) |
---|
| 135 | (mk_universe … one) |
---|
| 136 | it 4 0 0 (empty_map …) l1 in |
---|
| 137 | (* todo: args for main? *) |
---|
| 138 | let res ≝ add_graph … l1 |
---|
| 139 | (sequential … (COST_LABEL … (init_cost_label … p)) l2) |
---|
| 140 | res in |
---|
| 141 | let res ≝ add_graph … l2 |
---|
| 142 | (sequential … (CALL ERTL ? (inl … (prog_main … p)) 4 it) l3) |
---|
| 143 | res in |
---|
| 144 | let res ≝ add_graph … l3 |
---|
| 145 | (GOTO ? l3) |
---|
| 146 | res in |
---|
| 147 | res. |
---|
| 148 | % |
---|
| 149 | [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct |
---|
| 150 | % |
---|
| 151 | [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
---|
| 152 | |2: % |
---|
| 153 | |4,6: % whd in ⊢ (??%%→?); #EQ destruct |
---|
| 154 | ] |
---|
| 155 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
---|
| 156 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
---|
| 157 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
---|
| 158 | | %{l2} %{(init_cost_label … p)} % |
---|
| 159 | ] |
---|
| 160 | qed. |
---|