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

Moved definitions around so related are grouped together.

File:
1 edited

Legend:

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

    r289 r290  
    410410    nrepeat (napply (less_than_or_equal_monotone ? ?)).
    411411    napply (less_than_or_equal_zero).
     412nqed.
     413
     414ndefinition set_flags ≝
     415  λs: Status.
     416  λcy: Bit.
     417  λac: Maybe Bit.
     418  λov: Bit.
     419    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
     420    let old_cy ≝ get_index … nu Z ? in
     421    let old_ac ≝ get_index … nu one ? in
     422    let old_fo ≝ get_index … nu two ? in
     423    let old_rs1 ≝ get_index … nu three ? in
     424    let old_rs0 ≝ get_index … nl Z ? in
     425    let old_ov ≝ get_index … nl one ? in
     426    let old_ud ≝ get_index … nl two ? in
     427    let old_p ≝ get_index … nl three ? in
     428    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
     429    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
     430                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
     431      set_8051_sfr s SFR_PSW new_psw.
     432    ##[##1,2,3,4,5,6,7,8:
     433        nnormalize;
     434        nrepeat (napply less_than_or_equal_monotone);
     435        napply (less_than_or_equal_zero);
     436    ##]
    412437nqed.
    413438
     
    600625      set_low_internal_ram s new_low_internal_ram.
    601626     
    602 ndefinition 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     ##]
    625 nqed.
    626      
    627627ndefinition read_at_stack_pointer ≝
    628628  λs: Status.
Note: See TracChangeset for help on using the changeset viewer.