summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorBrian Campbell2018-01-16 11:32:50 +0000
committerBrian Campbell2018-01-16 11:32:50 +0000
commit4d0162a5dbeea6286fbeecdc3cec3b4e55fada8c (patch)
tree1daebda2367540ff866607e941ece5e02250d3fc /lib
parentb4c367435b335f6a7160ed379408425c66c39ae1 (diff)
Another useful monomorphisation rewrite
Diffstat (limited to 'lib')
-rw-r--r--lib/mono_rewrites.sail8
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index a72cdd79..144b7ae0 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -110,3 +110,11 @@ function sext_slice(xs,i,l) = {
let xs = (xs & slice_mask(i,l)) >> i in
extsv(xs)
}
+
+val UInt_slice : forall 'n, 'n >= 0.
+ (bits('n), int, int) -> int effect pure
+
+function UInt_slice(xs,i,l) = {
+ let xs = (xs & slice_mask(i,l)) >> i in
+ UInt(xs)
+}