Better conversion to 32-bit for bedrock2

c.f. #524 (comment)
mit-plv · Oct 15, 2019 · 344e403 · 344e403
1 parent 0c63685
commit 344e403
Showing 1 changed file with 10 additions and 8 deletions.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
@@ -851,14 +851,16 @@ Section with_bitwidth.
               ; (forall xl xh offset,
                     0 < offset < bitwidth
                     -> doublewidth (cstZsingle_to_double xl xh >> singlewidth ('offset))
-                       = cstZsingle_to_double
-                           (Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset)))
-                                  (singlewidth
-                                     (Z.truncating_shiftl
-                                        (singlewidth ('bitwidth))
-                                        (singlewidth xh)
-                                        (singlewidth ('(bitwidth - offset))))))
-                           (singlewidth xh >> singlewidth ('offset)))
+                       = (dlet l := singlewidth
+                                      (Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset)))
+                                             (singlewidth
+                                                (Z.truncating_shiftl
+                                                   (singlewidth ('bitwidth))
+                                                   (singlewidth xh)
+                                                   (singlewidth ('(bitwidth - offset)))))) in
+                              dlet h := singlewidth
+                                          (singlewidth xh >> singlewidth ('offset)) in
+                              cstZsingle_to_double l h))
              ]
           ].
 End with_bitwidth.