From 74c337e3d6ff293eb9c2a39f045c2192f132d164 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 21 Apr 2017 12:43:24 +0100
Subject: implement to_vec_big using zarith extract for some speedup.

---
 src/gen_lib/sail_values.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 29f814fe..41c1fd6a 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -521,15 +521,14 @@ let to_vec_big ord len n =
   let start = if ord then 0 else len-1 in
   if eq_big_int n zero_big_int
   then Vvector(array, start, ord)
-  else if gt_big_int n zero_big_int
-  then Vvector(divide_by_2_big array (len -1) n, start, ord)
   else
-    let abs_n = abs_big_int n in
-    let abs_array = divide_by_2_big array (len-1) abs_n in
-    let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in
-    match v_abs with
-    | Vvector(array,start,ord) -> Vvector(add_one_bit array true (len-1),start,ord)
-    | _ -> assert false
+    begin
+      for i = 0 to len - 1 do
+        if ((extract_big_int n (len - 1 - i) 1) == unit_big_int) then
+          array.(i) <- Vone
+      done;
+      Vvector(array, start, ord)
+    end
 
 let to_vec_inc_int (len,n) = to_vec_int true len n
 let to_vec_dec_int (len,n) = to_vec_int false len n
-- 
cgit v1.2.3