Changeset 3040
- Timestamp:
- Mar 29, 2013, 5:51:40 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LINToASM.ma
r3039 r3040 88 88 89 89 definition start_funct_translation : 90 ∀globals .(ident × (joint_function LIN globals)) →90 ∀globals,functions.(ident × (joint_function LIN globals functions)) → 91 91 state_monad ASM_universe unit ≝ 92 λg, id_f,u.92 λg,functs,id_f,u. 93 93 〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u) 94 94 (fresh_cost_label … u), it〉. … … 244 244 | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 245 245 | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 246 | ADDRESS id proof _ _ ⇒246 | ADDRESS id proof off _ _ ⇒ 247 247 ! Id ← Identifier_of_ident … id ; 248 return (Mov (inl ?? DPTR) Id (bv_zero ?))248 return (Mov (inl ?? DPTR) Id off) 249 249 | SET_CARRY ⇒ 250 250 return Instruction (SETB ? CARRY) … … 339 339 340 340 definition translate_fun_def ≝ 341 λglobals .342 λid_def : ident × (joint_function LIN globals ).341 λglobals,functions. 342 λid_def : ident × (joint_function LIN globals functions). 343 343 !_ start_funct_translation … id_def ; 344 344 (* ^ modify current function id ^ *)
Note: See TracChangeset
for help on using the changeset viewer.