Changeset 3102


Ignore:
Timestamp:
Apr 6, 2013, 4:11:42 PM (4 years ago)
Author:
mckinna
Message:

Removed redundant refs to current_instruction0,
which itself has been removed from AbstractStatus?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r3028 r3102  
    121121    change with (? → if eq_bv ??? then ? else ? = ?)
    122122    #assm
    123     cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
     123    cases (le_to_or_lt_eq … (nat_of_bitvector ? e) bound' ?)
    124124    [1:
    125125      #e_lt_assm
     
    271271  ∀classify_assm: ASM_classify0 instruction = cl_other.
    272272  ∀pi1 : ℕ.
    273    (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with 
     273   (if match lookup_opt ?? program_counter''' (costlabels prog) with 
    274274         [None ⇒ true
    275275         |Some _ ⇒ false
     
    405405  change with (ASM_classify0 ? = ?) in classifier_assm;
    406406  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    407   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    408407  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    409408qed.
     
    463462  change with (ASM_classify0 ? = ?) in classifier_assm;
    464463  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    465   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    466464  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    467465qed.
     
    483481  ∀classify_assm: ASM_classify0 instruction = cl_call.
    484482  (∀pi1:ℕ
    485   .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
     483  .if match lookup_opt ?? program_counter'' (costlabels prog) with 
    486484      [None ⇒ true | Some _ ⇒ false] 
    487485   then (∀start_status0:Status (cm prog)
     
    600598  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    601599  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    602   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    603600  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
    604601  #absurd destruct(absurd)
     
    665662  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    666663  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    667   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    668664  <FETCH in classifier_assm; >classify_assm
    669665  #absurd try (destruct(absurd))
Note: See TracChangeset for help on using the changeset viewer.