[698] | 1 | include "ASM/Util.ma". |
---|
| 2 | include "utilities/BitVectorTrieSet.ma". |
---|
| 3 | include "LIN/LIN.ma". |
---|
[2286] | 4 | include "ASM/ASM.ma". |
---|
[2708] | 5 | include "utilities/state.ma". |
---|
[1264] | 6 | |
---|
[2708] | 7 | (* utilities to provide Identifier's and addresses *) |
---|
| 8 | record ASM_universe (globals : list ident) : Type[0] := |
---|
| 9 | { id_univ : universe ASMTag |
---|
| 10 | ; current_funct : ident |
---|
| 11 | ; ident_map : identifier_map SymbolTag Identifier |
---|
| 12 | ; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier) |
---|
| 13 | ; address_map : identifier_map SymbolTag Word |
---|
| 14 | ; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map |
---|
| 15 | }. |
---|
| 16 | |
---|
| 17 | definition new_ASM_universe : |
---|
| 18 | ∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝ |
---|
| 19 | λp. |
---|
| 20 | let globals_addr_internal ≝ |
---|
| 21 | λres_offset : identifier_map SymbolTag Word × Z. |
---|
| 22 | λx_size: ident × region × nat. |
---|
| 23 | let 〈res, offset〉 ≝ res_offset in |
---|
| 24 | let 〈x, region, size〉 ≝ x_size in |
---|
| 25 | 〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in |
---|
| 26 | let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in |
---|
| 27 | mk_ASM_universe ? (mk_universe … one) |
---|
| 28 | (an_identifier … one (* dummy *)) |
---|
| 29 | (empty_map …) (empty_map …) |
---|
| 30 | (\fst addresses) ?. |
---|
| 31 | @hide_prf |
---|
| 32 | normalize nodelta |
---|
| 33 | cases p -p #vars #functs #main |
---|
| 34 | #i #H |
---|
| 35 | letin init_val ≝ (〈empty_map ? Word, OZ〉) |
---|
| 36 | cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars)) |
---|
| 37 | [ %2{H} ] -H |
---|
| 38 | lapply i -i lapply init_val -init_val elim vars -vars |
---|
| 39 | [2: ** #id #r #v #tl #IH ] #init_val #i |
---|
| 40 | [2: * [2: * ] #H @H ] |
---|
| 41 | * [2: #H cases (orb_Prop_true … H) -H ] #H |
---|
| 42 | @IH |
---|
| 43 | [ %1 cases init_val normalize nodelta #init_map #off |
---|
| 44 | >(proj1 ?? (eqb_true ???) H) @mem_set_add_id |
---|
| 45 | | %2{H} |
---|
| 46 | | %1 cases init_val in H; normalize nodelta #init_map #off #H |
---|
| 47 | >mem_set_add @orb_Prop_r @H |
---|
| 48 | ] |
---|
| 49 | qed. |
---|
| 50 | |
---|
| 51 | definition Identifier_of_label : |
---|
| 52 | ∀globals.label → state_monad (ASM_universe globals) Identifier ≝ |
---|
| 53 | λg,l,u. |
---|
| 54 | let current ≝ current_funct … u in |
---|
| 55 | let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in |
---|
| 56 | let 〈id, univ, lmap〉 ≝ |
---|
| 57 | match lookup … lmap l with |
---|
| 58 | [ Some id ⇒ 〈id, id_univ … u, lmap〉 |
---|
| 59 | | None ⇒ |
---|
| 60 | let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
| 61 | 〈id, univ, add … lmap l id〉 |
---|
| 62 | ] in |
---|
| 63 | 〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap) |
---|
| 64 | (address_map … u) (globals_are_in … u), id〉. |
---|
| 65 | |
---|
| 66 | definition Identifier_of_ident : |
---|
| 67 | ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝ |
---|
| 68 | λg,i,u. |
---|
| 69 | let imap ≝ ident_map … u in |
---|
| 70 | let 〈id, univ, imap〉 ≝ |
---|
| 71 | match lookup … imap i with |
---|
| 72 | [ Some id ⇒ 〈id, id_univ … u, imap〉 |
---|
| 73 | | None ⇒ |
---|
| 74 | let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
| 75 | 〈id, univ, add … imap i id〉 |
---|
| 76 | ] in |
---|
| 77 | 〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u) |
---|
| 78 | (address_map … u) (globals_are_in … u), id〉. |
---|
| 79 | |
---|
| 80 | definition start_funct_translation : |
---|
| 81 | ∀globals.(ident × (joint_function LIN globals)) → |
---|
| 82 | state_monad (ASM_universe globals) unit ≝ |
---|
| 83 | λg,id_f,u. |
---|
| 84 | 〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u) |
---|
| 85 | (address_map … u) (globals_are_in … u), it〉. |
---|
| 86 | |
---|
| 87 | definition address_of_ident : |
---|
| 88 | ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝ |
---|
| 89 | λglobals,i,prf,u. |
---|
| 90 | 〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed. |
---|
| 91 | |
---|
| 92 | definition ASM_fresh : |
---|
| 93 | ∀globals.state_monad (ASM_universe globals) Identifier ≝ |
---|
| 94 | λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
| 95 | 〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u) |
---|
| 96 | (address_map … u) (globals_are_in … u), id〉. |
---|
| 97 | |
---|
[2286] | 98 | definition register_address: Register → [[ acc_a; direct; registr ]] ≝ |
---|
| 99 | λr: Register. |
---|
| 100 | match r with |
---|
| 101 | [ Register00 ⇒ REGISTER [[ false; false; false ]] |
---|
| 102 | | Register01 ⇒ REGISTER [[ false; false; true ]] |
---|
| 103 | | Register02 ⇒ REGISTER [[ false; true; false ]] |
---|
| 104 | | Register03 ⇒ REGISTER [[ false; true; true ]] |
---|
| 105 | | Register04 ⇒ REGISTER [[ true; false; false ]] |
---|
| 106 | | Register05 ⇒ REGISTER [[ true; false; true ]] |
---|
| 107 | | Register06 ⇒ REGISTER [[ true; true; false ]] |
---|
| 108 | | Register07 ⇒ REGISTER [[ true; true; true ]] |
---|
| 109 | | RegisterA ⇒ ACC_A |
---|
| 110 | | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240) |
---|
| 111 | | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82) |
---|
| 112 | | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83) |
---|
| 113 | | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) |
---|
| 114 | ]. @I qed. |
---|
| 115 | |
---|
[2443] | 116 | definition vector_cast : |
---|
| 117 | ∀A,n,m.A → Vector A n → Vector A m ≝ |
---|
| 118 | λA,n,m,dflt,v. |
---|
| 119 | If leb n m then with prf do |
---|
| 120 | replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉ |
---|
| 121 | else with prf do |
---|
| 122 | \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)). |
---|
| 123 | lapply prf @(leb_elim n) |
---|
| 124 | [2,3: #_ * #abs elim (abs I) ] |
---|
| 125 | #H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …)) |
---|
| 126 | [ assumption ] |
---|
| 127 | @(transitive_le … (not_le_to_lt … H)) %2 %1 |
---|
| 128 | qed. |
---|
| 129 | |
---|
[2490] | 130 | definition arg_address : hdw_argument → |
---|
[2443] | 131 | [[ acc_a ; direct ; registr ; data ]] ≝ |
---|
[2490] | 132 | λa. |
---|
[2443] | 133 | match a |
---|
| 134 | with |
---|
[2490] | 135 | [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]]) |
---|
| 136 | | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]]) |
---|
[2443] | 137 | ]. |
---|
[2490] | 138 | [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I |
---|
[686] | 139 | qed. |
---|
[491] | 140 | |
---|
[2286] | 141 | definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). |
---|
[2443] | 142 | |
---|
[491] | 143 | definition data_of_int ≝ λbv. DATA bv. |
---|
[686] | 144 | definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). |
---|
| 145 | definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). |
---|
[491] | 146 | |
---|
[2286] | 147 | (* TODO: check and change to free bit *) |
---|
| 148 | definition asm_other_bit ≝ BIT_ADDR (zero_byte). |
---|
| 149 | |
---|
[2708] | 150 | definition translate_statements : |
---|
| 151 | ∀globals. |
---|
| 152 | joint_statement LIN globals → |
---|
| 153 | state_monad (ASM_universe globals) pseudo_instruction ≝ |
---|
| 154 | λglobals,statement. |
---|
| 155 | match statement with |
---|
[2490] | 156 | [ final instr ⇒ |
---|
[2286] | 157 | match instr with |
---|
[2708] | 158 | [ GOTO lbl ⇒ |
---|
| 159 | ! lbl' ← Identifier_of_label … lbl ; |
---|
| 160 | return Jmp (toASM_ident ? lbl) |
---|
| 161 | | RETURN ⇒ return Instruction (RET ?) |
---|
[2490] | 162 | | TAILCALL abs _ _ ⇒ Ⓧabs |
---|
[2286] | 163 | ] |
---|
[1282] | 164 | | sequential instr _ ⇒ |
---|
[2490] | 165 | match instr with |
---|
[2286] | 166 | [ step_seq instr' ⇒ |
---|
[2490] | 167 | match instr' with |
---|
| 168 | [ extension_seq ext ⇒ |
---|
[2286] | 169 | match ext with |
---|
| 170 | [ SAVE_CARRY ⇒ |
---|
[2708] | 171 | return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) |
---|
[2286] | 172 | | RESTORE_CARRY ⇒ |
---|
[2708] | 173 | return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) |
---|
| 174 | | LOW_ADDRESS reg lbl ⇒ |
---|
| 175 | ! lbl' ← Identifier_of_label … lbl ; |
---|
| 176 | return MovSuccessor (register_address reg) LOW lbl' |
---|
| 177 | | HIGH_ADDRESS reg lbl ⇒ |
---|
| 178 | ! lbl' ← Identifier_of_label … lbl ; |
---|
| 179 | return MovSuccessor (register_address reg) HIGH lbl' |
---|
[2286] | 180 | ] |
---|
[2708] | 181 | | COMMENT comment ⇒ return Comment comment |
---|
| 182 | | POP _ ⇒ return Instruction (POP ? accumulator_address) |
---|
| 183 | | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address) |
---|
| 184 | | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY) |
---|
[2490] | 185 | | OPACCS accs _ _ _ _ ⇒ |
---|
[2708] | 186 | return match accs with |
---|
[2286] | 187 | [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) |
---|
| 188 | | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) |
---|
| 189 | ] |
---|
[2490] | 190 | | OP1 op1 _ _ ⇒ |
---|
[2708] | 191 | return match op1 with |
---|
[2286] | 192 | [ Cmpl ⇒ Instruction (CPL ? ACC_A) |
---|
| 193 | | Inc ⇒ Instruction (INC ? ACC_A) |
---|
| 194 | | Rl ⇒ Instruction (RL ? ACC_A) |
---|
| 195 | ] |
---|
[2490] | 196 | | OP2 op2 _ _ reg ⇒ |
---|
[2708] | 197 | return match arg_address … reg |
---|
[2490] | 198 | return λx.is_in … [[ acc_a; |
---|
| 199 | direct; |
---|
| 200 | registr; |
---|
| 201 | data ]] x → ? with |
---|
| 202 | [ ACC_A ⇒ λacc_a: True. |
---|
| 203 | match op2 with |
---|
| 204 | [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address) |
---|
| 205 | | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address) |
---|
| 206 | | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address) |
---|
| 207 | | Xor ⇒ Instruction (CLR ? ACC_A) |
---|
| 208 | | _ ⇒ Instruction (NOP ?) |
---|
| 209 | ] |
---|
| 210 | | DIRECT d ⇒ λdirect1: True. |
---|
| 211 | match op2 with |
---|
| 212 | [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d)) |
---|
| 213 | | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d)) |
---|
| 214 | | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d)) |
---|
| 215 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 216 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 217 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) |
---|
| 218 | ] |
---|
| 219 | | REGISTER r ⇒ λregister1: True. |
---|
| 220 | match op2 with |
---|
| 221 | [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r)) |
---|
| 222 | | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r)) |
---|
| 223 | | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r)) |
---|
| 224 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 225 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 226 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) |
---|
| 227 | ] |
---|
| 228 | | DATA b ⇒ λdata : True. |
---|
| 229 | match op2 with |
---|
| 230 | [ Add ⇒ Instruction (ADD ? ACC_A (DATA b)) |
---|
| 231 | | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b)) |
---|
| 232 | | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b)) |
---|
| 233 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 234 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 235 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉)) |
---|
| 236 | ] |
---|
| 237 | | _ ⇒ Ⓧ |
---|
| 238 | ] (subaddressing_modein …) |
---|
[2708] | 239 | | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) |
---|
| 240 | | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) |
---|
[2490] | 241 | | ADDRESS addr proof _ _ ⇒ |
---|
[2708] | 242 | ! addr' ← address_of_ident … proof ; |
---|
| 243 | return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉))))) |
---|
[2490] | 244 | | SET_CARRY ⇒ |
---|
[2708] | 245 | return Instruction (SETB ? CARRY) |
---|
[2286] | 246 | | MOVE regs ⇒ |
---|
[2708] | 247 | return match regs with |
---|
[2490] | 248 | [ to_acc _ reg ⇒ |
---|
| 249 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 250 | direct; |
---|
[2490] | 251 | registr]] x → ? with |
---|
| 252 | [ REGISTER r ⇒ λregister9: True. |
---|
| 253 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) |
---|
| 254 | | DIRECT d ⇒ λdirect9: True. |
---|
| 255 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) |
---|
| 256 | | ACC_A ⇒ λacc_a: True. |
---|
| 257 | Instruction (NOP ?) |
---|
| 258 | | _ ⇒ Ⓧ |
---|
| 259 | ] (subaddressing_modein …) |
---|
| 260 | | from_acc reg _ ⇒ |
---|
| 261 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 262 | direct; |
---|
[2490] | 263 | registr ]] x → ? with |
---|
| 264 | [ REGISTER r ⇒ λregister8: True. |
---|
| 265 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) |
---|
| 266 | | ACC_A ⇒ λacc: True. |
---|
| 267 | Instruction (NOP ?) |
---|
| 268 | | DIRECT d ⇒ λdirect8: True. |
---|
| 269 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) |
---|
| 270 | | _ ⇒ Ⓧ |
---|
| 271 | ] (subaddressing_modein …) |
---|
| 272 | | int_to_reg reg b ⇒ |
---|
| 273 | match register_address reg return λx.is_in … [[ acc_a; |
---|
| 274 | direct; |
---|
| 275 | registr ]] x → ? with |
---|
| 276 | [ REGISTER r ⇒ λregister7: True. |
---|
| 277 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉)))))) |
---|
| 278 | | ACC_A ⇒ λacc: True. |
---|
| 279 | if eq_bv … (bv_zero …) b then |
---|
| 280 | Instruction (CLR ? ACC_A) |
---|
| 281 | else |
---|
| 282 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
| 283 | | DIRECT d ⇒ λdirect7: True. |
---|
| 284 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉))))) |
---|
| 285 | | _ ⇒ Ⓧ |
---|
| 286 | ] (subaddressing_modein …) |
---|
| 287 | | int_to_acc _ b ⇒ |
---|
| 288 | if eq_bv … (bv_zero …) b then |
---|
| 289 | Instruction (CLR ? ACC_A) |
---|
| 290 | else |
---|
| 291 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
[2286] | 292 | ] |
---|
| 293 | ] |
---|
[2708] | 294 | | CALL f _ _ ⇒ |
---|
| 295 | match f with |
---|
| 296 | [ inl id ⇒ |
---|
| 297 | ! id' ← Identifier_of_ident … id ; |
---|
| 298 | return Call (toASM_ident ? id') |
---|
| 299 | | inr _ ⇒ |
---|
| 300 | return Instruction (JMP … INDIRECT_DPTR) |
---|
| 301 | ] |
---|
| 302 | | COST_LABEL lbl ⇒ return Cost lbl |
---|
[2490] | 303 | | COND _ lbl ⇒ |
---|
[2708] | 304 | ! l ← Identifier_of_label … lbl; |
---|
| 305 | return Instruction (JNZ ? l) |
---|
[722] | 306 | ] |
---|
[2708] | 307 | | FCOND _ _ lbl_true lbl_false ⇒ |
---|
| 308 | ! l1 ← Identifier_of_label … lbl_true; |
---|
| 309 | ! l2 ← Identifier_of_label … lbl_false; |
---|
| 310 | return Jnz ACC_A l1 l2 |
---|
[1149] | 311 | ]. |
---|
[2443] | 312 | try @I |
---|
[686] | 313 | qed. |
---|
| 314 | |
---|
[1268] | 315 | |
---|
[723] | 316 | definition build_translated_statement ≝ |
---|
| 317 | λglobals. |
---|
[2708] | 318 | λstatement: lin_statement globals. |
---|
| 319 | ! stmt ← translate_statements globals (\snd statement) ; |
---|
| 320 | match \fst statement with |
---|
| 321 | [ Some lbl ⇒ |
---|
| 322 | ! lbl' ← Identifier_of_label globals lbl ; |
---|
| 323 | return 〈Some ? lbl', stmt〉 |
---|
| 324 | | None ⇒ |
---|
| 325 | return 〈None ?, stmt〉 |
---|
| 326 | ]. |
---|
[723] | 327 | |
---|
[686] | 328 | definition translate_code ≝ |
---|
[2708] | 329 | λglobals. |
---|
| 330 | λcode: list (lin_statement globals). |
---|
| 331 | m_list_map … (build_translated_statement globals) code. |
---|
[723] | 332 | |
---|
[696] | 333 | definition translate_fun_def ≝ |
---|
[2708] | 334 | λglobals. |
---|
| 335 | λid_def : ident × (joint_function LIN globals). |
---|
| 336 | !_ start_funct_translation … id_def ; |
---|
| 337 | (* ^ modify current function id ^ *) |
---|
| 338 | match \snd id_def with |
---|
[1268] | 339 | [ Internal int ⇒ |
---|
[2708] | 340 | let code ≝ joint_if_code … int in |
---|
| 341 | ! id ← Identifier_of_ident … (\fst id_def) ; |
---|
| 342 | ! code' ← translate_code … code ; |
---|
| 343 | match code' with |
---|
| 344 | [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *) |
---|
[1379] | 345 | | cons hd tl ⇒ |
---|
[2708] | 346 | match \fst hd with |
---|
| 347 | [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl) |
---|
| 348 | | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *) |
---|
| 349 | ] |
---|
[1379] | 350 | ] |
---|
[2708] | 351 | | External _ ⇒ return [ ] |
---|
[696] | 352 | ]. |
---|
[1515] | 353 | |
---|
[2754] | 354 | definition get_symboltable : |
---|
| 355 | ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝ |
---|
| 356 | λglobals,u. |
---|
| 357 | let imap ≝ ident_map … u in |
---|
| 358 | let f ≝ λiold,inew.cons ? 〈inew, iold〉 in |
---|
| 359 | 〈u, foldi ??? f imap [ ]〉. |
---|
| 360 | |
---|
[1995] | 361 | definition lin_to_asm : lin_program → pseudo_assembly_program ≝ |
---|
[696] | 362 | λp. |
---|
[2708] | 363 | state_run ?? (new_ASM_universe p) |
---|
| 364 | (let add_translation ≝ |
---|
| 365 | λacc,id_def. |
---|
| 366 | ! code ← translate_fun_def … id_def ; |
---|
| 367 | ! acc ← acc ; |
---|
| 368 | return (code @ acc) in |
---|
| 369 | ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ; |
---|
| 370 | ! exit_label ← ASM_fresh … ; |
---|
| 371 | ! main ← Identifier_of_ident … (prog_main … p) ; |
---|
| 372 | let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in |
---|
[2754] | 373 | ! symboltable ← get_symboltable … ; |
---|
[2708] | 374 | (* atm no data identifier is used in the code, so preamble must be empty *) |
---|
[2754] | 375 | return 〈[ ], symboltable, code〉). |
---|