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/common/ByteValues.ma

    r2176 r2275  
    44
    55include "common/Pointers.ma".
     6include "ASM/I8051.ma".
     7include "ASM/BitVectorTrie.ma".
    68
    79record part (*r: region*): Type[0] ≝
     
    7476  [ O ⇒ λ_.[]
    7577  | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    76 /3/ (*Andrea: by _ cannot be re-parsed*) qed.
     78<pr >pr' <plus_n_Sm_fast
     79// qed.
    7780
    7881definition bevals_of_pointer: pointer → list beval ≝
     
    164167definition BVfalse: beval ≝ BVByte (zero …).
    165168definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse.
     169
     170definition hw_register_env ≝ BitVectorTrie beval 6.
     171definition empty_hw_register_env: hw_register_env ≝ Stub ….
     172definition hwreg_retrieve: hw_register_env → Register → beval ≝
     173 λenv,r. lookup … (bitvector_of_register r) env BVundef.
     174definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     175 λr,v,env. insert … (bitvector_of_register r) v env.
Note: See TracChangeset for help on using the changeset viewer.