Changeset 3100


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

Removed redundant defn of current_instruction0,
which only appears in redundnant normalization steps in ASMCosts.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AbstractStatus.ma

    r2899 r3100  
    3434   ].
    3535
     36
     37(* JHM: redundant, save for the cost of an additional normalization step in ASMCosts.ma *
    3638definition current_instruction0 ≝
    3739  λcode_memory: BitVectorTrie Byte 16.
    3840  λprogram_counter: Word.
    3941    \fst (\fst (fetch … code_memory program_counter)).
     42*)
    4043
    4144definition current_instruction ≝
    4245  λcode_memory.
    43   λs: Status code_memory.
    44     current_instruction0 code_memory (program_counter … s).
     46  λs: Status code_memory.
     47(* current_instruction0 code_memory (program_counter … s) *)
     48    \fst (\fst (fetch … code_memory (program_counter … s))).
    4549   
    4650definition current_instruction_label ≝
    4751  λcode_memory.
    48   λcost_labels: BitVectorTrie costlabel 16.
     52  λcost_labels: costlabel_map.
    4953  λs: Status code_memory.
    5054  let pc ≝ program_counter … code_memory s in
     
    6064
    6165definition word_deqset: DeqSet ≝
    62   mk_DeqSet Word (eq_bv 16) ?.
     66  mk_DeqSet Word (eq_bv ?) ?.
    6367  @refl_iff_eq_bv_true
    6468qed.
Note: See TracChangeset for help on using the changeset viewer.