Changeset 2247 for src/ASM/Test.ma

Timestamp:

Jul 24, 2012, 6:00:48 PM (9 years ago)

Author:

mulligan

Message:

Work on the MOV instruction from today and bug fixes in set_arg_1.

File:

• src/ASM/Test.ma (modified) (4 diffs)

src/ASM/Test.ma

@@ -1133 +1133 @@
   match addr with
   [ BIT_ADDR b ⇒
-    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
     match head' … bit_1 with
     [ true ⇒
@@ -1162 +1162 @@
   match addr with
   [ BIT_ADDR b ⇒
-    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
     match head' … bit_1 with
     [ true ⇒
@@ -1211 +1211 @@
     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
       [ BIT_ADDR b ⇒ λbit_addr: True.
-        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
         match head' … bit_1 with
         [ true ⇒
@@ -1245 +1245 @@
     >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
   |2,3:
-    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
-    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     >p normalize nodelta >p1 normalize nodelta
     #map_bit_address_assm_1 #map_bit_address_assm_2