diff options
| author | Robert Norton | 2018-04-18 11:50:34 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-04-18 11:50:34 +0100 |
| commit | 6241cb04b8500e52413ab5b84737247cbfe44d45 (patch) | |
| tree | 9c0b0ef077b2be39b81a55c4741543be929b870d /src/gen_lib/sail_operators_mwords.lem | |
| parent | a7df7fd3b7e99067c9e9bb76cd1b28a42d38cb12 (diff) | |
| parent | 1896c2d61b25563496e5e06413f03771c7d74b9d (diff) | |
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/gen_lib/sail_operators_mwords.lem')
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 79b7674e..e3e1151a 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -70,6 +70,12 @@ let extz_vec _ w = Machine_word.zeroExtend w val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b let exts_vec _ w = Machine_word.signExtend w +val zero_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let zero_extend w _ = Machine_word.zeroExtend w + +val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let vector_truncate w _ = Machine_word.zeroExtend 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 |
