summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-18 19:17:30 +0000
committerAlasdair Armstrong2018-01-18 19:17:30 +0000
commit4baf8922637537e7f6594c79fdb00cf931f1232b (patch)
treeb90c68d1c0685e437bb6f18ed6d4fb82a5230940 /lib
parent0fa42d315e20f819af93c2a822ab1bc032dc4535 (diff)
parent373b081bc4b9669bbc17accf24e0dd392489f762 (diff)
Merge remote-tracking branch 'origin/experiments' into sail2
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)
+}