summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2018-02-14 17:13:29 +0000
committerBrian Campbell2018-02-14 17:13:29 +0000
commit4fd52d03967cc4e5609378dd59d9307991f2271d (patch)
treeff3d4f505cb5d0b8c680f483fc2ab43e1dbfd3be /src
parent23e4a6318260b38be4549ec7bbfab76dbb5eab13 (diff)
Another mono rewrite for aarch64
Diffstat (limited to 'src')
-rw-r--r--src/monomorphise.ml4
1 files changed, 4 insertions, 0 deletions
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)