Changeset 3104 for src/ASM/ASM.ma

Timestamp:

Apr 6, 2013, 6:37:17 PM (7 years ago)

Author:

sacerdot

Message:

Performance improvement.

File:

• src/ASM/ASM.ma (modified) (3 diffs)

src/ASM/ASM.ma

@@ -1177 +1177 @@
   (foldl_strong ?
    (λprefix.
-     Σres: nat × (BitVectorTrie Byte 16).
-      let 〈i,mem〉 ≝ res in
-      i = |prefix| ∧
+     Σres: nat × Word × (BitVectorTrie Byte 16).
+      let 〈i,bvi,mem〉 ≝ res in
+      i = |prefix| ∧ bvi = bitvector_of_nat … i ∧
       (i ≤ 2^16 →
         ∀pc. ∀pc_ok: pc < |prefix|.
@@ -1185 +1185 @@
    program 
    (λprefix,v,tl,prf,i_mem.
-     let 〈i,mem〉 ≝ i_mem in
-      〈S i,insert … (bitvector_of_nat … i) v mem〉)
-  〈0,Stub Byte 16〉).
-[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
-| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
-| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
-  [ >length_append >H1 normalize //
+     let 〈i,bvi,mem〉 ≝ i_mem in
+      〈S i,increment … bvi,insert … bvi v mem〉)
+  〈0,zero ?,Stub Byte 16〉).
+[3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2
+| % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*)
+| cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ)
+  cases H -H * #H1 #H3 #H2 destruct (p1) %
+  [ % [ >length_append >H1 normalize //
+      | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ]
   | #LE #pc #pc_ok
     cases (le_to_or_lt_eq … pc_ok)
@@ -1198 +1200 @@
       #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
       <H1 <plus_n_O whd in ⊢ (???%); //
-    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
+    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix
+      [2: /2 by lt_plus_to_lt_l/]
       >H2 [2: @(transitive_le … LE) //]
       cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
-      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
+      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3
       #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
       @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]