Another mono rewrite for aarch64

2 files changed, 13 insertions, 0 deletions

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 167a2fdd..2958c890 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -130,6 +130,15 @@ function UInt_slice(xs,i,l) = {
   UInt(xs)
 }
 
+val UInt_subrange : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> int effect pure
+
+function UInt_subrange(xs,i,j) = {
+  let xs = (xs & slice_mask(j,i-j)) >> i in
+  UInt(xs)
+}
+
+
 val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
 
 function zext_ones(m) = {
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 4f8fc257..71efcb22 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3448,10 +3448,14 @@ let rewrite_app env typ (id,args) =
 
   else if is_id env (Id "UInt") id then
     let is_slice = is_id env (Id "slice") in
+    let is_subrange = is_id env (Id "vector_subrange") in
     match args with
     | [E_aux (E_app (slice1, [vector1; start1; length1]),_)]
         when is_slice slice1 && not (is_constant length1) ->
        E_app (mk_id "UInt_slice", [vector1; start1; length1])
+    | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)]
+        when is_subrange subrange1 && not (is_constant_range (start1,end1)) ->
+       E_app (mk_id "UInt_subrange", [vector1; start1; end1])
 
     | _ -> E_app (id,args)