- Timestamp:
- Jul 30, 2012, 1:05:55 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/I8051.ma
r1987 r2275 4 4 include "ASM/String.ma". 5 5 include "ASM/ASM.ma". 6 include "ASM/Arithmetic.ma". 7 include "common/ByteValues.ma". 8 include "ASM/BitVectorTrie.ma". 6 include "ASM/Arithmetic.ma". 9 7 10 8 definition int_size ≝ bitvector_of_nat 8 1. … … 195 193 qed. 196 194 197 definition hw_register_env ≝ BitVectorTrie beval 6.198 definition empty_hw_register_env: hw_register_env ≝ Stub ….199 definition hwreg_retrieve: hw_register_env → Register → beval ≝200 λenv,r. lookup … (bitvector_of_register r) env BVundef.201 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝202 λr,v,env. insert … (bitvector_of_register r) v env.203 204 195 record Eval: Type[0] ≝ 205 196 {
Note: See TracChangeset
for help on using the changeset viewer.