Changeset 2247 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 24, 2012, 6:00:48 PM (8 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2207 r2247  
    11331133  match addr with
    11341134  [ BIT_ADDR b ⇒
    1135     let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1135    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    11361136    match head' … bit_1 with
    11371137    [ true ⇒
     
    11621162  match addr with
    11631163  [ BIT_ADDR b ⇒
    1164     let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1164    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    11651165    match head' … bit_1 with
    11661166    [ true ⇒
     
    12111211    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
    12121212      [ BIT_ADDR b ⇒ λbit_addr: True.
    1213         let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1213        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    12141214        match head' … bit_1 with
    12151215        [ true ⇒
     
    12451245    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
    12461246  |2,3:
    1247     >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    1248     whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    12491247    >p normalize nodelta >p1 normalize nodelta
    12501248    #map_bit_address_assm_1 #map_bit_address_assm_2
Note: See TracChangeset for help on using the changeset viewer.