From 1bb6e8a4333f204f1f9a65e741f1ae91cda399dc Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 8 Aug 2019 15:00:14 +0100
Subject: Fix machine words again

---
 src/toFromInterp_lib_mword.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/toFromInterp_lib_mword.ml b/src/toFromInterp_lib_mword.ml
index 928a56a0..21d3a38c 100644
--- a/src/toFromInterp_lib_mword.ml
+++ b/src/toFromInterp_lib_mword.ml
@@ -116,12 +116,12 @@ let bitToInterpValue = zbitToInterpValue
 let zbitvectorFromInterpValue typq_'n typq_'ord v = match v with
   | V_vector vs ->
      assert (Big_int.of_int (List.length vs) = typq_'n);
-     List.map bitFromInterpValue vs
-  | _ -> failwith "invalid interpreter value for vector"
+     Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs)
+  | _ -> failwith "invalid interpreter value for bitvector"
 
 let zbitvectorToInterpValue typq_'n typq_'ord v =
-  assert (Big_int.of_int (List.length v) = typq_'n);
-  V_vector (List.map bitToInterpValue v)
+  let bs = Lem.bitlistFromWord v in
+  V_vector (List.map (fun b -> Sail_lib.bit_of_bool b |> bitToInterpValue) bs)
 
 let bitvectorFromInterpValue = zbitvectorFromInterpValue
 let bitvectorToInterpValue = zbitvectorToInterpValue
@@ -135,7 +135,6 @@ let optionToInterpValue typq_'a v = match v with
   | None -> V_ctor ("None", [(unitToInterpValue ())])
   | Some (v0) -> V_ctor ("Some", [(typq_'a v0)])
 
-
 let bitsFromInterpValue v = match v with
   | V_vector vs ->
      Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs)
-- 
cgit v1.2.3