Changeset 1514 for src/ASM/Interpret.ma

Timestamp:

Nov 17, 2011, 5:41:08 PM (8 years ago)

Author:

mulligan

Message:

changes from today. matita keeps dieing

File:

• src/ASM/Interpret.ma (modified) (1 diff)

src/ASM/Interpret.ma

@@ -582 +582 @@
               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
               let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
-              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
+              let new_addr ≝ \snd (half_add ? dptr big_acc) in
               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
                 set_8051_sfr ? s SFR_ACC_A result
             | ACC_PC ⇒ λacc_pc: True.
               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
-              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
+              let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
               (* DPM: Under specified: does the carry from PC incrementation affect the *)
               (*      addition of the PC with the DPTR? At the moment, no.              *)
               let s ≝ set_program_counter ? s inc_pc in
-              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
+              let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
                 set_8051_sfr ? s SFR_ACC_A result