Changeset 2275 for src/ASM

Timestamp:

Jul 30, 2012, 1:05:55 PM (8 years ago)

Author:

tranquil

Message:

• moved around some code (I8051.ma does not depend on ByteValues?.ma anymore, rather the other way around)
• proposed reimplementation of beval with pointer arithmetics and stuff

File:

• src/ASM/I8051.ma (modified) (2 diffs)

src/ASM/I8051.ma

@@ -4 +4 @@
 include "ASM/String.ma".
 include "ASM/ASM.ma".
-include "ASM/Arithmetic.ma".
-include "common/ByteValues.ma".
-include "ASM/BitVectorTrie.ma".
+include "ASM/Arithmetic.ma".  
 
 definition int_size ≝ bitvector_of_nat 8 1.
@@ -195 +193 @@
 qed.
 
-definition hw_register_env ≝ BitVectorTrie beval 6.
-definition empty_hw_register_env: hw_register_env ≝ Stub ….
-definition hwreg_retrieve: hw_register_env → Register → beval ≝
- λenv,r. lookup … (bitvector_of_register r) env BVundef.
-definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
- λr,v,env. insert … (bitvector_of_register r) v env.
-  
 record Eval: Type[0] ≝
 {