Changeset 287


Ignore:
Timestamp:
Nov 25, 2010, 11:49:27 AM (9 years ago)
Author:
mulligan
Message:

Reading at stack pointer added.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Status.ma

    r286 r287  
    248248ndefinition set_code_memory ≝
    249249  λs: Status.
    250   λi: SFR8052.
    251250  λr: BitVectorTrie Byte sixteen.
    252     let index ≝ sfr_8052_index i in
    253251    let old_low_internal_ram ≝ low_internal_ram s in
    254252    let old_high_internal_ram ≝ high_internal_ram s in
     
    271269ndefinition set_low_internal_ram ≝
    272270  λs: Status.
    273   λi: SFR8052.
    274271  λr: BitVectorTrie Byte seven.
    275     let index ≝ sfr_8052_index i in
    276272    let old_code_memory ≝ code_memory s in
    277273    let old_high_internal_ram ≝ high_internal_ram s in
     
    294290ndefinition set_high_internal_ram ≝
    295291  λs: Status.
    296   λi: SFR8052.
    297292  λr: BitVectorTrie Byte seven.
    298     let index ≝ sfr_8052_index i in
    299293    let old_code_memory ≝ code_memory s in
    300294    let old_low_internal_ram ≝ low_internal_ram s in
     
    590584    napply less_than_or_equal_zero.
    591585nqed.
     586
     587ndefinition get_register ≝
     588  λs: Status.
     589  λb, c, d: Bit.
     590    let address ≝ bit_address_of_register s b c d in
     591      lookup … address (low_internal_ram s) (zero eight).
     592     
     593ndefinition set_register ≝
     594  λs: Status.
     595  λb, c, d: Bit.
     596  λv: Byte.
     597    let address ≝ bit_address_of_register s b c d in
     598    let old_low_internal_ram ≝ low_internal_ram s in
     599    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
     600      set_low_internal_ram s new_low_internal_ram.
     601     
     602ndefinition read_at_stack_pointer ≝
     603  λs: Status.
     604    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
     605    let m ≝ get_index … nu Z ? in
     606    let r1 ≝ get_index … nu one ? in
     607    let r2 ≝ get_index … nu two ? in
     608    let r3 ≝ get_index … nu three ? in
     609    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
     610    let memory ≝
     611      if m then
     612        (low_internal_ram s)
     613      else
     614        (high_internal_ram s)
     615    in
     616      lookup … address memory (zero eight).
     617    ##[##1,2,3,4:
     618        nnormalize;
     619        nrepeat (napply less_than_or_equal_monotone);
     620        napply less_than_or_equal_zero;
     621    ##]
     622nqed.
Note: See TracChangeset for help on using the changeset viewer.