Changeset 2275 for src/ASM


Ignore:
Timestamp:
Jul 30, 2012, 1:05:55 PM (7 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1987 r2275  
    44include "ASM/String.ma".
    55include "ASM/ASM.ma".
    6 include "ASM/Arithmetic.ma".
    7 include "common/ByteValues.ma".
    8 include "ASM/BitVectorTrie.ma".
     6include "ASM/Arithmetic.ma". 
    97
    108definition int_size ≝ bitvector_of_nat 8 1.
     
    195193qed.
    196194
    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  
    204195record Eval: Type[0] ≝
    205196{
Note: See TracChangeset for help on using the changeset viewer.