Changeset 3100

Timestamp:

Apr 6, 2013, 4:05:46 PM (8 years ago)

Author:

mckinna

Message:

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

File:

• src/ASM/AbstractStatus.ma (modified) (2 diffs)

src/ASM/AbstractStatus.ma

@@ -34 +34 @@
    ].
 
+
+(* JHM: redundant, save for the cost of an additional normalization step in ASMCosts.ma *
 definition current_instruction0 ≝
   λcode_memory: BitVectorTrie Byte 16.
   λprogram_counter: Word.
     \fst (\fst (fetch … code_memory program_counter)).
+*)
 
 definition current_instruction ≝
   λcode_memory.
-  λs: Status code_memory.
-    current_instruction0 code_memory (program_counter … s).
+  λs: Status code_memory. 
+(* current_instruction0 code_memory (program_counter … s) *)
+    \fst (\fst (fetch … code_memory (program_counter … s))).
     
 definition current_instruction_label ≝
   λcode_memory.
-  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_labels: costlabel_map.
   λs: Status code_memory.
   let pc ≝ program_counter … code_memory s in
@@ -60 +64 @@
 
 definition word_deqset: DeqSet ≝
-  mk_DeqSet Word (eq_bv 16) ?.
+  mk_DeqSet Word (eq_bv ?) ?.
   @refl_iff_eq_bv_true
 qed.