Changeset 1514 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 17, 2011, 5:41:08 PM (8 years ago)
Author:
mulligan
Message:

changes from today. matita keeps dieing

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1511 r1514  
    582582              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    583583              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    584               let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     584              let new_addr ≝ \snd (half_add ? dptr big_acc) in
    585585              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    586586                set_8051_sfr ? s SFR_ACC_A result
    587587            | ACC_PC ⇒ λacc_pc: True.
    588588              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    589               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
     589              let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
    590590              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    591591              (*      addition of the PC with the DPTR? At the moment, no.              *)
    592592              let s ≝ set_program_counter ? s inc_pc in
    593               let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
     593              let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
    594594              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    595595                set_8051_sfr ? s SFR_ACC_A result
Note: See TracChangeset for help on using the changeset viewer.