Changeset 2261


Ignore:
Timestamp:
Jul 25, 2012, 5:04:33 PM (7 years ago)
Author:
mulligan
Message:

Resolved conflict

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2260 r2261  
    22292229      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    22302230    ]
    2231   |*)42: (* PUSH *)
     2231  |42: (* PUSH *)
    22322232    >EQP -P normalize nodelta lapply instr_refl
    22332233    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
     
    22482248    |2:
    22492249      >EQs >EQticks <instr_refl
    2250       XXX
    2251     ]
    2252   |46: (* RET *)
    2253     >EQP -P normalize nodelta
    2254     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    2255     whd in maps_assm:(??%%); normalize nodelta in maps_assm;
    2256     lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
    2257     inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
    2258     [2: normalize nodelta #absurd destruct(absurd) ]
    2259     inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
    2260     [2: normalize nodelta #absurd destruct(absurd) ]
    2261     normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
    2262     whd in ⊢ (??%?);
    2263     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    2264     whd in ⊢ (??%?);
    2265     @(pair_replace ?????????? p) normalize nodelta
    2266     >EQs >EQticks <instr_refl
    2267     [1:
    2268       @eq_f3 try %
    2269       @sym_eq @(pose … (set_clock ????)) #status #status_refl
    2270       @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
    2271     |2:
    2272       @(pair_replace ?????????? p1) normalize nodelta
    2273       >EQs >EQticks <instr_refl
    2274       [1:
    2275         @eq_f3 try %
    2276         @sym_eq @(pose … (set_clock ????)) #status #status_refl
    2277         @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
    2278         [1:
    2279           cases daemon
    2280           (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
    2281         |2:
    2282           whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    2283           whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
    2284           whd in match sfr_8051_index; normalize nodelta
    2285           >get_index_v_set_index_hit
    2286           change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
    2287           cases daemon
    2288           (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
    2289         ]
    2290       |2:
    2291         cases daemon (* XXX *)
    2292       ]
    2293     ]
    2294   |47: (* POP *)
    2295   |48: (* XCH *)
     2250      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
     2251    ]
     2252  |*)43: (* POP *)
     2253  |44:
    22962254    >EQP -P normalize nodelta
    22972255    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     
    23142272      [1:
    23152273        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2316         [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
     2274        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
    23172275      |2:
    23182276        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2319         [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
     2277        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
    23202278      ]
    23212279    |2:
     
    23442302      ]
    23452303    ]
    2346   |49: (* XCHD *)
     2304  |45: (* XCHD *)
    23472305    >EQP -P normalize nodelta
    23482306    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     
    23722330        [1:
    23732331          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2374           [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
     2332          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
    23752333        |2:
    23762334          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2377           [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
     2335          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
    23782336        ]
    23792337      |2:
     
    24172375      ]
    24182376    ]
     2377  |46: (* RET *)
     2378    >EQP -P normalize nodelta
     2379    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     2380    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
     2381    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
     2382    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
     2383    [2: normalize nodelta #absurd destruct(absurd) ]
     2384    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
     2385    [2: normalize nodelta #absurd destruct(absurd) ]
     2386    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
     2387    whd in ⊢ (??%?);
     2388    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     2389    whd in ⊢ (??%?);
     2390    @(pair_replace ?????????? p) normalize nodelta
     2391    >EQs >EQticks <instr_refl
     2392    [1:
     2393      @eq_f3 try %
     2394      @sym_eq @(pose … (set_clock ????)) #status #status_refl
     2395      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
     2396    |2:
     2397      @(pair_replace ?????????? p1) normalize nodelta
     2398      >EQs >EQticks <instr_refl
     2399      [1:
     2400        @eq_f3 try %
     2401        @sym_eq @(pose … (set_clock ????)) #status #status_refl
     2402        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
     2403        [1:
     2404          cases daemon
     2405          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2406        |2:
     2407          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     2408          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
     2409          whd in match sfr_8051_index; normalize nodelta
     2410          >get_index_v_set_index_hit
     2411          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
     2412          cases daemon
     2413          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
     2414        ]
     2415      |2:
     2416        cases daemon (* XXX *)
     2417      ]
     2418    ]
     2419  |47: (* POP *)
     2420  |48: (* XCH *)
     2421  |49: (* XCHD *)
    24192422  |50: (* RET *)
    24202423  |51: (* RETI *)
Note: See TracChangeset for help on using the changeset viewer.