summaryrefslogtreecommitdiff
path: root/src/gen_lib/sail_operators_mwords.lem
diff options
context:
space:
mode:
authorRobert Norton2018-04-18 11:50:34 +0100
committerRobert Norton2018-04-18 11:50:34 +0100
commit6241cb04b8500e52413ab5b84737247cbfe44d45 (patch)
tree9c0b0ef077b2be39b81a55c4741543be929b870d /src/gen_lib/sail_operators_mwords.lem
parenta7df7fd3b7e99067c9e9bb76cd1b28a42d38cb12 (diff)
parent1896c2d61b25563496e5e06413f03771c7d74b9d (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.lem6
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