Changeset 2247 for src/ASM/Test.ma
- Timestamp:
- Jul 24, 2012, 6:00:48 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2207 r2247 1133 1133 match addr with 1134 1134 [ BIT_ADDR b ⇒ 1135 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW)in1135 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in 1136 1136 match head' … bit_1 with 1137 1137 [ true ⇒ … … 1162 1162 match addr with 1163 1163 [ BIT_ADDR b ⇒ 1164 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW)in1164 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in 1165 1165 match head' … bit_1 with 1166 1166 [ true ⇒ … … 1211 1211 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with 1212 1212 [ BIT_ADDR b ⇒ λbit_addr: True. 1213 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW)in1213 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in 1214 1214 match head' … bit_1 with 1215 1215 [ true ⇒ … … 1245 1245 >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % 1246 1246 |2,3: 1247 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))1248 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta1249 1247 >p normalize nodelta >p1 normalize nodelta 1250 1248 #map_bit_address_assm_1 #map_bit_address_assm_2
Note: See TracChangeset
for help on using the changeset viewer.