diff options
| -rw-r--r-- | src/gen_lib/sail2_operators_bitlists.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_mwords.lem | 7 |
2 files changed, 10 insertions, 0 deletions
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 |