Changeset 2679

Timestamp:

Feb 19, 2013, 3:15:41 PM (7 years ago)

Author:

mckinna

Message:

Further tweak to Brian's changes: no normalization reqd at all!

File:

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

src/ASM/ASMCosts.ma

@@ -635 +635 @@
     #classifier_assm
     destruct @⊥
-    try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
-    try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
-    cases (current_instruction ??) in classifier_assm; normalize #A #B try #C destruct
-    cases A in B; normalize #D try #E try #F destruct
+    change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
+    cases (current_instruction ??) in classifier_assm;
+    [8:
+      #preinstruction cases preinstruction
+    ]
+    try(#addr1 #addr2 #absurd destruct(absurd))
+    try(#addr #absurd destruct(absurd))
+    #absurd destruct(absurd)
   |5:
     #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
@@ -652 +656 @@
   try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
   try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
-  (*
-  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
-  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;