Changeset 317


Ignore:
Timestamp:
Nov 26, 2010, 5:45:04 PM (9 years ago)
Author:
mulligan
Message:

Fixed problems with arguments of register change.

File:
1 edited

Legend:

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

    r316 r317  
    611611ndefinition bit_address_of_register ≝
    612612  λs: Status.
    613   λb, c, d: Bit.
     613  λr: BitVector three.
     614    let b ≝ get_index ? r Z ? in
     615    let c ≝ get_index ? r one ? in
     616    let d ≝ get_index ? r two ? in
    614617    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    615618    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
     
    625628    in
    626629      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
    627     nnormalize.
    628     nrepeat (napply less_than_or_equal_monotone).
    629     napply less_than_or_equal_zero.
    630     nrepeat (napply less_than_or_equal_monotone).
    631     napply less_than_or_equal_zero.
     630  ##[##1,2,3,4,5:
     631      nnormalize;
     632      nrepeat (napply less_than_or_equal_monotone);
     633      napply less_than_or_equal_zero;
     634  ##]
    632635nqed.
    633636
    634637ndefinition get_register ≝
    635638  λs: Status.
    636   λb, c, d: Bit.
    637     let address ≝ bit_address_of_register s b c d in
     639  λr: BitVector three.
     640    let address ≝ bit_address_of_register s r in
    638641      lookup … address (low_internal_ram s) (zero eight).
    639642     
    640643ndefinition set_register ≝
    641644  λs: Status.
    642   λb, c, d: Bit.
     645  λr: BitVector three.
    643646  λv: Byte.
    644     let address ≝ bit_address_of_register s b c d in
     647    let address ≝ bit_address_of_register s r in
    645648    let old_low_internal_ram ≝ low_internal_ram s in
    646649    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
     
    735738      | EXT_INDIRECT e ⇒
    736739        λext_indirect: True.
    737           let address ≝ get_register s false false e in
     740          let address ≝ get_register s [[ false; false; e ]] in
    738741          let padded_address ≝ pad eight eight address in
    739742            lookup … sixteen padded_address (external_ram s) (zero eight)
     
    762765      | INDIRECT i ⇒
    763766        λindirect: True.
    764           let 〈 nu, nl 〉 ≝ split ? four four (get_register s false false i) in
     767          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    765768          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    766769          let bit_one ≝ get_index … bit_one_v Z ? in
     
    801804      | INDIRECT i ⇒
    802805        λindirect: True.
    803           let register ≝ get_register s false false i in
     806          let register ≝ get_register s [[ false; false; i ]] in
    804807          let 〈 nu, nl 〉 ≝ split ? four four register in
    805808          let bit_one ≝ get_index ? nu one ? in
     
    813816                set_high_internal_ram s memory
    814817            ]
    815       | REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v
     818      | REGISTER r ⇒ λregister: True. set_register s r v
    816819      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
    817820      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
    818821      | EXT_INDIRECT e ⇒
    819822        λext_indirect: True.
    820           let address ≝ get_register s false false e in
     823          let address ≝ get_register s [[ false; false; e ]] in
    821824          let padded_address ≝ pad eight eight address in
    822825          let memory ≝ insert ? sixteen padded_address v (external_ram s) in
Note: See TracChangeset for help on using the changeset viewer.