diff options
Diffstat (limited to 'src/gen_lib/sail2_operators_mwords.lem')
| -rw-r--r-- | src/gen_lib/sail2_operators_mwords.lem | 7 |
1 files changed, 7 insertions, 0 deletions
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 |