From 7da62ecee7d9eb2d16d42f9f8c5a5910b0950849 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 15 Mar 2019 14:41:16 +0000
Subject: Lem: Add missing implementations of vector_truncateLSB

---
 src/gen_lib/sail2_operators_bitlists.lem | 3 +++
 src/gen_lib/sail2_operators_mwords.lem   | 7 +++++++
 2 files changed, 10 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index bacf59e7..8b75fa38 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -41,6 +41,9 @@ let zeros len = repeat [B0] len
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
+val vector_truncateLSB : list bitU -> integer -> list bitU
+let vector_truncateLSB bs len = take_list len bs
+
 val vec_of_bits_maybe    : list bitU -> maybe (list bitU)
 val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
 val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index d47d9b40..181fa149 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -82,6 +82,13 @@ let zeros _ = Machine_word.wordFromNatural 0
 val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let vector_truncate w _ = Machine_word.zeroExtend w
 
+val vector_truncateLSB : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let vector_truncateLSB w len =
+  let len = nat_of_int len in
+  let lo = Machine_word.word_length w - len in
+  let hi = lo + len - 1 in
+  Machine_word.word_extract lo hi w
+
 val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
 let concat_vec = Machine_word.word_concat
 
-- 
cgit v1.2.3