Changeset 289


Ignore:
Timestamp:
Nov 25, 2010, 12:47:30 PM (9 years ago)
Author:
mulligan
Message:

Writing at stack pointer implemented.

File:
1 edited

Legend:

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

    r288 r289  
    647647nqed.
    648648
    649 ndefinition write_as_stack_pointer ≝
     649ndefinition write_at_stack_pointer ≝
    650650  λs: Status.
    651651  λv: Byte.
    652     ?.
     652    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
     653    let bit_zero ≝ get_index … nu Z ? in
     654    let bit_one ≝ get_index … nu one ? in
     655    let bit_two ≝ get_index … nu two ? in
     656    let bit_three ≝ get_index … nu three ? in
     657      if bit_zero then
     658        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     659                              v (low_internal_ram s) in
     660          set_low_internal_ram s memory
     661      else
     662        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     663                              v (high_internal_ram s) in
     664          set_high_internal_ram s memory.
     665    ##[##1,2,3,4:
     666        nnormalize;
     667        nrepeat (napply less_than_or_equal_monotone);
     668        napply less_than_or_equal_zero;
     669    ##]
     670nqed.
Note: See TracChangeset for help on using the changeset viewer.