Changeset 3102

Timestamp:

Apr 6, 2013, 4:11:42 PM (8 years ago)

Author:

mckinna

Message:

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

File:

• src/ASM/ASMCosts.ma (modified) (7 diffs)

src/ASM/ASMCosts.ma

@@ -121 +121 @@
     change with (? → if eq_bv ??? then ? else ? = ?)
     #assm
-    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
+    cases (le_to_or_lt_eq … (nat_of_bitvector ? e) bound' ?)
     [1:
       #e_lt_assm
@@ -271 +271 @@
   ∀classify_assm: ASM_classify0 instruction = cl_other.
   ∀pi1 : ℕ.
-   (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with 
+   (if match lookup_opt ?? program_counter''' (costlabels prog) with 
          [None ⇒ true
          |Some _ ⇒ false
@@ -405 +405 @@
   change with (ASM_classify0 ? = ?) in classifier_assm;
   whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
-  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
   <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
 qed.
@@ -463 +462 @@
   change with (ASM_classify0 ? = ?) in classifier_assm;
   whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
-  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
   <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
 qed.
@@ -483 +481 @@
   ∀classify_assm: ASM_classify0 instruction = cl_call.
   (∀pi1:ℕ
-  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
+  .if match lookup_opt ?? program_counter'' (costlabels prog) with 
       [None ⇒ true | Some _ ⇒ false] 
    then (∀start_status0:Status (cm prog)
@@ -600 +598 @@
   try (change with (ASM_classify0 ? = ?) in classifier_assm;)
   whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
-  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
   <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
   #absurd destruct(absurd)
@@ -665 +662 @@
   try (change with (ASM_classify0 ? = ?) in classifier_assm;)
   whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
-  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
   <FETCH in classifier_assm; >classify_assm
   #absurd try (destruct(absurd))