From 7d815832a9410a3975c6ec8438556916eab493eb Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Jul 2020 16:20:50 +0100
Subject: Define extz/s_vec in Sail for non-prover backends

---
 lib/mono_rewrites.sail | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 0702b374..1e7fe58f 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -8,9 +8,15 @@ $include <vector_dec.sail>
 
 /* External definitions not in the usual asl prelude */
 
-val extzv = "extz_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv = {lem: "extz_vec", coq: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+function extzv(m, v) = {
+  if m < 'n then truncate(v, m) else sail_zero_extend(v, m)
+}
 
-val extsv = "exts_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extsv = {lem: "exts_vec", coq: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+function extsv(m, v) = {
+  if m < 'n then truncate(v, m) else sail_sign_extend(v, m)
+}
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
-- 
cgit v1.2.3