Changeset 1511 for src/ASM/Interpret.ma

Timestamp:

Nov 16, 2011, 5:35:24 PM (8 years ago)

Author:

mulligan

Message:

proofs, added, changes to execute_1_0 function therefore required to remove excess lets

File:

• src/ASM/Interpret.ma (modified) (5 diffs)

src/ASM/Interpret.ma

@@ -545 +545 @@
           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
             [ ADDR11 a ⇒ λaddr11: True.
-              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
+              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
+              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
+              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
               let s ≝ write_at_stack_pointer ? s pc_bl in
-              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
+              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
               let s ≝ write_at_stack_pointer ? s pc_bu in
-              let 〈thr, eig〉 ≝ split ? 3 8 a in
-              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
+              let thr ≝ \fst (split ? 3 8 a) in
+              let eig ≝ \snd (split ? 3 8 a) in
+              let fiv ≝ \fst (split ? 5 3 pc_bu) in
+              let thr' ≝ \snd (split ? 5 3 pc_bu) in
               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
                 set_program_counter ? s new_addr
@@ -562 +565 @@
           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
             [ ADDR16 a ⇒ λaddr16: True.
-              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
+              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
+              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
+              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
               let s ≝ write_at_stack_pointer ? s pc_bl in
-              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
+              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
               let s ≝ set_8051_sfr ? s SFR_SP new_sp in
               let s ≝ write_at_stack_pointer ? s pc_bu in
@@ -596 +600 @@
           let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
           let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
-          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
-          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
+          let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
+          let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
             set_program_counter ? s new_pc
         | LJMP addr ⇒
@@ -610 +614 @@
           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
             [ RELATIVE r ⇒ λrelative: True.
-                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
+                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
                   set_program_counter ? s new_pc
             | _ ⇒ λother: False. ⊥
@@ -618 +622 @@
           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
             [ ADDR11 a ⇒ λaddr11: True.
-              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
-              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
+              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
+              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
+              let nu ≝ \fst (split ? 4 4 pc_bu) in
+              let nl ≝ \snd (split ? 4 4 pc_bu) in
               let bit ≝ get_index' ? O ? nl in
-              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
+              let relevant1 ≝ \fst (split ? 3 8 a) in
+              let relevant2 ≝ \snd (split ? 3 8 a) in
               let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
-              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
+              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
                 set_program_counter ? s new_pc
             | _ ⇒ λother: False. ⊥