Changeset 288


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

Set flags implemented.

File:
1 edited

Legend:

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

    r287 r288  
    600600      set_low_internal_ram s new_low_internal_ram.
    601601     
     602ndefinition set_flags ≝
     603  λs: Status.
     604  λcy: Bit.
     605  λac: Maybe Bit.
     606  λov: Bit.
     607    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
     608    let old_cy ≝ get_index … nu Z ? in
     609    let old_ac ≝ get_index … nu one ? in
     610    let old_fo ≝ get_index … nu two ? in
     611    let old_rs1 ≝ get_index … nu three ? in
     612    let old_rs0 ≝ get_index … nl Z ? in
     613    let old_ov ≝ get_index … nl one ? in
     614    let old_ud ≝ get_index … nl two ? in
     615    let old_p ≝ get_index … nl three ? in
     616    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
     617    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
     618                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
     619      set_8051_sfr s SFR_PSW new_psw.
     620    ##[##1,2,3,4,5,6,7,8:
     621        nnormalize;
     622        nrepeat (napply less_than_or_equal_monotone);
     623        napply (less_than_or_equal_zero);
     624    ##]
     625nqed.
     626     
    602627ndefinition read_at_stack_pointer ≝
    603628  λs: Status.
     
    621646    ##]
    622647nqed.
     648
     649ndefinition write_as_stack_pointer ≝
     650  λs: Status.
     651  λv: Byte.
     652    ?.
Note: See TracChangeset for help on using the changeset viewer.